Merge pull request #1558 from NathanJPhillips/feature/complete-journalling_symbol_table

Complete journalling symbol table

Author: peterschrammel

src/java_bytecode/java_bytecode_instrument.cpp

@@ -28,20 +28,20 @@ class java_bytecode_instrumentt:public messaget
 {
 public:
   java_bytecode_instrumentt(
-    symbol_tablet &_symbol_table,
+    symbol_table_baset &_symbol_table,
     const bool _throw_runtime_exceptions,
-    message_handlert &_message_handler):
-    messaget(_message_handler),
-    symbol_table(_symbol_table),
-    throw_runtime_exceptions(_throw_runtime_exceptions),
-    message_handler(_message_handler)
-    {
-    }
+    message_handlert &_message_handler)
+    : messaget(_message_handler),
+      symbol_table(_symbol_table),
+      throw_runtime_exceptions(_throw_runtime_exceptions),
+      message_handler(_message_handler)
+  {
+  }
 
   void operator()(exprt &expr);
 
 protected:
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
   const bool throw_runtime_exceptions;
   message_handlert &message_handler;
 
@@ -577,7 +577,7 @@ void java_bytecode_instrumentt::operator()(exprt &expr)
 ///   this flag is set to true.
 /// \param message_handler: stream to report status and warnings
 void java_bytecode_instrument_symbol(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   symbolt &symbol,
   const bool throw_runtime_exceptions,
   message_handlert &message_handler)

src/java_bytecode/java_bytecode_instrument.h

@@ -12,7 +12,7 @@ Date:   June 2017
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H
 
 void java_bytecode_instrument_symbol(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   symbolt &symbol,
   const bool throw_runtime_exceptions,
   message_handlert &_message_handler);

src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/c_types.h>
 
