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"
@@ -790,8 +791,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)
@@ -842,18 +846,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,
@@ -880,12 +887,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]
-      (const irep_idt &function_id, ci_lazy_methods_neededt lazy_methods_needed)
-    {
+    [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

@@ -22,6 +22,7 @@ Date: June 2006
 #include <util/file_util.h>
 #include <util/get_base_name.h>
 #include <util/suffix.h>
+#include <util/symbol_table_builder.h>
 #include <util/tempdir.h>
 #include <util/unicode.h>
 #include <util/version.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

@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_convert.h"
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/cprover_prefix.h>
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
@@ -20,8 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
-
-#include <util/c_types.h>
+#include <util/symbol_table_builder.h>
 
 #include "goto_convert_class.h"
 #include "destructor.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);
 }
 

src/goto-programs/goto_convert_functions.cpp

@@ -11,10 +11,11 @@ Date: June 2003
 #include "goto_convert_functions.h"
 
 #include <util/base_type.h>
+#include <util/fresh_symbol.h>
+#include <util/prefix.h>
 #include <util/std_code.h>
 #include <util/symbol_table.h>
-#include <util/prefix.h>
-#include <util/fresh_symbol.h>
+#include <util/symbol_table_builder.h>
 
 #include "goto_inline.h"
 
@@ -217,18 +218,23 @@ void goto_convert(
   goto_modelt &goto_model,
   message_handlert &message_handler)
 {
+  symbol_table_buildert symbol_table_builder =
+    symbol_table_buildert::wrap(goto_model.symbol_table);
+
   goto_convert(
-    goto_model.symbol_table,
-    goto_model.goto_functions,
-    message_handler);
+    symbol_table_builder, goto_model.goto_functions, message_handler);
 }
 
 void goto_convert(
   symbol_table_baset &symbol_table,
   goto_functionst &functions,
   message_handlert &message_handler)
 {
-  goto_convert_functionst goto_convert_functions(symbol_table, message_handler);
+  symbol_table_buildert symbol_table_builder =
+    symbol_table_buildert::wrap(symbol_table);
+
+  goto_convert_functionst goto_convert_functions(
+    symbol_table_builder, message_handler);
 
   goto_convert_functions.goto_convert(functions);
 }
@@ -239,7 +245,11 @@ void goto_convert(
   goto_functionst &functions,
   message_handlert &message_handler)
 {
-  goto_convert_functionst goto_convert_functions(symbol_table, message_handler);
+  symbol_table_buildert symbol_table_builder =
+    symbol_table_buildert::wrap(symbol_table);
+
+  goto_convert_functionst goto_convert_functions(
+    symbol_table_builder, message_handler);
 
   goto_convert_functions.convert_function(
     identifier, functions.function_map[identifier]);

src/goto-programs/lazy_goto_functions_map.h

@@ -11,9 +11,10 @@
 #include "goto_functions.h"
 #include "goto_convert_functions.h"
 
-#include <util/message.h>
 #include <langapi/language_file.h>
 #include <util/journalling_symbol_table.h>
+#include <util/message.h>
+#include <util/symbol_table_builder.h>
 
 /// Provides a wrapper for a map of lazily loaded goto_functiont.
 /// This incrementally builds a goto-functions object, while permitting
@@ -142,8 +143,11 @@ class lazy_goto_functions_mapt final
   // const first
   reference ensure_function_loaded_internal(const key_type &name) const
   {
+    symbol_table_buildert symbol_table_builder =
+      symbol_table_buildert::wrap(symbol_table);
+
     journalling_symbol_tablet journalling_table =
-      journalling_symbol_tablet::wrap(symbol_table);
+      journalling_symbol_tablet::wrap(symbol_table_builder);
     reference named_function=ensure_entry_converted(name, journalling_table);
     mapped_type function=named_function.second;
     if(processed_functions.count(name)==0)