CONTRACTS: Allow NULL function pointer contracts

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

@@ -0,0 +1,52 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+typedef int (*fun_t)(int);
+
+int add_one(int x)
+  __CPROVER_ensures(__CPROVER_return_value == __CPROVER_old(x) + 1);
+
+int foo(fun_t f_in, int x, fun_t *f_out)
+  // clang-format off
+__CPROVER_requires_contract(f_in, add_one, NULL)
+__CPROVER_assigns(f_out)
+__CPROVER_ensures(f_in ==>__CPROVER_return_value == __CPROVER_old(x) + 1)
+__CPROVER_ensures(!f_in ==>__CPROVER_return_value == __CPROVER_old(x))
+__CPROVER_ensures_contract(*f_out, add_one, NULL)
+// clang-format on
+{
+  *f_out = NULL;
+  if(f_in)
+  {
+    *f_out = f_in;
+    // this branch must be reachable
+    __CPROVER_assert(false, "then branch is reachable, expecting FAILURE");
+  CALL_F_IN:
+    return f_in(x);
+  }
+  else
+  {
+    // this branch must be reachable
+    __CPROVER_assert(false, "else branch is reachable, expecting FAILURE");
+    return x;
+  }
+}
+
+int main()
+{
+  fun_t f_in;
+  int x;
+  fun_t f_out;
+  foo(f_in, x, &f_out);
+  if(f_out)
+  {
+    __CPROVER_assert(false, "then branch is reachable, expecting FAILURE");
+  CALL_F_OUT:
+    __CPROVER_assert(f_out(1) == 2, "f_out satisfies add_one");
+  }
+  else
+  {
+    __CPROVER_assert(false, "else branch is reachable, expecting FAILURE");
+  }
+}

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

@@ -0,0 +1,31 @@
+CORE
+main.c
+--restrict-function-pointer foo.CALL_F_IN/add_one --restrict-function-pointer main.CALL_F_OUT/add_one --dfcc main --enforce-contract foo
+main.c function foo
+^\[foo.postcondition.\d+\] line 14 Check ensures clause of contract contract::foo for function foo: SUCCESS$
+^\[foo.postcondition.\d+\] line 15 Check ensures clause of contract contract::foo for function foo: SUCCESS$
+^\[foo.postcondition.\d+\] line 16 Assert function pointer '\*f_out_wrapper' obeys contract 'add_one' or '\(fun_t\)NULL': SUCCESS$
+^\[foo.assigns.\d+\] line 19 Check that \*f_out is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 22 Check that \*f_out is assignable: FAILURE$
+^\[foo.assertion.\d+\] line 24 then branch is reachable, expecting FAILURE: FAILURE$
+^\[foo.pointer_dereference.\d+\] line 26 dereferenced function pointer must be add_one: SUCCESS$
+^\[foo.assertion.\d+\] line 31 else branch is reachable, expecting FAILURE: FAILURE$
+^\[main.assertion.\d+\] line 44 then branch is reachable, expecting FAILURE: FAILURE$
+^\[main.assertion.\d+\] line 46 f_out satisfies add_one: SUCCESS$
+^\[main.pointer_dereference.\d+\] line 46 dereferenced function pointer must be add_one: SUCCESS$
+^\[main.assertion.\d+\] line 50 else branch is reachable, expecting FAILURE: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+foo requires that function pointer f_in satisfies the contract add_one or is NULL.
+When f_in is not NULL, foo calls f_in and the post condition of foo is that
+of add_one `__CPROVER_return_value == old(x) + 1`.
+When f_in is not NULL, foo returns x directly post condition of foo is that
+of add_one `__CPROVER_return_value == old(x)`.
+The function pointer f_out is ensured to satisfy the add_one contract or be NULL
+as a post condition.
+The main program calls f_out on a particular value if it is not null and asserts
+that the add_one post condition holds for a particular value.
+Assertions `assert(false)` are added to all branches to demonstrate reachability.

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

