Merge pull request #7380 from remi-delmas-3000/contracts-fix-havoc-codegen

CONTRACTS: Fix conditional havoc code

Author: tautschnig

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

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.

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

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.

src/ansi-c/library/cprover_contracts.c

@@ -1290,6 +1290,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;

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(