diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index c53c34375e3..d98b8b3dcca 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -146,20 +146,22 @@ std::unique_ptr cbmc_solverst::get_bv_refinement() prop->set_message_handler(get_message_handler()); - auto bv_refinement=util_make_unique(ns, *prop); - bv_refinement->set_ui(ui); + bv_refinementt::infot info; + info.ns=&ns; + info.prop=prop.get(); + info.ui=ui; // we allow setting some parameters - if(options.get_option("max-node-refinement")!="") - bv_refinement->max_node_refinement = + if(options.get_bool_option("max-node-refinement")) + info.max_node_refinement= options.get_unsigned_int_option("max-node-refinement"); - bv_refinement->do_array_refinement = - options.get_bool_option("refine-arrays"); - bv_refinement->do_arithmetic_refinement = - options.get_bool_option("refine-arithmetic"); + info.refine_arrays=options.get_bool_option("refine-arrays"); + info.refine_arithmetic=options.get_bool_option("refine-arithmetic"); - return util_make_unique(std::move(bv_refinement), std::move(prop)); + return util_make_unique( + util_make_unique(info), + std::move(prop)); } /// the string refinement adds to the bit vector refinement specifications for @@ -167,33 +169,26 @@ std::unique_ptr cbmc_solverst::get_bv_refinement() /// \return a solver for cbmc std::unique_ptr cbmc_solverst::get_string_refinement() { + string_refinementt::infot info; + info.ns=&ns; auto prop=util_make_unique(); prop->set_message_handler(get_message_handler()); - - auto string_refinement=util_make_unique( - ns, *prop, MAX_NB_REFINEMENT); - string_refinement->set_ui(ui); - - string_refinement->do_concretizing=options.get_bool_option("trace"); + info.prop=prop.get(); + info.refinement_bound=MAX_NB_REFINEMENT; + info.ui=ui; if(options.get_bool_option("string-max-length")) - string_refinement->set_max_string_length( - options.get_signed_int_option("string-max-length")); - if(options.get_bool_option("string-non-empty")) - string_refinement->enforce_non_empty_string(); - if(options.get_bool_option("string-printable")) - string_refinement->enforce_printable_characters(); - - if(options.get_option("max-node-refinement")!="") - string_refinement->max_node_refinement= + info.string_max_length=options.get_signed_int_option("string-max-length"); + info.string_non_empty=options.get_bool_option("string-non-empty"); + info.trace=options.get_bool_option("trace"); + info.string_printable=options.get_bool_option("string-printable"); + if(options.get_bool_option("max-node-refinement")) + info.max_node_refinement= options.get_unsigned_int_option("max-node-refinement"); - - string_refinement->do_array_refinement= - options.get_bool_option("refine-arrays"); - string_refinement->do_arithmetic_refinement= - options.get_bool_option("refine-arithmetic"); + info.refine_arrays=options.get_bool_option("refine-arrays"); + info.refine_arithmetic=options.get_bool_option("refine-arithmetic"); return util_make_unique( - std::move(string_refinement), std::move(prop)); + util_make_unique(info), std::move(prop)); } std::unique_ptr cbmc_solverst::get_smt1( diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index d1e72e227b3..6d4fb84db95 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -21,34 +21,44 @@ Author: Daniel Kroening, kroening@kroening.com class bv_refinementt:public bv_pointerst { public: - bv_refinementt(const namespacet &_ns, propt &_prop); - ~bv_refinementt(); + struct infot + { + const namespacet *ns=nullptr; + propt *prop=nullptr; + language_uit::uit ui=language_uit::uit::PLAIN; + /// Max number of times we refine a formula node + unsigned max_node_refinement=5; + /// Enable array refinement + bool refine_arrays=true; + /// Enable arithmetic refinement + bool refine_arithmetic=true; + }; - virtual decision_proceduret::resultt dec_solve(); + explicit bv_refinementt(const infot &info); - virtual std::string decision_procedure_text() const + decision_proceduret::resultt dec_solve() override; + + std::string decision_procedure_text() const override { return "refinement loop with "+prop.solver_text(); } - // NOLINTNEXTLINE(readability/identifiers) - typedef bv_pointerst SUB; - - // maximal number of times we refine a formula node - unsigned max_node_refinement; - // enable/disable refinements - bool do_array_refinement; - bool do_arithmetic_refinement; +protected: - using bv_pointerst::is_in_conflict; + // Refine array + void post_process_arrays() override; - void set_ui(language_uit::uit _ui) { ui=_ui; } + // Refine arithmetic + bvt convert_mult(const exprt &expr) override; + bvt convert_div(const div_exprt &expr) override; + bvt convert_mod(const mod_exprt &expr) override; + bvt convert_floatbv_op(const exprt &expr) override; -protected: - resultt prop_solve(); + void set_assumptions(const bvt &_assumptions) override; +private: // the list of operator approximations - struct approximationt + struct approximationt final { public: explicit approximationt(std::size_t _id_nr): @@ -79,39 +89,30 @@ class bv_refinementt:public bv_pointerst std::size_t id_nr; }; - typedef std::list approximationst; - approximationst approximations; - + resultt prop_solve(); approximationt &add_approximation(const exprt &expr, bvt &bv); + bool conflicts_with(approximationt &approximation); void check_SAT(approximationt &approximation); void check_UNSAT(approximationt &approximation); void initialize(approximationt &approximation); void get_values(approximationt &approximation); - bool is_in_conflict(approximationt &approximation); - - virtual void check_SAT(); - virtual void check_UNSAT(); - bool progress; - - // we refine the theory of arrays - virtual void post_process_arrays(); + void check_SAT(); + void check_UNSAT(); void arrays_overapproximated(); void freeze_lazy_constraints(); - // we refine expensive arithmetic - virtual bvt convert_mult(const exprt &expr); - virtual bvt convert_div(const div_exprt &expr); - virtual bvt convert_mod(const mod_exprt &expr); - virtual bvt convert_floatbv_op(const exprt &expr); - - // for collecting statistics - virtual void set_to(const exprt &expr, bool value); - - // overloading - virtual void set_assumptions(const bvt &_assumptions); + // MEMBERS + // Maximum number of times we refine a formula node + const unsigned max_node_refinement; + // Refinement toggles + const bool do_array_refinement; + const bool do_arithmetic_refinement; + bool progress; + std::vector approximations; bvt parent_assumptions; +protected: // use gui format language_uit::uit ui; }; diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index d471326ca0d..e3ac990b3a4 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -12,14 +12,13 @@ Author: Daniel Kroening, kroening@kroening.com #include -bv_refinementt::bv_refinementt( - const namespacet &_ns, propt &_prop): - bv_pointerst(_ns, _prop), - max_node_refinement(5), - do_array_refinement(true), - do_arithmetic_refinement(true), +bv_refinementt::bv_refinementt(const infot &info): + bv_pointerst(*info.ns, *info.prop), + max_node_refinement(info.max_node_refinement), + do_array_refinement(info.refine_arrays), + do_arithmetic_refinement(info.refine_arithmetic), progress(false), - ui(ui_message_handlert::uit::PLAIN) + ui(info.ui) { // check features we need PRECONDITION(prop.has_set_assumptions()); @@ -27,10 +26,6 @@ bv_refinementt::bv_refinementt( PRECONDITION(prop.has_is_in_conflict()); } -bv_refinementt::~bv_refinementt() -{ -} - decision_proceduret::resultt bv_refinementt::dec_solve() { // do the usual post-processing @@ -96,17 +91,16 @@ decision_proceduret::resultt bv_refinementt::prop_solve() // this puts the underapproximations into effect bvt assumptions=parent_assumptions; - for(approximationst::const_iterator - a_it=approximations.begin(); - a_it!=approximations.end(); - a_it++) + for(const approximationt &approximation : approximations) { assumptions.insert( assumptions.end(), - a_it->over_assumptions.begin(), a_it->over_assumptions.end()); + approximation.over_assumptions.begin(), + approximation.over_assumptions.end()); assumptions.insert( assumptions.end(), - a_it->under_assumptions.begin(), a_it->under_assumptions.end()); + approximation.under_assumptions.begin(), + approximation.under_assumptions.end()); } prop.set_assumptions(assumptions); @@ -127,40 +121,16 @@ void bv_refinementt::check_SAT() arrays_overapproximated(); - for(approximationst::iterator - a_it=approximations.begin(); - a_it!=approximations.end(); - a_it++) - check_SAT(*a_it); + for(approximationt &approximation : this->approximations) + check_SAT(approximation); } void bv_refinementt::check_UNSAT() { progress=false; - for(approximationst::iterator - a_it=approximations.begin(); - a_it!=approximations.end(); - a_it++) - check_UNSAT(*a_it); -} - -void bv_refinementt::set_to(const exprt &expr, bool value) -{ - #if 0 - unsigned prev=prop.no_variables(); - SUB::set_to(expr, value); - unsigned n=prop.no_variables()-prev; - std::cout << n << " EEE " << expr.id() << "@" << expr.type().id(); - forall_operands(it, expr) - std::cout << " " << it->id() << "@" << it->type().id(); - if(expr.id()=="=" && expr.operands().size()==2) - forall_operands(it, expr.op1()) - std::cout << " " << it->id() << "@" << it->type().id(); - std::cout << '\n'; - #else - SUB::set_to(expr, value); - #endif + for(approximationt &approximation : this->approximations) + check_UNSAT(approximation); } void bv_refinementt::set_assumptions(const bvt &_assumptions) diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp index 45a065a64ee..2a6627a34e3 100644 --- a/src/solvers/refinement/refine_arithmetic.cpp +++ b/src/solvers/refinement/refine_arithmetic.cpp @@ -373,7 +373,7 @@ void bv_refinementt::check_SAT(approximationt &a) void bv_refinementt::check_UNSAT(approximationt &a) { // part of the conflict? - if(!is_in_conflict(a)) + if(!this->conflicts_with(a)) return; status() << "Found assumption for `" << a.as_string() @@ -458,7 +458,7 @@ void bv_refinementt::check_UNSAT(approximationt &a) } /// check if an under-approximation is part of the conflict -bool bv_refinementt::is_in_conflict(approximationt &a) +bool bv_refinementt::conflicts_with(approximationt &a) { for(std::size_t i=0; i #include #include +#include #include -class string_constraint_generatort: messaget +class string_constraint_generatort final { public: // This module keeps a list of axioms. It has methods which generate // string constraints for different string functions and add them // to the axiom list. - string_constraint_generatort(namespacet _ns): - max_string_length(std::numeric_limits::max()), - force_printable_characters(false), - ns(_ns) - { } + // Used by format function + class format_specifiert; - // Constraints on the maximal length of strings - size_t max_string_length; + /// Arguments pack for the string_constraint_generator constructor + struct infot + { + const namespacet *ns=nullptr; + /// Max length of non-deterministic strings + size_t string_max_length=std::numeric_limits::max(); + /// Prefer printable characters in non-deterministic strings + bool string_printable=false; + }; - // Should we add constraints on the characters - bool force_printable_characters; + explicit string_constraint_generatort(const infot& info); - // Axioms are of three kinds: universally quantified string constraint, - // not contains string constraints and simple formulas. - std::list axioms; + /// Axioms are of three kinds: universally quantified string constraint, + /// not contains string constraints and simple formulas. + const std::vector &get_axioms() const; - // Boolean symbols for the results of some string functions - std::list boolean_symbols; + /// Boolean symbols for the results of some string functions + const std::vector &get_boolean_symbols() const; - // Symbols used in existential quantifications - std::list index_symbols; + /// Symbols used in existential quantifications + const std::vector &get_index_symbols() const; - // Used to store information about witnesses for not_contains constraints - std::map witness; + /// Set of strings that have been created by the generator + const std::set &get_created_strings() const; exprt get_witness_of( const string_not_contains_constraintt &c, @@ -65,51 +69,30 @@ class string_constraint_generatort: messaget return index_exprt(witness.at(c), univ_val); } - static unsigned next_symbol_id; - - static symbol_exprt fresh_symbol( + symbol_exprt fresh_symbol( const irep_idt &prefix, const typet &type=bool_typet()); - symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type); symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type); + + /// Maps unresolved symbols to the string_exprt that was created for them + string_exprt add_axioms_for_refined_string(const exprt &expr); + + exprt add_axioms_for_function_application( + const function_application_exprt &expr); + + symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type); + +private: symbol_exprt fresh_boolean(const irep_idt &prefix); string_exprt fresh_string(const refined_string_typet &type); string_exprt get_string_expr(const exprt &expr); plus_exprt plus_exprt_with_overflow_check(const exprt &op1, const exprt &op2); - // Maps unresolved symbols to the string_exprt that was created for them - std::map unresolved_symbols; - - // Set of strings that have been created by the generator - std::set created_strings; - string_exprt find_or_add_string_of_symbol( const symbol_exprt &sym, const refined_string_typet &ref_type); - string_exprt add_axioms_for_refined_string(const exprt &expr); - - exprt add_axioms_for_function_application( - const function_application_exprt &expr); - static constant_exprt constant_char(int i, const typet &char_type); - - // Used by format function - class format_specifiert; - -private: - // The integer with the longest string is Integer.MIN_VALUE which is -2^31, - // that is -2147483648 so takes 11 characters to write. - // The long with the longest string is Long.MIN_VALUE which is -2^63, - // approximately -9.223372037*10^18 so takes 20 characters to write. - const std::size_t MAX_INTEGER_LENGTH=11; - const std::size_t MAX_LONG_LENGTH=20; - const std::size_t MAX_FLOAT_LENGTH=15; - const std::size_t MAX_DOUBLE_LENGTH=30; - - std::map function_application_cache; - namespacet ns; - static irep_idt extract_java_string(const symbol_exprt &s); void add_default_axioms(const string_exprt &s); @@ -132,9 +115,6 @@ class string_constraint_generatort: messaget // The specification is partial: the actual value is not actually computed // but we ensure that hash codes of equal strings are equal. exprt add_axioms_for_hash_code(const function_application_exprt &f); - // To each string on which hash_code was called we associate a symbol - // representing the return value of the hash_code function. - std::map hash_code_of_string; exprt add_axioms_for_is_empty(const function_application_exprt &f); exprt add_axioms_for_is_prefix( @@ -331,12 +311,6 @@ class string_constraint_generatort: messaget // string pointers symbol_exprt add_axioms_for_intern(const function_application_exprt &f); - // Pool used for the intern method - std::map intern_of_string; - - // Tells which language is used. C and Java are supported - irep_idt mode; - // assert that the number of argument is equal to nb and extract them static const function_application_exprt::argumentst &args( const function_application_exprt &expr, size_t nb) @@ -346,16 +320,47 @@ class string_constraint_generatort: messaget return args; } -private: // Helper functions - exprt int_of_hex_char(const exprt &chr) const; - exprt is_high_surrogate(const exprt &chr) const; - exprt is_low_surrogate(const exprt &chr) const; - exprt character_equals_ignore_case( + static exprt int_of_hex_char(const exprt &chr); + static exprt is_high_surrogate(const exprt &chr); + static exprt is_low_surrogate(const exprt &chr); + static exprt character_equals_ignore_case( exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z); - bool is_constant_string(const string_exprt &expr) const; - string_exprt empty_string(const refined_string_typet &ref_type); + static bool is_constant_string(const string_exprt &expr); + static string_exprt empty_string(const refined_string_typet &ref_type); unsigned long to_integer_or_default(const exprt &expr, unsigned long def); + + // MEMBERS +public: + const size_t max_string_length; + // Used to store information about witnesses for not_contains constraints + std::map witness; +private: + // The integer with the longest string is Integer.MIN_VALUE which is -2^31, + // that is -2147483648 so takes 11 characters to write. + // The long with the longest string is Long.MIN_VALUE which is -2^63, + // approximately -9.223372037*10^18 so takes 20 characters to write. + CBMC_CONSTEXPR static const std::size_t MAX_INTEGER_LENGTH=11; + CBMC_CONSTEXPR static const std::size_t MAX_LONG_LENGTH=20; + CBMC_CONSTEXPR static const std::size_t MAX_FLOAT_LENGTH=15; + CBMC_CONSTEXPR static const std::size_t MAX_DOUBLE_LENGTH=30; + std::set m_created_strings; + unsigned m_symbol_count=0; + const messaget m_message; + const bool m_force_printable_characters; + + std::vector m_axioms; + std::map m_unresolved_symbols; + std::vector m_boolean_symbols; + std::vector m_index_symbols; + std::map m_function_application_cache; + const namespacet m_ns; + // To each string on which hash_code was called we associate a symbol + // representing the return value of the hash_code function. + std::map m_hash_code_of_string; + + // Pool used for the intern method + std::map m_intern_of_string; }; exprt is_digit_with_radix( @@ -363,13 +368,16 @@ exprt is_digit_with_radix( const bool strict_formatting, const exprt &radix_as_char, const unsigned long radix_ul); + exprt get_numeric_value_from_character( const exprt &chr, const typet &char_type, const typet &type, const bool strict_formatting, unsigned long radix_ul); + size_t max_printed_string_length(const typet &type, unsigned long ul_radix); + std::string utf16_constant_array_to_java( const array_exprt &arr, unsigned length); diff --git a/src/solvers/refinement/string_constraint_generator_code_points.cpp b/src/solvers/refinement/string_constraint_generator_code_points.cpp index d539e8d9e9e..55b914d1aa7 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)); - axioms.push_back(a1); + m_axioms.push_back(a1); implies_exprt a2(not_exprt(small), res.axiom_for_has_length(2)); - axioms.push_back(a2); + m_axioms.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)); - axioms.push_back(a3); + m_axioms.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()))); - axioms.push_back(a4); + m_axioms.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()))); - axioms.push_back(a5); + m_axioms.push_back(a5); return res; } @@ -79,7 +79,7 @@ string_exprt string_constraint_generatort::add_axioms_for_code_point( /// 0xD800..0xDBFF /// \par parameters: a character expression /// \return a Boolean expression -exprt string_constraint_generatort::is_high_surrogate(const exprt &chr) const +exprt string_constraint_generatort::is_high_surrogate(const exprt &chr) { return and_exprt( binary_relation_exprt(chr, ID_ge, constant_char(0xD800, chr.type())), @@ -92,7 +92,7 @@ exprt string_constraint_generatort::is_high_surrogate(const exprt &chr) const /// 0xDC00..0xDFFF /// \par parameters: a character expression /// \return a Boolean expression -exprt string_constraint_generatort::is_low_surrogate(const exprt &chr) const +exprt string_constraint_generatort::is_low_surrogate(const exprt &chr) { return and_exprt( binary_relation_exprt(chr, ID_ge, constant_char(0xDC00, chr.type())), @@ -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); - axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair))); - axioms.push_back( + m_axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair))); + m_axioms.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)); - axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair))); - axioms.push_back( + m_axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair))); + m_axioms.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())); - axioms.push_back(binary_relation_exprt(result, ID_le, length)); - axioms.push_back(binary_relation_exprt(result, ID_ge, minimum)); + m_axioms.push_back(binary_relation_exprt(result, ID_le, length)); + m_axioms.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)); - axioms.push_back(binary_relation_exprt(result, ID_le, maximum)); - axioms.push_back(binary_relation_exprt(result, ID_ge, minimum)); + m_axioms.push_back(binary_relation_exprt(result, ID_le, maximum)); + m_axioms.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 aa14d4192e8..7bc276cd24a 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)); - axioms.push_back(a1); + m_axioms.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); - axioms.push_back(a2); + m_axioms.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))); - axioms.push_back(a3); + m_axioms.push_back(a3); return tc_eq; } @@ -155,7 +155,7 @@ exprt string_constraint_generatort::add_axioms_for_hash_code( typet return_type=f.type(); typet index_type=str.length().type(); - auto pair=hash_code_of_string.insert( + auto pair=m_hash_code_of_string.insert( std::make_pair(str, fresh_symbol("hash", return_type))); exprt hash=pair.first->second; @@ -165,7 +165,7 @@ exprt string_constraint_generatort::add_axioms_for_hash_code( // c3: (|str|==|s| && exists i<|s|. s[i]!=str[i]) // WARNING: the specification may be incomplete - for(auto it : hash_code_of_string) + for(auto it : m_hash_code_of_string) { symbol_exprt i=fresh_exist_index("index_hash", index_type); equal_exprt c1(it.second, hash); @@ -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)))); - axioms.push_back(or_exprt(c1, or_exprt(c2, c3))); + m_axioms.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)); - axioms.push_back(a1); + m_axioms.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])); - axioms.push_back(a2); + m_axioms.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))); - axioms.push_back(a3); + m_axioms.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])); - axioms.push_back(a4); + m_axioms.push_back(a4); return res; } @@ -265,7 +265,7 @@ symbol_exprt string_constraint_generatort::add_axioms_for_intern( typet index_type=str.length().type(); - auto pair=intern_of_string.insert( + auto pair=m_intern_of_string.insert( std::make_pair(str, fresh_symbol("pool", return_type))); symbol_exprt intern=pair.first->second; @@ -275,19 +275,19 @@ symbol_exprt string_constraint_generatort::add_axioms_for_intern( // || (|str|==|s| &&exists i<|s|. s[i]!=str[i]) exprt disj=false_exprt(); - for(auto it : intern_of_string) + for(auto it : m_intern_of_string) disj=or_exprt( disj, equal_exprt(intern, it.second)); - axioms.push_back(disj); + m_axioms.push_back(disj); // WARNING: the specification may be incomplete or incorrect - for(auto it : intern_of_string) + for(auto it : m_intern_of_string) if(it.second!=str) { symbol_exprt i=fresh_exist_index("index_intern", index_type); - axioms.push_back( + m_axioms.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 40a59265c89..3f4f607addd 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)); - axioms.push_back(a1); + m_axioms.push_back(a1); implies_exprt a2(not_exprt(prem), equal_exprt(res.length(), s1.length())); - axioms.push_back(a2); + m_axioms.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])); - axioms.push_back(a3); + m_axioms.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); - axioms.push_back(a4); + m_axioms.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 13fea55161c..d701d27a583 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); - axioms.push_back(lemma); + m_axioms.push_back(lemma); } exprt s_length=from_integer(str.size(), ref_type.get_index_type()); - axioms.push_back(res.axiom_for_has_length(s_length)); + m_axioms.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 d164ad54264..da085756115 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)); - axioms.push_back(a1); + m_axioms.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); - axioms.push_back(a2); + m_axioms.push_back(a2); equal_exprt a3(int_expr, sum); - axioms.push_back(a3); + m_axioms.push_back(a3); return res; } diff --git a/src/solvers/refinement/string_constraint_generator_format.cpp b/src/solvers/refinement/string_constraint_generator_format.cpp index 7ad34d7d2ec..ae672e6a01c 100644 --- a/src/solvers/refinement/string_constraint_generator_format.cpp +++ b/src/solvers/refinement/string_constraint_generator_format.cpp @@ -313,10 +313,12 @@ string_exprt string_constraint_generatort::add_axioms_for_format_specifier( case format_specifiert::DATE_TIME: // TODO: DateTime not implemented // For all these unimplemented cases we return a non-deterministic string - warning() << "unimplemented format specifier: " << fs.conversion << eom; + m_message.warning() << "unimplemented format specifier: " << fs.conversion + << m_message.eom; return fresh_string(ref_type); default: - error() << "invalid format specifier: " << fs.conversion << eom; + m_message.error() << "invalid format specifier: " << fs.conversion + << m_message.eom; INVARIANT( false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]"); throw 0; @@ -432,8 +434,9 @@ string_exprt string_constraint_generatort::add_axioms_for_format( } else { - warning() << "ignoring format function with non constant first argument" - << eom; + m_message.warning() + << "ignoring format function with non constant first argument" + << m_message.eom; return fresh_string(ref_type); } } diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index 1dc54698bce..977b9832dbf 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())); - axioms.push_back(a1); + m_axioms.push_back(a1); equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1)); - axioms.push_back(a2); + m_axioms.push_back(a2); implies_exprt a3( contains, and_exprt( binary_relation_exprt(from_index, ID_le, index), equal_exprt(str[index], c))); - axioms.push_back(a3); + m_axioms.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))); - axioms.push_back(a4); + m_axioms.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))); - axioms.push_back(a5); + m_axioms.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())))); - axioms.push_back(a1); + m_axioms.push_back(a1); equal_exprt a2( not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type))); - axioms.push_back(a2); + m_axioms.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])); - axioms.push_back(a3); + m_axioms.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); - axioms.push_back(a4); + m_axioms.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); - axioms.push_back(a5); + m_axioms.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))); - axioms.push_back(a1); + m_axioms.push_back(a1); equal_exprt a2( not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type))); - axioms.push_back(a2); + m_axioms.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); - axioms.push_back(a3); + m_axioms.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); - axioms.push_back(a4); + m_axioms.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); - axioms.push_back(a5); + m_axioms.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)); - axioms.push_back(a1); + m_axioms.push_back(a1); equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1)); - axioms.push_back(a2); + m_axioms.push_back(a2); implies_exprt a3( contains, and_exprt( binary_relation_exprt(from_index, ID_ge, index), equal_exprt(str[index], c))); - axioms.push_back(a3); + m_axioms.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))); - axioms.push_back(a4); + m_axioms.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))); - axioms.push_back(a5); + m_axioms.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 71de1f136a2..f149ef3ecf1 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -19,6 +19,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include +#include #include #include #include @@ -26,7 +27,34 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include -unsigned string_constraint_generatort::next_symbol_id=1; +string_constraint_generatort::string_constraint_generatort( + const string_constraint_generatort::infot& info): + max_string_length(info.string_max_length), + m_force_printable_characters(info.string_printable), + m_ns(*info.ns) { } + +const std::vector &string_constraint_generatort::get_axioms() const +{ + return m_axioms; +} + +const std::vector & +string_constraint_generatort::get_index_symbols() const +{ + return m_index_symbols; +} + +const std::vector & +string_constraint_generatort::get_boolean_symbols() const +{ + return m_boolean_symbols; +} + +const std::set & +string_constraint_generatort::get_created_strings() const +{ + return m_created_strings; +} /// generate constant character expression with character type. /// \par parameters: integer representing a character, and a type for @@ -48,7 +76,7 @@ symbol_exprt string_constraint_generatort::fresh_symbol( const irep_idt &prefix, const typet &type) { std::ostringstream buf; - buf << "string_refinement#" << prefix << "#" << (next_symbol_id++); + buf << "string_refinement#" << prefix << "#" << ++m_symbol_count; irep_idt name(buf.str()); return symbol_exprt(name, type); } @@ -69,7 +97,7 @@ symbol_exprt string_constraint_generatort::fresh_exist_index( const irep_idt &prefix, const typet &type) { symbol_exprt s=fresh_symbol(prefix, type); - index_symbols.push_back(s); + m_index_symbols.push_back(s); return s; } @@ -80,7 +108,7 @@ symbol_exprt string_constraint_generatort::fresh_boolean( const irep_idt &prefix) { symbol_exprt b=fresh_symbol(prefix, bool_typet()); - boolean_symbols.push_back(b); + m_boolean_symbols.push_back(b); return b; } @@ -106,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)); - axioms.push_back(no_overflow); + m_axioms.push_back(no_overflow); return sum; } @@ -120,7 +148,7 @@ string_exprt string_constraint_generatort::fresh_string( symbol_exprt length=fresh_symbol("string_length", type.get_index_type()); symbol_exprt content=fresh_symbol("string_content", type.get_content_type()); string_exprt str(length, content, type); - created_strings.insert(str); + m_created_strings.insert(str); add_default_axioms(str); return str; } @@ -155,12 +183,12 @@ string_exprt string_constraint_generatort::get_string_expr(const exprt &expr) void string_constraint_generatort::add_default_axioms( const string_exprt &s) { - axioms.push_back( + m_axioms.push_back( s.axiom_for_length_ge(from_integer(0, s.length().type()))); if(max_string_length!=std::numeric_limits::max()) - axioms.push_back(s.axiom_for_length_le(max_string_length)); + m_axioms.push_back(s.axiom_for_length_le(max_string_length)); - if(force_printable_characters) + if(m_force_printable_characters) { symbol_exprt qvar=fresh_univ_index("printable", s.length().type()); exprt chr=s[qvar]; @@ -168,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); - axioms.push_back(sc); + m_axioms.push_back(sc); } } @@ -254,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); - axioms.push_back( + m_axioms.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)); - axioms.push_back(sc1); - axioms.push_back( + m_axioms.push_back(sc1); + m_axioms.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)); - axioms.push_back(sc2); + m_axioms.push_back(sc2); return res; } @@ -280,7 +308,7 @@ string_exprt string_constraint_generatort::find_or_add_string_of_symbol( { irep_idt id=sym.get_identifier(); string_exprt str=fresh_string(ref_type); - auto entry=unresolved_symbols.insert(std::make_pair(id, str)); + auto entry=m_unresolved_symbols.insert(std::make_pair(id, str)); return entry.first->second; } @@ -309,7 +337,7 @@ exprt string_constraint_generatort::add_axioms_for_function_application( new_expr.function()=symbol_exprt(str_id.substr(0, pos+4)); new_expr.type()=refined_string_typet(java_int_type(), java_char_type()); - auto res_it=function_application_cache.insert(std::make_pair(new_expr, + auto res_it=m_function_application_cache.insert(std::make_pair(new_expr, nil_exprt())); if(res_it.second) { @@ -329,7 +357,7 @@ exprt string_constraint_generatort::add_axioms_for_function_application( new_expr.function()=symbol_exprt(str_id.substr(0, pos+4)); new_expr.type()=refined_string_typet(java_int_type(), java_char_type()); - auto res_it=function_application_cache.insert(std::make_pair(new_expr, + auto res_it=m_function_application_cache.insert(std::make_pair(new_expr, nil_exprt())); if(res_it.second) { @@ -345,8 +373,8 @@ exprt string_constraint_generatort::add_axioms_for_function_application( // TODO: improve efficiency of this test by either ordering test by frequency // or using a map - auto res_it=function_application_cache.find(expr); - if(res_it!=function_application_cache.end() && res_it->second!=nil_exprt()) + auto res_it=m_function_application_cache.find(expr); + if(res_it!=m_function_application_cache.end() && res_it->second!=nil_exprt()) return res_it->second; exprt res; @@ -476,7 +504,7 @@ exprt string_constraint_generatort::add_axioms_for_function_application( msg+=id2string(id); DATA_INVARIANT(false, string_refinement_invariantt(msg)); } - function_application_cache[expr]=res; + m_function_application_cache[expr]=res; return res; } @@ -587,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()); - axioms.push_back(equal_exprt(char_sym, str[args(f, 2)[1]])); + m_axioms.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 69ee6e40cbc..c11b8ef4263 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))); - axioms.push_back(a1); + m_axioms.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])); - axioms.push_back(a2); + m_axioms.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); - axioms.push_back(a3); + m_axioms.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]); - axioms.push_back(implies_exprt(is_empty, s0.axiom_for_has_length(0))); - axioms.push_back(implies_exprt(s0.axiom_for_has_length(0), is_empty)); + 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)); 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)); - axioms.push_back(a1); + m_axioms.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])); - axioms.push_back(a2); + m_axioms.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); - axioms.push_back(a3); + m_axioms.push_back(a3); return tc_issuffix; } @@ -163,7 +163,7 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix( /// \param expr: a string expression /// \return a Boolean bool string_constraint_generatort::is_constant_string( - const string_exprt &expr) const + const string_exprt &expr) { if(expr.id()!=ID_struct || expr.operands().size()!=2 || @@ -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)); - axioms.push_back(a1); + m_axioms.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); - axioms.push_back(a2); + m_axioms.push_back(a2); implies_exprt a3( not_exprt(contains), equal_exprt(startpos, from_integer(-1, index_type))); - axioms.push_back(a3); + m_axioms.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])); - axioms.push_back(a4); + m_axioms.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); - axioms.push_back(a5); + m_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 b2566bab396..5bbbba82c6c 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 - axioms.push_back(res.axiom_for_has_length(k)); + m_axioms.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])); - axioms.push_back(a2); + m_axioms.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()))); - axioms.push_back(a3); + m_axioms.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))); - axioms.push_back(a1); + m_axioms.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); - axioms.push_back(a2); + m_axioms.push_back(a2); // Warning: check what to do if the string is not long enough - axioms.push_back(str.axiom_for_length_ge(end)); + m_axioms.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)])); - axioms.push_back(a4); + m_axioms.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())); - axioms.push_back(a1); + m_axioms.push_back(a1); binary_relation_exprt a2(idx, ID_ge, from_integer(0, index_type)); - axioms.push_back(a2); + m_axioms.push_back(a2); exprt a3=str.axiom_for_length_ge(idx); - axioms.push_back(a3); + m_axioms.push_back(a3); exprt a4=res.axiom_for_length_ge( from_integer(0, index_type)); - axioms.push_back(a4); + m_axioms.push_back(a4); exprt a5=res.axiom_for_length_le(str); - axioms.push_back(a5); + m_axioms.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); - axioms.push_back(a6); + m_axioms.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); - axioms.push_back(a7); + m_axioms.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); - axioms.push_back(a8); + m_axioms.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)); - axioms.push_back(a9); + m_axioms.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); - axioms.push_back(a1); + m_axioms.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); - axioms.push_back(a2); + m_axioms.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); - axioms.push_back(a1); + m_axioms.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); - axioms.push_back(a2); + m_axioms.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); - axioms.push_back(a3); + m_axioms.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))); - axioms.push_back(a1); + m_axioms.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] - axioms.push_back(res.axiom_for_has_same_length_as(str)); + m_axioms.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)); - axioms.push_back(a2); + m_axioms.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 1c215db583b..f54a821f623 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())); - axioms.push_back(a1); + m_axioms.push_back(a1); for(std::size_t i=0; i1) - axioms.push_back( + m_axioms.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)); - axioms.push_back(lemma); + m_axioms.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)); - axioms.push_back(non_empty); + m_axioms.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); - axioms.push_back(correct_first); + m_axioms.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); - axioms.push_back(correct_first); + m_axioms.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))); - axioms.push_back(contains_digit); + m_axioms.push_back(contains_digit); // |str| <= max_size - axioms.push_back(str.axiom_for_length_le(max_size)); + m_axioms.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)); - axioms.push_back(character_at_index_is_digit); + m_axioms.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))); - axioms.push_back(no_leading_zero); + m_axioms.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))); - axioms.push_back(no_leading_zero_after_minus); + m_axioms.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 "-". - axioms.push_back( + m_axioms.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)); - axioms.push_back(a5); + m_axioms.push_back(a5); } const implies_exprt a6( and_exprt(premise, not_exprt(starts_with_minus)), equal_exprt(input_int, sum)); - axioms.push_back(a6); + m_axioms.push_back(a6); const implies_exprt a7( and_exprt(premise, starts_with_minus), equal_exprt(input_int, unary_minus_exprt(sum))); - axioms.push_back(a7); + m_axioms.push_back(a7); } } @@ -530,7 +530,7 @@ unsigned long string_constraint_generatort::to_integer_or_default( const exprt &expr, unsigned long def) { mp_integer mp_radix; - bool to_integer_failed=to_integer(simplify_expr(expr, ns), mp_radix); + bool to_integer_failed=to_integer(simplify_expr(expr, m_ns), mp_radix); return to_integer_failed?def:integer2ulong(mp_radix); } diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 04fb0fbdc3f..608b70212aa 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -34,42 +34,47 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #include -string_refinementt::string_refinementt( - const namespacet &_ns, - propt &_prop, - unsigned refinement_bound): - supert(_ns, _prop), - use_counter_example(false), - do_concretizing(false), - initial_loop_bound(refinement_bound), - generator(_ns), - non_empty_string(false) -{ } - -/// Add constraints on the size of strings used in the program. -/// \param i: maximum length which is allowed for strings. -/// by default the strings length has no other limit -/// than the maximal integer according to the type of their -/// length, for instance 2^31-1 for Java. -void string_refinementt::set_max_string_length(size_t i) +static bool validate(const string_refinementt::infot &info) { - generator.max_string_length=i; + PRECONDITION(info.ns); + PRECONDITION(info.prop); + return true; } -/// Add constraints on the size of nondet character arrays to ensure they have -/// length at least 1 -void string_refinementt::enforce_non_empty_string() +static bv_refinementt::infot bv_refinement_info( + const string_refinementt::infot &in) { - non_empty_string=true; + bv_refinementt::infot out; + out.ns=in.ns; + out.prop=in.prop; + out.ui=in.ui; + out.max_node_refinement=in.max_node_refinement; + out.refine_arrays=in.refine_arrays; + out.refine_arithmetic=in.refine_arithmetic; + return out; } -/// Add constraints on characters used in the program to ensure they are -/// printable -void string_refinementt::enforce_printable_characters() +static string_constraint_generatort::infot +generator_info(const string_refinementt::infot &in) { - generator.force_printable_characters=true; + string_constraint_generatort::infot out; + out.ns=in.ns; + out.string_max_length=in.string_max_length; + out.string_printable=in.string_printable; + return out; } +string_refinementt::string_refinementt(const infot &info, bool): + supert(bv_refinement_info(info)), + use_counter_example(false), + do_concretizing(info.trace), + initial_loop_bound(info.refinement_bound), + generator(generator_info(info)), + non_empty_string(info.string_non_empty) { } + +string_refinementt::string_refinementt(const infot &info): + string_refinementt(info, validate(info)) { } + /// display the current index set, for debugging void string_refinementt::display_index_set() { @@ -373,7 +378,7 @@ void string_refinementt::concretize_results() { for(const auto &it : symbol_resolve) concretize_string(it.second); - for(const auto &it : generator.created_strings) + for(const auto &it : generator.get_created_strings()) concretize_string(it); add_instantiations(); } @@ -393,7 +398,7 @@ void string_refinementt::concretize_lengths() found_length[content]=length; } } - for(const auto &it : generator.created_strings) + for(const auto &it : generator.get_created_strings()) { if(is_refined_string_type(it.type())) { @@ -496,7 +501,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() supert::set_to(pair.first, pair.second); } - for(exprt &axiom : generator.axioms) + for(exprt axiom : generator.get_axioms()) { replace_expr(symbol_resolve, axiom); if(axiom.id()==ID_string_constraint) @@ -818,13 +823,13 @@ void string_refinementt::debug_model() } } - for(auto it : generator.boolean_symbols) + for(const auto it : generator.get_boolean_symbols()) { debug() << " - " << it.get_identifier() << ": " << from_expr(ns, "", supert::get(it)) << eom; } - for(auto it : generator.index_symbols) + for(const auto it : generator.get_index_symbols()) { debug() << " - " << it.get_identifier() << ": " << from_expr(ns, "", supert::get(it)) << eom; @@ -1752,8 +1757,14 @@ bool string_refinementt::is_axiom_sat( const exprt &axiom, const symbol_exprt& var, exprt &witness) { satcheck_no_simplifiert sat_check; - supert solver(ns, sat_check); - solver.set_ui(ui); + supert::infot info; + info.ns=&ns; + info.prop=&sat_check; + info.refine_arithmetic=true; + info.refine_arrays=true; + info.max_node_refinement=5; + info.ui=ui; + supert solver(info); solver << axiom; switch(solver()) diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 0eec3e99a9a..021176d4178 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -20,6 +20,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H +#include #include #include #include @@ -28,52 +29,59 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #define MAX_NB_REFINEMENT 100 -class string_refinementt: public bv_refinementt +class string_refinementt final: public bv_refinementt { public: - string_refinementt( - const namespacet &_ns, - propt &_prop, - unsigned refinement_bound); - - void set_mode(); - - // Should we use counter examples at each iteration? - bool use_counter_example; - - // Should we concretize strings when the solver finished - bool do_concretizing; + /// string_refinementt constructor arguments + struct infot + { + const namespacet *ns=nullptr; + propt *prop=nullptr; + language_uit::uit ui=language_uit::uit::PLAIN; + unsigned refinement_bound=0; + size_t string_max_length=std::numeric_limits::max(); + /// Make non-deterministic character arrays have at least one character + bool string_non_empty=false; + /// Concretize strings after solver is finished + bool trace=false; + /// Make non-deterministic characters printable + bool string_printable=false; + unsigned max_node_refinement=5; + bool refine_arrays=false; + bool refine_arithmetic=false; + bool use_counter_example=false; + }; + + explicit string_refinementt(const infot &); - void set_max_string_length(size_t i); - void enforce_non_empty_string(); - void enforce_printable_characters(); virtual std::string decision_procedure_text() const override { return "string refinement loop with "+prop.solver_text(); } - static exprt is_positive(const exprt &x); - exprt get(const exprt &expr) const override; protected: - typedef std::set expr_sett; - typedef std::list exprt_listt; - decision_proceduret::resultt dec_solve() override; - bvt convert_bool_bv(const exprt &boole, const exprt &orig); - private: + const bool use_counter_example; + const bool do_concretizing; // Base class typedef bv_refinementt supert; + typedef std::set expr_sett; + typedef std::list exprt_listt; + + string_refinementt(const infot &, bool); + bvt convert_bool_bv(const exprt &boole, const exprt &orig); + unsigned initial_loop_bound; string_constraint_generatort generator; - bool non_empty_string; + const bool non_empty_string; expr_sett nondet_arrays; // Simple constraints that have been given to the solver diff --git a/src/util/constexpr.def b/src/util/constexpr.def new file mode 100644 index 00000000000..fa4f20fa0f4 --- /dev/null +++ b/src/util/constexpr.def @@ -0,0 +1,6 @@ +#if defined(__GNUC__) || defined(__clang__) +#define CBMC_CONSTEXPR constexpr +#else +#define CBMC_CONSTEXPR +#endif + diff --git a/unit/solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp b/unit/solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp index 3f84064470f..82a636a9052 100644 --- a/unit/solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp +++ b/unit/solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp @@ -109,7 +109,8 @@ SCENARIO("calculate_max_string_length", "[core][solvers][refinement][string_constraint_generator_valueof]") { const unsigned long radixes[]={2, 8, 10, 16}; - const typet int_types[]={ + const typet int_types[]= + { signedbv_typet(32), unsignedbv_typet(32), signedbv_typet(64), diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp index b82fd7f0fa3..48cf3ed8e27 100644 --- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -119,7 +119,12 @@ std::string create_info(std::vector &lemmas, const namespacet &ns) decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns) { satcheck_no_simplifiert sat_check; - bv_refinementt solver(ns, sat_check); + bv_refinementt::infot info; + info.ns=&ns; + info.prop=&sat_check; + const auto ui=language_uit::uit::PLAIN; + info.ui=ui; + bv_refinementt solver(info); solver << expr; return solver(); } @@ -148,11 +153,13 @@ SCENARIO("instantiate_not_contains", // Generating the corresponding axioms and simplifying, recording info symbol_tablet symtab; namespacet empty_ns(symtab); - string_constraint_generatort generator(empty_ns); + string_constraint_generatort::infot info; + info.ns=&empty_ns; + string_constraint_generatort generator(info); exprt res=generator.add_axioms_for_function_application(func); std::string axioms; std::vector nc_axioms; - for(auto &axiom : generator.axioms) + for(exprt axiom : generator.get_axioms()) { simplify(axiom, ns); if(axiom.id()==ID_string_constraint) @@ -234,7 +241,9 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; namespacet empty_ns(symtab); - string_constraint_generatort generator(empty_ns); + string_constraint_generatort::infot info; + info.ns=&empty_ns; + string_constraint_generatort generator(info); generator.witness[vacuous]= generator.fresh_symbol("w", t.witness_type()); @@ -291,7 +300,9 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; namespacet ns(symtab); - string_constraint_generatort generator(ns); + string_constraint_generatort::infot info; + info.ns=&ns; + string_constraint_generatort generator(info); generator.witness[trivial]= generator.fresh_symbol("w", t.witness_type()); @@ -349,7 +360,9 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; namespacet empty_ns(symtab); - string_constraint_generatort generator(empty_ns); + string_constraint_generatort::infot info; + info.ns=&empty_ns; + string_constraint_generatort generator(info); generator.witness[trivial]= generator.fresh_symbol("w", t.witness_type()); @@ -408,7 +421,10 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; namespacet empty_ns(symtab); - string_constraint_generatort generator(empty_ns); + + string_constraint_generatort::infot info; + info.ns=&empty_ns; + string_constraint_generatort generator(info); generator.witness[trivial]= generator.fresh_symbol("w", t.witness_type()); @@ -466,7 +482,9 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; namespacet empty_ns(symtab); - string_constraint_generatort generator(empty_ns); + string_constraint_generatort::infot info; + info.ns=&empty_ns; + string_constraint_generatort generator(info); generator.witness[trivial]= generator.fresh_symbol("w", t.witness_type());