CONTRACTS: improved initialisation method for statics

Author: Remi Delmas

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

@@ -30,19 +30,26 @@ Author: Remi Delmas, delmarsd@amazon.com
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/goto_model.h>
+#include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unused_functions.h>
 
+#include <ansi-c/ansi_c_entry_point.h>
 #include <ansi-c/c_expr.h>
+#include <ansi-c/c_object_factory_parameters.h>
 #include <ansi-c/cprover_library.h>
 #include <goto-instrument/contracts/cfg_info.h>
 #include <goto-instrument/contracts/instrument_spec_assigns.h>
 #include <goto-instrument/contracts/utils.h>
 #include <goto-instrument/nondet_static.h>
+#include <langapi/language.h>
+#include <langapi/language_file.h>
+#include <langapi/mode.h>
 #include <linking/static_lifetime_init.h>
 
 void dfcc(
+  const optionst &options,
   goto_modelt &goto_model,
   const irep_idt &harness_id,
   const std::set<irep_idt> &to_check,
@@ -60,7 +67,7 @@ void dfcc(
   for(const auto &function_id : to_replace)
     to_replace_map.insert({function_id, function_id});
 
-  dfcct{goto_model, message_handler}.transform_goto_model(
+  dfcct{options, goto_model, message_handler}.transform_goto_model(
     harness_id,
     to_check_map,
     allow_recursive_calls,
@@ -70,6 +77,7 @@ void dfcc(
 }
 
 void dfcc(
+  const optionst &options,
   goto_modelt &goto_model,
   const irep_idt &harness_id,
   const std::map<irep_idt, irep_idt> &to_check,
@@ -79,7 +87,7 @@ void dfcc(
   const std::set<std::string> &to_exclude_from_nondet_static,
   message_handlert &message_handler)
 {
-  dfcct{goto_model, message_handler}.transform_goto_model(
+  dfcct{options, goto_model, message_handler}.transform_goto_model(
     harness_id,
     to_check,
     allow_recursive_calls,
@@ -90,8 +98,12 @@ void dfcc(
 
 std::map<irep_idt, irep_idt> dfcct::wrapped_functions_cache;
 
-dfcct::dfcct(goto_modelt &goto_model, message_handlert &message_handler)
-  : goto_model(goto_model),
+dfcct::dfcct(
+  const optionst &options,
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+  : options(options),
+    goto_model(goto_model),
     message_handler(message_handler),
     log(message_handler),
     utils(goto_model, message_handler),
@@ -126,26 +138,6 @@ void dfcct::check_transform_goto_model_preconditions(
   const bool apply_loop_contracts,
   const std::set<std::string> &to_exclude_from_nondet_static)
 {
-  // TODO reactivate this once I understand how entry points work
-  // Check that the goto_model entry point matches the given harness_id
-  // if(!config.main.has_value())
-  // {
-  //   log.error() << "dfcct::transform_goto_model: no entry point found in the"
-  //                  "goto model, expected '"
-  //               << harness_id << "', aborting contracts transformations."
-  //               << messaget::eom;
-  //   throw invalid_input_exceptiont(msg);
-  // }
-
-  // if(config.main.value() != harness_id)
-  // {
-  //   log.error() << "dfcct::transform_goto_model: entry point '"
-  //               << config.main.value()
-  //               << "' differs from given harness function '" << harness_id
-  //               << "', aborting contracts transformations." << messaget::eom;
-  //   throw invalid_input_exceptiont(msg);
-  // }
-
   // check there is at most one function to check
   PRECONDITION_WITH_DIAGNOSTICS(
     to_check.size() <= 1,
@@ -266,14 +258,6 @@ void dfcct::transform_goto_model(
   link_to_library(
     goto_model, log.get_message_handler(), cprover_c_library_factory);
 
-  // Make all statics nondet. This needs to be done before starting the program
-  // transformation since the instrumentation adds static variables
-  // which must keep their initial values to function as intended.
-  log.status()
-    << "Adding nondeterministic initialization of static/global variables."
-    << messaget::eom;
-  nondet_static(goto_model, to_exclude_from_nondet_static);
-
   // partition the set of functions of the goto_model
   std::set<irep_idt> pure_contract_symbols;
   std::set<irep_idt> other_symbols;
@@ -439,8 +423,74 @@ void dfcct::transform_goto_model(
   instrument.get_instrumented_functions(instrumented_functions);
   swap_and_wrap.get_swapped_functions(instrumented_functions);
 
-  // update statics and static function maps
-  log.status() << "Updating CPROVER init function" << messaget::eom;
-  library.create_initialize_function(instrumented_functions);
+  // Re-initialise the GOTO model.
+  //
+  // The new entry point must be the proof harness function specified for
+  // instrumentation.
+  //
+  // The "initialize" (aka INITIALIZE_FUNCTION) is the function that assigns
+  // initial values to all statics of the model;
+  //
+  // The initialize function must do the following:
+  // - assign a nondet value to all statics of the user program
+  // - assign the specified initial value to all instrumentation statics
+  // - add an entry in the static unbounded map of instrumented functions
+  // for each instrumented function
+  //
+  // A call to `nondet_static` will re-generate the initialize function with
+  // nondet values. The intrumentation statics will not get nondet initialised
+  // by virtue of being tagged with ID_C_no_nondet_initialization.
+  //
+  // However, nondet_static expects instructions to be either function calls
+  // or assignments with a symbol_exprt LHS.
+  // Since entries for the instrumented function maps are not symbol_exprts but
+  // index_exprts they need to be moved to the harness function.
+  //
+  // The "start" function (aka goto_functionst::entry_point()) is the
+  // function from which SymEx starts.
+  //
+  // The start function must do the following:
+  // - call the initialize function,
+  // - generate nondet values for the arguments of the proof harness function
+  // - call the harness function with said nondet arguments
+  //
+  // All of which can be done using a call to `generate_ansi_c_start_function`,
+  // assuming the initialize function is already available in the symbol table.
+  //
+  // So we do the following:
+  // - regenerate the "initialize" function
+  // - call nondet_static
+  // - add extra instructions at the end of the harness function for the
+  // instrumented functions map
+  // - call generate_ansi_c_start_function
+
+  // Make all user-defined statics nondet.
+  // Other statics added by the instrumentation will be unaffected because they
+  // are tagged with ID_C_no_nondet_initialization when created
+
+  // Update statics and static function maps
+  log.status() << "Updating init function" << messaget::eom;
+  utils.create_initialize_function();
+  goto_model.goto_functions.update();
+  nondet_static(goto_model, to_exclude_from_nondet_static);
+
+  // Initialize the map of instrumented functions by adding extra instructions
+  // to the harness function
+  auto &init_function = goto_model.goto_functions.function_map[harness_id];
+  auto &body = init_function.body;
+  auto begin = body.instructions.begin();
+  goto_programt payload;
+  library.add_instrumented_functions_map_init_instructions(
+    instrumented_functions, begin->source_location(), payload);
+  body.destructive_insert(begin, payload);
+
+  // Define harness as the entry point, overriding any preexisting one.
+  log.status() << "Setting entry point to " << harness_id << messaget::eom;
+  generate_ansi_c_start_function(
+    utils.get_function_symbol(harness_id),
+    goto_model.symbol_table,
+    message_handler,
+    c_object_factory_parameterst(options));
+
   goto_model.goto_functions.update();
 }

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

@@ -52,6 +52,7 @@ class message_handlert;
 class symbolt;
 class conditional_target_group_exprt;
 class cfg_infot;
+class optionst;
 
 #define FLAG_DFCC "dfcc"
 #define OPT_DFCC "(" FLAG_DFCC "):"
@@ -78,6 +79,8 @@ class cfg_infot;
 /// \pre This function requires that the contract associated to function `foo`
 /// exists in the symbol table as symbol `contract::foo`.
 ///
+/// \param options CLI options (used to lookup options for language config when
+/// re-defining the model's entry point)
 /// \param goto_model GOTO model to transform
 /// \param harness_id proof harness name, must be the entry point of the model
 /// \param to_check set of functions to check against their contract
@@ -89,6 +92,7 @@ class cfg_infot;
 /// static program symbols.
 /// \param message_handler used for debug/warning/error messages
 void dfcc(
+  const optionst &options,
   goto_modelt &goto_model,
   const irep_idt &harness_id,
   const std::set<irep_idt> &to_check,
@@ -106,6 +110,8 @@ void dfcc(
 /// When checking function `foo` against contract `bar`, we require the
 /// actual contract symbol to exist as `contract::bar` in the symbol table.
 ///
+/// \param options CLI options (used to lookup options for language config when
+/// re-defining the model's entry point)
 /// \param goto_model GOTO model to transform
 /// \param harness_id Proof harness name, must be the entry point of the model
 /// \param to_check functions-to-contract mapping for contract checking
@@ -117,6 +123,7 @@ void dfcc(
 /// static program symbols.
 /// \param message_handler used for debug/warning/error messages
 void dfcc(
+  const optionst &options,
   goto_modelt &goto_model,
   const irep_idt &harness_id,
   const std::map<irep_idt, irep_idt> &to_check,
@@ -132,9 +139,14 @@ class dfcct
 {
 public:
   /// Class constructor
+  /// \param options CLI options (used to lookup options for language config
+  /// when re-defining the model's entry point)
   /// \param goto_model GOTO model to transform
   /// \param message_handler used for debug/warning/error messages
-  dfcct(goto_modelt &goto_model, message_handlert &message_handler);
+  dfcct(
+    const optionst &options,
+    goto_modelt &goto_model,
+    message_handlert &message_handler);
 
   /// Applies function contracts and loop contracts transformation to GOTO model
   /// using the dynamic frame condition checking approach.
@@ -178,6 +190,7 @@ class dfcct
     const std::set<std::string> &to_exclude_from_nondet_static);
 
 protected:
+  const optionst &options;
   goto_modelt &goto_model;
   message_handlert &message_handler;
   messaget log;

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

@@ -833,9 +833,6 @@ void dfcc_instrumentt::instrument_assign(
   }
 }
 
-#if 0
-// TODO re-enable once we can have nondet-static with with arbitrary LHS
-// expressions in the INITIALIZE_FUNCTION function
 void dfcc_instrumentt::instrument_fptr_call_instruction_dynamic_lookup(
   const exprt &write_set,
   goto_programt::targett &target,
@@ -864,7 +861,7 @@ void dfcc_instrumentt::instrument_fptr_call_instruction_dynamic_lookup(
                                    : address_of_exprt(callf));
   auto index_expr = index_exprt(
     library.get_instrumented_functions_map_symbol().symbol_expr(), object_id);
-  auto cond = notequal_exprt(index_expr, from_integer(1, c_bool_typet(8)));
+  auto cond = notequal_exprt(index_expr, from_integer(1, unsigned_char_type()));
   goto_programt payload;
   auto goto_no_inst =
     payload.add(goto_programt::make_incomplete_goto(cond, target_location));
@@ -885,7 +882,7 @@ void dfcc_instrumentt::instrument_fptr_call_instruction_dynamic_lookup(
   target->turn_into_skip();
   insert_before_swap_and_advance(goto_program, target, payload);
 }
-#endif
+
 void dfcc_instrumentt::instrument_call_instruction(
   const exprt &write_set,
   goto_programt::targett &target,
@@ -907,11 +904,11 @@ void dfcc_instrumentt::instrument_call_instruction(
     }
     else
     {
-      // this is a function pointer call.
-      // pass write set argument
-      target->call_arguments().push_back(write_set);
-      // TODO use instrument_fptr_call_instruction_dynamic_lookup once symex
-      // is able to dispatch function pointers internally
+      // This is a function pointer call. We insert a dynamic lookup into the
+      // map of instrumented functions to determine if the target function is
+      // able to accept a write set parameter.
+      instrument_fptr_call_instruction_dynamic_lookup(
+        write_set, target, goto_program);
     }
   }
 }

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

@@ -308,18 +308,18 @@ class dfcc_instrumentt
     goto_programt::targett &target,
     goto_programt &goto_program);
 
-  // TODO re-enable once we can have nondet-static with with arbitrary LHS
-  // expressions in the INITIALIZE_FUNCTION function
-#if 0
-  /// do pass the extra write set parameter only to function pointers that point
-  /// to instrumented functions that can effectively accept it.
+  /// Before calling a function pointer, performs a dynamic lookup into
+  /// the map of instrumented function provided by
+  /// \ref dfcc_libraryt.get_instrumented_functions_map_symbol,
+  /// and passes the write_set parameter to the funciton pointer only if
+  /// it points to a function known to be instrumented and hence able to accept
+  /// this parameter.
   /// \pre \p target points to a `CALL` instruction where the function
   /// expression is not a \ref symbol_exprt.
   void instrument_fptr_call_instruction_dynamic_lookup(
     const exprt &write_set,
     goto_programt::targett &target,
     goto_programt &goto_program);
-#endif
 
   /// Inserts deallocation checks and a write set update before a call
   /// to the __CPROVER_deallocate function.