Function contracts: new method for havocking assigns clause targets

that works when there are dependencies between targets.

We now take a snapshot of the target addresses if they are valid and
havoc them in a second step if they are valid.  Previously we were
havocking targets directly in an arbitrary sequence, and havocking
s->ptr before *(s->ptr) or __CPROVER_POINTER_OBJECT(s->ptr) would
cause spurious errors.

Added a regression test with dependent assigns targets that fails
using the previous method.

Author: Remi Delmas

regression/contracts/assigns_enforce_21/test.desc

@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 main.c function bar
 ^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
-^\[bar.\d+\] line \d+ Check that x is assignable: FAILURE$
+^\[bar.\d+\] line \d+ Check that x assigned by replaced quz is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_replace_08/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo --replace-call-with-contract bar _ --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
-\[foo.\d+\] line \d+ Check that \*z is assignable: FAILURE$
+\[foo.\d+\] line \d+ Check that \*z assigned by replaced bar is assignable: FAILURE$
 ^.* 1 of \d+ failed \(\d+ iteration.*\)$
 ^VERIFICATION FAILED$
 --

regression/contracts/assigns_replace_09/test.desc

@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract bar --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[foo.\d+\] line \d+ Check that \*z is assignable: SUCCESS$
+\[foo.\d+\] line \d+ Check that \*z assigned by replaced bar is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^Condition: \!not\_found$

regression/contracts/assigns_replace_havoc_dependent_targets_fail/enforce.desc

@@ -0,0 +1,9 @@
+CORE
+main_enforce.c
+--enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Verifies the contract being replaced in `replace_resize_vec.desc`.

regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_enforce.c

@@ -0,0 +1,9 @@
+#include "vect.h"
+
+int main()
+{
+  vect *v;
+  size_t incr;
+  resize_vec(v, incr);
+  return 0;
+}

regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_replace.c

@@ -0,0 +1,8 @@
+#include "vect.h"
+
+int main()
+{
+  vect *v;
+  resize_vec_incr10(v);
+  return 0;
+}

regression/contracts/assigns_replace_havoc_dependent_targets_fail/replace.desc

@@ -0,0 +1,16 @@
+CORE
+main_replace.c
+--replace-call-with-contract resize_vec --enforce-contract resize_vec_incr10 _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+^\[.*\] .* Check that v->size assigned by replaced resize_vec is assignable: SUCCESS
+^\[.*\] .* Check that v->arr assigned by replaced resize_vec is assignable: FAILURE
+^\[.*\] .* Check that POINTER_OBJECT\(\(const void \*\)v->arr\) assigned by replaced resize_vec is assignable: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Shows that when an assigns clause contains targets that are dependent, 
+in this case, a pointer variable `v->arr` and
+the object it points to `__CPROVER_POINTER_OBJECT(v->arr)`, we can correctly
+havoc them when replacing the call by the contract.
+In this version of the test the inclusion check must fail.

regression/contracts/assigns_replace_havoc_dependent_targets_fail/vect.h

