From 6b2a4ee76d396235076160e32c4c6d3489391536 Mon Sep 17 00:00:00 2001
From: Remi Delmas <delmasrd@amazon.com>
Date: Wed, 23 Nov 2022 21:02:20 +0000
Subject: [PATCH] CONTRACTS: conditional havoc code

The condition was being checked on the
write set variable instead of write set element
variable
---
 .../havoc-conditional-target/check-foo.c      | 20 +++++++++++++
 .../havoc-conditional-target/check-foo.desc   |  9 ++++++
 .../havoc-conditional-target/replace-foo.c    | 30 +++++++++++++++++++
 .../havoc-conditional-target/replace-foo.desc |  9 ++++++
 src/ansi-c/library/cprover_contracts.c        |  4 +++
 .../dynamic-frames/dfcc_spec_functions.cpp    |  6 ++--
 6 files changed, 75 insertions(+), 3 deletions(-)
 create mode 100644 regression/contracts-dfcc/havoc-conditional-target/check-foo.c
 create mode 100644 regression/contracts-dfcc/havoc-conditional-target/check-foo.desc
 create mode 100644 regression/contracts-dfcc/havoc-conditional-target/replace-foo.c
 create mode 100644 regression/contracts-dfcc/havoc-conditional-target/replace-foo.desc

diff --git a/regression/contracts-dfcc/havoc-conditional-target/check-foo.c b/regression/contracts-dfcc/havoc-conditional-target/check-foo.c
new file mode 100644
index 00000000000..da3a6a97f2a
--- /dev/null
+++ b/regression/contracts-dfcc/havoc-conditional-target/check-foo.c
@@ -0,0 +1,20 @@
+#include <stdlib.h>
+
+void foo(int *out)
+  // clang-format off
+__CPROVER_requires(out ==> __CPROVER_is_fresh(out, sizeof(*out)))
+__CPROVER_assigns(out: *out)
+__CPROVER_ensures(out ==> *out == 1)
+// clang-format on
+{
+  if(out)
+    *out = 1;
+}
+
+int nondet_int();
+
+void main()
+{
+  int *out;
+  foo(out);
+}
diff --git a/regression/contracts-dfcc/havoc-conditional-target/check-foo.desc b/regression/contracts-dfcc/havoc-conditional-target/check-foo.desc
new file mode 100644
index 00000000000..3e04ad3edfb
--- /dev/null
+++ b/regression/contracts-dfcc/havoc-conditional-target/check-foo.desc
@@ -0,0 +1,9 @@
+CORE
+check-foo.c
+--dfcc main --enforce-contract foo _ --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks conditional havocs are behaving as expected.
diff --git a/regression/contracts-dfcc/havoc-conditional-target/replace-foo.c b/regression/contracts-dfcc/havoc-conditional-target/replace-foo.c
new file mode 100644
index 00000000000..34b9236caf9
--- /dev/null
+++ b/regression/contracts-dfcc/havoc-conditional-target/replace-foo.c
@@ -0,0 +1,30 @@
+#include <stdlib.h>
+
+void foo(int *out)
+  // clang-format off
+__CPROVER_requires(out ==> __CPROVER_is_fresh(out, sizeof(*out)))
+__CPROVER_assigns(out: *out)
+__CPROVER_ensures(out ==> *out == 1)
+// clang-format on
+{
+  if(out)
+    *out = 1;
+}
+
+int nondet_int();
+
+void bar()
+{
+  int i = 0;
+  int *out = nondet_int() ? &i : NULL;
+  foo(out);
+  // clang-format off
+  __CPROVER_assert(!out ==> (i == 0), "out not null implies initial value");
+  __CPROVER_assert(out ==> (i == 1), "out null implies updated value");
+  // clang-format on
+}
+
+int main(void)
+{
+  bar();
+}
diff --git a/regression/contracts-dfcc/havoc-conditional-target/replace-foo.desc b/regression/contracts-dfcc/havoc-conditional-target/replace-foo.desc
new file mode 100644
index 00000000000..3c7a77420d5
--- /dev/null
+++ b/regression/contracts-dfcc/havoc-conditional-target/replace-foo.desc
@@ -0,0 +1,9 @@
+CORE
+replace-foo.c
+--dfcc main --enforce-contract bar --replace-call-with-contract foo _ --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks conditional havocs are behaving as expected.
diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c
index d07148f0fdb..6a60374ad3a 100644
--- a/src/ansi-c/library/cprover_contracts.c
+++ b/src/ansi-c/library/cprover_contracts.c
@@ -1286,6 +1286,10 @@ void *__CPROVER_contracts_write_set_havoc_get_assignable_target(
   __CPROVER_size_t idx)
 {
 __CPROVER_HIDE:;
+#ifdef DFCC_DEBUG
+  __CPROVER_assert(write_set != 0, "write_set not NULL");
+#endif
+
   __CPROVER_contracts_car_t car = set->contract_assigns.elems[idx];
   if(car.is_writable)
     return car.lb;
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp
index 1ef72e3491f..bdf780b84c3 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp
@@ -200,10 +200,9 @@ void dfcc_spec_functionst::generate_havoc_function(
       // Use same source location as original call
       source_locationt location(ins_it->source_location());
       auto hook = hook_opt.value();
-      auto write_set_var = write_set_symbol.symbol_expr();
       code_function_callt call(
         library.dfcc_fun_symbol.at(hook).symbol_expr(),
-        {write_set_var, from_integer(next_idx, size_type())});
+        {write_set_symbol.symbol_expr(), from_integer(next_idx, size_type())});
 
       if(hook == dfcc_funt::WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET)
       {
@@ -233,7 +232,8 @@ void dfcc_spec_functionst::generate_havoc_function(
         body.add(goto_programt::make_function_call(call, location));
 
         auto goto_instruction = body.add(goto_programt::make_incomplete_goto(
-          utils.make_null_check_expr(write_set_var)));
+          utils.make_null_check_expr(target_expr), location));
+
         // create nondet assignment to the target
         side_effect_expr_nondett nondet(target_type, location);
         body.add(goto_programt::make_assignment(