diff --git a/regression/jbmc-strings/long_string/Test.class b/regression/jbmc-strings/long_string/Test.class index de6b488b03b..9442a3c1cf4 100644 Binary files a/regression/jbmc-strings/long_string/Test.class and b/regression/jbmc-strings/long_string/Test.class differ diff --git a/regression/jbmc-strings/long_string/Test.java b/regression/jbmc-strings/long_string/Test.java index 63b0d69babc..5decee61931 100644 --- a/regression/jbmc-strings/long_string/Test.java +++ b/regression/jbmc-strings/long_string/Test.java @@ -30,7 +30,9 @@ public static void checkAbort(String s, String t) { String u = s.concat(t); // Filter out - if(u.length() < 67_108_864) + // 67_108_864 corresponds to the maximum length for which the solver + // will concretize the string. + if(u.length() <= 67_108_864) return; if(CProverString.charAt(u, 2_000_000) != 'b') return; diff --git a/regression/jbmc-strings/long_string/test_abort.desc b/regression/jbmc-strings/long_string/test_abort.desc index 22074e1ed1e..8daa50acd1a 100644 --- a/regression/jbmc-strings/long_string/test_abort.desc +++ b/regression/jbmc-strings/long_string/test_abort.desc @@ -1,9 +1,10 @@ CORE Test.class ---refine-strings --function Test.checkAbort -^EXIT=6$ +--refine-strings --function Test.checkAbort --trace +^EXIT=10$ ^SIGNAL=0$ +dynamic_object[0-9]*=\(assignment removed\) -- -- -This tests should abort, because concretizing a string of the required -length may take to much memory. +This tests that the object does not appear in the trace, because concretizing +a string of the required length may take too much memory. diff --git a/regression/jbmc-strings/max-length-generic-array/IntegerTests.class b/regression/jbmc-strings/max-length-generic-array/IntegerTests.class new file mode 100644 index 00000000000..6120bff5bb6 Binary files /dev/null and b/regression/jbmc-strings/max-length-generic-array/IntegerTests.class differ diff --git a/regression/jbmc-strings/max-length-generic-array/IntegerTests.java b/regression/jbmc-strings/max-length-generic-array/IntegerTests.java new file mode 100644 index 00000000000..c57b3e19be8 --- /dev/null +++ b/regression/jbmc-strings/max-length-generic-array/IntegerTests.java @@ -0,0 +1,44 @@ +public class IntegerTests { + + public static Boolean testMyGenSet(Integer key) { + if (key == null) return null; + MyGenSet ms = new MyGenSet<>(); + ms.array[0] = 101; + if (ms.contains(key)) return true; + return false; + } + + public static Boolean testMySet(Integer key) { + if (key == null) return null; + MySet ms = new MySet(); + ms.array[0] = 101; + if (ms.contains(key)) return true; + return false; + } + +} + +class MyGenSet { + E[] array; + @SuppressWarnings("unchecked") + MyGenSet() { + array = (E[]) new Object[1]; + } + boolean contains(E o) { + if (o.equals(array[0])) + return true; + return false; + } +} + +class MySet { + Integer[] array; + MySet() { + array = new Integer[1]; + } + boolean contains(Integer o) { + if (o.equals(array[0])) + return true; + return false; + } +} diff --git a/regression/jbmc-strings/max-length-generic-array/MyGenSet.class b/regression/jbmc-strings/max-length-generic-array/MyGenSet.class new file mode 100644 index 00000000000..e92e43fee85 Binary files /dev/null and b/regression/jbmc-strings/max-length-generic-array/MyGenSet.class differ diff --git a/regression/jbmc-strings/max-length-generic-array/MySet.class b/regression/jbmc-strings/max-length-generic-array/MySet.class new file mode 100644 index 00000000000..e890519fb8b Binary files /dev/null and b/regression/jbmc-strings/max-length-generic-array/MySet.class differ diff --git a/regression/jbmc-strings/max-length-generic-array/test.desc b/regression/jbmc-strings/max-length-generic-array/test.desc new file mode 100644 index 00000000000..3862a4978b3 --- /dev/null +++ b/regression/jbmc-strings/max-length-generic-array/test.desc @@ -0,0 +1,19 @@ +CORE +IntegerTests.class +-refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMySet --cover location +^EXIT=0$ +^SIGNAL=0$ +coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 1 .* SATISFIED +coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 3 .* SATISFIED +coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 4 .* SATISFIED +coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 6 .* SATISFIED +coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 7 .* SATISFIED +coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 12 .* SATISFIED +coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 13 .* SATISFIED +coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 16 .* SATISFIED +coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 17 .* SATISFIED +coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 21 .* SATISFIED +coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 19 .* SATISFIED +coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 20 .* SATISFIED +coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 22 .* SATISFIED +coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 23 .* SATISFIED diff --git a/regression/jbmc-strings/max-length-generic-array/test_gen.desc b/regression/jbmc-strings/max-length-generic-array/test_gen.desc new file mode 100644 index 00000000000..ec123c9a16a --- /dev/null +++ b/regression/jbmc-strings/max-length-generic-array/test_gen.desc @@ -0,0 +1,20 @@ +CORE +IntegerTests.class +-refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMyGenSet --cover location +^EXIT=0$ +^SIGNAL=0$ +coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 1 .* SATISFIED +coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 3 .* SATISFIED +coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 4 .* SATISFIED +coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 6 .* SATISFIED +coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 7 .* SATISFIED +coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 10 .* SATISFIED +coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 13 .* SATISFIED +coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 14 .* SATISFIED +coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 17 .* SATISFIED +coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 18 .* SATISFIED +coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 22 .* SATISFIED +coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 20 .* SATISFIED +coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 21 .* SATISFIED +coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 23 .* SATISFIED +coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 24 .* SATISFIED diff --git a/regression/jbmc-strings/max-length/Test.class b/regression/jbmc-strings/max-length/Test.class new file mode 100644 index 00000000000..0bc43cd0bdb Binary files /dev/null and b/regression/jbmc-strings/max-length/Test.class differ diff --git a/regression/jbmc-strings/max-length/Test.java b/regression/jbmc-strings/max-length/Test.java new file mode 100644 index 00000000000..e947169506d --- /dev/null +++ b/regression/jbmc-strings/max-length/Test.java @@ -0,0 +1,37 @@ +public class Test { + + static void checkMaxInputLength(String arg1, String arg2) { + // Filter + if (arg1 == null || arg2 == null) + return; + + // The validity of this depends on string-max-input-length + assert arg1.length() + arg2.length() < 1_000_000; + } + + static void checkMaxLength(String arg1, String arg2) { + // Filter + if (arg1 == null || arg2 == null) + return; + + if(arg1.length() + arg2.length() < 4_001) + return; + + // Act + String s = arg1.concat(arg2); + + // When string-max-length is smaller than 4_000 this will + // always be the case + assert org.cprover.CProverString.charAt(s, 4_000) == '?'; + } + + static void main(String argv[]) { + // Filter + if (argv.length < 2) + return; + + // Act + checkMaxInputLength(argv[0], argv[1]); + checkMaxLength(argv[0], argv[1]); + } +} diff --git a/regression/jbmc-strings/max-length/test1.desc b/regression/jbmc-strings/max-length/test1.desc new file mode 100644 index 00000000000..1cdaf80b01e --- /dev/null +++ b/regression/jbmc-strings/max-length/test1.desc @@ -0,0 +1,6 @@ +CORE +Test.class +--refine-strings --verbosity 10 --string-max-input-length 499999 --function Test.checkMaxInputLength +^EXIT=0$ +^SIGNAL=0$ +assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: SUCCESS diff --git a/regression/jbmc-strings/max-length/test2.desc b/regression/jbmc-strings/max-length/test2.desc new file mode 100644 index 00000000000..e705d18deda --- /dev/null +++ b/regression/jbmc-strings/max-length/test2.desc @@ -0,0 +1,6 @@ +CORE +Test.class +--refine-strings --verbosity 10 --string-max-input-length 500000 --function Test.checkMaxInputLength +^EXIT=10$ +^SIGNAL=0$ +assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: FAILURE diff --git a/regression/jbmc-strings/max-length/test3.desc b/regression/jbmc-strings/max-length/test3.desc new file mode 100644 index 00000000000..ab4c3b62db5 --- /dev/null +++ b/regression/jbmc-strings/max-length/test3.desc @@ -0,0 +1,6 @@ +CORE +Test.class +--refine-strings --verbosity 10 --string-max-length 4001 --function Test.checkMaxLength +^EXIT=10$ +^SIGNAL=0$ +assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: FAILURE diff --git a/regression/jbmc-strings/max-length/test4.desc b/regression/jbmc-strings/max-length/test4.desc new file mode 100644 index 00000000000..b1cdfc3d39c --- /dev/null +++ b/regression/jbmc-strings/max-length/test4.desc @@ -0,0 +1,11 @@ +CORE +Test.class +--refine-strings --verbosity 10 --string-max-length 4000 --function Test.checkMaxLength +^SIGNAL=0$ +-- +^EXIT=0$ +assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: SUCCESS +-- +The solver may give an ERROR because the value of string-max-length is too +small to give an answer about the assertion. +So we just check that the answer is not success. diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 5962d65ecc9..e7189f965d1 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -999,8 +999,9 @@ void cbmc_parse_optionst::help() " --refine use refinement procedure (experimental)\n" " --refine-strings use string refinement (experimental)\n" " --string-printable add constraint that strings are printable (experimental)\n" // NOLINT(*) - " --string-max-length add constraint on the length of strings\n" // NOLINT(*) " --string-max-input-length add constraint on the length of input strings\n" // NOLINT(*) + " --string-max-length add constraint on the length of strings" + " (deprecated: use string-max-input-length instead)\n" // NOLINT(*) " --outfile filename output formula to given file\n" " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*) " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*) diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index 557bf1ca3b7..ed5787af6d3 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -177,7 +177,7 @@ std::unique_ptr cbmc_solverst::get_string_refinement() info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT; info.ui=ui; if(options.get_bool_option("string-max-length")) - info.string_max_length=options.get_signed_int_option("string-max-length"); + info.max_string_length = options.get_signed_int_option("string-max-length"); info.trace=options.get_bool_option("trace"); if(options.get_bool_option("max-node-refinement")) info.max_node_refinement= diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index a139b75c613..967113657ce 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -55,6 +55,10 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) if(cmd.isset("string-max-input-length")) object_factory_parameters.max_nondet_string_length= std::stoi(cmd.get_value("string-max-input-length")); + else if(cmd.isset("string-max-length")) + object_factory_parameters.max_nondet_string_length = + std::stoi(cmd.get_value("string-max-length")); + object_factory_parameters.string_printable = cmd.isset("string-printable"); if(cmd.isset("java-max-vla-length")) max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length")); diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 009882d2dab..b759b72f471 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -877,7 +877,7 @@ codet java_string_library_preprocesst::code_assign_string_expr_to_java_string( /// \param symbol_table: symbol table /// \param [out] code: code block that gets appended the following code: /// ~~~~~~~~~~~~~~~~~~~~~~ -/// lhs.length=rhs->length +/// lhs.length = rhs==null ? 0 : rhs->length /// lhs.data=rhs->data /// ~~~~~~~~~~~~~~~~~~~~~~ void java_string_library_preprocesst::code_assign_java_string_to_string_expr( @@ -898,8 +898,13 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr( const dereference_exprt deref = checked_dereference(rhs, deref_type); - // Fields of the string object - const exprt rhs_length = get_length(deref, symbol_table); + // Although we should not reach this code if rhs is null, the association + // `pointer -> length` is added to the solver anyway, so we have to make sure + // the length is set to something reasonable. + const auto rhs_length = if_exprt( + equal_exprt(rhs, null_pointer_exprt(to_pointer_type(rhs.type()))), + from_integer(0, lhs.length().type()), + get_length(deref, symbol_table)); // Assignments code.add(code_assignt(lhs.length(), rhs_length), loc); diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 0beb04b766f..5a921d11adc 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -94,14 +94,7 @@ class string_constraint_generatort final // Used by format function class format_specifiert; - /// Arguments pack for the string_constraint_generator constructor - struct infot - { - /// Max length of non-deterministic strings - size_t string_max_length=std::numeric_limits::max(); - }; - - string_constraint_generatort(const infot& info, const namespacet& ns); + explicit string_constraint_generatort(const namespacet &ns); /// Axioms are of three kinds: universally quantified string constraint, /// not contains string constraints and simple formulas. @@ -181,10 +174,9 @@ class string_constraint_generatort final static constant_exprt constant_char(int i, const typet &char_type); - array_string_exprt + const array_string_exprt & char_array_of_pointer(const exprt &pointer, const exprt &length); - void add_default_axioms(const array_string_exprt &s); exprt axiom_for_is_positive_index(const exprt &x); void add_constraint_on_characters( @@ -402,7 +394,6 @@ class string_constraint_generatort final // MEMBERS public: - const size_t max_string_length; // Used to store information about witnesses for not_contains constraints std::map witness; private: diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 72cb6a97120..3b3dc66c846 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -28,10 +28,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include -string_constraint_generatort::string_constraint_generatort( - const string_constraint_generatort::infot &info, - const namespacet &ns) - : array_pool(fresh_symbol), max_string_length(info.string_max_length), ns(ns) +string_constraint_generatort::string_constraint_generatort(const namespacet &ns) + : array_pool(fresh_symbol), ns(ns) { } @@ -172,7 +170,6 @@ array_string_exprt string_constraint_generatort::fresh_string( symbol_exprt content = fresh_symbol("string_content", array_type); array_string_exprt str = to_array_string_expr(content); created_strings.insert(str); - add_default_axioms(str); return str; } @@ -279,7 +276,7 @@ exprt string_constraint_generatort::associate_array_to_pointer( const exprt &pointer_expr = f.arguments()[1]; array_pool.insert(pointer_expr, array_expr); - add_default_axioms(to_array_string_expr(array_expr)); + created_strings.emplace(to_array_string_expr(array_expr)); return from_integer(0, f.type()); } @@ -319,27 +316,6 @@ void string_constraint_generatort::clear_constraints() not_contains_constraints.clear(); } -/// adds standard axioms about the length of the string and its content: * its -/// length should be positive * it should not exceed max_string_length * if -/// force_printable_characters is true then all characters should belong to the -/// range of ASCII characters between ' ' and '~' -/// \param s: a string expression -/// \return a string expression that is linked to the argument through axioms -/// that are added to the list -void string_constraint_generatort::add_default_axioms( - const array_string_exprt &s) -{ - // If `s` was already added we do nothing. - if(!created_strings.insert(s).second) - return; - - const exprt index_zero = from_integer(0, s.length().type()); - lemmas.push_back(s.axiom_for_length_ge(index_zero)); - - if(max_string_length!=std::numeric_limits::max()) - lemmas.push_back(s.axiom_for_length_le(max_string_length)); -} - /// Add constraint on characters of a string. /// /// This constraint is @@ -409,14 +385,13 @@ array_string_exprt array_poolt::find(const exprt &pointer, const exprt &length) } /// Adds creates a new array if it does not already exists -/// \todo This should be replaced by associate_char_array_to_char_pointer -array_string_exprt string_constraint_generatort::char_array_of_pointer( +/// \todo This should be replaced +/// by array_poolt.make_char_array_for_char_pointer +const array_string_exprt &string_constraint_generatort::char_array_of_pointer( const exprt &pointer, const exprt &length) { - const array_string_exprt array = array_pool.find(pointer, length); - add_default_axioms(array); - return array; + return *created_strings.insert(array_pool.find(pointer, length)).first; } array_string_exprt array_poolt::find(const refined_string_exprt &str) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index c2685dc6202..7a080dd361a 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -28,6 +28,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #include #include +#include static bool is_valid_string_constraint( messaget::mstreamt &stream, @@ -166,11 +167,14 @@ static bool validate(const string_refinementt::infot &info) return true; } -string_refinementt::string_refinementt(const infot &info, bool): - supert(info), - config_(info), - loop_bound_(info.refinement_bound), - generator(info, *info.ns) { } +string_refinementt::string_refinementt(const infot &info, bool) + : supert(info), + config_(info), + loop_bound_(info.refinement_bound), + max_string_length(info.max_string_length), + generator(*info.ns) +{ +} string_refinementt::string_refinementt(const infot &info): string_refinementt(info, validate(info)) { } @@ -723,11 +727,8 @@ decision_proceduret::resultt string_refinementt::dec_solve() generator.fresh_symbol("not_contains_witness", witness_type); } - for(exprt lemma : generator.get_lemmas()) - { - symbol_resolve.replace_expr(lemma); + for(const exprt &lemma : generator.get_lemmas()) add_lemma(lemma); - } // Initial try without index set const auto get = [this](const exprt &expr) { return this->get(expr); }; @@ -737,13 +738,13 @@ decision_proceduret::resultt string_refinementt::dec_solve() { bool satisfied; std::vector counter_examples; - std::tie(satisfied, counter_examples)=check_axioms( + std::tie(satisfied, counter_examples) = check_axioms( axioms, generator, get, debug(), ns, - generator.max_string_length, + max_string_length, config_.use_counter_example, supert::config_.ui, symbol_resolve); @@ -781,13 +782,13 @@ decision_proceduret::resultt string_refinementt::dec_solve() { bool satisfied; std::vector counter_examples; - std::tie(satisfied, counter_examples)=check_axioms( + std::tie(satisfied, counter_examples) = check_axioms( axioms, generator, get, debug(), ns, - generator.max_string_length, + max_string_length, config_.use_counter_example, supert::config_.ui, symbol_resolve); @@ -936,12 +937,17 @@ static optionalt get_array( if(n > MAX_CONCRETE_STRING_SIZE) { - stream << "(sr::get_array) long string (size=" << n << ")" << eom; - std::ostringstream msg; - msg << "consider reducing string-max-input-length so that no string " - << "exceeds " << MAX_CONCRETE_STRING_SIZE << " in length and make sure" - << " all functions returning strings are available in the classpath"; - throw string_refinement_invariantt(msg.str()); + stream << "(sr::get_array) long string (size " << format(arr.length()) + << " = " << n << ") " << format(arr) << eom; + stream << "(sr::get_array) consider reducing string-max-input-length so " + "that no string exceeds " + << MAX_CONCRETE_STRING_SIZE + << " in length and " + "make sure all functions returning strings are loaded" + << eom; + stream << "(sr::get_array) this can also happen on invalid object access" + << eom; + return nil_exprt(); } if( @@ -1121,9 +1127,6 @@ static exprt substitute_array_access( const bool left_propagate) { const exprt &array = index_expr.array(); - - if(array.id() == ID_symbol) - return index_expr; if(auto array_of = expr_try_dynamic_cast(array)) return array_of->op(); if(auto array_with = expr_try_dynamic_cast(array)) @@ -1136,7 +1139,12 @@ static exprt substitute_array_access( return substitute_array_access( *if_expr, index_expr.index(), symbol_generator, left_propagate); - UNREACHABLE; + 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())); + return index_expr; } /// Auxiliary function for substitute_array_access @@ -2119,9 +2127,11 @@ exprt string_refinementt::get(const exprt &expr) const } INVARIANT( - array.id() == ID_symbol, - "apart from symbols, array valuations can be interpreted as sparse " - "arrays"); + array.is_nil() || array.id() == ID_symbol, + std::string( + "apart from symbols, array valuations can be interpreted as " + "sparse arrays, id: ") + + id2string(array.id())); return index_exprt(array, index); } @@ -2137,7 +2147,7 @@ exprt string_refinementt::get(const exprt &expr) const if( const auto arr_model_opt = - get_array(super_get, ns, generator.max_string_length, debug(), arr)) + get_array(super_get, ns, max_string_length, debug(), arr)) return *arr_model_opt; if(generator.get_created_strings().count(arr)) @@ -2171,14 +2181,7 @@ static optionalt find_counter_example( const symbol_exprt &var) { satcheck_no_simplifiert sat_check; - bv_refinementt::infot info; - info.ns=&ns; - info.prop=&sat_check; - info.refine_arithmetic=true; - info.refine_arrays=true; - info.max_node_refinement=5; - info.ui=ui; - bv_refinementt solver(info); + boolbvt solver(ns, sat_check); solver << axiom; if(solver()==decision_proceduret::resultt::D_SATISFIABLE) diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 0fd5dbc8f5a..ec7892838ed 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -31,8 +31,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits::max() #define CHARACTER_FOR_UNKNOWN '?' -// Limit the size of strings in traces to 64M chars to avoid memout -#define MAX_CONCRETE_STRING_SIZE (1 << 26) class string_refinementt final: public bv_refinementt { @@ -43,11 +41,11 @@ class string_refinementt final: public bv_refinementt /// Concretize strings after solver is finished bool trace=false; bool use_counter_example=true; + std::size_t max_string_length; }; public: /// string_refinementt constructor arguments struct infot : public bv_refinementt::infot, - public string_constraint_generatort::infot, public configt { }; @@ -69,6 +67,7 @@ class string_refinementt final: public bv_refinementt const configt config_; std::size_t loop_bound_; + std::size_t max_string_length; string_constraint_generatort generator; // Simple constraints that have been given to the solver diff --git a/src/util/magic.h b/src/util/magic.h index 48c72436e2d..3d1c2ed8d90 100644 --- a/src/util/magic.h +++ b/src/util/magic.h @@ -10,5 +10,7 @@ const std::size_t CNF_DUMP_BLOCK_SIZE = 4096; const std::size_t MAX_FLATTENED_ARRAY_SIZE=1000; const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH = 16; +// Limit the size of strings in traces to 64M chars to avoid memout +const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26; #endif diff --git a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp index b292e445ae2..fb65105afbb 100644 --- a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp +++ b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp @@ -68,10 +68,11 @@ TEST_CASE("Convert exprt to string exprt") std::regex_replace(line, spaces, " "), numbers, "")); } - const std::vector reference_code = { // NOLINT + const std::vector reference_code = { + // NOLINT "char *cprover_string_content;", "int cprover_string_length;", - "cprover_string_length = a->length;", + "cprover_string_length = a == null ? 0 : a->length;", "cprover_string_content = a->data;"}; for(std::size_t i = 0; diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp index 3556cc26915..db6e28193c4 100644 --- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -195,8 +195,7 @@ SCENARIO("instantiate_not_contains", // Generating the corresponding axioms and simplifying, recording info symbol_tablet symtab; const namespacet empty_ns(symtab); - string_constraint_generatort::infot info; - string_constraint_generatort generator(info, ns); + string_constraint_generatort generator(ns); exprt res=generator.add_axioms_for_function_application(func); std::string axioms; std::vector nc_axioms; @@ -297,8 +296,7 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; const namespacet empty_ns(symtab); - string_constraint_generatort::infot info; - string_constraint_generatort generator(info, ns); + string_constraint_generatort generator(ns); generator.witness[vacuous]= generator.fresh_symbol("w", t.witness_type()); @@ -353,8 +351,7 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; const namespacet ns(symtab); - string_constraint_generatort::infot info; - string_constraint_generatort generator(info, ns); + string_constraint_generatort generator(ns); generator.witness[trivial]= generator.fresh_symbol("w", t.witness_type()); @@ -410,8 +407,7 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; const namespacet empty_ns(symtab); - string_constraint_generatort::infot info; - string_constraint_generatort generator(info, ns); + string_constraint_generatort generator(ns); generator.witness[trivial]= generator.fresh_symbol("w", t.witness_type()); @@ -470,8 +466,7 @@ SCENARIO("instantiate_not_contains", symbol_tablet symtab; const namespacet empty_ns(symtab); - string_constraint_generatort::infot info; - string_constraint_generatort generator(info, ns); + string_constraint_generatort generator(ns); generator.witness[trivial]= generator.fresh_symbol("w", t.witness_type()); @@ -527,8 +522,7 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; const namespacet empty_ns(symtab); - string_constraint_generatort::infot info; - string_constraint_generatort generator(info, ns); + string_constraint_generatort generator(ns); generator.witness[trivial]= generator.fresh_symbol("w", t.witness_type());