@@ -0,0 +1,48 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct vect
+{
+  char *arr;
+  size_t size;
+} vect;
+
+void resize_vec(vect *v, size_t incr)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
+  0 < incr && incr < __CPROVER_max_malloc_size - v->size &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+__CPROVER_assigns(v->size, v->arr, __CPROVER_POINTER_OBJECT(v->arr))
+__CPROVER_ensures(
+  v->size == __CPROVER_old(v->size) + __CPROVER_old(incr) &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+// clang-format on
+{
+  free(v->arr);
+  v->size += incr;
+  v->arr = malloc(v->size);
+  return;
+}
+
+void resize_vec_incr10(vect *v)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
+  v->size + 10 < __CPROVER_max_malloc_size &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+__CPROVER_assigns(v->size)
+__CPROVER_ensures(
+  v->size == __CPROVER_old(v->size) + 10 &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+// clang-format on
+{
+  resize_vec(v, 10);
+  return;
+}

regression/contracts/assigns_replace_havoc_dependent_targets_pass/enforce.desc

@@ -0,0 +1,9 @@
+CORE
+main_enforce.c
+--enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Verifies the contract being replaced in `replace_resize_vec.desc`.

regression/contracts/assigns_replace_havoc_dependent_targets_pass/main_enforce.c

@@ -0,0 +1,9 @@
+#include "vect.h"
+
+int main()
+{
+  vect *v;
+  size_t incr;
+  resize_vec(v, incr);
+  return 0;
+}

regression/contracts/assigns_replace_havoc_dependent_targets_pass/main_replace.c

@@ -0,0 +1,8 @@
+#include "vect.h"
+
+int main()
+{
+  vect *v;
+  resize_vec_incr10(v);
+  return 0;
+}

regression/contracts/assigns_replace_havoc_dependent_targets_pass/replace.desc

@@ -0,0 +1,16 @@
+CORE
+main_replace.c
+--replace-call-with-contract resize_vec --enforce-contract resize_vec_incr10 _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+^VERIFICATION SUCCESSFUL$
+^\[.*\] .* Check that v->size assigned by replaced resize_vec is assignable: SUCCESS
+^\[.*\] .* Check that v->arr assigned by replaced resize_vec is assignable: SUCCESS
+^\[.*\] .* Check that POINTER_OBJECT\(\(const void \*\)v->arr\) assigned by replaced resize_vec is assignable: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Shows that when an assigns clause contains targets that are dependent, 
+in this case, a pointer variable `v->arr` and
+the object it points to `__CPROVER_POINTER_OBJECT(v->arr)`, we can correctly
+havoc them when replacing the call by the contract.
+In this version of the test the inclusion check must pass.

regression/contracts/assigns_replace_havoc_dependent_targets_pass/vect.h

@@ -0,0 +1,48 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct vect
+{
+  char *arr;
+  size_t size;
+} vect;
+
+void resize_vec(vect *v, size_t incr)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
+  0 < incr && incr < __CPROVER_max_malloc_size - v->size &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+__CPROVER_assigns(v->size, v->arr, __CPROVER_POINTER_OBJECT(v->arr))
+__CPROVER_ensures(
+  v->size == __CPROVER_old(v->size) + __CPROVER_old(incr) &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+// clang-format on
+{
+  free(v->arr);
+  v->size += incr;
+  v->arr = malloc(v->size);
+  return;
+}
+
+void resize_vec_incr10(vect *v)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
+  v->size + 10 < __CPROVER_max_malloc_size &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+__CPROVER_assigns(*v, __CPROVER_POINTER_OBJECT(v->arr))
+__CPROVER_ensures(
+  v->size == __CPROVER_old(v->size) + 10 &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+// clang-format on
+{
+  resize_vec(v, 10);
+  return;
+}

src/goto-instrument/Makefile

@@ -18,6 +18,7 @@ SRC = accelerate/accelerate.cpp \
       call_sequences.cpp \
       contracts/assigns.cpp \
       contracts/contracts.cpp \
+      contracts/havoc_assigns_clause_targets.cpp \
       contracts/memory_predicates.cpp \
       contracts/utils.cpp \
       concurrency.cpp \

src/goto-instrument/contracts/contracts.cpp

@@ -43,6 +43,7 @@ Date: February 2016
 #include <util/replace_symbol.h>
 #include <util/std_code.h>
 
+#include "havoc_assigns_clause_targets.h"
 #include "memory_predicates.h"
 #include "utils.h"
 
@@ -786,15 +787,17 @@ bool code_contractst::apply_function_contract(
   // ...for assigns clause targets
   if(!assigns_clause.empty())
   {
-    assigns_clauset assigns_clause(
-      targets.operands(), log, ns, target_function, symbol_table);
-
-    // Havoc all targets in the write set
-    assignst assigns;
-    assigns.insert(targets.operands().cbegin(), targets.operands().cend());
-
-    havoc_assigns_targetst havoc_gen(assigns, ns);
-    havoc_gen.append_full_havoc_code(location, havoc_instructions);
+    // Havoc all targets in the assigns clause
+    // TODO handle local statics possibly touched by this function
+    havoc_assigns_clause_targets(
+      target_function,
+      targets.operands(),
+      havoc_instructions,
+      // context parameters
+      location,
+      mode,
+      ns,
+      symbol_table);
   }
 
   // ...for the return value
@@ -1401,8 +1404,20 @@ code_contractst::add_inclusion_check(
   source_locationt location_no_checks =
     instruction_it->source_location_nonconst();
   disable_pointer_checks(location_no_checks);
-  location_no_checks.set_comment(
-    "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable");
+
+  // does this assignment come from some contract replacement ?
+  const auto &comment = location_no_checks.get_comment();
+  if(is_assigns_clause_replacement_tracking_comment(comment))
+  {
+    location_no_checks.set_comment(
+      "Check that " + id2string(comment) + " is assignable");
+  }
+  else
+  {
+    location_no_checks.set_comment(
+      "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable");
+  }
+
   assertion.add(goto_programt::make_assertion(
     assigns.generate_inclusion_check(car, cfg_info_opt), location_no_checks));
   insert_before_swap_and_advance(program, instruction_it, assertion);