CONTRACTS: adding requires and ensures clauses for function pointers

Syntax extensions and typechecking, and simple contract enforcement
and replacement logic.

Author: Remi Delmas

regression/contracts/function-pointer-contracts-enforce/main.c

@@ -0,0 +1,62 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+bool nondet_bool();
+
+// type of functions that manipulate arrays
+typedef void (*arr_fun_t)(char *arr, size_t size);
+
+// A contract for the arr_fun_t type
+// requires a fresh array and positive size
+// resets the first element to zero
+void contract(char *arr, size_t size)
+  // clang-format off
+__CPROVER_requires((size > 0 && __CPROVER_is_fresh(arr, size)))
+__CPROVER_assigns(arr[0]) 
+__CPROVER_ensures(arr[0] == 0)
+// clang-format on
+{
+}
+
+arr_fun_t bar()
+  // clang-format off
+ __CPROVER_ensures_contract(__CPROVER_return_value, contract)
+// clang-format on
+{
+  return contract;
+}
+
+// Testing pre-conditions constructs
+// Takes a function pointer as input, uses it if its preconditions are met
+int foo(char *arr, size_t size, arr_fun_t fun)
+  // clang-format off
+__CPROVER_requires_contract(fun, contract)
+__CPROVER_requires(arr == NULL || __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(arr && size > 0: arr[0])
+__CPROVER_ensures(arr && size > 0 ==> (arr[0] == 0 && __CPROVER_return_value == 0))
+__CPROVER_ensures(!(arr && size > 0) ==> __CPROVER_return_value == -1)
+// clang-format on
+{
+  if(nondet_bool())
+    fun = bar(); // non-deterministically get a function pointer from bar()
+
+  int retval = -1;
+  if(arr && size > 0)
+  {
+    // calls the function pointer to do update the array
+    fun(arr, size);
+    retval = 0;
+  }
+  return retval;
+}
+
+void main()
+{
+  size_t size;
+  char *arr;
+  arr_fun_t fun;
+  // The precondition that `fun` obeys `contract`
+  // and that bar returns a function that obeys `contract`
+  // are used establish the post-conditions of `foo`
+  foo(arr, size, fun);
+}

regression/contracts/function-pointer-contracts-enforce/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-contract foo --restrict-function-pointer foo.function_pointer_call.1/contract --replace-call-with-contract contract --replace-call-with-contract bar
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that we can require that a function pointer satisfies some named
+contract when verifying another function, and successfully replace a call to this 
+function pointer by the contract.

regression/contracts/function-pointer-contracts-replace/main.c

@@ -0,0 +1,39 @@
+#include <assert.h>
+#include <stdlib.h>
+
+// type of functions that manipulate arrays
+typedef void (*arr_fun_t)(char *arr, size_t size);
+
+// A contract for the arr_fun_t type
+void contract(char *arr, size_t size)
+  // clang-format off
+__CPROVER_requires((size > 0 && __CPROVER_is_fresh(arr, size)))
+__CPROVER_assigns(arr[0]) 
+__CPROVER_ensures(arr[0] == 0)
+// clang-format on
+{
+}
+
+arr_fun_t foo(arr_fun_t infun, arr_fun_t *outfun)
+  // clang-format off
+__CPROVER_requires_contract(infun, contract)
+__CPROVER_ensures_contract(*outfun, contract)
+__CPROVER_ensures_contract(__CPROVER_return_value, contract)
+// clang-format on
+{
+  *outfun = contract;
+  return infun;
+}
+
+void main()
+{
+  // establish pre-conditions before replacement
+  arr_fun_t infun = contract;
+
+  arr_fun_t outfun1 = NULL;
+  arr_fun_t outfun2 = foo(infun, &outfun1);
+
+  // checking post-conditions after replacement
+  assert(outfun1 == contract);
+  assert(outfun2 == contract);
+}

regression/contracts/function-pointer-contracts-replace/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--replace-call-with-contract foo
+^\[precondition.\d+] Assert function pointer 'infun' obeys contract 'contract': SUCCESS$
+^\[main.assertion.\d+].* assertion outfun1 == contract: SUCCESS$
+^\[main.assertion.\d+].* assertion outfun2 == contract: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that, when replacing a call by its contract,
+requires_contract clauses are translated to equality checks
+and that ensures_contract are translated to assignments.

src/ansi-c/ansi_c_convert_type.cpp

@@ -259,6 +259,12 @@ void ansi_c_convert_typet::read_rec(const typet &type)
       static_cast<const exprt &>(static_cast<const irept &>(type));
     requires.push_back(to_unary_expr(as_expr).op());
   }
