Slice global inits: update the symbol table

Update the symbol table and auto-generate __CPROVER_initialize instead
of hand-tweaking the function. This will ensure that any further
rebuilding of __CPROVER_initialize preserves those changes.

Author: tautschnig

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1376,7 +1376,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   {
     log.status() << "Slicing away initializations of unused global variables"
                  << messaget::eom;
-    slice_global_inits(goto_model);
+    slice_global_inits(goto_model, ui_message_handler);
   }
 
   if(cmdline.isset("string-abstraction"))
@@ -1663,7 +1663,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
     log.status() << "Slicing away initializations of unused global variables"
                  << messaget::eom;
-    slice_global_inits(goto_model);
+    slice_global_inits(goto_model, ui_message_handler);
 
     log.status() << "Performing an aggressive slice" << messaget::eom;
     aggressive_slicert aggressive_slicer(goto_model, ui_message_handler);

src/goto-programs/slice_global_inits.cpp

@@ -20,15 +20,15 @@ Date:   December 2016
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
 
-#include <util/invariant.h>
-
-#include <goto-programs/goto_functions.h>
-#include <goto-programs/goto_model.h>
-#include <goto-programs/remove_skip.h>
-
 #include <linking/static_lifetime_init.h>
 
-void slice_global_inits(goto_modelt &goto_model)
+#include "goto_convert_functions.h"
+#include "goto_functions.h"
+#include "goto_model.h"
+
+void slice_global_inits(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
 {
   // gather all functions reachable from the entry point
   const irep_idt entry_point=goto_functionst::entry_point();
@@ -115,22 +115,35 @@ void slice_global_inits(goto_modelt &goto_model)
   }
 
   // now remove unnecessary initializations
-  for(auto &instruction : goto_program.instructions)
+  bool changed = false;
+  for(auto &entry : goto_model.symbol_table)
   {
-    if(instruction.is_assign())
+    if(
+      entry.second.is_static_lifetime && !entry.second.is_type &&
+      !entry.second.is_macro && entry.second.type.id() != ID_code &&
+      !has_prefix(id2string(entry.first), CPROVER_PREFIX) &&
+      symbols_to_keep.find(entry.first) == symbols_to_keep.end())
     {
-      const symbol_exprt &symbol_expr =
-        to_symbol_expr(instruction.assign_lhs());
-      const irep_idt id=symbol_expr.get_identifier();
-
-      if(
-        !has_prefix(id2string(id), CPROVER_PREFIX) &&
-        symbols_to_keep.find(id) == symbols_to_keep.end())
-      {
-        instruction.turn_into_skip();
-      }
+      symbolt &symbol = goto_model.symbol_table.get_writeable_ref(entry.first);
+      symbol.is_extern = true;
+      symbol.value.make_nil();
+      symbol.value.set(ID_C_no_nondet_initialization, 1);
+      changed = true;
     }
   }
 
-  remove_skip(goto_functions);
+  if(
+    changed &&
+    goto_model.goto_functions.function_map.erase(INITIALIZE_FUNCTION) != 0)
+  {
+    static_lifetime_init(
+      goto_model.symbol_table,
+      goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location);
+    goto_convert(
+      INITIALIZE_FUNCTION,
+      goto_model.symbol_table,
+      goto_model.goto_functions,
+      message_handler);
+    goto_model.goto_functions.update();
+  }
 }

src/goto-programs/slice_global_inits.h

@@ -17,6 +17,7 @@ Date:   December 2016
 #include <util/exception_utils.h>
 
 class goto_modelt;
+class message_handlert;
 
 class user_input_error_exceptiont : public cprover_exception_baset
 {
@@ -35,6 +36,11 @@ class user_input_error_exceptiont : public cprover_exception_baset
   std::string message;
 };
 
-void slice_global_inits(goto_modelt &);
+/// Remove initialization of global variables that are not used in any function
+/// reachable from the entry point of \p goto_model.
+/// Warnings are reported via \p message_handler.
+void slice_global_inits(
+  goto_modelt &goto_model,
+  message_handlert &message_handler);
 
 #endif

src/linking/static_lifetime_init.cpp

@@ -72,6 +72,9 @@ static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
   if((symbol.value.is_nil() && symbol.is_extern) ||
      symbol.value.id() == ID_nondet)
   {
+    if(symbol.value.get_bool(ID_C_no_nondet_initialization))
+      return {};
+
     // Nondet initialise if not linked, or if explicitly requested.
     // Compilers would usually complain about the unlinked symbol case.
     const auto nondet = nondet_initializer(symbol.type, symbol.location, ns);