@@ -0,0 +1,57 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+typedef int (*fun_t)(int);
+
+int add_one(int x)
+  __CPROVER_ensures(__CPROVER_return_value == __CPROVER_old(x) + 1);
+
+// returns either a pointer to a function that satisfies add_one or NULL
+fun_t get_add_one()
+  __CPROVER_ensures_contract(__CPROVER_return_value, add_one, NULL);
+
+int foo(int x, fun_t *f_out)
+  // clang-format off
+__CPROVER_assigns(*f_out)
+__CPROVER_ensures(
+  __CPROVER_return_value == __CPROVER_old(x) + 1 ||
+  __CPROVER_return_value == __CPROVER_old(x))
+__CPROVER_ensures_contract(*f_out, add_one, NULL)
+// clang-format on
+{
+  *f_out = NULL;
+  // obtain a pointer to a function that satisfies add_one;
+  fun_t f_in = get_add_one();
+  if(f_in)
+  {
+    *f_out = f_in;
+    // this branch must be reachable
+    __CPROVER_assert(false, "then branch is reachable, expecting FAILURE");
+  CALL_F_IN:
+    return f_in(x);
+  }
+  else
+  {
+    // this branch must be reachable
+    __CPROVER_assert(false, "else branch is reachable, expecting FAILURE");
+    return x;
+  }
+}
+
+int main()
+{
+  int x;
+  fun_t f_out;
+  foo(x, &f_out);
+  if(f_out)
+  {
+    __CPROVER_assert(false, "then branch is reachable, expecting FAILURE");
+  CALL_F_OUT:
+    __CPROVER_assert(f_out(1) == 2, "f_out satisfies add_one");
+  }
+  else
+  {
+    __CPROVER_assert(false, "else branch is reachable, expecting FAILURE");
+  }
+}

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

@@ -0,0 +1,28 @@
+CORE
+main.c
+--restrict-function-pointer foo.CALL_F_IN/add_one --restrict-function-pointer main.CALL_F_OUT/add_one --dfcc main --enforce-contract foo --replace-call-with-contract get_add_one
+^\[foo.postcondition.\d+\] line 18 Check ensures clause of contract contract::foo for function foo: SUCCESS$
+^\[foo.postcondition.\d+\] line 20 Assert function pointer '\*f_out_wrapper' obeys contract 'add_one' or '\(fun_t\)NULL': SUCCESS$
+^\[foo.assertion.\d+\] line 30 then branch is reachable, expecting FAILURE: FAILURE$
+^\[foo.pointer_dereference.\d+\] line 32 dereferenced function pointer must be add_one: SUCCESS$
+^\[foo.assertion.\d+\] line 37 else branch is reachable, expecting FAILURE: FAILURE$
+^\[main.assertion.\d+\] line 49 then branch is reachable, expecting FAILURE: FAILURE$
+^\[main.assertion.\d+\] line 51 f_out satisfies add_one: SUCCESS$
+^\[main.pointer_dereference.\d+\] line 51 dereferenced function pointer must be add_one: SUCCESS$
+^\[main.assertion.\d+\] line 55 else branch is reachable, expecting FAILURE: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+foo obtains function pointer f_in through get_add_one, which is replaced by
+its contract.
+When f_in is not NULL, foo calls f_in and the post condition of foo is that
+of add_one `__CPROVER_return_value == old(x) + 1`.
+When f_in is not NULL, foo returns x directly post condition of foo is that
+of add_one `__CPROVER_return_value == old(x)`.
+The function pointer f_out is ensured to satisfy the add_one contract or be NULL
+as a post condition.
+The main program calls f_out on a particular value if it is not null and asserts
+that the add_one post condition holds for a particular value.
+Assertions `assert(false)` are added to all branches to demonstrate reachability.

src/ansi-c/c_expr.h