-void java_internal_additions(symbol_tablet &dest)
+void java_internal_additions(symbol_table_baset &dest)
 {
   // add __CPROVER_rounding_mode
 

src/java_bytecode/java_bytecode_internal_additions.h

@@ -10,8 +10,8 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INTERNAL_ADDITIONS_H
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INTERNAL_ADDITIONS_H
 
-#include <util/symbol_table.h>
+#include <util/symbol_table_base.h>
 
-void java_internal_additions(symbol_tablet &dest);
+void java_internal_additions(symbol_table_baset &dest);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INTERNAL_ADDITIONS_H

src/java_bytecode/java_bytecode_language.cpp

@@ -355,7 +355,7 @@ void java_bytecode_languaget::convert_lazy_method(
 /// generated by string_preprocess.
 /// \param context: a symbol table
 void java_bytecode_languaget::replace_string_methods(
-  symbol_tablet &context)
+  symbol_table_baset &context)
 {
   // Symbols that have code type are potentialy to be replaced
   std::list<symbolt> code_symbols;
@@ -386,7 +386,7 @@ void java_bytecode_languaget::replace_string_methods(
   }
 }
 
-bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
+bool java_bytecode_languaget::final(symbol_table_baset &symbol_table)
 {
   PRECONDITION(language_options_initialized);
 

src/java_bytecode/java_bytecode_language.h

@@ -108,10 +108,9 @@ class java_bytecode_languaget:public languaget
     symbol_tablet &context,
     const std::string &module) override;
 
-  void replace_string_methods(symbol_tablet &context);
+  void replace_string_methods(symbol_table_baset &context);
 
-  virtual bool final(
-    symbol_tablet &context) override;
+  virtual bool final(symbol_table_baset &context) override;
 
   void show_parse(std::ostream &out) override;
 

src/java_bytecode/java_entry_point.cpp

@@ -36,7 +36,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_types.h"
 #include "java_utils.h"
 
-static void create_initialize(symbol_tablet &symbol_table)
+static void create_initialize(symbol_table_baset &symbol_table)
 {
   // If __CPROVER_initialize already exists, replace it. It may already exist
   // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend.
@@ -89,8 +89,8 @@ static bool is_non_null_library_global(const irep_idt &symbolid)
   return non_null_globals.count(symbolid);
 }
 
-void java_static_lifetime_init(
-  symbol_tablet &symbol_table,
+static void java_static_lifetime_init(
+  symbol_table_baset &symbol_table,
   const source_locationt &source_location,
   bool assume_init_pointers_not_null,
   const object_factory_parameterst &object_factory_parameters,
@@ -162,7 +162,7 @@ void java_static_lifetime_init(
 exprt::operandst java_build_arguments(
   const symbolt &function,
   code_blockt &init_code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   bool assume_init_pointers_not_null,
   object_factory_parameterst object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
@@ -246,7 +246,7 @@ void java_record_outputs(
   const symbolt &function,
   const exprt::operandst &main_arguments,
   code_blockt &init_code,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   const code_typet::parameterst &parameters=
     to_code_type(function.type).parameters();
@@ -319,7 +319,7 @@ void java_record_outputs(
 }
 
 main_function_resultt get_main_symbol(
-  symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   const irep_idt &main_class,
   message_handlert &message_handler,
   bool allow_no_body)
@@ -445,7 +445,7 @@ main_function_resultt get_main_symbol(
 ///
 /// \returns true if error occurred on entry point search
 bool java_entry_point(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const irep_idt &main_class,
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
@@ -500,7 +500,7 @@ bool java_entry_point(
 /// \returns true if error occurred on entry point search, false otherwise
 bool generate_java_start_function(
   const symbolt &symbol,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   const object_factory_parameterst& object_factory_parameters,

src/java_bytecode/java_entry_point.h

@@ -19,7 +19,7 @@ Author: Daniel Kroening, [email protected]
 #define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL "uncaught_exception'"
 
 bool java_entry_point(
-  class symbol_tablet &symbol_table,
+  class symbol_table_baset &symbol_table,
   const irep_idt &main_class,
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
@@ -61,14 +61,14 @@ struct main_function_resultt
 
 /// Figures out the entry point of the code to verify
 main_function_resultt get_main_symbol(
-  symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   const irep_idt &main_class,
   message_handlert &,
-  bool allow_no_body=false);
+  bool allow_no_body = false);
 
 bool generate_java_start_function(
   const symbolt &symbol,
-  class symbol_tablet &symbol_table,
+  class symbol_table_baset &symbol_table,
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   const object_factory_parameterst& object_factory_parameters,

src/java_bytecode/java_object_factory.cpp

@@ -35,10 +35,10 @@ Author: Daniel Kroening, [email protected]
 #include "java_root_class.h"
 
 static symbolt &new_tmp_symbol(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   const typet &type,
-  const std::string &prefix="tmp_object_factory")
+  const std::string &prefix = "tmp_object_factory")
 {
   return get_fresh_aux_symbol(
     type,
@@ -69,7 +69,7 @@ class java_object_factoryt
   std::unordered_set<irep_idt, irep_id_hash> recursion_set;
 
   /// The symbol table.
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
 
   /// A namespace built from exclusively one symbol table - the one above.
   namespacet ns;
@@ -102,9 +102,9 @@ class java_object_factoryt
     std::vector<const symbolt *> &_symbols_created,
     const source_locationt &loc,
     const object_factory_parameterst _object_factory_parameters,
-    symbol_tablet &_symbol_table,
-    const select_pointer_typet &pointer_type_selector):
-      symbols_created(_symbols_created),
+    symbol_table_baset &_symbol_table,
+    const select_pointer_typet &pointer_type_selector)
+    : symbols_created(_symbols_created),
       loc(loc),
       object_factory_parameters(_object_factory_parameters),
       symbol_table(_symbol_table),
@@ -182,7 +182,7 @@ class java_object_factoryt
 exprt allocate_dynamic_object(
   const exprt &target_expr,
   const typet &allocate_type,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &output_code,
   std::vector<const symbolt *> &symbols_created,
@@ -241,7 +241,7 @@ exprt allocate_dynamic_object(
 /// \param output_code: code block to which the necessary code is added
 void allocate_dynamic_object_with_decl(
   const exprt &target_expr,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &output_code)
 {
@@ -543,7 +543,7 @@ codet initialize_nondet_string_struct(
   const exprt &obj,
   const std::size_t &max_nondet_string_length,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   bool printable)
 {
   PRECONDITION(
@@ -636,7 +636,7 @@ static bool add_nondet_string_pointer_initialization(
   const exprt &expr,
   const std::size_t &max_nondet_string_length,
   bool printable,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &code)
 {
@@ -1361,7 +1361,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   bool allow_null,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const object_factory_parameterst &parameters,
   allocation_typet alloc_type,
   const source_locationt &loc,
@@ -1457,7 +1457,7 @@ exprt object_factory(
 void gen_nondet_init(
   const exprt &expr,
   code_blockt &init_code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
@@ -1521,7 +1521,7 @@ exprt object_factory(
 void gen_nondet_init(
   const exprt &expr,
   code_blockt &init_code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,

src/java_bytecode/java_object_factory.h

@@ -91,7 +91,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   bool allow_null,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const object_factory_parameterst &parameters,
   allocation_typet alloc_type,
   const source_locationt &location,
@@ -117,7 +117,7 @@ enum class update_in_placet
 void gen_nondet_init(
   const exprt &expr,
   code_blockt &init_code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
@@ -129,7 +129,7 @@ void gen_nondet_init(
 void gen_nondet_init(
   const exprt &expr,
   code_blockt &init_code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
@@ -140,23 +140,23 @@ void gen_nondet_init(
 exprt allocate_dynamic_object(
   const exprt &target_expr,
   const typet &allocate_type,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &output_code,
   std::vector<const symbolt *> &symbols_created,
-  bool cast_needed=false);
+  bool cast_needed = false);
 
 void allocate_dynamic_object_with_decl(
   const exprt &target_expr,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &output_code);
 
 codet initialize_nondet_string_struct(
   const exprt &obj,
   const std::size_t &max_nondet_string_length,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   bool printable);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H