Overwrite String functions during bytecode conversion

Replace all String functions in the preprocessing, even if they exist
already (e.g. if a model exists).

This implements issue diffblue/test-gen#360

Author: Joel Allred

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1530,18 +1530,20 @@ codet java_bytecode_convert_methodt::convert_instructions(
         symbol.type=arg0.type();
         symbol.value.make_nil();
         symbol.mode=ID_java;
-
         assign_parameter_names(
           to_code_type(symbol.type),
           symbol.name,
           symbol_table);
 
-        // The string refinement module may provide a definition for this
-        // function.
+        symbol_table.add(symbol);
+      }
+
+      // Create code for functions on Strings and replace the body.
+      if(string_preprocess.shall_function_be_overriden(id))
+      {
+        symbolt &symbol=(*symbol_table.symbols.find(id)).second;
         symbol.value=string_preprocess.code_for_function(
           id, to_code_type(symbol.type), loc, symbol_table);
-
-        symbol_table.add(symbol);
       }
 
       if(is_virtual)

src/java_bytecode/java_string_library_preprocess.cpp

@@ -1793,37 +1793,104 @@ exprt java_string_library_preprocesst::code_for_function(
 {
   auto it_id=cprover_equivalent_to_java_function.find(function_id);
   if(it_id!=cprover_equivalent_to_java_function.end())
+  {
+    overriden.insert(function_id);
     return make_function_from_call(it_id->second, type, loc, symbol_table);
+  }
 
   it_id=cprover_equivalent_to_java_string_returning_function.find(function_id);
   if(it_id!=cprover_equivalent_to_java_string_returning_function.end())
+  {
+    overriden.insert(function_id);
     return make_string_returning_function_from_call(
       it_id->second, type, loc, symbol_table);
+  }
 
   it_id=cprover_equivalent_to_java_constructor.find(function_id);
   if(it_id!=cprover_equivalent_to_java_constructor.end())
+  {
+    overriden.insert(function_id);
     return make_init_function_from_call(
       it_id->second, type, loc, symbol_table);
+  }
 
   it_id=cprover_equivalent_to_java_assign_and_return_function.find(function_id);
   if(it_id!=cprover_equivalent_to_java_assign_and_return_function.end())
+  {
+    overriden.insert(function_id);
     return make_assign_and_return_function_from_call(
       it_id->second, type, loc, symbol_table);
+  }
 
   it_id=cprover_equivalent_to_java_assign_function.find(function_id);
   if(it_id!=cprover_equivalent_to_java_assign_function.end())
+  {
+    overriden.insert(function_id);
     return make_assign_function_from_call(
       it_id->second, type, loc, symbol_table);
+  }
 
   auto it=conversion_table.find(function_id);
   if(it!=conversion_table.end())
+  {
+    overriden.insert(function_id);
     return it->second(type, loc, symbol_table);
+  }
 
   return nil_exprt();
 }
 
 /*******************************************************************\
 
+Function: java_string_library_preprocesst::shall_function_be_overriden
+
+  Inputs:
+    function_id - name of the function
+
+ Outputs: True if the function has a known replacement for its body
+          or if it has already been replaced (by a call to
+          code_for_function), false otherwise.
+
+ Purpose: Check whether the current function's body is to be replaced
+          with the code created in the preprocessing.
+
+\*******************************************************************/
+
+bool java_string_library_preprocesst::shall_function_be_overriden(
+  const irep_idt &function_id)
+{
+  if(overriden.find(function_id)!=overriden.end())
+    return false;
+
+  auto it_id=cprover_equivalent_to_java_function.find(function_id);
+  if(it_id!=cprover_equivalent_to_java_function.end())
+    return true;
+
+  it_id=cprover_equivalent_to_java_string_returning_function.find(function_id);
+  if(it_id!=cprover_equivalent_to_java_string_returning_function.end())
+    return true;
+
+  it_id=cprover_equivalent_to_java_constructor.find(function_id);
+  if(it_id!=cprover_equivalent_to_java_constructor.end())
+    return true;
+
+  it_id=cprover_equivalent_to_java_assign_and_return_function.find(function_id);
+  if(it_id!=cprover_equivalent_to_java_assign_and_return_function.end())
+    return true;
+
+  it_id=cprover_equivalent_to_java_assign_function.find(function_id);
+  if(it_id!=cprover_equivalent_to_java_assign_function.end())
+    return true;
+
+  auto it=conversion_table.find(function_id);
+  if(it!=conversion_table.end())
+    return true;
+
+  return false;
+}
+
+/*******************************************************************\
+
 Function: java_string_library_preprocesst::is_known_string_type
 
   Inputs:

src/java_bytecode/java_string_library_preprocess.h

@@ -39,6 +39,8 @@ class java_string_library_preprocesst:public messaget
     const source_locationt &loc,
     symbol_tablet &symbol_table);
 
+  bool shall_function_be_overriden(const irep_idt &function_id);
+
   codet replace_character_call(code_function_callt call)
   {
     return character_preprocess.replace_character_call(call);
@@ -78,6 +80,10 @@ class java_string_library_preprocesst:public messaget
 
   typedef std::unordered_map<irep_idt, irep_idt, irep_id_hash> id_mapt;
 
+  // Keeps functions on strings of which we have replaced the body, so that we
+  // only do it once.
+  std::unordered_set<irep_idt, irep_id_hash> overriden;
+
   // Table mapping each java method signature to the code generating function
   std::unordered_map<irep_idt, conversion_functiont, irep_id_hash>
     conversion_table;