using the same wrapping approach for enforcement and replacement

Author: Remi Delmas

src/goto-instrument/contracts/dfcc.cpp

@@ -47,6 +47,7 @@ Author: Remi Delmas, delmarsd@amazon.com
 
 #include <ansi-c/c_expr.h>
 #include <ansi-c/cprover_library.h>
+#include <linking/static_lifetime_init.h>
 // #include <goto-instrument/loop_utils.h>
 
 #include "instrument_spec_assigns.h"
@@ -472,11 +473,11 @@ void dfcct::transform_goto_model(
 
   // swap and wrap contract-checked functions
   for(const auto &entry : check_contracts)
-    wrap_with_contract_check(entry.first, entry.second);
+    check_contract(entry.first, entry.second);
 
   // swap and wrap contract-replaced functions
   for(const auto &entry : replace_contracts)
-    wrap_with_contract_abstraction(entry.first, entry.second);
+    replace_with_contract(entry.first, entry.second);
 }
 
 void dfcct::transform_harness_function(const irep_idt &function_id)
@@ -1934,6 +1935,42 @@ void dfcct::instrument_other(
   }
 }
 
+symbol_exprt dfcct::add_recursion_tracking_variable(const irep_idt &function_id)
+{
+  const auto &function_symbol = get_function_symbol(function_id);
+  const irep_idt identifier = id2string(function_id) + "::on_stack";
+  symbolt new_symbol;
+  new_symbol.name = identifier;
+  new_symbol.base_name = identifier;
+  new_symbol.pretty_name = identifier;
+  new_symbol.type = bool_typet();
+  new_symbol.is_static_lifetime = true;
+  new_symbol.value = false_exprt();
+  new_symbol.mode = function_symbol.mode;
+  new_symbol.module = function_symbol.module;
+  new_symbol.location = function_symbol.location;
+  new_symbol.is_thread_local = true;
+  new_symbol.is_lvalue = true;
+
+  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();
+  }
+
+  return new_symbol.symbol_expr();
+}
+
 void dfcct::wrap_function(
   const irep_idt &function_id,
   const irep_idt &wrapped_function_id)
@@ -2030,33 +2067,81 @@ void dfcct::wrap_function(
   wrapper_fun.body.add(goto_programt::make_end_function(sl));
 }
 
