diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library index 14e140fa7c6..42b32df3dd0 160000 --- a/jbmc/lib/java-models-library +++ b/jbmc/lib/java-models-library @@ -1 +1 @@ -Subproject commit 14e140fa7c6f72314777ac8bd3b69a2fb8e3246e +Subproject commit 42b32df3dd0b16a462d07815e2ece896c62ddcbf diff --git a/jbmc/regression/jbmc-strings/StringHashCode/Test.class b/jbmc/regression/jbmc-strings/StringHashCode/Test.class new file mode 100644 index 00000000000..c20b91ccdbc Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringHashCode/Test.class differ diff --git a/jbmc/regression/jbmc-strings/StringHashCode/Test.java b/jbmc/regression/jbmc-strings/StringHashCode/Test.java new file mode 100644 index 00000000000..371a7ff3a8c --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringHashCode/Test.java @@ -0,0 +1,26 @@ +public class Test { + + public static int check(String s, int nondet) { + if(s == null) + return -1; + + if(nondet == 0) { + // This is always true + assert "foo".hashCode() == 101574; + } else if(nondet == 1) { + // This is always false + assert "foo".hashCode() != 101574; + } else if(nondet == 2) { + // This is sometimes false + assert !s.startsWith("foo") && s.hashCode() == 101574; + } else if(nondet == 3) { + // This is always true + assert s.hashCode() == 101574 || !(s.startsWith("foo") && s.length() == 3); + } else { + // This is always false + assert "bar".hashCode() == 101574; + } + + return s.hashCode(); + } +} diff --git a/jbmc/regression/jbmc-strings/StringHashCode/test.desc b/jbmc/regression/jbmc-strings/StringHashCode/test.desc new file mode 100644 index 00000000000..ebaee89b608 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringHashCode/test.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--max-nondet-string-length 1000 --function Test.check --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --unwind 10 +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 8 function .*: SUCCESS +assertion at file Test.java line 11 function .*: FAILURE +assertion at file Test.java line 14 function .*: FAILURE +assertion at file Test.java line 17 function .*: SUCCESS +assertion at file Test.java line 20 function .*: FAILURE diff --git a/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc b/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc index 85a0880af9d..95958b1468e 100644 --- a/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc @@ -1,6 +1,6 @@ CORE test_hash_code.class ---max-nondet-string-length 1000 --function test_hash_code.main +--max-nondet-string-length 1000 --function test_hash_code.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index f133d0c3930..7df2a729d7a 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1517,9 +1517,6 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_string_returning_function[format_signature] = ID_cprover_string_format_func; - cprover_equivalent_to_java_function - ["java::java.lang.String.hashCode:()I"]= - ID_cprover_string_hash_code_func; cprover_equivalent_to_java_function ["java::java.lang.String.indexOf:(I)I"]= ID_cprover_string_index_of_func; diff --git a/src/solvers/README.md b/src/solvers/README.md index 5380b51c547..4ceb8ef92e8 100644 --- a/src/solvers/README.md +++ b/src/solvers/README.md @@ -430,9 +430,6 @@ allocates a new string before calling a primitive. * `cprover_string_equals_ignore_case` : \copybrief add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) \link add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink - * `cprover_string_hash_code` : - \copybrief string_constraint_generatort::add_axioms_for_hash_code - \link string_constraint_generatort::add_axioms_for_hash_code More... \endlink * `cprover_string_is_prefix` : \copybrief add_axioms_for_is_prefix \link add_axioms_for_is_prefix More... \endlink diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h index 642d29c985c..11031e0fcc0 100644 --- a/src/solvers/strings/string_constraint_generator.h +++ b/src/solvers/strings/string_constraint_generator.h @@ -75,18 +75,8 @@ class string_constraint_generatort final exprt associate_length_to_array(const function_application_exprt &f); - // Add axioms corresponding to the String.hashCode java function - // The specification is partial: the actual value is not actually computed - // but we ensure that hash codes of equal strings are equal. - std::pair - add_axioms_for_hash_code(const function_application_exprt &f); - // MEMBERS const messaget message; - - // 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; }; // 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 7a91d1961a2..d12b13b18dc 100644 --- a/src/solvers/strings/string_constraint_generator_comparison.cpp +++ b/src/solvers/strings/string_constraint_generator_comparison.cpp @@ -176,44 +176,6 @@ std::pair add_axioms_for_equals_ignore_case( return {typecast_exprt(eq, f.type()), std::move(constraints)}; } -/// Value that is identical for strings with the same content -/// -/// Add axioms stating that if two strings are equal then the values -/// returned by this function are equal. -/// These axioms are, for each string `s` on which hash was called: -/// * \f$ hash(str)=hash(s) \lor |str| \ne |s| -/// \lor (|str|=|s| \land \exists i<|s|.\ s[i]\ne str[i]) \f$ -/// \param f: function application with argument refined_string `str` -/// \return integer expression `hash(str)` -std::pair -string_constraint_generatort::add_axioms_for_hash_code( - const function_application_exprt &f) -{ - PRECONDITION(f.arguments().size() == 1); - string_constraintst hash_constraints; - const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]); - const typet &return_type = f.type(); - const typet &index_type = str.length_type(); - - auto pair = hash_code_of_string.insert( - std::make_pair(str, fresh_symbol("hash", return_type))); - const exprt hash = pair.first->second; - - for(auto it : hash_code_of_string) - { - const symbol_exprt i = fresh_symbol("index_hash", index_type); - const equal_exprt c1(it.second, hash); - const notequal_exprt c2(it.first.length(), str.length()); - const and_exprt c3( - equal_exprt(it.first.length(), str.length()), - and_exprt( - notequal_exprt(str[i], it.first[i]), - and_exprt(greater_than(str.length(), i), is_positive(i)))); - hash_constraints.existential.push_back(or_exprt(c1, or_exprt(c2, c3))); - } - return {hash, std::move(hash_constraints)}; -} - /// Lexicographic comparison of two strings /// /// Add axioms ensuring the result corresponds to that of the `String.compareTo` diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp index a655ca1e1c4..ae184de1f5d 100644 --- a/src/solvers/strings/string_constraint_generator_main.cpp +++ b/src/solvers/strings/string_constraint_generator_main.cpp @@ -240,8 +240,6 @@ string_constraint_generatort::add_axioms_for_function_application( return add_axioms_for_is_suffix(fresh_symbol, expr, true, array_pool); 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) - return add_axioms_for_hash_code(expr); 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) diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 379becad8e2..61dde9fe1e2 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -609,7 +609,6 @@ IREP_ID_ONE(cprover_string_equals_ignore_case_func) IREP_ID_ONE(cprover_string_empty_string_func) 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_insert_func) IREP_ID_ONE(cprover_string_insert_int_func)