@@ -329,11 +329,11 @@ class function_pointer_obeys_contract_exprt : public exprt
 public:
   explicit function_pointer_obeys_contract_exprt(
     exprt _function_pointer,
-    exprt _contract)
+    exprt _contract_pointers)
     : exprt(ID_function_pointer_obeys_contract, empty_typet{})
   {
     add_to_operands(std::move(_function_pointer));
-    add_to_operands(std::move(_contract));
+    add_to_operands(std::move(_contract_pointers));
   }
 
   static void check(
@@ -344,6 +344,13 @@ class function_pointer_obeys_contract_exprt : public exprt
       vm,
       expr.operands().size() == 2,
       "function pointer obeys contract expression must have two operands");
+
+    DATA_CHECK(
+      vm,
+      expr.operands()[1].id() == ID_expression_list,
+      "function pointer obeys contract expression second operand must be an "
+      "ID_expression_list expression, found " +
+        id2string(expr.operands()[1].id()));
   }
 
   static void validate(
@@ -364,24 +371,14 @@ class function_pointer_obeys_contract_exprt : public exprt
     return op0();
   }
 
-  const symbol_exprt &contract_symbol_expr() const
-  {
-    return to_symbol_expr(op1().operands().at(0));
-  }
-
-  symbol_exprt &contract_symbol_expr()
+  const exprt::operandst &contract_pointers() const
   {
-    return to_symbol_expr(op1().operands().at(0));
-  }
-
-  const exprt &address_of_contract() const
-  {
-    return op1();
+    return op1().operands();
   }
 
-  exprt &address_of_contract()
+  exprt::operandst &contract_pointers()
   {
-    return op1();
+    return op1().operands();
   }
 };
 

src/ansi-c/c_typecheck_code.cpp

@@ -9,17 +9,17 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// C Language Type Checking
 
-#include "c_typecheck_base.h"
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_util.h>
 #include <util/range.h>
+#include <util/simplify_expr.h>
 #include <util/string_constant.h>
 
 #include "ansi_c_declaration.h"
 #include "c_expr.h"
