Merge pull request #7680 from tautschnig/cleanup/recreate-init

Factor out re-creating __CPROVER_initialize into a function

Author: kroening

src/goto-cc/linker_script_merge.cpp

@@ -84,20 +84,11 @@ int linker_script_merget::add_linker_script_definitions()
                 << messaget::eom;
     return fail;
   }
-  if(
-    original_goto_model->goto_functions.function_map.erase(
-      INITIALIZE_FUNCTION) != 0)
+
+  if(original_goto_model->can_produce_function(INITIALIZE_FUNCTION))
   {
-    static_lifetime_init(
-      original_goto_model->symbol_table,
-      original_goto_model->symbol_table.lookup_ref(INITIALIZE_FUNCTION)
-        .location);
-    goto_convert(
-      INITIALIZE_FUNCTION,
-      original_goto_model->symbol_table,
-      original_goto_model->goto_functions,
-      log.get_message_handler());
-    original_goto_model->goto_functions.update();
+    recreate_initialize_function(
+      *original_goto_model, log.get_message_handler());
   }
 
   fail=goto_and_object_mismatch(linker_defined_symbols, linker_values);

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -560,8 +560,8 @@ void dfcct::reinitialize_model()
   swap_and_wrap.get_swapped_functions(instrumented_functions);
 
   log.status() << "Updating init function" << messaget::eom;
-  utils.create_initialize_function();
-  goto_model.goto_functions.update();
+  if(goto_model.can_produce_function(INITIALIZE_FUNCTION))
+    recreate_initialize_function(goto_model, message_handler);
   nondet_static(goto_model, to_exclude_from_nondet_static);
 
   // Initialize the map of instrumented functions by adding extra instructions

src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp

@@ -140,22 +140,6 @@ const symbolt &dfcc_utilst::create_static_symbol(
   return symbol;
 }
 
-void dfcc_utilst::create_initialize_function()
-{
-  if(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();
-  }
-}
-
 void dfcc_utilst::fix_parameters_symbols(const irep_idt &function_id)
 {
   auto &function_symbol = get_function_symbol(function_id);

src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h

@@ -82,10 +82,6 @@ class dfcc_utilst
     const exprt &initial_value,
     const bool no_nondet_initialization = true);
 
-  /// Regenerates the CPROVER_INITIALIZE function which defines all global
-  /// statics of the goto model.
-  void create_initialize_function();
-
   /// Creates a new parameter symbol for the given function_id
   const symbolt &create_new_parameter_symbol(
     const irep_idt &function_id,

src/goto-instrument/contracts/memory_predicates.cpp

@@ -210,18 +210,8 @@ void is_fresh_baset::add_declarations(const std::string &decl_string)
     }
   }
 
-  if(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,
-      log.get_message_handler());
-    goto_model.goto_functions.update();
-  }
+  if(goto_model.can_produce_function(INITIALIZE_FUNCTION))
+    recreate_initialize_function(goto_model, message_handler);
 }
 
 void is_fresh_baset::update_fn_call(

src/goto-instrument/stack_depth.cpp

@@ -40,18 +40,8 @@ static symbol_exprt add_stack_depth_symbol(
   bool failed = goto_model.symbol_table.add(new_symbol);
   CHECK_RETURN(!failed);
 
-  if(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();
-  }
+  if(goto_model.can_produce_function(INITIALIZE_FUNCTION))
+    recreate_initialize_function(goto_model, message_handler);
 
   return new_symbol.symbol_expr();
 }

src/goto-programs/link_to_library.cpp

@@ -159,19 +159,8 @@ void link_to_library(
       break;
   }
 
-  if(need_reinit)
-  {
-    goto_model.unload(INITIALIZE_FUNCTION);
-    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();
-  }
+  if(need_reinit && goto_model.can_produce_function(INITIALIZE_FUNCTION))
+    recreate_initialize_function(goto_model, message_handler);
 
   if(!object_type_updates.empty())
     finalize_linking(goto_model, object_type_updates);

src/goto-programs/slice_global_inits.cpp

@@ -22,7 +22,6 @@ Date:   December 2016
 
 #include <linking/static_lifetime_init.h>
 
-#include "goto_convert_functions.h"
 #include "goto_functions.h"
 #include "goto_model.h"
 
@@ -132,18 +131,6 @@ void slice_global_inits(
     }
   }
 
-  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();
-  }
+  if(changed && goto_model.can_produce_function(INITIALIZE_FUNCTION))
+    recreate_initialize_function(goto_model, message_handler);
 }

src/linking/CMakeLists.txt

@@ -3,4 +3,4 @@ add_library(linking ${sources})
 
 generic_includes(linking)
 
-target_link_libraries(linking util)
+target_link_libraries(linking goto-programs util)

src/linking/static_lifetime_init.cpp

@@ -16,6 +16,9 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/symbol_table_base.h>
 
+#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_model.h>
+
 #include <set>
 
 static optionalt<codet> static_lifetime_init(
@@ -157,3 +160,21 @@ void static_lifetime_init(
     }
   }
 }
+
+void recreate_initialize_function(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  auto unloaded = goto_model.unload(INITIALIZE_FUNCTION);
+  PRECONDITION(unloaded == 1);
+
+  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/linking/static_lifetime_init.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/cprover_prefix.h>
 
+class goto_modelt;
+class message_handlert;
 class source_locationt;
 class symbol_table_baset;
 
@@ -21,4 +23,9 @@ void static_lifetime_init(
 
 #define INITIALIZE_FUNCTION CPROVER_PREFIX "initialize"
 
+/// Regenerates the CPROVER_INITIALIZE function, which initializes all
+/// non-function symbols of the goto model that have static lifetime. It is an
+/// error if CPROVER_INITIALIZE was not present beforehand.
+void recreate_initialize_function(goto_modelt &, message_handlert &);
+
 #endif // CPROVER_LINKING_STATIC_LIFETIME_INIT_H