From a630bb7da7faec6100c6845a26afd42ab44a5490 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 13 Apr 2018 07:19:47 +0100 Subject: [PATCH 01/14] Correct bound in test with long string To make the solver abort the length has to be strictly greater than 2^26. --- regression/jbmc-strings/long_string/Test.class | Bin 985 -> 985 bytes regression/jbmc-strings/long_string/Test.java | 4 +++- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/regression/jbmc-strings/long_string/Test.class b/regression/jbmc-strings/long_string/Test.class index de6b488b03b1fb4093bf83ec7dc0a8eec3ef3a01..9442a3c1cf466c5158a588f53da0901a688f5f87 100644 GIT binary patch delta 39 scmcb~ev^HJ4m0E8$-2yzqRI>s3@Qwg45~m<4M=J-7&B;1u4aw{0IkjkRsaA1 delta 39 tcmcb~ev^HJ4m0DT$-2yzqKXU>3`z`=49W~DK&Z-~&S1=-F}a#K4gjqC2T1?` 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; From 5b3a1a410df2e5f6041d4ac77aa4146904b0097e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 1 Mar 2018 13:40:46 +0000 Subject: [PATCH 02/14] Remove unnecessary replace_expr This is already done in add_lemma. --- src/solvers/refinement/string_refinement.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index c2685dc6202..dd384135af3 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -723,11 +723,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); }; From b0c6528dcbfd380340f7429035d874296276c0e5 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 26 Feb 2018 08:28:32 +0000 Subject: [PATCH 03/14] Use boolbvt for getting counter examples We use this counter examples in the string solver but the formula given there don't use arrays so it is enough to use boolbvt. --- src/solvers/refinement/string_refinement.cpp | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index dd384135af3..2356acc6ddf 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -2168,14 +2168,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) From 5fde05a36ee63b4b9f3368be1cfa227fcac38b02 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 08:54:10 +0000 Subject: [PATCH 04/14] Use string-max-length as default max input-length Having input string longer than string-max-length does not make sense as the solver will not know how to analyse them. So when string-max-input-length is not specified we can use string-max-length instead. --- src/java_bytecode/java_bytecode_language.cpp | 4 ++++ 1 file changed, 4 insertions(+) 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")); From 56e7b37a49f84dd0c039d2016f25424e4a0a3bfe Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 12 Apr 2018 19:09:01 +0100 Subject: [PATCH 05/14] Make get_array return nil for long strings Instead of aborting the program when the string is too long, we consider this happened because of some invalid object, and return nil as a model of the array. Access to this invalid object is prevented by other part of the code and should not occur in the trace. --- .../jbmc-strings/long_string/test_abort.desc | 9 +++++---- src/solvers/refinement/string_refinement.cpp | 17 +++++++++++------ 2 files changed, 16 insertions(+), 10 deletions(-) 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/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 2356acc6ddf..e358cade7b2 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -933,12 +933,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( From ff25fe256753218a74ac4d780b14ee3e0abc5bf1 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 12 Apr 2018 19:03:00 +0100 Subject: [PATCH 06/14] Weaken invariant for nil exprt as model of array nil_exprt happens when the underlying solver has no formula talking about the array --- src/solvers/refinement/string_refinement.cpp | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index e358cade7b2..3c081bf1adc 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1123,9 +1123,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)) @@ -1138,7 +1135,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 @@ -2121,9 +2123,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); } From 1d4f26ccc0fb1fb38bb2ea43ce841af657d98b06 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 12 Apr 2018 18:54:45 +0100 Subject: [PATCH 07/14] Assign 0 to string length for null Java String 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 of the string_exprt is set to something reasonable. --- src/java_bytecode/java_string_library_preprocess.cpp | 11 ++++++++--- .../convert_exprt_to_string_exprt.cpp | 5 +++-- 2 files changed, 11 insertions(+), 5 deletions(-) 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/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; From 2154047f32e1e652b893f4e403c8968532a648b0 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 19 Feb 2018 15:43:15 +0000 Subject: [PATCH 08/14] Get rid of default axioms for strings These default axioms where too strict and where applied even for strings that may never be created in the actual program. This could for instance lead to problematic contradiction for a Java object which could be casted either to a string or an int: the axiom added there would apply both on the string and on the integer. --- .../refinement/string_constraint_generator.h | 1 - .../string_constraint_generator_main.cpp | 29 +++---------------- 2 files changed, 4 insertions(+), 26 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 0beb04b766f..1102011302a 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -184,7 +184,6 @@ class string_constraint_generatort final 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( diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 72cb6a97120..db60ef1e786 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -172,7 +172,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 +278,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 +318,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,13 +387,14 @@ 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 +/// \todo This should be replaced +/// by array_poolt.make_char_array_for_char_pointer 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); + created_strings.insert(array); return array; } From d726577fe3f1a81da4114a594c44314ddbe4eb31 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 16 Apr 2018 08:21:37 +0100 Subject: [PATCH 09/14] Make char_array_of_pointer return a reference --- src/solvers/refinement/string_constraint_generator.h | 2 +- src/solvers/refinement/string_constraint_generator_main.cpp | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 1102011302a..d9d69abf325 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -181,7 +181,7 @@ 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); exprt axiom_for_is_positive_index(const exprt &x); diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index db60ef1e786..41f7cf193d7 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -389,13 +389,11 @@ 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 array_poolt.make_char_array_for_char_pointer -array_string_exprt string_constraint_generatort::char_array_of_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); - created_strings.insert(array); - return array; + return *created_strings.insert(array_pool.find(pointer, length)).first; } array_string_exprt array_poolt::find(const refined_string_exprt &str) From b83182f82291542a11de6a6298ba518da89c6161 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 19 Feb 2018 15:45:44 +0000 Subject: [PATCH 10/14] Get rid of string_max_length field In constraint generator, this was used for adding default axioms but is no longer used. --- src/cbmc/cbmc_solvers.cpp | 2 +- .../refinement/string_constraint_generator.h | 10 +------- .../string_constraint_generator_main.cpp | 6 ++--- src/solvers/refinement/string_refinement.cpp | 23 +++++++++++-------- src/solvers/refinement/string_refinement.h | 3 ++- .../instantiate_not_contains.cpp | 18 +++++---------- 6 files changed, 25 insertions(+), 37 deletions(-) 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/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index d9d69abf325..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. @@ -401,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 41f7cf193d7..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) { } diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 3c081bf1adc..52539307f0f 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -166,11 +166,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)) { } @@ -734,13 +737,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); @@ -778,13 +781,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); @@ -2143,7 +2146,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)) diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 0fd5dbc8f5a..f33c1bcf0b0 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -43,11 +43,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 +69,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/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()); From 0e8a8634e1f1bf67d331467f9981182708aa9754 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 22 Feb 2018 12:13:48 +0000 Subject: [PATCH 11/14] Add test for generics array and strings This adds an int greater than string-max-length in a generic array. This is to check that TG-2138 is fixed. Before the issue was solved setting the array to 101 was in contradiction with default axioms added by the string solver. --- .../IntegerTests.class | Bin 0 -> 834 bytes .../IntegerTests.java | 44 ++++++++++++++++++ .../max-length-generic-array/MyGenSet.class | Bin 0 -> 501 bytes .../max-length-generic-array/MySet.class | Bin 0 -> 446 bytes .../max-length-generic-array/test.desc | 19 ++++++++ .../max-length-generic-array/test_gen.desc | 20 ++++++++ 6 files changed, 83 insertions(+) create mode 100644 regression/jbmc-strings/max-length-generic-array/IntegerTests.class create mode 100644 regression/jbmc-strings/max-length-generic-array/IntegerTests.java create mode 100644 regression/jbmc-strings/max-length-generic-array/MyGenSet.class create mode 100644 regression/jbmc-strings/max-length-generic-array/MySet.class create mode 100644 regression/jbmc-strings/max-length-generic-array/test.desc create mode 100644 regression/jbmc-strings/max-length-generic-array/test_gen.desc 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 0000000000000000000000000000000000000000..6120bff5bb6f256912ddb4120be2d604bb633a6e GIT binary patch literal 834 zcmaKq&2G~`6ot=?V^3_{Hlb~x^p6%=>;w}2c10{e0#!=rB2}e^)g(+SmtZ5usgy_I zEsBI_1rlP1#4{npozx~~gBLS*?s(33&z<@C`^z@~kMYRCES3dU92Br@^ROzg=3pH+ zb!NlCCT#hUXs;iqE4riZIs-LiK9&uBYOC*&A@i zP1G=Hk6)^=qY{GWwNB)zYz}02+}sTlb*$nYKbLzJMFS#&#eMZ6(4b1Hw$Hp_LqlB5p-d=cbQeBqgoW2RTvmcW-NjwpbJ0Lk;J#iw zAeikj!}P&5z4MU$UBCN}a@s_#*Ujrqn_JC`WEj7T4b1Sf(4PUmPLz49@M@K3 z;@Pa7gFbRVxXPn7N%F;D9t#}nUlkuM@Z6~VfJtXxQ8+w@(W-w!@jFbTtS(@6>b1`h zA5bb@pmb*Fflm}BnpKz_7g^inQY@@MaQ{nKlZc!svKVXi|nPydWN(a>1gDY e9MAn9&t;OfK8q!`z0Jm_ymf)=Y;I{%;*CH4c&lXq literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..e92e43fee856008bdc97ae12d7bab364c7cd6c44 GIT binary patch literal 501 zcmZWl%TB^T6g|_Hr-c>~1w`YrU?Rr2Lc+$NF#%naxRBLQC!~l)`!L~C{0BBBJ`xj+ zYd^|(M_CwI%$HM^VP51j-CC?)!YokneX!{EpYh z+#A-<1|#8w2Mj6O9eO;Be8Hggdu@W^P1ke77K3V4&j~%8TvF2LxSlwTt_Q;J@xhpo zq%-kC?s@@3!CI_cymklj-=4(7(F7=pCV6zyc=Xm zLNes-QY<-U?FFo+y+Qea`ULHPForDIEL5^ZXehxznS28#sie9=Iax2aU3-M4?mZ)R kkC--7X9OyLp!Hr6->{*?ZMo1hN} z>Id|rqBAKZ)Z$*=J?EZt5AXBq?E}CbR&AJAu&|gx3Pl?lN*2l%mIP8VisVS3cv%84nJ|R=x4P}pkO0$6`Y|U+9jelYCdjyMy>>7(ViOlh}%{k$+-YbM>yhD42 z{zyQ;VV{T2z77K$oHvt2ViV~;xx}oni5wmB HKTCygXD3y! literal 0 HcmV?d00001 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 From 132a26b6a4f9a31dbb6713384aab625366e5a1a9 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 23 Feb 2018 09:51:53 +0000 Subject: [PATCH 12/14] Add tests showing the effect on string-max-length These tests show how the result of the solver can depend on the string-max-input-length and string-max-length parameters. --- regression/jbmc-strings/max-length/Test.class | Bin 0 -> 1064 bytes regression/jbmc-strings/max-length/Test.java | 37 ++++++++++++++++++ regression/jbmc-strings/max-length/test1.desc | 6 +++ regression/jbmc-strings/max-length/test2.desc | 6 +++ regression/jbmc-strings/max-length/test3.desc | 6 +++ regression/jbmc-strings/max-length/test4.desc | 11 ++++++ 6 files changed, 66 insertions(+) create mode 100644 regression/jbmc-strings/max-length/Test.class create mode 100644 regression/jbmc-strings/max-length/Test.java create mode 100644 regression/jbmc-strings/max-length/test1.desc create mode 100644 regression/jbmc-strings/max-length/test2.desc create mode 100644 regression/jbmc-strings/max-length/test3.desc create mode 100644 regression/jbmc-strings/max-length/test4.desc diff --git a/regression/jbmc-strings/max-length/Test.class b/regression/jbmc-strings/max-length/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..0bc43cd0bdbcf889136c6b16a07dfa40f3004bb0 GIT binary patch literal 1064 zcmZva?N8HC6vm&sb?ep@_JWKz+2nm2$P`hd5*4Q=L{JmZMEqjuno%4b={jQKf5I2V zFMdW7Ae!JeP5hgT@wsJeF)U4QZ_hpbJ?A{9zyE$a0Wgo78oH2)B8IGnOBe|v{@}if zQ4JwvWMoXkI3_eEOv+_SMNUH=1r^f*J>y2bZn>UabLtQ6y0KBU$^v3tAiQ8Zws%(` zn9IKuP)fD3B@kb>9qVahd&6?qWHJfnre(feG2SgXI}LByaw^`Yz*KH|%h)xFRl}(i zS3TEuDtFFDB)DtUGvxO>ORLtwR zjvE4rHsIODmSuYXg-*Msk=3RrG;)crX3a4TrcQRSD1W{`fq|M^DVjTOZP#*(rRV;$ z1vfVhcagMo2ij7;#EG?wELAydrk1U`?ONql)0}|U-~kI<#|ZzCF8)~}(J$@dE(G?4 zB-a$*hWQjSS~!9@kcsHw8uo(%5os6qGW7)lynxBVPpH$spd5TbU=IU@Lj>el{^cr7YK581zesLE-TqWK|wVcre&3Z5BGBfYd4K9rK))|1bdeGP4F3Zv9L;n9 literal 0 HcmV?d00001 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. From 05b924ca35c4239856e4bc4db30686589e866f6f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 16 Apr 2018 08:02:12 +0100 Subject: [PATCH 13/14] Deprecate string-max-length option --- src/cbmc/cbmc_parse_options.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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(*) From b59a4535a92a62207fddca863f6e8af8b36a46e6 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 16 Apr 2018 08:27:57 +0100 Subject: [PATCH 14/14] Move MAX_CONCRETE_STRING_SIZE definition to magic --- src/solvers/refinement/string_refinement.cpp | 1 + src/solvers/refinement/string_refinement.h | 2 -- src/util/magic.h | 2 ++ 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 52539307f0f..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, diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index f33c1bcf0b0..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 { 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