Wrap incoming symbol tables in suffix-aware versions

Author: JohnDumbell

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <json/json_parser.h>
 
 #include <goto-programs/class_hierarchy.h>
+#include <util/symbol_table_builder.h>
 
 #include "java_bytecode_concurrency_instrumentation.h"
 #include "java_bytecode_convert_class.h"
@@ -787,8 +788,11 @@ bool java_bytecode_languaget::typecheck(
       break;
     case LAZY_METHODS_MODE_EAGER:
       {
+        symbol_table_buildert symbol_table_builder =
+            symbol_table_buildert::wrap(symbol_table);
+
         journalling_symbol_tablet journalling_symbol_table =
-          journalling_symbol_tablet::wrap(symbol_table);
+          journalling_symbol_tablet::wrap(symbol_table_builder);
 
         // Convert all synthetic methods:
         for(const auto &function_id_and_type : synthetic_methods)
@@ -839,18 +843,21 @@ bool java_bytecode_languaget::generate_support_functions(
 {
   PRECONDITION(language_options_initialized);
 
+  symbol_table_buildert symbol_table_builder =
+      symbol_table_buildert::wrap(symbol_table);
+
   main_function_resultt res=
     get_main_symbol(symbol_table, main_class, get_message_handler());
   if(!res.is_success())
     return res.is_error();
 
   // Load the main function into the symbol table to get access to its
   // parameter names
-  convert_lazy_method(res.main_function.name, symbol_table);
+  convert_lazy_method(res.main_function.name, symbol_table_builder);
 
   // generate the test harness in __CPROVER__start and a call the entry point
   return java_entry_point(
-    symbol_table,
+    symbol_table_builder,
     main_class,
     get_message_handler(),
     assume_inputs_non_null,
@@ -877,12 +884,15 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
   symbol_tablet &symbol_table,
   method_bytecodet &method_bytecode)
 {
+  symbol_table_buildert symbol_table_builder =
+      symbol_table_buildert::wrap(symbol_table);
+
   const method_convertert method_converter =
-    [this, &symbol_table]
+    [this, &symbol_table_builder]
       (const irep_idt &function_id, ci_lazy_methods_neededt lazy_methods_needed)
     {
       return convert_single_method(
-        function_id, symbol_table, std::move(lazy_methods_needed));
+        function_id, symbol_table_builder, std::move(lazy_methods_needed));
     };
 
   ci_lazy_methodst method_gather(

src/goto-cc/compile.cpp

@@ -25,6 +25,7 @@ Date: June 2006
 #include <util/tempdir.h>
 #include <util/unicode.h>
 #include <util/version.h>
+#include <util/symbol_table_builder.h>
 
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/ansi_c_entry_point.h>
@@ -692,37 +693,40 @@ void compilet::add_compiler_specific_defines(configt &config) const
 
 void compilet::convert_symbols(goto_functionst &dest)
 {
+  symbol_table_buildert symbol_table_builder =
+      symbol_table_buildert::wrap(goto_model.symbol_table);
+
   goto_convert_functionst converter(
-    goto_model.symbol_table, get_message_handler());
+    symbol_table_builder, get_message_handler());
 
   // the compilation may add symbols!
 
   symbol_tablet::symbolst::size_type before=0;
 
-  while(before != goto_model.symbol_table.symbols.size())
+  while(before != symbol_table_builder.symbols.size())
   {
-    before = goto_model.symbol_table.symbols.size();
+    before = symbol_table_builder.symbols.size();
 
     typedef std::set<irep_idt> symbols_sett;
     symbols_sett symbols;
 
-    for(const auto &named_symbol : goto_model.symbol_table.symbols)
+    for(const auto &named_symbol : symbol_table_builder.symbols)
       symbols.insert(named_symbol.first);
 
     // the symbol table iterators aren't stable
     for(const auto &symbol : symbols)
     {
       symbol_tablet::symbolst::const_iterator s_it =
-        goto_model.symbol_table.symbols.find(symbol);
-      CHECK_RETURN(s_it != goto_model.symbol_table.symbols.end());
+        symbol_table_builder.symbols.find(symbol);
+      CHECK_RETURN(s_it != symbol_table_builder.symbols.end());
 
       if(
         s_it->second.is_function() && !s_it->second.is_compiled() &&
         s_it->second.value.is_not_nil())
       {
         debug() << "Compiling " << s_it->first << eom;
         converter.convert_function(s_it->first, dest.function_map[s_it->first]);
-        goto_model.symbol_table.get_writeable_ref(symbol).set_compiled();
+        symbol_table_builder.get_writeable_ref(symbol).set_compiled();
       }
     }
   }

src/goto-programs/goto_convert.cpp

@@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
-
+#include <util/symbol_table_builder.h>
 #include <util/c_types.h>
 
 #include "goto_convert_class.h"
@@ -1939,7 +1939,9 @@ void goto_convert(
   message_handlert &message_handler,
   const irep_idt &mode)
 {
-  goto_convertt goto_convert(symbol_table, message_handler);
+  symbol_table_buildert symbol_table_builder =
+      symbol_table_buildert::wrap(symbol_table);
+  goto_convertt goto_convert(symbol_table_builder, message_handler);
   goto_convert.goto_convert(code, dest, mode);
 }