Support for empty assigns clause

CBMC currently doesn't enforce assigns clauses if there isn't one.
However, whenever enforcing a function contract, the absence of an
assigns clause should be interpreted as an empty write set
(i.e., no inputs will be modified by this function).
CBMC now properly checks for empty assigns clause behavior.

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/contracts/assigns_enforce_05/test.desc

@@ -1,9 +1,9 @@
 CORE
 main.c
 --enforce-all-contracts
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
+^VERIFICATION SUCCESSFUL$
 --
 --
 This test checks that verification fails when a function with an assigns clause calls a function without an assigns clause.

regression/contracts/assigns_enforce_15/main.c

@@ -0,0 +1,20 @@
+int foo(int *x) __CPROVER_assigns(*x)
+  __CPROVER_ensures(__CPROVER_return_value == *x + 5)
+{
+  int z = 5;
+  int y = bar(&z);
+  return *x + 5;
+}
+
+int bar(int *a) __CPROVER_ensures(__CPROVER_return_value >= 5)
+{
+  *a = *a + 2;
+  return *a;
+}
+
+int main()
+{
+  int n;
+  n = foo(&n);
+  return 0;
+}

regression/contracts/assigns_enforce_15/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

regression/contracts/function_check_02/main.c

@@ -5,9 +5,15 @@
 // in ensures to fail.
 
 int initialize(int *arr)
+  /* clang-format off */
+  __CPROVER_assigns(*arr)
   __CPROVER_ensures(
-    __CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}
+    __CPROVER_forall {
+      int i;
+      (0 <= i && i < 10) ==> arr[i] == i
+    }
   )
+/* clang-format on */
 {
   for(int i = 0; i < 10; i++)
   {

regression/contracts/quantifiers-exists-ensures-01/main.c

@@ -1,8 +1,10 @@
 // clang-format off
-int f1(int *arr) __CPROVER_ensures(__CPROVER_exists {
-  int i;
-  (0 <= i && i < 10) ==> arr[i] == i
-})
+int f1(int *arr)
+  __CPROVER_assigns(*arr)
+  __CPROVER_ensures(__CPROVER_exists {
+    int i;
+    (0 <= i && i < 10) ==> arr[i] == i
+  })
 // clang-format on
 {
   for(int i = 0; i < 10; i++)

regression/contracts/quantifiers-forall-ensures-01/main.c

@@ -1,8 +1,10 @@
 // clang-format off
-int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
-  int i;
-  (0 <= i && i < 10) ==> arr[i] == 0
-})
+int f1(int *arr)
+  __CPROVER_assigns(*arr)
+  __CPROVER_ensures(__CPROVER_forall {
+    int i;
+    (0 <= i && i < 10) ==> arr[i] == 0
+  })
 // clang-format on
 {
   for(int i = 0; i < 10; i++)

regression/contracts/quantifiers-nested-01/main.c

@@ -1,12 +1,14 @@
 // clang-format off
-int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
-  int i;
-  __CPROVER_forall
-  {
-    int j;
-    (0 <= i && i < 10 && i <= j && j < 10) ==> arr[i] <= arr[j]
-  }
-})
+int f1(int *arr)
+  __CPROVER_assigns(*arr)
+  __CPROVER_ensures(__CPROVER_forall {
+    int i;
+    __CPROVER_forall
+    {
+      int j;
+      (0 <= i && i < 10 && i <= j && j < 10) ==> arr[i] <= arr[j]
+    }
+  })
 // clang-format on
 {
   for(int i = 0; i < 10; i++)

regression/contracts/quantifiers-nested-03/main.c

@@ -1,4 +1,4 @@
-int f1(int *arr)
+int f1(int *arr) __CPROVER_assigns(*arr)
   __CPROVER_ensures(__CPROVER_return_value == 0 && __CPROVER_exists {
     int i;
     (0 <= i && i < 10) && arr[i] == i

src/goto-instrument/code_contracts.cpp

@@ -513,20 +513,8 @@ void code_contractst::instrument_call_statement(
 
   exprt called_assigns =
     to_code_with_contract_type(called_symbol.type).assigns();
-  if(called_assigns.is_nil()) // Called function has no assigns clause
-  {
-    // Create a false assertion, so the analysis
-    // will fail if this function is called.
-    goto_programt failing_assertion;
-    failing_assertion.add(goto_programt::make_assertion(
-      false_exprt(), instruction_iterator->source_location));
-    program.insert_before_swap(instruction_iterator, failing_assertion);
-    ++instruction_iterator;
-
-    return;
-  }
-    else // Called function has assigns clause
-    {
+  if(!called_assigns.is_nil()) // Called function has assigns clause
+  {
       replace_symbolt replace;
       // Replace formal parameters
       code_function_callt::argumentst::const_iterator a_it =
@@ -540,6 +528,7 @@ void code_contractst::instrument_call_statement(
         if(!p_it->get_identifier().empty())
         {
           symbol_exprt p(p_it->get_identifier(), p_it->type());
+          std::cout << "p.get_identifier: " << p.get_identifier() << std::endl;
           replace.insert(p, *a_it);
         }
       }
@@ -634,9 +623,6 @@ bool code_contractst::add_pointer_checks(const std::string &function_name)
   const auto &type = to_code_with_contract_type(function_symbol.type);
 
   exprt assigns_expr = type.assigns();
-  // Return if there are no reference checks to perform.
-  if(assigns_expr.is_nil())
-    return false;
 
   assigns_clauset assigns(assigns_expr, *this, function_id, log);
 

src/goto-instrument/code_contracts.h

@@ -14,6 +14,7 @@ Date: February 2016
 #ifndef CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
 #define CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
 
+#include <iostream>
 #include <set>
 #include <string>
 #include <unordered_set>