contract enforcement alpha

Author: Remi Delmas

src/goto-instrument/contracts/dfcc.cpp

@@ -247,14 +247,14 @@ void dfcct::transform_goto_model(
   // generate assignable_t functions from contracts
   for(const auto &function_id : spec_assigns_from_contract_functions)
   {
-    dsl_contract_handler.dfcc_spec_assigns_function_from_contract(
+    dsl_contract_handler.create_spec_assigns_function_from_contract(
       function_id, spec_assigns_functions);
   }
 
   // inline all assignable_t functions
   for(const auto &function_id : spec_assigns_functions)
   {
-    inline_and_check_loop_freeness(function_id);
+    utils.inline_and_check_loop_freeness(function_id);
   }
 
   // instrument all assignable_t functions
@@ -266,14 +266,14 @@ void dfcct::transform_goto_model(
   // generate frees_t functions from contracts
   for(const auto &function_id : spec_frees_from_contract_functions)
   {
-    dsl_contract_handler.dfcc_spec_frees_function_from_contract(
+    dsl_contract_handler.create_spec_frees_function_from_contract(
       function_id, spec_frees_functions);
   }
 
   // inline all frees_t functions
   for(const auto &function_id : spec_frees_functions)
   {
-    inline_and_check_loop_freeness(function_id);
+    utils.inline_and_check_loop_freeness(function_id);
   }
 
   // instrument all frees_t functions
@@ -327,7 +327,8 @@ void dfcct::transform_harness_function(const irep_idt &function_id)
 {
   /*
     Transforming the harness function just consists in passing a NULL value
-    for the __dfcc_set parameter to each function call or function pointer call.
+    for the assignable_set parameter to each function call or
+    function pointer call.
     This will result in no DFCC set updates or checks being performed in 
     functions called directly from the harness.
   */
@@ -399,7 +400,7 @@ const symbolt &dfcct::add_dfcc_param(const irep_idt &function_id)
   const auto &sym = utils.create_symbol(
     library.dfcc_type[dfcc_typet::SET_PTR],
     id2string(function_id),
-    "__dfcc_set",
+    "__to_check",
     function_symbol.location,
     function_symbol.mode,
     function_symbol.module,
@@ -413,68 +414,6 @@ const symbolt &dfcct::add_dfcc_param(const irep_idt &function_id)
   return sym;
 }
 
-const symbolt &dfcct::add_dfcc_local(
-  const irep_idt &function_id,
-  const int contract_assigns_size_hint,
-  const bool contract_frees_append,
-  goto_programt &decl_init,
-  goto_programt &dead)
-{
-  const auto &function_symbol = utils.get_function_symbol(function_id);
-
-  const auto &sym = utils.create_symbol(
-    library.dfcc_type[dfcc_typet::SET],
-    id2string(function_id),
-    "__dfcc_set_local",
-    function_symbol.location,
-    function_symbol.mode,
-    function_symbol.module,
-    false);
-
-  const auto sym_expr = sym.symbol_expr();
-  decl_init.add(goto_programt::make_decl(sym_expr));
-
-  // initialise
-  auto function_sym_expr =
-    library.dfcc_fun_symbol.at(dfcc_funt::SET_CREATE).symbol_expr();
-  code_function_callt code_function_call(function_sym_expr);
-  auto &arguments = code_function_call.arguments();
-  arguments.emplace_back(address_of_exprt(sym_expr));
-  arguments.emplace_back(from_integer(contract_assigns_size_hint, size_type()));
-  arguments.emplace_back(
-    (contract_frees_append ? (exprt)true_exprt() : (exprt)false_exprt()));
-
-  // kill
-  dead.add(goto_programt::make_dead(sym_expr));
-  return sym;
-}
-
-void dfcct::inline_and_check_loop_freeness(const irep_idt &function_id)
-{
-  auto &goto_function = goto_model.goto_functions.function_map.at(function_id);
-
-  PRECONDITION_WITH_DIAGNOSTICS(
-    goto_function.body_available(),
-    "dfcc: function " + id2string(function_id) + " must have a body");
-
-  inlining_decoratort decorated(log.get_message_handler());
-  namespacet ns{goto_model.symbol_table};
-  goto_function_inline(
-    goto_model.goto_functions, function_id, ns, log.get_message_handler());
-
-  PRECONDITION_WITH_DIAGNOSTICS(
-    decorated.get_recursive_function_warnings_count() == 0,
-    "dfcc: function " + id2string(function_id) +
-      " must not contain recursive function calls");
-
-  PRECONDITION_WITH_DIAGNOSTICS(
-    is_loop_free(goto_function.body, ns, log),
-    "dfcc: function " + id2string(function_id) + " must not contain loops");
-
-  // restore internal invariants
-  goto_model.goto_functions.update();
-}
-
 void dfcct::to_dfcc_spec_assigns_function(const irep_idt &function_id)
 {
   log.debug() << "dfcc: to_dfcc_spec_assigns_function(" << function_id << ")"
@@ -488,7 +427,7 @@ void dfcct::to_dfcc_spec_assigns_function(const irep_idt &function_id)
 
   // add __dfcc_set parameter
   auto &set_symbol = utils.add_parameter(
-    function_id, "__dfcc_set", library.dfcc_type[dfcc_typet::SET_PTR]);
+    function_id, "__to_populate", library.dfcc_type[dfcc_typet::SET_PTR]);
 
   // rewrite calls
   Forall_goto_program_instructions(ins_it, goto_function.body)
@@ -525,8 +464,8 @@ void dfcct::to_dfcc_spec_assigns_function(const irep_idt &function_id)
       {
         INVARIANT(
           false,
-          "to_dfcc_spec_assigns_function: function calls must be inlined "
-          "before calling this function");
+          "dfcct::to_dfcc_spec_assigns_function: function calls must be "
+          "inlined before calling this function");
       }
     }
   }

src/goto-instrument/contracts/dfcc.h

@@ -117,8 +117,16 @@ class dfcct
   /// Aborts on recursion warnings during inlining.
   void inline_and_check_loop_freeness(const irep_idt &function_id);
 
-  /// Transforms a function that returns __CPROVER_assignable_t into a function
-  /// that accepts an extra __CPROVER_assignable_car_set_t parameter
+  /// Transforms a function `__CPROVER_assignable_t foo(params)` into
+  /// ```
+  /// __CPROVER_assignable_t foo(
+  ///   params,
+  ///   __CPROVER_assignable_set_t populate, 
+  ///   __CPROVER_assignable_set_t side_effect_check
+  /// )
+  /// ```
+  /// - `populate` is the set to populate.
+  /// - `side_effect` is the set to use for checking side effects.
   /// The function must have been previously inlined and be loop-free.
   void to_dfcc_spec_assigns_function(const irep_idt &function_id);
 
@@ -140,23 +148,6 @@ class dfcct
   /// Adds the __dfcc_set parameter to the given function.
   const symbolt &add_dfcc_param(const irep_idt &function_id);
 
-  /// \brief Generates a local symbol and initialisation of a assignable set
-  /// in the given function.
-  /// \param function_id name of the function to generate code for
-  /// \param contract_assigns_size_hint size hint to initialise contract_assigns
-  /// \param contract_frees_append if true, activates append mode on the
-  /// which is required when building an assignable set for contract replacement
-  /// and enable SET_CHECK_ASSIGNS_CLAUSE_INCLUSION,
-  /// SET_CHECK_FREES_CLAUSE_INCLUSION, SET_DEALLOCATE_FREEABLE
-  /// \param decl_init program where declaration and initialisation are added
-  /// \param dead program where dead instruction is added
-  const symbolt &add_dfcc_local(
-    const irep_idt &function_id,
-    const int contract_assigns_size_hint,
-    const bool contract_frees_append,
-    goto_programt &decl_init,
-    goto_programt &dead);
-
   /// Wraps the given function_id
   /// in a wrapper that checks the given contract_id against the function.
   ///

src/goto-instrument/contracts/dfcc_library.cpp

@@ -13,6 +13,7 @@ Author: Remi Delmas, [email protected]
 #include <util/message.h>
 
 #include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_function.h>
 #include <goto-programs/goto_model.h>
 
 #include <ansi-c/cprover_library.h>
@@ -89,6 +90,18 @@ const std::map<irep_idt, dfcc_funt> dfcc_libraryt::dfcc_hook = {
   {CPROVER_PREFIX "object_upto", dfcc_funt::SET_INSERT_OBJECT_UPTO},
   {CPROVER_PREFIX "freeable", dfcc_funt::SET_ADD_FREEABLE}};
 
+const std::set<irep_idt> dfcc_libraryt::assignable_builtin_names = {
+  CPROVER_PREFIX "assignable",
+  CPROVER_PREFIX "assignable_set_insert_assignable",
+  CPROVER_PREFIX "whole_object",
+  CPROVER_PREFIX "assignable_set_insert_whole_object",
+  CPROVER_PREFIX "object_from",
+  CPROVER_PREFIX "assignable_set_insert_object_from",
+  CPROVER_PREFIX "object_upto",
+  CPROVER_PREFIX "assignable_set_insert_object_upto",
+  CPROVER_PREFIX "freeable",
+  CPROVER_PREFIX "assignable_set_add_freeable"};
+
 const std::map<dfcc_funt, std::pair<bool, bool>>
   dfcc_libraryt::inline_and_unwind = {
     {dfcc_funt::CAR_CREATE, {false, false}},
@@ -195,3 +208,42 @@ void dfcc_libraryt::load()
     dfcc_type[pair.first] = ns.lookup(pair.second).type;
   }
 }
+
+const int
+dfcc_libraryt::count_calls_to_buitins(const goto_functiont &goto_function)
+{
+  int nof_calls = 0;
+  forall_goto_program_instructions(ins_it, goto_function.body)
+  {
+    if(ins_it->is_function_call())
+    {
+      if(ins_it->call_function().id() != ID_symbol)
+      {
+        log.error().source_location = ins_it->source_location();
+        log.error() << "dfcc: function pointer calls not supported"
+                    << messaget::eom;
+        throw 0;
+      }
+
+      const irep_idt &callee_id =
+        to_symbol_expr(ins_it->call_function()).get_identifier();
+
+      // only process built-in functions that return assignable_t,
+      // error out on any other function call
+      // find the corresponding instrumentation hook
+      auto found = assignable_builtin_names.find(callee_id);
+      if(found != assignable_builtin_names.end())
+      {
+        ++nof_calls;
+      }
+      else
+      {
+        INVARIANT(
+          false,
+          "dfcc_libraryt::count_calls_to_buitins: all function calls must be "
+          "inlined before calling this function");
+      }
+    }
+  }
+  return nof_calls;
+}

src/goto-instrument/contracts/dfcc_library.h

@@ -62,6 +62,7 @@ enum class dfcc_funt
 };
 
 class goto_modelt;
+class goto_functiont;
 class messaget;
 class message_handlert;
 class symbolt;
@@ -97,6 +98,9 @@ class dfcc_libraryt
   /// built-in function name to enum
   static const std::map<irep_idt, dfcc_funt> dfcc_hook;
 
+  /// built-in function names (front-end and instrumentation hooks)
+  static const std::set<irep_idt> assignable_builtin_names;
+
   /// true iff the library function must be inlined and unwound
   static const std::map<dfcc_funt, std::pair<bool, bool>> inline_and_unwind;
 
@@ -111,6 +115,12 @@ class dfcc_libraryt
 
   /// Adds all the `cprover_dfcc.c` library types and functions to the model
   void load();
+
+  /// Given a goto function representing an assigns clause, counts
+  /// and returns the number of function calls to built-in
+  /// __CPROVER_assignable_t functions it contains.
+  /// Any call other than to a built-in makes the function fail
+  const int count_calls_to_buitins(const goto_functiont &goto_function);
 };
 
 #endif