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.

Author: romainbrenguier

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;

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

src/solvers/strings/string_constraint_generator.h

@@ -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/strings/string_constraint_generator_comparison.cpp

@@ -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_main.cpp

@@ -308,8 +308,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/util/irep_ids.def

@@ -611,7 +611,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)