+  else if(type.id() == ID_C_spec_requires_contract)
+  {
+    const exprt &as_expr =
+      static_cast<const exprt &>(static_cast<const irept &>(type));
+    requires_contract.push_back(to_unary_expr(as_expr).op());
+  }
   else if(type.id() == ID_C_spec_assigns)
   {
     const exprt &as_expr =
@@ -273,6 +279,12 @@ void ansi_c_convert_typet::read_rec(const typet &type)
       static_cast<const exprt &>(static_cast<const irept &>(type));
     ensures.push_back(to_unary_expr(as_expr).op());
   }
+  else if(type.id() == ID_C_spec_ensures_contract)
+  {
+    const exprt &as_expr =
+      static_cast<const exprt &>(static_cast<const irept &>(type));
+    ensures_contract.push_back(to_unary_expr(as_expr).op());
+  }
   else
     other.push_back(type);
 }
@@ -322,12 +334,20 @@ void ansi_c_convert_typet::write(typet &type)
     if(!requires.empty())
       to_code_with_contract_type(type).requires() = std::move(requires);
 
+    if(!requires_contract.empty())
+      to_code_with_contract_type(type).requires_contract() =
+        std::move(requires_contract);
+
     if(!assigns.empty())
       to_code_with_contract_type(type).assigns() = std::move(assigns);
 
     if(!ensures.empty())
       to_code_with_contract_type(type).ensures() = std::move(ensures);
 
+    if(!ensures_contract.empty())
+      to_code_with_contract_type(type).ensures_contract() =
+        std::move(ensures_contract);
+
     if(constructor || destructor)
     {
       if(constructor && destructor)

src/ansi-c/ansi_c_convert_type.h

@@ -47,7 +47,8 @@ class ansi_c_convert_typet:public messaget
   bool constructor, destructor;
 
   // contracts
-  exprt::operandst assigns, ensures, requires;
+  exprt::operandst assigns, ensures, requires, ensures_contract,
+    requires_contract;
 
   // storage spec
   c_storage_spect c_storage_spec;

src/ansi-c/c_expr.h

@@ -320,4 +320,96 @@ to_conditional_target_group_expr(exprt &expr)
   return ret;
 }
 
+/// \brief A class for expressions representing a
+/// `requires_contract(fptr, contract)` clause
+/// or an `ensures_contract(fptr, contract)` clause
+/// in a function contract.
+class function_pointer_obeys_contract_exprt : public exprt
+{
+public:
+  explicit function_pointer_obeys_contract_exprt(
+    exprt _function_pointer,
+    exprt _contract)
+    : exprt(ID_function_pointer_obeys_contract, empty_typet{})
+  {
+    add_to_operands(std::move(_function_pointer));
+    add_to_operands(std::move(_contract));
+  }
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      vm,
+      expr.operands().size() == 2,
+      "function pointer obeys contract expression must have two operands");
+  }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    check(expr, vm);
+  }
+
+  const exprt &function_pointer() const
+  {
+    return op0();
+  }
+
+  exprt &function_pointer()
+  {
+    return op0();
+  }
+
+  const exprt &contract() const
+  {
+    return op1();
+  }
+
+  exprt &contract()
+  {
+    return op1();
+  }
+};
+
+inline void validate_expr(const function_pointer_obeys_contract_exprt &value)
+{
+  function_pointer_obeys_contract_exprt::check(value);
+}
+
+template <>
+inline bool
+can_cast_expr<function_pointer_obeys_contract_exprt>(const exprt &base)
+{
+  return base.id() == ID_function_pointer_obeys_contract;
+}
+
+/// \brief Cast an exprt to a \ref function_pointer_obeys_contract_exprt
+///
+/// \a expr must be known to be \ref function_pointer_obeys_contract_exprt
+///
+/// \param expr: Source expression
+/// \return Object of type \ref function_pointer_obeys_contract_exprt
+inline const function_pointer_obeys_contract_exprt &
+to_function_pointer_obeys_contract_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_function_pointer_obeys_contract);
+  auto &ret = static_cast<const function_pointer_obeys_contract_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_function_pointer_obeys_contract_expr(const exprt &expr)
+inline function_pointer_obeys_contract_exprt &
+to_function_pointer_obeys_contract_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_function_pointer_obeys_contract);
+  auto &ret = static_cast<function_pointer_obeys_contract_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_ANSI_C_C_EXPR_H

