Merge pull request diffblue#213 from diffblue/feature/recording-symbol-table

Recording symbol table

Author: NathanJPhillips

cbmc/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;

cbmc/src/ansi-c/ansi_c_entry_point.cpp

@@ -478,7 +478,7 @@ bool generate_ansi_c_start_function(
   new_symbol.value.swap(init_code);
   new_symbol.mode=symbol.mode;
 
-  if(!symbol_table.insert(std::move(new_symbol)))
+  if(!symbol_table.insert(std::move(new_symbol)).second)
   {
     messaget message;
     message.set_message_handler(message_handler);

cbmc/src/ansi-c/ansi_c_language.cpp

@@ -106,7 +106,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,

cbmc/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(

cbmc/src/ansi-c/type2name.cpp

@@ -266,6 +266,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));
 }

cbmc/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;

cbmc/src/cpp/cpp_language.cpp

@@ -126,7 +126,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()))

cbmc/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,

cbmc/src/cpp/cpp_typecheck_compound_type.cpp

@@ -536,7 +536,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
         vt_symb_type.type.set(ID_name, vt_symb_type.name);
         vt_symb_type.is_type=true;
 
-        const bool failed=!symbol_table.insert(std::move(vt_symb_type));
+        const bool failed=!symbol_table.insert(std::move(vt_symb_type)).second;
         assert(!failed);
 
         // add a virtual-table pointer
@@ -612,7 +612,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
           arg.set(ID_C_identifier, arg_symb.name);
 
           // add the parameter to the symbol table
-          const bool failed=!symbol_table.insert(std::move(arg_symb));
+          const bool failed=!symbol_table.insert(std::move(arg_symb)).second;
           assert(!failed);
         }
 
@@ -670,7 +670,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
 
         // add the function to the symbol table
         {
-          bool failed=!symbol_table.insert(std::move(func_symb));
+          bool failed=!symbol_table.insert(std::move(func_symb)).second;
           assert(!failed);
         }
 

cbmc/src/cpp/cpp_typecheck_namespace.cpp

@@ -73,7 +73,7 @@ void cpp_typecheckt::convert(cpp_namespace_spect &namespace_spec)
     symbol.module=module;
     symbol.type=typet(ID_namespace);
 
-    if(!symbol_table.insert(std::move(symbol)))
+    if(!symbol_table.insert(std::move(symbol)).second)
     {
       error().source_location=symbol.location;
       error() << "cpp_typecheckt::convert_namespace: symbol_table.move() failed"

cbmc/src/cpp/cpp_typecheck_virtual_table.cpp

@@ -95,7 +95,7 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
     }
     vt_symb_var.value=values;
 
-    bool failed=!symbol_table.insert(std::move(vt_symb_var));
+    bool failed=!symbol_table.insert(std::move(vt_symb_var)).second;
     assert(!failed);
   }
 }

cbmc/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());

cbmc/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;

cbmc/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;

cbmc/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;

cbmc/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()

cbmc/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

cbmc/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)
 {

cbmc/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 &);
 

cbmc/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;

cbmc/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,16 @@ 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 +427,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 +440,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

cbmc/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,

cbmc/src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -82,7 +82,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);
@@ -108,7 +108,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 << '"' << '=';
@@ -117,7 +117,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)

cbmc/src/java_bytecode/java_entry_point.cpp

@@ -669,7 +669,7 @@ bool generate_java_start_function(
   new_symbol.value.swap(init_code);
   new_symbol.mode=ID_java;
 
-  if(!symbol_table.insert(std::move(new_symbol)))
+  if(!symbol_table.insert(std::move(new_symbol)).second)
   {
     message.error() << "failed to move main symbol" << messaget::eom;
     return true;

cbmc/src/java_bytecode/java_utils.cpp

@@ -86,10 +86,9 @@ void generate_class_stub(
   new_symbol.mode=ID_java;
   new_symbol.is_type=true;
 
-  optionalt<std::reference_wrapper<symbolt>> res=
-    symbol_table.insert(std::move(new_symbol));
+  std::pair<symbolt &, bool> res=symbol_table.insert(std::move(new_symbol));
 
-  if(!res)
+  if(!res.second)
   {
     messaget message(message_handler);
     message.warning() <<
@@ -100,7 +99,7 @@ void generate_class_stub(
   else
   {
     // create the class identifier etc
-    java_root_class(*res);
+    java_root_class(res.first);
   }
 }
 

cbmc/src/jsil/jsil_entry_point.cpp

@@ -162,7 +162,7 @@ bool jsil_entry_point(
   new_symbol.type.swap(main_type);
   new_symbol.value.swap(init_code);
 
-  if(!symbol_table.insert(std::move(new_symbol)))
+  if(!symbol_table.insert(std::move(new_symbol)).second)
   {
     messaget message;
     message.set_message_handler(message_handler);

cbmc/src/jsil/jsil_language.cpp

@@ -152,7 +152,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());
 

cbmc/src/jsil/jsil_typecheck.cpp

@@ -927,7 +927,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,

cbmc/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,

cbmc/src/langapi/language_util.cpp

@@ -153,13 +153,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);
 }
 
@@ -185,6 +185,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);
 }