From 22b48852e0046c4bdde83089952824ad793886ca Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Fri, 25 Aug 2017 15:23:26 +0100 Subject: [PATCH 01/32] Remove usage of static in the header file --- src/solvers/refinement/string_constraint.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index 867284101e3..c553efb8c7e 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -144,7 +144,7 @@ extern inline string_constraintt &to_string_constraint(exprt &expr) /// \param [in] identifier: identifier for `from_expr` /// \param [in] expr: constraint to render /// \return rendered string -inline static std::string from_expr( +inline std::string from_expr( const namespacet &ns, const irep_idt &identifier, const string_constraintt &expr) @@ -218,7 +218,7 @@ class string_not_contains_constraintt: public exprt /// \param [in] identifier: identifier for `from_expr` /// \param [in] expr: constraint to render /// \return rendered string -inline static std::string from_expr( +inline std::string from_expr( const namespacet &ns, const irep_idt &identifier, const string_not_contains_constraintt &expr) From 848f2a53dac9f73004a4647a9a59b7c6ce2fa247 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Fri, 25 Aug 2017 15:35:15 +0100 Subject: [PATCH 02/32] Constraint gen cosmetics - final - constexpr constants - private variables - explicit constructor --- .../refinement/string_constraint_generator.h | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index b679924ee31..bf412c5fbc1 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -26,14 +26,14 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include -class string_constraint_generatort: messaget +class string_constraint_generatort final: messaget { 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): + explicit string_constraint_generatort(namespacet _ns): max_string_length(std::numeric_limits::max()), force_printable_characters(false), ns(_ns) @@ -91,21 +91,19 @@ class string_constraint_generatort: messaget 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: + static constant_exprt constant_char(int i, const typet &char_type); // 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; + constexpr static const std::size_t MAX_INTEGER_LENGTH=11; + constexpr static const std::size_t MAX_LONG_LENGTH=20; + constexpr static const std::size_t MAX_FLOAT_LENGTH=15; + constexpr static const std::size_t MAX_DOUBLE_LENGTH=30; std::map function_application_cache; namespacet ns; @@ -346,7 +344,6 @@ 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; @@ -363,13 +360,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); From 3217fe337899b439493cc746a97544279ce07a0b Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Fri, 25 Aug 2017 15:40:55 +0100 Subject: [PATCH 03/32] constraint_generator message is a member --- src/solvers/refinement/string_constraint_generator.h | 3 ++- .../refinement/string_constraint_generator_format.cpp | 10 ++++++---- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index bf412c5fbc1..109cfa2ee1d 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -26,7 +26,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include -class string_constraint_generatort final: messaget +class string_constraint_generatort final { public: // This module keeps a list of axioms. It has methods which generate @@ -95,6 +95,7 @@ class string_constraint_generatort final: messaget class format_specifiert; private: + messaget m_message; static constant_exprt constant_char(int i, const typet &char_type); // The integer with the longest string is Integer.MIN_VALUE which is -2^31, // that is -2147483648 so takes 11 characters to write. diff --git a/src/solvers/refinement/string_constraint_generator_format.cpp b/src/solvers/refinement/string_constraint_generator_format.cpp index 7ad34d7d2ec..fdfff031d9a 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,8 @@ 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); } } From c51e35e813573c0bcd239593b894eef9776128c0 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Fri, 25 Aug 2017 15:42:30 +0100 Subject: [PATCH 04/32] Use C++11 initialization for constraint generator members --- src/solvers/refinement/string_constraint_generator.h | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 109cfa2ee1d..45dbc89c343 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -33,17 +33,13 @@ class string_constraint_generatort final // string constraints for different string functions and add them // to the axiom list. - explicit string_constraint_generatort(namespacet _ns): - max_string_length(std::numeric_limits::max()), - force_printable_characters(false), - ns(_ns) - { } + explicit string_constraint_generatort(namespacet _ns): ns(_ns) { } // Constraints on the maximal length of strings - size_t max_string_length; + size_t max_string_length=std::numeric_limits::max(); // Should we add constraints on the characters - bool force_printable_characters; + bool force_printable_characters=false; // Axioms are of three kinds: universally quantified string constraint, // not contains string constraints and simple formulas. From cf950aba5ef8d54194fb506ae3170c1b120a4bab Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Fri, 25 Aug 2017 15:45:23 +0100 Subject: [PATCH 05/32] Use vector instead of list for constraint_generator data --- src/solvers/refinement/string_constraint_generator.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 45dbc89c343..32b899e5f59 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -43,13 +43,13 @@ class string_constraint_generatort final // Axioms are of three kinds: universally quantified string constraint, // not contains string constraints and simple formulas. - std::list axioms; + std::vector axioms; // Boolean symbols for the results of some string functions - std::list boolean_symbols; + std::vector boolean_symbols; // Symbols used in existential quantifications - std::list index_symbols; + std::vector index_symbols; // Used to store information about witnesses for not_contains constraints std::map witness; From 8043a0d8250eea4e8c42146266aa004b3105c86b Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Fri, 25 Aug 2017 16:03:49 +0100 Subject: [PATCH 06/32] Hide index_symbols and boolean_symbols in constraint generator --- src/solvers/refinement/string_constraint_generator.h | 8 +++++--- .../refinement/string_constraint_generator_main.cpp | 12 ++++++++++++ src/solvers/refinement/string_refinement.cpp | 4 ++-- 3 files changed, 19 insertions(+), 5 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 32b899e5f59..fa0755f4dbb 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -46,10 +46,10 @@ class string_constraint_generatort final std::vector axioms; // Boolean symbols for the results of some string functions - std::vector boolean_symbols; + const std::vector get_boolean_symbols() const; - // Symbols used in existential quantifications - std::vector 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; @@ -92,6 +92,8 @@ class string_constraint_generatort final private: messaget m_message; + std::vector boolean_symbols; + std::vector index_symbols; static constant_exprt constant_char(int i, const typet &char_type); // The integer with the longest string is Integer.MIN_VALUE which is -2^31, // that is -2147483648 so takes 11 characters to write. diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 71de1f136a2..3cfef714af8 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -28,6 +28,18 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com unsigned string_constraint_generatort::next_symbol_id=1; +const std::vector +&string_constraint_generatort::get_index_symbols() const +{ + return this->index_symbols; +} + +const std::vector +string_constraint_generatort::get_boolean_symbols() const +{ + return boolean_symbols; +} + /// generate constant character expression with character type. /// \par parameters: integer representing a character, and a type for /// characters; diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 04fb0fbdc3f..e1f02a2f7f1 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -818,13 +818,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; From 16a0a34644cd58c45938bdc24eccd0d477df576a Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Fri, 25 Aug 2017 16:04:10 +0100 Subject: [PATCH 07/32] constraint generator const namespace --- src/solvers/refinement/string_constraint_generator.h | 11 ++++++----- .../refinement/string_constraint_generator_main.cpp | 9 +++++++-- src/solvers/refinement/string_refinement.cpp | 2 +- .../instantiate_not_contains.cpp | 2 +- 4 files changed, 15 insertions(+), 9 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index fa0755f4dbb..6a396e91155 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -43,13 +43,13 @@ class string_constraint_generatort final // Axioms are of three kinds: universally quantified string constraint, // not contains string constraints and simple formulas. - std::vector axioms; + const std::vector &get_axioms() const; // Boolean symbols for the results of some string functions - const std::vector get_boolean_symbols() const; + const std::vector &get_boolean_symbols() const; /// Symbols used in existential quantifications - const std::vector& get_index_symbols() const; + const std::vector &get_index_symbols() const; // Used to store information about witnesses for not_contains constraints std::map witness; @@ -73,7 +73,6 @@ class string_constraint_generatort final 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; @@ -92,6 +91,8 @@ class string_constraint_generatort final private: messaget m_message; + std::vector axioms; + std::map unresolved_symbols; std::vector boolean_symbols; std::vector index_symbols; static constant_exprt constant_char(int i, const typet &char_type); @@ -105,7 +106,7 @@ class string_constraint_generatort final constexpr static const std::size_t MAX_DOUBLE_LENGTH=30; std::map function_application_cache; - namespacet ns; + const namespacet ns; static irep_idt extract_java_string(const symbol_exprt &s); diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 3cfef714af8..210ba4a3491 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -28,6 +28,11 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com unsigned string_constraint_generatort::next_symbol_id=1; +const std::vector &string_constraint_generatort::get_axioms() const +{ + return this->axioms; +} + const std::vector &string_constraint_generatort::get_index_symbols() const { @@ -35,9 +40,9 @@ const std::vector } const std::vector -string_constraint_generatort::get_boolean_symbols() const +&string_constraint_generatort::get_boolean_symbols() const { - return boolean_symbols; + return this->boolean_symbols; } /// generate constant character expression with character type. diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index e1f02a2f7f1..1cca895fdc3 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -496,7 +496,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) 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..c48b512f09d 100644 --- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -152,7 +152,7 @@ SCENARIO("instantiate_not_contains", 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) From 51d897a517b0326de59e8ff031d4c71ab4a43159 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 12:12:06 +0100 Subject: [PATCH 08/32] Better string_refinement constructor Act 1 --- src/cbmc/cbmc_solvers.cpp | 23 +++++----- src/solvers/refinement/string_refinement.cpp | 46 ++++++++------------ src/solvers/refinement/string_refinement.h | 28 +++++++----- 3 files changed, 46 insertions(+), 51 deletions(-) diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index c53c34375e3..385308035e7 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -167,21 +167,20 @@ 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(); + 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"); + + auto string_refinement=util_make_unique(info); if(options.get_option("max-node-refinement")!="") string_refinement->max_node_refinement= diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 1cca895fdc3..8e42d813f29 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -34,41 +34,29 @@ 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; + INVARIANT(info.ns, "Should not be null"); + INVARIANT(info.prop, "Should not be null"); + INVARIANT(info.ui, "Should not be null"); + 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() +string_refinementt::string_refinementt(const infot &info, bool): + supert(*info.ns, *info.prop), + use_counter_example(false), + do_concretizing(info.trace), + initial_loop_bound(info.refinement_bound), + generator(*info.ns), + non_empty_string(info.string_non_empty) { - non_empty_string=true; + this->set_ui(ui); + generator.max_string_length=info.string_max_length; + generator.force_printable_characters=info.string_printable; } -/// Add constraints on characters used in the program to ensure they are -/// printable -void string_refinementt::enforce_printable_characters() -{ - generator.force_printable_characters=true; -} +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() diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 0eec3e99a9a..b6cd0e7e456 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -31,10 +31,21 @@ Author: Alberto Griggio, alberto.griggio@gmail.com class string_refinementt: public bv_refinementt { public: - string_refinementt( - const namespacet &_ns, - propt &_prop, - unsigned refinement_bound); + /// string_refinementt constructor arguments + struct infot + { + const namespacet *ns=nullptr; + propt *prop=nullptr; + const language_uit::uit *ui=nullptr; + 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; + bool trace=false; + /// Make non-deterministic characters printable + bool string_printable=false; + }; + explicit string_refinementt(const infot &); void set_mode(); @@ -42,11 +53,7 @@ class string_refinementt: public bv_refinementt bool use_counter_example; // Should we concretize strings when the solver finished - bool do_concretizing; - - void set_max_string_length(size_t i); - void enforce_non_empty_string(); - void enforce_printable_characters(); + const bool do_concretizing; virtual std::string decision_procedure_text() const override { @@ -68,12 +75,13 @@ class string_refinementt: public bv_refinementt private: // Base class typedef bv_refinementt supert; + string_refinementt(const infot &, bool); 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 From 9146575b7a56eac12f3a3cd38e5db3c45707d41c Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 12:36:49 +0100 Subject: [PATCH 09/32] Better string_refinement constructor Act II --- src/cbmc/cbmc_solvers.cpp | 16 +++++--------- src/solvers/refinement/string_refinement.cpp | 3 +++ src/solvers/refinement/string_refinement.h | 23 +++++++++++--------- 3 files changed, 21 insertions(+), 21 deletions(-) diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index 385308035e7..8f66bad71be 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -179,20 +179,14 @@ std::unique_ptr cbmc_solverst::get_string_refinement() 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"); - - auto string_refinement=util_make_unique(info); - - if(options.get_option("max-node-refinement")!="") - string_refinement->max_node_refinement= + 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/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 8e42d813f29..0631fff4e2d 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -53,6 +53,9 @@ string_refinementt::string_refinementt(const infot &info, bool): this->set_ui(ui); generator.max_string_length=info.string_max_length; generator.force_printable_characters=info.string_printable; + this->max_node_refinement=info.max_node_refinement; + this->do_array_refinement=info.refine_arrays; + this->do_arithmetic_refinement=info.refine_arithmetic; } string_refinementt::string_refinementt(const infot &info): diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index b6cd0e7e456..2b9668ed791 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -28,7 +28,7 @@ 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 constructor arguments @@ -41,19 +41,21 @@ class string_refinementt: public bv_refinementt size_t string_max_length=std::numeric_limits::max(); /// Make non deterministic character arrays have at least one character bool string_non_empty=false; + // Should we concretize strings when the solver 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; }; + explicit string_refinementt(const infot &); void set_mode(); // Should we use counter examples at each iteration? - bool use_counter_example; - - // Should we concretize strings when the solver finished - const bool do_concretizing; + const bool use_counter_example=false; virtual std::string decision_procedure_text() const override { @@ -65,17 +67,18 @@ class string_refinementt: public bv_refinementt 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 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; From a00b2dbc791dbcd4178a6305e5c1d3846b5ad861 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 12:43:21 +0100 Subject: [PATCH 10/32] String refinement - remove unused public methods, fix comments --- src/solvers/refinement/string_refinement.h | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 2b9668ed791..0d3884e6340 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -39,9 +39,9 @@ class string_refinementt final: public bv_refinementt const language_uit::uit *ui=nullptr; unsigned refinement_bound=0; size_t string_max_length=std::numeric_limits::max(); - /// Make non deterministic character arrays have at least one character + /// Make non-deterministic character arrays have at least one character bool string_non_empty=false; - // Should we concretize strings when the solver finished + // Concretize strings after solver is finished bool trace=false; /// Make non-deterministic characters printable bool string_printable=false; @@ -52,9 +52,6 @@ class string_refinementt final: public bv_refinementt explicit string_refinementt(const infot &); - void set_mode(); - - // Should we use counter examples at each iteration? const bool use_counter_example=false; virtual std::string decision_procedure_text() const override @@ -62,8 +59,6 @@ class string_refinementt final: public bv_refinementt return "string refinement loop with "+prop.solver_text(); } - static exprt is_positive(const exprt &x); - exprt get(const exprt &expr) const override; protected: From 30fe11b604840755b7a02cb97865f7fa75895afc Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 13:07:15 +0100 Subject: [PATCH 11/32] Better string_constraint_generator constructor --- .../refinement/string_constraint_generator.h | 20 +++++++++++++------ .../string_constraint_generator_main.cpp | 6 ++++++ src/solvers/refinement/string_refinement.cpp | 20 +++++++++++++------ 3 files changed, 34 insertions(+), 12 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 6a396e91155..0c3dccb0871 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -33,13 +33,19 @@ class string_constraint_generatort final // string constraints for different string functions and add them // to the axiom list. - explicit string_constraint_generatort(namespacet _ns): ns(_ns) { } + /// 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; + }; - // Constraints on the maximal length of strings - size_t max_string_length=std::numeric_limits::max(); + explicit string_constraint_generatort(const infot& info); - // Should we add constraints on the characters - bool force_printable_characters=false; + const size_t max_string_length; // Axioms are of three kinds: universally quantified string constraint, // not contains string constraints and simple formulas. @@ -90,7 +96,9 @@ class string_constraint_generatort final class format_specifiert; private: - messaget m_message; + const messaget m_message; + const bool force_printable_characters; + std::vector axioms; std::map unresolved_symbols; std::vector boolean_symbols; diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 210ba4a3491..bb0df1acf54 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -28,6 +28,12 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com 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), + force_printable_characters(info.string_printable), + ns(*info.ns) { } + const std::vector &string_constraint_generatort::get_axioms() const { return this->axioms; diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 0631fff4e2d..59c888fe430 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -36,23 +36,31 @@ Author: Alberto Griggio, alberto.griggio@gmail.com static bool validate(const string_refinementt::infot &info) { - INVARIANT(info.ns, "Should not be null"); - INVARIANT(info.prop, "Should not be null"); - INVARIANT(info.ui, "Should not be null"); + PRECONDITION(info.ns); + PRECONDITION(info.prop); + PRECONDITION(info.ui); return true; } +static string_constraint_generatort::infot +generator_info(const string_refinementt::infot &in) +{ + 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(*info.ns, *info.prop), use_counter_example(false), do_concretizing(info.trace), initial_loop_bound(info.refinement_bound), - generator(*info.ns), + generator(generator_info(info)), non_empty_string(info.string_non_empty) { this->set_ui(ui); - generator.max_string_length=info.string_max_length; - generator.force_printable_characters=info.string_printable; this->max_node_refinement=info.max_node_refinement; this->do_array_refinement=info.refine_arrays; this->do_arithmetic_refinement=info.refine_arithmetic; From 99c815ef1c5421babc26fafda18ef7f02271aa6c Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 13:14:50 +0100 Subject: [PATCH 12/32] Make string_constraint_generatort::fresh_symbol non-static --- src/solvers/refinement/string_constraint_generator.h | 6 +++--- src/solvers/refinement/string_constraint_generator_main.cpp | 4 +--- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 0c3dccb0871..49eb819d0ae 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -67,9 +67,7 @@ class string_constraint_generatort final 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); @@ -96,6 +94,8 @@ class string_constraint_generatort final class format_specifiert; private: + unsigned m_symbol_count=0; + const messaget m_message; const bool force_printable_characters; diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index bb0df1acf54..12ead6fd13e 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -26,8 +26,6 @@ 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), @@ -71,7 +69,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); } From abe4046b3cda3756124341761a3e3017d3ec69ff Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 18:06:27 +0100 Subject: [PATCH 13/32] Better bv_refinement constructor --- src/cbmc/cbmc_solvers.cpp | 20 ++++++++------- src/solvers/refinement/bv_refinement.h | 16 ++++++++++-- src/solvers/refinement/bv_refinement_loop.cpp | 17 +++++-------- src/solvers/refinement/string_refinement.cpp | 25 ++++++++++++++++--- 4 files changed, 53 insertions(+), 25 deletions(-) diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index 8f66bad71be..bb45db31698 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 diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index d1e72e227b3..a81fffa8176 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -21,8 +21,20 @@ 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; + const language_uit::uit *ui=nullptr; + /// 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; + }; + + bv_refinementt(const infot &info); virtual decision_proceduret::resultt dec_solve(); diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index d471326ca0d..d5f5ef1e5d7 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 diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 59c888fe430..60b3294c90d 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -42,6 +42,19 @@ static bool validate(const string_refinementt::infot &info) return true; } +static bv_refinementt::infot bv_refinement_info( + const string_refinementt::infot &in) +{ + 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; +} + static string_constraint_generatort::infot generator_info(const string_refinementt::infot &in) { @@ -53,7 +66,7 @@ generator_info(const string_refinementt::infot &in) } string_refinementt::string_refinementt(const infot &info, bool): - supert(*info.ns, *info.prop), + supert(bv_refinement_info(info)), use_counter_example(false), do_concretizing(info.trace), initial_loop_bound(info.refinement_bound), @@ -1751,8 +1764,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()) From 792a70d361d8c7021c04b2a94e0a8a12cb404867 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 19:12:08 +0100 Subject: [PATCH 14/32] Hide bv_refinement members, add override specifier --- src/solvers/refinement/bv_refinement.h | 63 +++++++++----------- src/solvers/refinement/string_refinement.cpp | 8 +-- 2 files changed, 29 insertions(+), 42 deletions(-) diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index a81fffa8176..06a9cb2b8c0 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -36,31 +36,31 @@ class bv_refinementt:public bv_pointerst bv_refinementt(const infot &info); - virtual decision_proceduret::resultt dec_solve(); + decision_proceduret::resultt dec_solve() override; - virtual std::string decision_procedure_text() const + 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(); + // Collect stats + void set_to(const exprt &expr, bool value) override; + 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): @@ -92,38 +92,31 @@ class bv_refinementt:public bv_pointerst }; typedef std::list approximationst; - approximationst approximations; + resultt prop_solve(); approximationt &add_approximation(const exprt &expr, bvt &bv); + bool is_in_conflict(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::list approximations; bvt parent_assumptions; +protected: // use gui format language_uit::uit ui; }; diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 60b3294c90d..3c72bd4f1b3 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -71,13 +71,7 @@ string_refinementt::string_refinementt(const infot &info, bool): do_concretizing(info.trace), initial_loop_bound(info.refinement_bound), generator(generator_info(info)), - non_empty_string(info.string_non_empty) -{ - this->set_ui(ui); - this->max_node_refinement=info.max_node_refinement; - this->do_array_refinement=info.refine_arrays; - this->do_arithmetic_refinement=info.refine_arithmetic; -} + non_empty_string(info.string_non_empty) { } string_refinementt::string_refinementt(const infot &info): string_refinementt(info, validate(info)) { } From 07f6b394912c87bbff9abb04943039bc03db9fe8 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 19:03:29 +0100 Subject: [PATCH 15/32] Remove unnecessary typedef --- src/solvers/refinement/bv_refinement.h | 4 +-- src/solvers/refinement/bv_refinement_loop.cpp | 25 +++++++------------ 2 files changed, 10 insertions(+), 19 deletions(-) diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index 06a9cb2b8c0..4ba483f79ea 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -91,8 +91,6 @@ class bv_refinementt:public bv_pointerst std::size_t id_nr; }; - typedef std::list approximationst; - resultt prop_solve(); approximationt &add_approximation(const exprt &expr, bvt &bv); bool is_in_conflict(approximationt &approximation); @@ -113,7 +111,7 @@ class bv_refinementt:public bv_pointerst const bool do_array_refinement; const bool do_arithmetic_refinement; bool progress; - std::list approximations; + std::vector approximations; bvt parent_assumptions; protected: diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index d5f5ef1e5d7..9deb5508076 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -91,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); @@ -122,22 +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); + for(approximationt &approximation : this->approximations) + check_UNSAT(approximation); } void bv_refinementt::set_to(const exprt &expr, bool value) From 50173d60b2913e8c761911bb69eccae28c883e73 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 21:49:38 +0100 Subject: [PATCH 16/32] Make some string_constraint_generator methods static --- src/solvers/refinement/string_constraint_generator.h | 12 ++++++------ .../string_constraint_generator_code_points.cpp | 4 ++-- .../string_constraint_generator_testing.cpp | 2 +- .../string_constraint_generator_valueof.cpp | 2 +- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 49eb819d0ae..9bc930c777f 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -353,13 +353,13 @@ class string_constraint_generatort final } // 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); }; diff --git a/src/solvers/refinement/string_constraint_generator_code_points.cpp b/src/solvers/refinement/string_constraint_generator_code_points.cpp index d539e8d9e9e..e6c39598aa3 100644 --- a/src/solvers/refinement/string_constraint_generator_code_points.cpp +++ b/src/solvers/refinement/string_constraint_generator_code_points.cpp @@ -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())), diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp index 69ee6e40cbc..4aa29969eb7 100644 --- a/src/solvers/refinement/string_constraint_generator_testing.cpp +++ b/src/solvers/refinement/string_constraint_generator_testing.cpp @@ -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 || diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 1c215db583b..850e45ca281 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -189,7 +189,7 @@ string_exprt string_constraint_generatort::add_axioms_from_int_with_radix( /// \param chr: a character expression in the following set: /// 0123456789abcdef /// \return an integer expression -exprt string_constraint_generatort::int_of_hex_char(const exprt &chr) const +exprt string_constraint_generatort::int_of_hex_char(const exprt &chr) { exprt zero_char=constant_char('0', chr.type()); exprt nine_char=constant_char('9', chr.type()); From aa85392094e916f38b7e07f11446798b53ec3dcb Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 22:00:55 +0100 Subject: [PATCH 17/32] Make more generator methods private --- .../refinement/string_constraint_generator.h | 25 ++++++++++--------- 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 9bc930c777f..c9cbaf8f056 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -33,6 +33,9 @@ class string_constraint_generatort final // string constraints for different string functions and add them // to the axiom list. + // Used by format function + class format_specifiert; + /// Arguments pack for the string_constraint_generator constructor struct infot { @@ -69,31 +72,29 @@ class string_constraint_generatort final 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); - 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 // 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); - // Used by format function - class format_specifiert; - private: + symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type); + 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); + + string_exprt find_or_add_string_of_symbol( + const symbol_exprt &sym, + const refined_string_typet &ref_type); + unsigned m_symbol_count=0; const messaget m_message; From 5368c8c2a3e66723ef40b5a1508cb9df7d5008ed Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 22:09:29 +0100 Subject: [PATCH 18/32] Private get_created_strings --- src/solvers/refinement/string_constraint_generator.h | 9 ++++++--- .../refinement/string_constraint_generator_main.cpp | 6 ++++++ src/solvers/refinement/string_refinement.cpp | 4 ++-- 3 files changed, 14 insertions(+), 5 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index c9cbaf8f056..df161100f60 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -60,6 +60,9 @@ class string_constraint_generatort final /// Symbols used in existential quantifications const std::vector &get_index_symbols() const; + // Set of strings that have been created by the generator + const std::set &get_created_strings() const; + // Used to store information about witnesses for not_contains constraints std::map witness; @@ -76,15 +79,15 @@ class string_constraint_generatort final // Maps unresolved symbols to the string_exprt that was created for them - // Set of strings that have been created by the generator - std::set created_strings; - string_exprt add_axioms_for_refined_string(const exprt &expr); exprt add_axioms_for_function_application( const function_application_exprt &expr); private: + + std::set created_strings; + symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type); symbol_exprt fresh_boolean(const irep_idt &prefix); string_exprt fresh_string(const refined_string_typet &type); diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 12ead6fd13e..e0caa7bed65 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -49,6 +49,12 @@ const std::vector return this->boolean_symbols; } +const std::set +&string_constraint_generatort::get_created_strings() const +{ + return this->created_strings; +} + /// generate constant character expression with character type. /// \par parameters: integer representing a character, and a type for /// characters; diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 3c72bd4f1b3..65a38bd7c0b 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -379,7 +379,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(); } @@ -399,7 +399,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())) { From a440da73462f3d61d5138c73ff875ca0cf55dfa3 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 22:29:19 +0100 Subject: [PATCH 19/32] Group generator's member variables --- .../refinement/string_constraint_generator.h | 71 +++++++++---------- 1 file changed, 35 insertions(+), 36 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index df161100f60..8e30612c8d8 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -48,8 +48,6 @@ class string_constraint_generatort final explicit string_constraint_generatort(const infot& info); - const size_t max_string_length; - // Axioms are of three kinds: universally quantified string constraint, // not contains string constraints and simple formulas. const std::vector &get_axioms() const; @@ -63,9 +61,6 @@ class string_constraint_generatort final // Set of strings that have been created by the generator const std::set &get_created_strings() const; - // Used to store information about witnesses for not_contains constraints - std::map witness; - exprt get_witness_of( const string_not_contains_constraintt &c, const exprt &univ_val) const @@ -86,8 +81,6 @@ class string_constraint_generatort final private: - std::set created_strings; - symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type); symbol_exprt fresh_boolean(const irep_idt &prefix); string_exprt fresh_string(const refined_string_typet &type); @@ -98,27 +91,7 @@ class string_constraint_generatort final const symbol_exprt &sym, const refined_string_typet &ref_type); - unsigned m_symbol_count=0; - - const messaget m_message; - const bool force_printable_characters; - - std::vector axioms; - std::map unresolved_symbols; - std::vector boolean_symbols; - std::vector index_symbols; static constant_exprt constant_char(int i, const typet &char_type); - // 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. - constexpr static const std::size_t MAX_INTEGER_LENGTH=11; - constexpr static const std::size_t MAX_LONG_LENGTH=20; - constexpr static const std::size_t MAX_FLOAT_LENGTH=15; - constexpr static const std::size_t MAX_DOUBLE_LENGTH=30; - - std::map function_application_cache; - const namespacet ns; static irep_idt extract_java_string(const symbol_exprt &s); @@ -142,9 +115,6 @@ class string_constraint_generatort final // 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( @@ -341,12 +311,6 @@ class string_constraint_generatort final // 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) @@ -365,6 +329,41 @@ class string_constraint_generatort final 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: + // Used to store information about witnesses for not_contains constraints + const size_t max_string_length; + 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. + constexpr static const std::size_t MAX_INTEGER_LENGTH=11; + constexpr static const std::size_t MAX_LONG_LENGTH=20; + constexpr static const std::size_t MAX_FLOAT_LENGTH=15; + constexpr static const std::size_t MAX_DOUBLE_LENGTH=30; + std::set created_strings; + unsigned m_symbol_count=0; + const messaget m_message; + const bool force_printable_characters; + + std::vector axioms; + std::map unresolved_symbols; + std::vector boolean_symbols; + std::vector index_symbols; + std::map function_application_cache; + const namespacet 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 hash_code_of_string; + + // Pool used for the intern method + std::map intern_of_string; + + // Tells which language is used. C and Java are supported + irep_idt mode; }; exprt is_digit_with_radix( From 01c6767bb8f127406d6e61e2301926502d5cb6fb Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 22:39:48 +0100 Subject: [PATCH 20/32] Rename axioms to m_axioms --- .../refinement/string_constraint_generator.h | 6 +-- ...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 | 28 +++++------ .../string_constraint_generator_testing.cpp | 26 +++++----- ...ng_constraint_generator_transformation.cpp | 48 +++++++++---------- .../string_constraint_generator_valueof.cpp | 40 ++++++++-------- 11 files changed, 129 insertions(+), 129 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 8e30612c8d8..885e40497f3 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -344,12 +344,12 @@ class string_constraint_generatort final constexpr static const std::size_t MAX_LONG_LENGTH=20; constexpr static const std::size_t MAX_FLOAT_LENGTH=15; constexpr static const std::size_t MAX_DOUBLE_LENGTH=30; - std::set created_strings; + std::set m_created_strings; unsigned m_symbol_count=0; const messaget m_message; - const bool force_printable_characters; + const bool m_force_printable_characters; - std::vector axioms; + std::vector m_axioms; std::map unresolved_symbols; std::vector boolean_symbols; std::vector 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 e6c39598aa3..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; } @@ -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..3e81a742417 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; } @@ -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; } @@ -279,7 +279,7 @@ symbol_exprt string_constraint_generatort::add_axioms_for_intern( 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 @@ -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); - 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_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 e0caa7bed65..f2f623265e2 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -29,12 +29,12 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com string_constraint_generatort::string_constraint_generatort( const string_constraint_generatort::infot& info): max_string_length(info.string_max_length), - force_printable_characters(info.string_printable), + m_force_printable_characters(info.string_printable), ns(*info.ns) { } const std::vector &string_constraint_generatort::get_axioms() const { - return this->axioms; + return m_axioms; } const std::vector @@ -52,7 +52,7 @@ const std::vector const std::set &string_constraint_generatort::get_created_strings() const { - return this->created_strings; + return m_created_strings; } /// generate constant character expression with character type. @@ -133,7 +133,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; } @@ -147,7 +147,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; } @@ -182,12 +182,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]; @@ -195,7 +195,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); } } @@ -281,18 +281,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; } @@ -614,7 +614,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 4aa29969eb7..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; } @@ -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 850e45ca281..3d8b4c6bccb 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); } } From e5c45a5b84273a37423b042be4c8a11a4486a716 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Sat, 26 Aug 2017 22:54:58 +0100 Subject: [PATCH 21/32] Prefix all generator member variables with "m_" --- .../refinement/string_constraint_generator.h | 17 ++++++-------- ...string_constraint_generator_comparison.cpp | 10 ++++----- .../string_constraint_generator_main.cpp | 22 +++++++++---------- .../string_constraint_generator_valueof.cpp | 2 +- 4 files changed, 24 insertions(+), 27 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 885e40497f3..525f54174c3 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -350,20 +350,17 @@ class string_constraint_generatort final const bool m_force_printable_characters; std::vector m_axioms; - std::map unresolved_symbols; - std::vector boolean_symbols; - std::vector index_symbols; - std::map function_application_cache; - const namespacet ns; + 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 hash_code_of_string; + std::map m_hash_code_of_string; // Pool used for the intern method - std::map intern_of_string; - - // Tells which language is used. C and Java are supported - irep_idt mode; + std::map m_intern_of_string; }; exprt is_digit_with_radix( diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp index 3e81a742417..7bc276cd24a 100644 --- a/src/solvers/refinement/string_constraint_generator_comparison.cpp +++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp @@ -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); @@ -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,7 +275,7 @@ 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)); @@ -283,7 +283,7 @@ symbol_exprt string_constraint_generatort::add_axioms_for_intern( // 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); diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index f2f623265e2..b1d8856c0c4 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -30,7 +30,7 @@ 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), - ns(*info.ns) { } + m_ns(*info.ns) { } const std::vector &string_constraint_generatort::get_axioms() const { @@ -40,13 +40,13 @@ const std::vector &string_constraint_generatort::get_axioms() const const std::vector &string_constraint_generatort::get_index_symbols() const { - return this->index_symbols; + return m_index_symbols; } const std::vector &string_constraint_generatort::get_boolean_symbols() const { - return this->boolean_symbols; + return m_boolean_symbols; } const std::set @@ -96,7 +96,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; } @@ -107,7 +107,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; } @@ -307,7 +307,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; } @@ -336,7 +336,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) { @@ -356,7 +356,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) { @@ -372,8 +372,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; @@ -503,7 +503,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; } diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 3d8b4c6bccb..f54a821f623 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -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); } From 1282d03a7d256263b3a73099ee152ce1b12b6c23 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Tue, 29 Aug 2017 16:17:57 +0100 Subject: [PATCH 22/32] Update unit tests with new constructors --- .../refinement/string_constraint_generator.h | 4 +-- .../instantiate_not_contains.cpp | 32 +++++++++++++++---- 2 files changed, 27 insertions(+), 9 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 525f54174c3..40fae5e19ab 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -79,9 +79,9 @@ class string_constraint_generatort final exprt add_axioms_for_function_application( const function_application_exprt &expr); -private: - 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); 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 c48b512f09d..8f064d946f6 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,7 +153,9 @@ 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; @@ -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()); From 40871878c880d898fffa84e1ba9339af93d6acbb Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Tue, 29 Aug 2017 16:14:06 +0100 Subject: [PATCH 23/32] Don't pass language_uit::uit as a pointer --- src/cbmc/cbmc_solvers.cpp | 4 ++-- src/solvers/refinement/bv_refinement.h | 2 +- src/solvers/refinement/bv_refinement_loop.cpp | 2 +- src/solvers/refinement/string_refinement.cpp | 3 +-- src/solvers/refinement/string_refinement.h | 2 +- .../instantiate_not_contains.cpp | 4 ++-- 6 files changed, 8 insertions(+), 9 deletions(-) diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index bb45db31698..d98b8b3dcca 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -149,7 +149,7 @@ std::unique_ptr cbmc_solverst::get_bv_refinement() bv_refinementt::infot info; info.ns=&ns; info.prop=prop.get(); - info.ui=&ui; + info.ui=ui; // we allow setting some parameters if(options.get_bool_option("max-node-refinement")) @@ -175,7 +175,7 @@ std::unique_ptr cbmc_solverst::get_string_refinement() prop->set_message_handler(get_message_handler()); info.prop=prop.get(); info.refinement_bound=MAX_NB_REFINEMENT; - info.ui=&ui; + info.ui=ui; if(options.get_bool_option("string-max-length")) info.string_max_length=options.get_signed_int_option("string-max-length"); info.string_non_empty=options.get_bool_option("string-non-empty"); diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index 4ba483f79ea..17fc63ff728 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -25,7 +25,7 @@ class bv_refinementt:public bv_pointerst { const namespacet *ns=nullptr; propt *prop=nullptr; - const language_uit::uit *ui=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 diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index 9deb5508076..4e96ac8e82a 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -18,7 +18,7 @@ bv_refinementt::bv_refinementt(const infot &info): do_array_refinement(info.refine_arrays), do_arithmetic_refinement(info.refine_arithmetic), progress(false), - ui(*info.ui) + ui(info.ui) { // check features we need PRECONDITION(prop.has_set_assumptions()); diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 65a38bd7c0b..608b70212aa 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -38,7 +38,6 @@ static bool validate(const string_refinementt::infot &info) { PRECONDITION(info.ns); PRECONDITION(info.prop); - PRECONDITION(info.ui); return true; } @@ -1764,7 +1763,7 @@ bool string_refinementt::is_axiom_sat( info.refine_arithmetic=true; info.refine_arrays=true; info.max_node_refinement=5; - info.ui=&ui; + info.ui=ui; supert solver(info); solver << axiom; diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 0d3884e6340..ccb082a8878 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -36,7 +36,7 @@ class string_refinementt final: public bv_refinementt { const namespacet *ns=nullptr; propt *prop=nullptr; - const language_uit::uit *ui=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 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 8f064d946f6..48cf3ed8e27 100644 --- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -122,8 +122,8 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns) bv_refinementt::infot info; info.ns=&ns; info.prop=&sat_check; - const auto ui = language_uit::uit::PLAIN; - info.ui=&ui; + const auto ui=language_uit::uit::PLAIN; + info.ui=ui; bv_refinementt solver(info); solver << expr; return solver(); From 83a29dc09f1ea56bd8cd55952f81269bad20b5dd Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Tue, 29 Aug 2017 16:30:21 +0100 Subject: [PATCH 24/32] Fix linter errors --- src/solvers/refinement/bv_refinement.h | 2 +- .../refinement/string_constraint_generator_format.cpp | 5 +++-- .../calculate_max_string_length.cpp | 3 ++- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index 17fc63ff728..d8c5931400b 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -34,7 +34,7 @@ class bv_refinementt:public bv_pointerst bool refine_arithmetic=true; }; - bv_refinementt(const infot &info); + explicit bv_refinementt(const infot &info); decision_proceduret::resultt dec_solve() override; diff --git a/src/solvers/refinement/string_constraint_generator_format.cpp b/src/solvers/refinement/string_constraint_generator_format.cpp index fdfff031d9a..ae672e6a01c 100644 --- a/src/solvers/refinement/string_constraint_generator_format.cpp +++ b/src/solvers/refinement/string_constraint_generator_format.cpp @@ -434,8 +434,9 @@ string_exprt string_constraint_generatort::add_axioms_for_format( } else { - m_message.warning() << "ignoring format function with non constant first argument" - << m_message.eom; + m_message.warning() + << "ignoring format function with non constant first argument" + << m_message.eom; return fresh_string(ref_type); } } 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), From 107704a1aab3bdb5320b9a034aea4e50a38c4c73 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Tue, 29 Aug 2017 17:07:58 +0100 Subject: [PATCH 25/32] Fix is_in_conflict with conflict override --- src/solvers/refinement/bv_refinement.h | 2 +- src/solvers/refinement/refine_arithmetic.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index d8c5931400b..1f7b1c1f85e 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -93,7 +93,7 @@ class bv_refinementt:public bv_pointerst resultt prop_solve(); approximationt &add_approximation(const exprt &expr, bvt &bv); - bool is_in_conflict(approximationt &approximation); + bool conflicts_with(approximationt &approximation); void check_SAT(approximationt &approximation); void check_UNSAT(approximationt &approximation); void initialize(approximationt &approximation); 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 Date: Tue, 29 Aug 2017 17:14:15 +0100 Subject: [PATCH 26/32] Preprocess constexpr --- .../refinement/string_constraint_generator.h | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 40fae5e19ab..2a7d3e2822b 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -26,6 +26,12 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include +#if defined(__GNUC__) || defined(__clang__) +#define CBMC_CONSTEXPR constexpr +#else +#define CBMC_CONSTEXPR +#endif + class string_constraint_generatort final { public: @@ -340,10 +346,10 @@ class string_constraint_generatort final // 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. - constexpr static const std::size_t MAX_INTEGER_LENGTH=11; - constexpr static const std::size_t MAX_LONG_LENGTH=20; - constexpr static const std::size_t MAX_FLOAT_LENGTH=15; - constexpr static const std::size_t MAX_DOUBLE_LENGTH=30; + 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; From acaad4fd2e8b386307af9afca7e9d342886a2000 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Wed, 30 Aug 2017 11:22:24 +0100 Subject: [PATCH 27/32] Remove dead bv_refinementt::set_to --- src/solvers/refinement/bv_refinement.h | 2 -- src/solvers/refinement/bv_refinement_loop.cpp | 18 ------------------ 2 files changed, 20 deletions(-) diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index 1f7b1c1f85e..6d4fb84db95 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -54,8 +54,6 @@ class bv_refinementt:public bv_pointerst bvt convert_mod(const mod_exprt &expr) override; bvt convert_floatbv_op(const exprt &expr) override; - // Collect stats - void set_to(const exprt &expr, bool value) override; void set_assumptions(const bvt &_assumptions) override; private: diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index 4e96ac8e82a..e3ac990b3a4 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -133,24 +133,6 @@ void bv_refinementt::check_UNSAT() check_UNSAT(approximation); } -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 -} - void bv_refinementt::set_assumptions(const bvt &_assumptions) { parent_assumptions=_assumptions; From 04fae6d7b32656d2c948a3908efbc2ed7932ff8d Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Wed, 30 Aug 2017 11:34:04 +0100 Subject: [PATCH 28/32] Correct comment --- src/solvers/refinement/string_constraint_generator.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 2a7d3e2822b..666c60e95a6 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -338,8 +338,8 @@ class string_constraint_generatort final // MEMBERS public: - // Used to store information about witnesses for not_contains constraints 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, From 7fd2bfa53436fff54562c187d69fe6078fb70697 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Wed, 30 Aug 2017 12:01:44 +0100 Subject: [PATCH 29/32] Use_counter_example assignable via constructor --- src/solvers/refinement/string_refinement.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index ccb082a8878..35edb45ff01 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -48,11 +48,11 @@ class string_refinementt final: public bv_refinementt unsigned max_node_refinement=5; bool refine_arrays=false; bool refine_arithmetic=false; + bool use_counter_example=false; }; explicit string_refinementt(const infot &); - const bool use_counter_example=false; virtual std::string decision_procedure_text() const override { @@ -65,6 +65,7 @@ class string_refinementt final: public bv_refinementt decision_proceduret::resultt dec_solve() override; private: + const bool use_counter_example; const bool do_concretizing; // Base class typedef bv_refinementt supert; From 22d699cbe61437184fb1d9185f539852fcbae9ec Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Wed, 30 Aug 2017 17:08:48 +0100 Subject: [PATCH 30/32] Move constexpr ifdef into a util header --- src/solvers/refinement/string_constraint_generator.h | 7 +------ .../refinement/string_constraint_generator_main.cpp | 1 + src/solvers/refinement/string_refinement.h | 1 + src/util/constexpr.def | 6 ++++++ 4 files changed, 9 insertions(+), 6 deletions(-) create mode 100644 src/util/constexpr.def diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 666c60e95a6..f4de12b7544 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -24,14 +24,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include #include +#include #include -#if defined(__GNUC__) || defined(__clang__) -#define CBMC_CONSTEXPR constexpr -#else -#define CBMC_CONSTEXPR -#endif - class string_constraint_generatort final { public: diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index b1d8856c0c4..9c49b6acfbb 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 diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 35edb45ff01..11e290e252b 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 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 + From 8da7c3003cbb875727e9f13de6a901fca60f5372 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Wed, 30 Aug 2017 17:13:50 +0100 Subject: [PATCH 31/32] Constraint generator doxygen --- src/solvers/refinement/string_constraint_generator.h | 11 +++++------ src/solvers/refinement/string_refinement.h | 2 +- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index f4de12b7544..7a0667fb397 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -49,17 +49,17 @@ class string_constraint_generatort final explicit string_constraint_generatort(const infot& info); - // Axioms are of three kinds: universally quantified string constraint, - // not contains string constraints and simple formulas. + /// 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 + /// Boolean symbols for the results of some string functions const std::vector &get_boolean_symbols() const; /// Symbols used in existential quantifications const std::vector &get_index_symbols() const; - // Set of strings that have been created by the generator + /// Set of strings that have been created by the generator const std::set &get_created_strings() const; exprt get_witness_of( @@ -73,8 +73,7 @@ class string_constraint_generatort final const irep_idt &prefix, const typet &type=bool_typet()); symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type); - // Maps unresolved symbols to the string_exprt that was created for them - + /// 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( diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 11e290e252b..021176d4178 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -42,7 +42,7 @@ class string_refinementt final: public bv_refinementt 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 + /// Concretize strings after solver is finished bool trace=false; /// Make non-deterministic characters printable bool string_printable=false; From 0838f611e4f130943cfa48d5aaf86a91d9233ea8 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Wed, 30 Aug 2017 17:15:24 +0100 Subject: [PATCH 32/32] Fix function declaration slicing --- .../refinement/string_constraint_generator_main.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 9c49b6acfbb..f149ef3ecf1 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -38,20 +38,20 @@ const std::vector &string_constraint_generatort::get_axioms() const return m_axioms; } -const std::vector -&string_constraint_generatort::get_index_symbols() const +const std::vector & +string_constraint_generatort::get_index_symbols() const { return m_index_symbols; } -const std::vector -&string_constraint_generatort::get_boolean_symbols() const +const std::vector & +string_constraint_generatort::get_boolean_symbols() const { return m_boolean_symbols; } -const std::set -&string_constraint_generatort::get_created_strings() const +const std::set & +string_constraint_generatort::get_created_strings() const { return m_created_strings; }