Merge pull request #983 from romainbrenguier/pull-request/override-in-final-step

Overwrite String functions in final step of bytecode conversion

Author: forejtv

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -45,13 +45,14 @@ class java_bytecode_convert_classt:public messaget
   {
     add_array_types();
 
-    if(parse_tree.loading_successful)
+    bool loading_success=parse_tree.loading_successful;
+    if(loading_success)
       convert(parse_tree.parsed_class);
-    else if(string_preprocess.is_known_string_type(
-              parse_tree.parsed_class.name))
+
+    if(string_preprocess.is_known_string_type(parse_tree.parsed_class.name))
       string_preprocess.add_string_type(
         parse_tree.parsed_class.name, symbol_table);
-    else
+    else if(!loading_success)
       generate_class_stub(parse_tree.parsed_class.name);
   }
 

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1550,17 +1550,11 @@ 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.value=string_preprocess.code_for_function(
-          id, to_code_type(symbol.type), loc, symbol_table);
-
         symbol_table.add(symbol);
       }
 

src/java_bytecode/java_bytecode_language.cpp

@@ -799,6 +799,43 @@ void java_bytecode_languaget::convert_lazy_method(
 
 /*******************************************************************\
 
+Function: java_bytecode_languaget::replace_string_methods
+
+  Inputs:
+    context - a symbol table
+
+ Purpose: Replace methods of the String library that are in the symbol table
+          by code generated by string_preprocess.
+
+\*******************************************************************/
+
+void java_bytecode_languaget::replace_string_methods(
+  symbol_tablet &context)
+{
+  // Symbols that have code type are potentialy to be replaced
+  std::list<symbolt> code_symbols;
+  forall_symbols(symbol, context.symbols)
+  {
+    if(symbol->second.type.id()==ID_code)
+      code_symbols.push_back(symbol->second);
+  }
+
+  for(const auto &symbol : code_symbols)
+  {
+    const irep_idt &id=symbol.name;
+    exprt generated_code=string_preprocess.code_for_function(
+      id, to_code_type(symbol.type), symbol.location, context);
+    if(generated_code.is_not_nil())
+    {
+      // Replace body of the function by code generated by string preprocess
+      symbolt &symbol=context.lookup(id);
+      symbol.value=generated_code;
+    }
+  }
+}
+
+/*******************************************************************\
+
 Function: java_bytecode_languaget::final
 
   Inputs:
@@ -816,6 +853,9 @@ bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
   */
   java_internal_additions(symbol_table);
 
+  // Replace code of String methods calls by code we generate
+  replace_string_methods(symbol_table);
+
   main_function_resultt res=
     get_main_symbol(symbol_table, main_class, get_message_handler());
   if(res.stop_convert)

src/java_bytecode/java_bytecode_language.h

@@ -49,6 +49,8 @@ class java_bytecode_languaget:public languaget
     symbol_tablet &context,
     const std::string &module) override;
 
+  void replace_string_methods(symbol_tablet &context);
+
   virtual bool final(
     symbol_tablet &context) override;
 

src/java_bytecode/java_string_library_preprocess.cpp

@@ -319,7 +319,10 @@ void java_string_library_preprocesst::add_string_type(
   string_symbol.type=string_type;
   string_symbol.is_type=true;
 
-  symbol_table.add(string_symbol);
+  // Overwrite any pre-existing symbol in the table, e.g. created by
+  // a loaded model.
+  symbol_table.remove(string_symbol.name);
+  assert(!symbol_table.add(string_symbol));
 }
 
 /*******************************************************************\