From 7b5fb34c8366dbf76c7756b2b3f8a7693ac66f99 Mon Sep 17 00:00:00 2001 From: Jesse Sigal Date: Fri, 21 Jul 2017 14:54:16 +0100 Subject: [PATCH 1/4] Fixed universal constraints that break invariants. In preparation for checking the invariant of universal constraints, all violations have been fixed. Additionally, an `indexOf` axiom had an off-by-one error and the contains regression test was missing a `--string-max-length`. --- .../java_case/test_case.class | Bin 1019 -> 1011 bytes .../java_contains/test.desc | 2 +- .../string_constraint_generator_indexof.cpp | 164 +++++------------- .../string_constraint_generator_main.cpp | 1 - .../string_constraint_generator_testing.cpp | 77 ++------ ...ng_constraint_generator_transformation.cpp | 23 ++- 6 files changed, 79 insertions(+), 188 deletions(-) diff --git a/regression/strings-smoke-tests/java_case/test_case.class b/regression/strings-smoke-tests/java_case/test_case.class index 863da75113c20863de00fa0169902a184502cd74..68e4955d131a90116d90e40d96257ebf8e98c2f3 100644 GIT binary patch delta 25 hcmey({+WG)2O|&5;c18485vj(Z#%qva}48rCIE+_3PJz? delta 33 rcmV++0N(%e2m1%GNC6ZG!+^tw!-&I{0RRZYpu?xbsKd6iQ~{p?1%?l% diff --git a/regression/strings-smoke-tests/java_contains/test.desc b/regression/strings-smoke-tests/java_contains/test.desc index e0ca4731a4..b2a9cae259 100644 --- a/regression/strings-smoke-tests/java_contains/test.desc +++ b/regression/strings-smoke-tests/java_contains/test.desc @@ -1,6 +1,6 @@ CORE test_contains.class ---refine-strings +--refine-strings --string-max-length 100 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index 33e6cc960d..5990fc4c9e 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -15,7 +15,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include /// Add axioms stating that the returned value is the index within str of the -/// first occurence of c starting the search at from_index, or -1 if no such +/// first occurrence of c starting the search at from_index, or -1 if no such /// character occurs at or after position from_index. /// \param str: a string expression /// \param c: an expression representing a character @@ -69,7 +69,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of( } /// Add axioms stating that the returned value is the index within haystack of -/// the first occurence of needle starting the search at from_index, or -1 if +/// the first occurrence of needle starting the search at from_index, or -1 if /// needle does not occur at or after position from_index. /// \param haystack: a string expression /// \param needle: a string expression @@ -92,7 +92,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( // contains ==> haystack[n+offset]=needle[n] // a4 : forall n:[from_index,offset[. // contains ==> (exists m:[0,|needle|[. haystack[m+n] != needle[m]]) - // a5: forall n:[from_index,|haystack|-|needle|[. + // a5: forall n:[from_index,|haystack|-|needle|]. // !contains ==> (exists m:[0,|needle|[. haystack[m+n] != needle[m]) implies_exprt a1( @@ -116,70 +116,35 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])); axioms.push_back(a3); - if(!is_constant_string(needle)) - { - // string_not contains_constraintt are formulas of the form: - // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y] - string_not_contains_constraintt a4( - from_index, - offset, - contains, - from_integer(0, index_type), - needle.length(), - haystack, - needle); - axioms.push_back(a4); + // string_not contains_constraintt are formulas of the form: + // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y] + string_not_contains_constraintt a4( + from_index, + offset, + contains, + from_integer(0, index_type), + needle.length(), + haystack, + needle); + axioms.push_back(a4); - string_not_contains_constraintt a5( - from_index, + string_not_contains_constraintt a5( + from_index, + plus_exprt( // Add 1 for inclusive upper bound. minus_exprt(haystack.length(), needle.length()), - not_exprt(contains), - from_integer(0, index_type), - needle.length(), - haystack, - needle); - axioms.push_back(a5); - } - else - { - // Unfold the existential quantifier as a disjunction in case of a constant - // a4 && a5 <=> a6: - // forall n:[from_index,|haystack|-|needle|]. - // !contains || n < offset ==> - // haystack[n] != needle[0] || ... || - // haystack[n+|needle|-1] != needle[|needle|-1] - symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type); - mp_integer sub_length; - INVARIANT( - !to_integer(needle.length(), sub_length), - string_refinement_invariantt("a constant string must have constant " - "length")); - exprt::operandst disjuncts; - for(mp_integer offset=0; offset a6: - // forall n:[0, min(from_index, |haystack| - |needle|)]. - // !contains || (n > offset) ==> - // haystack[n] != needle[0] || ... || - // haystack[n+|needle|-1] != needle[|needle|-1] - symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type); - mp_integer sub_length; - INVARIANT( - !to_integer(needle.length(), sub_length), - string_refinement_invariantt("a constant string must have constant " - "length")); - exprt::operandst disjuncts; - for(mp_integer offset=0; offset AND_{i < |s1|} s1[i] = s0[startpos + i] - mp_integer s1_length; - INVARIANT( - !to_integer(s1.length(), s1_length), - string_refinement_invariantt("a constant string expression must have a " - "constant length")); - exprt::operandst conjuncts; - for(mp_integer i=0; i |s1| > |s0| || - // (forall qvar <= |s0| - |s1|. - // !(AND_{i < |s1|} s1[i] == s0[i + qvar]) - // - // which we implement as: - // forall qvar <= |s0| - |s1|. (!contains && |s0| >= |s1|) - // ==> !(AND_{i < |s1|} (s1[i] == s0[qvar+i])) - symbol_exprt qvar=fresh_univ_index("QA_contains_constant", index_type); - exprt::operandst conjuncts1; - for(mp_integer i=0; i= |s1|) + // ==> exists witness < |s1|. s1[witness] != s0[startpos+witness] + string_not_contains_constraintt a5( + from_integer(0, index_type), + plus_exprt(from_integer(1, index_type), length_diff), + and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)), + from_integer(0, index_type), + s1.length(), + s0, + s1); + axioms.push_back(a5); - string_constraintt a5( - qvar, - plus_exprt(from_integer(1, index_type), length_diff), - and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)), - not_exprt(conjunction(conjuncts1))); - axioms.push_back(a5); - } - else - { - symbol_exprt qvar=fresh_univ_index("QA_contains", index_type); - exprt qvar_shifted=plus_exprt(qvar, startpos); - string_constraintt a4( - qvar, s1.length(), contains, equal_exprt(s1[qvar], s0[qvar_shifted])); - axioms.push_back(a4); - - // We rewrite axiom a4 as: - // forall startpos <= |s0|-|s1|. (!contains && |s0| >= |s1|) - // ==> exists witness < |s1|. s1[witness] != s0[startpos+witness] - string_not_contains_constraintt a5( - from_integer(0, index_type), - plus_exprt(from_integer(1, index_type), length_diff), - and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)), - from_integer(0, index_type), s1.length(), s0, s1); - axioms.push_back(a5); - } return typecast_exprt(contains, f.type()); } diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index 1e2f8d0f53..49680c8b9c 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -287,7 +287,6 @@ string_exprt string_constraint_generatort::add_axioms_for_to_upper_case( exprt char_a=constant_char('a', char_type); exprt char_A=constant_char('A', char_type); exprt char_z=constant_char('z', char_type); - exprt char_Z=constant_char('Z', char_type); // TODO: add support for locales using case mapping information // from the UnicodeData file. @@ -296,21 +295,29 @@ string_exprt string_constraint_generatort::add_axioms_for_to_upper_case( // a1 : |res| = |str| // a2 : forall idx res[idx]=str[idx]+'A'-'a' // a3 : forall idx res[idx]=str[idx] + // Note that index expressions are only allowed in the body of universal + // axioms, so we use a trivial premise and push our premise into the body. exprt a1=res.axiom_for_has_same_length_as(str); axioms.push_back(a1); - symbol_exprt idx=fresh_univ_index("QA_upper_case", index_type); + symbol_exprt idx1=fresh_univ_index("QA_upper_case1", index_type); exprt is_lower_case=and_exprt( - binary_relation_exprt(char_a, ID_le, str[idx]), - binary_relation_exprt(str[idx], ID_le, char_z)); + binary_relation_exprt(char_a, ID_le, str[idx1]), + binary_relation_exprt(str[idx1], ID_le, char_z)); minus_exprt diff(char_A, char_a); - equal_exprt convert(res[idx], plus_exprt(str[idx], diff)); - string_constraintt a2(idx, res.length(), is_lower_case, convert); + equal_exprt convert(res[idx1], plus_exprt(str[idx1], diff)); + implies_exprt body1(is_lower_case, convert); + string_constraintt a2(idx1, res.length(), body1); axioms.push_back(a2); - equal_exprt eq(res[idx], str[idx]); - string_constraintt a3(idx, res.length(), not_exprt(is_lower_case), eq); + symbol_exprt idx2=fresh_univ_index("QA_upper_case2", index_type); + exprt is_not_lower_case=not_exprt(and_exprt( + binary_relation_exprt(char_a, ID_le, str[idx2]), + binary_relation_exprt(str[idx2], ID_le, char_z))); + equal_exprt eq(res[idx2], str[idx2]); + implies_exprt body2(is_not_lower_case, eq); + string_constraintt a3(idx2, res.length(), body2); axioms.push_back(a3); return res; } From 9f4179fc868462bbe6f09293a60cbba63db8c599 Mon Sep 17 00:00:00 2001 From: Jesse Sigal Date: Fri, 21 Jul 2017 14:40:07 +0100 Subject: [PATCH 2/4] Fixed checking of not contains axioms Previously, the Skolem form the not contains axioms was checked by negating it with the Skolem function for the existential still being used. This is logically incorrect and has been fixed. In the negation of the not contains axiom (whence the existential becomes a universal qunatifier), we expand the universal as a conjunction. Additionally, `string_refinement::get` did not properly get refined strings, which it does now. --- src/solvers/refinement/string_refinement.cpp | 64 ++++++++++++++------ src/solvers/refinement/string_refinement.h | 1 - 2 files changed, 44 insertions(+), 21 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 71fd4c4618..e22df07dd0 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1023,12 +1023,10 @@ void string_refinementt::substitute_array_access(exprt &expr) const /// \pre Symbols other than the universal variable should have been replaced by /// their valuation in the current model. /// \param axiom: the not_contains constraint to add the negation of -/// \param val: the existential witness for the axiom /// \param univ_var: the universal variable for the negation of the axiom /// \return: the negation of the axiom under the current evaluation exprt string_refinementt::negation_of_not_contains_constraint( const string_not_contains_constraintt &axiom, - const exprt &val, const symbol_exprt &univ_var) { exprt lbu=axiom.univ_lower_bound(); @@ -1040,7 +1038,8 @@ exprt string_refinementt::negation_of_not_contains_constraint( to_integer(to_constant_expr(ubu), ub_int); if(ub_int<=lb_int) { - debug() << "empty constraint with current model" << eom; + debug() << "(string_refinement::check_axioms) empty constraint with " + << "current model, adding false" << eom; return false_exprt(); } } @@ -1048,26 +1047,38 @@ exprt string_refinementt::negation_of_not_contains_constraint( exprt lbe=axiom.exists_lower_bound(); exprt ube=axiom.exists_upper_bound(); + INVARIANT( + lbe.id()==ID_constant && ube.id()==ID_constant, + string_refinement_invariantt("please")); + + mp_integer lbe_int, ube_int; + to_integer(to_constant_expr(lbe), lbe_int); + to_integer(to_constant_expr(ube), ube_int); + if(axiom.premise()==false_exprt()) { - debug() << "(string_refinement::check_axioms) adding false" << eom; + debug() << "(string_refinement::check_axioms) false premise, adding false" + << eom; return false_exprt(); } - // Witness is the Skolem function for the existential, which we evaluate at - // univ_var. and_exprt univ_bounds( binary_relation_exprt(lbu, ID_le, univ_var), binary_relation_exprt(ubu, ID_gt, univ_var)); - and_exprt exists_bounds( - binary_relation_exprt(lbe, ID_le, val), - binary_relation_exprt(ube, ID_gt, val)); - equal_exprt equal_chars( - axiom.s0()[plus_exprt(univ_var, val)], - axiom.s1()[val]); - and_exprt negaxiom(univ_bounds, axiom.premise(), exists_bounds, equal_chars); - debug() << "(sr::check_axioms) negated not_contains axiom: " + std::vector conjuncts; + for(mp_integer i=lbe_int; isecond); } + else if(refined_string_typet::is_refined_string_type(ecopy.type()) && + ecopy.id()==ID_struct) + { + string_exprt ecopy2=to_string_expr(ecopy); + const exprt &econtent=ecopy2.content(); + const exprt &elength=ecopy2.length(); + + exprt len=supert::get(elength); + len=simplify_expr(len, ns); + const exprt arr=get_array(econtent, len); + ecopy=string_exprt(len, arr, ecopy.type()); + } ecopy=supert::get(ecopy); @@ -1772,6 +1795,7 @@ bool string_refinementt::is_axiom_sat( } case decision_proceduret::resultt::D_UNSATISFIABLE: return false; + case decision_proceduret::resultt::D_ERROR: default: INVARIANT(false, string_refinement_invariantt("failure in checking axiom")); // To tell the compiler that the previous line bails diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 743366d628..d53f005742 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -120,7 +120,6 @@ private: void add_instantiations(); exprt negation_of_not_contains_constraint( const string_not_contains_constraintt &axiom, - const exprt &val, const symbol_exprt &univ_var); exprt negation_of_constraint(const string_constraintt &axiom); void debug_model(); From d43f9b50c11d7e6ef930a18238301a0d47b6cbeb Mon Sep 17 00:00:00 2001 From: Jesse Sigal Date: Wed, 19 Jul 2017 11:58:18 +0100 Subject: [PATCH 3/4] Added `string_constraintt` invariant checking Updated the documentation to explicitly state the invariants (and turned on MathJax in Doxygen). Created a function to check the invariant and added a check in `string_refinementt::dec_solve`. --- src/doxyfile | 2 +- src/solvers/refinement/string_constraint.h | 33 +++ ...ng_constraint_generator_transformation.cpp | 5 +- src/solvers/refinement/string_refinement.cpp | 230 +++++++++++++++--- src/solvers/refinement/string_refinement.h | 6 +- 5 files changed, 230 insertions(+), 46 deletions(-) diff --git a/src/doxyfile b/src/doxyfile index 7d894c4e70..4bccf022c9 100644 --- a/src/doxyfile +++ b/src/doxyfile @@ -1473,7 +1473,7 @@ FORMULA_TRANSPARENT = YES # The default value is: NO. # This tag requires that the tag GENERATE_HTML is set to YES. -USE_MATHJAX = NO +USE_MATHJAX = YES # When MathJax is enabled you can set the default output format to be used for # the MathJax output. See the MathJax site (see: diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index 03233ab083..6edb848b55 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -24,6 +24,30 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include #include +#include + +/*! \brief Universally quantified string constraint + + This represents a universally quantified string constraint as laid out in + DOI: 10.1007/978-3-319-03077-7. The paper seems to specify a universal + constraint as follows. + + A universal constraint is of the form \f$\forall n. L(n) \rightarrow + P(n, s_0,\ldots, s_k)\f$ where + + 1. \f$L(n)\f$ does not contain string indices [possibly not required, but + implied by examples] + 2. \f$\forall n. L(n) \rightarrow P'\left(s_0[f_0(n)],\ldots, s_k[f_k(n)] + \right)\f$, i.e. when focusing on one specific string, all indices are + the same [stated in a roundabout manner] + 3. Each \f$f\f$ is linear and therefore has an inverse [explicitly stated] + 4. \f$L(n)\f$ and \f$P(n, s_0,\ldots, s_k)\f$ may contain other (free) + variables, but in \f$P\f$, \f$n\f$ can only occur as an argument to an + \f$f\f$ [explicitly stated, implied] + + We extend this slightly by restricting n to be in a specific range, but this + is another implication which can be pushed in to \f$L(n)\f$. +*/ class string_constraintt: public exprt { @@ -114,6 +138,15 @@ extern inline string_constraintt &to_string_constraint(exprt &expr) return static_cast(expr); } +inline static std::string from_expr( + const namespacet &ns, + const irep_idt &identifier, + const string_constraintt &expr) +{ + return from_expr(ns, identifier, expr.premise())+" => "+ + from_expr(ns, identifier, expr.body()); +} + class string_not_contains_constraintt: public exprt { public: diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index 49680c8b9c..abbd6d3479 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -293,8 +293,9 @@ string_exprt string_constraint_generatort::add_axioms_for_to_upper_case( // We add axioms: // a1 : |res| = |str| - // a2 : forall idx res[idx]=str[idx]+'A'-'a' - // a3 : forall idx res[idx]=str[idx] + // a2 : forall idx1 + // res[idx1]=str[idx1]+'A'-'a' + // a3 : forall idx2 res[idx2]=str[idx2] // Note that index expressions are only allowed in the body of universal // axioms, so we use a trivial premise and push our premise into the body. diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index e22df07dd0..1ea01ef2c7 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -19,6 +19,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #include +#include #include #include #include @@ -517,6 +518,10 @@ decision_proceduret::resultt string_refinementt::dec_solve() if(axiom.id()==ID_string_constraint) { string_constraintt c=to_string_constraint(axiom); + DATA_INVARIANT( + is_valid_string_constraint(c), + string_refinement_invariantt( + "string constraints satisfy their invariant")); universal_axioms.push_back(c); } else if(axiom.id()==ID_string_not_contains_constraint) @@ -1025,10 +1030,11 @@ void string_refinementt::substitute_array_access(exprt &expr) const /// \param axiom: the not_contains constraint to add the negation of /// \param univ_var: the universal variable for the negation of the axiom /// \return: the negation of the axiom under the current evaluation -exprt string_refinementt::negation_of_not_contains_constraint( +static exprt negation_of_not_contains_constraint( const string_not_contains_constraintt &axiom, const symbol_exprt &univ_var) { + // If the for all is vacuously true, the negation is false. exprt lbu=axiom.univ_lower_bound(); exprt ubu=axiom.univ_upper_bound(); if(lbu.id()==ID_constant && ubu.id()==ID_constant) @@ -1037,37 +1043,29 @@ exprt string_refinementt::negation_of_not_contains_constraint( to_integer(to_constant_expr(lbu), lb_int); to_integer(to_constant_expr(ubu), ub_int); if(ub_int<=lb_int) - { - debug() << "(string_refinement::check_axioms) empty constraint with " - << "current model, adding false" << eom; return false_exprt(); - } } exprt lbe=axiom.exists_lower_bound(); exprt ube=axiom.exists_upper_bound(); - INVARIANT( - lbe.id()==ID_constant && ube.id()==ID_constant, - string_refinement_invariantt("please")); - mp_integer lbe_int, ube_int; to_integer(to_constant_expr(lbe), lbe_int); to_integer(to_constant_expr(ube), ube_int); + // If the premise is false, the implication is trivially true, so the + // negation is false. if(axiom.premise()==false_exprt()) - { - debug() << "(string_refinement::check_axioms) false premise, adding false" - << eom; return false_exprt(); - } and_exprt univ_bounds( binary_relation_exprt(lbu, ID_le, univ_var), binary_relation_exprt(ubu, ID_gt, univ_var)); + // The negated existential becomes an universal, and this is the unrolling of + // that universal quantifier. std::vector conjuncts; - for(mp_integer i=lbe_int; i> array_index_mapt; + +/// \related string_constraintt +class gather_indices_visitort: public const_expr_visitort +{ +public: + array_index_mapt indices; + + gather_indices_visitort(): indices() {} + + void operator()(const exprt &expr) override + { + if(expr.id()==ID_index) + { + const index_exprt index=to_index_expr(expr); + const exprt s(index.array()); + const exprt i(index.index()); + indices[s].push_back(i); + } + } +}; + +/// \related string_constraintt +static array_index_mapt gather_indices(const exprt &expr) +{ + gather_indices_visitort v; + expr.visit(v); + return v.indices; +} + +/// \related string_constraintt +class is_linear_arithmetic_expr_visitort: public const_expr_visitort +{ +public: + bool correct; + + is_linear_arithmetic_expr_visitort(): correct(true) {} + + void operator()(const exprt &expr) override + { + if(expr.id()!=ID_plus && expr.id()!=ID_minus && expr.id()!=ID_unary_minus) + { + // This represents that the expr is a valid leaf, may not be future proof + // or 100% enforced, but is correct prescriptively. All non-sum exprs must + // be leaves. + correct&=expr.operands().empty(); + } + } +}; + +/// \related string_constraintt +static bool is_linear_arithmetic_expr(const exprt &expr) +{ + is_linear_arithmetic_expr_visitort v; + expr.visit(v); + return v.correct; +} + +/// The universally quantified variable is only allowed to occur in index +/// expressions in the body of a string constraint. This function returns true +/// if this is the case and false otherwise. +/// \related string_constraintt +/// \param [in] expr: The string constraint to check +/// \return true if the universal variable only occurs in index expressions, +/// false otherwise. +static bool universal_only_in_index(const string_constraintt &expr) +{ + // For efficiency, we do a depth-first search of the + // body. The exprt visitors do a BFS and hide the stack/queue, so we would + // need to store a map from child to parent. + + // The unsigned int represents index depth we are. For example, if we are + // considering the fragment `a[b[x]]` (not inside an index expression), then + // the stack would look something like `[..., (a, 0), (b, 1), (x, 2)]`. + typedef std::pair valuet; + std::stack stack; + // We start at 0 since expr is not an index expression, so expr.body() is not + // in an index expression. + stack.push(valuet(expr.body(), 0)); + while(!stack.empty()) + { + // Inspect current value + const valuet cur=stack.top(); + stack.pop(); + const exprt e=cur.first; + const unsigned index_depth=cur.second; + const unsigned child_index_depth=index_depth+(e.id()==ID_index?0:1); + + // If we found the universal variable not in an index_exprt, fail + if(e==expr.univ_var() && index_depth==0) + return false; + else + forall_operands(it, e) + stack.push(valuet(*it, child_index_depth)); + } + return true; +} + +/// Checks the data invariant for \link string_constraintt +/// \related string_constraintt +/// \param [in] expr: the string constraint to check +/// \return whether the constraint satisfies the invariant +bool string_refinementt::is_valid_string_constraint( + const string_constraintt &expr) +{ + // Condition 1: The premise cannot contain any string indices + const array_index_mapt premise_indices=gather_indices(expr.premise()); + if(!premise_indices.empty()) + { + error() << "Premise has indices: " << from_expr(ns, "", expr) << ", map: {"; + for(const auto &pair : premise_indices) + { + error() << from_expr(ns, "", pair.first) << ": {"; + for(const auto &i : pair.second) + error() << from_expr(ns, "", i) << ", "; + } + error() << "}}" << eom; + return false; + } + + const array_index_mapt body_indices=gather_indices(expr.body()); + // Must validate for each string. Note that we have an invariant that the + // second value in the pair is non-empty. + for(const auto &pair : body_indices) + { + // Condition 2: All indices of the same string must be the of the same form + const exprt rep=pair.second.back(); + for(size_t j=0; j &m, const typet &type, bool negated=false) const; + bool is_valid_string_constraint(const string_constraintt &expr); + exprt simplify_sum(const exprt &f) const; template void pad_vector( From c306d56e72a9a7898b24030294865fd52c234cbd Mon Sep 17 00:00:00 2001 From: Jesse Sigal Date: Fri, 21 Jul 2017 14:49:53 +0100 Subject: [PATCH 4/4] Fixed some spelling errors --- src/solvers/refinement/string_refinement.cpp | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 1ea01ef2c7..a8c66d6340 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -211,7 +211,7 @@ void string_refinementt::set_char_array_equality( /// remove functions applications and create the necessary axioms /// \par parameters: an expression containing function applications -/// \return an epression containing no function application +/// \return an expression containing no function application exprt string_refinementt::substitute_function_applications(exprt expr) { for(size_t i=0; i /// 2, y -> -1. @@ -1355,7 +1355,7 @@ exprt string_refinementt::sum_over_map( } /// \par parameters: an expression with only plus and minus expr -/// \return an equivalent expression in a cannonical form +/// \return an equivalent expression in a canonical form exprt string_refinementt::simplify_sum(const exprt &f) const { std::map map=map_representation_of_sum(f); @@ -1375,7 +1375,7 @@ exprt string_refinementt::compute_inverse_function( exprt positive, negative; // number of time the element should be added (can be negative) // qvar has to be equal to val - f(0) if it appears positively in f - // (ie if f(qvar)=f(0) + qvar) and f(0) - val if it appears negatively + // (i.e. if f(qvar)=f(0) + qvar) and f(0) - val if it appears negatively // in f. So we start by computing val - f(0). std::map elems=map_representation_of_sum(minus_exprt(val, f)); @@ -1611,7 +1611,7 @@ exprt find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar) /// \return substitute `qvar` the universally quantified variable of `axiom`, by /// an index `val`, in `axiom`, so that the index used for `str` equals `val`. /// For instance, if `axiom` corresponds to $\forall q. s[q+x]='a' && -/// t[q]='b'$, `instantiate(axom,s,v)` would return an expression for +/// t[q]='b'$, `instantiate(axiom,s,v)` would return an expression for /// $s[v]='a' && t[v-x]='b'$. exprt string_refinementt::instantiate( const string_constraintt &axiom, const exprt &str, const exprt &val) @@ -1690,7 +1690,7 @@ void string_refinementt::instantiate_not_contains( /// replace array-lists by 'with' expressions /// \par parameters: an expression containing array-list expressions -/// \return an epression containing no array-list +/// \return an expression containing no array-list exprt string_refinementt::substitute_array_lists(exprt expr) const { for(size_t i=0; i