Check subset relationship of assigns clause during replacement

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

regression/contracts/assigns_replace_08/main.c

@@ -0,0 +1,19 @@
+#include <stdlib.h>
+
+int x;
+int *z = &x;
+
+void bar() __CPROVER_assigns(*z)
+{
+}
+
+void foo() __CPROVER_assigns()
+{
+  bar();
+}
+
+int main()
+{
+  foo();
+  return 0;
+}

regression/contracts/assigns_replace_08/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--enforce-contract foo --replace-call-with-contract bar _ --pointer-primitive-check
+^EXIT=10$
+^SIGNAL=0$
+\[\d+\] file main.c line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
+\[\d+\] file main.c line \d+ Check that \*z is assignable: FAILURE$
+^.* 2 of \d+ failed \(\d+ iteration.*\)$
+^VERIFICATION FAILED$
+--
+\[\d+\] file main.c line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS$
+\[\d+\] file main.c line \d+ Check that \*z is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+Checks whether CBMC properly evaluates subset relationship on assigns
+during replacement.

regression/contracts/assigns_validity_pointer_01/main.c

@@ -17,17 +17,17 @@ void baz() __CPROVER_assigns(*z) __CPROVER_ensures(z == NULL || *z == 7)
     *z = 7;
 }
 
-void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0)
+void foo(int *x) __CPROVER_assigns(*x, *z) __CPROVER_requires(*x > 0)
   __CPROVER_ensures(*x == 3)
 {
   bar(x, NULL);
-  z == NULL;
   baz();
 }
 
 int main()
 {
   int n;
+  z = malloc(sizeof(*z));
   foo(&n);
 
   assert(n == 3);

regression/contracts/assigns_validity_pointer_02/test.desc

@@ -3,11 +3,16 @@ main.c
 --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[foo.\d+\] line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS$
+^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that baz\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
-//^([foo\.1] line 15 assertion: FAILURE)
 --
-\[foo\.1\] line 24 assertion: FAILURE
-\[foo\.3\] line 27 assertion: FAILURE
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$
+^\[foo.\d+\] line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
+^\[foo.\d+\] line \d+ Check that \*x is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that baz\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
 --
 Verification:
 This test checks support for a NULL pointer that is assigned to by

regression/contracts/assigns_validity_pointer_04/test.desc

@@ -3,8 +3,10 @@ main.c
 --enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz _ --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
+^\[\d+\] file main.c line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
+^\[\d+\] file main.c line \d+ Check that baz\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
 ^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$
-^.* 1 of \d+ failed \(\d+ iteration.*\)$
+^.* 3 of \d+ failed \(\d+ iteration.*\)$
 ^VERIFICATION FAILED$
 // bar
 ASSERT \*foo::x > 0

regression/contracts/test_aliasing_ensure_indirect/test.desc

@@ -7,7 +7,7 @@ main.c
 \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
 \[bar.\d+\] line \d+ Check that z is assignable: SUCCESS
 \[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS
-\[foo.\d+\] line \d+ Check that callee's assigns clause is a subset of caller's: SUCCESS
+\[foo.\d+\] line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --

src/goto-instrument/contracts/contracts.cpp

@@ -601,8 +601,31 @@ bool code_contractst::apply_function_contract(
   // in the assigns clause.
   if(assigns.is_not_nil())
   {
-    assigns_clauset assigns_cause(assigns, log, ns);
-    auto assigns_havoc = assigns_cause.generate_havoc_code();
+    assigns_clauset assigns_clause(assigns, log, ns);
+
+    // Retrieve assigns clause of the caller function if exists.
+    const irep_idt &caller_function = target->source_location.get_function();
+    auto caller_assigns =
+      to_code_with_contract_type(ns.lookup(caller_function).type).assigns();
+
+    if(caller_assigns.is_not_nil())
+    {
+      // check subset relationship of assigns clause for called function
+      assigns_clauset caller_assigns_clause(caller_assigns, log, ns);
+      goto_programt subset_check_assertion;
+      subset_check_assertion.add(goto_programt::make_assertion(
+        caller_assigns_clause.generate_subset_check(assigns_clause),
+        assigns_clause.location));
+      subset_check_assertion.instructions.back().source_location.set_comment(
+        "Check that " + id2string(function) +
+        "'s assigns clause is a subset of " + id2string(caller_function) +
+        "'s assigns clause");
+      insert_before_swap_and_advance(
+        goto_program, target, subset_check_assertion);
+    }
+
+    // Havoc all targets in global write set
+    auto assigns_havoc = assigns_clause.generate_havoc_code();
 
     // Insert the non-deterministic assignment immediately before the call site.
     insert_before_swap_and_advance(goto_program, target, assigns_havoc);
@@ -772,8 +795,8 @@ void code_contractst::instrument_call_statement(
     alias_assertion.instructions.back().source_location.set_comment(
       "Check that " + from_expr(ns, alias_expr.id(), alias_expr) +
       " is assignable");
-    program.insert_before_swap(instruction_iterator, alias_assertion);
-    ++instruction_iterator;
+    insert_before_swap_and_advance(
+      program, instruction_iterator, alias_assertion);
   }
 
   const symbolt &called_symbol = ns.lookup(called_name);
@@ -810,9 +833,12 @@ void code_contractst::instrument_call_statement(
     alias_assertion.add(goto_programt::make_assertion(
       subset_check, instruction_iterator->source_location));
     alias_assertion.instructions.back().source_location.set_comment(
-      "Check that callee's assigns clause is a subset of caller's");
-    program.insert_before_swap(instruction_iterator, alias_assertion);
-    ++instruction_iterator;
+      "Check that " + id2string(called_name) +
+      "'s assigns clause is a subset of " +
+      id2string(instruction_iterator->source_location.get_function()) +
+      "'s assigns clause");
+    insert_before_swap_and_advance(
+      program, instruction_iterator, alias_assertion);
   }
 }