JBMC: add failed symbols on a per-function basis

This uses our journal of all new symbols relating to this function, both
from the front-end's activity and subsequent goto-conversion and post-processing
(e.g. remove-returns' new symbols) and creates corresponding failed symbols.

Author: smowton

src/jbmc/jbmc_parse_options.cpp

@@ -573,6 +573,10 @@ int jbmc_parse_optionst::get_goto_program(
       *this, options, get_message_handler());
     lazy_goto_model.initialize(cmdline);
 
+    // Add failed symbols for any symbol created prior to loading any
+    // particular function:
+    add_failed_symbols(lazy_goto_model.symbol_table);
+
     status() << "Generating GOTO Program" << messaget::eom;
     lazy_goto_model.load_all_functions();
 
@@ -693,6 +697,17 @@ void jbmc_parse_optionst::process_goto_function(
 
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_function, ns);
+
+    // add failed symbols for anything created relating to this particular
+    // function (note this means subseqent passes mustn't create more!):
+    journalling_symbol_tablet::changesett new_symbols =
+      symbol_table.get_inserted();
+    for(const irep_idt &new_symbol_name : new_symbols)
+    {
+      add_failed_symbol_if_needed(
+        symbol_table.lookup_ref(new_symbol_name),
+        symbol_table);
+    }
   }
 
   catch(const char *e)
@@ -739,10 +754,6 @@ bool jbmc_parse_optionst::process_goto_functions(
       nondet_static(goto_model);
     }
 
-    // add failed symbols
-    // needs to be done before pointer analysis
-    add_failed_symbols(goto_model.symbol_table);
-
     // recalculate numbers, etc.
     goto_model.goto_functions.update();
 

src/pointer-analysis/add_failed_symbols.cpp

@@ -20,7 +20,7 @@ irep_idt failed_symbol_id(const irep_idt &id)
   return id2string(id)+"$object";
 }
 
-void add_failed_symbol(symbolt &symbol, symbol_tablet &symbol_table)
+void add_failed_symbol(symbolt &symbol, symbol_table_baset &symbol_table)
 {
   if(symbol.type.id()==ID_pointer)
   {
@@ -43,7 +43,8 @@ void add_failed_symbol(symbolt &symbol, symbol_tablet &symbol_table)
   }
 }
 
-void add_failed_symbol(const symbolt &symbol, symbol_tablet &symbol_table)
+void add_failed_symbol_if_needed(
+  const symbolt &symbol, symbol_table_baset &symbol_table)
 {
   if(!symbol.is_lvalue)
     return;
@@ -54,7 +55,7 @@ void add_failed_symbol(const symbolt &symbol, symbol_tablet &symbol_table)
   add_failed_symbol(*symbol_table.get_writeable(symbol.name), symbol_table);
 }
 
-void add_failed_symbols(symbol_tablet &symbol_table)
+void add_failed_symbols(symbol_table_baset &symbol_table)
 {
   // the symbol table iterators are not stable, and
   // we are adding new symbols, this
@@ -64,7 +65,7 @@ void add_failed_symbols(symbol_tablet &symbol_table)
     symbol_list.push_back(&(named_symbol.second));
 
   for(const symbolt *symbol : symbol_list)
-    add_failed_symbol(*symbol, symbol_table);
+    add_failed_symbol_if_needed(*symbol, symbol_table);
 }
 
 exprt get_failed_symbol(

src/pointer-analysis/add_failed_symbols.h

@@ -14,12 +14,16 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/irep.h>
 
-class symbol_tablet;
+class symbol_table_baset;
+class symbolt;
 class exprt;
 class namespacet;
 class symbol_exprt;
 
-void add_failed_symbols(symbol_tablet &symbol_table);
+void add_failed_symbols(symbol_table_baset &symbol_table);
+
+void add_failed_symbol_if_needed(
+  const symbolt &symbol, symbol_table_baset &symbol_table);
 
 irep_idt failed_symbol_id(const irep_idt &identifier);