Merge pull request #4546 from romainbrenguier/feature/string-hash-code

Use model for String.hashCode

Author: romainbrenguier

jbmc/lib/java-models-library

@@ -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();
+    }
+}

jbmc/regression/jbmc-strings/StringHashCode/Test.class

@@ -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

jbmc/regression/jbmc-strings/StringHashCode/Test.java

@@ -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$

jbmc/regression/jbmc-strings/StringHashCode/test.desc

@@ -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;

jbmc/regression/strings-smoke-tests/java_hash_code/test.desc

@@ -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

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -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<exprt, string_constraintst>
-  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<array_string_exprt, exprt> hash_code_of_string;
 };
 
 // Type used by primitives to signal errors

src/solvers/README.md

@@ -176,44 +176,6 @@ std::pair<exprt, string_constraintst> 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<exprt, string_constraintst>
-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`

src/solvers/strings/string_constraint_generator.h

@@ -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)

src/solvers/strings/string_constraint_generator_comparison.cpp

@@ -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)