JBMC: run add-failed-symbols on a per-function basis

src/goto-programs/convert_nondet.cpp

@@ -32,7 +32,7 @@ Author: Reuben Thomas, [email protected]
 static goto_programt::targett insert_nondet_init_code(
   goto_programt &goto_program,
   const goto_programt::targett &target,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   const object_factory_parameterst &object_factory_parameters)
 {
@@ -113,7 +113,7 @@ static goto_programt::targett insert_nondet_init_code(
 /// \param max_nondet_array_length: Maximum size of new nondet arrays.
 void convert_nondet(
   goto_programt &goto_program,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   const object_factory_parameterst &object_factory_parameters)
 {
@@ -146,7 +146,7 @@ void convert_nondet(
 
 void convert_nondet(
   goto_functionst &goto_functions,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   const object_factory_parameterst &object_factory_parameters)
 {

src/goto-programs/convert_nondet.h

@@ -15,7 +15,7 @@ Author: Reuben Thomas, [email protected]
 #include <cstddef> // size_t
 
 class goto_functionst;
-class symbol_tablet;
+class symbol_table_baset;
 class goto_modelt;
 class goto_model_functiont;
 class message_handlert;
@@ -30,7 +30,7 @@ struct object_factory_parameterst;
 ///   objects.
 void convert_nondet(
   goto_functionst &,
-  symbol_tablet &,
+  symbol_table_baset &,
   message_handlert &,
   const object_factory_parameterst &object_factory_parameters);
 

src/goto-programs/goto_convert.cpp

@@ -2178,7 +2178,7 @@ const symbolt &goto_convertt::lookup(const irep_idt &identifier)
 
 void goto_convert(
   const codet &code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_programt &dest,
   message_handlert &message_handler)
 {
@@ -2212,7 +2212,7 @@ void goto_convert(
 }
 
 void goto_convert(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_programt &dest,
   message_handlert &message_handler)
 {

src/goto-programs/goto_convert.h

@@ -20,13 +20,13 @@ Author: Daniel Kroening, [email protected]
 // start from given code
 void goto_convert(
   const codet &code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_programt &dest,
   message_handlert &message_handler);
 
 // start from "main"
 void goto_convert(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_programt &dest,
   message_handlert &message_handler);
 

src/goto-programs/goto_convert_class.h

@@ -29,7 +29,7 @@ class goto_convertt:public messaget
   void goto_convert(const codet &code, goto_programt &dest);
 
   goto_convertt(
-    symbol_tablet &_symbol_table,
+    symbol_table_baset &_symbol_table,
     message_handlert &_message_handler):
     messaget(_message_handler),
     symbol_table(_symbol_table),
@@ -44,7 +44,7 @@ class goto_convertt:public messaget
   }
 
 protected:
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
   namespacet ns;
   unsigned temporary_counter;
   std::string tmp_symbol_prefix;

src/goto-programs/goto_convert_functions.cpp

@@ -21,7 +21,7 @@ Date: June 2003
 #include "goto_inline.h"
 
 goto_convert_functionst::goto_convert_functionst(
-  symbol_tablet &_symbol_table,
+  symbol_table_baset &_symbol_table,
   message_handlert &_message_handler):
   goto_convertt(_symbol_table, _message_handler)
 {
@@ -234,7 +234,7 @@ void goto_convert(
 }
 
 void goto_convert(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_functionst &functions,
   message_handlert &message_handler)
 {
@@ -269,7 +269,7 @@ void goto_convert(
 
 void goto_convert(
   const irep_idt &identifier,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_functionst &functions,
   message_handlert &message_handler)
 {

src/goto-programs/goto_convert_functions.h

@@ -20,7 +20,7 @@ Date: June 2003
 
 // convert it all!
 void goto_convert(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_functionst &functions,
   message_handlert &);
 
@@ -32,7 +32,7 @@ void goto_convert(
 // just convert a specific function
 void goto_convert(
   const irep_idt &identifier,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_functionst &functions,
   message_handlert &);
 
@@ -45,7 +45,7 @@ class goto_convert_functionst:public goto_convertt
     goto_functionst::goto_functiont &result);
 
   goto_convert_functionst(
-    symbol_tablet &_symbol_table,
+    symbol_table_baset &_symbol_table,
     message_handlert &_message_handler);
 
   virtual ~goto_convert_functionst();

src/goto-programs/goto_model.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
 
 #include <util/symbol_table.h>
+#include <util/journalling_symbol_table.h>
 
 #include "goto_functions.h"
 
@@ -82,9 +83,12 @@ class goto_model_functiont
   ///   goto programs, specifically incrementing its unused_location_number
   ///   member each time a program is re-numbered.
   /// \param goto_function: function to wrap.
-  explicit goto_model_functiont(
-    goto_modelt &goto_model, goto_functionst::goto_functiont &goto_function):
-  goto_model(goto_model),
+  goto_model_functiont(
+    journalling_symbol_tablet &symbol_table,
+    goto_functionst &goto_functions,
+    goto_functionst::goto_functiont &goto_function):
+  symbol_table(symbol_table),
+  goto_functions(goto_functions),
   goto_function(goto_function)
   {
   }
@@ -94,14 +98,16 @@ class goto_model_functiont
   /// program order within the program.
   void compute_location_numbers()
   {
-    goto_model.goto_functions.compute_location_numbers(goto_function.body);
+    goto_functions.compute_location_numbers(goto_function.body);
   }
 
   /// Get symbol table
-  /// \return symbol table from the associated GOTO model
-  symbol_tablet &get_symbol_table()
+  /// \return journalling symbol table that (a) wraps the global symbol table,
+  ///   and (b) has recorded all symbol mutations (insertions, updates and
+  ///   deletions) that resulted from creating `goto_function`.
+  journalling_symbol_tablet &get_symbol_table()
   {
-    return goto_model.symbol_table;
+    return symbol_table;
   }
 
   /// Get GOTO function
@@ -111,17 +117,9 @@ class goto_model_functiont
     return goto_function;
   }
 
-  /// Get GOTO model. This returns a const reference because this interface is
-  /// intended for use where non-const access to the whole model should not be
-  /// allowed.
-  /// \return const view of the whole GOTO model.
-  const goto_modelt &get_goto_model()
-  {
-    return goto_model;
-  }
-
 private:
-  goto_modelt &goto_model;
+  journalling_symbol_tablet &symbol_table;
+  goto_functionst &goto_functions;
   goto_functionst::goto_functiont &goto_function;
 };
 

src/goto-programs/lazy_goto_functions_map.h

@@ -11,7 +11,7 @@
 #include "goto_convert_functions.h"
 #include <util/message.h>
 #include <util/language_file.h>
-
+#include <util/journalling_symbol_table.h>
 
 /// Provides a wrapper for a map of lazily loaded goto_functiont.
 /// This incrementally builds a goto-functions object, while permitting
@@ -48,7 +48,9 @@ class lazy_goto_functions_mapt final
   typedef std::size_t size_type;
 
   typedef
-  std::function<void(goto_functionst::goto_functiont &function)>
+    std::function<void(
+      goto_functionst::goto_functiont &function,
+      journalling_symbol_tablet &function_symbols)>
     post_process_functiont;
 
 private:
@@ -61,11 +63,8 @@ class lazy_goto_functions_mapt final
 
   language_filest &language_files;
   symbol_tablet &symbol_table;
-  // This is mutable because it has internal state that it changes during the
-  // course of conversion. Strictly it should make that state mutable or
-  // recreate it for each conversion, but it's easier just to store it mutable.
-  mutable goto_convert_functionst convert_functions;
   const post_process_functiont post_process_function;
+  message_handlert &message_handler;
 
 public:
   /// Creates a lazy_goto_functions_mapt.
@@ -78,8 +77,8 @@ class lazy_goto_functions_mapt final
   : goto_functions(goto_functions),
     language_files(language_files),
     symbol_table(symbol_table),
-    convert_functions(symbol_table, message_handler),
-    post_process_function(std::move(post_process_function))
+    post_process_function(std::move(post_process_function)),
+    message_handler(message_handler)
   {
   }
 
@@ -122,29 +121,43 @@ class lazy_goto_functions_mapt final
   // const first
   reference ensure_function_loaded_internal(const key_type &name) const
   {
-    reference named_function=ensure_entry_converted(name);
+    journalling_symbol_tablet journalling_table =
+      journalling_symbol_tablet::wrap(symbol_table);
+    reference named_function=ensure_entry_converted(name, journalling_table);
     mapped_type function=named_function.second;
     if(processed_functions.count(name)==0)
     {
       // Run function-pass conversions
-      post_process_function(function);
+      post_process_function(function, journalling_table);
       // Assign procedure-local location numbers for now
       function.body.compute_location_numbers();
       processed_functions.insert(name);
     }
     return named_function;
   }
 
-  reference ensure_entry_converted(const key_type &name) const
+  /// Convert a function if not already converted, then return a reference to
+  /// its goto_functionst map entry.
+  /// \param name: ID of the function to convert
+  /// \param function_symbol_table: mutable symbol table reference to be used
+  ///   when converting the function (e.g. to add new local variables).
+  ///   Note we should not use a global pre-cached symbol table reference for
+  ///   this so that our callers can insert a journalling table here if needed.
+  /// \return reference to the new or existing goto_functions map entry.
+  reference ensure_entry_converted(
+    const key_type &name,
+    symbol_table_baset &function_symbol_table) const
   {
     typename underlying_mapt::iterator it=goto_functions.find(name);
     if(it!=goto_functions.end())
       return *it;
     // Fill in symbol table entry body if not already done
     // If this returns false then it's a stub
-    language_files.convert_lazy_method(name, symbol_table);
+    language_files.convert_lazy_method(name, function_symbol_table);
     // Create goto_functiont
     goto_functionst::goto_functiont function;
+    goto_convert_functionst convert_functions(
+      function_symbol_table, message_handler);
     convert_functions.convert_function(name, function);
     // Add to map
     return *goto_functions.emplace(name, std::move(function)).first;

src/goto-programs/lazy_goto_model.cpp

@@ -28,9 +28,14 @@ lazy_goto_modelt::lazy_goto_modelt(
       goto_model->goto_functions.function_map,
       language_files,
       symbol_table,
-      [this] (goto_functionst::goto_functiont &function) -> void
+      [this] (
+        goto_functionst::goto_functiont &function,
+        journalling_symbol_tablet &journalling_symbol_table) -> void
       {
-        goto_model_functiont model_function(*goto_model, function);
+        goto_model_functiont model_function(
+          journalling_symbol_table,
+          goto_model->goto_functions,
+          function);
         this->post_process_function(model_function, *this);
       },
       message_handler),
@@ -48,9 +53,14 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
       goto_model->goto_functions.function_map,
       language_files,
       symbol_table,
-      [this] (goto_functionst::goto_functiont &function) -> void
+      [this] (
+        goto_functionst::goto_functiont &function,
+        journalling_symbol_tablet &journalling_symbol_table) -> void
       {
-        goto_model_functiont model_function(*goto_model, function);
+        goto_model_functiont model_function(
+          journalling_symbol_table,
+          goto_model->goto_functions,
+          function);
         this->post_process_function(model_function, *this);
       },
       other.message_handler),

src/goto-programs/remove_instanceof.cpp

@@ -22,7 +22,7 @@ Author: Chris Smowton, [email protected]
 class remove_instanceoft
 {
 public:
-  explicit remove_instanceoft(symbol_tablet &symbol_table)
+  explicit remove_instanceoft(symbol_table_baset &symbol_table)
   : symbol_table(symbol_table), ns(symbol_table)
   {
     class_hierarchy(symbol_table);
@@ -35,7 +35,7 @@ class remove_instanceoft
   bool lower_instanceof(goto_programt &, goto_programt::targett);
 
 protected:
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
   namespacet ns;
   class_hierarchyt class_hierarchy;
 
@@ -183,7 +183,7 @@ bool remove_instanceoft::lower_instanceof(goto_programt &goto_program)
 void remove_instanceof(
   goto_programt::targett target,
   goto_programt &goto_program,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   remove_instanceoft rem(symbol_table);
   rem.lower_instanceof(goto_program, target);
@@ -196,7 +196,7 @@ void remove_instanceof(
 /// \param symbol_table: The symbol table to add symbols to.
 void remove_instanceof(
   goto_functionst::goto_functiont &function,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   remove_instanceoft rem(symbol_table);
   rem.lower_instanceof(function.body);
@@ -209,7 +209,7 @@ void remove_instanceof(
 /// \param symbol_table: The symbol table to add symbols to.
 void remove_instanceof(
   goto_functionst &goto_functions,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   remove_instanceoft rem(symbol_table);
   bool changed=false;