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,11 @@
 CORE
 main.c
 --enforce-all-contracts
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
+^\[f1.1\] line 3 .*: SUCCESS$
+^VERIFICATION SUCCESSFUL$
 --
 --
-This test checks that verification fails when a function with an assigns clause calls a function without an assigns clause.
+This test checks that verification succeeds when enforcing a contract
+for functions, without assigns clauses, that don't modify anything.

regression/contracts/assigns_enforce_15/main.c

@@ -0,0 +1,29 @@
+int global = 0;
+
+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 baz() __CPROVER_ensures(__CPROVER_return_value == global)
+{
+  global = global + 1;
+  return global;
+}
+
+int main()
+{
+  int n;
+  n = foo(&n);
+  n = baz();
+  return 0;
+}

regression/contracts/assigns_enforce_15/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[bar.1\] line 13 .*: FAILURE$
+^\[baz.1\] line 18 .*: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when enforcing a contract
+for functions, without assigns clauses, that modify an input.

regression/contracts/function_check_02/main.c

@@ -4,10 +4,16 @@
 // A known bug (resolved in PR #2278) causes the use of quantifiers
 // in ensures to fail.
 
+// clang-format off
 int initialize(int *arr)
+  __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 =
@@ -634,9 +622,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);