+#include "c_typecheck_base.h"
 
 void c_typecheck_baset::start_typecheck_code()
 {
@@ -1101,11 +1101,11 @@ void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract(
 {
   if(!can_cast_expr<function_pointer_obeys_contract_exprt>(expr))
   {
-    error().source_location = expr.source_location();
-    error() << "expected ID_function_pointer_obeys_contract expression in "
-               "requires_contract/ensures_contract clause, found "
-            << expr.id() << eom;
-    throw 0;
+    throw invalid_source_file_exceptiont(
+      "expected ID_function_pointer_obeys_contract expression in "
+      "requires_contract/ensures_contract clause, found " +
+        id2string(expr.id()),
+      expr.source_location());
   }
 
   auto &obeys_expr = to_function_pointer_obeys_contract_expr(expr);
@@ -1121,60 +1121,73 @@ void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract(
     function_pointer.type().id() != ID_pointer ||
     to_pointer_type(function_pointer.type()).base_type().id() != ID_code)
   {
-    error().source_location = expr.source_location();
-    error() << "the first parameter of the clause must be a function pointer "
-               "expression"
-            << eom;
-    throw 0;
+    throw invalid_source_file_exceptiont(
+      "the first parameter of the clause must be a function pointer expression",
+      expr.source_location());
   }
 
   if(!function_pointer.get_bool(ID_C_lvalue))
   {
-    error().source_location = function_pointer.source_location();
-    error() << "first parameter of the clause must be an lvalue" << eom;
-    throw 0;
+    throw invalid_source_file_exceptiont(
+      "the first parameter of the clause must be an lvalue",
+      function_pointer.source_location());
   }
 
   if(has_subexpr(function_pointer, ID_side_effect))
   {
-    error().source_location = function_pointer.source_location();
-    error() << "first parameter of the clause must have no side-effects" << eom;
-    throw 0;
+    throw invalid_source_file_exceptiont(
+      "the first parameter of the clause must have no side-effects",
+      function_pointer.source_location());
   }
 
   if(has_subexpr(function_pointer, ID_if))
   {
-    error().source_location = function_pointer.source_location();
-    error() << "first parameter of the clause must have no ternary operator"
-            << eom;
-    throw 0;
+    throw invalid_source_file_exceptiont(
+      "the first parameter of the clause must have no ternary operator",
+      function_pointer.source_location());
   }
 
-  // second parameter must be the address of a function symbol
-  auto &address_of_contract = obeys_expr.address_of_contract();
-  typecheck_expr(address_of_contract);
+  // second parameter must be a list of size 1 or 2 with:
+  // - a function symbol with compatible type
+  // - a null value
+  auto contract_pointers_size = obeys_expr.contract_pointers().size();
+  if(contract_pointers_size < 1 || contract_pointers_size > 2)
+  {
+    throw invalid_source_file_exceptiont(
+      "requires_contract/ensures_contract clauses must have two or three "
+      "parameters",
+      obeys_expr.source_location());
+  }
 
+  auto &first_target = obeys_expr.contract_pointers().at(0);
+  typecheck_expr(first_target);
   if(
-    address_of_contract.id() != ID_address_of ||
-    to_address_of_expr(address_of_contract).object().id() != ID_symbol ||
-    address_of_contract.type().id() != ID_pointer ||
-    to_pointer_type(address_of_contract.type()).base_type().id() != ID_code)
-  {
-    error().source_location = expr.source_location();
-    error() << "the second parameter of the requires_contract/ensures_contract "
-               "clause must be a function symbol"
-            << eom;
-    throw 0;
+    first_target.id() != ID_address_of ||
+    to_address_of_expr(first_target).object().id() != ID_symbol ||
+    first_target.type().id() != ID_pointer ||
+    to_pointer_type(first_target.type()).base_type().id() != ID_code ||
+    function_pointer.type() != first_target.type())
+  {
+    throw invalid_source_file_exceptiont(
+      "the second parameter of the clause must be a pointer to a contract "
+      "symbol with the same type as the first parameter",
+      first_target.source_location());
   }
 
-  if(function_pointer.type() != address_of_contract.type())
+  if(contract_pointers_size == 2)
   {
-    error().source_location = expr.source_location();
-    error() << "the first and second parameter of the "
-               "requires_contract/ensures_contract clause must have the same "
-               "function pointer type "
-            << eom;
-    throw 0;
+    auto &second_target = obeys_expr.contract_pointers().at(1);
+    typecheck_expr(second_target);
+    auto simplified = simplify_expr(second_target, namespacet(symbol_table));
+    if(
+      !simplified.is_constant() ||
+      !is_null_pointer(to_constant_expr(simplified)))
+      throw invalid_source_file_exceptiont(
+        "the (optional) third parameter of the clause must be NULL",
+        second_target.source_location());
+    // add typecast around NULL
+    obeys_expr.contract_pointers()[1] =
+      typecast_exprt(simplified, function_pointer.type());
   }
 }
 

src/ansi-c/parser.y

@@ -3299,7 +3299,7 @@ cprover_function_contract:
           set($$, ID_C_spec_requires);
           mto($$, $3);
         }
-        | TOK_CPROVER_ENSURES_CONTRACT '(' unary_expression ',' unary_expression ')'
+        | TOK_CPROVER_ENSURES_CONTRACT '(' unary_expression ',' unary_expression_list ')'
         {
           $$=$1;
           set($$, ID_C_spec_ensures_contract);
@@ -3309,7 +3309,7 @@ cprover_function_contract:
           tmp.add_source_location()=parser_stack($$).source_location();
           parser_stack($$).add_to_operands(std::move(tmp));
         }
-        | TOK_CPROVER_REQUIRES_CONTRACT '(' unary_expression ',' unary_expression ')'
+        | TOK_CPROVER_REQUIRES_CONTRACT '(' unary_expression ',' unary_expression_list ')'
         {
           $$=$1;
           set($$, ID_C_spec_requires_contract);