diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index d3861bda26a..5e9b39f5f68 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -28,7 +28,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include + +#include #include diff --git a/jbmc/src/jbmc/module_dependencies.txt b/jbmc/src/jbmc/module_dependencies.txt index a03a731ed11..e878b9c20fe 100644 --- a/jbmc/src/jbmc/module_dependencies.txt +++ b/jbmc/src/jbmc/module_dependencies.txt @@ -11,4 +11,5 @@ langapi # should go away linking pointer-analysis solvers/refinement +solvers/strings util diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 531a3cb8fe7..1dbcd830f4f 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -54,9 +54,9 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ java_bytecode/java_virtual_functions/virtual_functions.cpp \ java_bytecode/load_method_by_regex.cpp \ pointer-analysis/custom_value_set_analysis.cpp \ - solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \ - solvers/refinement/string_refinement/dependency_graph.cpp \ - solvers/refinement/string_refinement/string_symbol_resolution.cpp \ + solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp \ + solvers/strings/string_refinement/dependency_graph.cpp \ + solvers/strings/string_refinement/string_symbol_resolution.cpp \ util/expr_iterator.cpp \ util/has_subtype.cpp \ util/parameter_indices.cpp \ diff --git a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp similarity index 93% rename from jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp rename to jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp index d7da8903792..4a673595f5d 100644 --- a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp @@ -8,18 +8,18 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com #include -#include #include #include +#include -#include #include +#include -#include #include +#include -#include #include +#include /// \class Types used throughout the test. Currently it is impossible to /// statically initialize this value, there is a PR to allow this @@ -27,9 +27,17 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com class tt { public: - tt() {} - typet char_type() const {return java_char_type();} - typet length_type() const {return java_int_type();} + tt() + { + } + typet char_type() const + { + return java_char_type(); + } + typet length_type() const + { + return java_int_type(); + } array_typet array_type() const { return array_typet(char_type(), infinity_exprt(length_type())); @@ -60,7 +68,7 @@ constant_exprt from_integer(const mp_integer &i) /// \return corresponding `string_exprt` array_string_exprt make_string_exprt(const std::string &str) { - const constant_exprt length=from_integer(str.length(), t.length_type()); + const constant_exprt length = from_integer(str.length(), t.length_type()); array_exprt content({}, array_typet(t.char_type(), length)); for(const char c : str) @@ -92,7 +100,7 @@ std::set full_index_set(const array_string_exprt &s) { const mp_integer n = numeric_cast_v(s.length()); std::set ret; - for(mp_integer i=0; i> product(const std::set xs, const std::set ys) exprt combine_lemmas(const std::vector &lemmas, const namespacet &ns) { // Conjunction of new lemmas - exprt conj=conjunction(lemmas); + exprt conj = conjunction(lemmas); // Simplify simplify(conj, ns); @@ -137,7 +145,7 @@ std::string create_info(std::vector &lemmas, const namespacet &ns) get_language_from_mode(ID_java)->from_expr(lemma, lemma_string, ns); new_lemmas += lemma_string + "\n\n"; } - return "Instantiated lemmas:\n"+new_lemmas; + return "Instantiated lemmas:\n" + new_lemmas; } /// Checks the satisfiability of the given expression. @@ -148,8 +156,8 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns) { satcheck_no_simplifiert sat_check; bv_refinementt::infot info; - info.ns=&ns; - info.prop=&sat_check; + info.ns = &ns; + info.prop = &sat_check; info.output_xml = false; bv_refinementt solver(info); solver << expr; @@ -157,7 +165,8 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns) } // The [!mayfail] tag allows tests to fail while reporting the failure -SCENARIO("instantiate_not_contains", +SCENARIO( + "instantiate_not_contains", "[!mayfail][core][solvers][refinement][string_constraint_instantiation]") { // For printing expression @@ -261,10 +270,10 @@ SCENARIO("instantiate_not_contains", decision_proceduret::resultt result = check_sat(conj, empty_ns); // Require SAT - if(result==decision_proceduret::resultt::D_ERROR) + if(result == decision_proceduret::resultt::D_ERROR) INFO("Got an error"); - REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE); + REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE); } } } @@ -311,10 +320,10 @@ SCENARIO("instantiate_not_contains", decision_proceduret::resultt result = check_sat(conj, empty_ns); // Require SAT - if(result==decision_proceduret::resultt::D_ERROR) + if(result == decision_proceduret::resultt::D_ERROR) INFO("Got an error"); - REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE); + REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE); } } } @@ -362,10 +371,10 @@ SCENARIO("instantiate_not_contains", decision_proceduret::resultt result = check_sat(conj, empty_ns); // Require UNSAT - if(result==decision_proceduret::resultt::D_ERROR) + if(result == decision_proceduret::resultt::D_ERROR) INFO("Got an error"); - REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE); + REQUIRE(result == decision_proceduret::resultt::D_UNSATISFIABLE); } } } @@ -414,10 +423,10 @@ SCENARIO("instantiate_not_contains", decision_proceduret::resultt result = check_sat(conj, empty_ns); // Require UNSAT - if(result==decision_proceduret::resultt::D_ERROR) + if(result == decision_proceduret::resultt::D_ERROR) INFO("Got an error"); - REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE); + REQUIRE(result == decision_proceduret::resultt::D_UNSATISFIABLE); } } } @@ -465,10 +474,10 @@ SCENARIO("instantiate_not_contains", decision_proceduret::resultt result = check_sat(conj, empty_ns); // Require UNSAT - if(result==decision_proceduret::resultt::D_ERROR) + if(result == decision_proceduret::resultt::D_ERROR) INFO("Got an error"); - REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE); + REQUIRE(result == decision_proceduret::resultt::D_UNSATISFIABLE); } } } @@ -517,10 +526,10 @@ SCENARIO("instantiate_not_contains", decision_proceduret::resultt result = check_sat(conj, empty_ns); // Require UNSAT - if(result==decision_proceduret::resultt::D_ERROR) + if(result == decision_proceduret::resultt::D_ERROR) INFO("Got an error"); - REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE); + REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE); } } } diff --git a/jbmc/unit/solvers/refinement/string_constraint_instantiation/module_dependencies.txt b/jbmc/unit/solvers/strings/string_constraint_instantiation/module_dependencies.txt similarity index 88% rename from jbmc/unit/solvers/refinement/string_constraint_instantiation/module_dependencies.txt rename to jbmc/unit/solvers/strings/string_constraint_instantiation/module_dependencies.txt index 0741e46c2df..83b02a43c06 100644 --- a/jbmc/unit/solvers/refinement/string_constraint_instantiation/module_dependencies.txt +++ b/jbmc/unit/solvers/strings/string_constraint_instantiation/module_dependencies.txt @@ -2,6 +2,7 @@ java_bytecode langapi # should go away solvers/refinement solvers/sat +solvers/strings string_constraint_instantiation testing-utils util diff --git a/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp b/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp similarity index 99% rename from jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp rename to jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp index be2c4d72868..4bbf21c5d22 100644 --- a/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp +++ b/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp @@ -9,11 +9,11 @@ Author: Diffblue Ltd. #include +#include +#include #include -#include #include -#include -#include +#include #ifdef DEBUG #include diff --git a/jbmc/unit/solvers/refinement/string_refinement/module_dependencies.txt b/jbmc/unit/solvers/strings/string_refinement/module_dependencies.txt similarity index 85% rename from jbmc/unit/solvers/refinement/string_refinement/module_dependencies.txt rename to jbmc/unit/solvers/strings/string_refinement/module_dependencies.txt index 0c66e23bb4a..5042f45bb3e 100644 --- a/jbmc/unit/solvers/refinement/string_refinement/module_dependencies.txt +++ b/jbmc/unit/solvers/strings/string_refinement/module_dependencies.txt @@ -2,5 +2,6 @@ java_bytecode langapi # should go away string_refinement solvers/refinement +solvers/strings testing-utils util diff --git a/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp b/jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp similarity index 89% rename from jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp rename to jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp index 81f225ed78a..352bd3d4eb9 100644 --- a/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp +++ b/jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp @@ -9,17 +9,19 @@ Author: Diffblue Ltd. #include +#include + +#include +#include +#include #include #include #include -#include #include -#include -#include -#include -SCENARIO("string_identifiers_resolution_from_equations", -"[core][solvers][refinement][string_refinement]") +SCENARIO( + "string_identifiers_resolution_from_equations", + "[core][solvers][refinement][string_refinement]") { // For printing expression register_language(new_java_bytecode_language); @@ -50,8 +52,7 @@ SCENARIO("string_identifiers_resolution_from_equations", WHEN("There is no function call") { union_find_replacet symbol_resolve = - string_identifiers_resolution_from_equations( - equations, ns, stream); + string_identifiers_resolution_from_equations(equations, ns, stream); THEN("The symbol resolution structure is empty") { @@ -69,8 +70,7 @@ SCENARIO("string_identifiers_resolution_from_equations", symbol_exprt bool_sym("bool_b", bool_typet()); equations.emplace_back(bool_sym, fun); union_find_replacet symbol_resolve = - string_identifiers_resolution_from_equations( - equations, ns, stream); + string_identifiers_resolution_from_equations(equations, ns, stream); THEN("Equations that depend on it should be added") { diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index bb6329ecebe..1b26e83ab7e 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -29,7 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include #include "bmc.h" #include "xml_interface.h" diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 2c1f9a85373..20c2520fa33 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -28,9 +28,9 @@ Author: Daniel Kroening, Peter Schrammel #include #include #include -#include #include #include +#include solver_factoryt::solver_factoryt( const optionst &_options, diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 924294b3297..d176bb6ecfb 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -161,23 +161,23 @@ SRC = $(BOOLEFORCE_SRC) \ refinement/bv_refinement_loop.cpp \ refinement/refine_arithmetic.cpp \ refinement/refine_arrays.cpp \ - refinement/string_builtin_function.cpp \ - refinement/string_refinement.cpp \ - refinement/string_refinement_util.cpp \ - refinement/string_constraint.cpp \ - refinement/string_constraint_generator_code_points.cpp \ - refinement/string_constraint_generator_comparison.cpp \ - refinement/string_constraint_generator_concat.cpp \ - refinement/string_constraint_generator_constants.cpp \ - refinement/string_constraint_generator_indexof.cpp \ - refinement/string_constraint_generator_insert.cpp \ - refinement/string_constraint_generator_float.cpp \ - refinement/string_constraint_generator_format.cpp \ - refinement/string_constraint_generator_main.cpp \ - refinement/string_constraint_generator_testing.cpp \ - refinement/string_constraint_generator_transformation.cpp \ - refinement/string_constraint_generator_valueof.cpp \ - refinement/string_constraint_instantiation.cpp \ + strings/string_builtin_function.cpp \ + strings/string_refinement.cpp \ + strings/string_refinement_util.cpp \ + strings/string_constraint.cpp \ + strings/string_constraint_generator_code_points.cpp \ + strings/string_constraint_generator_comparison.cpp \ + strings/string_constraint_generator_concat.cpp \ + strings/string_constraint_generator_constants.cpp \ + strings/string_constraint_generator_indexof.cpp \ + strings/string_constraint_generator_insert.cpp \ + strings/string_constraint_generator_float.cpp \ + strings/string_constraint_generator_format.cpp \ + strings/string_constraint_generator_main.cpp \ + strings/string_constraint_generator_testing.cpp \ + strings/string_constraint_generator_transformation.cpp \ + strings/string_constraint_generator_valueof.cpp \ + strings/string_constraint_instantiation.cpp \ sat/cnf.cpp \ sat/cnf_clause_list.cpp \ sat/dimacs_cnf.cpp \ diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp index d78c9dceac0..6eaf78a4b72 100644 --- a/src/solvers/refinement/refine_arithmetic.cpp +++ b/src/solvers/refinement/refine_arithmetic.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include // Parameters @@ -167,10 +166,7 @@ void bv_refinementt::check_SAT(approximationt &a) if(type.id()==ID_floatbv) { - // these are all ternary - INVARIANT( - a.expr.operands().size()==3, - string_refinement_invariantt("all floatbv typed exprs are ternary")); + const auto &float_op = to_ieee_float_op_expr(a.expr); if(a.over_state==MAX_STATE) return; @@ -182,7 +178,7 @@ void bv_refinementt::check_SAT(approximationt &a) o1.unpack(a.op1_value); // get actual rounding mode - exprt rounding_mode_expr = get(a.expr.op2()); + exprt rounding_mode_expr = get(float_op.rounding_mode()); const std::size_t rounding_mode_int = numeric_cast_v(rounding_mode_expr); ieee_floatt::rounding_modet rounding_mode = @@ -279,8 +275,7 @@ void bv_refinementt::check_SAT(approximationt &a) { // these are all binary INVARIANT( - a.expr.operands().size()==2, - string_refinement_invariantt("all (un)signedbv typed exprs are binary")); + a.expr.operands().size() == 2, "all (un)signedbv typed exprs are binary"); // already full interpretation? if(a.over_state>0) diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp index 2e713b44d39..fc6cefbfb7b 100644 --- a/src/solvers/refinement/refine_arrays.cpp +++ b/src/solvers/refinement/refine_arrays.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include /// generate array constraints @@ -55,9 +54,6 @@ void bv_refinementt::arrays_overapproximated() if(current.id()==ID_implies) { implies_exprt imp=to_implies_expr(current); - DATA_INVARIANT( - imp.operands().size()==2, - string_refinement_invariantt("implies must have two operands")); exprt implies_simplified=get(imp.op0()); if(implies_simplified==false_exprt()) { @@ -70,8 +66,7 @@ void bv_refinementt::arrays_overapproximated() { or_exprt orexp=to_or_expr(current); INVARIANT( - orexp.operands().size()==2, - string_refinement_invariantt("only treats the case of a binary or")); + orexp.operands().size() == 2, "only treats the case of a binary or"); exprt o1=get(orexp.op0()); exprt o2=get(orexp.op1()); if(o1==true_exprt() || o2 == true_exprt()) @@ -95,10 +90,7 @@ void bv_refinementt::arrays_overapproximated() lazy_array_constraints.erase(it++); break; default: - INVARIANT( - false, - string_refinement_invariantt("error in array over approximation " - "check")); + INVARIANT(false, "error in array over approximation check"); } } diff --git a/src/solvers/strings/module_dependencies.txt b/src/solvers/strings/module_dependencies.txt new file mode 100644 index 00000000000..4f743b2d89d --- /dev/null +++ b/src/solvers/strings/module_dependencies.txt @@ -0,0 +1,6 @@ +solvers/flattening +solvers/floatbv +solvers/refinement +solvers/sat +solvers/strings +util diff --git a/src/solvers/refinement/string_builtin_function.cpp b/src/solvers/strings/string_builtin_function.cpp similarity index 96% rename from src/solvers/refinement/string_builtin_function.cpp rename to src/solvers/strings/string_builtin_function.cpp index 692d6d64d75..003024bdac7 100644 --- a/src/solvers/refinement/string_builtin_function.cpp +++ b/src/solvers/strings/string_builtin_function.cpp @@ -247,13 +247,11 @@ string_constraintst string_set_char_builtin_functiont::constraints( { string_constraintst constraints; constraints.existential.push_back(length_constraint()); - constraints.existential.push_back( - implies_exprt( - and_exprt( - binary_relation_exprt( - from_integer(0, position.type()), ID_le, position), - binary_relation_exprt(position, ID_lt, result.length())), - equal_exprt(result[position], character))); + constraints.existential.push_back(implies_exprt( + and_exprt( + binary_relation_exprt(from_integer(0, position.type()), ID_le, position), + binary_relation_exprt(position, ID_lt, result.length())), + equal_exprt(result[position], character))); constraints.universal.push_back([&] { const symbol_exprt q = generator.fresh_symbol("QA_char_set", position.type()); @@ -323,28 +321,25 @@ static exprt is_upper_case(const exprt &character) const exprt char_Z = from_integer('Z', character.type()); exprt::operandst upper_case; // Characters between 'A' and 'Z' are upper-case - upper_case.push_back( - and_exprt( - binary_relation_exprt(char_A, ID_le, character), - binary_relation_exprt(character, ID_le, char_Z))); + upper_case.push_back(and_exprt( + binary_relation_exprt(char_A, ID_le, character), + binary_relation_exprt(character, ID_le, char_Z))); // Characters between 0xc0 (latin capital A with grave) // and 0xd6 (latin capital O with diaeresis) are upper-case - upper_case.push_back( - and_exprt( - binary_relation_exprt( - from_integer(0xc0, character.type()), ID_le, character), - binary_relation_exprt( - character, ID_le, from_integer(0xd6, character.type())))); + upper_case.push_back(and_exprt( + binary_relation_exprt( + from_integer(0xc0, character.type()), ID_le, character), + binary_relation_exprt( + character, ID_le, from_integer(0xd6, character.type())))); // Characters between 0xd8 (latin capital O with stroke) // and 0xde (latin capital thorn) are upper-case - upper_case.push_back( - and_exprt( - binary_relation_exprt( - from_integer(0xd8, character.type()), ID_le, character), - binary_relation_exprt( - character, ID_le, from_integer(0xde, character.type())))); + upper_case.push_back(and_exprt( + binary_relation_exprt( + from_integer(0xd8, character.type()), ID_le, character), + binary_relation_exprt( + character, ID_le, from_integer(0xde, character.type())))); return disjunction(upper_case); } diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/strings/string_builtin_function.h similarity index 100% rename from src/solvers/refinement/string_builtin_function.h rename to src/solvers/strings/string_builtin_function.h index addbebadccf..bd7d1696580 100644 --- a/src/solvers/refinement/string_builtin_function.h +++ b/src/solvers/strings/string_builtin_function.h @@ -4,10 +4,10 @@ #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H #define CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H -#include +#include "string_constraint_generator.h" #include #include -#include "string_constraint_generator.h" +#include class array_poolt; struct string_constraintst; diff --git a/src/solvers/refinement/string_constraint.cpp b/src/solvers/strings/string_constraint.cpp similarity index 100% rename from src/solvers/refinement/string_constraint.cpp rename to src/solvers/strings/string_constraint.cpp diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/strings/string_constraint.h similarity index 98% rename from src/solvers/refinement/string_constraint.h rename to src/solvers/strings/string_constraint.h index 2b77ca6bb64..45a205ad1a6 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/strings/string_constraint.h @@ -20,9 +20,10 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H -#include "bv_refinement.h" #include "string_refinement_invariant.h" +#include + #include #include #include @@ -160,6 +161,6 @@ struct hash irep_hash()(constraint.s1); } }; -} +} // namespace std #endif diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h similarity index 95% rename from src/solvers/refinement/string_constraint_generator.h rename to src/solvers/strings/string_constraint_generator.h index 3a1d6de2157..a01cc674130 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/strings/string_constraint_generator.h @@ -21,12 +21,12 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H #include -#include -#include -#include +#include #include #include -#include +#include +#include +#include /// Generation of fresh symbols of a given type class symbol_generatort final @@ -126,8 +126,8 @@ class string_constraint_generatort final explicit string_constraint_generatort(const namespacet &ns); - std::pair add_axioms_for_function_application( - const function_application_exprt &expr); + std::pair + add_axioms_for_function_application(const function_application_exprt &expr); symbol_generatort fresh_symbol; @@ -148,8 +148,8 @@ class string_constraint_generatort final /// \todo This does not work at the moment because of the way we treat /// string pointers. /// \deprecated Not tested. - std::pair add_axioms_for_intern( - const function_application_exprt &f); + std::pair + add_axioms_for_intern(const function_application_exprt &f); exprt associate_array_to_pointer(const function_application_exprt &f); @@ -265,8 +265,8 @@ std::pair add_axioms_for_is_suffix( std::pair add_axioms_for_length( const function_application_exprt &f, array_poolt &array_pool); -std::pair add_axioms_for_empty_string( - const function_application_exprt &f); +std::pair +add_axioms_for_empty_string(const function_application_exprt &f); std::pair add_axioms_for_copy( symbol_generatort &fresh_symbol, @@ -355,9 +355,8 @@ std::pair add_axioms_for_string_of_int( const exprt &input_int, size_t max_size, const namespacet &ns); -std::pair add_axioms_from_int_hex( - const array_string_exprt &res, - const exprt &i); +std::pair +add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i); std::pair add_axioms_from_int_hex( const function_application_exprt &f, array_poolt &array_pool); @@ -368,15 +367,13 @@ std::pair add_axioms_from_long( std::pair add_axioms_from_bool( const function_application_exprt &f, array_poolt &array_pool); -std::pair add_axioms_from_bool( - const array_string_exprt &res, - const exprt &i); +std::pair +add_axioms_from_bool(const array_string_exprt &res, const exprt &i); std::pair add_axioms_from_char( const function_application_exprt &f, array_poolt &array_pool); -std::pair add_axioms_from_char( - const array_string_exprt &res, - const exprt &i); +std::pair +add_axioms_from_char(const array_string_exprt &res, const exprt &i); std::pair add_axioms_for_index_of( symbol_generatort &fresh_symbol, const array_string_exprt &str, @@ -478,8 +475,8 @@ std::pair add_axioms_for_trim( std::pair add_axioms_for_code_point( const array_string_exprt &res, const exprt &code_point); -std::pair add_axioms_for_char_literal( - const function_application_exprt &f); +std::pair +add_axioms_for_char_literal(const function_application_exprt &f); /// Add axioms corresponding the String.codePointCount java function /// \todo This function is underspecified, we do not compute the exact value diff --git a/src/solvers/refinement/string_constraint_generator_code_points.cpp b/src/solvers/strings/string_constraint_generator_code_points.cpp similarity index 90% rename from src/solvers/refinement/string_constraint_generator_code_points.cpp rename to src/solvers/strings/string_constraint_generator_code_points.cpp index da89d9ae200..8210f7857ff 100644 --- a/src/solvers/refinement/string_constraint_generator_code_points.cpp +++ b/src/solvers/strings/string_constraint_generator_code_points.cpp @@ -10,7 +10,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// \file /// Generates string constraints for Java functions dealing with code points -#include +#include "string_constraint_generator.h" /// add axioms for the conversion of an integer representing a java /// code point to a utf-16 string @@ -23,8 +23,8 @@ std::pair add_axioms_for_code_point( { string_constraintst constraints; const typet &char_type = res.content().type().subtype(); - const typet &type=code_point.type(); - PRECONDITION(type.id()==ID_signedbv); + const typet &type = code_point.type(); + PRECONDITION(type.id() == ID_signedbv); // We add axioms: // a1 : code_point<0x010000 => |res|=1 @@ -35,10 +35,10 @@ std::pair add_axioms_for_code_point( // For more explenations about this conversion, see: // https://en.wikipedia.org/wiki/UTF-16 - exprt hex010000=from_integer(0x010000, type); - exprt hexD800=from_integer(0xD800, type); - exprt hexDC00=from_integer(0xDC00, type); - exprt hex0400=from_integer(0x0400, type); + exprt hex010000 = from_integer(0x010000, type); + exprt hexD800 = from_integer(0xD800, type); + exprt hexDC00 = from_integer(0xDC00, type); + exprt hex0400 = from_integer(0x0400, type); binary_relation_exprt small(code_point, ID_lt, hex010000); implies_exprt a1(small, length_eq(res, 1)); @@ -104,9 +104,9 @@ static exprt is_low_surrogate(const exprt &chr) /// \return an integer expression of type return_type exprt pair_value(exprt char1, exprt char2, typet return_type) { - exprt hex010000=from_integer(0x010000, return_type); - exprt hex0800=from_integer(0x0800, return_type); - exprt hex0400=from_integer(0x0400, return_type); + exprt hex010000 = from_integer(0x010000, return_type); + exprt hex0800 = from_integer(0x0800, return_type); + exprt hex0400 = from_integer(0x0400, return_type); mult_exprt m1(mod_exprt(char1, hex0800), hex0400); mod_exprt m2(char2, hex0400); return plus_exprt(hex010000, plus_exprt(m1, m2)); @@ -125,14 +125,14 @@ std::pair add_axioms_for_code_point_at( { string_constraintst constraints; const typet &return_type = f.type(); - PRECONDITION(return_type.id()==ID_signedbv); + PRECONDITION(return_type.id() == ID_signedbv); PRECONDITION(f.arguments().size() == 2); const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]); const exprt &pos = f.arguments()[1]; const symbol_exprt result = fresh_symbol("char", return_type); const exprt index1 = from_integer(1, str.length().type()); - const exprt &char1=str[pos]; + const exprt &char1 = str[pos]; const exprt &char2 = str[plus_exprt(pos, index1)]; const typecast_exprt char1_as_int(char1, return_type); const typecast_exprt char2_as_int(char2, return_type); @@ -156,17 +156,17 @@ std::pair add_axioms_for_code_point_before( const function_application_exprt &f, array_poolt &array_pool) { - const function_application_exprt::argumentst &args=f.arguments(); - PRECONDITION(args.size()==2); - typet return_type=f.type(); - PRECONDITION(return_type.id()==ID_signedbv); - symbol_exprt result=fresh_symbol("char", return_type); + const function_application_exprt::argumentst &args = f.arguments(); + PRECONDITION(args.size() == 2); + typet return_type = f.type(); + PRECONDITION(return_type.id() == ID_signedbv); + symbol_exprt result = fresh_symbol("char", return_type); array_string_exprt str = get_string_expr(array_pool, args[0]); string_constraintst constraints; - const exprt &char1= + const exprt &char1 = str[minus_exprt(args[1], from_integer(2, str.length().type()))]; - const exprt &char2= + const exprt &char2 = str[minus_exprt(args[1], from_integer(1, str.length().type()))]; const typecast_exprt char1_as_int(char1, return_type); const typecast_exprt char2_as_int(char2, return_type); @@ -199,7 +199,7 @@ std::pair add_axioms_for_code_point_count( const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]); const exprt &begin = f.arguments()[1]; const exprt &end = f.arguments()[2]; - const typet &return_type=f.type(); + const typet &return_type = f.type(); const symbol_exprt result = fresh_symbol("code_point_count", return_type); const minus_exprt length(end, begin); const div_exprt minimum(length, from_integer(2, length.type())); @@ -226,7 +226,7 @@ std::pair add_axioms_for_offset_by_code_point( string_constraintst constraints; const exprt &index = f.arguments()[1]; const exprt &offset = f.arguments()[2]; - const typet &return_type=f.type(); + const typet &return_type = f.type(); const symbol_exprt result = fresh_symbol("offset_by_code_point", return_type); const exprt minimum = plus_exprt(index, offset); @@ -238,4 +238,3 @@ std::pair add_axioms_for_offset_by_code_point( return {result, constraints}; } - diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/strings/string_constraint_generator_comparison.cpp similarity index 96% rename from src/solvers/refinement/string_constraint_generator_comparison.cpp rename to src/solvers/strings/string_constraint_generator_comparison.cpp index 7c956342ffb..4b32028894b 100644 --- a/src/solvers/refinement/string_constraint_generator_comparison.cpp +++ b/src/solvers/strings/string_constraint_generator_comparison.cpp @@ -11,7 +11,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// Generates string constraints for function comparing strings, such as: /// equals, equalsIgnoreCase, compareTo, hashCode, intern -#include +#include "string_constraint_generator.h" + #include /// Equality of the content of two strings @@ -33,7 +34,7 @@ std::pair add_axioms_for_equals( const function_application_exprt &f, array_poolt &pool) { - PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool); + PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool); PRECONDITION(f.arguments().size() == 2); string_constraintst constraints; @@ -42,7 +43,7 @@ std::pair add_axioms_for_equals( symbol_exprt eq = fresh_symbol("equal"); typecast_exprt tc_eq(eq, f.type()); - typet index_type=s1.length().type(); + typet index_type = s1.length().type(); // Axiom 1. constraints.existential.push_back( @@ -134,7 +135,7 @@ std::pair add_axioms_for_equals_ignore_case( const function_application_exprt &f, array_poolt &pool) { - PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool); + PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool); PRECONDITION(f.arguments().size() == 2); string_constraintst constraints; const symbol_exprt eq = fresh_symbol("equal_ignore_case"); @@ -196,7 +197,7 @@ string_constraint_generatort::add_axioms_for_hash_code( const typet &return_type = f.type(); const typet &index_type = str.length().type(); - auto pair=hash_code_of_string.insert( + auto pair = hash_code_of_string.insert( std::make_pair(str, fresh_symbol("hash", return_type))); const exprt hash = pair.first->second; @@ -242,7 +243,7 @@ std::pair add_axioms_for_compare_to( array_poolt &pool) { PRECONDITION(f.arguments().size() == 2); - const typet &return_type=f.type(); + const typet &return_type = f.type(); PRECONDITION(return_type.id() == ID_signedbv); string_constraintst constraints; const array_string_exprt &s1 = get_string_expr(pool, f.arguments()[0]); @@ -311,10 +312,10 @@ string_constraint_generatort::add_axioms_for_intern( string_constraintst intern_constraints; const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]); // For now we only enforce content equality and not pointer equality - const typet &return_type=f.type(); + const typet &return_type = f.type(); const typet index_type = str.length().type(); - auto pair=intern_of_string.insert( + auto pair = intern_of_string.insert( std::make_pair(str, fresh_symbol("pool", return_type))); const symbol_exprt intern = pair.first->second; @@ -330,7 +331,7 @@ string_constraint_generatort::add_axioms_for_intern( // WARNING: the specification may be incomplete or incorrect for(auto it : intern_of_string) - if(it.second!=str) + if(it.second != str) { symbol_exprt i = fresh_symbol("index_intern", index_type); intern_constraints.existential.push_back(or_exprt( diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/strings/string_constraint_generator_concat.cpp similarity index 98% rename from src/solvers/refinement/string_constraint_generator_concat.cpp rename to src/solvers/strings/string_constraint_generator_concat.cpp index 6b5465b0daa..185e1c733e2 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/strings/string_constraint_generator_concat.cpp @@ -11,7 +11,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// Generates string constraints for functions adding content add the end of /// strings -#include +#include "string_constraint_generator.h" /// Add axioms enforcing that `res` is the concatenation of `s1` with /// the substring of `s2` starting at index `start_index'` and ending @@ -129,7 +129,7 @@ std::pair add_axioms_for_concat( const array_string_exprt &s1, const array_string_exprt &s2) { - exprt index_zero=from_integer(0, s2.length().type()); + exprt index_zero = from_integer(0, s2.length().type()); return add_axioms_for_concat_substr( fresh_symbol, res, s1, s2, index_zero, s2.length()); } diff --git a/src/solvers/refinement/string_constraint_generator_constants.cpp b/src/solvers/strings/string_constraint_generator_constants.cpp similarity index 92% rename from src/solvers/refinement/string_constraint_generator_constants.cpp rename to src/solvers/strings/string_constraint_generator_constants.cpp index cd1ca773f21..3347264e7ab 100644 --- a/src/solvers/refinement/string_constraint_generator_constants.cpp +++ b/src/solvers/strings/string_constraint_generator_constants.cpp @@ -9,7 +9,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// \file /// Generates string constraints for constant strings -#include +#include "string_constraint_generator.h" #include #include @@ -28,7 +28,7 @@ std::pair add_axioms_for_constant( string_constraintst constraints; const typet &index_type = res.length().type(); const typet &char_type = res.content().type().subtype(); - std::string c_str=id2string(sval); + std::string c_str = id2string(sval); std::wstring str; /// \todo We should have a special treatment for java strings when the @@ -38,9 +38,9 @@ std::pair add_axioms_for_constant( str=utf8_to_utf16_little_endian(c_str); else #endif - str=widen(c_str); + str = widen(c_str); - for(std::size_t i=0; i add_axioms_for_constant( /// \param f: function application with arguments integer `length` and character /// pointer `ptr`. /// \return integer expression equal to zero -std::pair add_axioms_for_empty_string( - const function_application_exprt &f) +std::pair +add_axioms_for_empty_string(const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 2); string_constraintst constraints; @@ -115,7 +115,7 @@ std::pair add_axioms_from_literal( const function_application_exprt &f, array_poolt &array_pool) { - const function_application_exprt::argumentst &args=f.arguments(); + const function_application_exprt::argumentst &args = f.arguments(); PRECONDITION(args.size() == 3); // Bad args to string literal? const array_string_exprt res = char_array_of_pointer(array_pool, args[1], args[0]); diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/strings/string_constraint_generator_float.cpp similarity index 80% rename from src/solvers/refinement/string_constraint_generator_float.cpp rename to src/solvers/strings/string_constraint_generator_float.cpp index 4127a655bf1..e84bc29638e 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/strings/string_constraint_generator_float.cpp @@ -15,7 +15,6 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include "string_constraint_generator.h" - /// Gets the unbiased exponent in a floating-point bit-vector /// /// \todo Refactor with float_bv.cpp float_utils.h @@ -24,8 +23,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// \return A new 32 bit integer expression representing the exponent. /// Note that 32 bits are sufficient for the exponent even /// in octuple precision. -exprt get_exponent( - const exprt &src, const ieee_float_spect &spec) +exprt get_exponent(const exprt &src, const ieee_float_spect &spec) { const extractbits_exprt exp_bits( src, spec.f + spec.e - 1, spec.f, unsignedbv_typet(spec.e)); @@ -43,7 +41,7 @@ exprt get_exponent( /// \return An unsigned value representing the fractional part. exprt get_fraction(const exprt &src, const ieee_float_spect &spec) { - return extractbits_exprt(src, spec.f-1, 0, unsignedbv_typet(spec.f)); + return extractbits_exprt(src, spec.f - 1, 0, unsignedbv_typet(spec.f)); } /// Gets the significand as a java integer, looking for the hidden bit. @@ -57,14 +55,16 @@ exprt get_fraction(const exprt &src, const ieee_float_spect &spec) /// \return An integer expression of the given type representing the /// significand. exprt get_significand( - const exprt &src, const ieee_float_spect &spec, const typet &type) + const exprt &src, + const ieee_float_spect &spec, + const typet &type) { - PRECONDITION(type.id()==ID_unsignedbv); - PRECONDITION(to_unsignedbv_type(type).get_width()>spec.f); + PRECONDITION(type.id() == ID_unsignedbv); + PRECONDITION(to_unsignedbv_type(type).get_width() > spec.f); typecast_exprt fraction(get_fraction(src, spec), type); - exprt exponent=get_exponent(src, spec); + exprt exponent = get_exponent(src, spec); equal_exprt all_zeros(exponent, from_integer(0, exponent.type())); - exprt hidden_bit=from_integer((1 << spec.f), type); + exprt hidden_bit = from_integer((1 << spec.f), type); bitor_exprt with_hidden_bit(fraction, hidden_bit); return if_exprt(all_zeros, fraction, with_hidden_bit); } @@ -76,9 +76,9 @@ exprt get_significand( exprt constant_float(const double f, const ieee_float_spect &float_spec) { ieee_floatt fl(float_spec); - if(float_spec==ieee_float_spect::single_precision()) + if(float_spec == ieee_float_spect::single_precision()) fl.from_float(f); - else if(float_spec==ieee_float_spect::double_precision()) + else if(float_spec == ieee_float_spect::double_precision()) fl.from_double(f); else UNREACHABLE; @@ -90,7 +90,8 @@ exprt constant_float(const double f, const ieee_float_spect &float_spec) /// \return expression representing a 32 bit integer exprt round_expr_to_zero(const exprt &f) { - exprt rounding=from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32)); + exprt rounding = + from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32)); return floatbv_typecast_exprt(f, rounding, signedbv_typet(32)); } @@ -101,8 +102,8 @@ exprt round_expr_to_zero(const exprt &f) /// \return An expression representing floating point multiplication. exprt floatbv_mult(const exprt &f, const exprt &g) { - PRECONDITION(f.type()==g.type()); - ieee_floatt::rounding_modet rounding=ieee_floatt::ROUND_TO_EVEN; + PRECONDITION(f.type() == g.type()); + ieee_floatt::rounding_modet rounding = ieee_floatt::ROUND_TO_EVEN; exprt mult(ID_floatbv_mult, f.type()); mult.copy_to_operands(f); mult.copy_to_operands(g); @@ -118,7 +119,8 @@ exprt floatbv_mult(const exprt &f, const exprt &g) /// integer as a float. exprt floatbv_of_int_expr(const exprt &i, const ieee_float_spect &spec) { - exprt rounding=from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32)); + exprt rounding = + from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32)); return floatbv_typecast_exprt(i, rounding, spec.to_type()); } @@ -136,10 +138,11 @@ exprt floatbv_of_int_expr(const exprt &i, const ieee_float_spect &spec) /// \param spec: specification for floating point exprt estimate_decimal_exponent(const exprt &f, const ieee_float_spect &spec) { - exprt log_10_of_2=constant_float(0.30102999566398119521373889472449302, spec); - exprt bin_exp=get_exponent(f, spec); - exprt float_bin_exp=floatbv_of_int_expr(bin_exp, spec); - exprt dec_exp=floatbv_mult(float_bin_exp, log_10_of_2); + exprt log_10_of_2 = + constant_float(0.30102999566398119521373889472449302, spec); + exprt bin_exp = get_exponent(f, spec); + exprt float_bin_exp = floatbv_of_int_expr(bin_exp, spec); + exprt dec_exp = floatbv_mult(float_bin_exp, log_10_of_2); binary_relation_exprt negative_exp(dec_exp, ID_lt, constant_float(0.0, spec)); // Rounding to zero is not correct for negative numbers, so we substract 1. minus_exprt dec_minus_one(dec_exp, constant_float(1.0, spec)); @@ -205,7 +208,7 @@ std::pair add_axioms_for_string_of_float( array_poolt &array_pool, const namespacet &ns) { - const floatbv_typet &type=to_floatbv_type(f.type()); + const floatbv_typet &type = to_floatbv_type(f.type()); const ieee_float_spect float_spec(type); const typet &char_type = res.content().type().subtype(); const typet &index_type = res.length().type(); @@ -257,10 +260,10 @@ std::pair add_axioms_for_fractional_part( const exprt &int_expr, size_t max_size) { - PRECONDITION(int_expr.type().id()==ID_signedbv); - PRECONDITION(max_size>=2); + PRECONDITION(int_expr.type().id() == ID_signedbv); + PRECONDITION(max_size >= 2); string_constraintst constraints; - const typet &type=int_expr.type(); + const typet &type = int_expr.type(); const typet &char_type = res.content().type().subtype(); const typet &index_type = res.length().type(); const exprt ten = from_integer(10, type); @@ -283,9 +286,9 @@ std::pair add_axioms_for_fractional_part( exprt::operandst digit_constraints; digit_constraints.push_back(starts_with_dot); - exprt sum=from_integer(0, type); + exprt sum = from_integer(0, type); - for(size_t j=1; j add_axioms_for_fractional_part( after_end, from_integer(0, type), typecast_exprt(minus_exprt(res[j], zero_char), type)); - sum=plus_exprt(ten_sum, to_add); + sum = plus_exprt(ten_sum, to_add); and_exprt is_number( binary_relation_exprt(res[j], ID_ge, zero_char), @@ -305,16 +308,16 @@ std::pair add_axioms_for_fractional_part( digit_constraints.push_back(is_number); // There are no trailing zeros except for ".0" (i.e j=2) - if(j>1) + if(j > 1) { not_exprt no_trailing_zero(and_exprt( - equal_exprt(res.length(), from_integer(j+1, res.length().type())), - equal_exprt(res[j], zero_char))); + equal_exprt(res.length(), from_integer(j + 1, res.length().type())), + equal_exprt(res[j], zero_char))); digit_constraints.push_back(no_trailing_zero); } } - exprt a2=conjunction(digit_constraints); + exprt a2 = conjunction(digit_constraints); constraints.existential.push_back(a2); equal_exprt a3(int_expr, sum); @@ -356,7 +359,7 @@ std::pair add_axioms_from_float_scientific_notation( const typet &char_type = res.content().type().subtype(); // This is used for rounding float to integers. - exprt round_to_zero_expr=from_integer(ieee_floatt::ROUND_TO_ZERO, int_type); + exprt round_to_zero_expr = from_integer(ieee_floatt::ROUND_TO_ZERO, int_type); // `bin_exponent` is $e$ in the formulas exprt bin_exponent = get_exponent(float_expr, float_spec); @@ -369,7 +372,7 @@ std::pair add_axioms_from_float_scientific_notation( // `bin_significand` represents $m$ and is obtained // by multiplying `binary_significand_as_int` by // 1/0x800000 = 2^-23 = 1.1920928955078125 * 10^-7 - exprt bin_significand=floatbv_mult( + exprt bin_significand = floatbv_mult( floatbv_typecast_exprt(bin_significand_int, round_to_zero_expr, float_type), constant_float(1.1920928955078125e-7, float_spec)); @@ -380,45 +383,45 @@ std::pair add_axioms_from_float_scientific_notation( // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[0,128] std::vector two_power_e_over_ten_power_d_table( - { 1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28, 2.56, - 5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768, 6.5536, - 1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861, 1.67772, - 3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748, 4.29497, - 8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756, 1.09951, - 2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737, 2.81475, - 5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288, 7.20576, - 1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337, 1.84467, - 3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118, 4.72237, - 9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463, 1.20893, - 2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743, 3.09485, - 6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141, 7.92282, - 1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412, 2.02824, - 4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615, 5.1923, - 1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614, 1.32923, - 2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141}); + {1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28, + 2.56, 5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768, + 6.5536, 1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861, + 1.67772, 3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748, + 4.29497, 8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756, + 1.09951, 2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737, + 2.81475, 5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288, + 7.20576, 1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337, + 1.84467, 3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118, + 4.72237, 9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463, + 1.20893, 2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743, + 3.09485, 6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141, + 7.92282, 1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412, + 2.02824, 4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615, + 5.1923, 1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614, + 1.32923, 2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141}); // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[-128,-1] std::vector two_power_e_over_ten_power_d_table_negatives( - { 2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158, - 7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965, - 1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519, - 4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089, - 1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559, - 3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590, - 8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879, - 2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051, - 5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889, - 1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636, - 3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747, - 9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415, - 2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023, - 5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939, - 1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313, - 3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5}); + {2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158, + 7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965, + 1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519, + 4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089, + 1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559, + 3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590, + 8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879, + 2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051, + 5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889, + 1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636, + 3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747, + 9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415, + 2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023, + 5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939, + 1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313, + 3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5}); // bias_table used to find the bias factor - exprt conversion_factor_table_size=from_integer( - two_power_e_over_ten_power_d_table_negatives.size()+ + exprt conversion_factor_table_size = from_integer( + two_power_e_over_ten_power_d_table_negatives.size() + two_power_e_over_ten_power_d_table.size(), int_type); array_exprt conversion_factor_table( @@ -438,8 +441,8 @@ std::pair add_axioms_from_float_scientific_notation( conversion_factor_table, shifted_index, float_type); // `dec_significand` is $n = m * bias_factor$ - exprt dec_significand=floatbv_mult(conversion_factor, bin_significand); - exprt dec_significand_int=round_expr_to_zero(dec_significand); + exprt dec_significand = floatbv_mult(conversion_factor, bin_significand); + exprt dec_significand_int = round_expr_to_zero(dec_significand); // `dec_exponent` is $d$ in the formulas // it is obtained from the approximation, checking whether it is not too small @@ -451,11 +454,11 @@ std::pair add_axioms_from_float_scientific_notation( dec_exponent_estimate); // `dec_significand` is divided by 10 if it exceeds 10 - dec_significand=if_exprt( + dec_significand = if_exprt( estimate_too_small, floatbv_mult(dec_significand, constant_float(0.1, float_spec)), dec_significand); - dec_significand_int=round_expr_to_zero(dec_significand); + dec_significand_int = round_expr_to_zero(dec_significand); array_string_exprt string_expr_integer_part = array_pool.fresh_string(index_type, char_type); auto result1 = add_axioms_for_string_of_int( @@ -464,13 +467,13 @@ std::pair add_axioms_from_float_scientific_notation( dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec)); // shifted_float is floor(float_expr * 1e5) - exprt shifting=constant_float(1e5, float_spec); - exprt shifted_float= + exprt shifting = constant_float(1e5, float_spec); + exprt shifted_float = round_expr_to_zero(floatbv_mult(fractional_part, shifting)); // Numbers with greater or equal value to the following, should use // the exponent notation. - exprt max_non_exponent_notation=from_integer(100000, shifted_float.type()); + exprt max_non_exponent_notation = from_integer(100000, shifted_float.type()); // fractional_part_shifted is floor(float_expr * 100000) % 100000 const mod_exprt fractional_part_shifted( diff --git a/src/solvers/refinement/string_constraint_generator_format.cpp b/src/solvers/strings/string_constraint_generator_format.cpp similarity index 83% rename from src/solvers/refinement/string_constraint_generator_format.cpp rename to src/solvers/strings/string_constraint_generator_format.cpp index c8eb4f44279..6e96d974074 100644 --- a/src/solvers/refinement/string_constraint_generator_format.cpp +++ b/src/solvers/strings/string_constraint_generator_format.cpp @@ -12,8 +12,8 @@ Date: May 2017 /// Generates string constraints for the Java format function #include -#include #include +#include #include #include @@ -27,35 +27,35 @@ class format_specifiert { public: // Constants describing the meaning of characters in format specifiers. - static const char DECIMAL_INTEGER ='d'; - static const char OCTAL_INTEGER ='o'; - static const char HEXADECIMAL_INTEGER ='x'; - static const char HEXADECIMAL_INTEGER_UPPER='X'; - static const char SCIENTIFIC ='e'; - static const char SCIENTIFIC_UPPER ='E'; - static const char GENERAL ='g'; - static const char GENERAL_UPPER ='G'; - static const char DECIMAL_FLOAT ='f'; - static const char HEXADECIMAL_FLOAT ='a'; - static const char HEXADECIMAL_FLOAT_UPPER ='A'; - static const char CHARACTER ='c'; - static const char CHARACTER_UPPER ='C'; - static const char DATE_TIME ='t'; - static const char DATE_TIME_UPPER ='T'; - static const char BOOLEAN ='b'; - static const char BOOLEAN_UPPER ='B'; - static const char STRING ='s'; - static const char STRING_UPPER ='S'; - static const char HASHCODE ='h'; - static const char HASHCODE_UPPER ='H'; - static const char LINE_SEPARATOR ='n'; - static const char PERCENT_SIGN ='%'; - - int index=-1; + static const char DECIMAL_INTEGER = 'd'; + static const char OCTAL_INTEGER = 'o'; + static const char HEXADECIMAL_INTEGER = 'x'; + static const char HEXADECIMAL_INTEGER_UPPER = 'X'; + static const char SCIENTIFIC = 'e'; + static const char SCIENTIFIC_UPPER = 'E'; + static const char GENERAL = 'g'; + static const char GENERAL_UPPER = 'G'; + static const char DECIMAL_FLOAT = 'f'; + static const char HEXADECIMAL_FLOAT = 'a'; + static const char HEXADECIMAL_FLOAT_UPPER = 'A'; + static const char CHARACTER = 'c'; + static const char CHARACTER_UPPER = 'C'; + static const char DATE_TIME = 't'; + static const char DATE_TIME_UPPER = 'T'; + static const char BOOLEAN = 'b'; + static const char BOOLEAN_UPPER = 'B'; + static const char STRING = 's'; + static const char STRING_UPPER = 'S'; + static const char HASHCODE = 'h'; + static const char HASHCODE_UPPER = 'H'; + static const char LINE_SEPARATOR = 'n'; + static const char PERCENT_SIGN = '%'; + + int index = -1; std::string flag; int width; int precision; - bool dt=false; + bool dt = false; char conversion; format_specifiert( @@ -64,23 +64,28 @@ class format_specifiert int _width, int _precision, bool _dt, - char c): - index(_index), + char c) + : index(_index), flag(_flag), width(_width), precision(_precision), dt(_dt), conversion(c) - { } + { + } }; // Format text represent a constant part of a format string. class format_textt { public: - explicit format_textt(std::string _content): content(_content) { } + explicit format_textt(std::string _content) : content(_content) + { + } - format_textt(const format_textt &fs): content(fs.content) { } + format_textt(const format_textt &fs) : content(fs.content) + { + } std::string get_content() const { @@ -95,13 +100,17 @@ class format_textt class format_elementt { public: - typedef enum {SPECIFIER, TEXT} format_typet; + typedef enum + { + SPECIFIER, + TEXT + } format_typet; - explicit format_elementt(format_typet _type): type(_type), fstring("") + explicit format_elementt(format_typet _type) : type(_type), fstring("") { } - explicit format_elementt(std::string s): type(TEXT), fstring(s) + explicit format_elementt(std::string s) : type(TEXT), fstring(s) { } @@ -112,12 +121,12 @@ class format_elementt bool is_format_specifier() const { - return type==SPECIFIER; + return type == SPECIFIER; } bool is_format_text() const { - return type==TEXT; + return type == TEXT; } format_specifiert get_format_specifier() const @@ -184,19 +193,19 @@ static bool check_format_string(std::string s) /// conversion type. static format_specifiert format_specifier_of_match(std::smatch &m) { - int index=m[1].str().empty()?-1:std::stoi(m[1].str()); - std::string flag=m[2].str().empty()?"":m[2].str(); - int width=m[3].str().empty()?-1:std::stoi(m[3].str()); - int precision=m[4].str().empty()?-1:std::stoi(m[4].str()); - std::string tT=m[5].str(); - - bool dt=(tT!=""); - if(tT=="T") + int index = m[1].str().empty() ? -1 : std::stoi(m[1].str()); + std::string flag = m[2].str().empty() ? "" : m[2].str(); + int width = m[3].str().empty() ? -1 : std::stoi(m[3].str()); + int precision = m[4].str().empty() ? -1 : std::stoi(m[4].str()); + std::string tT = m[5].str(); + + bool dt = (tT != ""); + if(tT == "T") flag.push_back(format_specifiert::DATE_TIME_UPPER); INVARIANT( - m[6].str().length()==1, "format conversion should be one character"); - char conversion=m[6].str()[0]; + m[6].str().length() == 1, "format conversion should be one character"); + char conversion = m[6].str()[0]; return format_specifiert(index, flag, width, precision, dt, conversion); } @@ -208,7 +217,7 @@ static format_specifiert format_specifier_of_match(std::smatch &m) /// \return A vector of format_elementt. static std::vector parse_format_string(std::string s) { - std::string format_specifier= + std::string format_specifier = "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])"; std::regex regex(format_specifier); std::vector al; @@ -216,14 +225,14 @@ static std::vector parse_format_string(std::string s) while(std::regex_search(s, match, regex)) { - if(match.position()!=0) + if(match.position() != 0) { - std::string pre_match=s.substr(0, match.position()); + std::string pre_match = s.substr(0, match.position()); al.emplace_back(pre_match); } al.emplace_back(format_specifier_of_match(match)); - s=match.suffix(); + s = match.suffix(); } al.emplace_back(s); @@ -234,11 +243,11 @@ static std::vector parse_format_string(std::string s) /// \param expr: a structured expression /// \param component_name: name of the desired component /// \return Expression in the component of `expr` named `component_name`. -static exprt get_component_in_struct( - const struct_exprt &expr, irep_idt component_name) +static exprt +get_component_in_struct(const struct_exprt &expr, irep_idt component_name) { - const struct_typet &type=to_struct_type(expr.type()); - std::size_t number=type.component_number(component_name); + const struct_typet &type = to_struct_type(expr.type()); + std::size_t number = type.component_number(component_name); return expr.operands()[number]; } @@ -331,7 +340,7 @@ add_axioms_for_format_specifier( case format_specifiert::HASHCODE_UPPER: { format_specifiert fs_lower = fs; - fs_lower.conversion=tolower(fs.conversion); + fs_lower.conversion = tolower(fs.conversion); auto format_specifier_result = add_axioms_for_format_specifier( fresh_symbol, fs_lower, @@ -390,9 +399,9 @@ std::pair add_axioms_for_format( const namespacet &ns) { string_constraintst constraints; - const std::vector format_strings=parse_format_string(s); + const std::vector format_strings = parse_format_string(s); std::vector intermediary_strings; - std::size_t arg_count=0; + std::size_t arg_count = 0; const typet &char_type = res.content().type().subtype(); const typet &index_type = res.length().type(); @@ -400,27 +409,28 @@ std::pair add_axioms_for_format( { if(fe.is_format_specifier()) { - const format_specifiert &fs=fe.get_format_specifier(); - if(fs.conversion!=format_specifiert::PERCENT_SIGN && - fs.conversion!=format_specifiert::LINE_SEPARATOR) + const format_specifiert &fs = fe.get_format_specifier(); + if( + fs.conversion != format_specifiert::PERCENT_SIGN && + fs.conversion != format_specifiert::LINE_SEPARATOR) { exprt arg; - if(fs.index==-1) + if(fs.index == -1) { INVARIANT( - arg_count 0, "index in format should be positive"); INVARIANT( - static_cast(fs.index)<=args.size(), + static_cast(fs.index) <= args.size(), "number of format must match specifiers"); // first argument `args[0]` corresponds to index 1 - arg=to_struct_expr(args[fs.index-1]); + arg = to_struct_expr(args[fs.index - 1]); } auto result = add_axioms_for_format_specifier( @@ -498,7 +508,7 @@ utf16_constant_array_to_java(const array_exprt &arr, std::size_t length) std::wstring out(length, '?'); - for(std::size_t i=0; i(to_constant_expr(arr.operands()[i])); return utf16_native_endian_to_java(out); @@ -534,8 +544,8 @@ std::pair add_axioms_for_format( { const auto length = numeric_cast_v(to_constant_expr(s1.length())); - std::string s=utf16_constant_array_to_java( - to_array_expr(s1.content()), length); + std::string s = + utf16_constant_array_to_java(to_array_expr(s1.content()), length); // List of arguments after s std::vector args(f.arguments().begin() + 3, f.arguments().end()); return add_axioms_for_format( diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/strings/string_constraint_generator_indexof.cpp similarity index 95% rename from src/solvers/refinement/string_constraint_generator_indexof.cpp rename to src/solvers/strings/string_constraint_generator_indexof.cpp index 1fa6c53b4d4..10b46ba5fda 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/strings/string_constraint_generator_indexof.cpp @@ -11,8 +11,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// Generates string constraints for the family of indexOf and lastIndexOf java /// functions -#include -#include +#include "string_constraint_generator.h" +#include "string_refinement_invariant.h" /// Add axioms stating that the returned value is the index within `haystack` /// (`str`) of the first occurrence of `needle` (`c`) starting the search at @@ -42,11 +42,11 @@ std::pair add_axioms_for_index_of( const exprt &from_index) { string_constraintst constraints; - const typet &index_type=str.length().type(); + const typet &index_type = str.length().type(); symbol_exprt index = fresh_symbol("index_of", index_type); symbol_exprt contains = fresh_symbol("contains_in_index_of"); - exprt minus1=from_integer(-1, index_type); + exprt minus1 = from_integer(-1, index_type); and_exprt a1( binary_relation_exprt(index, ID_ge, minus1), binary_relation_exprt(index, ID_lt, str.length())); @@ -115,7 +115,7 @@ std::pair add_axioms_for_index_of_string( const exprt &from_index) { string_constraintst constraints; - const typet &index_type=haystack.length().type(); + const typet &index_type = haystack.length().type(); symbol_exprt offset = fresh_symbol("index_of", index_type); symbol_exprt contains = fresh_symbol("contains_substring"); @@ -128,8 +128,7 @@ std::pair add_axioms_for_index_of_string( constraints.existential.push_back(a1); equal_exprt a2( - not_exprt(contains), - equal_exprt(offset, from_integer(-1, index_type))); + not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type))); constraints.existential.push_back(a2); symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type); @@ -209,7 +208,7 @@ std::pair add_axioms_for_last_index_of_string( const exprt &from_index) { string_constraintst constraints; - const typet &index_type=haystack.length().type(); + const typet &index_type = haystack.length().type(); symbol_exprt offset = fresh_symbol("index_of", index_type); symbol_exprt contains = fresh_symbol("contains_substring"); @@ -223,8 +222,7 @@ std::pair add_axioms_for_last_index_of_string( constraints.existential.push_back(a1); equal_exprt a2( - not_exprt(contains), - equal_exprt(offset, from_integer(-1, index_type))); + not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type))); constraints.existential.push_back(a2); symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type); @@ -293,17 +291,17 @@ std::pair add_axioms_for_index_of( const function_application_exprt &f, array_poolt &array_pool) { - const function_application_exprt::argumentst &args=f.arguments(); + const function_application_exprt::argumentst &args = f.arguments(); PRECONDITION(args.size() == 2 || args.size() == 3); const array_string_exprt str = get_string_expr(array_pool, args[0]); - const exprt &c=args[1]; + const exprt &c = args[1]; const typet &index_type = str.length().type(); const typet &char_type = str.content().type().subtype(); PRECONDITION(f.type() == index_type); const exprt from_index = args.size() == 2 ? from_integer(0, index_type) : args[2]; - if(c.type().id()==ID_unsignedbv || c.type().id()==ID_signedbv) + if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv) { return add_axioms_for_index_of( fresh_symbol, str, typecast_exprt(c, char_type), from_index); @@ -312,7 +310,8 @@ std::pair add_axioms_for_index_of( { INVARIANT( is_refined_string_type(c.type()), - string_refinement_invariantt("c can only be a (un)signedbv or a refined " + string_refinement_invariantt( + "c can only be a (un)signedbv or a refined " "string and the (un)signedbv case is already handled")); array_string_exprt sub = get_string_expr(array_pool, c); return add_axioms_for_index_of_string(fresh_symbol, str, sub, from_index); @@ -417,7 +416,7 @@ std::pair add_axioms_for_last_index_of( const function_application_exprt &f, array_poolt &array_pool) { - const function_application_exprt::argumentst &args=f.arguments(); + const function_application_exprt::argumentst &args = f.arguments(); PRECONDITION(args.size() == 2 || args.size() == 3); const array_string_exprt str = get_string_expr(array_pool, args[0]); const exprt c = args[1]; @@ -427,7 +426,7 @@ std::pair add_axioms_for_last_index_of( const exprt from_index = args.size() == 2 ? str.length() : args[2]; - if(c.type().id()==ID_unsignedbv || c.type().id()==ID_signedbv) + if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv) { return add_axioms_for_last_index_of( fresh_symbol, str, typecast_exprt(c, char_type), from_index); diff --git a/src/solvers/refinement/string_constraint_generator_insert.cpp b/src/solvers/strings/string_constraint_generator_insert.cpp similarity index 98% rename from src/solvers/refinement/string_constraint_generator_insert.cpp rename to src/solvers/strings/string_constraint_generator_insert.cpp index 617911c2de4..be6e2cb3993 100644 --- a/src/solvers/refinement/string_constraint_generator_insert.cpp +++ b/src/solvers/strings/string_constraint_generator_insert.cpp @@ -9,8 +9,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// \file /// Generates string constraints for the family of insert Java functions -#include -#include +#include "string_constraint_generator.h" +#include "string_refinement_invariant.h" + #include /// Add axioms ensuring the result `res` corresponds to `s1` where we @@ -37,7 +38,7 @@ std::pair add_axioms_for_insert( const array_string_exprt &s2, const exprt &offset) { - PRECONDITION(offset.type()==s1.length().type()); + PRECONDITION(offset.type() == s1.length().type()); string_constraintst constraints; const typet &index_type = s1.length().type(); diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp similarity index 87% rename from src/solvers/refinement/string_constraint_generator_main.cpp rename to src/solvers/strings/string_constraint_generator_main.cpp index 02da80879fa..bd6894c62c8 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/strings/string_constraint_generator_main.cpp @@ -17,17 +17,17 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// Li and Indradeep Ghosh, which gives examples of constraints for several /// functions. -#include +#include "string_constraint_generator.h" +#include "string_refinement_invariant.h" #include #include -#include #include +#include #include #include #include -#include string_constraint_generatort::string_constraint_generatort(const namespacet &ns) : array_pool(fresh_symbol), ns(ns) @@ -135,7 +135,7 @@ array_string_exprt array_poolt::make_char_array_for_char_pointer( to_array_string_expr(fresh_symbol(symbol_name, char_array_type)); const auto insert_result = arrays_of_pointers.insert({char_pointer, array_sym}); - return to_array_string_expr(insert_result.first->second); + return to_array_string_expr(insert_result.first->second); } void array_poolt::insert( @@ -371,98 +371,98 @@ string_constraint_generatort::add_axioms_for_function_application( { const irep_idt &id = get_function_name(expr); - if(id==ID_cprover_char_literal_func) + if(id == ID_cprover_char_literal_func) return add_axioms_for_char_literal(expr); - else if(id==ID_cprover_string_length_func) + else if(id == ID_cprover_string_length_func) return add_axioms_for_length(expr, array_pool); - else if(id==ID_cprover_string_equal_func) + else if(id == ID_cprover_string_equal_func) return add_axioms_for_equals(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_equals_ignore_case_func) + else if(id == ID_cprover_string_equals_ignore_case_func) return add_axioms_for_equals_ignore_case(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_is_empty_func) + else if(id == ID_cprover_string_is_empty_func) return add_axioms_for_is_empty(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_char_at_func) + else if(id == ID_cprover_string_char_at_func) return add_axioms_for_char_at(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_is_prefix_func) + else if(id == ID_cprover_string_is_prefix_func) return add_axioms_for_is_prefix(fresh_symbol, expr, false, array_pool); - else if(id==ID_cprover_string_is_suffix_func) + else if(id == ID_cprover_string_is_suffix_func) return add_axioms_for_is_suffix(fresh_symbol, expr, false, array_pool); - else if(id==ID_cprover_string_startswith_func) + else if(id == ID_cprover_string_startswith_func) return add_axioms_for_is_prefix(fresh_symbol, expr, true, array_pool); - else if(id==ID_cprover_string_endswith_func) + else if(id == ID_cprover_string_endswith_func) return add_axioms_for_is_suffix(fresh_symbol, expr, true, array_pool); - else if(id==ID_cprover_string_contains_func) + else if(id == ID_cprover_string_contains_func) return add_axioms_for_contains(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_hash_code_func) + else if(id == ID_cprover_string_hash_code_func) return add_axioms_for_hash_code(expr, array_pool); - else if(id==ID_cprover_string_index_of_func) + else if(id == ID_cprover_string_index_of_func) return add_axioms_for_index_of(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_last_index_of_func) + else if(id == ID_cprover_string_last_index_of_func) return add_axioms_for_last_index_of(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_parse_int_func) + else if(id == ID_cprover_string_parse_int_func) return add_axioms_for_parse_int(fresh_symbol, expr, array_pool, ns); - else if(id==ID_cprover_string_code_point_at_func) + else if(id == ID_cprover_string_code_point_at_func) return add_axioms_for_code_point_at(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_code_point_before_func) + else if(id == ID_cprover_string_code_point_before_func) return add_axioms_for_code_point_before(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_code_point_count_func) + else if(id == ID_cprover_string_code_point_count_func) return add_axioms_for_code_point_count(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_offset_by_code_point_func) + else if(id == ID_cprover_string_offset_by_code_point_func) return add_axioms_for_offset_by_code_point(fresh_symbol, expr); - else if(id==ID_cprover_string_compare_to_func) + else if(id == ID_cprover_string_compare_to_func) return add_axioms_for_compare_to(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_literal_func) + else if(id == ID_cprover_string_literal_func) return add_axioms_from_literal(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_concat_code_point_func) + else if(id == ID_cprover_string_concat_code_point_func) return add_axioms_for_concat_code_point(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_insert_func) + else if(id == ID_cprover_string_insert_func) return add_axioms_for_insert(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_insert_int_func) + else if(id == ID_cprover_string_insert_int_func) return add_axioms_for_insert_int(fresh_symbol, expr, array_pool, ns); - else if(id==ID_cprover_string_insert_long_func) + else if(id == ID_cprover_string_insert_long_func) return add_axioms_for_insert_int(fresh_symbol, expr, array_pool, ns); - else if(id==ID_cprover_string_insert_bool_func) + else if(id == ID_cprover_string_insert_bool_func) return add_axioms_for_insert_bool(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_insert_char_func) + else if(id == ID_cprover_string_insert_char_func) return add_axioms_for_insert_char(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_insert_double_func) + else if(id == ID_cprover_string_insert_double_func) return add_axioms_for_insert_double(fresh_symbol, expr, array_pool, ns); - else if(id==ID_cprover_string_insert_float_func) + else if(id == ID_cprover_string_insert_float_func) return add_axioms_for_insert_float(fresh_symbol, expr, array_pool, ns); - else if(id==ID_cprover_string_substring_func) + else if(id == ID_cprover_string_substring_func) return add_axioms_for_substring(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_trim_func) + else if(id == ID_cprover_string_trim_func) return add_axioms_for_trim(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_empty_string_func) + else if(id == ID_cprover_string_empty_string_func) return add_axioms_for_empty_string(expr); - else if(id==ID_cprover_string_copy_func) + else if(id == ID_cprover_string_copy_func) return add_axioms_for_copy(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_of_int_hex_func) + else if(id == ID_cprover_string_of_int_hex_func) return add_axioms_from_int_hex(expr, array_pool); - else if(id==ID_cprover_string_of_float_func) + else if(id == ID_cprover_string_of_float_func) return add_axioms_for_string_of_float(fresh_symbol, expr, array_pool, ns); - else if(id==ID_cprover_string_of_float_scientific_notation_func) + else if(id == ID_cprover_string_of_float_scientific_notation_func) return add_axioms_from_float_scientific_notation( fresh_symbol, expr, array_pool, ns); - else if(id==ID_cprover_string_of_double_func) + else if(id == ID_cprover_string_of_double_func) return add_axioms_from_double(fresh_symbol, expr, array_pool, ns); - else if(id==ID_cprover_string_of_long_func) + else if(id == ID_cprover_string_of_long_func) return add_axioms_from_long(expr, array_pool, ns); - else if(id==ID_cprover_string_of_bool_func) + else if(id == ID_cprover_string_of_bool_func) return add_axioms_from_bool(expr, array_pool); - else if(id==ID_cprover_string_of_char_func) + else if(id == ID_cprover_string_of_char_func) return add_axioms_from_char(expr, array_pool); - else if(id==ID_cprover_string_set_length_func) + else if(id == ID_cprover_string_set_length_func) return add_axioms_for_set_length(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_delete_func) + else if(id == ID_cprover_string_delete_func) return add_axioms_for_delete(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_delete_char_at_func) + else if(id == ID_cprover_string_delete_char_at_func) return add_axioms_for_delete_char_at(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_replace_func) + else if(id == ID_cprover_string_replace_func) return add_axioms_for_replace(fresh_symbol, expr, array_pool); - else if(id==ID_cprover_string_intern_func) + else if(id == ID_cprover_string_intern_func) return add_axioms_for_intern(expr); - else if(id==ID_cprover_string_format_func) + else if(id == ID_cprover_string_format_func) return add_axioms_for_format(fresh_symbol, expr, array_pool, message, ns); else if(id == ID_cprover_string_constrain_characters_func) return add_axioms_for_constrain_characters(fresh_symbol, expr, array_pool); @@ -470,7 +470,7 @@ string_constraint_generatort::add_axioms_for_function_application( { std::string msg( "string_constraint_generator::function_application: unknown symbol :"); - msg+=id2string(id); + msg += id2string(id); DATA_INVARIANT(false, string_refinement_invariantt(msg)); } UNREACHABLE; @@ -490,7 +490,7 @@ std::pair add_axioms_for_copy( const function_application_exprt &f, array_poolt &array_pool) { - const auto &args=f.arguments(); + const auto &args = f.arguments(); PRECONDITION(args.size() == 3 || args.size() == 5); const array_string_exprt res = char_array_of_pointer(array_pool, args[1], args[0]); @@ -527,23 +527,24 @@ exprt is_positive(const exprt &x) /// add axioms stating that the returned value is equal to the argument /// \param f: function application with one character argument /// \return a new character expression -std::pair add_axioms_for_char_literal( - const function_application_exprt &f) +std::pair +add_axioms_for_char_literal(const function_application_exprt &f) { - const function_application_exprt::argumentst &args=f.arguments(); - PRECONDITION(args.size()==1); // there should be exactly 1 arg to char literal + const function_application_exprt::argumentst &args = f.arguments(); + PRECONDITION( + args.size() == 1); // there should be exactly 1 arg to char literal - const exprt &arg=args[0]; + const exprt &arg = args[0]; // for C programs argument to char literal should be one string constant // of size 1. - if(arg.operands().size()==1 && - arg.op0().operands().size()==1 && - arg.op0().op0().operands().size()==2 && - arg.op0().op0().op0().id()==ID_string_constant) + if( + arg.operands().size() == 1 && arg.op0().operands().size() == 1 && + arg.op0().op0().operands().size() == 2 && + arg.op0().op0().op0().id() == ID_string_constant) { const string_constantt &s = to_string_constant(arg.op0().op0().op0()); const std::string &sval = id2string(s.get_value()); - CHECK_RETURN(sval.size()==1); + CHECK_RETURN(sval.size() == 1); return {from_integer(unsigned(sval[0]), arg.type()), {}}; } else diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/strings/string_constraint_generator_testing.cpp similarity index 93% rename from src/solvers/refinement/string_constraint_generator_testing.cpp rename to src/solvers/strings/string_constraint_generator_testing.cpp index 5310304b374..1c24648070c 100644 --- a/src/solvers/refinement/string_constraint_generator_testing.cpp +++ b/src/solvers/strings/string_constraint_generator_testing.cpp @@ -10,8 +10,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// \file /// Generates string constraints for string functions that return Boolean values -#include -#include +#include "string_constraint_generator.h" +#include "string_refinement_invariant.h" + #include /// Add axioms stating that the returned expression is true exactly when the @@ -102,8 +103,8 @@ std::pair add_axioms_for_is_prefix( bool swap_arguments, array_poolt &array_pool) { - const function_application_exprt::argumentst &args=f.arguments(); - PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool); + const function_application_exprt::argumentst &args = f.arguments(); + PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool); PRECONDITION(args.size() == 2 || args.size() == 3); const array_string_exprt &s0 = get_string_expr(array_pool, args[swap_arguments ? 1u : 0u]); @@ -128,7 +129,7 @@ std::pair add_axioms_for_is_empty( const function_application_exprt &f, array_poolt &array_pool) { - PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool); + PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool); PRECONDITION(f.arguments().size() == 1); // We add axioms: // a1 : is_empty => |s0| = 0 @@ -171,9 +172,9 @@ std::pair add_axioms_for_is_suffix( bool swap_arguments, array_poolt &array_pool) { - const function_application_exprt::argumentst &args=f.arguments(); - PRECONDITION(args.size()==2); // bad args to string issuffix? - PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool); + const function_application_exprt::argumentst &args = f.arguments(); + PRECONDITION(args.size() == 2); // bad args to string issuffix? + PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool); string_constraintst constraints; symbol_exprt issuffix = fresh_symbol("issuffix"); @@ -182,7 +183,7 @@ std::pair add_axioms_for_is_suffix( get_string_expr(array_pool, args[swap_arguments ? 1u : 0u]); const array_string_exprt &s1 = get_string_expr(array_pool, args[swap_arguments ? 0u : 1u]); - const typet &index_type=s0.length().type(); + const typet &index_type = s0.length().type(); implies_exprt a1(issuffix, length_ge(s1, s0.length())); constraints.existential.push_back(a1); @@ -236,7 +237,7 @@ std::pair add_axioms_for_contains( array_poolt &array_pool) { PRECONDITION(f.arguments().size() == 2); - PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool); + PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool); string_constraintst constraints; const array_string_exprt s0 = get_string_expr(array_pool, f.arguments()[0]); const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[1]); @@ -254,8 +255,7 @@ std::pair add_axioms_for_contains( constraints.existential.push_back(a2); implies_exprt a3( - not_exprt(contains), - equal_exprt(startpos, from_integer(-1, index_type))); + not_exprt(contains), equal_exprt(startpos, from_integer(-1, index_type))); constraints.existential.push_back(a3); symbol_exprt qvar = fresh_symbol("QA_contains", index_type); diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/strings/string_constraint_generator_transformation.cpp similarity index 95% rename from src/solvers/refinement/string_constraint_generator_transformation.cpp rename to src/solvers/strings/string_constraint_generator_transformation.cpp index d31f4c8adfa..14fb9fced88 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/strings/string_constraint_generator_transformation.cpp @@ -11,8 +11,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// Generates string constraints for string transformations, that is, functions /// taking one string and returning another -#include -#include +#include "string_constraint_generator.h" +#include "string_refinement_invariant.h" + #include /// Reduce or extend a string to have the given length @@ -96,7 +97,7 @@ std::pair add_axioms_for_substring( const function_application_exprt &f, array_poolt &array_pool) { - const function_application_exprt::argumentst &args=f.arguments(); + const function_application_exprt::argumentst &args = f.arguments(); PRECONDITION(args.size() == 4 || args.size() == 5); const array_string_exprt str = get_string_expr(array_pool, args[2]); const array_string_exprt res = @@ -129,8 +130,8 @@ std::pair add_axioms_for_substring( const exprt &end) { const typet &index_type = str.length().type(); - PRECONDITION(start.type()==index_type); - PRECONDITION(end.type()==index_type); + PRECONDITION(start.type() == index_type); + PRECONDITION(end.type() == index_type); string_constraintst constraints; const exprt start1 = maximum(start, from_integer(0, start.type())); @@ -259,18 +260,17 @@ static optionalt> to_char_pair( exprt expr2, std::function get_string_expr) { - if((expr1.type().id()==ID_unsignedbv - || expr1.type().id()==ID_char) - && (expr2.type().id()==ID_char - || expr2.type().id()==ID_unsignedbv)) + if( + (expr1.type().id() == ID_unsignedbv || expr1.type().id() == ID_char) && + (expr2.type().id() == ID_char || expr2.type().id() == ID_unsignedbv)) return std::make_pair(expr1, expr2); const auto expr1_str = get_string_expr(expr1); const auto expr2_str = get_string_expr(expr2); const auto expr1_length = numeric_cast(expr1_str.length()); const auto expr2_length = numeric_cast(expr2_str.length()); - if(expr1_length && expr2_length && *expr1_length==1 && *expr2_length==1) + if(expr1_length && expr2_length && *expr1_length == 1 && *expr2_length == 1) return std::make_pair(exprt(expr1_str[0]), exprt(expr2_str[0])); - return { }; + return {}; } /// Replace a character by another in a string @@ -310,15 +310,14 @@ std::pair add_axioms_for_replace( return get_string_expr(array_pool, e); })) { - const auto old_char=maybe_chars->first; - const auto new_char=maybe_chars->second; + const auto old_char = maybe_chars->first; + const auto new_char = maybe_chars->second; constraints.existential.push_back(equal_exprt(res.length(), str.length())); symbol_exprt qvar = fresh_symbol("QA_replace", str.length().type()); implies_exprt case1( - equal_exprt(str[qvar], old_char), - equal_exprt(res[qvar], new_char)); + equal_exprt(str[qvar], old_char), equal_exprt(res[qvar], new_char)); implies_exprt case2( not_exprt(equal_exprt(str[qvar], old_char)), equal_exprt(res[qvar], str[qvar])); @@ -345,7 +344,7 @@ std::pair add_axioms_for_delete_char_at( const array_string_exprt res = char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]); const array_string_exprt str = get_string_expr(array_pool, f.arguments()[2]); - exprt index_one=from_integer(1, str.length().type()); + exprt index_one = from_integer(1, str.length().type()); return add_axioms_for_delete( fresh_symbol, res, @@ -379,8 +378,8 @@ std::pair add_axioms_for_delete( const exprt &end, array_poolt &array_pool) { - PRECONDITION(start.type()==str.length().type()); - PRECONDITION(end.type()==str.length().type()); + PRECONDITION(start.type() == str.length().type()); + PRECONDITION(end.type() == str.length().type()); const typet &index_type = str.length().type(); const typet &char_type = str.content().type().subtype(); const array_string_exprt sub1 = diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/strings/string_constraint_generator_valueof.cpp similarity index 85% rename from src/solvers/refinement/string_constraint_generator_valueof.cpp rename to src/solvers/strings/string_constraint_generator_valueof.cpp index a6210e57ea3..d10e33fd441 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/strings/string_constraint_generator_valueof.cpp @@ -11,10 +11,11 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// Generates string constraints for functions generating strings from other /// types, in particular int, long, float, double, char, bool -#include -#include -#include +#include "string_constraint_generator.h" +#include "string_refinement_invariant.h" + #include +#include #include #include @@ -80,12 +81,11 @@ std::pair add_axioms_from_bool( /// \param b: Boolean expression /// \return code 0 on success DEPRECATED("This is Java specific and should be implemented in Java instead") -std::pair add_axioms_from_bool( - const array_string_exprt &res, - const exprt &b) +std::pair +add_axioms_from_bool(const array_string_exprt &res, const exprt &b) { const typet &char_type = res.content().type().subtype(); - PRECONDITION(b.type()==bool_typet() || b.type().id()==ID_c_bool); + PRECONDITION(b.type() == bool_typet() || b.type().id() == ID_c_bool); string_constraintst constraints; typecast_exprt eq(b, bool_typet()); @@ -95,24 +95,24 @@ std::pair add_axioms_from_bool( // a3 : !eq => res = |"false"| // a4 : forall i < |"false"|. !eq => res[i]="false"[i] - std::string str_true="true"; + std::string str_true = "true"; const implies_exprt a1(eq, length_eq(res, str_true.length())); constraints.existential.push_back(a1); - for(std::size_t i=0; i add_axioms_for_string_of_int( size_t max_size, const namespacet &ns) { - const constant_exprt radix=from_integer(10, input_int.type()); + const constant_exprt radix = from_integer(10, input_int.type()); return add_axioms_for_string_of_int_with_radix( res, input_int, radix, max_size, ns); } @@ -158,24 +158,24 @@ std::pair add_axioms_for_string_of_int_with_radix( const namespacet &ns) { PRECONDITION(max_size < std::numeric_limits::max()); - const typet &type=input_int.type(); - PRECONDITION(type.id()==ID_signedbv); + const typet &type = input_int.type(); + PRECONDITION(type.id() == ID_signedbv); /// Most of the time we can evaluate radix as an integer. The value 0 is used /// to indicate when we can't tell what the radix is. const unsigned long radix_ul = to_integer_or_default(radix, 0, ns); - CHECK_RETURN((radix_ul>=2 && radix_ul<=36) || radix_ul==0); + CHECK_RETURN((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0); - if(max_size==0) + if(max_size == 0) { - max_size=max_printed_string_length(type, radix_ul); - CHECK_RETURN(max_size::max()); + max_size = max_printed_string_length(type, radix_ul); + CHECK_RETURN(max_size < std::numeric_limits::max()); } const typet &char_type = res.content().type().subtype(); const typecast_exprt radix_as_char(radix, char_type); const typecast_exprt radix_input_type(radix, type); - const bool strict_formatting=true; + const bool strict_formatting = true; auto result1 = add_axioms_for_correct_number_format( res, radix_as_char, radix_ul, max_size, strict_formatting); @@ -213,35 +213,34 @@ static exprt int_of_hex_char(const exprt &chr) /// \param i: an integer argument /// \return code 0 on success DEPRECATED("use add_axioms_for_string_of_int_with_radix instead") -std::pair add_axioms_from_int_hex( - const array_string_exprt &res, - const exprt &i) +std::pair +add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i) { - const typet &type=i.type(); - PRECONDITION(type.id()==ID_signedbv); + const typet &type = i.type(); + PRECONDITION(type.id() == ID_signedbv); string_constraintst constraints; const typet &index_type = res.length().type(); const typet &char_type = res.content().type().subtype(); - exprt sixteen=from_integer(16, index_type); + exprt sixteen = from_integer(16, index_type); exprt minus_char = from_integer('-', char_type); exprt zero_char = from_integer('0', char_type); exprt nine_char = from_integer('9', char_type); exprt a_char = from_integer('a', char_type); exprt f_char = from_integer('f', char_type); - size_t max_size=8; + size_t max_size = 8; constraints.existential.push_back( and_exprt(length_gt(res, 0), length_le(res, max_size))); - for(size_t size=1; size<=max_size; size++) + for(size_t size = 1; size <= max_size; size++) { - exprt sum=from_integer(0, type); - exprt all_numbers=true_exprt(); - exprt chr=res[0]; + exprt sum = from_integer(0, type); + exprt all_numbers = true_exprt(); + exprt chr = res[0]; - for(size_t j=0; j add_axioms_from_int_hex( and_exprt( binary_relation_exprt(chr, ID_ge, a_char), binary_relation_exprt(chr, ID_le, f_char))); - all_numbers=and_exprt(all_numbers, is_number); + all_numbers = and_exprt(all_numbers, is_number); } const equal_exprt premise = length_eq(res, size); @@ -259,7 +258,7 @@ std::pair add_axioms_from_int_hex( implies_exprt(premise, and_exprt(equal_exprt(i, sum), all_numbers))); // disallow 0s at the beginning - if(size>1) + if(size > 1) constraints.existential.push_back( implies_exprt(premise, not_exprt(equal_exprt(res[0], zero_char)))); } @@ -308,9 +307,8 @@ std::pair add_axioms_from_char( /// \param res: array of characters expression /// \param c: character expression /// \return code 0 on success -std::pair add_axioms_from_char( - const array_string_exprt &res, - const exprt &c) +std::pair +add_axioms_from_char(const array_string_exprt &res, const exprt &c) { string_constraintst constraints; constraints.existential = { @@ -339,10 +337,10 @@ string_constraintst add_axioms_for_correct_number_format( const typet &char_type = str.content().type().subtype(); const typet &index_type = str.length().type(); - const exprt &chr=str[0]; + const exprt &chr = str[0]; const equal_exprt starts_with_minus(chr, from_integer('-', char_type)); const equal_exprt starts_with_plus(chr, from_integer('+', char_type)); - const exprt starts_with_digit= + const exprt starts_with_digit = is_digit_with_radix(chr, strict_formatting, radix_as_char, radix_ul); // |str| > 0 @@ -375,7 +373,7 @@ string_constraintst add_axioms_for_correct_number_format( // 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 // str.length(), and str.length() <= max_size - for(std::size_t index=1; index is_digit_with_radix(str[index], radix) const implies_exprt character_at_index_is_digit( @@ -427,10 +425,10 @@ string_constraintst add_axioms_for_characters_in_integer_string( const typet &char_type = str.content().type().subtype(); const equal_exprt starts_with_minus(str[0], from_integer('-', char_type)); - const constant_exprt zero_expr=from_integer(0, type); + const constant_exprt zero_expr = from_integer(0, type); exprt::operandst digit_constraints; - exprt sum=get_numeric_value_from_character( + exprt sum = get_numeric_value_from_character( str[0], char_type, type, strict_formatting, radix_ul); /// Deal with size==1 case separately. There are axioms from @@ -439,7 +437,7 @@ string_constraintst add_axioms_for_characters_in_integer_string( constraints.existential.push_back( implies_exprt(length_eq(str, 1), equal_exprt(input_int, sum))); - for(size_t size=2; size<=max_string_length; size++) + for(size_t size = 2; size <= max_string_length; size++) { // sum_0 := numeric value of res[0] (which is 0 if res[0] is '-') // For each 1<=j=max_string_length-2 || radix_ul==0) + if(size - 1 >= max_string_length - 2 || radix_ul == 0) { const and_exprt no_overflow( equal_exprt(sum, div_exprt(radix_sum, radix)), binary_relation_exprt(new_sum, ID_ge, radix_sum)); digit_constraints.push_back(no_overflow); } - sum=new_sum; + sum = new_sum; const equal_exprt premise = length_eq(str, size); @@ -512,24 +510,26 @@ std::pair add_axioms_for_parse_int( array_poolt &array_pool, const namespacet &ns) { - PRECONDITION(f.arguments().size()==1 || f.arguments().size()==2); + PRECONDITION(f.arguments().size() == 1 || f.arguments().size() == 2); const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]); - const typet &type=f.type(); - PRECONDITION(type.id()==ID_signedbv); - const exprt radix=f.arguments().size()==1? - static_cast(from_integer(10, type)): - static_cast(typecast_exprt(f.arguments()[1], type)); + const typet &type = f.type(); + PRECONDITION(type.id() == ID_signedbv); + const exprt radix = + f.arguments().size() == 1 + ? static_cast(from_integer(10, type)) + : static_cast(typecast_exprt(f.arguments()[1], type)); // Most of the time we can evaluate radix as an integer. The value 0 is used // to indicate when we can't tell what the radix is. const unsigned long radix_ul = to_integer_or_default(radix, 0, ns); - PRECONDITION((radix_ul>=2 && radix_ul<=36) || radix_ul==0); + PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0); - const symbol_exprt input_int=fresh_symbol("parsed_int", type); + const symbol_exprt input_int = fresh_symbol("parsed_int", type); const typet &char_type = str.content().type().subtype(); const typecast_exprt radix_as_char(radix, char_type); - const bool strict_formatting=false; + const bool strict_formatting = false; - const std::size_t max_string_length=max_printed_string_length(type, radix_ul); + const std::size_t max_string_length = + max_printed_string_length(type, radix_ul); /// \todo We should throw an exception when constraints added in /// add_axioms_for_correct_number_format do not hold. @@ -565,24 +565,23 @@ exprt is_digit_with_radix( const exprt &radix_as_char, const unsigned long radix_ul) { - PRECONDITION((radix_ul>=2 && radix_ul<=36) || radix_ul==0); - const typet &char_type=chr.type(); - const exprt zero_char=from_integer('0', char_type); + PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0); + const typet &char_type = chr.type(); + const exprt zero_char = from_integer('0', char_type); const and_exprt is_digit_when_radix_le_10( binary_relation_exprt(chr, ID_ge, zero_char), - binary_relation_exprt( - chr, ID_lt, plus_exprt(zero_char, radix_as_char))); + binary_relation_exprt(chr, ID_lt, plus_exprt(zero_char, radix_as_char))); - if(radix_ul<=10 && radix_ul!=0) + if(radix_ul <= 10 && radix_ul != 0) { return is_digit_when_radix_le_10; } else { - const exprt nine_char=from_integer('9', char_type); - const exprt a_char=from_integer('a', char_type); - const constant_exprt ten_char_type=from_integer(10, char_type); + const exprt nine_char = from_integer('9', char_type); + const exprt a_char = from_integer('a', char_type); + const constant_exprt ten_char_type = from_integer(10, char_type); const minus_exprt radix_minus_ten(radix_as_char, ten_char_type); @@ -597,15 +596,14 @@ exprt is_digit_with_radix( if(!strict_formatting) { - exprt A_char=from_integer('A', char_type); - is_digit_when_radix_gt_10.copy_to_operands( - and_exprt( - binary_relation_exprt(chr, ID_ge, A_char), - binary_relation_exprt( - chr, ID_lt, plus_exprt(A_char, radix_minus_ten)))); + exprt A_char = from_integer('A', char_type); + is_digit_when_radix_gt_10.copy_to_operands(and_exprt( + binary_relation_exprt(chr, ID_ge, A_char), + binary_relation_exprt( + chr, ID_lt, plus_exprt(A_char, radix_minus_ten)))); } - if(radix_ul==0) + if(radix_ul == 0) { return if_exprt( binary_relation_exprt(radix_as_char, ID_le, ten_char_type), @@ -636,14 +634,14 @@ exprt get_numeric_value_from_character( const bool strict_formatting, const unsigned long radix_ul) { - const constant_exprt zero_char=from_integer('0', char_type); + const constant_exprt zero_char = from_integer('0', char_type); /// There are four cases, which occur in ASCII in the following order: /// '+' and '-', digits, upper case letters, lower case letters const binary_relation_exprt upper_case_lower_case_or_digit( chr, ID_ge, zero_char); - if(radix_ul<=10 && radix_ul!=0) + if(radix_ul <= 10 && radix_ul != 0) { /// return char >= '0' ? (char - '0') : 0 return typecast_exprt( @@ -655,11 +653,11 @@ exprt get_numeric_value_from_character( } else { - const constant_exprt a_char=from_integer('a', char_type); + const constant_exprt a_char = from_integer('a', char_type); const binary_relation_exprt lower_case(chr, ID_ge, a_char); - const constant_exprt A_char=from_integer('A', char_type); + const constant_exprt A_char = from_integer('A', char_type); const binary_relation_exprt upper_case_or_lower_case(chr, ID_ge, A_char); - const constant_exprt ten_int=from_integer(10, char_type); + const constant_exprt ten_int = from_integer(10, char_type); if(strict_formatting) { @@ -705,13 +703,13 @@ exprt get_numeric_value_from_character( /// \return the maximum string length size_t max_printed_string_length(const typet &type, unsigned long radix_ul) { - if(radix_ul==0) + if(radix_ul == 0) { - radix_ul=2; + radix_ul = 2; } - double n_bits=static_cast(to_bitvector_type(type).get_width()); - double radix=static_cast(radix_ul); - bool signed_type=type.id()==ID_signedbv; + double n_bits = static_cast(to_bitvector_type(type).get_width()); + double radix = static_cast(radix_ul); + bool signed_type = type.id() == ID_signedbv; /// We want to calculate max, the maximum number of characters needed to /// represent any value of the given type. /// @@ -730,8 +728,8 @@ size_t max_printed_string_length(const typet &type, unsigned long radix_ul) /// = min{k: k >= n_bits / log_2(radix)} /// = min{k: k >= ceil(n_bits / log_2(radix))} /// = ceil(n_bits / log_2(radix)) - double max=signed_type? - floor(static_cast(n_bits-1)/log2(radix))+2.0: - ceil(static_cast(n_bits)/log2(radix)); + double max = signed_type + ? floor(static_cast(n_bits - 1) / log2(radix)) + 2.0 + : ceil(static_cast(n_bits) / log2(radix)); return static_cast(max); } diff --git a/src/solvers/refinement/string_constraint_instantiation.cpp b/src/solvers/strings/string_constraint_instantiation.cpp similarity index 93% rename from src/solvers/refinement/string_constraint_instantiation.cpp rename to src/solvers/strings/string_constraint_instantiation.cpp index 965611724f4..a12b09b0ba7 100644 --- a/src/solvers/refinement/string_constraint_instantiation.cpp +++ b/src/solvers/strings/string_constraint_instantiation.cpp @@ -9,7 +9,7 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com /// \file /// Defines related function for string constraints. -#include +#include "string_constraint_instantiation.h" /// Instantiates a quantified formula representing `not_contains` by /// substituting the quantifiers and generating axioms. @@ -33,8 +33,8 @@ std::vector instantiate_not_contains( { // We have s0[x+f(x)] and s1[f(x)], so to have i0 indexing s0 and i1 // indexing s1, we need x = i0 - i1 and f(i0 - i1) = f(x) = i1. - const exprt &i0=pair.first; - const exprt &i1=pair.second; + const exprt &i0 = pair.first; + const exprt &i1 = pair.second; const minus_exprt val(i0, i1); const and_exprt universal_bound( binary_relation_exprt(axiom.univ_lower_bound, ID_le, val), diff --git a/src/solvers/refinement/string_constraint_instantiation.h b/src/solvers/strings/string_constraint_instantiation.h similarity index 87% rename from src/solvers/refinement/string_constraint_instantiation.h rename to src/solvers/strings/string_constraint_instantiation.h index c7c96375350..23971cfd4a9 100644 --- a/src/solvers/refinement/string_constraint_instantiation.h +++ b/src/solvers/strings/string_constraint_instantiation.h @@ -12,8 +12,8 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H -#include -#include +#include "string_constraint.h" +#include "string_constraint_generator.h" std::vector instantiate_not_contains( const string_not_contains_constraintt &axiom, diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp similarity index 90% rename from src/solvers/refinement/string_refinement.cpp rename to src/solvers/strings/string_refinement.cpp index 3dbe59ba22b..23b84598de7 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -17,18 +17,18 @@ Author: Alberto Griggio, alberto.griggio@gmail.com /// Parameterized Array and Interval Automaton" by Guodong Li and Indradeep /// Ghosh. -#include +#include "string_refinement.h" +#include "string_constraint_instantiation.h" #include #include +#include #include +#include #include #include -#include -#include -#include -#include #include +#include static bool is_valid_string_constraint( messaget::mstreamt &stream, @@ -134,24 +134,22 @@ static exprt substitute_array_access( /// \param index_value: map containing values of specific vector cells /// \return Vector containing values as described in the map template -static std::vector fill_in_map_as_vector( - const std::map &index_value) +static std::vector +fill_in_map_as_vector(const std::map &index_value) { std::vector result; if(!index_value.empty()) { - result.resize(index_value.rbegin()->first+1); - for(auto it=index_value.rbegin(); it!=index_value.rend(); ++it) + result.resize(index_value.rbegin()->first + 1); + for(auto it = index_value.rbegin(); it != index_value.rend(); ++it) { - const std::size_t index=it->first; + const std::size_t index = it->first; const T &value = it->second; - const auto next=std::next(it); - const std::size_t leftmost_index_to_pad= - next!=index_value.rend() - ? next->first+1 - : 0; - for(std::size_t j=leftmost_index_to_pad; j<=index; j++) - result[j]=value; + const auto next = std::next(it); + const std::size_t leftmost_index_to_pad = + next != index_value.rend() ? next->first + 1 : 0; + for(std::size_t j = leftmost_index_to_pad; j <= index; j++) + result[j] = value; } } return result; @@ -172,26 +170,28 @@ string_refinementt::string_refinementt(const infot &info, bool) { } -string_refinementt::string_refinementt(const infot &info): - string_refinementt(info, validate(info)) { } +string_refinementt::string_refinementt(const infot &info) + : string_refinementt(info, validate(info)) +{ +} /// Write index set to the given stream, use for debugging -static void display_index_set( - messaget::mstreamt &stream, - const index_set_pairt &index_set) +static void +display_index_set(messaget::mstreamt &stream, const index_set_pairt &index_set) { - const auto eom=messaget::eom; - std::size_t count=0; - std::size_t count_current=0; + const auto eom = messaget::eom; + std::size_t count = 0; + std::size_t count_current = 0; for(const auto &i : index_set.cumulative) { - const exprt &s=i.first; + const exprt &s = i.first; stream << "IS(" << format(s) << ")=={" << eom; for(const auto &j : i.second) { - const auto it=index_set.current.find(i.first); - if(it!=index_set.current.end() && it->second.find(j)!=it->second.end()) + const auto it = index_set.current.find(i.first); + if( + it != index_set.current.end() && it->second.find(j) != it->second.end()) { count_current++; stream << "**"; @@ -199,7 +199,7 @@ static void display_index_set( stream << " " << format(j) << ";" << eom; count++; } - stream << "}" << eom; + stream << "}" << eom; } stream << count << " elements in index set (" << count_current << " newly added)" << eom; @@ -285,7 +285,7 @@ replace_expr_copy(const union_find_replacet &symbol_resolve, exprt expr) /// \param value: the boolean value to set it to void string_refinementt::set_to(const exprt &expr, bool value) { - PRECONDITION(expr.type().id()==ID_bool); + PRECONDITION(expr.type().id() == ID_bool); PRECONDITION(equality_propagation); if(expr.id() == ID_equal && value) @@ -322,14 +322,14 @@ static void add_equations_for_symbol_resolution( { const exprt &lhs = eq.lhs(); const exprt &rhs = eq.rhs(); - if(lhs.id()!=ID_symbol) + if(lhs.id() != ID_symbol) { stream << log_message << "non symbol lhs: " << format(lhs) << " with rhs: " << format(rhs) << eom; continue; } - if(lhs.type()!=rhs.type()) + if(lhs.type() != rhs.type()) { stream << log_message << "non equal types lhs: " << format(lhs) << "\n####################### rhs: " << format(rhs) << eom; @@ -773,7 +773,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() for(const auto &instance : initial_instances) add_lemma(instance); - while((loop_bound_--)>0) + while((loop_bound_--) > 0) { dependencies.clean_cache(); const decision_proceduret::resultt refined_result = supert::dec_solve(); @@ -839,7 +839,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() } } debug() << "string_refinementt::dec_solve reached the maximum number" - << "of steps allowed" << eom; + << "of steps allowed" << eom; return resultt::D_ERROR; } @@ -856,7 +856,7 @@ void string_refinementt::add_lemma( current_constraints.push_back(lemma); - exprt simple_lemma=lemma; + exprt simple_lemma = lemma; if(simplify_lemma) simplify(simple_lemma, ns); @@ -907,14 +907,14 @@ static optionalt get_array( const auto eom = messaget::eom; const exprt &size = arr.length(); exprt arr_val = simplify_expr(super_get(arr), ns); - exprt size_val=super_get(size); - size_val=simplify_expr(size_val, ns); + exprt size_val = super_get(size); + size_val = simplify_expr(size_val, ns); const typet char_type = arr.type().subtype(); - const typet &index_type=size.type(); + const typet &index_type = size.type(); const array_typet empty_ret_type(char_type, from_integer(0, index_type)); const array_of_exprt empty_ret(from_integer(0, char_type), empty_ret_type); - if(size_val.id()!=ID_constant) + if(size_val.id() != ID_constant) { stream << "(sr::get_array) string of unknown size: " << format(size_val) << eom; @@ -957,10 +957,10 @@ static optionalt get_array( /// \return a string static std::string string_of_array(const array_exprt &arr) { - if(arr.type().id()!=ID_array) - return std::string(""); + if(arr.type().id() != ID_array) + return std::string(""); - exprt size_expr=to_array_type(arr.type()).size(); + exprt size_expr = to_array_type(arr.type()).size(); auto n = numeric_cast_v(size_expr); return utf16_constant_array_to_java(arr, n); } @@ -981,20 +981,19 @@ static exprt get_char_array_and_concretize( const auto &eom = messaget::eom; stream << "- " << format(arr) << ":\n"; stream << std::string(4, ' ') << "- type: " << format(arr.type()) << eom; - const auto arr_model_opt = - get_array(super_get, ns, stream, arr); + const auto arr_model_opt = get_array(super_get, ns, stream, arr); if(arr_model_opt) { stream << std::string(4, ' ') << "- char_array: " << format(*arr_model_opt) << '\n'; - stream << std::string(4, ' ') << "- type : " << format(arr_model_opt->type()) - << eom; + stream << std::string(4, ' ') + << "- type : " << format(arr_model_opt->type()) << eom; const exprt simple = simplify_expr(*arr_model_opt, ns); - stream << std::string(4, ' ') << "- simplified_char_array: " << format(simple) - << eom; + stream << std::string(4, ' ') + << "- simplified_char_array: " << format(simple) << eom; if( - const auto concretized_array = get_array( - super_get, ns, stream, to_array_string_expr(simple))) + const auto concretized_array = + get_array(super_get, ns, stream, to_array_string_expr(simple))) { stream << std::string(4, ' ') << "- concretized_char_array: " << format(*concretized_array) @@ -1030,8 +1029,8 @@ void debug_model( for(const auto &pointer_array : generator.array_pool.get_arrays_of_pointers()) { const auto arr = pointer_array.second; - const exprt model = get_char_array_and_concretize( - super_get, ns, stream, arr); + const exprt model = + get_char_array_and_concretize(super_get, ns, stream, arr); stream << "- " << format(arr) << ":\n" << " - pointer: " << format(pointer_array.first) << "\n" @@ -1123,8 +1122,8 @@ static exprt substitute_array_access( INVARIANT( array.is_nil() || array.id() == ID_symbol, std::string( - "in case the array is unknown, it should be a symbol or nil, id: ") - + id2string(array.id())); + "in case the array is unknown, it should be a symbol or nil, id: ") + + id2string(array.id())); return index_expr; } @@ -1205,7 +1204,7 @@ static exprt negation_of_not_contains_constraint( // that universal quantifier. std::vector conjuncts; conjuncts.reserve(numeric_cast_v(ube - lbe)); - for(mp_integer i=lbe; i> check_axioms( const std::unordered_map ¬_contain_witnesses) { - const auto eom=messaget::eom; + const auto eom = messaget::eom; // clang-format off const auto gen_symbol = [&](const irep_idt &id, const typet &type) { @@ -1278,9 +1278,9 @@ static std::pair> check_axioms( stream << "string_refinement::check_axioms: " << axioms.universal.size() << " universal axioms:" << eom; - for(size_t i=0; i> check_axioms( const auto &witness = find_counter_example(ns, with_concretized_arrays, axiom.univ_var)) { - stream << std::string(4, ' ') << "- violated_for: " - << format(axiom.univ_var) << "=" << format(*witness) << eom; - violated[i]=*witness; + stream << std::string(4, ' ') + << "- violated_for: " << format(axiom.univ_var) << "=" + << format(*witness) << eom; + violated[i] = *witness; } else stream << std::string(4, ' ') << "- correct" << eom; @@ -1311,40 +1312,40 @@ static std::pair> check_axioms( // Maps from indexes of violated not_contains axiom to a witness of violation std::map violated_not_contains; - stream << "there are " << axioms.not_contains.size() - << " not_contains axioms" << eom; + stream << "there are " << axioms.not_contains.size() << " not_contains axioms" + << eom; for(std::size_t i = 0; i < axioms.not_contains.size(); i++) { - const string_not_contains_constraintt &nc_axiom=axioms.not_contains[i]; + const string_not_contains_constraintt &nc_axiom = axioms.not_contains[i]; const symbol_exprt univ_var = generator.fresh_symbol( "not_contains_univ_var", nc_axiom.s0.length().type()); const exprt negated_axiom = negation_of_not_contains_constraint( nc_axiom, univ_var, [&](const exprt &expr) { - return simplify_expr(get(expr), ns); }); + return simplify_expr(get(expr), ns); + }); stream << std::string(2, ' ') << i << ".\n"; debug_check_axioms_step( stream, nc_axiom, nc_axiom, negated_axiom, negated_axiom); - if( - const auto witness = - find_counter_example(ns, negated_axiom, univ_var)) + if(const auto witness = find_counter_example(ns, negated_axiom, univ_var)) { - stream << std::string(4, ' ') << "- violated_for: " - << univ_var.get_identifier() << "=" << format(*witness) << eom; - violated_not_contains[i]=*witness; + stream << std::string(4, ' ') + << "- violated_for: " << univ_var.get_identifier() << "=" + << format(*witness) << eom; + violated_not_contains[i] = *witness; } } if(violated.empty() && violated_not_contains.empty()) { stream << "no violated property" << eom; - return { true, std::vector() }; + return {true, std::vector()}; } else { - stream << violated.size() - << " universal string axioms can be violated" << eom; + stream << violated.size() << " universal string axioms can be violated" + << eom; stream << violated_not_contains.size() << " not_contains string axioms can be violated" << eom; @@ -1354,8 +1355,8 @@ static std::pair> check_axioms( for(const auto &v : violated) { - const exprt &val=v.second; - const string_constraintt &axiom=axioms.universal[v.first]; + const exprt &val = v.second; + const string_constraintt &axiom = axioms.universal[v.first]; exprt instance(axiom.body); replace_expr(axiom.univ_var, val, instance); @@ -1370,13 +1371,13 @@ static std::pair> check_axioms( for(const auto &v : violated_not_contains) { - const exprt &val=v.second; - const string_not_contains_constraintt &axiom= + const exprt &val = v.second; + const string_not_contains_constraintt &axiom = axioms.not_contains[v.first]; const exprt func_val = index_exprt(not_contain_witnesses.at(axiom), val); - const exprt comp_val=simplify_sum(plus_exprt(val, func_val)); + const exprt comp_val = simplify_sum(plus_exprt(val, func_val)); std::set> indices; indices.insert(std::pair(comp_val, func_val)); @@ -1384,10 +1385,10 @@ static std::pair> check_axioms( ::instantiate_not_contains(axiom, indices, not_contain_witnesses)[0]; lemmas.push_back(counter); } - return { false, lemmas }; + return {false, lemmas}; } } - return { false, std::vector() }; + return {false, std::vector()}; } /// \param f: an expression with only addition and subtraction @@ -1399,34 +1400,34 @@ static std::map map_representation_of_sum(const exprt &f) // number of time the leaf should be added (can be negative) std::map elems; - std::list > to_process; + std::list> to_process; to_process.emplace_back(f, true); while(!to_process.empty()) { - exprt cur=to_process.back().first; - bool positive=to_process.back().second; + exprt cur = to_process.back().first; + bool positive = to_process.back().second; to_process.pop_back(); - if(cur.id()==ID_plus) + if(cur.id() == ID_plus) { for(const auto &op : cur.operands()) to_process.emplace_back(op, positive); } - else if(cur.id()==ID_minus) + else if(cur.id() == ID_minus) { to_process.emplace_back(cur.op1(), !positive); to_process.emplace_back(cur.op0(), positive); } - else if(cur.id()==ID_unary_minus) + else if(cur.id() == ID_unary_minus) { to_process.emplace_back(cur.op0(), !positive); } else { if(positive) - elems[cur]=elems[cur]+1; + elems[cur] = elems[cur] + 1; else - elems[cur]=elems[cur]-1; + elems[cur] = elems[cur] - 1; } } return elems; @@ -1438,25 +1439,23 @@ static std::map map_representation_of_sum(const exprt &f) /// \return a expression for the sum of each element in the map a number of /// times given by the corresponding integer in the map. For a map x -> 2, y /// -> -1 would give an expression $x + x - y$. -static exprt sum_over_map( - std::map &m, - const typet &type, - bool negated=false) +static exprt +sum_over_map(std::map &m, const typet &type, bool negated = false) { - exprt sum=nil_exprt(); - mp_integer constants=0; + exprt sum = nil_exprt(); + mp_integer constants = 0; typet index_type; if(m.empty()) return from_integer(0, type); else - index_type=m.begin()->first.type(); + index_type = m.begin()->first.type(); for(const auto &term : m) { // We should group constants together... - const exprt &t=term.first; - int second=negated?(-term.second):term.second; - if(t.id()==ID_constant) + const exprt &t = term.first; + int second = negated ? (-term.second) : term.second; + if(t.id() == ID_constant) { const auto int_value = numeric_cast_v(to_constant_expr(t)); constants += int_value * second; @@ -1467,42 +1466,42 @@ static exprt sum_over_map( { case -1: if(sum.is_nil()) - sum=unary_minus_exprt(t); + sum = unary_minus_exprt(t); else - sum=minus_exprt(sum, t); + sum = minus_exprt(sum, t); break; case 1: if(sum.is_nil()) - sum=t; + sum = t; else - sum=plus_exprt(sum, t); + sum = plus_exprt(sum, t); break; default: - if(second>1) + if(second > 1) { if(sum.is_nil()) - sum=t; + sum = t; else plus_exprt(sum, t); - for(int i=1; isecond; i--) - sum=minus_exprt(sum, t); + sum = minus_exprt(sum, t); + for(int i = -1; i > second; i--) + sum = minus_exprt(sum, t); } } } } - exprt index_const=from_integer(constants, index_type); + exprt index_const = from_integer(constants, index_type); if(sum.is_not_nil()) return plus_exprt(sum, index_const); else @@ -1513,7 +1512,7 @@ static exprt sum_over_map( /// \return an equivalent expression in a canonical form exprt simplify_sum(const exprt &f) { - std::map map=map_representation_of_sum(f); + std::map map = map_representation_of_sum(f); return sum_over_map(map, f.type()); } @@ -1526,28 +1525,26 @@ exprt simplify_sum(const exprt &f) /// to be equal to `val`. For instance, if `f` corresponds to the expression /// $q + x$, `compute_inverse_function(q,v,f)` returns an expression /// for $v - x$. -static exprt compute_inverse_function( - const exprt &qvar, - const exprt &val, - const exprt &f) +static exprt +compute_inverse_function(const exprt &qvar, const exprt &val, const exprt &f) { exprt positive, negative; // number of time the element should be added (can be negative) // qvar has to be equal to val - f(0) if it appears positively in f // (i.e. if f(qvar)=f(0) + qvar) and f(0) - val if it appears negatively // in f. So we start by computing val - f(0). - std::map elems=map_representation_of_sum(minus_exprt(val, f)); + std::map elems = map_representation_of_sum(minus_exprt(val, f)); // true if qvar appears negatively in f (positively in elems): - bool neg=false; + bool neg = false; - auto it=elems.find(qvar); + auto it = elems.find(qvar); INVARIANT( - it!=elems.end(), + it != elems.end(), string_refinement_invariantt("a function must have an occurrence of qvar")); - if(it->second==1 || it->second==-1) + if(it->second == 1 || it->second == -1) { - neg=(it->second==1); + neg = (it->second == 1); } else { @@ -1571,12 +1568,14 @@ class find_qvar_visitort : public const_expr_visitort public: bool found; - explicit find_qvar_visitort(const exprt &qvar): qvar_(qvar), found(false) {} + explicit find_qvar_visitort(const exprt &qvar) : qvar_(qvar), found(false) + { + } void operator()(const exprt &expr) override { - if(expr==qvar_) - found=true; + if(expr == qvar_) + found = true; } }; @@ -1628,7 +1627,7 @@ static void update_index_set( /// expression will be appended static void get_sub_arrays(const exprt &array_expr, std::vector &accu) { - if(array_expr.id()==ID_if) + if(array_expr.id() == ID_if) { get_sub_arrays(to_if_expr(array_expr).true_case(), accu); get_sub_arrays(to_if_expr(array_expr).false_case(), accu); @@ -1661,7 +1660,7 @@ static void add_to_index_set( { simplify(i, ns); const bool is_size_t = numeric_cast(i).has_value(); - if(i.id()!=ID_constant || is_size_t) + if(i.id() != ID_constant || is_size_t) { std::vector sub_arrays; get_sub_arrays(s, sub_arrays); @@ -1743,12 +1742,12 @@ static void initial_index_set( { auto it = axiom.premise.depth_begin(); const auto end = axiom.premise.depth_end(); - while(it!=end) + while(it != end) { if(it->id() == ID_index && is_char_type(it->type())) { - const exprt &s=it->op0(); - const exprt &i=it->op1(); + const exprt &s = it->op0(); + const exprt &i = it->op1(); // cur is of the form s[i] and no quantified variable appears in i add_to_index_set(index_set, ns, s, i); @@ -1778,16 +1777,16 @@ static void update_index_set( while(!to_process.empty()) { - exprt cur=to_process.back(); + exprt cur = to_process.back(); to_process.pop_back(); if(cur.id() == ID_index && is_char_type(cur.type())) { - const exprt &s=cur.op0(); - const exprt &i=cur.op1(); + const exprt &s = cur.op0(); + const exprt &i = cur.op1(); DATA_INVARIANT( - s.type().id()==ID_array, + s.type().id() == ID_array, string_refinement_invariantt("index expressions must index on arrays")); - exprt simplified=simplify_sum(i); + exprt simplified = simplify_sum(i); if(s.id() != ID_array) // do not update index set of constant arrays add_to_index_set(index_set, ns, s, simplified); } @@ -1842,10 +1841,8 @@ find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar) /// \param str: an array of characters /// \param val: an index expression /// \return instantiated formula -static exprt instantiate( - const string_constraintt &axiom, - const exprt &str, - const exprt &val) +static exprt +instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val) { exprt::operandst conjuncts; for(const auto &index : find_indexes(axiom.body, str, axiom.univ_var)) @@ -1890,15 +1887,16 @@ static std::vector instantiate( const array_string_exprt &s0 = axiom.s0; const array_string_exprt &s1 = axiom.s1; - const auto &index_set0=index_set.cumulative.find(s0.content()); - const auto &index_set1=index_set.cumulative.find(s1.content()); - const auto ¤t_index_set0=index_set.current.find(s0.content()); - const auto ¤t_index_set1=index_set.current.find(s1.content()); + const auto &index_set0 = index_set.cumulative.find(s0.content()); + const auto &index_set1 = index_set.cumulative.find(s1.content()); + const auto ¤t_index_set0 = index_set.current.find(s0.content()); + const auto ¤t_index_set1 = index_set.current.find(s1.content()); - if(index_set0!=index_set.cumulative.end() && - index_set1!=index_set.cumulative.end() && - current_index_set0!=index_set.current.end() && - current_index_set1!=index_set.current.end()) + if( + index_set0 != index_set.cumulative.end() && + index_set1 != index_set.cumulative.end() && + current_index_set0 != index_set.current.end() && + current_index_set1 != index_set.current.end()) { typedef std::pair expr_pairt; std::set index_pairs; @@ -1912,7 +1910,7 @@ static std::vector instantiate( return ::instantiate_not_contains(axiom, index_pairs, witnesses); } - return { }; + return {}; } /// Replace array-lists by 'with' expressions. @@ -1930,21 +1928,22 @@ exprt substitute_array_lists(exprt expr, size_t string_max_length) if(expr.id() == ID_array_list) { DATA_INVARIANT( - expr.operands().size()>=2, + expr.operands().size() >= 2, string_refinement_invariantt("array-lists must have at least two " - "operands")); + "operands")); const typet &char_type = expr.operands()[1].type(); array_typet arr_type(char_type, infinity_exprt(char_type)); - exprt ret_expr=array_of_exprt(from_integer(0, char_type), arr_type); + exprt ret_expr = array_of_exprt(from_integer(0, char_type), arr_type); - for(size_t i=0; i(index); - if(!index.is_constant() || - (index_value && *index_value find_counter_example( boolbvt solver(ns, sat_check); solver << axiom; - if(solver()==decision_proceduret::resultt::D_SATISFIABLE) + if(solver() == decision_proceduret::resultt::D_SATISFIABLE) return solver.get(var); else - return { }; + return {}; } /// \related string_constraintt @@ -2135,19 +2131,19 @@ static bool is_valid_string_constraint( const namespacet &ns, const string_constraintt &constraint) { - const auto eom=messaget::eom; + const auto eom = messaget::eom; const array_index_mapt body_indices = gather_indices(constraint.body); // Must validate for each string. Note that we have an invariant that the // second value in the pair is non-empty. for(const auto &pair : body_indices) { // Condition 1: All indices of the same string must be the of the same form - const exprt rep=pair.second.back(); - for(size_t j=0; j -#include #include +#include #include -#include -#include -#include -#include + +#include "string_constraint.h" +#include "string_constraint_generator.h" +#include "string_refinement_invariant.h" +#include "string_refinement_util.h" // clang-format off #define OPT_STRING_REFINEMENT \ @@ -59,25 +60,27 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits::max() -class string_refinementt final: public bv_refinementt +class string_refinementt final : public bv_refinementt { private: struct configt { - std::size_t refinement_bound=0; - bool use_counter_example=true; + std::size_t refinement_bound = 0; + bool use_counter_example = true; }; + public: /// string_refinementt constructor arguments - struct infot : public bv_refinementt::infot, - public configt + struct infot : public bv_refinementt::infot, public configt { }; explicit string_refinementt(const infot &); std::string decision_procedure_text() const override - { return "string refinement loop with "+prop.solver_text(); } + { + return "string refinement loop with " + prop.solver_text(); + } exprt get(const exprt &expr) const override; void set_to(const exprt &expr, bool value) override; diff --git a/src/solvers/refinement/string_refinement_invariant.h b/src/solvers/strings/string_refinement_invariant.h similarity index 74% rename from src/solvers/refinement/string_refinement_invariant.h rename to src/solvers/strings/string_refinement_invariant.h index 59f0c64cc28..f1f65432d67 100644 --- a/src/solvers/refinement/string_refinement_invariant.h +++ b/src/solvers/strings/string_refinement_invariant.h @@ -9,7 +9,7 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_INVARIANT_H #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_INVARIANT_H -#define string_refinement_invariantt(reason) \ - (("string_refinement_invariantt("+std::string(reason)+")").c_str()) +#define string_refinement_invariantt(reason) \ + (("string_refinement_invariantt(" + std::string(reason) + ")").c_str()) #endif // CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_INVARIANT_H diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/strings/string_refinement_util.cpp similarity index 98% rename from src/solvers/refinement/string_refinement_util.cpp rename to src/solvers/strings/string_refinement_util.cpp index 4686bfaf2e6..0204f66e0b5 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/strings/string_refinement_util.cpp @@ -6,20 +6,20 @@ Author: Diffblue Ltd. \*******************************************************************/ +#include "string_refinement_util.h" #include -#include #include #include +#include +#include #include -#include -#include -#include #include +#include #include #include #include -#include -#include "string_refinement_util.h" +#include +#include /// Applies `f` on all strings contained in `e` that are not if-expressions. /// For instance on input `cond1?s1:cond2?s2:s3` we apply `f` on s1, s2 and s3. @@ -29,9 +29,8 @@ static void for_each_atomic_string( bool is_char_type(const typet &type) { - return type.id() == ID_unsignedbv && - to_unsignedbv_type(type).get_width() <= - STRING_REFINEMENT_MAX_CHAR_WIDTH; + return type.id() == ID_unsignedbv && to_unsignedbv_type(type).get_width() <= + STRING_REFINEMENT_MAX_CHAR_WIDTH; } bool is_char_array_type(const typet &type, const namespacet &ns) @@ -432,8 +431,9 @@ void string_dependenciest::for_each_dependency( const auto string_node = node_at(to_array_string_expr(current)); INVARIANT( string_node, - "dependencies of the node should have been added to the graph at node creation " - + current.get().pretty()); + "dependencies of the node should have been added to the graph at " + "node creation " + + current.get().pretty()); f(*string_node); } } diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/strings/string_refinement_util.h similarity index 99% rename from src/solvers/refinement/string_refinement_util.h rename to src/solvers/strings/string_refinement_util.h index 230c34127fd..89cf37d81b5 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/strings/string_refinement_util.h @@ -158,7 +158,6 @@ class equation_symbol_mappingt std::unordered_map> strings_in_equation; }; - /// Keep track of dependencies between strings. /// Each string points to the builtin_function calls on which it depends. /// Each builtin_function points to the strings on which the result depends. diff --git a/unit/Makefile b/unit/Makefile index da9bfa98181..bc2e452bca6 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -34,14 +34,14 @@ SRC += analyses/ai/ai.cpp \ pointer-analysis/value_set.cpp \ solvers/floatbv/float_utils.cpp \ solvers/miniBDD/miniBDD.cpp \ - solvers/refinement/array_pool/array_pool.cpp \ - solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \ - solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \ - solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \ - solvers/refinement/string_refinement/concretize_array.cpp \ - solvers/refinement/string_refinement/sparse_array.cpp \ - solvers/refinement/string_refinement/substitute_array_list.cpp \ - solvers/refinement/string_refinement/union_find_replace.cpp \ + solvers/strings/array_pool/array_pool.cpp \ + solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \ + solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \ + solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp \ + solvers/strings/string_refinement/concretize_array.cpp \ + solvers/strings/string_refinement/sparse_array.cpp \ + solvers/strings/string_refinement/substitute_array_list.cpp \ + solvers/strings/string_refinement/union_find_replace.cpp \ util/cmdline.cpp \ util/expr_cast/expr_cast.cpp \ util/expr.cpp \ 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 deleted file mode 100644 index 76539a2cf3e..00000000000 --- a/unit/solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp +++ /dev/null @@ -1,150 +0,0 @@ -/*******************************************************************\ - -Module: Unit tests for calculate_max_string_length in - solvers/refinement/string_constraint_generator_valueof.cpp - -Author: Diffblue Ltd. - -\*******************************************************************/ - -#include - -#include -#include - -/// Get the string length needed to print any value of the given type with the -/// given radix. -static size_t expected_length(unsigned long radix, const typet &type) -{ - std::string longest(""); - if(radix==2) - { - if(type==unsignedbv_typet(32)) - { - longest="11111111111111111111111111111111"; - } - else if(type==unsignedbv_typet(64)) - { - longest= - "1111111111111111111111111111111111111111111111111111111111111111"; - } - else if(type==signedbv_typet(32)) - { - longest="-10000000000000000000000000000000"; - } - else if(type==signedbv_typet(64)) - { - longest= - "-1000000000000000000000000000000000000000000000000000000000000000"; - } - } - else if(radix==8) - { - if(type==unsignedbv_typet(32)) - { - longest="37777777777"; - } - else if(type==unsignedbv_typet(64)) - { - longest= - "1777777777777777777777"; - } - else if(type==signedbv_typet(32)) - { - longest="-20000000000"; - } - else if(type==signedbv_typet(64)) - { - longest= - "-1000000000000000000000"; - } - } - else if(radix==10) - { - if(type==unsignedbv_typet(32)) - { - longest="4294967295"; - } - else if(type==unsignedbv_typet(64)) - { - longest= - "18446744073709551615"; - } - else if(type==signedbv_typet(32)) - { - longest="-2147483648"; - } - else if(type==signedbv_typet(64)) - { - longest= - "-9223372036854775808"; - } - } - else if(radix==16) - { - if(type==unsignedbv_typet(32)) - { - longest="ffffffff"; - } - else if(type==unsignedbv_typet(64)) - { - longest= - "ffffffffffffffff"; - } - else if(type==signedbv_typet(32)) - { - longest="-80000000"; - } - else if(type==signedbv_typet(64)) - { - longest= - "-8000000000000000"; - } - } - - return longest.size(); -} - -SCENARIO("calculate_max_string_length", - "[core][solvers][refinement][string_constraint_generator_valueof]") -{ - const unsigned long radixes[]={2, 8, 10, 16}; - const typet int_types[]= - { - signedbv_typet(32), - unsignedbv_typet(32), - signedbv_typet(64), - unsignedbv_typet(64), - }; - - for(const typet &type : int_types) - { - std::string type_str=type.pretty(); - std::replace(type_str.begin(), type_str.end(), '\n', ' '); - WHEN("type = "+type_str) - { - for(const unsigned long radix : radixes) - { - WHEN("radix = "+std::to_string(radix)) - { - size_t actual_value=max_printed_string_length(type, radix); - THEN("value is correct") - { - size_t expected_value=expected_length(radix, type); - // Due to floating point rounding errors, we sometime get one more - // than the actual value, which is perfectly fine for our purposes - // Double brackets here prevent Catch trying to decompose a - // complex expression - REQUIRE(( - actual_value==expected_value || actual_value==expected_value+1)); - } - THEN("value is no greater than with default radix") - { - size_t actual_value_for_default=max_printed_string_length(type, 0); - REQUIRE(actual_value<=actual_value_for_default); - } - } - } - } - } -} diff --git a/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp b/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp deleted file mode 100644 index bfe1eae99a6..00000000000 --- a/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp +++ /dev/null @@ -1,134 +0,0 @@ -/*******************************************************************\ - -Module: Unit tests for get_numeric_value_from_character in - solvers/refinement/string_constraint_generator_valueof.cpp - -Author: Diffblue Ltd. - -\*******************************************************************/ - -#include - -#include -#include -#include -#include -#include - -/// Get the simplified return value of get_numeric_value_from_character called -/// with a radix -static exprt actual( - const mp_integer &character, - const typet &char_type, - const typet &int_type, - const bool strict_formatting, - const unsigned long radix_ul) -{ - const constant_exprt chr=from_integer(character, char_type); - symbol_tablet symtab; - const namespacet ns(symtab); - return simplify_expr( - get_numeric_value_from_character( - chr, char_type, int_type, strict_formatting, radix_ul), - ns); -} - -SCENARIO("get_numeric_value_from_character", - "[core][solvers][refinement][string_constraint_generator_valueof]") -{ - const typet char_type_1=unsignedbv_typet(8); - const typet char_type_2=unsignedbv_typet(16); - const typet char_type_3=unsignedbv_typet(32); - const typet int_type_1=signedbv_typet(8); - const typet int_type_2=signedbv_typet(16); - const typet int_type_3=signedbv_typet(32); - const typet int_type_4=signedbv_typet(64); - - WHEN("character='0'") - { - mp_integer character='0'; - mp_integer expected_mp=0; - const typet& char_type=char_type_1; - const typet& int_type=int_type_1; - const constant_exprt expected=from_integer(expected_mp, int_type); - - REQUIRE(expected==actual(character, char_type, int_type, true, 0)); - REQUIRE(expected==actual(character, char_type, int_type, true, 36)); - REQUIRE(expected==actual(character, char_type, int_type, true, 10)); - REQUIRE(expected==actual(character, char_type, int_type, false, 0)); - REQUIRE(expected==actual(character, char_type, int_type, false, 36)); - REQUIRE(expected==actual(character, char_type, int_type, false, 10)); - } - WHEN("character='9'") - { - mp_integer character='9'; - mp_integer expected_mp=9; - const typet& char_type=char_type_2; - const typet& int_type=int_type_2; - const constant_exprt expected=from_integer(expected_mp, int_type); - - REQUIRE(expected==actual(character, char_type, int_type, true, 0)); - REQUIRE(expected==actual(character, char_type, int_type, true, 36)); - REQUIRE(expected==actual(character, char_type, int_type, true, 10)); - REQUIRE(expected==actual(character, char_type, int_type, false, 0)); - REQUIRE(expected==actual(character, char_type, int_type, false, 36)); - REQUIRE(expected==actual(character, char_type, int_type, false, 10)); - } - WHEN("character='A'") - { - mp_integer character='A'; - mp_integer expected_mp=10; - const typet& char_type=char_type_3; - const typet& int_type=int_type_3; - const constant_exprt expected=from_integer(expected_mp, int_type); - - REQUIRE(expected==actual(character, char_type, int_type, false, 0)); - REQUIRE(expected==actual(character, char_type, int_type, false, 36)); - REQUIRE(expected!=actual(character, char_type, int_type, false, 10)); - } - WHEN("character='z'") - { - mp_integer character='z'; - mp_integer expected_mp=35; - const typet& char_type=char_type_1; - const typet& int_type=int_type_4; - const constant_exprt expected=from_integer(expected_mp, int_type); - - REQUIRE(expected==actual(character, char_type, int_type, true, 0)); - REQUIRE(expected==actual(character, char_type, int_type, true, 36)); - REQUIRE(expected!=actual(character, char_type, int_type, true, 10)); - REQUIRE(expected==actual(character, char_type, int_type, false, 0)); - REQUIRE(expected==actual(character, char_type, int_type, false, 36)); - REQUIRE(expected!=actual(character, char_type, int_type, false, 10)); - } - WHEN("character='+'") - { - mp_integer character='+'; - mp_integer expected_mp=0; - const typet& char_type=char_type_2; - const typet& int_type=int_type_1; - const constant_exprt expected=from_integer(expected_mp, int_type); - - REQUIRE(expected==actual(character, char_type, int_type, true, 0)); - REQUIRE(expected==actual(character, char_type, int_type, true, 36)); - REQUIRE(expected==actual(character, char_type, int_type, true, 10)); - REQUIRE(expected==actual(character, char_type, int_type, false, 0)); - REQUIRE(expected==actual(character, char_type, int_type, false, 36)); - REQUIRE(expected==actual(character, char_type, int_type, false, 10)); - } - WHEN("character='-'") - { - mp_integer character='-'; - mp_integer expected_mp=0; - const typet& char_type=char_type_3; - const typet& int_type=int_type_2; - const constant_exprt expected=from_integer(expected_mp, int_type); - - REQUIRE(expected==actual(character, char_type, int_type, true, 0)); - REQUIRE(expected==actual(character, char_type, int_type, true, 36)); - REQUIRE(expected==actual(character, char_type, int_type, true, 10)); - REQUIRE(expected==actual(character, char_type, int_type, false, 0)); - REQUIRE(expected==actual(character, char_type, int_type, false, 36)); - REQUIRE(expected==actual(character, char_type, int_type, false, 10)); - } -} diff --git a/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp b/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp deleted file mode 100644 index 6be62a87808..00000000000 --- a/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp +++ /dev/null @@ -1,227 +0,0 @@ -/*******************************************************************\ - -Module: Unit tests for is_digit_with_radix in - solvers/refinement/string_constraint_generator_valueof.cpp - -Author: Diffblue Ltd. - -\*******************************************************************/ - -#include - -#include -#include -#include -#include -#include - -/// Get the simplified return value of is_digit_with_radix called with a radix -static exprt actual( - const mp_integer int_value, - const exprt &radix_as_char, - const unsigned long radix_ul, - const bool strict_formatting) -{ - const typet char_type=unsignedbv_typet(16); - const constant_exprt chr=from_integer(int_value, char_type); - symbol_tablet symtab; - const namespacet ns(symtab); - - return simplify_expr( - is_digit_with_radix(chr, strict_formatting, radix_as_char, radix_ul), ns); -} - -/// Get the simplified return value of is_digit_with_radix called with a radix -static exprt actual_with_radix( - const mp_integer int_value, - const unsigned long radix_ul, - const bool strict_formatting) -{ - const typet char_type=unsignedbv_typet(16); - const constant_exprt radix_as_char=from_integer(radix_ul, char_type); - - return actual(int_value, radix_as_char, radix_ul, strict_formatting); -} - -/// Get the simplified return value of is_digit_with_radix called without a -/// radix -static exprt actual_without_radix( - const mp_integer int_value, - const unsigned long radix_ul, - const bool strict_formatting) -{ - const typet char_type=unsignedbv_typet(16); - const constant_exprt radix_as_char=from_integer(radix_ul, char_type); - - return actual(int_value, radix_as_char, 0, strict_formatting); -} - -SCENARIO("is_digit_with_radix without strict formatting", - "[core][solvers][refinement][string_constraint_generator_valueof]") -{ - WHEN("Radix 10") - { - const unsigned long radix_ul=10; - - WHEN("char '0'") - { - WHEN("strict formatting on") - { - const bool strict=true; - REQUIRE(true_exprt()==actual_without_radix('0', radix_ul, strict)); - REQUIRE(true_exprt()==actual_with_radix('0', radix_ul, strict)); - } - WHEN("strict formatting off") - { - const bool strict=false; - REQUIRE(true_exprt()==actual_without_radix('0', radix_ul, strict)); - REQUIRE(true_exprt()==actual_with_radix('0', radix_ul, strict)); - } - } - WHEN("char '9'") - { - WHEN("strict formatting on") - { - const bool strict=true; - REQUIRE(true_exprt()==actual_without_radix('9', radix_ul, strict)); - REQUIRE(true_exprt()==actual_with_radix('9', radix_ul, strict)); - } - WHEN("strict formatting off") - { - const bool strict=false; - REQUIRE(true_exprt()==actual_without_radix('9', radix_ul, strict)); - REQUIRE(true_exprt()==actual_with_radix('9', radix_ul, strict)); - } - } - WHEN("char 'a'") - { - WHEN("strict formatting on") - { - const bool strict=true; - REQUIRE(false_exprt()==actual_without_radix('a', radix_ul, strict)); - REQUIRE(false_exprt()==actual_with_radix('a', radix_ul, strict)); - } - WHEN("strict formatting off") - { - const bool strict=false; - REQUIRE(false_exprt()==actual_without_radix('a', radix_ul, strict)); - REQUIRE(false_exprt()==actual_with_radix('a', radix_ul, strict)); - } - } - } - WHEN("Radix 8") - { - const unsigned long radix_ul=8; - - WHEN("char '7'") - { - WHEN("strict formatting on") - { - const bool strict=true; - REQUIRE(true_exprt()==actual_without_radix('7', radix_ul, strict)); - REQUIRE(true_exprt()==actual_with_radix('7', radix_ul, strict)); - } - WHEN("strict formatting off") - { - const bool strict=false; - REQUIRE(true_exprt()==actual_without_radix('7', radix_ul, strict)); - REQUIRE(true_exprt()==actual_with_radix('7', radix_ul, strict)); - } - } - WHEN("char '8'") - { - WHEN("strict formatting on") - { - const bool strict=true; - REQUIRE(false_exprt()==actual_without_radix('8', radix_ul, strict)); - REQUIRE(false_exprt()==actual_with_radix('8', radix_ul, strict)); - } - WHEN("strict formatting off") - { - const bool strict=false; - REQUIRE(false_exprt()==actual_without_radix('8', radix_ul, strict)); - REQUIRE(false_exprt()==actual_with_radix('8', radix_ul, strict)); - } - } - } - WHEN("Radix 16") - { - const unsigned long radix_ul=16; - - WHEN("char '5'") - { - WHEN("strict formatting on") - { - const bool strict=true; - REQUIRE(true_exprt()==actual_without_radix('5', radix_ul, strict)); - REQUIRE(true_exprt()==actual_with_radix('5', radix_ul, strict)); - } - WHEN("strict formatting off") - { - const bool strict=false; - REQUIRE(true_exprt()==actual_without_radix('5', radix_ul, strict)); - REQUIRE(true_exprt()==actual_with_radix('5', radix_ul, strict)); - } - } - WHEN("char 'a'") - { - WHEN("strict formatting on") - { - const bool strict=true; - REQUIRE(true_exprt()==actual_without_radix('a', radix_ul, strict)); - REQUIRE(true_exprt()==actual_with_radix('a', radix_ul, strict)); - } - WHEN("strict formatting off") - { - const bool strict=false; - REQUIRE(true_exprt()==actual_without_radix('a', radix_ul, strict)); - REQUIRE(true_exprt()==actual_with_radix('a', radix_ul, strict)); - } - } - WHEN("char 'A'") - { - WHEN("strict formatting on") - { - const bool strict=true; - REQUIRE(false_exprt()==actual_without_radix('A', radix_ul, strict)); - REQUIRE(false_exprt()==actual_with_radix('A', radix_ul, strict)); - } - WHEN("strict formatting off") - { - const bool strict=false; - REQUIRE(true_exprt()==actual_without_radix('A', radix_ul, strict)); - REQUIRE(true_exprt()==actual_with_radix('A', radix_ul, strict)); - } - } - WHEN("char 'f'") - { - WHEN("strict formatting on") - { - const bool strict=true; - REQUIRE(true_exprt()==actual_without_radix('f', radix_ul, strict)); - REQUIRE(true_exprt()==actual_with_radix('f', radix_ul, strict)); - } - WHEN("strict formatting off") - { - const bool strict=false; - REQUIRE(true_exprt()==actual_without_radix('f', radix_ul, strict)); - REQUIRE(true_exprt()==actual_with_radix('f', radix_ul, strict)); - } - } - WHEN("char 'g'") - { - WHEN("strict formatting on") - { - const bool strict=true; - REQUIRE(false_exprt()==actual_without_radix('g', radix_ul, strict)); - REQUIRE(false_exprt()==actual_with_radix('g', radix_ul, strict)); - } - WHEN("strict formatting off") - { - const bool strict=false; - REQUIRE(false_exprt()==actual_without_radix('g', radix_ul, strict)); - REQUIRE(false_exprt()==actual_with_radix('g', radix_ul, strict)); - } - } - } -} diff --git a/unit/solvers/refinement/string_refinement/substitute_array_list.cpp b/unit/solvers/refinement/string_refinement/substitute_array_list.cpp deleted file mode 100644 index c63caef418e..00000000000 --- a/unit/solvers/refinement/string_refinement/substitute_array_list.cpp +++ /dev/null @@ -1,56 +0,0 @@ -/*******************************************************************\ - -Module: Unit tests for get_numeric_value_from_character in - solvers/refinement/string_constraint_generator_valueof.cpp - -Author: Diffblue Ltd. - -\*******************************************************************/ - -#include - -#include -#include -#include -#include -#include - -SCENARIO("substitute_array_list", - "[core][solvers][refinement][string_refinement]") -{ - const typet char_type=unsignedbv_typet(16); - const typet int_type=signedbv_typet(32); - const array_typet array_type(char_type, infinity_exprt(int_type)); - const exprt index0=from_integer(0, int_type); - const exprt charx=from_integer('x', char_type); - const exprt index1=from_integer(1, int_type); - const exprt chary=from_integer('y', char_type); - const exprt index100=from_integer(100, int_type); - - // arr is `array-list [ 0 , 'x' , 1 , 'y' , 2 , 'z']` - array_list_exprt arr( - {index0, charx, index1, chary, index100, from_integer('z', char_type)}, - array_type); - - // Max length is 2, so index 2 should get ignored. - const exprt subst=substitute_array_lists(arr, 2); - - // Check that `subst = e1 WITH [1:='y']` - REQUIRE(subst.id()==ID_with); - REQUIRE(subst.operands().size()==3); - const exprt &e1=subst.op0(); - REQUIRE(subst.op1()==index1); - REQUIRE(subst.op2()==chary); - - // Check that `e1 = e2 WITH [0:='x']` - REQUIRE(e1.id()==ID_with); - REQUIRE(e1.operands().size()==3); - const exprt &e2=e1.op0(); - REQUIRE(e1.op1()==index0); - REQUIRE(e1.op2()==charx); - - // Check that `e1 = ARRAY_OF 0` - REQUIRE(e2.id()==ID_array_of); - REQUIRE(e2.operands().size()==1); - REQUIRE(e2.op0()==from_integer(0, char_type)); -} diff --git a/unit/solvers/refinement/array_pool/array_pool.cpp b/unit/solvers/strings/array_pool/array_pool.cpp similarity index 95% rename from unit/solvers/refinement/array_pool/array_pool.cpp rename to unit/solvers/strings/array_pool/array_pool.cpp index b8a064568e9..bb6a286cd68 100644 --- a/unit/solvers/refinement/array_pool/array_pool.cpp +++ b/unit/solvers/strings/array_pool/array_pool.cpp @@ -9,10 +9,9 @@ Author: Diffblue Ltd. #include -#include +#include -SCENARIO( - "array_pool", "[core][solvers][refinement][string_constraint_generator]") +SCENARIO("array_pool", "[core][solvers][strings][string_constraint_generator]") { const std::size_t pointer_width = 16; const auto char_type = unsignedbv_typet(8); @@ -88,8 +87,9 @@ SCENARIO( const array_string_exprt associated_array = pool.find(if_expr, pointer_length); - THEN("Arrays associated to the subexpressions are the subexpressions of " - "the associated array") + THEN( + "Arrays associated to the subexpressions are the subexpressions of " + "the associated array") { const symbol_exprt pointer_length1("pointer_length1", length_type); const array_string_exprt associated_to_true = diff --git a/unit/solvers/refinement/array_pool/module_dependencies.txt b/unit/solvers/strings/array_pool/module_dependencies.txt similarity index 70% rename from unit/solvers/refinement/array_pool/module_dependencies.txt rename to unit/solvers/strings/array_pool/module_dependencies.txt index 71b28bcf83d..60319981c6b 100644 --- a/unit/solvers/refinement/array_pool/module_dependencies.txt +++ b/unit/solvers/strings/array_pool/module_dependencies.txt @@ -1,3 +1,4 @@ solvers/refinement +solvers/strings testing-utils util diff --git a/unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp b/unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp new file mode 100644 index 00000000000..fd93101a534 --- /dev/null +++ b/unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp @@ -0,0 +1,146 @@ +/*******************************************************************\ + +Module: Unit tests for calculate_max_string_length in + solvers/refinement/string_constraint_generator_valueof.cpp + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include + +#include +#include + +/// Get the string length needed to print any value of the given type with the +/// given radix. +static size_t expected_length(unsigned long radix, const typet &type) +{ + std::string longest(""); + if(radix == 2) + { + if(type == unsignedbv_typet(32)) + { + longest = "11111111111111111111111111111111"; + } + else if(type == unsignedbv_typet(64)) + { + longest = + "1111111111111111111111111111111111111111111111111111111111111111"; + } + else if(type == signedbv_typet(32)) + { + longest = "-10000000000000000000000000000000"; + } + else if(type == signedbv_typet(64)) + { + longest = + "-1000000000000000000000000000000000000000000000000000000000000000"; + } + } + else if(radix == 8) + { + if(type == unsignedbv_typet(32)) + { + longest = "37777777777"; + } + else if(type == unsignedbv_typet(64)) + { + longest = "1777777777777777777777"; + } + else if(type == signedbv_typet(32)) + { + longest = "-20000000000"; + } + else if(type == signedbv_typet(64)) + { + longest = "-1000000000000000000000"; + } + } + else if(radix == 10) + { + if(type == unsignedbv_typet(32)) + { + longest = "4294967295"; + } + else if(type == unsignedbv_typet(64)) + { + longest = "18446744073709551615"; + } + else if(type == signedbv_typet(32)) + { + longest = "-2147483648"; + } + else if(type == signedbv_typet(64)) + { + longest = "-9223372036854775808"; + } + } + else if(radix == 16) + { + if(type == unsignedbv_typet(32)) + { + longest = "ffffffff"; + } + else if(type == unsignedbv_typet(64)) + { + longest = "ffffffffffffffff"; + } + else if(type == signedbv_typet(32)) + { + longest = "-80000000"; + } + else if(type == signedbv_typet(64)) + { + longest = "-8000000000000000"; + } + } + + return longest.size(); +} + +SCENARIO( + "calculate_max_string_length", + "[core][solvers][strings][string_constraint_generator_valueof]") +{ + const unsigned long radixes[] = {2, 8, 10, 16}; + const typet int_types[] = { + signedbv_typet(32), + unsignedbv_typet(32), + signedbv_typet(64), + unsignedbv_typet(64), + }; + + for(const typet &type : int_types) + { + std::string type_str = type.pretty(); + std::replace(type_str.begin(), type_str.end(), '\n', ' '); + WHEN("type = " + type_str) + { + for(const unsigned long radix : radixes) + { + WHEN("radix = " + std::to_string(radix)) + { + size_t actual_value = max_printed_string_length(type, radix); + THEN("value is correct") + { + size_t expected_value = expected_length(radix, type); + // Due to floating point rounding errors, we sometime get one more + // than the actual value, which is perfectly fine for our purposes + // Double brackets here prevent Catch trying to decompose a + // complex expression + REQUIRE( + (actual_value == expected_value || + actual_value == expected_value + 1)); + } + THEN("value is no greater than with default radix") + { + size_t actual_value_for_default = + max_printed_string_length(type, 0); + REQUIRE(actual_value <= actual_value_for_default); + } + } + } + } + } +} diff --git a/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp b/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp new file mode 100644 index 00000000000..faf2a032a33 --- /dev/null +++ b/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp @@ -0,0 +1,136 @@ +/*******************************************************************\ + +Module: Unit tests for get_numeric_value_from_character in + solvers/refinement/string_constraint_generator_valueof.cpp + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include + +#include + +#include +#include +#include +#include + +/// Get the simplified return value of get_numeric_value_from_character called +/// with a radix +static exprt actual( + const mp_integer &character, + const typet &char_type, + const typet &int_type, + const bool strict_formatting, + const unsigned long radix_ul) +{ + const constant_exprt chr = from_integer(character, char_type); + symbol_tablet symtab; + const namespacet ns(symtab); + return simplify_expr( + get_numeric_value_from_character( + chr, char_type, int_type, strict_formatting, radix_ul), + ns); +} + +SCENARIO( + "get_numeric_value_from_character", + "[core][solvers][strings][string_constraint_generator_valueof]") +{ + const typet char_type_1 = unsignedbv_typet(8); + const typet char_type_2 = unsignedbv_typet(16); + const typet char_type_3 = unsignedbv_typet(32); + const typet int_type_1 = signedbv_typet(8); + const typet int_type_2 = signedbv_typet(16); + const typet int_type_3 = signedbv_typet(32); + const typet int_type_4 = signedbv_typet(64); + + WHEN("character='0'") + { + mp_integer character = '0'; + mp_integer expected_mp = 0; + const typet &char_type = char_type_1; + const typet &int_type = int_type_1; + const constant_exprt expected = from_integer(expected_mp, int_type); + + REQUIRE(expected == actual(character, char_type, int_type, true, 0)); + REQUIRE(expected == actual(character, char_type, int_type, true, 36)); + REQUIRE(expected == actual(character, char_type, int_type, true, 10)); + REQUIRE(expected == actual(character, char_type, int_type, false, 0)); + REQUIRE(expected == actual(character, char_type, int_type, false, 36)); + REQUIRE(expected == actual(character, char_type, int_type, false, 10)); + } + WHEN("character='9'") + { + mp_integer character = '9'; + mp_integer expected_mp = 9; + const typet &char_type = char_type_2; + const typet &int_type = int_type_2; + const constant_exprt expected = from_integer(expected_mp, int_type); + + REQUIRE(expected == actual(character, char_type, int_type, true, 0)); + REQUIRE(expected == actual(character, char_type, int_type, true, 36)); + REQUIRE(expected == actual(character, char_type, int_type, true, 10)); + REQUIRE(expected == actual(character, char_type, int_type, false, 0)); + REQUIRE(expected == actual(character, char_type, int_type, false, 36)); + REQUIRE(expected == actual(character, char_type, int_type, false, 10)); + } + WHEN("character='A'") + { + mp_integer character = 'A'; + mp_integer expected_mp = 10; + const typet &char_type = char_type_3; + const typet &int_type = int_type_3; + const constant_exprt expected = from_integer(expected_mp, int_type); + + REQUIRE(expected == actual(character, char_type, int_type, false, 0)); + REQUIRE(expected == actual(character, char_type, int_type, false, 36)); + REQUIRE(expected != actual(character, char_type, int_type, false, 10)); + } + WHEN("character='z'") + { + mp_integer character = 'z'; + mp_integer expected_mp = 35; + const typet &char_type = char_type_1; + const typet &int_type = int_type_4; + const constant_exprt expected = from_integer(expected_mp, int_type); + + REQUIRE(expected == actual(character, char_type, int_type, true, 0)); + REQUIRE(expected == actual(character, char_type, int_type, true, 36)); + REQUIRE(expected != actual(character, char_type, int_type, true, 10)); + REQUIRE(expected == actual(character, char_type, int_type, false, 0)); + REQUIRE(expected == actual(character, char_type, int_type, false, 36)); + REQUIRE(expected != actual(character, char_type, int_type, false, 10)); + } + WHEN("character='+'") + { + mp_integer character = '+'; + mp_integer expected_mp = 0; + const typet &char_type = char_type_2; + const typet &int_type = int_type_1; + const constant_exprt expected = from_integer(expected_mp, int_type); + + REQUIRE(expected == actual(character, char_type, int_type, true, 0)); + REQUIRE(expected == actual(character, char_type, int_type, true, 36)); + REQUIRE(expected == actual(character, char_type, int_type, true, 10)); + REQUIRE(expected == actual(character, char_type, int_type, false, 0)); + REQUIRE(expected == actual(character, char_type, int_type, false, 36)); + REQUIRE(expected == actual(character, char_type, int_type, false, 10)); + } + WHEN("character='-'") + { + mp_integer character = '-'; + mp_integer expected_mp = 0; + const typet &char_type = char_type_3; + const typet &int_type = int_type_2; + const constant_exprt expected = from_integer(expected_mp, int_type); + + REQUIRE(expected == actual(character, char_type, int_type, true, 0)); + REQUIRE(expected == actual(character, char_type, int_type, true, 36)); + REQUIRE(expected == actual(character, char_type, int_type, true, 10)); + REQUIRE(expected == actual(character, char_type, int_type, false, 0)); + REQUIRE(expected == actual(character, char_type, int_type, false, 36)); + REQUIRE(expected == actual(character, char_type, int_type, false, 10)); + } +} diff --git a/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp b/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp new file mode 100644 index 00000000000..42d5db8d4fa --- /dev/null +++ b/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp @@ -0,0 +1,229 @@ +/*******************************************************************\ + +Module: Unit tests for is_digit_with_radix in + solvers/refinement/string_constraint_generator_valueof.cpp + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include + +#include + +#include +#include +#include +#include + +/// Get the simplified return value of is_digit_with_radix called with a radix +static exprt actual( + const mp_integer int_value, + const exprt &radix_as_char, + const unsigned long radix_ul, + const bool strict_formatting) +{ + const typet char_type = unsignedbv_typet(16); + const constant_exprt chr = from_integer(int_value, char_type); + symbol_tablet symtab; + const namespacet ns(symtab); + + return simplify_expr( + is_digit_with_radix(chr, strict_formatting, radix_as_char, radix_ul), ns); +} + +/// Get the simplified return value of is_digit_with_radix called with a radix +static exprt actual_with_radix( + const mp_integer int_value, + const unsigned long radix_ul, + const bool strict_formatting) +{ + const typet char_type = unsignedbv_typet(16); + const constant_exprt radix_as_char = from_integer(radix_ul, char_type); + + return actual(int_value, radix_as_char, radix_ul, strict_formatting); +} + +/// Get the simplified return value of is_digit_with_radix called without a +/// radix +static exprt actual_without_radix( + const mp_integer int_value, + const unsigned long radix_ul, + const bool strict_formatting) +{ + const typet char_type = unsignedbv_typet(16); + const constant_exprt radix_as_char = from_integer(radix_ul, char_type); + + return actual(int_value, radix_as_char, 0, strict_formatting); +} + +SCENARIO( + "is_digit_with_radix without strict formatting", + "[core][solvers][strings][string_constraint_generator_valueof]") +{ + WHEN("Radix 10") + { + const unsigned long radix_ul = 10; + + WHEN("char '0'") + { + WHEN("strict formatting on") + { + const bool strict = true; + REQUIRE(true_exprt() == actual_without_radix('0', radix_ul, strict)); + REQUIRE(true_exprt() == actual_with_radix('0', radix_ul, strict)); + } + WHEN("strict formatting off") + { + const bool strict = false; + REQUIRE(true_exprt() == actual_without_radix('0', radix_ul, strict)); + REQUIRE(true_exprt() == actual_with_radix('0', radix_ul, strict)); + } + } + WHEN("char '9'") + { + WHEN("strict formatting on") + { + const bool strict = true; + REQUIRE(true_exprt() == actual_without_radix('9', radix_ul, strict)); + REQUIRE(true_exprt() == actual_with_radix('9', radix_ul, strict)); + } + WHEN("strict formatting off") + { + const bool strict = false; + REQUIRE(true_exprt() == actual_without_radix('9', radix_ul, strict)); + REQUIRE(true_exprt() == actual_with_radix('9', radix_ul, strict)); + } + } + WHEN("char 'a'") + { + WHEN("strict formatting on") + { + const bool strict = true; + REQUIRE(false_exprt() == actual_without_radix('a', radix_ul, strict)); + REQUIRE(false_exprt() == actual_with_radix('a', radix_ul, strict)); + } + WHEN("strict formatting off") + { + const bool strict = false; + REQUIRE(false_exprt() == actual_without_radix('a', radix_ul, strict)); + REQUIRE(false_exprt() == actual_with_radix('a', radix_ul, strict)); + } + } + } + WHEN("Radix 8") + { + const unsigned long radix_ul = 8; + + WHEN("char '7'") + { + WHEN("strict formatting on") + { + const bool strict = true; + REQUIRE(true_exprt() == actual_without_radix('7', radix_ul, strict)); + REQUIRE(true_exprt() == actual_with_radix('7', radix_ul, strict)); + } + WHEN("strict formatting off") + { + const bool strict = false; + REQUIRE(true_exprt() == actual_without_radix('7', radix_ul, strict)); + REQUIRE(true_exprt() == actual_with_radix('7', radix_ul, strict)); + } + } + WHEN("char '8'") + { + WHEN("strict formatting on") + { + const bool strict = true; + REQUIRE(false_exprt() == actual_without_radix('8', radix_ul, strict)); + REQUIRE(false_exprt() == actual_with_radix('8', radix_ul, strict)); + } + WHEN("strict formatting off") + { + const bool strict = false; + REQUIRE(false_exprt() == actual_without_radix('8', radix_ul, strict)); + REQUIRE(false_exprt() == actual_with_radix('8', radix_ul, strict)); + } + } + } + WHEN("Radix 16") + { + const unsigned long radix_ul = 16; + + WHEN("char '5'") + { + WHEN("strict formatting on") + { + const bool strict = true; + REQUIRE(true_exprt() == actual_without_radix('5', radix_ul, strict)); + REQUIRE(true_exprt() == actual_with_radix('5', radix_ul, strict)); + } + WHEN("strict formatting off") + { + const bool strict = false; + REQUIRE(true_exprt() == actual_without_radix('5', radix_ul, strict)); + REQUIRE(true_exprt() == actual_with_radix('5', radix_ul, strict)); + } + } + WHEN("char 'a'") + { + WHEN("strict formatting on") + { + const bool strict = true; + REQUIRE(true_exprt() == actual_without_radix('a', radix_ul, strict)); + REQUIRE(true_exprt() == actual_with_radix('a', radix_ul, strict)); + } + WHEN("strict formatting off") + { + const bool strict = false; + REQUIRE(true_exprt() == actual_without_radix('a', radix_ul, strict)); + REQUIRE(true_exprt() == actual_with_radix('a', radix_ul, strict)); + } + } + WHEN("char 'A'") + { + WHEN("strict formatting on") + { + const bool strict = true; + REQUIRE(false_exprt() == actual_without_radix('A', radix_ul, strict)); + REQUIRE(false_exprt() == actual_with_radix('A', radix_ul, strict)); + } + WHEN("strict formatting off") + { + const bool strict = false; + REQUIRE(true_exprt() == actual_without_radix('A', radix_ul, strict)); + REQUIRE(true_exprt() == actual_with_radix('A', radix_ul, strict)); + } + } + WHEN("char 'f'") + { + WHEN("strict formatting on") + { + const bool strict = true; + REQUIRE(true_exprt() == actual_without_radix('f', radix_ul, strict)); + REQUIRE(true_exprt() == actual_with_radix('f', radix_ul, strict)); + } + WHEN("strict formatting off") + { + const bool strict = false; + REQUIRE(true_exprt() == actual_without_radix('f', radix_ul, strict)); + REQUIRE(true_exprt() == actual_with_radix('f', radix_ul, strict)); + } + } + WHEN("char 'g'") + { + WHEN("strict formatting on") + { + const bool strict = true; + REQUIRE(false_exprt() == actual_without_radix('g', radix_ul, strict)); + REQUIRE(false_exprt() == actual_with_radix('g', radix_ul, strict)); + } + WHEN("strict formatting off") + { + const bool strict = false; + REQUIRE(false_exprt() == actual_without_radix('g', radix_ul, strict)); + REQUIRE(false_exprt() == actual_with_radix('g', radix_ul, strict)); + } + } + } +} diff --git a/unit/solvers/refinement/string_constraint_generator_valueof/module_dependencies.txt b/unit/solvers/strings/string_constraint_generator_valueof/module_dependencies.txt similarity index 82% rename from unit/solvers/refinement/string_constraint_generator_valueof/module_dependencies.txt rename to unit/solvers/strings/string_constraint_generator_valueof/module_dependencies.txt index ee346fe1dd4..7acd5bbec93 100644 --- a/unit/solvers/refinement/string_constraint_generator_valueof/module_dependencies.txt +++ b/unit/solvers/strings/string_constraint_generator_valueof/module_dependencies.txt @@ -1,4 +1,5 @@ solvers/refinement +solvers/strings string_constraint_generator_valueof testing-utils util diff --git a/unit/solvers/refinement/string_refinement/concretize_array.cpp b/unit/solvers/strings/string_refinement/concretize_array.cpp similarity index 66% rename from unit/solvers/refinement/string_refinement/concretize_array.cpp rename to unit/solvers/strings/string_refinement/concretize_array.cpp index 130f9d21a8b..0d7f27b615a 100644 --- a/unit/solvers/refinement/string_refinement/concretize_array.cpp +++ b/unit/solvers/strings/string_refinement/concretize_array.cpp @@ -10,24 +10,26 @@ Author: Diffblue Ltd. #include #include -#include #include +#include #include -#include -SCENARIO("concretize_array_expression", - "[core][solvers][refinement][string_refinement]") +#include + +SCENARIO( + "concretize_array_expression", + "[core][solvers][strings][string_refinement]") { // Arrange - const typet char_type=unsignedbv_typet(16); - const typet int_type=signedbv_typet(32); - const exprt index1=from_integer(1, int_type); - const exprt charx=from_integer('x', char_type); - const exprt index4=from_integer(4, int_type); - const exprt chary=from_integer('y', char_type); - const exprt index100=from_integer(100, int_type); - const exprt char0=from_integer('0', char_type); - const exprt index2=from_integer(2, int_type); + const typet char_type = unsignedbv_typet(16); + const typet int_type = signedbv_typet(32); + const exprt index1 = from_integer(1, int_type); + const exprt charx = from_integer('x', char_type); + const exprt index4 = from_integer(4, int_type); + const exprt chary = from_integer('y', char_type); + const exprt index100 = from_integer(100, int_type); + const exprt char0 = from_integer('0', char_type); + const exprt index2 = from_integer(2, int_type); const exprt charz = from_integer('z', char_type); array_typet array_type(char_type, infinity_exprt(int_type)); @@ -52,5 +54,5 @@ SCENARIO("concretize_array_expression", array_exprt expected( {charx, charx, chary, chary, chary, charz, charz}, array_type); to_array_type(expected.type()).size() = from_integer(7, int_type); - REQUIRE(concrete==expected); + REQUIRE(concrete == expected); } diff --git a/unit/solvers/refinement/string_refinement/module_dependencies.txt b/unit/solvers/strings/string_refinement/module_dependencies.txt similarity index 77% rename from unit/solvers/refinement/string_refinement/module_dependencies.txt rename to unit/solvers/strings/string_refinement/module_dependencies.txt index 863836fb0c3..dc9eb355784 100644 --- a/unit/solvers/refinement/string_refinement/module_dependencies.txt +++ b/unit/solvers/strings/string_refinement/module_dependencies.txt @@ -1,4 +1,5 @@ solvers/refinement +solvers/strings string_refinement testing-utils util diff --git a/unit/solvers/refinement/string_refinement/sparse_array.cpp b/unit/solvers/strings/string_refinement/sparse_array.cpp similarity index 95% rename from unit/solvers/refinement/string_refinement/sparse_array.cpp rename to unit/solvers/strings/string_refinement/sparse_array.cpp index 99b01f52848..fd460e104ec 100644 --- a/unit/solvers/refinement/string_refinement/sparse_array.cpp +++ b/unit/solvers/strings/string_refinement/sparse_array.cpp @@ -9,14 +9,16 @@ Author: Diffblue Ltd. #include +#include + #include -#include #include +#include #include -#include + #include -SCENARIO("sparse_array", "[core][solvers][refinement][string_refinement]") +SCENARIO("sparse_array", "[core][solvers][strings][string_refinement]") { GIVEN("`ARRAY_OF(0) WITH [4:=x] WITH [1:=y] WITH [100:=z]`") { diff --git a/unit/solvers/strings/string_refinement/substitute_array_list.cpp b/unit/solvers/strings/string_refinement/substitute_array_list.cpp new file mode 100644 index 00000000000..aa98a14f73a --- /dev/null +++ b/unit/solvers/strings/string_refinement/substitute_array_list.cpp @@ -0,0 +1,55 @@ +/*******************************************************************\ + +Module: Unit tests for get_numeric_value_from_character in + solvers/refinement/string_constraint_generator_valueof.cpp + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include + +SCENARIO("substitute_array_list", "[core][solvers][strings][string_refinement]") +{ + const typet char_type = unsignedbv_typet(16); + const typet int_type = signedbv_typet(32); + const array_typet array_type(char_type, infinity_exprt(int_type)); + const exprt index0 = from_integer(0, int_type); + const exprt charx = from_integer('x', char_type); + const exprt index1 = from_integer(1, int_type); + const exprt chary = from_integer('y', char_type); + const exprt index100 = from_integer(100, int_type); + + // arr is `array-list [ 0 , 'x' , 1 , 'y' , 2 , 'z']` + array_list_exprt arr( + {index0, charx, index1, chary, index100, from_integer('z', char_type)}, + array_type); + + // Max length is 2, so index 2 should get ignored. + const exprt subst = substitute_array_lists(arr, 2); + + // Check that `subst = e1 WITH [1:='y']` + REQUIRE(subst.id() == ID_with); + REQUIRE(subst.operands().size() == 3); + const exprt &e1 = subst.op0(); + REQUIRE(subst.op1() == index1); + REQUIRE(subst.op2() == chary); + + // Check that `e1 = e2 WITH [0:='x']` + REQUIRE(e1.id() == ID_with); + REQUIRE(e1.operands().size() == 3); + const exprt &e2 = e1.op0(); + REQUIRE(e1.op1() == index0); + REQUIRE(e1.op2() == charx); + + // Check that `e1 = ARRAY_OF 0` + REQUIRE(e2.id() == ID_array_of); + REQUIRE(e2.operands().size() == 1); + REQUIRE(e2.op0() == from_integer(0, char_type)); +} diff --git a/unit/solvers/refinement/string_refinement/union_find_replace.cpp b/unit/solvers/strings/string_refinement/union_find_replace.cpp similarity index 94% rename from unit/solvers/refinement/string_refinement/union_find_replace.cpp rename to unit/solvers/strings/string_refinement/union_find_replace.cpp index 85884f9d7c3..564ec973bcf 100644 --- a/unit/solvers/refinement/string_refinement/union_find_replace.cpp +++ b/unit/solvers/strings/string_refinement/union_find_replace.cpp @@ -9,13 +9,14 @@ Author: Diffblue Ltd. #include +#include + #include #include -#include #include -#include +#include -SCENARIO("union_find_replace", "[core][solvers][refinement][string_refinement]") +SCENARIO("union_find_replace", "[core][solvers][strings][string_refinement]") { GIVEN("An empty dictionary") {