From 426ff72ec853cb48921bec9105fbf6a7caac5ebc Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 30 Apr 2019 08:23:48 +0100 Subject: [PATCH 1/4] Update submodule for diffblue/java-models-library#22 (String.intern) This contains a model for String.intern https://github.com/diffblue/java-models-library/pull/22 --- jbmc/lib/java-models-library | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library index 0e6413deb5..14e140fa7c 160000 --- a/jbmc/lib/java-models-library +++ b/jbmc/lib/java-models-library @@ -1 +1 @@ -Subproject commit 0e6413deb54cd90aa5578e88cd0ca9d4810d0b0d +Subproject commit 14e140fa7c6f72314777ac8bd3b69a2fb8e3246e From b7667ec9df764da61e280686f91f9ffc62d87345 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 30 Apr 2019 08:05:55 +0100 Subject: [PATCH 2/4] Add models to String.intern test This will become necessary when the String.intern implementation is moved to models. --- jbmc/regression/strings-smoke-tests/java_intern/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/regression/strings-smoke-tests/java_intern/test.desc b/jbmc/regression/strings-smoke-tests/java_intern/test.desc index d7afd59f09..a152083b00 100644 --- a/jbmc/regression/strings-smoke-tests/java_intern/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_intern/test.desc @@ -1,6 +1,6 @@ CORE test_intern.class ---max-nondet-string-length 1000 --function test_intern.main +--max-nondet-string-length 1000 --function test_intern.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --unwind 10 ^EXIT=0$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ From e6a5a11a4e0847953b16a4b89635d4247142cef8 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 18 Apr 2019 16:22:09 +0100 Subject: [PATCH 3/4] Remove cprover_string_intern handling in the solver This has never been tested and should rather be handled by the models, it is a Java specific feature. --- .../java_string_library_preprocess.cpp | 3 -- src/solvers/README.md | 1 - .../strings/string_constraint_generator.h | 10 ---- ...string_constraint_generator_comparison.cpp | 50 ------------------- .../string_constraint_generator_main.cpp | 2 - src/util/irep_ids.def | 1 - 6 files changed, 67 deletions(-) diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index cfba517519..17b70749d2 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1532,9 +1532,6 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_function ["java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]= ID_cprover_string_index_of_func; - cprover_equivalent_to_java_function - ["java::java.lang.String.intern:()Ljava/lang/String;"]= - ID_cprover_string_intern_func; cprover_equivalent_to_java_function ["java::java.lang.String.isEmpty:()Z"]= ID_cprover_string_is_empty_func; diff --git a/src/solvers/README.md b/src/solvers/README.md index fe6bebb445..5380b51c54 100644 --- a/src/solvers/README.md +++ b/src/solvers/README.md @@ -518,7 +518,6 @@ allocates a new string before calling a primitive. Pointer to char array association is now handled by `string_constraint_generatort`, there is no need for explicit conversion. - * `cprover_string_intern` : Never tested. * `cprover_string_is_empty` : Should use `cprover_string_length(s) == 0` instead. * `cprover_string_is_suffix` : Should use `cprover_string_is_prefix` with an diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h index c75c2827a8..cd6a11e8e8 100644 --- a/src/solvers/strings/string_constraint_generator.h +++ b/src/solvers/strings/string_constraint_generator.h @@ -71,13 +71,6 @@ public: make_array_pointer_association(const function_application_exprt &expr); private: - /// Add axioms corresponding to the String.intern java function - /// \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); - exprt associate_array_to_pointer(const function_application_exprt &f); exprt associate_length_to_array(const function_application_exprt &f); @@ -95,9 +88,6 @@ private: // To each string on which hash_code was called we associate a symbol // representing the return value of the hash_code function. std::map hash_code_of_string; - - // Pool used for the intern method - std::map intern_of_string; }; // Type used by primitives to signal errors diff --git a/src/solvers/strings/string_constraint_generator_comparison.cpp b/src/solvers/strings/string_constraint_generator_comparison.cpp index 0b4ce3b250..73ff7dbbff 100644 --- a/src/solvers/strings/string_constraint_generator_comparison.cpp +++ b/src/solvers/strings/string_constraint_generator_comparison.cpp @@ -297,53 +297,3 @@ std::pair add_axioms_for_compare_to( return {res, std::move(constraints)}; } - -/// Add axioms stating that the return value for two equal string should be the -/// same -/// \deprecated never tested -/// \param f: function application with one string argument -/// \return a string expression -DEPRECATED(SINCE(2017, 10, 5, "never tested")) -std::pair -string_constraint_generatort::add_axioms_for_intern( - const function_application_exprt &f) -{ - PRECONDITION(f.arguments().size() == 1); - 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 index_type = str.length().type(); - - auto pair = intern_of_string.insert( - std::make_pair(str, fresh_symbol("pool", return_type))); - const symbol_exprt intern = pair.first->second; - - // intern(str)=s_0 || s_1 || ... - // for each string s. - // intern(str)=intern(s) || |str|!=|s| - // || (|str|==|s| &&exists i<|s|. s[i]!=str[i]) - - exprt::operandst disj; - for(auto it : intern_of_string) - disj.push_back(equal_exprt(intern, it.second)); - intern_constraints.existential.push_back(disjunction(disj)); - - // WARNING: the specification may be incomplete or incorrect - for(auto it : intern_of_string) - if(it.second != str) - { - symbol_exprt i = fresh_symbol("index_intern", index_type); - intern_constraints.existential.push_back(or_exprt( - equal_exprt(it.second, intern), - or_exprt( - notequal_exprt(str.length(), it.first.length()), - and_exprt( - equal_exprt(str.length(), it.first.length()), - and_exprt( - notequal_exprt(str[i], it.first[i]), - and_exprt(length_gt(str, i), is_positive(i))))))); - } - - return {intern, std::move(intern_constraints)}; -} diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp index 566bb4241e..1dbff1de86 100644 --- a/src/solvers/strings/string_constraint_generator_main.cpp +++ b/src/solvers/strings/string_constraint_generator_main.cpp @@ -307,8 +307,6 @@ string_constraint_generatort::add_axioms_for_function_application( return add_axioms_for_delete_char_at(fresh_symbol, expr, array_pool); 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) - return add_axioms_for_intern(expr); 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) diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 414be9f190..06cee887e3 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -612,7 +612,6 @@ IREP_ID_ONE(cprover_string_endswith_func) IREP_ID_ONE(cprover_string_format_func) IREP_ID_ONE(cprover_string_hash_code_func) IREP_ID_ONE(cprover_string_index_of_func) -IREP_ID_ONE(cprover_string_intern_func) IREP_ID_ONE(cprover_string_insert_func) IREP_ID_ONE(cprover_string_insert_int_func) IREP_ID_ONE(cprover_string_insert_long_func) From 524c13ff2dc1dc3f9100e9bd1f020606d0b23656 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 30 Apr 2019 08:10:38 +0100 Subject: [PATCH 4/4] Improve test for String.intern We add a version of the test which should fail in addition to the one that should pass. --- .../strings-smoke-tests/java_intern/test.desc | 4 +-- .../java_intern/testFail.desc | 8 +++++ .../java_intern/test_intern.class | Bin 634 -> 779 bytes .../java_intern/test_intern.java | 29 +++++++++++++----- 4 files changed, 32 insertions(+), 9 deletions(-) create mode 100644 jbmc/regression/strings-smoke-tests/java_intern/testFail.desc diff --git a/jbmc/regression/strings-smoke-tests/java_intern/test.desc b/jbmc/regression/strings-smoke-tests/java_intern/test.desc index a152083b00..375ecdff2d 100644 --- a/jbmc/regression/strings-smoke-tests/java_intern/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_intern/test.desc @@ -1,8 +1,8 @@ CORE test_intern.class ---max-nondet-string-length 1000 --function test_intern.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --unwind 10 +--max-nondet-string-length 1000 --function test_intern.testPass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --unwind 10 ^EXIT=0$ ^SIGNAL=0$ -^\[.*assertion.1\].* line 9.* SUCCESS$ +^\[.*assertion.1\].* line 12.* SUCCESS$ -- non equal types diff --git a/jbmc/regression/strings-smoke-tests/java_intern/testFail.desc b/jbmc/regression/strings-smoke-tests/java_intern/testFail.desc new file mode 100644 index 0000000000..a72b013394 --- /dev/null +++ b/jbmc/regression/strings-smoke-tests/java_intern/testFail.desc @@ -0,0 +1,8 @@ +CORE +test_intern.class +--max-nondet-string-length 1000 --function test_intern.testFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --unwind 10 +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 24.* FAILURE$ +-- +non equal types diff --git a/jbmc/regression/strings-smoke-tests/java_intern/test_intern.class b/jbmc/regression/strings-smoke-tests/java_intern/test_intern.class index 894615c0a9ace0fcbbb8c5d1f6cf63d94ac49f49..defb553cae2717dcce068198c384e21d8a270f97 100644 GIT binary patch delta 458 zcmaKnF;Bu!6ot=g3$HB&p-2T3Q9)4?V`6Z3Ff7KzM4e4R1_B|*c5?9tFg0xc0cT^P ziG%JA#^2*0o>wEr#pLC_ckemxyZ3$=qvX!(=hHKQCN^x?D4HnQC}ZA&i3N#@jf5&L zN>ptuVOe4&+TL%NVK)em{2&lWABTRYf9PMF`0YVgq9zclEx$L2Mq6GQ83EmIcPKfi zW7RLRbWEf|dRd@^DiOold zJ7q+cF&P&HEabke;}@}es+2M{rR$K47NItOIH(coQYk=8m>3fI>0#Nz?6hYe8m9p2 zu6E$c@w=#B|B_vj^CTBY_DC)gR{D=@()zPaGaehrx#k0`8%X08hJFu2ZKnO%OwF2r M=Ip8cr5EdSU+~p4RR910 delta 345 zcmY+8KTE?<6vcn9`SX%A)wZ^2tj2#;2SEg>yMwqn=`Lx>P}CqclZzj~DRdK@okdV^ z@B{b-T>Tsl>P>`#yvM!o+;i?Z@7De@ciz8W-+(@w9xj1H$0KCkMbp(Rcvu9QMURLj z&2qkb5Skb9C{@&svv_!R6kndigY!hQlHYF!J~f3A4~Bw$R$24$sOFzhtC}U_>~xf7 z$yKW9`K+@s>8R^NExDlTVWE_lfkJGg&IpR6E9utO3+k~DGAq?Che}rKf6~c^+Pf*3 zu5cn38(WSROGh*=J+W^H(?#v#