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 diff --git a/jbmc/regression/strings-smoke-tests/java_intern/test.desc b/jbmc/regression/strings-smoke-tests/java_intern/test.desc index d7afd59f09..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 +--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 894615c0a9..defb553cae 100644 Binary files a/jbmc/regression/strings-smoke-tests/java_intern/test_intern.class and b/jbmc/regression/strings-smoke-tests/java_intern/test_intern.class differ diff --git a/jbmc/regression/strings-smoke-tests/java_intern/test_intern.java b/jbmc/regression/strings-smoke-tests/java_intern/test_intern.java index b8abb9f1f2..c6b5556049 100644 --- a/jbmc/regression/strings-smoke-tests/java_intern/test_intern.java +++ b/jbmc/regression/strings-smoke-tests/java_intern/test_intern.java @@ -1,11 +1,26 @@ public class test_intern { - public static void main() - { - String s1 = "abc"; - String s3 = "abc"; - String x = s1.intern(); - String y = s3.intern(); - assert(x == y); + public static void testPass() + { + // Arrange + String s1 = "abc"; + String s2 = "abc"; + // Act + String x = s1.intern(); + String y = s2.intern(); + // Assert + assert(x == y); + } + + public static void testFail() + { + // Arrange + String s1 = "abc"; + String s2 = "abd"; + // Act + String x = s1.intern(); + String y = s2.intern(); + // Assert + assert(x == y); } } diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 465359614c..d4e5b52658 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)