Merge pull request #4554 from romainbrenguier/clean-up/string-intern

Remove cprover_string_intern handling in the solver

Author: romainbrenguier

jbmc/lib/java-models-library

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

jbmc/regression/strings-smoke-tests/java_intern/test.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

jbmc/regression/strings-smoke-tests/java_intern/testFail.desc

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

jbmc/regression/strings-smoke-tests/java_intern/test_intern.class

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

jbmc/regression/strings-smoke-tests/java_intern/test_intern.java

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

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -71,13 +71,6 @@ class string_constraint_generatort final
   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<symbol_exprt, string_constraintst>
-  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 @@ class string_constraint_generatort final
   // 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;
-
-  // Pool used for the intern method
-  std::map<array_string_exprt, symbol_exprt> intern_of_string;
 };
 
 // Type used by primitives to signal errors

src/solvers/README.md

@@ -297,53 +297,3 @@ std::pair<exprt, string_constraintst> 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<symbol_exprt, string_constraintst>
-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)};
-}

src/solvers/strings/string_constraint_generator.h

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

src/solvers/strings/string_constraint_generator_comparison.cpp

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