From e4e667120449d3041c33b4301710b574ea7d7ee2 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Wed, 27 Sep 2017 11:06:19 +0100 Subject: [PATCH 1/7] Move expr_cast into a separate file --- src/solvers/refinement/expr_cast.h | 58 ++++++++++++++++++++ src/solvers/refinement/string_refinement.cpp | 58 +------------------- 2 files changed, 59 insertions(+), 57 deletions(-) create mode 100644 src/solvers/refinement/expr_cast.h diff --git a/src/solvers/refinement/expr_cast.h b/src/solvers/refinement/expr_cast.h new file mode 100644 index 00000000000..77d2f5ae3a1 --- /dev/null +++ b/src/solvers/refinement/expr_cast.h @@ -0,0 +1,58 @@ +#include + +/// Convert exprt to a specific type. Throw bad_cast if conversion +/// cannot be performed +/// Generic case doesn't exist, specialize for different types accordingly +/// TODO: this should go to util + +// Tag dispatching struct + +template +struct expr_cast_implt final { }; + +template<> +struct expr_cast_implt final +{ + optionalt operator()(const exprt &expr) const + { + mp_integer out; + if(to_integer(expr, out)) + return {}; + return out; + } +}; + +template<> +struct expr_cast_implt final +{ + optionalt operator()(const exprt &expr) const + { + if(const auto tmp=expr_cast_implt()(expr)) + if(tmp->is_long() && *tmp>=0) + return tmp->to_long(); + return {}; + } +}; + +template<> +struct expr_cast_implt final +{ + optionalt operator()(const exprt &expr) const + { + if(is_refined_string_type(expr.type())) + return to_string_expr(expr); + return {}; + } +}; + +template +optionalt expr_cast(const exprt& expr) +{ return expr_cast_implt()(expr); } + +template +T expr_cast_v(const exprt &expr) +{ + const auto maybe=expr_cast(expr); + INVARIANT(maybe, "Bad conversion"); + return *maybe; +} diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 8cd4924ffec..6fdab35a97a 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -26,6 +26,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #include #include +#include "expr_cast.h" static exprt substitute_array_with_expr(const exprt &expr, const exprt &index); @@ -95,63 +96,6 @@ static exprt get_array( const std::function &super_get, const exprt &arr); -/// Convert exprt to a specific type. Throw bad_cast if conversion -/// cannot be performed -/// Generic case doesn't exist, specialize for different types accordingly -/// TODO: this should go to util - -// Tag dispatching struct - -template -struct expr_cast_implt final { }; - -template<> -struct expr_cast_implt final -{ - optionalt operator()(const exprt &expr) const - { - mp_integer out; - if(to_integer(expr, out)) - return {}; - return out; - } -}; - -template<> -struct expr_cast_implt final -{ - optionalt operator()(const exprt &expr) const - { - if(const auto tmp=expr_cast_implt()(expr)) - if(tmp->is_long() && *tmp>=0) - return tmp->to_long(); - return {}; - } -}; - -template<> -struct expr_cast_implt final -{ - optionalt operator()(const exprt &expr) const - { - if(is_refined_string_type(expr.type())) - return to_string_expr(expr); - return {}; - } -}; - -template -optionalt expr_cast(const exprt& expr) -{ return expr_cast_implt()(expr); } - -template -T expr_cast_v(const exprt &expr) -{ - const auto maybe=expr_cast(expr); - INVARIANT(maybe, "Bad conversion"); - return *maybe; -} - /// Convert index-value map to a vector of values. If a value for an /// index is not defined, set it to the value referenced by the next higher /// index. The length of the resulting vector is the key of the map's From fedba190ed005671dff24582be5703fed50da834 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Fri, 15 Sep 2017 11:31:15 +0100 Subject: [PATCH 2/7] Split string generator axioms into separate vectors --- src/solvers/refinement/string_constraint.h | 8 +-- .../refinement/string_constraint_generator.h | 9 +++- ...tring_constraint_generator_code_points.cpp | 26 +++++----- ...string_constraint_generator_comparison.cpp | 26 +++++----- .../string_constraint_generator_concat.cpp | 8 +-- .../string_constraint_generator_constants.cpp | 4 +- .../string_constraint_generator_float.cpp | 6 +-- .../string_constraint_generator_indexof.cpp | 40 +++++++-------- .../string_constraint_generator_main.cpp | 44 ++++++++-------- .../string_constraint_generator_testing.cpp | 26 +++++----- ...ng_constraint_generator_transformation.cpp | 48 ++++++++--------- .../string_constraint_generator_valueof.cpp | 40 +++++++-------- src/solvers/refinement/string_refinement.cpp | 51 +++++++++---------- 13 files changed, 168 insertions(+), 168 deletions(-) diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index f2a19153fe6..a7a7ccb5ca6 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -49,7 +49,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com is another implication which can be pushed in to \f$L(n)\f$. */ -class string_constraintt: public exprt +class string_constraintt final: public exprt { public: // String constraints are of the form @@ -88,8 +88,8 @@ class string_constraintt: public exprt const symbol_exprt &_univ_var, const exprt &bound_inf, const exprt &bound_sup, - const exprt &prem, - const exprt &body): + const exprt &prem, // Index guard + const exprt &body): // value constraint exprt(ID_string_constraint) { copy_to_operands(prem, body); @@ -155,7 +155,7 @@ inline std::string from_expr( from_expr(ns, identifier, expr.body()); } -class string_not_contains_constraintt: public exprt +class string_not_contains_constraintt final: public exprt { public: // string_not contains_constraintt are formula of the form: diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index ff5b4040005..f59dfdff5cc 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -50,7 +50,10 @@ class string_constraint_generatort final /// Axioms are of three kinds: universally quantified string constraint, /// not contains string constraints and simple formulas. - const std::vector &get_axioms() const; + const std::vector &lemmas() const; + const std::vector &constraints() const; + const std::vector + ¬_contains_constraints() const; /// Boolean symbols for the results of some string functions const std::vector &get_boolean_symbols() const; @@ -353,7 +356,9 @@ class string_constraint_generatort final const messaget m_message; const bool m_force_printable_characters; - std::vector m_axioms; + std::vector lemmas_; + std::vector constraints_; + std::vector not_contains_constraints_; std::map m_unresolved_symbols; std::vector m_boolean_symbols; std::vector m_index_symbols; diff --git a/src/solvers/refinement/string_constraint_generator_code_points.cpp b/src/solvers/refinement/string_constraint_generator_code_points.cpp index 55b914d1aa7..fb6b9fd278b 100644 --- a/src/solvers/refinement/string_constraint_generator_code_points.cpp +++ b/src/solvers/refinement/string_constraint_generator_code_points.cpp @@ -48,27 +48,27 @@ string_exprt string_constraint_generatort::add_axioms_for_code_point( binary_relation_exprt small(code_point, ID_lt, hex010000); implies_exprt a1(small, res.axiom_for_has_length(1)); - m_axioms.push_back(a1); + lemmas_.push_back(a1); implies_exprt a2(not_exprt(small), res.axiom_for_has_length(2)); - m_axioms.push_back(a2); + lemmas_.push_back(a2); typecast_exprt code_point_as_char(code_point, ref_type.get_char_type()); implies_exprt a3(small, equal_exprt(res[0], code_point_as_char)); - m_axioms.push_back(a3); + lemmas_.push_back(a3); plus_exprt first_char( hexD800, div_exprt(minus_exprt(code_point, hex010000), hex0400)); implies_exprt a4( not_exprt(small), equal_exprt(res[0], typecast_exprt(first_char, ref_type.get_char_type()))); - m_axioms.push_back(a4); + lemmas_.push_back(a4); plus_exprt second_char(hexDC00, mod_exprt(code_point, hex0400)); implies_exprt a5( not_exprt(small), equal_exprt(res[1], typecast_exprt(second_char, ref_type.get_char_type()))); - m_axioms.push_back(a5); + lemmas_.push_back(a5); return res; } @@ -141,8 +141,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_at( str[plus_exprt_with_overflow_check(pos, index1)]); exprt return_pair=and_exprt(is_high_surrogate(str[pos]), is_low); - m_axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair))); - m_axioms.push_back( + lemmas_.push_back(implies_exprt(return_pair, equal_exprt(result, pair))); + lemmas_.push_back( implies_exprt(not_exprt(return_pair), equal_exprt(result, char1_as_int))); return result; } @@ -172,8 +172,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_before( exprt return_pair=and_exprt( is_high_surrogate(char1), is_low_surrogate(char2)); - m_axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair))); - m_axioms.push_back( + lemmas_.push_back(implies_exprt(return_pair, equal_exprt(result, pair))); + lemmas_.push_back( implies_exprt(not_exprt(return_pair), equal_exprt(result, char2_as_int))); return result; } @@ -193,8 +193,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_count( symbol_exprt result=fresh_symbol("code_point_count", return_type); minus_exprt length(end, begin); div_exprt minimum(length, from_integer(2, length.type())); - m_axioms.push_back(binary_relation_exprt(result, ID_le, length)); - m_axioms.push_back(binary_relation_exprt(result, ID_ge, minimum)); + lemmas_.push_back(binary_relation_exprt(result, ID_le, length)); + lemmas_.push_back(binary_relation_exprt(result, ID_ge, minimum)); return result; } @@ -217,8 +217,8 @@ exprt string_constraint_generatort::add_axioms_for_offset_by_code_point( exprt minimum=plus_exprt_with_overflow_check(index, offset); exprt maximum=plus_exprt_with_overflow_check( index, plus_exprt_with_overflow_check(offset, offset)); - m_axioms.push_back(binary_relation_exprt(result, ID_le, maximum)); - m_axioms.push_back(binary_relation_exprt(result, ID_ge, minimum)); + lemmas_.push_back(binary_relation_exprt(result, ID_le, maximum)); + lemmas_.push_back(binary_relation_exprt(result, ID_ge, minimum)); return result; } diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp index 7bc276cd24a..511ecfdff48 100644 --- a/src/solvers/refinement/string_constraint_generator_comparison.cpp +++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp @@ -39,11 +39,11 @@ exprt string_constraint_generatort::add_axioms_for_equals( // || (witness |s1|!=s2 || (0 <=witness<|s1| &&!char_equal_ignore_case) implies_exprt a1(eq, s1.axiom_for_has_same_length_as(s2)); - m_axioms.push_back(a1); + lemmas_.push_back(a1); symbol_exprt qvar=fresh_univ_index("QA_equal_ignore_case", index_type); exprt constr2=character_equals_ignore_case( s1[qvar], s2[qvar], char_a, char_A, char_Z); string_constraintt a2(qvar, s1.length(), eq, constr2); - m_axioms.push_back(a2); + constraints_.push_back(a2); symbol_exprt witness=fresh_exist_index( "witness_unequal_ignore_case", index_type); @@ -139,7 +139,7 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case( or_exprt( notequal_exprt(s1.length(), s2.length()), and_exprt(bound_witness, witness_diff))); - m_axioms.push_back(a3); + lemmas_.push_back(a3); return tc_eq; } @@ -177,7 +177,7 @@ exprt string_constraint_generatort::add_axioms_for_hash_code( and_exprt( str.axiom_for_length_gt(i), axiom_for_is_positive_index(i)))); - m_axioms.push_back(or_exprt(c1, or_exprt(c2, c3))); + lemmas_.push_back(or_exprt(c1, or_exprt(c2, c3))); } return hash; } @@ -211,11 +211,11 @@ exprt string_constraint_generatort::add_axioms_for_compare_to( equal_exprt res_null=equal_exprt(res, from_integer(0, return_type)); implies_exprt a1(res_null, s1.axiom_for_has_same_length_as(s2)); - m_axioms.push_back(a1); + lemmas_.push_back(a1); symbol_exprt i=fresh_univ_index("QA_compare_to", index_type); string_constraintt a2(i, s1.length(), res_null, equal_exprt(s1[i], s2[i])); - m_axioms.push_back(a2); + constraints_.push_back(a2); symbol_exprt x=fresh_exist_index("index_compare_to", index_type); equal_exprt ret_char_diff( @@ -242,12 +242,12 @@ exprt string_constraint_generatort::add_axioms_for_compare_to( and_exprt( binary_relation_exprt(x, ID_ge, from_integer(0, return_type)), or_exprt(cond1, cond2))); - m_axioms.push_back(a3); + lemmas_.push_back(a3); symbol_exprt i2=fresh_univ_index("QA_compare_to", index_type); string_constraintt a4( i2, x, not_exprt(res_null), equal_exprt(s1[i2], s2[i2])); - m_axioms.push_back(a4); + constraints_.push_back(a4); return res; } @@ -279,7 +279,7 @@ symbol_exprt string_constraint_generatort::add_axioms_for_intern( disj=or_exprt( disj, equal_exprt(intern, it.second)); - m_axioms.push_back(disj); + lemmas_.push_back(disj); // WARNING: the specification may be incomplete or incorrect @@ -287,7 +287,7 @@ symbol_exprt string_constraint_generatort::add_axioms_for_intern( if(it.second!=str) { symbol_exprt i=fresh_exist_index("index_intern", index_type); - m_axioms.push_back( + lemmas_.push_back( or_exprt( equal_exprt(it.second, intern), or_exprt( diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index 3f4f607addd..3d8a7a0367f 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -46,20 +46,20 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_substr( exprt res_length=plus_exprt_with_overflow_check( s1.length(), minus_exprt(end_index, start_index)); implies_exprt a1(prem, equal_exprt(res.length(), res_length)); - m_axioms.push_back(a1); + lemmas_.push_back(a1); implies_exprt a2(not_exprt(prem), equal_exprt(res.length(), s1.length())); - m_axioms.push_back(a2); + lemmas_.push_back(a2); symbol_exprt idx=fresh_univ_index("QA_index_concat", res.length().type()); string_constraintt a3(idx, s1.length(), equal_exprt(s1[idx], res[idx])); - m_axioms.push_back(a3); + constraints_.push_back(a3); symbol_exprt idx2=fresh_univ_index("QA_index_concat2", res.length().type()); equal_exprt res_eq( res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start_index, idx2)]); string_constraintt a4(idx2, minus_exprt(end_index, start_index), res_eq); - m_axioms.push_back(a4); + constraints_.push_back(a4); return res; } diff --git a/src/solvers/refinement/string_constraint_generator_constants.cpp b/src/solvers/refinement/string_constraint_generator_constants.cpp index d701d27a583..2011c7619ae 100644 --- a/src/solvers/refinement/string_constraint_generator_constants.cpp +++ b/src/solvers/refinement/string_constraint_generator_constants.cpp @@ -40,12 +40,12 @@ string_exprt string_constraint_generatort::add_axioms_for_constant( exprt idx=from_integer(i, ref_type.get_index_type()); exprt c=from_integer(str[i], ref_type.get_char_type()); equal_exprt lemma(res[idx], c); - m_axioms.push_back(lemma); + lemmas_.push_back(lemma); } exprt s_length=from_integer(str.size(), ref_type.get_index_type()); - m_axioms.push_back(res.axiom_for_has_length(s_length)); + lemmas_.push_back(res.axiom_for_has_length(s_length)); return res; } diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index da085756115..1200a5ec395 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -237,7 +237,7 @@ string_exprt string_constraint_generatort::add_axioms_for_fractional_part( and_exprt a1(res.axiom_for_length_gt(1), res.axiom_for_length_le(max)); - m_axioms.push_back(a1); + lemmas_.push_back(a1); equal_exprt starts_with_dot(res[0], from_integer('.', char_type)); @@ -275,10 +275,10 @@ string_exprt string_constraint_generatort::add_axioms_for_fractional_part( } exprt a2=conjunction(digit_constraints); - m_axioms.push_back(a2); + lemmas_.push_back(a2); equal_exprt a3(int_expr, sum); - m_axioms.push_back(a3); + lemmas_.push_back(a3); return res; } diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index 977b9832dbf..77056399237 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -39,22 +39,22 @@ exprt string_constraint_generatort::add_axioms_for_index_of( and_exprt a1( binary_relation_exprt(index, ID_ge, minus1), binary_relation_exprt(index, ID_lt, str.length())); - m_axioms.push_back(a1); + lemmas_.push_back(a1); equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1)); - m_axioms.push_back(a2); + lemmas_.push_back(a2); implies_exprt a3( contains, and_exprt( binary_relation_exprt(from_index, ID_le, index), equal_exprt(str[index], c))); - m_axioms.push_back(a3); + lemmas_.push_back(a3); symbol_exprt n=fresh_univ_index("QA_index_of", index_type); string_constraintt a4( n, from_index, index, contains, not_exprt(equal_exprt(str[n], c))); - m_axioms.push_back(a4); + constraints_.push_back(a4); symbol_exprt m=fresh_univ_index("QA_index_of", index_type); string_constraintt a5( @@ -63,7 +63,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of( str.length(), not_exprt(contains), not_exprt(equal_exprt(str[m], c))); - m_axioms.push_back(a5); + constraints_.push_back(a5); return index; } @@ -101,12 +101,12 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( binary_relation_exprt(from_index, ID_le, offset), binary_relation_exprt( offset, ID_le, minus_exprt(haystack.length(), needle.length())))); - m_axioms.push_back(a1); + lemmas_.push_back(a1); equal_exprt a2( not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type))); - m_axioms.push_back(a2); + lemmas_.push_back(a2); symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type); string_constraintt a3( @@ -114,7 +114,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( needle.length(), contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])); - m_axioms.push_back(a3); + constraints_.push_back(a3); // 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] @@ -126,7 +126,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( needle.length(), haystack, needle); - m_axioms.push_back(a4); + not_contains_constraints_.push_back(a4); string_not_contains_constraintt a5( from_index, @@ -138,7 +138,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( needle.length(), haystack, needle); - m_axioms.push_back(a5); + not_contains_constraints_.push_back(a5); return offset; } @@ -181,17 +181,17 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string( binary_relation_exprt( offset, ID_le, minus_exprt(haystack.length(), needle.length())), binary_relation_exprt(offset, ID_le, from_index))); - m_axioms.push_back(a1); + lemmas_.push_back(a1); equal_exprt a2( not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type))); - m_axioms.push_back(a2); + lemmas_.push_back(a2); symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type); equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]); string_constraintt a3(qvar, needle.length(), contains, constr3); - m_axioms.push_back(a3); + constraints_.push_back(a3); // end_index is min(from_index, |str| - |substring|) minus_exprt length_diff(haystack.length(), needle.length()); @@ -208,7 +208,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string( needle.length(), haystack, needle); - m_axioms.push_back(a4); + not_contains_constraints_.push_back(a4); string_not_contains_constraintt a5( from_integer(0, index_type), @@ -218,7 +218,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string( needle.length(), haystack, needle); - m_axioms.push_back(a5); + not_contains_constraints_.push_back(a5); return offset; } @@ -289,17 +289,17 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of( and_exprt a1( binary_relation_exprt(index, ID_ge, minus1), binary_relation_exprt(index, ID_lt, from_index_plus_one)); - m_axioms.push_back(a1); + lemmas_.push_back(a1); equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1)); - m_axioms.push_back(a2); + lemmas_.push_back(a2); implies_exprt a3( contains, and_exprt( binary_relation_exprt(from_index, ID_ge, index), equal_exprt(str[index], c))); - m_axioms.push_back(a3); + lemmas_.push_back(a3); symbol_exprt n=fresh_univ_index("QA_last_index_of1", index_type); string_constraintt a4( @@ -308,7 +308,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of( from_index_plus_one, contains, not_exprt(equal_exprt(str[n], c))); - m_axioms.push_back(a4); + constraints_.push_back(a4); symbol_exprt m=fresh_univ_index("QA_last_index_of2", index_type); string_constraintt a5( @@ -316,7 +316,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of( from_index_plus_one, not_exprt(contains), not_exprt(equal_exprt(str[m], c))); - m_axioms.push_back(a5); + constraints_.push_back(a5); return index; } diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 2eca6940c7b..02748d487a7 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -33,28 +33,28 @@ string_constraint_generatort::string_constraint_generatort( m_force_printable_characters(info.string_printable), m_ns(ns) { } -const std::vector &string_constraint_generatort::get_axioms() const -{ - return m_axioms; -} +const std::vector &string_constraint_generatort::lemmas() const +{ return lemmas_; } + +const std::vector +&string_constraint_generatort::constraints() const +{ return constraints_; } + +const std::vector +&string_constraint_generatort::not_contains_constraints() const +{ return not_contains_constraints_; } const std::vector & string_constraint_generatort::get_index_symbols() const -{ - return m_index_symbols; -} +{ return m_index_symbols; } const std::vector & string_constraint_generatort::get_boolean_symbols() const -{ - return m_boolean_symbols; -} +{ return m_boolean_symbols; } const std::set & string_constraint_generatort::get_created_strings() const -{ - return m_created_strings; -} +{ return m_created_strings; } /// generate constant character expression with character type. /// \par parameters: integer representing a character, and a type for @@ -134,7 +134,7 @@ plus_exprt string_constraint_generatort::plus_exprt_with_overflow_check( implies_exprt no_overflow(equal_exprt(neg1, neg2), equal_exprt(neg1, neg_sum)); - m_axioms.push_back(no_overflow); + lemmas_.push_back(no_overflow); return sum; } @@ -183,10 +183,10 @@ string_exprt string_constraint_generatort::get_string_expr(const exprt &expr) void string_constraint_generatort::add_default_axioms( const string_exprt &s) { - m_axioms.push_back( + lemmas_.push_back( s.axiom_for_length_ge(from_integer(0, s.length().type()))); if(max_string_length!=std::numeric_limits::max()) - m_axioms.push_back(s.axiom_for_length_le(max_string_length)); + lemmas_.push_back(s.axiom_for_length_le(max_string_length)); if(m_force_printable_characters) { @@ -196,7 +196,7 @@ void string_constraint_generatort::add_default_axioms( binary_relation_exprt(chr, ID_ge, from_integer(' ', chr.type())), binary_relation_exprt(chr, ID_le, from_integer('~', chr.type()))); string_constraintt sc(qvar, s.length(), printable); - m_axioms.push_back(sc); + constraints_.push_back(sc); } } @@ -282,18 +282,18 @@ string_exprt string_constraint_generatort::add_axioms_for_if( const typet &index_type=ref_type.get_index_type(); string_exprt res=fresh_string(ref_type); - m_axioms.push_back( + lemmas_.push_back( implies_exprt(expr.cond(), res.axiom_for_has_same_length_as(t))); symbol_exprt qvar=fresh_univ_index("QA_string_if_true", index_type); equal_exprt qequal(res[qvar], t[qvar]); string_constraintt sc1(qvar, t.length(), implies_exprt(expr.cond(), qequal)); - m_axioms.push_back(sc1); - m_axioms.push_back( + constraints_.push_back(sc1); + lemmas_.push_back( implies_exprt(not_exprt(expr.cond()), res.axiom_for_has_same_length_as(f))); symbol_exprt qvar2=fresh_univ_index("QA_string_if_false", index_type); equal_exprt qequal2(res[qvar2], f[qvar2]); string_constraintt sc2(qvar2, f.length(), or_exprt(expr.cond(), qequal2)); - m_axioms.push_back(sc2); + constraints_.push_back(sc2); return res; } @@ -615,7 +615,7 @@ exprt string_constraint_generatort::add_axioms_for_char_at( string_exprt str=get_string_expr(args(f, 2)[0]); const refined_string_typet &ref_type=to_refined_string_type(str.type()); symbol_exprt char_sym=fresh_symbol("char", ref_type.get_char_type()); - m_axioms.push_back(equal_exprt(char_sym, str[args(f, 2)[1]])); + lemmas_.push_back(equal_exprt(char_sym, str[args(f, 2)[1]])); return char_sym; } diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp index c11b8ef4263..badfb97aefa 100644 --- a/src/solvers/refinement/string_constraint_generator_testing.cpp +++ b/src/solvers/refinement/string_constraint_generator_testing.cpp @@ -34,7 +34,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix( isprefix, str.axiom_for_length_ge(plus_exprt_with_overflow_check( prefix.length(), offset))); - m_axioms.push_back(a1); + lemmas_.push_back(a1); symbol_exprt qvar=fresh_univ_index("QA_isprefix", index_type); string_constraintt a2( @@ -43,7 +43,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix( isprefix, equal_exprt(str[plus_exprt_with_overflow_check(qvar, offset)], prefix[qvar])); - m_axioms.push_back(a2); + constraints_.push_back(a2); symbol_exprt witness=fresh_exist_index("witness_not_isprefix", index_type); and_exprt witness_diff( @@ -59,7 +59,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix( witness_diff); implies_exprt a3(not_exprt(isprefix), s0_notpref_s1); - m_axioms.push_back(a3); + lemmas_.push_back(a3); return isprefix; } @@ -99,8 +99,8 @@ exprt string_constraint_generatort::add_axioms_for_is_empty( symbol_exprt is_empty=fresh_boolean("is_empty"); string_exprt s0=get_string_expr(args(f, 1)[0]); - m_axioms.push_back(implies_exprt(is_empty, s0.axiom_for_has_length(0))); - m_axioms.push_back(implies_exprt(s0.axiom_for_has_length(0), is_empty)); + lemmas_.push_back(implies_exprt(is_empty, s0.axiom_for_has_length(0))); + lemmas_.push_back(implies_exprt(s0.axiom_for_has_length(0), is_empty)); return typecast_exprt(is_empty, f.type()); } @@ -133,14 +133,14 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix( // &&s1[witness]!=s0[witness + s0.length-s1.length] implies_exprt a1(issuffix, s1.axiom_for_length_ge(s0)); - m_axioms.push_back(a1); + lemmas_.push_back(a1); symbol_exprt qvar=fresh_univ_index("QA_suffix", index_type); exprt qvar_shifted=plus_exprt( qvar, minus_exprt(s1.length(), s0.length())); string_constraintt a2( qvar, s0.length(), issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])); - m_axioms.push_back(a2); + constraints_.push_back(a2); symbol_exprt witness=fresh_exist_index("witness_not_suffix", index_type); exprt shifted=plus_exprt( @@ -155,7 +155,7 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix( axiom_for_is_positive_index(witness)))); implies_exprt a3(not_exprt(issuffix), constr3); - m_axioms.push_back(a3); + lemmas_.push_back(a3); return tc_issuffix; } @@ -202,7 +202,7 @@ exprt string_constraint_generatort::add_axioms_for_contains( // exists witness < |s1|. s1[witness] != s0[witness + startpos]) implies_exprt a1(contains, s0.axiom_for_length_ge(s1)); - m_axioms.push_back(a1); + lemmas_.push_back(a1); symbol_exprt startpos=fresh_exist_index("startpos_contains", index_type); minus_exprt length_diff(s0.length(), s1.length()); @@ -210,18 +210,18 @@ exprt string_constraint_generatort::add_axioms_for_contains( axiom_for_is_positive_index(startpos), binary_relation_exprt(startpos, ID_le, length_diff)); implies_exprt a2(contains, bounds); - m_axioms.push_back(a2); + lemmas_.push_back(a2); implies_exprt a3( not_exprt(contains), equal_exprt(startpos, from_integer(-1, index_type))); - m_axioms.push_back(a3); + lemmas_.push_back(a3); 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])); - m_axioms.push_back(a4); + constraints_.push_back(a4); // We rewrite axiom a4 as: // forall startpos <= |s0|-|s1|. (!contains && |s0| >= |s1|) @@ -234,7 +234,7 @@ exprt string_constraint_generatort::add_axioms_for_contains( s1.length(), s0, s1); - m_axioms.push_back(a5); + not_contains_constraints_.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 5bbbba82c6c..bbed42c0424 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -35,7 +35,7 @@ string_exprt string_constraint_generatort::add_axioms_for_set_length( // a2 : forall i<|res|. i < |s1| ==> res[i] = s1[i] // a3 : forall i<|res|. i >= |s1| ==> res[i] = 0 - m_axioms.push_back(res.axiom_for_has_length(k)); + lemmas_.push_back(res.axiom_for_has_length(k)); symbol_exprt idx=fresh_univ_index( "QA_index_set_length", ref_type.get_index_type()); @@ -44,7 +44,7 @@ string_exprt string_constraint_generatort::add_axioms_for_set_length( res.length(), s1.axiom_for_length_gt(idx), equal_exprt(s1[idx], res[idx])); - m_axioms.push_back(a2); + constraints_.push_back(a2); symbol_exprt idx2=fresh_univ_index( "QA_index_set_length2", ref_type.get_index_type()); @@ -53,7 +53,7 @@ string_exprt string_constraint_generatort::add_axioms_for_set_length( res.length(), s1.axiom_for_length_le(idx2), equal_exprt(res[idx2], constant_char(0, ref_type.get_char_type()))); - m_axioms.push_back(a3); + constraints_.push_back(a3); return res; } @@ -113,21 +113,21 @@ string_exprt string_constraint_generatort::add_axioms_for_substring( implies_exprt a1( binary_relation_exprt(start, ID_lt, end), res.axiom_for_has_length(minus_exprt(end, start))); - m_axioms.push_back(a1); + lemmas_.push_back(a1); exprt is_empty=res.axiom_for_has_length(from_integer(0, index_type)); implies_exprt a2(binary_relation_exprt(start, ID_ge, end), is_empty); - m_axioms.push_back(a2); + lemmas_.push_back(a2); // Warning: check what to do if the string is not long enough - m_axioms.push_back(str.axiom_for_length_ge(end)); + lemmas_.push_back(str.axiom_for_length_ge(end)); symbol_exprt idx=fresh_univ_index("QA_index_substring", index_type); string_constraintt a4(idx, res.length(), equal_exprt(res[idx], str[plus_exprt(start, idx)])); - m_axioms.push_back(a4); + constraints_.push_back(a4); return res; } @@ -158,25 +158,25 @@ string_exprt string_constraint_generatort::add_axioms_for_trim( exprt a1=str.axiom_for_length_ge( plus_exprt_with_overflow_check(idx, res.length())); - m_axioms.push_back(a1); + lemmas_.push_back(a1); binary_relation_exprt a2(idx, ID_ge, from_integer(0, index_type)); - m_axioms.push_back(a2); + lemmas_.push_back(a2); exprt a3=str.axiom_for_length_ge(idx); - m_axioms.push_back(a3); + lemmas_.push_back(a3); exprt a4=res.axiom_for_length_ge( from_integer(0, index_type)); - m_axioms.push_back(a4); + lemmas_.push_back(a4); exprt a5=res.axiom_for_length_le(str); - m_axioms.push_back(a5); + lemmas_.push_back(a5); symbol_exprt n=fresh_univ_index("QA_index_trim", index_type); binary_relation_exprt non_print(str[n], ID_le, space_char); string_constraintt a6(n, idx, non_print); - m_axioms.push_back(a6); + constraints_.push_back(a6); symbol_exprt n2=fresh_univ_index("QA_index_trim2", index_type); minus_exprt bound(str.length(), plus_exprt_with_overflow_check(idx, @@ -187,12 +187,12 @@ string_exprt string_constraint_generatort::add_axioms_for_trim( space_char); string_constraintt a7(n2, bound, eqn2); - m_axioms.push_back(a7); + constraints_.push_back(a7); symbol_exprt n3=fresh_univ_index("QA_index_trim3", index_type); equal_exprt eqn3(res[n3], str[plus_exprt(n3, idx)]); string_constraintt a8(n3, res.length(), eqn3); - m_axioms.push_back(a8); + constraints_.push_back(a8); minus_exprt index_before( plus_exprt_with_overflow_check(idx, res.length()), @@ -203,7 +203,7 @@ string_exprt string_constraint_generatort::add_axioms_for_trim( and_exprt( binary_relation_exprt(str[idx], ID_gt, space_char), no_space_before)); - m_axioms.push_back(a9); + lemmas_.push_back(a9); return res; } @@ -235,7 +235,7 @@ string_exprt string_constraint_generatort::add_axioms_for_to_lower_case( // diff = 'a'-'A' = 0x20 exprt a1=res.axiom_for_has_same_length_as(str); - m_axioms.push_back(a1); + lemmas_.push_back(a1); symbol_exprt idx=fresh_univ_index("QA_lower_case", index_type); exprt::operandst upper_case; @@ -268,7 +268,7 @@ string_exprt string_constraint_generatort::add_axioms_for_to_lower_case( if_exprt conditional_convert(is_upper_case, converted, non_converted); string_constraintt a2(idx, res.length(), conditional_convert); - m_axioms.push_back(a2); + constraints_.push_back(a2); return res; } @@ -299,7 +299,7 @@ string_exprt string_constraint_generatort::add_axioms_for_to_upper_case( // axioms, so we use a trivial premise and push our premise into the body. exprt a1=res.axiom_for_has_same_length_as(str); - m_axioms.push_back(a1); + lemmas_.push_back(a1); symbol_exprt idx1=fresh_univ_index("QA_upper_case1", index_type); exprt is_lower_case=and_exprt( @@ -309,7 +309,7 @@ string_exprt string_constraint_generatort::add_axioms_for_to_upper_case( equal_exprt convert(res[idx1], plus_exprt(str[idx1], diff)); implies_exprt body1(is_lower_case, convert); string_constraintt a2(idx1, res.length(), body1); - m_axioms.push_back(a2); + constraints_.push_back(a2); symbol_exprt idx2=fresh_univ_index("QA_upper_case2", index_type); exprt is_not_lower_case=not_exprt(and_exprt( @@ -318,7 +318,7 @@ string_exprt string_constraint_generatort::add_axioms_for_to_upper_case( equal_exprt eq(res[idx2], str[idx2]); implies_exprt body2(is_not_lower_case, eq); string_constraintt a3(idx2, res.length(), body2); - m_axioms.push_back(a3); + constraints_.push_back(a3); return res; } @@ -355,7 +355,7 @@ string_exprt string_constraint_generatort::add_axioms_for_char_set( and_exprt( equal_exprt(res.content(), sarrnew), res.axiom_for_has_same_length_as(str))); - m_axioms.push_back(a1); + lemmas_.push_back(a1); return res; } @@ -379,7 +379,7 @@ string_exprt string_constraint_generatort::add_axioms_for_replace( // str[qvar]=oldChar => res[qvar]=newChar // !str[qvar]=oldChar => res[qvar]=str[qvar] - m_axioms.push_back(res.axiom_for_has_same_length_as(str)); + lemmas_.push_back(res.axiom_for_has_same_length_as(str)); symbol_exprt qvar=fresh_univ_index("QA_replace", ref_type.get_index_type()); implies_exprt case1( @@ -389,7 +389,7 @@ string_exprt string_constraint_generatort::add_axioms_for_replace( not_exprt(equal_exprt(str[qvar], old_char)), equal_exprt(res[qvar], str[qvar])); string_constraintt a2(qvar, res.length(), and_exprt(case1, case2)); - m_axioms.push_back(a2); + constraints_.push_back(a2); return res; } diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index f54a821f623..ed8d51193d0 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -94,24 +94,24 @@ string_exprt string_constraint_generatort::add_axioms_from_bool( std::string str_true="true"; implies_exprt a1(eq, res.axiom_for_has_length(str_true.length())); - m_axioms.push_back(a1); + lemmas_.push_back(a1); for(std::size_t i=0; i1) - m_axioms.push_back( + lemmas_.push_back( implies_exprt(premise, not_exprt(equal_exprt(res[0], zero_char)))); } return res; @@ -288,7 +288,7 @@ string_exprt string_constraint_generatort::add_axioms_from_char( { string_exprt res=fresh_string(ref_type); and_exprt lemma(equal_exprt(res[0], c), res.axiom_for_has_length(1)); - m_axioms.push_back(lemma); + lemmas_.push_back(lemma); return res; } @@ -323,30 +323,30 @@ void string_constraint_generatort::add_axioms_for_correct_number_format( // |str| > 0 const exprt non_empty=str.axiom_for_length_ge(from_integer(1, index_type)); - m_axioms.push_back(non_empty); + lemmas_.push_back(non_empty); if(strict_formatting) { // str[0] = '-' || is_digit_with_radix(str[0], radix) const or_exprt correct_first(starts_with_minus, starts_with_digit); - m_axioms.push_back(correct_first); + lemmas_.push_back(correct_first); } else { // str[0] = '-' || str[0] = '+' || is_digit_with_radix(str[0], radix) const or_exprt correct_first( starts_with_minus, starts_with_digit, starts_with_plus); - m_axioms.push_back(correct_first); + lemmas_.push_back(correct_first); } // str[0]='+' or '-' ==> |str| > 1 const implies_exprt contains_digit( or_exprt(starts_with_minus, starts_with_plus), str.axiom_for_length_ge(from_integer(2, index_type))); - m_axioms.push_back(contains_digit); + lemmas_.push_back(contains_digit); // |str| <= max_size - m_axioms.push_back(str.axiom_for_length_le(max_size)); + lemmas_.push_back(str.axiom_for_length_le(max_size)); // forall 1 <= i < |str| . is_digit_with_radix(str[i], radix) // We unfold the above because we know that it will be used for all i up to @@ -358,7 +358,7 @@ void string_constraint_generatort::add_axioms_for_correct_number_format( str.axiom_for_length_ge(from_integer(index+1, index_type)), is_digit_with_radix( str[index], strict_formatting, radix_as_char, radix_ul)); - m_axioms.push_back(character_at_index_is_digit); + lemmas_.push_back(character_at_index_is_digit); } if(strict_formatting) @@ -369,12 +369,12 @@ void string_constraint_generatort::add_axioms_for_correct_number_format( const implies_exprt no_leading_zero( equal_exprt(chr, zero_char), str.axiom_for_has_length(from_integer(1, index_type))); - m_axioms.push_back(no_leading_zero); + lemmas_.push_back(no_leading_zero); // no_leading_zero_after_minus : str[0]='-' => str[1]!='0' implies_exprt no_leading_zero_after_minus( starts_with_minus, not_exprt(equal_exprt(str[1], zero_char))); - m_axioms.push_back(no_leading_zero_after_minus); + lemmas_.push_back(no_leading_zero_after_minus); } } @@ -412,7 +412,7 @@ void string_constraint_generatort::add_axioms_for_characters_in_integer_string( /// Deal with size==1 case separately. There are axioms from /// add_axioms_for_correct_number_format which say that the string must /// contain at least one digit, so we don't have to worry about "+" or "-". - m_axioms.push_back( + lemmas_.push_back( implies_exprt(str.axiom_for_has_length(1), equal_exprt(input_int, sum))); for(size_t size=2; size<=max_string_length; size++) @@ -456,18 +456,18 @@ void string_constraint_generatort::add_axioms_for_characters_in_integer_string( if(!digit_constraints.empty()) { const implies_exprt a5(premise, conjunction(digit_constraints)); - m_axioms.push_back(a5); + lemmas_.push_back(a5); } const implies_exprt a6( and_exprt(premise, not_exprt(starts_with_minus)), equal_exprt(input_int, sum)); - m_axioms.push_back(a6); + lemmas_.push_back(a6); const implies_exprt a7( and_exprt(premise, starts_with_minus), equal_exprt(input_int, unary_minus_exprt(sum))); - m_axioms.push_back(a7); + lemmas_.push_back(a7); } } diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 6fdab35a97a..5a2e094014e 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -507,35 +507,30 @@ decision_proceduret::resultt string_refinementt::dec_solve() supert::set_to(pair.first, pair.second); } - for(exprt axiom : generator.get_axioms()) + for(string_constraintt constraint : generator.constraints()) { - replace_expr(symbol_resolve, axiom); - if(axiom.id()==ID_string_constraint) - { - string_constraintt univ_axiom= - to_string_constraint(axiom); - DATA_INVARIANT( - is_valid_string_constraint(error(), ns, univ_axiom), - string_refinement_invariantt( - "string constraints satisfy their invariant")); - axioms.universal.push_back(univ_axiom); - } - else if(axiom.id()==ID_string_not_contains_constraint) - { - string_not_contains_constraintt nc_axiom= - to_string_not_contains_constraint(axiom); - const refined_string_typet &rtype= - to_refined_string_type(nc_axiom.s0().type()); - const typet &index_type=rtype.get_index_type(); - array_typet witness_type(index_type, infinity_exprt(index_type)); - generator.witness[nc_axiom]= - generator.fresh_symbol("not_contains_witness", witness_type); - axioms.not_contains.push_back(nc_axiom); - } - else - { - add_lemma(axiom); - } + replace_expr(symbol_resolve, constraint); + DATA_INVARIANT( + is_valid_string_constraint(debug(), ns, constraint), + string_refinement_invariantt( + "string constraints satisfy their invariant")); + axioms.universal.push_back(constraint); + } + + for(auto nc_axiom : generator.not_contains_constraints()) + { + replace_expr(symbol_resolve, nc_axiom); + const refined_string_typet rtype=to_refined_string_type(nc_axiom.s0().type()); + const typet &index_type=rtype.get_index_type(); + const array_typet witness_type(index_type, infinity_exprt(index_type)); + generator.witness[nc_axiom]= + generator.fresh_symbol("not_contains_witness", witness_type); + axioms.not_contains.push_back(nc_axiom); + } + for(exprt lemma : generator.lemmas()) + { + replace_expr(symbol_resolve, lemma); + add_lemma(lemma); } found_length.clear(); From 61a32d36691ea9d99cd6409a60ed33733d9a82df Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sun, 17 Sep 2017 14:56:43 +0100 Subject: [PATCH 3/7] Drop string constraint:exprt inheritance --- src/solvers/refinement/string_constraint.h | 87 +++++++------------- src/solvers/refinement/string_refinement.cpp | 62 +++++++------- 2 files changed, 59 insertions(+), 90 deletions(-) diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index a7a7ccb5ca6..1c9f36ee6eb 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -23,8 +23,10 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include #include +#include #include #include +#include /*! \brief Universally quantified string constraint @@ -49,52 +51,37 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com is another implication which can be pushed in to \f$L(n)\f$. */ -class string_constraintt final: public exprt +struct string_constraintt final { -public: + exprt premise=true_exprt(); // Index guard + exprt body; // value constraint + symbol_exprt univ_var; + exprt lower_bound=from_integer(0, java_int_type()); + exprt upper_bound; // String constraints are of the form // forall univ_var in [lower_bound,upper_bound[. premise => body - - const exprt &premise() const - { - return op0(); - } - - const exprt &body() const - { - return op1(); - } - - const symbol_exprt &univ_var() const - { - return to_symbol_expr(op2()); - } - - const exprt &upper_bound() const + void replace(replace_mapt& symbol_resolve) { - return op3(); - } - - const exprt &lower_bound() const - { - return operands()[4]; - } + replace_expr(symbol_resolve, premise); + replace_expr(symbol_resolve, body); + replace_expr(symbol_resolve, univ_var); + replace_expr(symbol_resolve, upper_bound); + replace_expr(symbol_resolve, lower_bound); + }; - private: - string_constraintt(); + string_constraintt() = delete; - public: string_constraintt( const symbol_exprt &_univ_var, const exprt &bound_inf, const exprt &bound_sup, - const exprt &prem, // Index guard - const exprt &body): // value constraint - exprt(ID_string_constraint) - { - copy_to_operands(prem, body); - copy_to_operands(_univ_var, bound_sup, bound_inf); - } + const exprt &prem, + const exprt &body): + premise(prem), + body(body), + univ_var(_univ_var), + lower_bound(bound_inf), + upper_bound(bound_sup) { } // Default bound inferior is 0 string_constraintt( @@ -104,7 +91,7 @@ class string_constraintt final: public exprt const exprt &body): string_constraintt( _univ_var, - from_integer(0, _univ_var.type()), + from_integer(0, java_int_type()), bound_sup, prem, body) @@ -121,23 +108,11 @@ class string_constraintt final: public exprt exprt univ_within_bounds() const { return and_exprt( - binary_relation_exprt(lower_bound(), ID_le, univ_var()), - binary_relation_exprt(upper_bound(), ID_gt, univ_var())); + binary_relation_exprt(lower_bound, ID_le, univ_var), + binary_relation_exprt(upper_bound, ID_gt, univ_var)); } }; -extern inline const string_constraintt &to_string_constraint(const exprt &expr) -{ - PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5); - return static_cast(expr); -} - -extern inline string_constraintt &to_string_constraint(exprt &expr) -{ - PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5); - return static_cast(expr); -} - /// Used for debug printing. /// \param [in] ns: namespace for `from_expr` /// \param [in] identifier: identifier for `from_expr` @@ -148,11 +123,11 @@ inline std::string from_expr( const irep_idt &identifier, const string_constraintt &expr) { - return "forall "+from_expr(ns, identifier, expr.univ_var())+" in ["+ - from_expr(ns, identifier, expr.lower_bound())+", "+ - from_expr(ns, identifier, expr.upper_bound())+"). "+ - from_expr(ns, identifier, expr.premise())+" => "+ - from_expr(ns, identifier, expr.body()); + return "forall "+from_expr(ns, identifier, expr.univ_var)+" in ["+ + from_expr(ns, identifier, expr.lower_bound)+", "+ + from_expr(ns, identifier, expr.upper_bound)+"). "+ + from_expr(ns, identifier, expr.premise)+" => "+ + from_expr(ns, identifier, expr.body); } class string_not_contains_constraintt final: public exprt diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 5a2e094014e..1e51b4d8737 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -509,7 +509,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() for(string_constraintt constraint : generator.constraints()) { - replace_expr(symbol_resolve, constraint); + constraint.replace(symbol_resolve); DATA_INVARIANT( is_valid_string_constraint(debug(), ns, constraint), string_refinement_invariantt( @@ -1128,23 +1128,21 @@ static exprt negation_of_not_contains_constraint( static exprt negation_of_constraint(const string_constraintt &axiom) { // If the for all is vacuously true, the negation is false. - const exprt &lb=axiom.lower_bound(); - const exprt &ub=axiom.upper_bound(); - if(lb.id()==ID_constant && ub.id()==ID_constant) + if(axiom.lower_bound.is_constant() && axiom.upper_bound.is_constant()) { - const auto lb_int=expr_cast(lb); - const auto ub_int=expr_cast(ub); + const auto lb_int=expr_cast(axiom.lower_bound); + const auto ub_int=expr_cast(axiom.upper_bound); if(!lb_int || !ub_int || ub_int<=lb_int) return false_exprt(); } // If the premise is false, the implication is trivially true, so the // negation is false. - if(axiom.premise()==false_exprt()) + if(axiom.premise==false_exprt()) return false_exprt(); - and_exprt premise(axiom.premise(), axiom.univ_within_bounds()); - and_exprt negaxiom(premise, not_exprt(axiom.body())); + and_exprt premise(axiom.premise, axiom.univ_within_bounds()); + and_exprt negaxiom(premise, not_exprt(axiom.body)); return negaxiom; } @@ -1209,14 +1207,10 @@ static std::pair> check_axioms( for(size_t i=0; i> check_axioms( stream << " - negated_axiom_without_array_access:\n" << " " << from_expr(ns, "", with_concretized_arrays) << '\n'; - if(const auto &witness= - find_counter_example(ns, ui, with_concretized_arrays, univ_var)) + if(const auto witness= + find_counter_example(ns, ui, with_concretized_arrays, axiom.univ_var)) { stream << " - violated_for: " - << univ_var.get_identifier() + << axiom.univ_var.get_identifier() << "=" << from_expr(ns, "", *witness) << '\n'; violated[i]=*witness; } @@ -1331,14 +1325,14 @@ static std::pair> check_axioms( const exprt &val=v.second; const string_constraintt &axiom=axioms.universal[v.first]; - implies_exprt instance(axiom.premise(), axiom.body()); - replace_expr(axiom.univ_var(), val, instance); + implies_exprt instance(axiom.premise, axiom.body); + replace_expr(axiom.univ_var, val, instance); // We are not sure the index set contains only positive numbers exprt bounds=and_exprt( axiom.univ_within_bounds(), binary_relation_exprt( from_integer(0, val.type()), ID_le, val)); - replace_expr(axiom.univ_var(), val, bounds); + replace_expr(axiom.univ_var, val, bounds); const implies_exprt counter(bounds, instance); stream << " - " << from_expr(ns, "", counter) << eom; @@ -1641,9 +1635,9 @@ static void initial_index_set( const namespacet &ns, const string_constraintt &axiom) { - const symbol_exprt &qvar=axiom.univ_var(); + const symbol_exprt &qvar=axiom.univ_var; std::list to_process; - to_process.push_back(axiom.body()); + to_process.push_back(axiom.body); while(!to_process.empty()) { @@ -1666,8 +1660,8 @@ static void initial_index_set( // otherwise we add k-1 exprt e(i); const minus_exprt kminus1( - axiom.upper_bound(), - from_integer(1, axiom.upper_bound().type())); + axiom.upper_bound, + from_integer(1, axiom.upper_bound.type())); replace_expr(qvar, kminus1, e); add_to_index_set(index_set, ns, s, e); } @@ -1795,19 +1789,19 @@ static exprt instantiate( const exprt &str, const exprt &val) { - exprt idx=find_index(axiom.body(), str, axiom.univ_var()); + exprt idx=find_index(axiom.body, str, axiom.univ_var); if(idx.is_nil()) return true_exprt(); - exprt r=compute_inverse_function(stream, axiom.univ_var(), val, idx); - implies_exprt instance(axiom.premise(), axiom.body()); - replace_expr(axiom.univ_var(), r, instance); + exprt r=compute_inverse_function(stream, axiom.univ_var, val, idx); + implies_exprt instance(axiom.premise, axiom.body); + replace_expr(axiom.univ_var, r, instance); // We are not sure the index set contains only positive numbers exprt bounds=and_exprt( axiom.univ_within_bounds(), binary_relation_exprt( from_integer(0, val.type()), ID_le, val)); - replace_expr(axiom.univ_var(), r, bounds); + replace_expr(axiom.univ_var, r, bounds); return implies_exprt(bounds, instance); } @@ -2044,7 +2038,7 @@ static bool universal_only_in_index(const string_constraintt &expr) 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)); + stack.push(valuet(expr.body, 0)); while(!stack.empty()) { // Inspect current value @@ -2055,7 +2049,7 @@ static bool universal_only_in_index(const string_constraintt &expr) 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) + if(e==expr.univ_var && index_depth==0) return false; else forall_operands(it, e) @@ -2075,7 +2069,7 @@ static bool is_valid_string_constraint( { const auto eom=messaget::eom; // Condition 1: The premise cannot contain any string indices - const array_index_mapt premise_indices=gather_indices(expr.premise()); + const array_index_mapt premise_indices=gather_indices(expr.premise); if(!premise_indices.empty()) { stream << "Premise has indices: " << from_expr(ns, "", expr) << ", map: {"; @@ -2089,7 +2083,7 @@ static bool is_valid_string_constraint( return false; } - const array_index_mapt body_indices=gather_indices(expr.body()); + 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) From 3000ac9757eab6a5e011a54298e53d4cbad4a088 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Wed, 27 Sep 2017 11:19:15 +0100 Subject: [PATCH 4/7] Turn string_constraintt into a simple struct --- src/solvers/refinement/string_constraint.h | 72 +++++-------------- ...string_constraint_generator_comparison.cpp | 25 +++++-- .../string_constraint_generator_concat.cpp | 10 ++- .../string_constraint_generator_indexof.cpp | 58 ++++++++------- .../string_constraint_generator_main.cpp | 15 +++- .../string_constraint_generator_testing.cpp | 26 ++++--- ...ng_constraint_generator_transformation.cpp | 63 ++++++++++------ src/solvers/refinement/string_refinement.cpp | 17 +++-- 8 files changed, 160 insertions(+), 126 deletions(-) diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index 1c9f36ee6eb..7cd27678f68 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -49,6 +49,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com 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$. + + String constraints are of the form + forall univ_var in [lower_bound,upper_bound[. premise => body */ struct string_constraintt final @@ -58,61 +61,24 @@ struct string_constraintt final symbol_exprt univ_var; exprt lower_bound=from_integer(0, java_int_type()); exprt upper_bound; - // String constraints are of the form - // forall univ_var in [lower_bound,upper_bound[. premise => body - void replace(replace_mapt& symbol_resolve) - { - replace_expr(symbol_resolve, premise); - replace_expr(symbol_resolve, body); - replace_expr(symbol_resolve, univ_var); - replace_expr(symbol_resolve, upper_bound); - replace_expr(symbol_resolve, lower_bound); - }; - - string_constraintt() = delete; - - string_constraintt( - const symbol_exprt &_univ_var, - const exprt &bound_inf, - const exprt &bound_sup, - const exprt &prem, - const exprt &body): - premise(prem), - body(body), - univ_var(_univ_var), - lower_bound(bound_inf), - upper_bound(bound_sup) { } - - // Default bound inferior is 0 - string_constraintt( - const symbol_exprt &_univ_var, - const exprt &bound_sup, - const exprt &prem, - const exprt &body): - string_constraintt( - _univ_var, - from_integer(0, java_int_type()), - bound_sup, - prem, - body) - {} - - // Default premise is true - string_constraintt( - const symbol_exprt &_univ_var, - const exprt &bound_sup, - const exprt &body): - string_constraintt(_univ_var, bound_sup, true_exprt(), body) - {} - - exprt univ_within_bounds() const - { - return and_exprt( - binary_relation_exprt(lower_bound, ID_le, univ_var), - binary_relation_exprt(upper_bound, ID_gt, univ_var)); - } }; +inline void replace(string_constraintt &axiom, const replace_mapt& symbol_resolve) +{ + replace_expr(symbol_resolve, axiom.premise); + replace_expr(symbol_resolve, axiom.body); + replace_expr(symbol_resolve, axiom.univ_var); + replace_expr(symbol_resolve, axiom.upper_bound); + replace_expr(symbol_resolve, axiom.lower_bound); +} + +inline exprt univ_within_bounds(const string_constraintt &axiom) +{ + return and_exprt( + binary_relation_exprt(axiom.lower_bound, ID_le, axiom.univ_var), + binary_relation_exprt(axiom.upper_bound, ID_gt, axiom.univ_var)); +} + /// Used for debug printing. /// \param [in] ns: namespace for `from_expr` /// \param [in] identifier: identifier for `from_expr` diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp index 511ecfdff48..de9bdb5cc6c 100644 --- a/src/solvers/refinement/string_constraint_generator_comparison.cpp +++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp @@ -42,7 +42,11 @@ exprt string_constraint_generatort::add_axioms_for_equals( lemmas_.push_back(a1); symbol_exprt qvar=fresh_univ_index("QA_equal", index_type); - string_constraintt a2(qvar, s1.length(), eq, equal_exprt(s1[qvar], s2[qvar])); + string_constraintt a2; + a2.univ_var=qvar; + a2.upper_bound=s1.length(); + a2.premise=eq; + a2.body=equal_exprt(s1[qvar], s2[qvar]); constraints_.push_back(a2); symbol_exprt witness=fresh_exist_index("witness_unequal", index_type); @@ -122,7 +126,11 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case( symbol_exprt qvar=fresh_univ_index("QA_equal_ignore_case", index_type); exprt constr2=character_equals_ignore_case( s1[qvar], s2[qvar], char_a, char_A, char_Z); - string_constraintt a2(qvar, s1.length(), eq, constr2); + string_constraintt a2; + a2.univ_var=qvar; + a2.upper_bound=s1.length(); + a2.premise=eq; + a2.body=constr2; constraints_.push_back(a2); symbol_exprt witness=fresh_exist_index( @@ -214,7 +222,11 @@ exprt string_constraint_generatort::add_axioms_for_compare_to( lemmas_.push_back(a1); symbol_exprt i=fresh_univ_index("QA_compare_to", index_type); - string_constraintt a2(i, s1.length(), res_null, equal_exprt(s1[i], s2[i])); + string_constraintt a2; + a2.univ_var=i; + a2.upper_bound=s1.length(); + a2.premise=res_null; + a2.body=equal_exprt(s1[i], s2[i]); constraints_.push_back(a2); symbol_exprt x=fresh_exist_index("index_compare_to", index_type); @@ -245,8 +257,11 @@ exprt string_constraint_generatort::add_axioms_for_compare_to( lemmas_.push_back(a3); symbol_exprt i2=fresh_univ_index("QA_compare_to", index_type); - string_constraintt a4( - i2, x, not_exprt(res_null), equal_exprt(s1[i2], s2[i2])); + string_constraintt a4; + a4.univ_var=i2; + a4.upper_bound=x; + a4.premise=not_exprt(res_null); + a4.body=equal_exprt(s1[i2], s2[i2]); constraints_.push_back(a4); return res; diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index 3d8a7a0367f..6ee92397d12 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -52,13 +52,19 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_substr( lemmas_.push_back(a2); symbol_exprt idx=fresh_univ_index("QA_index_concat", res.length().type()); - string_constraintt a3(idx, s1.length(), equal_exprt(s1[idx], res[idx])); + string_constraintt a3; + a3.univ_var=idx; + a3.upper_bound=s1.length(); + a3.body=equal_exprt(s1[idx], res[idx]); constraints_.push_back(a3); symbol_exprt idx2=fresh_univ_index("QA_index_concat2", res.length().type()); equal_exprt res_eq( res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start_index, idx2)]); - string_constraintt a4(idx2, minus_exprt(end_index, start_index), res_eq); + string_constraintt a4; + a4.univ_var=idx2; + a4.upper_bound=minus_exprt(end_index, start_index); + a4.body=res_eq; constraints_.push_back(a4); return res; diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index 77056399237..8166fe4430b 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -52,17 +52,21 @@ exprt string_constraint_generatort::add_axioms_for_index_of( lemmas_.push_back(a3); symbol_exprt n=fresh_univ_index("QA_index_of", index_type); - string_constraintt a4( - n, from_index, index, contains, not_exprt(equal_exprt(str[n], c))); + string_constraintt a4; + a4.univ_var=n; + a4.lower_bound=from_index; + a4.upper_bound=index; + a4.premise=contains; + a4.body=not_exprt(equal_exprt(str[n], c)); constraints_.push_back(a4); symbol_exprt m=fresh_univ_index("QA_index_of", index_type); - string_constraintt a5( - m, - from_index, - str.length(), - not_exprt(contains), - not_exprt(equal_exprt(str[m], c))); + string_constraintt a5; + a5.univ_var=m, + a5.lower_bound=from_index, + a5.upper_bound=str.length(), + a5.premise=not_exprt(contains), + a5.body=not_exprt(equal_exprt(str[m], c)); constraints_.push_back(a5); return index; @@ -109,11 +113,11 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( lemmas_.push_back(a2); symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type); - string_constraintt a3( - qvar, - needle.length(), - contains, - equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])); + string_constraintt a3; + a3.univ_var=qvar; + a3.upper_bound=needle.length(); + a3.premise=contains; + a3.body=equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar]); constraints_.push_back(a3); // string_not contains_constraintt are formulas of the form: @@ -190,7 +194,11 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string( symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type); equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]); - string_constraintt a3(qvar, needle.length(), contains, constr3); + string_constraintt a3; + a3.univ_var=qvar; + a3.upper_bound=needle.length(); + a3.premise=contains; + a3.body=constr3; constraints_.push_back(a3); // end_index is min(from_index, |str| - |substring|) @@ -302,20 +310,20 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of( lemmas_.push_back(a3); symbol_exprt n=fresh_univ_index("QA_last_index_of1", index_type); - string_constraintt a4( - n, - plus_exprt(index, index1), - from_index_plus_one, - contains, - not_exprt(equal_exprt(str[n], c))); + string_constraintt a4; + a4.univ_var=n; + a4.lower_bound=plus_exprt(index, index1); + a4.upper_bound=from_index_plus_one; + a4.premise=contains; + a4.body=not_exprt(equal_exprt(str[n], c)); constraints_.push_back(a4); symbol_exprt m=fresh_univ_index("QA_last_index_of2", index_type); - string_constraintt a5( - m, - from_index_plus_one, - not_exprt(contains), - not_exprt(equal_exprt(str[m], c))); + string_constraintt a5; + a5.univ_var=m; + a5.upper_bound=from_index_plus_one; + a5.premise=not_exprt(contains); + a5.body=not_exprt(equal_exprt(str[m], c)); constraints_.push_back(a5); return index; diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 02748d487a7..c415bf252fc 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -195,7 +195,10 @@ void string_constraint_generatort::add_default_axioms( and_exprt printable( binary_relation_exprt(chr, ID_ge, from_integer(' ', chr.type())), binary_relation_exprt(chr, ID_le, from_integer('~', chr.type()))); - string_constraintt sc(qvar, s.length(), printable); + string_constraintt sc; + sc.univ_var=qvar; + sc.upper_bound=s.length(); + sc.body=printable; constraints_.push_back(sc); } } @@ -286,13 +289,19 @@ string_exprt string_constraint_generatort::add_axioms_for_if( implies_exprt(expr.cond(), res.axiom_for_has_same_length_as(t))); symbol_exprt qvar=fresh_univ_index("QA_string_if_true", index_type); equal_exprt qequal(res[qvar], t[qvar]); - string_constraintt sc1(qvar, t.length(), implies_exprt(expr.cond(), qequal)); + string_constraintt sc1; + sc1.univ_var=qvar; + sc1.upper_bound=t.length(); + sc1.body=implies_exprt(expr.cond(), qequal); constraints_.push_back(sc1); lemmas_.push_back( implies_exprt(not_exprt(expr.cond()), res.axiom_for_has_same_length_as(f))); symbol_exprt qvar2=fresh_univ_index("QA_string_if_false", index_type); equal_exprt qequal2(res[qvar2], f[qvar2]); - string_constraintt sc2(qvar2, f.length(), or_exprt(expr.cond(), qequal2)); + string_constraintt sc2; + sc2.univ_var=qvar2; + sc2.upper_bound=f.length(); + sc2.body=or_exprt(expr.cond(), qequal2); constraints_.push_back(sc2); return res; } diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp index badfb97aefa..4d62bb595fb 100644 --- a/src/solvers/refinement/string_constraint_generator_testing.cpp +++ b/src/solvers/refinement/string_constraint_generator_testing.cpp @@ -37,12 +37,12 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix( lemmas_.push_back(a1); symbol_exprt qvar=fresh_univ_index("QA_isprefix", index_type); - string_constraintt a2( - qvar, - prefix.length(), - isprefix, - equal_exprt(str[plus_exprt_with_overflow_check(qvar, offset)], - prefix[qvar])); + string_constraintt a2; + a2.univ_var=qvar; + a2.upper_bound=prefix.length(); + a2.premise=isprefix; + a2.body=equal_exprt( + str[plus_exprt_with_overflow_check(qvar, offset)], prefix[qvar]); constraints_.push_back(a2); symbol_exprt witness=fresh_exist_index("witness_not_isprefix", index_type); @@ -138,8 +138,11 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix( symbol_exprt qvar=fresh_univ_index("QA_suffix", index_type); exprt qvar_shifted=plus_exprt( qvar, minus_exprt(s1.length(), s0.length())); - string_constraintt a2( - qvar, s0.length(), issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])); + string_constraintt a2; + a2.univ_var=qvar; + a2.upper_bound=s0.length(); + a2.premise=issuffix; + a2.body=equal_exprt(s0[qvar], s1[qvar_shifted]); constraints_.push_back(a2); symbol_exprt witness=fresh_exist_index("witness_not_suffix", index_type); @@ -219,8 +222,11 @@ exprt string_constraint_generatort::add_axioms_for_contains( 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])); + string_constraintt a4; + a4.univ_var=qvar; + a4.upper_bound=s1.length(); + a4.premise=contains; + a4.body=equal_exprt(s1[qvar], s0[qvar_shifted]); constraints_.push_back(a4); // We rewrite axiom a4 as: diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index bbed42c0424..36671785dee 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -39,20 +39,20 @@ string_exprt string_constraint_generatort::add_axioms_for_set_length( symbol_exprt idx=fresh_univ_index( "QA_index_set_length", ref_type.get_index_type()); - string_constraintt a2( - idx, - res.length(), - s1.axiom_for_length_gt(idx), - equal_exprt(s1[idx], res[idx])); + string_constraintt a2; + a2.univ_var=idx; + a2.upper_bound=res.length(); + a2.premise=s1.axiom_for_length_gt(idx); + a2.body=equal_exprt(s1[idx], res[idx]); constraints_.push_back(a2); symbol_exprt idx2=fresh_univ_index( "QA_index_set_length2", ref_type.get_index_type()); - string_constraintt a3( - idx2, - res.length(), - s1.axiom_for_length_le(idx2), - equal_exprt(res[idx2], constant_char(0, ref_type.get_char_type()))); + string_constraintt a3; + a3.univ_var=idx2; + a3.upper_bound=res.length(); + a3.premise=s1.axiom_for_length_le(idx2); + a3.body=equal_exprt(res[idx2], constant_char(0, ref_type.get_char_type())); constraints_.push_back(a3); return res; @@ -123,10 +123,10 @@ string_exprt string_constraint_generatort::add_axioms_for_substring( lemmas_.push_back(str.axiom_for_length_ge(end)); symbol_exprt idx=fresh_univ_index("QA_index_substring", index_type); - string_constraintt a4(idx, - res.length(), - equal_exprt(res[idx], - str[plus_exprt(start, idx)])); + string_constraintt a4; + a4.univ_var=idx; + a4.upper_bound=res.length(); + a4.body=equal_exprt(res[idx], str[plus_exprt(start, idx)]); constraints_.push_back(a4); return res; } @@ -175,7 +175,10 @@ string_exprt string_constraint_generatort::add_axioms_for_trim( symbol_exprt n=fresh_univ_index("QA_index_trim", index_type); binary_relation_exprt non_print(str[n], ID_le, space_char); - string_constraintt a6(n, idx, non_print); + string_constraintt a6; + a6.univ_var=n; + a6.upper_bound=idx; + a6.body=non_print; constraints_.push_back(a6); symbol_exprt n2=fresh_univ_index("QA_index_trim2", index_type); @@ -186,12 +189,18 @@ string_exprt string_constraint_generatort::add_axioms_for_trim( ID_le, space_char); - string_constraintt a7(n2, bound, eqn2); + string_constraintt a7; + a7.univ_var=n2; + a7.upper_bound=bound; + a7.body=eqn2; constraints_.push_back(a7); symbol_exprt n3=fresh_univ_index("QA_index_trim3", index_type); equal_exprt eqn3(res[n3], str[plus_exprt(n3, idx)]); - string_constraintt a8(n3, res.length(), eqn3); + string_constraintt a8; + a8.univ_var=n3; + a8.upper_bound=res.length(); + a8.body=eqn3; constraints_.push_back(a8); minus_exprt index_before( @@ -267,7 +276,10 @@ string_exprt string_constraint_generatort::add_axioms_for_to_lower_case( binary_relation_exprt(str[idx], ID_lt, from_integer(0x100, char_type))); if_exprt conditional_convert(is_upper_case, converted, non_converted); - string_constraintt a2(idx, res.length(), conditional_convert); + string_constraintt a2; + a2.univ_var=idx; + a2.upper_bound=res.length(); + a2.body=conditional_convert; constraints_.push_back(a2); return res; @@ -308,7 +320,10 @@ string_exprt string_constraint_generatort::add_axioms_for_to_upper_case( minus_exprt diff(char_A, char_a); equal_exprt convert(res[idx1], plus_exprt(str[idx1], diff)); implies_exprt body1(is_lower_case, convert); - string_constraintt a2(idx1, res.length(), body1); + string_constraintt a2; + a2.univ_var=idx1; + a2.upper_bound=res.length(); + a2.body=body1; constraints_.push_back(a2); symbol_exprt idx2=fresh_univ_index("QA_upper_case2", index_type); @@ -317,7 +332,10 @@ string_exprt string_constraint_generatort::add_axioms_for_to_upper_case( 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); + string_constraintt a3; + a3.univ_var=idx2; + a3.upper_bound=res.length(); + a3.body=body2; constraints_.push_back(a3); return res; } @@ -388,7 +406,10 @@ string_exprt string_constraint_generatort::add_axioms_for_replace( implies_exprt case2( not_exprt(equal_exprt(str[qvar], old_char)), equal_exprt(res[qvar], str[qvar])); - string_constraintt a2(qvar, res.length(), and_exprt(case1, case2)); + string_constraintt a2; + a2.univ_var=qvar; + a2.upper_bound=res.length(); + a2.body=and_exprt(case1, case2); constraints_.push_back(a2); return res; } diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 1e51b4d8737..3e8ba663244 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -509,7 +509,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() for(string_constraintt constraint : generator.constraints()) { - constraint.replace(symbol_resolve); + replace(constraint, symbol_resolve); DATA_INVARIANT( is_valid_string_constraint(debug(), ns, constraint), string_refinement_invariantt( @@ -1141,7 +1141,7 @@ static exprt negation_of_constraint(const string_constraintt &axiom) if(axiom.premise==false_exprt()) return false_exprt(); - and_exprt premise(axiom.premise, axiom.univ_within_bounds()); + and_exprt premise(axiom.premise, univ_within_bounds(axiom)); and_exprt negaxiom(premise, not_exprt(axiom.body)); return negaxiom; @@ -1208,9 +1208,12 @@ static std::pair> check_axioms( { const string_constraintt &axiom=axioms.universal[i]; - const string_constraintt axiom_in_model( - axiom.univ_var, get(axiom.lower_bound), get(axiom.upper_bound), - get(axiom.premise), get(axiom.body)); + string_constraintt axiom_in_model; + axiom_in_model.univ_var=axiom.univ_var; + axiom_in_model.lower_bound=get(axiom.lower_bound); + axiom_in_model.upper_bound=get(axiom.upper_bound); + axiom_in_model.premise=get(axiom.premise); + axiom_in_model.body=get(axiom.body); exprt negaxiom=negation_of_constraint(axiom_in_model); @@ -1329,7 +1332,7 @@ static std::pair> check_axioms( replace_expr(axiom.univ_var, val, instance); // We are not sure the index set contains only positive numbers exprt bounds=and_exprt( - axiom.univ_within_bounds(), + univ_within_bounds(axiom), binary_relation_exprt( from_integer(0, val.type()), ID_le, val)); replace_expr(axiom.univ_var, val, bounds); @@ -1798,7 +1801,7 @@ static exprt instantiate( replace_expr(axiom.univ_var, r, instance); // We are not sure the index set contains only positive numbers exprt bounds=and_exprt( - axiom.univ_within_bounds(), + univ_within_bounds(axiom), binary_relation_exprt( from_integer(0, val.type()), ID_le, val)); replace_expr(axiom.univ_var, r, bounds); From 016d37483fdfeb0662885dfac6a364a5cdc3ef94 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Wed, 27 Sep 2017 11:47:30 +0100 Subject: [PATCH 5/7] Move string_constraint function definitions to cpp file --- src/solvers/Makefile | 1 + src/solvers/refinement/string_constraint.cpp | 66 ++++++++++++++++++ src/solvers/refinement/string_constraint.h | 70 ++++---------------- src/solvers/refinement/string_refinement.h | 1 + 4 files changed, 80 insertions(+), 58 deletions(-) create mode 100644 src/solvers/refinement/string_constraint.cpp diff --git a/src/solvers/Makefile b/src/solvers/Makefile index a3e7219db4d..4975c7a93c9 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -168,6 +168,7 @@ SRC = $(BOOLEFORCE_SRC) \ refinement/refine_arithmetic.cpp \ refinement/refine_arrays.cpp \ refinement/string_refinement.cpp \ + refinement/string_constraint.cpp \ refinement/string_constraint_generator_code_points.cpp \ refinement/string_constraint_generator_comparison.cpp \ refinement/string_constraint_generator_concat.cpp \ diff --git a/src/solvers/refinement/string_constraint.cpp b/src/solvers/refinement/string_constraint.cpp new file mode 100644 index 00000000000..bf39191da48 --- /dev/null +++ b/src/solvers/refinement/string_constraint.cpp @@ -0,0 +1,66 @@ +#include "string_constraint.h" + +void replace(string_constraintt &axiom, const replace_mapt& symbol_resolve) +{ + replace_expr(symbol_resolve, axiom.premise); + replace_expr(symbol_resolve, axiom.body); + replace_expr(symbol_resolve, axiom.univ_var); + replace_expr(symbol_resolve, axiom.upper_bound); + replace_expr(symbol_resolve, axiom.lower_bound); +} + +exprt univ_within_bounds(const string_constraintt &axiom) +{ + return and_exprt( + binary_relation_exprt(axiom.lower_bound, ID_le, axiom.univ_var), + binary_relation_exprt(axiom.upper_bound, ID_gt, axiom.univ_var)); +} + +std::string from_expr( + const namespacet &ns, + const irep_idt &identifier, + const string_constraintt &expr) +{ + return "forall "+from_expr(ns, identifier, expr.univ_var)+" in ["+ + from_expr(ns, identifier, expr.lower_bound)+", "+ + from_expr(ns, identifier, expr.upper_bound)+"). "+ + from_expr(ns, identifier, expr.premise)+" => "+ + from_expr(ns, identifier, expr.body); +} + +std::string from_expr( + const namespacet &ns, + const irep_idt &identifier, + const string_not_contains_constraintt &expr) +{ + return "forall x in ["+ + from_expr(ns, identifier, expr.univ_lower_bound())+", "+ + from_expr(ns, identifier, expr.univ_upper_bound())+"). "+ + from_expr(ns, identifier, expr.premise())+" => ("+ + "exists y in ["+from_expr(ns, identifier, expr.exists_lower_bound())+", "+ + from_expr(ns, identifier, expr.exists_upper_bound())+"). "+ + from_expr(ns, identifier, expr.s0())+"[x+y] != "+ + from_expr(ns, identifier, expr.s1())+"[y])"; +} + +const string_not_contains_constraintt +&to_string_not_contains_constraint(const exprt &expr) +{ + PRECONDITION(expr.id()==ID_string_not_contains_constraint); + DATA_INVARIANT( + expr.operands().size()==7, + string_refinement_invariantt("string_not_contains_constraintt must have 7 " + "operands")); + return static_cast(expr); +} + +string_not_contains_constraintt +&to_string_not_contains_constraint(exprt &expr) +{ + PRECONDITION(expr.id()==ID_string_not_contains_constraint); + DATA_INVARIANT( + expr.operands().size()==7, + string_refinement_invariantt("string_not_contains_constraintt must have 7 " + "operands")); + return static_cast(expr); +} diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index 7cd27678f68..fb58b1caa4b 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -63,38 +63,19 @@ struct string_constraintt final exprt upper_bound; }; -inline void replace(string_constraintt &axiom, const replace_mapt& symbol_resolve) -{ - replace_expr(symbol_resolve, axiom.premise); - replace_expr(symbol_resolve, axiom.body); - replace_expr(symbol_resolve, axiom.univ_var); - replace_expr(symbol_resolve, axiom.upper_bound); - replace_expr(symbol_resolve, axiom.lower_bound); -} - -inline exprt univ_within_bounds(const string_constraintt &axiom) -{ - return and_exprt( - binary_relation_exprt(axiom.lower_bound, ID_le, axiom.univ_var), - binary_relation_exprt(axiom.upper_bound, ID_gt, axiom.univ_var)); -} +void replace(string_constraintt &axiom, const replace_mapt& symbol_resolve); + +exprt univ_within_bounds(const string_constraintt &axiom); /// Used for debug printing. /// \param [in] ns: namespace for `from_expr` /// \param [in] identifier: identifier for `from_expr` /// \param [in] expr: constraint to render /// \return rendered string -inline std::string from_expr( +std::string from_expr( const namespacet &ns, const irep_idt &identifier, - const string_constraintt &expr) -{ - return "forall "+from_expr(ns, identifier, expr.univ_var)+" in ["+ - from_expr(ns, identifier, expr.lower_bound)+", "+ - from_expr(ns, identifier, expr.upper_bound)+"). "+ - from_expr(ns, identifier, expr.premise)+" => "+ - from_expr(ns, identifier, expr.body); -} + const string_constraintt &expr); class string_not_contains_constraintt final: public exprt { @@ -158,41 +139,14 @@ class string_not_contains_constraintt final: public exprt /// \param [in] identifier: identifier for `from_expr` /// \param [in] expr: constraint to render /// \return rendered string -inline std::string from_expr( +std::string from_expr( const namespacet &ns, const irep_idt &identifier, - const string_not_contains_constraintt &expr) -{ - return "forall x in ["+ - from_expr(ns, identifier, expr.univ_lower_bound())+", "+ - from_expr(ns, identifier, expr.univ_upper_bound())+"). "+ - from_expr(ns, identifier, expr.premise())+" => ("+ - "exists y in ["+from_expr(ns, identifier, expr.exists_lower_bound())+", "+ - from_expr(ns, identifier, expr.exists_upper_bound())+"). "+ - from_expr(ns, identifier, expr.s0())+"[x+y] != "+ - from_expr(ns, identifier, expr.s1())+"[y])"; -} - -inline const string_not_contains_constraintt -&to_string_not_contains_constraint(const exprt &expr) -{ - PRECONDITION(expr.id()==ID_string_not_contains_constraint); - DATA_INVARIANT( - expr.operands().size()==7, - string_refinement_invariantt("string_not_contains_constraintt must have 7 " - "operands")); - return static_cast(expr); -} - -inline string_not_contains_constraintt -&to_string_not_contains_constraint(exprt &expr) -{ - PRECONDITION(expr.id()==ID_string_not_contains_constraint); - DATA_INVARIANT( - expr.operands().size()==7, - string_refinement_invariantt("string_not_contains_constraintt must have 7 " - "operands")); - return static_cast(expr); -} + const string_not_contains_constraintt &expr); + +const string_not_contains_constraintt +&to_string_not_contains_constraint(const exprt &expr); + +string_not_contains_constraintt &to_string_not_contains_constraint(exprt &expr); #endif diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index d6c7814367a..ec505518d46 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -109,4 +109,5 @@ class string_refinementt final: public bv_refinementt exprt substitute_array_lists(exprt expr, std::size_t string_max_length); exprt concretize_arrays_in_expression( exprt expr, std::size_t string_max_length); + #endif From ba1a89bec146c2102b1495af9bb2e09f06191787 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Wed, 27 Sep 2017 11:53:25 +0100 Subject: [PATCH 6/7] Move string_constraint functions out of string_refinement --- src/solvers/refinement/string_constraint.cpp | 163 ++++++++++++++++++ src/solvers/refinement/string_constraint.h | 9 + src/solvers/refinement/string_refinement.cpp | 170 ------------------- 3 files changed, 172 insertions(+), 170 deletions(-) diff --git a/src/solvers/refinement/string_constraint.cpp b/src/solvers/refinement/string_constraint.cpp index bf39191da48..5e132a86f71 100644 --- a/src/solvers/refinement/string_constraint.cpp +++ b/src/solvers/refinement/string_constraint.cpp @@ -1,4 +1,6 @@ +#include #include "string_constraint.h" +#include void replace(string_constraintt &axiom, const replace_mapt& symbol_resolve) { @@ -64,3 +66,164 @@ string_not_contains_constraintt "operands")); return static_cast(expr); } + +/// \related string_constraintt +typedef std::map> 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; +} + +bool is_valid_string_constraint( + messaget::mstreamt &stream, + const namespacet &ns, + const string_constraintt &expr) +{ + const auto eom=messaget::eom; + // Condition 1: The premise cannot contain any string indices + const array_index_mapt premise_indices=gather_indices(expr.premise); + if(!premise_indices.empty()) + { + stream << "Premise has indices: " << from_expr(ns, "", expr) << ", map: {"; + for(const auto &pair : premise_indices) + { + stream << from_expr(ns, "", pair.first) << ": {"; + for(const auto &i : pair.second) + stream << from_expr(ns, "", i) << ", "; + } + stream << "}}" << 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 find_counter_example( const namespacet &ns, ui_message_handlert::uit ui, @@ -1961,168 +1956,3 @@ static optionalt find_counter_example( else return { }; } - -/// \related string_constraintt -typedef std::map> 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 -static bool is_valid_string_constraint( - messaget::mstreamt &stream, - const namespacet &ns, - const string_constraintt &expr) -{ - const auto eom=messaget::eom; - // Condition 1: The premise cannot contain any string indices - const array_index_mapt premise_indices=gather_indices(expr.premise); - if(!premise_indices.empty()) - { - stream << "Premise has indices: " << from_expr(ns, "", expr) << ", map: {"; - for(const auto &pair : premise_indices) - { - stream << from_expr(ns, "", pair.first) << ": {"; - for(const auto &i : pair.second) - stream << from_expr(ns, "", i) << ", "; - } - stream << "}}" << 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 Date: Sun, 17 Sep 2017 16:51:12 +0100 Subject: [PATCH 7/7] Add environment class --- src/solvers/refinement/environment.h | 78 ++++++++++++++++++++++++++++ 1 file changed, 78 insertions(+) create mode 100644 src/solvers/refinement/environment.h diff --git a/src/solvers/refinement/environment.h b/src/solvers/refinement/environment.h new file mode 100644 index 00000000000..41f1de7c698 --- /dev/null +++ b/src/solvers/refinement/environment.h @@ -0,0 +1,78 @@ +class environmentt +{ +public: + static environmentt java() { + environmentt env; + env.int_type_=java_int_type(); + env.char_type_=java_int_type(); + env.array_type_=array_typet(env.char_type_, infinity_exprt(env.int_type_)); + env.string_type_=refined_string_typet(env.int_type_, env.char_type_); + return env; + } + + template< + typename T, + typename std::enable_if::value, int>::type=0> + T make_expr(T&& expr) + { return std::move(expr); } + + constant_exprt make_expr(char i) + { return from_integer(i, char_type_); } + + template< + typename T, + typename std::enable_if::value, int>::type=0> + constant_exprt make_expr(const T& i) + { return from_integer(i, int_type_); } + + template< + typename T, + typename std::enable_if::value, int>::type=0> + string_exprt make_expr(const T &str) + { + const constant_exprt length=make_expr(str.length()); + array_exprt content(array_type_); + for(const char ch : str) + content.copy_to_operands(make_expr(ch)); + return string_exprt(length, content, string_type_); + } + + template< + typename T, + typename std::enable_if< + std::is_convertible::value && + !std::is_same::value, int>::type=0> + string_exprt make_expr(const T &str) + { return make_expr(std::string(str)); } + + template + function_application_exprt make_expr( + const dstringt &id, + typet return_type, + Args&&... args) + { + function_application_exprt func(symbol_exprt(id), return_type); + func.arguments() = { make_expr(std::forward(args))... }; + return func; + } + + struct_exprt make_struct_expr(std::map members) + { + struct_typet type; + for (const auto& pair : members) { + type.components().push_back({ pair.first, pair.second.type() }); + } + struct_exprt expr(type); + for (const auto& pair : members) { + expr.operands().push_back(pair.second); + } + return expr; + } +private: + environmentt()=default; + + typet int_type_; + typet char_type_; + typet array_type_; + typet string_type_; +};