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
@@ -449,32 +449,6 @@ const symbolt &dfcct::add_dfcc_local(
   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 << ")"

src/goto-instrument/contracts/dfcc_library.cpp

@@ -13,6 +13,7 @@ Author: Remi Delmas, delmarsd@amazon.com
 #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

src/goto-instrument/contracts/dfcc_utils.cpp

@@ -20,11 +20,14 @@ Author: Remi Delmas, delmarsd@amazon.com
 #include <util/std_types.h>
 
 #include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_inline.h>
 #include <goto-programs/goto_model.h>
 
 #include <ansi-c/c_expr.h>
 #include <linking/static_lifetime_init.h>
 
+#include "utils.h"
+
 dfcc_utilst::dfcc_utilst(goto_modelt &goto_model, messaget &log)
   : goto_model(goto_model), log(log), message_handler(log.get_message_handler())
 {
@@ -48,7 +51,7 @@ const symbolt &dfcc_utilst::create_symbol(
   const irep_idt &module,
   bool is_parameter)
 {
-  log.debug() << "dfcc_utilst: create_symbol(" << prefix << "::" << base_name
+  log.debug() << "dfcc_utilst::create_symbol(" << prefix << "::" << base_name
               << ")" << messaget::eom;
 
   symbolt &symbol = get_fresh_aux_symbol(
@@ -70,7 +73,7 @@ const symbolt &dfcc_utilst::create_static_symbol(
   const irep_idt &module,
   const exprt &initial_value)
 {
-  log.debug() << "dfcc_utilst: create_static_symbol(" << prefix
+  log.debug() << "dfcc_utilst::create_static_symbol(" << prefix
               << "::" << base_name << ")" << messaget::eom;
 
   symbolt &symbol = get_fresh_aux_symbol(
@@ -115,7 +118,7 @@ const symbolt &dfcc_utilst::add_parameter(
   const std::string &base_name,
   const typet &type)
 {
-  log.debug() << "dfcc_utilst: add_parameter(" << function_id << ", "
+  log.debug() << "dfcc_utilst::add_parameter(" << function_id << ", "
               << base_name << ")" << messaget::eom;
 
   symbolt &function_symbol = get_function_symbol(function_id);
@@ -144,14 +147,14 @@ const symbolt &dfcc_utilst::clone_and_rename_function(
   std::function<const typet(const typet &)> &trans_ret_type,
   std::function<const source_locationt(const source_locationt &)> &trans_loc)
 {
-  log.debug() << "dfcc_utilst: clone_and_rename_function(" << function_id << ")"
+  log.debug() << "dfcc_utilst::clone_and_rename_function(" << function_id << ")"
               << messaget::eom;
   const symbolt &old_function_symbol = get_function_symbol(function_id);
   code_typet old_code_type = to_code_type(old_function_symbol.type);
 
   irep_idt new_function_id = trans_fun(function_id);
 
-  log.debug() << "dfcc_utilst: clone_and_rename_function: function "
+  log.debug() << "dfcc_utilst::clone_and_rename_function: function "
               << function_id << "->" << new_function_id << messaget::eom;
 
   code_typet::parameterst new_params;
@@ -180,7 +183,7 @@ const symbolt &dfcc_utilst::clone_and_rename_function(
 
   if(!goto_model.symbol_table.add(new_function_symbol))
   {
-    log.error() << "dfcc_utilst: clone_and_rename_function: renamed function "
+    log.error() << "dfcc_utilst::clone_and_rename_function: renamed function "
                 << function_id << " -> " << new_function_id << " already exists"
                 << messaget::eom;
     exit(0);
@@ -225,7 +228,7 @@ void dfcc_utilst::clone_parameters(
     new_params.push_back(new_param);
 
     // build symbol
-    log.debug() << "dfcc_utilst: clone_parameters: param " << old_base_name
+    log.debug() << "dfcc_utilst::clone_parameters: param " << old_base_name
                 << "->" << new_param_id << messaget::eom;
     parameter_symbolt new_param_symbol;
     new_param_symbol.base_name = new_base_name;
@@ -237,7 +240,7 @@ void dfcc_utilst::clone_parameters(
     new_param_symbol.location = location;
     if(!goto_model.symbol_table.add(new_param_symbol))
     {
-      log.error() << "dfcc_utilst: clone_parameters: renamed parameter "
+      log.error() << "dfcc_utilst::clone_parameters: renamed parameter "
                   << old_param.get_identifier() << " -> "
                   << new_param.get_identifier() << " already exists"
                   << messaget::eom;
@@ -248,12 +251,11 @@ void dfcc_utilst::clone_parameters(
 
 const symbolt &dfcc_utilst::clone_and_rename_function(
   const irep_idt &function_id,
-  const std::string &suffix,
+  const irep_idt &new_function_id,
   optionalt<typet> new_return_type = {})
 {
   std::function<const irep_idt(const irep_idt &)> trans_fun =
-    [&](const irep_idt &old_name)
-  { return id2string(old_name) + "::" + suffix; };
+    [&](const irep_idt &old_name) { return new_function_id; };
 
   std::function<const irep_idt(const irep_idt &)> trans_param =
     [&](const irep_idt &old_name) { return old_name; };
@@ -279,7 +281,7 @@ void dfcc_utilst::wrap_function(
   auto old_function = goto_functions.function_map.find(function_id);
   INVARIANT(
     old_function != goto_functions.function_map.end(),
-    "dfcc_utilst: function to wrap " + id2string(function_id) +
+    "dfcc_utilst::wrap_function: function to wrap " + id2string(function_id) +
       " must exist in the program");
 
   // Register the wrapped function under the new name
@@ -290,7 +292,8 @@ void dfcc_utilst::wrap_function(
   INVARIANT(
     goto_functions.function_map.find(wrapped_function_id) !=
       goto_functions.function_map.end(),
-    "dfcc_utilst: wrapped function " + id2string(wrapped_function_id) +
+    "dfcc_utilst::wrap_function: wrapped function " +
+      id2string(wrapped_function_id) +
       " shall exist in function_map at this point");
 
   // Remove previous entry
@@ -300,7 +303,8 @@ void dfcc_utilst::wrap_function(
   INVARIANT(
     goto_functions.function_map.find(function_id) ==
       goto_functions.function_map.end(),
-    "dfcc_utilst: the original function " + id2string(function_id) +
+    "dfcc_utilst::wrap_function: the original function " +
+      id2string(function_id) +
       " shall not exist in function_map anymore at this point");
 
   // Add new symbol for the wrapped function in the symbol table
@@ -316,8 +320,8 @@ void dfcc_utilst::wrap_function(
   const auto wrapped_found = symbol_table.insert(std::move(wrapped_sym));
   INVARIANT(
     wrapped_found.second,
-    "dfcc_utilst: wrapped function symbol " + id2string(wrapped_function_id) +
-      " already exists in the symbol table");
+    "dfcc_utilst::wrap_function: wrapped function symbol " +
+      id2string(wrapped_function_id) + " already exists in the symbol table");
 
   // Re-insert a symbol for `function_id` which is now the wrapper function
   symbolt wrapper_sym;
@@ -347,17 +351,17 @@ void dfcc_utilst::wrap_function(
   // Remove original symbol from the symbol_table
   if(!goto_model.symbol_table.remove(function_id))
   {
-    log.error() << "dfcc_utilst: could not remove " << function_id
-                << " from the symbol table" << messaget::eom;
+    log.error() << "dfcc_utilst::wrap_function: could not remove "
+                << function_id << " from the symbol table" << messaget::eom;
     exit(0);
   }
 
   // Insert update symbol in the symbol_table
   const auto wrapper_sym_found = symbol_table.insert(std::move(wrapper_sym));
   INVARIANT(
     wrapper_sym_found.second,
-    "dfcc_utilst: could not insert symbol " + id2string(function_id) +
-      " in the symbol table");
+    "dfcc_utilst::wrap_function: could not insert symbol " +
+      id2string(function_id) + " in the symbol table");
 
   // Insert wrapper function in the function_map
   goto_functiont &wrapper_fun = goto_functions.function_map[function_id];
@@ -372,14 +376,15 @@ const exprt dfcc_utilst::make_null_check_expr(const exprt &ptr)
 
 exprt dfcc_utilst::make_sizeof_expr(const exprt &expr)
 {
-  log.debug() << "dfcc_utilst : make_sizeof_expr(" << format(expr) << ")"
+  log.debug() << "dfcc_utilst::make_sizeof_expr(" << format(expr) << ")"
               << messaget::eom;
   const auto &size =
     size_of_expr(expr.type(), namespacet(goto_model.symbol_table));
 
   PRECONDITION_WITH_DIAGNOSTICS(
     size.has_value(),
-    "dfcc_utilst: no definite size for lvalue target:\n" + expr.pretty());
+    "dfcc_utilst::make_sizeof_expr: no definite size for lvalue target:\n" +
+      expr.pretty());
 
   return typecast_exprt::conditional_cast(size.value(), size_type());
 }
@@ -389,4 +394,32 @@ exprt dfcc_utilst::make_map_start_address(const exprt &expr)
   return typecast_exprt::conditional_cast(
     address_of_exprt(index_exprt(expr, from_integer(0, c_index_type()))),
     pointer_type(bool_typet()));
-}
+}
+
+void dfcc_utilst::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_utilst::inline_and_check_loop_freeness: 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_utilst::inline_and_check_loop_freeness: function " +
+      id2string(function_id) + " must not contain recursive function calls");
+
+  PRECONDITION_WITH_DIAGNOSTICS(
+    is_loop_free(goto_function.body, ns, log),
+    "dfcc_utilst::inline_and_check_loop_freeness: function " +
+      id2string(function_id) + " must not contain loops");
+
+  // restore internal invariants
+  goto_model.goto_functions.update();
+}