-void dfcct::wrap_with_contract_check(
+void dfcct::check_contract(
   const irep_idt &function_id,
   const irep_idt &contract_id)
 {
-  
+  /* Generates this code 
+  ```
+  IF on_stack GOTO replace;
+  on_stack = true;
+  <check_contracting_instructions>;
+  on_stack = false;
+  GOTO end;
+
+  replace:
+  <add_contract_replacement_instructions>;
+
+  end: 
+  END_FUNCTION;
+  ```
+ */
+  irep_idt wrapped_id =
+    id2string(function_id) + "_wrapped_for_contract_checking";
+  wrap_function(function_id, wrapped_id);
+
+  goto_programt body;
+
+  auto on_stack = add_recursion_tracking_variable(wrapped_id);
+
+  auto recursion_check_goto =
+    body.add(goto_programt::make_incomplete_goto(on_stack));
+  body.add(goto_programt::make_assignment(on_stack, true_exprt()));
+  add_contract_checking_instructions(
+    wrapped_id, function_id, contract_id, body);
+  body.add(goto_programt::make_assignment(on_stack, false_exprt()));
+
+  auto goto_end_function = body.add(goto_programt::make_incomplete_goto());
+
+  auto contract_replacement_label = body.add(goto_programt::make_skip());
+
+  recursion_check_goto->complete_goto(contract_replacement_label);
+
+  add_contract_replacement_instructions(function_id, contract_id, body);
+
+  auto end_function_label = body.add(goto_programt::make_end_function());
+  goto_end_function->complete_goto(end_function_label);
+  goto_model.goto_functions.function_map.at(function_id).body.swap(body);
 }
 
-void dfcct::wrap_with_contract_abstraction(
+void dfcct::replace_with_contract(
   const irep_idt &function_id,
   const irep_idt &contract_id)
 {
-  
+  irep_idt wrapped_id =
+    id2string(function_id) + "_wrapped_for_contract_replacement";
+  wrap_function(function_id, wrapped_id);
+  goto_programt body;
+  add_contract_replacement_instructions(function_id, contract_id, body);
+  body.add(goto_programt::make_end_function());
+  goto_model.goto_functions.function_map.at(function_id).body.swap(body);
 }
 
-void dfcct::generate_contract_abstraction_body(
-  const irep_idt &wrapped_id,
+void dfcct::add_contract_replacement_instructions(
   const irep_idt &wrapper_id,
-  const irep_idt &contract_id)
+  const irep_idt &contract_id,
+  goto_programt &dest)
 {
+  //HERE
 }
 
-//  HERE
-void dfcct::generate_contract_check_body(
+void dfcct::add_contract_checking_instructions(
   const irep_idt &wrapped_id,
   const irep_idt &wrapper_id,
-  const irep_idt &contract_id)
+  const irep_idt &contract_id,
+  goto_programt &dest)
 {
+  //HERE
 }
 // {
   // TODO 

src/goto-instrument/contracts/dfcc.h

@@ -219,7 +219,8 @@ class dfcct
   /// Adds the given symbol as parameter to the given code_typet.
   void add_parameter(const symbolt &symbol, code_typet &code_type);
 
-  /// Adds a parameter to the given function
+  /// Adds a parameter with given `base_name` and `type` to the given 
+  /// `function_id`. Both the symbol and the goto_function are updated.
   const symbolt &add_parameter(
     const irep_idt &function_id,
     const std::string &base_name,
@@ -245,66 +246,15 @@ class dfcct
     goto_programt &decl_init,
     goto_programt &dead);
 
-  /// Wraps the given function_id
-  /// in a wrapper that checks the given contract_id against the function.
-  void wrap_with_contract_check(
-    const irep_idt &function_id,
-    const irep_idt &contract_id);
-
-  /// Genrates the body of the wrapper function as follows:
-  ///
-  /// ```
-  /// static _Bool replace_wrapper_by_contract = 0;
-  ///
-  /// ret_t wrapper(params) {
-  ///   if(replace_wrapper_by_contract) {
-  ///     // replace call with contract
-  ///     return contract::replace(params);
-  ///   } else {
-  ///     // check contract against wrapped function
-  ///     replace_wrapper_by_contract = 1;
-  ///     ret_t ret;
-  ///     // declare history params ...
-  ///     assume(requires);
-  ///     ret = wrapped(params);
-  ///     assert(ensures);
-  ///     replace_wrapper_by_contract = 0;
-  ///     return ret;
-  ///   }
-  /// }
-  /// ```
-  /// \param wrapped_id name of the function that is to be wrapped
-  /// \param contract_id name of the symbol carrying the contract clauses
-  /// \param wrapper_id name to use for the wrapper function
-  void generate_contract_check_body(
-    const irep_idt &wrapped_id,
-    const irep_idt &wrapper_id,
-    const irep_idt &contract_id);
-
-  /// Generates the body of the wrapper function as follows:
-  /// ```
-  /// ret_t wrapper(params) {
-  ///     return contract::replace(params);
-  /// }
-  void wrap_with_contract_abstraction(
-    const irep_idt &function_id,
-    const irep_idt &contract_id);
-
-  void generate_contract_abstraction_body(
-    const irep_idt &wrapped_id,
-    const irep_idt &wrapper_id,
-    const irep_idt &contract_id);
-
-
   /// Given a function to wrap `foo` and a new name `wrapped_foo`
   ///
   /// ```
   /// ret_t foo(x_t foo::x, y_t foo::y) { foo_body; }
   /// ```
   ///
-  /// This creates a new entry in the symbol_table for
-  /// `wrapped_foo` and moves the goto_function `foo_body` under
-  /// `wrapped_foo` in `function_map`.
+  /// This method creates a new entry in the symbol_table for
+  /// `wrapped_foo` and moves the body of the original function, `foo_body`,
+  /// under `wrapped_foo` in `function_map`.
   ///
   /// The parameter symbols of `wrapped_foo` remain the same as in `foo`:
   /// ```
@@ -329,10 +279,101 @@ class dfcct
     const irep_idt &wrapped_function_id);
 
 
+  /// Wraps the given function_id
+  /// in a wrapper that checks the given contract_id against the function.
+  ///
+  /// ```
+  /// static bool on_stack = false;
+  /// 
+  /// ret_t foo(params) {
+  /// IF on_stack GOTO replacement_label;
+  /// <contract checking instructions>
+  /// replacement_label;
+  /// <contract replacement instructions>
+  /// }
+  /// ```
+  void check_contract(
+    const irep_idt &function_id,
+    const irep_idt &contract_id);
+
+  /// Wraps the given function_id
+  /// in a wrapper that models contract replacement.
+  void replace_with_contract(
+    const irep_idt &function_id,
+    const irep_idt &contract_id);
+
+
+  /// Adds instruction modeling contract checking, assuming 
+  /// `ret_t wrapper_id(params, __dfcc_set)` receives the instructions.
+  ///
+  /// \param wrapped_id name of the function that is to be wrapped
+  /// \param contract_id name of the symbol carrying the contract clauses
+  /// \param wrapper_id name to use for the wrapper function
+  /// \param dest goto program where instructions are appended
+  ///
+  /// The generated instructions:
+  /// ```
+  /// DECL __dfcc_set_local: assignable_set_t;
+  /// CALL assignable_set_create(
+  ///      &__dfcc_set_local, size_hint(contract_id), append_mode = false);
+  /// CALL contract_id::assigns(params, &_dfcc_set_local);
+  /// CALL contract_id::frees(params, &_dfcc_set_local);
+  /// DECL __is_fresh_set: assignable_obj_set_t;
+  /// CALL obj_set_create(&__is_fresh_set);
+  /// ASSUME contract::pre(params);
+  /// DECL hist = ...;
+  /// CALL ret = wrapped_id(params, &__dfcc_set_local);
+  /// ASSERT contract::post(params, hist, ret);
+  /// SET_RETURN_VALUE ret;
+  /// ```
+  ///
+  void add_contract_checking_instructions(
+    const irep_idt &wrapped_id,
+    const irep_idt &wrapper_id,
+    const irep_idt &contract_id,
+    goto_programt& dest);
+
+
+  /// Adds instruction modeling contract replacement, assuming 
+  /// `ret_t wrapper(params, __dfcc_set)` receives the instructions.
+  ///
+  /// \param contract_id name of the symbol carrying the contract clauses
+  /// \param wrapper_id name to use for the wrapper function
+  /// \param dest goto program where instructions are appended
+  ///
+  /// The generated instructions:
+  /// ```
+  /// DECL __dfcc_set_local: assignable_set_t ;
+  /// CALL assignable_set_create(
+  ///     &__dfcc_set_local, size_hint(contract_id), append_mode = true);
+  /// CALL contract::assigns(params, &_dfcc_set_local);
+  /// CALL contract::frees(params, &_dfcc_set_local);
+  /// ASSERT check_assigns_clause_inclusion(__dfcc_set, &__dfcc_set_local);
+  /// ASSERT check_frees_clause_inclusion(__dfcc_set, &__dfcc_set_local);
+  /// DECL __is_fresh_set: assignable_obj_set_t;
+  /// CALL obj_set_create(&__is_fresh_set);
+  /// ASSERT contract::pre(params);
+  /// DECL hist = ...; // snapshot history variables
+  /// CALL contract::havoc(__dfcc_set_local);
+  /// CALL ret = nondet();
+  /// ASSUME contract::post(params, hist, ret);
+  /// SET_RETURN_VALUE ret;
+  /// ```
+  void add_contract_replacement_instructions(
+    const irep_idt &wrapper_id,
+    const irep_idt &contract_id,
+    goto_programt& dest);
+
+  /// Adds a global static `function_id::on_stack` for tracking
+  /// recursive calls to `function_id`.
+  symbol_exprt add_recursion_tracking_variable(const irep_idt &function_id);
+
   /// Creates a new symbol in the `symbol_table` by cloning
-  /// the given `function_id` function.
+  /// the given `function_id` function and transforming the
+  /// function's name, parameter names, return type and source location
+  /// using the given functions.
   ///
-  /// Also creates a new `goto_function` under the new name in
+  /// Also creates a new `goto_function` under the transformed name in
   /// the `function_map` with new parameters and an empty body.
   /// Returns the new symbol.
   ///