From 0b7047fba1c163ca508c51a721167746621582c2 Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Tue, 5 Nov 2024 09:27:00 -0600
Subject: [PATCH] Switch to a more aggressive loop-assigns widening strategy
 for DFCC

---
 .../invar_havoc_dynamic_array_const_idx/main.c  |  2 +-
 .../loop_assigns_inference-05/main.c            | 17 +++++++++++++++++
 .../loop_assigns_inference-05/test.desc         | 15 +++++++++++++++
 .../dynamic-frames/dfcc_infer_loop_assigns.cpp  |  4 +++-
 4 files changed, 36 insertions(+), 2 deletions(-)
 create mode 100644 regression/contracts-dfcc/loop_assigns_inference-05/main.c
 create mode 100644 regression/contracts-dfcc/loop_assigns_inference-05/test.desc

diff --git a/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/main.c b/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/main.c
index 10d2c7a1904..69d7285b4c2 100644
--- a/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/main.c
+++ b/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/main.c
@@ -10,7 +10,7 @@ void main()
   data[4] = 0;
 
   for(unsigned i = 0; i < SIZE; i++)
-    __CPROVER_loop_invariant(i <= SIZE)
+    __CPROVER_assigns(data[1], i) __CPROVER_loop_invariant(i <= SIZE)
     {
       data[1] = i;
     }
diff --git a/regression/contracts-dfcc/loop_assigns_inference-05/main.c b/regression/contracts-dfcc/loop_assigns_inference-05/main.c
new file mode 100644
index 00000000000..b4888b702ed
--- /dev/null
+++ b/regression/contracts-dfcc/loop_assigns_inference-05/main.c
@@ -0,0 +1,17 @@
+#include <stdlib.h>
+
+#define SIZE 8
+
+int main()
+{
+  int i = 0;
+  int *j = malloc(SIZE * sizeof(int));
+  for(i = 0; i < SIZE; i++)
+    // __CPROVER_assigns(h.pos, i)
+    __CPROVER_loop_invariant(0 <= i && i <= SIZE)
+    {
+      int *k;
+      k = j + i;
+      *k = 1;
+    }
+}
diff --git a/regression/contracts-dfcc/loop_assigns_inference-05/test.desc b/regression/contracts-dfcc/loop_assigns_inference-05/test.desc
new file mode 100644
index 00000000000..dcba2a1f5eb
--- /dev/null
+++ b/regression/contracts-dfcc/loop_assigns_inference-05/test.desc
@@ -0,0 +1,15 @@
+CORE dfcc-only
+main.c
+--no-malloc-may-fail --dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.loop_invariant_base.\d+\] line \d+ Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line \d+ Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line \d+ Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line \d+ Check step was unwound for loop .*: SUCCESS$
+^\[set_len.assigns.\d+\] line \d+ Check that \*k is assignable: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks assigns __CPROVER_object_whole(k) is inferred correctly,
+which requires widening *k to the whole object.
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
index 5c36617734e..36c724498e2 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
@@ -262,7 +262,9 @@ static assignst dfcc_infer_loop_assigns_for_loop(
     {
       address_of_exprt address_of_expr(expr);
       address_of_expr.add_source_location() = expr.source_location();
-      if(!is_constant(address_of_expr))
+      // Widen assigns targets to object_whole if `expr` is a dereference or
+      // with constant address.
+      if(expr.id() == ID_dereference || !is_constant(address_of_expr))
       {
         // Target address is not constant, widening to the whole object
         result.emplace(make_object_whole_call_expr(address_of_expr, ns));