src/ansi-c/c_typecheck_base.cpp

@@ -699,6 +699,15 @@ void c_typecheck_baset::typecheck_declaration(
 
       typecheck_symbol(symbol);
 
+      auto check_history_expr = [&](const exprt expr) {
+        disallow_subexpr_by_id(
+          expr, ID_old, CPROVER_PREFIX "old is not allowed in preconditions.");
+        disallow_subexpr_by_id(
+          expr,
+          ID_loop_entry,
+          CPROVER_PREFIX "loop_entry is not allowed in preconditions.");
+      };
+
       // check the contract, if any
       symbolt &new_symbol = symbol_table.get_writeable_ref(identifier);
       if(new_symbol.type.id() == ID_code)
@@ -708,29 +717,36 @@ void c_typecheck_baset::typecheck_declaration(
         // available
         auto &code_type = to_code_with_contract_type(new_symbol.type);
 
+        for(auto &expr : code_type.requires_contract())
+        {
+          typecheck_spec_function_pointer_obeys_contract(expr);
+          check_history_expr(expr);
+        }
+
         for(auto &requires : code_type.requires())
         {
           typecheck_expr(requires);
           implicit_typecast_bool(requires);
-          disallow_subexpr_by_id(
-            requires,
-            ID_old,
-            CPROVER_PREFIX "old is not allowed in preconditions.");
-          disallow_subexpr_by_id(
-            requires,
-            ID_loop_entry,
-            CPROVER_PREFIX "loop_entry is not allowed in preconditions.");
+          check_history_expr(requires);
         }
 
         typecheck_spec_assigns(code_type.assigns());
 
-        if(!as_const(code_type).ensures().empty())
-        {
-          const auto &return_type = code_type.return_type();
+        const auto &return_type = code_type.return_type();
+        if(return_type.id() != ID_empty)
+          parameter_map[CPROVER_PREFIX "return_value"] = return_type;
 
-          if(return_type.id() != ID_empty)
-            parameter_map[CPROVER_PREFIX "return_value"] = return_type;
+        for(auto &expr : code_type.ensures_contract())
+        {
+          typecheck_spec_function_pointer_obeys_contract(expr);
+          disallow_subexpr_by_id(
+            expr,
+            ID_loop_entry,
+            CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
+        }
 
+        if(!as_const(code_type).ensures().empty())
+        {
           for(auto &ensures : code_type.ensures())
           {
             typecheck_expr(ensures);
@@ -740,10 +756,10 @@ void c_typecheck_baset::typecheck_declaration(
               ID_loop_entry,
               CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
           }
-
-          if(return_type.id() != ID_empty)
-            parameter_map.erase(CPROVER_PREFIX "return_value");
         }
+
+        if(return_type.id() != ID_empty)
+          parameter_map.erase(CPROVER_PREFIX "return_value");
       }
     }
   }

src/ansi-c/c_typecheck_base.h

@@ -146,6 +146,7 @@ class c_typecheck_baset:
   virtual void typecheck_start_thread(codet &code);
 
   // contracts
+  virtual void typecheck_spec_function_pointer_obeys_contract(exprt &expr);
   virtual void typecheck_spec_assigns(exprt::operandst &targets);
   virtual void typecheck_spec_assigns_condition(exprt &condition);
   virtual void typecheck_spec_assigns_target(exprt &target);