From 2ca390c9c236f5a555225d0598171c6d39789daf Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Mon, 11 Oct 2021 10:50:11 +0100 Subject: [PATCH 1/4] Add comment with example strings matched or not by regex As suggested in code review. --- src/solvers/smt2_incremental/smt_terms.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/solvers/smt2_incremental/smt_terms.cpp b/src/solvers/smt2_incremental/smt_terms.cpp index 852748ce593..438fbb286e2 100644 --- a/src/solvers/smt2_incremental/smt_terms.cpp +++ b/src/solvers/smt2_incremental/smt_terms.cpp @@ -50,6 +50,8 @@ bool smt_bool_literal_termt::value() const static bool is_valid_smt_identifier(irep_idt identifier) { + // The below regex matches a complete string which does not contain the `|` + // character. So it would match the string `foo bar`, but not `|foo bar|`. static const std::regex valid{R"(^[^\|]*$)"}; return std::regex_match(id2string(identifier), valid); } From c3f1985e2f76785dba61d969b04c41250f2668b8 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Mon, 11 Oct 2021 10:50:12 +0100 Subject: [PATCH 2/4] Simplify regex used in `is_valid_smt_identifier` There are 2 simplifications here. 1) A swap to a normal string literal, rather that a raw string literal, as there is only a single character which needs escaping. 2) A change to remove the `^` and `$` for matching the start and end of the string. These were redundant, because `std::regex_match` already requires the regex to match the full string rather than a partial sub-match. This simplification is already tested by the "smt_identifier_termt construction" test in the smt_terms unit tests. --- src/solvers/smt2_incremental/smt_terms.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/smt2_incremental/smt_terms.cpp b/src/solvers/smt2_incremental/smt_terms.cpp index 438fbb286e2..9323926f5ba 100644 --- a/src/solvers/smt2_incremental/smt_terms.cpp +++ b/src/solvers/smt2_incremental/smt_terms.cpp @@ -52,7 +52,7 @@ static bool is_valid_smt_identifier(irep_idt identifier) { // The below regex matches a complete string which does not contain the `|` // character. So it would match the string `foo bar`, but not `|foo bar|`. - static const std::regex valid{R"(^[^\|]*$)"}; + static const std::regex valid{"[^\\|]*"}; return std::regex_match(id2string(identifier), valid); } From 232ecfdd101759caeba078d59230aed81f261832 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Mon, 11 Oct 2021 10:50:13 +0100 Subject: [PATCH 3/4] Add comment explaining why smt identifiers are checked Because the purpose of this INVARIANT was not neccessarily apparent without reading the doxygen in the header file. --- src/solvers/smt2_incremental/smt_terms.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/solvers/smt2_incremental/smt_terms.cpp b/src/solvers/smt2_incremental/smt_terms.cpp index 9323926f5ba..11855a2eed0 100644 --- a/src/solvers/smt2_incremental/smt_terms.cpp +++ b/src/solvers/smt2_incremental/smt_terms.cpp @@ -59,6 +59,10 @@ static bool is_valid_smt_identifier(irep_idt identifier) smt_identifier_termt::smt_identifier_termt(irep_idt identifier, smt_sortt sort) : smt_termt(ID_smt_identifier_term, std::move(sort)) { + // The below invariant exists as a sanity check that the string being used for + // the identifier is in unescaped form. This is because the escaping and + // unescaping are implementation details of the printing to string and + // response parsing respectively, not part of the underlying data. INVARIANT( is_valid_smt_identifier(identifier), R"(Identifiers may not contain | characters.)"); From 200500c98439fe653cd1a07d766b00e6a1d6cb07 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Mon, 11 Oct 2021 10:50:15 +0100 Subject: [PATCH 4/4] Rename `dependencies_needed` to `push_dependencies_needed` In order to make it more explict that this function has side-effects on the stack of expressions to be defined. --- .../smt2_incremental_decision_procedure.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 0d6661de16f..7a9cdadb37d 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -49,7 +49,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions( return expr_identifier.first; }); std::stack to_be_defined; - const auto dependencies_needed = [&](const exprt &expr) { + const auto push_dependencies_needed = [&](const exprt &expr) { bool result = false; for(const auto &dependency : gather_dependent_expressions(expr)) { @@ -60,11 +60,11 @@ void smt2_incremental_decision_proceduret::define_dependent_functions( } return result; }; - dependencies_needed(expr); + push_dependencies_needed(expr); while(!to_be_defined.empty()) { const exprt current = to_be_defined.top(); - if(dependencies_needed(current)) + if(push_dependencies_needed(current)) continue; if(const auto symbol_expr = expr_try_dynamic_cast(current)) { @@ -81,7 +81,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions( } else { - if(dependencies_needed(symbol->value)) + if(push_dependencies_needed(symbol->value)) continue; const smt_define_function_commandt function{ symbol->name, {}, convert_expr_to_smt(symbol->value)};