Add recording symbol table

src/analyses/is_threaded.cpp

@@ -85,7 +85,7 @@ class is_threaded_domaint:public ai_domain_baset
 void is_threadedt::compute(const goto_functionst &goto_functions)
 {
   // the analysis doesn't actually use the namespace, fake one
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
   const namespacet ns(symbol_table);
 
   ait<is_threaded_domaint> is_threaded_analysis;

src/ansi-c/ansi_c_language.cpp

@@ -105,7 +105,7 @@ bool ansi_c_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
 {
-  symbol_tablet new_symbol_table;
+  concrete_symbol_tablet new_symbol_table;
 
   if(ansi_c_typecheck(
     parse_tree,

src/ansi-c/ansi_c_typecheck.cpp

@@ -42,7 +42,7 @@ bool ansi_c_typecheck(
   const unsigned errors_before=
     message_handler.get_message_count(messaget::M_ERROR);
 
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
   ansi_c_parse_treet ansi_c_parse_tree;
 
   ansi_c_typecheckt ansi_c_typecheck(

src/ansi-c/type2name.cpp

@@ -269,6 +269,6 @@ std::string type2name(const typet &type, const namespacet &ns)
 
 std::string type2name(const typet &type)
 {
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
   return type2name(type, namespacet(symbol_table));
 }

src/cbmc/bmc.h

@@ -68,7 +68,7 @@ class bmct:public safety_checkert
 
 protected:
   const optionst &options;
-  symbol_tablet new_symbol_table;
+  concrete_symbol_tablet new_symbol_table;
   namespacet ns;
   symex_target_equationt equation;
   symex_bmct symex;

src/cpp/cpp_language.cpp

@@ -125,7 +125,7 @@ bool cpp_languaget::typecheck(
   if(module=="")
     return false;
 
-  symbol_tablet new_symbol_table;
+  concrete_symbol_tablet new_symbol_table;
 
   if(cpp_typecheck(
       cpp_parse_tree, new_symbol_table, module, get_message_handler()))

src/cpp/cpp_typecheck.cpp

@@ -102,7 +102,7 @@ bool cpp_typecheck(
   const unsigned errors_before=
     message_handler.get_message_count(messaget::M_ERROR);
 
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
   cpp_parse_treet cpp_parse_tree;
 
   cpp_typecheckt cpp_typecheck(cpp_parse_tree, symbol_table,

src/goto-cc/linker_script_merge.cpp

@@ -53,7 +53,7 @@ int linker_script_merget::add_linker_script_definitions()
     return fail;
   }
 
-  symbol_tablet original_st;
+  concrete_symbol_tablet original_st;
   goto_functionst original_gf;
   fail=read_goto_binary(goto_file, original_st, original_gf,
       get_message_handler());

src/goto-instrument/dump_c.cpp

@@ -46,7 +46,7 @@ void dump_ct::operator()(std::ostream &os)
 
   // add copies of struct types when ID_C_transparent_union is only
   // annotated to parameter
-  symbol_tablet symbols_transparent;
+  concrete_symbol_tablet symbols_transparent;
   for(const auto &named_symbol : copied_symbol_table.symbols)
   {
     const symbolt &symbol=named_symbol.second;

src/goto-instrument/dump_c_class.h

@@ -48,7 +48,7 @@ class dump_ct
 
 protected:
   const goto_functionst &goto_functions;
-  symbol_tablet copied_symbol_table;
+  concrete_symbol_tablet copied_symbol_table;
   const namespacet ns;
   std::unique_ptr<languaget> language;
   const bool harness;

src/goto-instrument/model_argc_argv.cpp

@@ -106,7 +106,7 @@ bool model_argc_argv(
   ansi_c_language.parse(iss, "");
   config.ansi_c.preprocessor=pp;
 
-  symbol_tablet tmp_symbol_table;
+  concrete_symbol_tablet tmp_symbol_table;
   ansi_c_language.typecheck(tmp_symbol_table, "<built-in-library>");
 
   goto_programt init_instructions;

src/goto-instrument/unwind.cpp

@@ -325,7 +325,7 @@ void goto_unwindt::unwind(
       i_it!=goto_program.instructions.end();)
   {
 #ifdef DEBUG
-    symbol_tablet st;
+    concrete_symbol_tablet st;
     namespacet ns(st);
     std::cout << "Instruction:\n";
     goto_program.output_instruction(ns, "", std::cout, i_it);

src/goto-programs/goto_model.h

@@ -22,7 +22,7 @@ Author: Daniel Kroening, [email protected]
 class goto_modelt
 {
 public:
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
   goto_functionst goto_functions;
 
   void clear()

src/goto-programs/goto_program_template.h

@@ -495,7 +495,7 @@ class goto_program_templatet
   /// Output goto-program to given stream
   std::ostream &output(std::ostream &out) const
   {
-    return output(namespacet(symbol_tablet()), "", out);
+    return output(namespacet(concrete_symbol_tablet()), "", out);
   }
 
   /// Output a single instruction

src/goto-programs/read_goto_binary.cpp

@@ -251,7 +251,7 @@ bool read_object_and_link(
 /// \return true on error, false otherwise
 bool read_object_and_link(
   const std::string &file_name,
-  symbol_tablet &dest_symbol_table,
+  concrete_symbol_tablet &dest_symbol_table,
   goto_functionst &dest_functions,
   message_handlert &message_handler)
 {

src/goto-programs/read_goto_binary.h

@@ -18,6 +18,7 @@ class goto_functionst;
 class goto_modelt;
 class message_handlert;
 class symbol_tablet;
+class concrete_symbol_tablet;
 
 bool read_goto_binary(
   const std::string &filename,
@@ -34,7 +35,7 @@ bool is_goto_binary(const std::string &filename);
 
 bool read_object_and_link(
   const std::string &file_name,
-  symbol_tablet &,
+  concrete_symbol_tablet &,
   goto_functionst &,
   message_handlert &);
 

src/goto-symex/symex_target_equation.cpp

@@ -723,7 +723,7 @@ std::ostream &operator<<(
   const symex_target_equationt::SSA_stept &step)
 {
   // may cause lookup failures, since it's blank
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
   namespacet ns(symbol_table);
   step.output(ns, out);
   return out;

src/java_bytecode/ci_lazy_methods.cpp

@@ -172,7 +172,9 @@ bool ci_lazy_methodst::operator()(
   while(any_new_methods);
 
   // Remove symbols for methods that were declared but never used:
-  symbol_tablet keep_symbols;
+  std::unordered_set<irep_idt, irep_id_hash> unreachable_symbols;
+  for(const auto &sym : symbol_table.symbols)
+    unreachable_symbols.insert(sym.first);
 
   for(const auto &sym : symbol_table.symbols)
   {
@@ -184,16 +186,19 @@ bool ci_lazy_methodst::operator()(
       continue;
     }
     if(sym.second.type.id()==ID_code)
-      gather_needed_globals(sym.second.value, symbol_table, keep_symbols);
-    keep_symbols.add(sym.second);
+    {
+      gather_needed_globals(
+        sym.second.value, symbol_table, unreachable_symbols);
+    }
+    unreachable_symbols.erase(sym.first);
   }
 
-  debug() << "CI lazy methods: removed "
-          << symbol_table.symbols.size() - keep_symbols.symbols.size()
-          << " unreaclass_hierarchyable methods and globals"
-          << eom;
+  debug()
+    << "CI lazy methods: removed " << unreachable_symbols.size()
+    << " unreachable methods and globals" << eom;
 
-  symbol_table.swap(keep_symbols);
+  for(const irep_idt &symbol_name : unreachable_symbols)
+    symbol_table.remove(symbol_name);
 
   return false;
 }
@@ -425,7 +430,7 @@ void ci_lazy_methodst::get_virtual_method_targets(
 void ci_lazy_methodst::gather_needed_globals(
   const exprt &e,
   const symbol_tablet &symbol_table,
-  symbol_tablet &needed)
+  std::unordered_set<irep_idt, irep_id_hash> &unreachable)
 {
   if(e.id()==ID_symbol)
   {
@@ -438,12 +443,12 @@ void ci_lazy_methodst::gather_needed_globals(
     if(findit!=symbol_table.symbols.end() &&
        findit->second.is_static_lifetime)
     {
-      needed.add(findit->second);
+      unreachable.erase(findit->first);
     }
   }
   else
     forall_operands(opit, e)
-      gather_needed_globals(*opit, symbol_table, needed);
+      gather_needed_globals(*opit, symbol_table, unreachable);
 }
 
 /// See param lazy_methods

src/java_bytecode/ci_lazy_methods.h

@@ -13,6 +13,7 @@
 #define CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H
 
 #include <map>
+#include <unordered_set>
 #include <functional>
 
 #include <util/irep.h>
@@ -90,7 +91,7 @@ class ci_lazy_methodst:public messaget
   void gather_needed_globals(
     const exprt &e,
     const symbol_tablet &symbol_table,
-    symbol_tablet &needed);
+    std::unordered_set<irep_idt, irep_id_hash> &unreachable);
 
   void gather_field_types(const typet &class_type,
     const namespacet &ns,

src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -83,7 +83,7 @@ void java_bytecode_parse_treet::classt::output(std::ostream &out) const
 
 void java_bytecode_parse_treet::annotationt::output(std::ostream &out) const
 {
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 
   out << '@' << type2java(type, ns);
@@ -109,7 +109,7 @@ void java_bytecode_parse_treet::annotationt::output(std::ostream &out) const
 void java_bytecode_parse_treet::annotationt::element_value_pairt::output(
   std::ostream &out) const
 {
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 
   out << '"' << element_name << '"' << '=';
@@ -118,7 +118,7 @@ void java_bytecode_parse_treet::annotationt::element_value_pairt::output(
 
 void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
 {
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 
   for(const auto &annotation : annotations)

src/jsil/jsil_language.cpp

@@ -145,7 +145,7 @@ bool jsil_languaget::to_expr(
     result=true;
   else
   {
-    symbol_tablet symbol_table;
+    concrete_symbol_tablet symbol_table;
     result=
       jsil_convert(parse_tree, symbol_table, get_message_handler());
 

src/jsil/jsil_typecheck.cpp

@@ -925,7 +925,7 @@ bool jsil_typecheck(
   const unsigned errors_before=
     message_handler.get_message_count(messaget::M_ERROR);
 
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
 
   jsil_typecheckt jsil_typecheck(
     symbol_table,

src/langapi/language_ui.h

@@ -21,7 +21,7 @@ class language_uit:public messaget
 {
 public:
   language_filest language_files;
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
 
   language_uit(
     const cmdlinet &cmdline,

src/langapi/language_util.cpp

@@ -78,13 +78,13 @@ std::string type_to_name(
 
 std::string from_expr(const exprt &expr)
 {
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
   return from_expr(namespacet(symbol_table), "", expr);
 }
 
 std::string from_type(const typet &type)
 {
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
   return from_type(namespacet(symbol_table), "", type);
 }
 
@@ -110,6 +110,6 @@ exprt to_expr(
 
 std::string type_to_name(const typet &type)
 {
-  symbol_tablet symbol_table;
+  concrete_symbol_tablet symbol_table;
   return type_to_name(namespacet(symbol_table), "", type);
 }

src/pointer-analysis/goto_program_dereference.cpp

@@ -436,7 +436,7 @@ void dereference(
   value_setst &value_sets)
 {
   optionst options;
-  symbol_tablet new_symbol_table;
+  concrete_symbol_tablet new_symbol_table;
   goto_program_dereferencet
     goto_program_dereference(ns, new_symbol_table, options, value_sets);
   goto_program_dereference.dereference_expression(target, expr);