Merge pull request #6074 from feliperodri/empty-assigns-clause

Enforce purity on missing assigns clause

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 \d+ .*: 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 \d+ .*: FAILURE$
+^\[baz.1\] line \d+ .*: 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,50 +513,38 @@ 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 =
+      call.arguments().begin();
+    for(code_typet::parameterst::const_iterator p_it =
+          called_type.parameters().begin();
+        p_it != called_type.parameters().end() &&
+        a_it != call.arguments().end();
+        ++p_it, ++a_it)
     {
-      replace_symbolt replace;
-      // Replace formal parameters
-      code_function_callt::argumentst::const_iterator a_it =
-        call.arguments().begin();
-      for(code_typet::parameterst::const_iterator p_it =
-            called_type.parameters().begin();
-          p_it != called_type.parameters().end() &&
-          a_it != call.arguments().end();
-          ++p_it, ++a_it)
+      if(!p_it->get_identifier().empty())
       {
-        if(!p_it->get_identifier().empty())
-        {
-          symbol_exprt p(p_it->get_identifier(), p_it->type());
-          replace.insert(p, *a_it);
-        }
+        symbol_exprt p(p_it->get_identifier(), p_it->type());
+        replace.insert(p, *a_it);
       }
-
-      replace(called_assigns);
-
-      // check compatibility of assigns clause with the called function
-      assigns_clauset called_assigns_clause(
-        called_assigns, *this, function_id, log);
-      exprt compatible =
-        assigns_clause.compatible_expression(called_assigns_clause);
-      goto_programt alias_assertion;
-      alias_assertion.add(goto_programt::make_assertion(
-        compatible, instruction_iterator->source_location));
-      program.insert_before_swap(instruction_iterator, alias_assertion);
-      ++instruction_iterator;
     }
+
+    replace(called_assigns);
+
+    // check compatibility of assigns clause with the called function
+    assigns_clauset called_assigns_clause(
+      called_assigns, *this, function_id, log);
+    exprt compatible =
+      assigns_clause.compatible_expression(called_assigns_clause);
+    goto_programt alias_assertion;
+    alias_assertion.add(goto_programt::make_assertion(
+      compatible, instruction_iterator->source_location));
+    program.insert_before_swap(instruction_iterator, alias_assertion);
+    ++instruction_iterator;
+  }
 }
 
 bool code_contractst::check_for_looped_mallocs(const goto_programt &program)
@@ -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);