Merge pull request #6345 from feliperodri/fix-contract-replacement

Check subset relationship of assigns clause during replacement

Author: feliperodri

regression/contracts/assigns_enforce_structs_07/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --enforce-all-contracts _ --pointer-check
 ^EXIT=10$
@@ -12,3 +12,6 @@ main.c
 --
 Checks whether CBMC properly evaluates write set of members
 from invalid objects. In this case, they are not writable.
+
+Bug: We need to check the validity of each dereference
+when accessing struct members.

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/ansi-c/ansi_c_convert_type.cpp

@@ -272,6 +272,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
       for(auto &assignment : to_unary_expr(as_expr).op().operands())
         assigns.add_to_operands(std::move(assignment));
     }
+    assigns.add_source_location() = as_expr.source_location();
   }
   else if(type.id() == ID_C_spec_ensures)
   {

src/goto-instrument/contracts/assigns.cpp

@@ -43,45 +43,62 @@ exprt assigns_clauset::targett::normalize(const exprt &expr)
 exprt assigns_clauset::targett::generate_containment_check(
   const address_of_exprt &lhs_address) const
 {
-  exprt::operandst condition;
+  exprt::operandst address_validity;
+  exprt::operandst containment_check;
 
   // __CPROVER_w_ok(target, sizeof(target))
-  condition.push_back(w_ok_exprt(
+  address_validity.push_back(w_ok_exprt(
     address,
     size_of_expr(dereference_exprt(address).type(), parent.ns).value()));
 
+  // __CPROVER_w_ok(lhs, sizeof(lhs))
+  address_validity.push_back(w_ok_exprt(
+    lhs_address,
+    size_of_expr(dereference_exprt(lhs_address).type(), parent.ns).value()));
+
   // __CPROVER_same_object(lhs, target)
-  condition.push_back(same_object(lhs_address, address));
+  containment_check.push_back(same_object(lhs_address, address));
 
   // If assigns target was a dereference, comparing objects is enough
-  if(id == ID_dereference)
+  // and the resulting condition will be
+  // __CPROVER_w_ok(target, sizeof(target))
+  // && __CPROVER_w_ok(lhs, sizeof(lhs))
+  // ==> __CPROVER_same_object(lhs, target)
+  if(id != ID_dereference)
   {
-    return conjunction(condition);
+    const auto lhs_offset = pointer_offset(lhs_address);
+    const auto own_offset = pointer_offset(address);
+
+    // __CPROVER_offset(lhs) >= __CPROVER_offset(target)
+    containment_check.push_back(
+      binary_relation_exprt(lhs_offset, ID_ge, own_offset));
+
+    const auto lhs_region = plus_exprt(
+      typecast_exprt::conditional_cast(
+        size_of_expr(lhs_address.object().type(), parent.ns).value(),
+        lhs_offset.type()),
+      lhs_offset);
+
+    const exprt own_region = plus_exprt(
+      typecast_exprt::conditional_cast(
+        size_of_expr(address.object().type(), parent.ns).value(),
+        own_offset.type()),
+      own_offset);
+
+    // (sizeof(lhs) + __CPROVER_offset(lhs)) <=
+    // (sizeof(target) + __CPROVER_offset(target))
+    containment_check.push_back(
+      binary_relation_exprt(lhs_region, ID_le, own_region));
   }
 
-  const auto lhs_offset = pointer_offset(lhs_address);
-  const auto own_offset = pointer_offset(address);
-
-  // __CPROVER_offset(lhs) >= __CPROVER_offset(target)
-  condition.push_back(binary_relation_exprt(lhs_offset, ID_ge, own_offset));
-
-  const auto lhs_region = plus_exprt(
-    typecast_exprt::conditional_cast(
-      size_of_expr(lhs_address.object().type(), parent.ns).value(),
-      lhs_offset.type()),
-    lhs_offset);
-
-  const exprt own_region = plus_exprt(
-    typecast_exprt::conditional_cast(
-      size_of_expr(address.object().type(), parent.ns).value(),
-      own_offset.type()),
-    own_offset);
-
-  // (sizeof(lhs) + __CPROVER_offset(lhs)) <=
-  // (sizeof(target) + __CPROVER_offset(target))
-  condition.push_back(binary_relation_exprt(lhs_region, ID_le, own_region));
-
-  return conjunction(condition);
+  // __CPROVER_w_ok(target, sizeof(target))
+  // && __CPROVER_w_ok(lhs, sizeof(lhs))
+  // ==> __CPROVER_same_object(lhs, target)
+  //     && __CPROVER_offset(lhs) >= __CPROVER_offset(target)
+  //     && (sizeof(lhs) + __CPROVER_offset(lhs)) <=
+  //        (sizeof(target) + __CPROVER_offset(target))
+  return binary_relation_exprt(
+    conjunction(address_validity), ID_implies, conjunction(containment_check));
 }
 
 assigns_clauset::assigns_clauset(
@@ -152,7 +169,6 @@ exprt assigns_clauset::generate_containment_check(const exprt &lhs) const
   {
     condition.push_back(target.generate_containment_check(lhs_address));
   }
-
   for(const auto &target : global_write_set)
   {
     condition.push_back(target.generate_containment_check(lhs_address));
@@ -174,12 +190,6 @@ exprt assigns_clauset::generate_subset_check(
   exprt result = true_exprt();
   for(const auto &subtarget : subassigns.global_write_set)
   {
-    // TODO: Optimize the implication generated due to the validity check.
-    // In some cases, e.g. when `subtarget` is known to be `NULL`,
-    // the implication can be skipped entirely. See #6105 for more details.
-    auto validity_check =
-      w_ok_exprt(subtarget.address, from_integer(0, unsigned_int_type()));
-
     exprt::operandst current_subtarget_found_conditions;
     for(const auto &target : global_write_set)
     {
@@ -191,12 +201,7 @@ exprt assigns_clauset::generate_subset_check(
       current_subtarget_found_conditions.push_back(
         target.generate_containment_check(subtarget.address));
     }
-
-    auto current_subtarget_found = or_exprt(
-      not_exprt(validity_check),
-      disjunction(current_subtarget_found_conditions));
-
-    result = and_exprt(result, current_subtarget_found);
+    result = and_exprt(result, disjunction(current_subtarget_found_conditions));
   }
 
   return result;

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