CONTRACTS: allow NULL function pointer contracts

Adds a thrid optional NULL parameter to requires_contract
and ensures_contract clauses, allows a pointer to a function
to either satisfy a given contract or to be NULL.

Author: Remi Delmas

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);

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

@@ -877,22 +877,38 @@ void dfcc_wrapper_programt::assert_function_pointer_obeys_contract(
   const irep_idt &property_class,
   goto_programt &dest)
 {
-  function_pointer_contracts.insert(
-    expr.contract_symbol_expr().get_identifier());
   source_locationt loc(expr.source_location());
   loc.set_property_class(property_class);
   std::stringstream comment;
   comment << "Assert function pointer '"
           << from_expr_using_mode(
                ns, contract_symbol.mode, expr.function_pointer())
-          << "' obeys contract '"
-          << from_expr_using_mode(
-               ns, contract_symbol.mode, expr.address_of_contract())
-          << "'";
+          << "' obeys contract ";
+
+  exprt::operandst disjuncts;
+
+  for(std::size_t i = 0; i < expr.contract_pointers().size(); i++)
+  {
+    const exprt &contract_pointer = expr.contract_pointers().at(i);
+    if(contract_pointer.id() == ID_address_of)
+    {
+      function_pointer_contracts.insert(
+        to_symbol_expr(to_address_of_expr(contract_pointer).object())
+          .get_identifier());
+    }
+    if(i > 0)
+      comment << " or ";
+
+    comment << "'"
+            << from_expr_using_mode(ns, contract_symbol.mode, contract_pointer)
+            << "'";
+    disjuncts.push_back(equal_exprt{expr.function_pointer(), contract_pointer});
+  }
   loc.set_comment(comment.str());
-  code_assertt assert_expr(
-    equal_exprt{expr.function_pointer(), expr.address_of_contract()});
+
+  code_assertt assert_expr{or_exprt{disjuncts}};
   assert_expr.add_source_location() = loc;
+
   goto_programt instructions;
   converter.goto_convert(assert_expr, instructions, contract_symbol.mode);
   dest.destructive_append(instructions);
@@ -902,21 +918,60 @@ void dfcc_wrapper_programt::assume_function_pointer_obeys_contract(
   const function_pointer_obeys_contract_exprt &expr,
   goto_programt &dest)
 {
-  function_pointer_contracts.insert(
-    expr.contract_symbol_expr().get_identifier());
+  for(std::size_t i = 0; i < expr.contract_pointers().size(); i++)
+  {
+    const exprt &contract_pointer = expr.contract_pointers().at(i);
 
-  source_locationt loc(expr.source_location());
-  std::stringstream comment;
-  comment << "Assume function pointer '"
-          << from_expr_using_mode(
-               ns, contract_symbol.mode, expr.function_pointer())
-          << "' obeys contract '"
-          << from_expr_using_mode(
-               ns, contract_symbol.mode, expr.contract_symbol_expr())
-          << "'";
-  loc.set_comment(comment.str());
-  dest.add(goto_programt::make_assignment(
-    expr.function_pointer(), expr.address_of_contract(), loc));
+    if(contract_pointer.id() == ID_address_of)
+    {
+      function_pointer_contracts.insert(
+        to_symbol_expr(to_address_of_expr(contract_pointer).object())
+          .get_identifier());
+    }
+
+    const auto &loc = contract_pointer.source_location();
+    if(i == 0)
+    {
+      // First is assignment unconditional
+      // ```
+      // function_pointer := contract_pointer;
+      // ```
+      dest.add(goto_programt::make_assignment(
+        expr.function_pointer(), contract_pointer, loc));
+    }
+    else
+    {
+      // Remaining are nondet
+      // ```
+      // DECL skip: bool
+      // ASSIGN skip = nondet_bool;
+      // IF skip goto skip_label;
+      // function_pointer = contract_pointer;
+      // skip_label:
+      // DEAD skip;
+      // ```
+      const auto skip_var = utils
+                              .create_symbol(
+                                bool_typet(),
+                                wrapped_symbol.name,
+                                "skip",
+                                loc,
+                                wrapper_symbol.mode,
+                                wrapper_symbol.module,
+                                false)
+                              .symbol_expr();
+      dest.add(goto_programt::make_decl(skip_var, loc));
+      dest.add(goto_programt::make_assignment(
+        skip_var, side_effect_expr_nondett(bool_typet(), loc), loc));
+      auto goto_instr =
+        dest.add(goto_programt::make_incomplete_goto(skip_var, loc));
+      dest.add(goto_programt::make_assignment(
+        expr.function_pointer(), contract_pointer, loc));
+      auto skip_target = dest.add(goto_programt::make_skip(loc));
+      goto_instr->complete_goto(skip_target);
+      dest.add(goto_programt::make_dead(skip_var, loc));
+    }
+  }
 }
 
 void dfcc_wrapper_programt::encode_function_call()