Use symbol_table_baset instead of symbol_tablet where possible

We almost never create a fresh symbol table, and any time we do so we
should really make sure this is the intended behaviour.

Author: tautschnig

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -34,7 +34,7 @@ Author: Diffblue Ltd.
 ///   these method bodies are produced internally, rather than generated from
 ///   Java bytecode.
 ci_lazy_methodst::ci_lazy_methodst(
-  const symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   const irep_idt &main_class,
   const std::vector<irep_idt> &main_jar_classes,
   const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
@@ -96,7 +96,7 @@ static bool references_class_model(const exprt &expr)
 /// \param message_handler: the message handler to use for output
 /// \return Returns false on success
 bool ci_lazy_methodst::operator()(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   method_bytecodet &method_bytecode,
   const method_convertert &method_converter,
   message_handlert &message_handler)
@@ -221,7 +221,16 @@ bool ci_lazy_methodst::operator()(
               << symbol_table.symbols.size() - keep_symbols.symbols.size()
               << " unreachable methods and globals" << messaget::eom;
 
-  symbol_table.swap(keep_symbols);
+  auto sorted_to_keep = keep_symbols.sorted_symbol_names();
+  auto all_sorted = symbol_table.sorted_symbol_names();
+  auto it = sorted_to_keep.cbegin();
+  for(const auto &id : all_sorted)
+  {
+    if(it == sorted_to_keep.cend() || id != *it)
+      symbol_table.remove(id);
+    else
+      ++it;
+  }
 
   return false;
 }
@@ -238,7 +247,7 @@ bool ci_lazy_methodst::handle_virtual_methods_with_no_callees(
   std::unordered_set<irep_idt> &instantiated_classes,
   const std::unordered_set<class_method_descriptor_exprt, irep_hash>
     &virtual_functions,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   ci_lazy_methods_neededt lazy_methods_loader(
     methods_to_convert_later,
@@ -321,7 +330,7 @@ ci_lazy_methodst::convert_and_analyze_method(
   std::unordered_set<irep_idt> &methods_already_populated,
   const bool class_initializer_already_seen,
   const irep_idt &method_name,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   std::unordered_set<irep_idt> &methods_to_convert_later,
   std::unordered_set<irep_idt> &instantiated_classes,
   std::unordered_set<class_method_descriptor_exprt, irep_hash>
@@ -367,7 +376,7 @@ ci_lazy_methodst::convert_and_analyze_method(
 ///   * all the methods of the main jar file
 /// \return set of identifiers of entry point methods
 std::unordered_set<irep_idt> ci_lazy_methodst::entry_point_methods(
-  const symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   message_handlert &message_handler)
 {
   std::unordered_set<irep_idt> methods_to_convert_later;
@@ -481,7 +490,7 @@ void ci_lazy_methodst::get_virtual_method_targets(
   const class_method_descriptor_exprt &called_function,
   const std::unordered_set<irep_idt> &instantiated_classes,
   std::unordered_set<irep_idt> &callable_methods,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   const auto &call_class = called_function.class_id();
   const auto &method_name = called_function.mangled_method_name();
@@ -506,8 +515,8 @@ void ci_lazy_methodst::get_virtual_method_targets(
 ///   `e` or its children.
 void ci_lazy_methodst::gather_needed_globals(
   const exprt &e,
-  const symbol_tablet &symbol_table,
-  symbol_tablet &needed)
+  const symbol_table_baset &symbol_table,
+  symbol_table_baset &needed)
 {
   if(e.id()==ID_symbol)
   {
@@ -546,7 +555,7 @@ irep_idt ci_lazy_methodst::get_virtual_method_target(
   const std::unordered_set<irep_idt> &instantiated_classes,
   const irep_idt &call_basename,
   const irep_idt &classname,
-  const symbol_tablet &symbol_table)
+  const symbol_table_baset &symbol_table)
 {
   // Program-wide, is this class ever instantiated?
   if(!instantiated_classes.count(classname))

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -27,6 +27,7 @@ class ci_lazy_methods_neededt;
 class java_class_loadert;
 class message_handlert;
 class select_pointer_typet;
+class symbol_table_baset;
 
 // Map from method id to class_method_and_bytecodet
 class method_bytecodet
@@ -90,14 +91,14 @@ typedef std::function<
   bool(const irep_idt &function_id, ci_lazy_methods_neededt)>
   method_convertert;
 
-typedef std::function<std::vector<irep_idt>(const symbol_tablet &)>
+typedef std::function<std::vector<irep_idt>(const symbol_table_baset &)>
   load_extra_methodst;
 
 class ci_lazy_methodst
 {
 public:
   ci_lazy_methodst(
-    const symbol_tablet &symbol_table,
+    const symbol_table_baset &symbol_table,
     const irep_idt &main_class,
     const std::vector<irep_idt> &main_jar_classes,
     const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
@@ -108,7 +109,7 @@ class ci_lazy_methodst
 
   // not const since messaget
   bool operator()(
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     method_bytecodet &method_bytecode,
     const method_convertert &method_converter,
     message_handlert &message_handler);
@@ -127,18 +128,18 @@ class ci_lazy_methodst
     const class_method_descriptor_exprt &called_function,
     const std::unordered_set<irep_idt> &instantiated_classes,
     std::unordered_set<irep_idt> &callable_methods,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   void gather_needed_globals(
     const exprt &e,
-    const symbol_tablet &symbol_table,
-    symbol_tablet &needed);
+    const symbol_table_baset &symbol_table,
+    symbol_table_baset &needed);
 
   irep_idt get_virtual_method_target(
     const std::unordered_set<irep_idt> &instantiated_classes,
     const irep_idt &call_basename,
     const irep_idt &classname,
-    const symbol_tablet &symbol_table);
+    const symbol_table_baset &symbol_table);
 
   static irep_idt build_virtual_method_name(
     const irep_idt &class_name,
@@ -154,7 +155,7 @@ class ci_lazy_methodst
   const synthetic_methods_mapt &synthetic_methods;
 
   std::unordered_set<irep_idt> entry_point_methods(
-    const symbol_tablet &symbol_table,
+    const symbol_table_baset &symbol_table,
     message_handlert &message_handler);
 
   struct convert_method_resultt
@@ -168,7 +169,7 @@ class ci_lazy_methodst
     std::unordered_set<irep_idt> &methods_already_populated,
     const bool class_initializer_already_seen,
     const irep_idt &method_name,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     std::unordered_set<irep_idt> &methods_to_convert_later,
     std::unordered_set<irep_idt> &instantiated_classes,
     std::unordered_set<class_method_descriptor_exprt, irep_hash>
@@ -180,7 +181,7 @@ class ci_lazy_methodst
     std::unordered_set<irep_idt> &instantiated_classes,
     const std::unordered_set<class_method_descriptor_exprt, irep_hash>
       &virtual_functions,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 };
 
 #endif // CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H

jbmc/src/java_bytecode/ci_lazy_methods_needed.h

@@ -19,7 +19,7 @@ Author: Chris Smowton, [email protected]
 class namespacet;
 class pointer_typet;
 class select_pointer_typet;
-class symbol_tablet;
+class symbol_table_baset;
 class typet;
 
 class ci_lazy_methods_neededt
@@ -28,7 +28,7 @@ class ci_lazy_methods_neededt
   ci_lazy_methods_neededt(
     std::unordered_set<irep_idt> &_callable_methods,
     std::unordered_set<irep_idt> &_instantiated_classes,
-    const symbol_tablet &_symbol_table,
+    const symbol_table_baset &_symbol_table,
     const select_pointer_typet &pointer_type_selector)
     : callable_methods(_callable_methods),
       instantiated_classes(_instantiated_classes),
@@ -53,7 +53,7 @@ class ci_lazy_methods_neededt
   // found so far, so we can use a membership test to avoid
   // repeatedly exploring a class hierarchy.
   std::unordered_set<irep_idt> &instantiated_classes;
-  const symbol_tablet &symbol_table;
+  const symbol_table_baset &symbol_table;
 
   const select_pointer_typet &pointer_type_selector;
 

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -7,17 +7,18 @@ Author: Kurt Degiogrio, [email protected]
 \*******************************************************************/
 
 #include "java_bytecode_concurrency_instrumentation.h"
-#include "expr2java.h"
-#include "java_types.h"
-#include "java_utils.h"
 
 #include <util/arith_tools.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_iterator.h>
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/std_types.h>
-#include <util/symbol_table.h>
+#include <util/symbol_table_base.h>
+
+#include "expr2java.h"
+#include "java_types.h"
+#include "java_utils.h"
 
 // Disable linter to allow an std::string constant.
 const std::string next_thread_id = CPROVER_PREFIX "_next_thread_id";// NOLINT(*)
@@ -33,7 +34,7 @@ const std::string thread_id = CPROVER_PREFIX "_thread_id";// NOLINT(*)
 /// /param is_static_lifetime: if true this symbol will be set as static
 /// /return returns new or existing symbol.
 static symbolt add_or_get_symbol(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const irep_idt &name,
   const irep_idt &base_name,
   const typet &type,
@@ -101,7 +102,7 @@ static const std::string get_thread_block_identifier(
 /// \param object: expression representing a 'java.Lang.Object'. This object is
 ///   used to achieve object-level locking by calling monitoroenter/monitorexit.
 static codet get_monitor_call(
-  const symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   bool is_enter,
   const exprt &object)
 {
@@ -206,7 +207,7 @@ static void monitor_exits(codet &code, const codet &monitorexit)
 /// \param symbol: writeable symbol hosting code to synchronize
 /// \param sync_object: object to use as a lock
 static void instrument_synchronized_code(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   symbolt &symbol,
   const exprt &sync_object)
 {
@@ -271,7 +272,7 @@ static void instrument_synchronized_code(
 static void instrument_start_thread(
   const code_function_callt &f_code,
   codet &code,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   PRECONDITION(f_code.arguments().size() == 1);
 
@@ -341,7 +342,7 @@ static void instrument_start_thread(
 static void instrument_end_thread(
   const code_function_callt &f_code,
   codet &code,
-  const symbol_tablet &symbol_table)
+  const symbol_table_baset &symbol_table)
 {
   PRECONDITION(f_code.arguments().size() == 1);
   (void)symbol_table; // unused parameter
@@ -375,7 +376,7 @@ static void instrument_end_thread(
 static void instrument_get_current_thread_id(
   const code_function_callt &f_code,
   codet &code,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   PRECONDITION(f_code.arguments().size() == 0);
 
@@ -406,7 +407,7 @@ static void instrument_get_current_thread_id(
 static void instrument_get_monitor_count(
   const code_function_callt &f_code,
   codet &code,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   PRECONDITION(f_code.arguments().size() == 1);
 
@@ -484,10 +485,10 @@ static void instrument_get_monitor_count(
 /// symex. See https://github.com/diffblue/cbmc/issues/1630/for more details.
 ///
 /// \param symbol_table: a symbol table
-void convert_threadblock(symbol_tablet &symbol_table)
+void convert_threadblock(symbol_table_baset &symbol_table)
 {
-  using instrument_callbackt =
-    std::function<void(const code_function_callt&, codet&, symbol_tablet&)>;
+  using instrument_callbackt = std::function<void(
+    const code_function_callt &, codet &, symbol_table_baset &)>;
   using expr_replacement_mapt =
     std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
 
@@ -603,7 +604,7 @@ void convert_threadblock(symbol_tablet &symbol_table)
 /// \param symbol_table: a symbol table
 /// \param message_handler: status output
 void convert_synchronized_methods(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler)
 {
   namespacet ns(symbol_table);

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.h

@@ -9,11 +9,11 @@ Author: Kurt Degiogrio, [email protected]
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONCURRENCY_INSTRUMENTATION_H
 
 class message_handlert;
-class symbol_tablet;
+class symbol_table_baset;
 
-void convert_threadblock(symbol_tablet &symbol_table);
+void convert_threadblock(symbol_table_baset &symbol_table);
 void convert_synchronized_methods(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler);
 
 #endif

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -31,7 +31,7 @@ class java_bytecode_convert_classt
 {
 public:
   java_bytecode_convert_classt(
-    symbol_tablet &_symbol_table,
+    symbol_table_baset &_symbol_table,
     message_handlert &_message_handler,
     size_t _max_array_length,
     method_bytecodet &method_bytecode,
@@ -105,7 +105,7 @@ class java_bytecode_convert_classt
 
 private:
   messaget log;
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
   const size_t max_array_length;
   method_bytecodet &method_bytecode;
   java_string_library_preprocesst &string_preprocess;
@@ -790,7 +790,7 @@ void java_bytecode_convert_classt::convert(
   }
 }
 
-void add_java_array_types(symbol_tablet &symbol_table)
+void add_java_array_types(symbol_table_baset &symbol_table)
 {
   const std::string letters="ijsbcfdza";
 
@@ -1003,7 +1003,7 @@ void add_java_array_types(symbol_tablet &symbol_table)
 
 bool java_bytecode_convert_class(
   const java_class_loadert::parse_tree_with_overlayst &parse_trees,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   size_t max_array_length,
   method_bytecodet &method_bytecode,
@@ -1188,7 +1188,7 @@ void convert_java_annotations(
 /// corresponding outer classes.
 void mark_java_implicitly_generic_class_type(
   const irep_idt &class_name,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   const std::string qualified_class_name = "java::" + id2string(class_name);
   PRECONDITION(symbol_table.has_symbol(qualified_class_name));