From 2fd6095ba8f56cd43749bc331ecad86e509ec91c Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Mon, 28 Oct 2024 12:16:18 -0500
Subject: [PATCH] Support alias of member pointers in loop assigns inference

---
 .../loop_assigns_inference-04/main.c          | 22 ++++++
 .../loop_assigns_inference-04/test.desc       | 10 +++
 src/goto-instrument/loop_utils.cpp            | 70 ++++++++++++++++---
 3 files changed, 93 insertions(+), 9 deletions(-)
 create mode 100644 regression/contracts/loop_assigns_inference-04/main.c
 create mode 100644 regression/contracts/loop_assigns_inference-04/test.desc

diff --git a/regression/contracts/loop_assigns_inference-04/main.c b/regression/contracts/loop_assigns_inference-04/main.c
new file mode 100644
index 00000000000..fd6886eef0a
--- /dev/null
+++ b/regression/contracts/loop_assigns_inference-04/main.c
@@ -0,0 +1,22 @@
+struct hole
+{
+  int pos;
+};
+
+void set_len(struct hole *h, unsigned long int new_len)
+{
+  h->pos = new_len;
+}
+
+int main()
+{
+  int i = 0;
+  struct hole h;
+  h.pos = 0;
+  for(i = 0; i < 5; i++)
+    // __CPROVER_assigns(h.pos, i)
+    __CPROVER_loop_invariant(h.pos == i)
+    {
+      set_len(&h, h.pos + 1);
+    }
+}
diff --git a/regression/contracts/loop_assigns_inference-04/test.desc b/regression/contracts/loop_assigns_inference-04/test.desc
new file mode 100644
index 00000000000..4a019f2d1b2
--- /dev/null
+++ b/regression/contracts/loop_assigns_inference-04/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks assigns h->pos is inferred correctly.
diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp
index f05998a023a..e099b8c28c7 100644
--- a/src/goto-instrument/loop_utils.cpp
+++ b/src/goto-instrument/loop_utils.cpp
@@ -53,38 +53,90 @@ void get_assigns_lhs(
   assignst &assigns,
   std::function<bool(const exprt &)> predicate)
 {
-  if(
-    (lhs.id() == ID_symbol || lhs.id() == ID_member || lhs.id() == ID_index) &&
-    predicate(lhs))
+  assignst new_assigns;
+
+  if(lhs.id() == ID_symbol || lhs.id() == ID_index)
   {
-    assigns.insert(lhs);
+    // All variables `v` and their indexing expressions `v[idx]` are assigns.
+    new_assigns.insert(lhs);
+  }
+  else if(lhs.id() == ID_member)
+  {
+    auto op = to_member_expr(lhs).struct_op();
+    auto component_name = to_member_expr(lhs).get_component_name();
+
+    // Insert expressions of form `v.member`.
+    if(op.id() == ID_symbol)
+    {
+      new_assigns.insert(lhs);
+    }
+    // For expressions of form `v->member`, insert all targets `u->member`,
+    // where `u` and `v` alias.
+    else if(op.id() == ID_dereference)
+    {
+      const pointer_arithmetict ptr(to_dereference_expr(op).pointer());
+      for(const auto &mod : local_may_alias.get(t, ptr.pointer))
+      {
+        if(mod.id() == ID_unknown)
+        {
+          continue;
+        }
+        const exprt typed_mod =
+          typecast_exprt::conditional_cast(mod, ptr.pointer.type());
+        exprt to_insert;
+        if(ptr.offset.is_nil())
+        {
+          // u->member
+          to_insert = member_exprt(
+            dereference_exprt{typed_mod}, component_name, lhs.type());
+        }
+        else
+        {
+          // (u+offset)->member
+          to_insert = member_exprt(
+            dereference_exprt{plus_exprt{typed_mod, ptr.offset}},
+            component_name,
+            lhs.type());
+        }
+        new_assigns.insert(to_insert);
+      }
+    }
   }
   else if(lhs.id() == ID_dereference)
   {
+    // All dereference `*v` and their alias `*u` are assigns.
     const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
     for(const auto &mod : local_may_alias.get(t, ptr.pointer))
     {
-      const typecast_exprt typed_mod{mod, ptr.pointer.type()};
       if(mod.id() == ID_unknown)
       {
         continue;
       }
+      const exprt typed_mod =
+        typecast_exprt::conditional_cast(mod, ptr.pointer.type());
       exprt to_insert;
       if(ptr.offset.is_nil())
         to_insert = dereference_exprt{typed_mod};
       else
         to_insert = dereference_exprt{plus_exprt{typed_mod, ptr.offset}};
-      if(predicate(to_insert))
-        assigns.insert(std::move(to_insert));
+      new_assigns.insert(std::move(to_insert));
     }
   }
   else if(lhs.id() == ID_if)
   {
     const if_exprt &if_expr = to_if_expr(lhs);
 
-    get_assigns_lhs(local_may_alias, t, if_expr.true_case(), assigns);
-    get_assigns_lhs(local_may_alias, t, if_expr.false_case(), assigns);
+    get_assigns_lhs(
+      local_may_alias, t, if_expr.true_case(), assigns, predicate);
+    get_assigns_lhs(
+      local_may_alias, t, if_expr.false_case(), assigns, predicate);
   }
+
+  std::copy_if(
+    new_assigns.begin(),
+    new_assigns.end(),
+    std::inserter(assigns, assigns.begin()),
+    predicate);
 }
 
 void get_assigns(