From 2a270741ae31e50d5a03d3063bd2c66e4ddbfcd4 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 4 Nov 2024 20:13:14 +0000
Subject: [PATCH] goto-symex: assumed pointer equalities must update value set

Value sets and constant propagation are our only sources of points-to
information when resolving dereferences in goto-symex. Therefore,
assuming or branching on equalities of pointer-typed variables must have
us consider both of their value sets to be equal. Else we may end up
with spurious counterexamples as seen with the enclosed regression test
(where we previously did not have any known value for `a`).

Fixes: #8492
---
 regression/cbmc/Pointer_Assume2/main.c    | 27 +++++++++++++++++++++++
 regression/cbmc/Pointer_Assume2/test.desc |  7 ++++++
 src/goto-symex/goto_state.cpp             | 25 ++++++++++++++++-----
 3 files changed, 54 insertions(+), 5 deletions(-)
 create mode 100644 regression/cbmc/Pointer_Assume2/main.c
 create mode 100644 regression/cbmc/Pointer_Assume2/test.desc

diff --git a/regression/cbmc/Pointer_Assume2/main.c b/regression/cbmc/Pointer_Assume2/main.c
new file mode 100644
index 00000000000..5847dc08a07
--- /dev/null
+++ b/regression/cbmc/Pointer_Assume2/main.c
@@ -0,0 +1,27 @@
+int main()
+{
+  int *r;
+  int *a;
+#if 1
+  _Bool tmp_if_expr;
+  if(r == 0)
+  {
+    tmp_if_expr = 0;
+  }
+  else
+  {
+    r = __CPROVER_allocate(sizeof(int), 0);
+    tmp_if_expr = 1;
+  }
+
+  __CPROVER_assume(tmp_if_expr);
+#else
+  // this works, because we constant-propagate r as an address-of expression
+  __CPROVER_assume(r != 0);
+  r = __CPROVER_allocate(sizeof(int), 0);
+#endif
+  __CPROVER_assume(r != 0);
+  __CPROVER_assume(r == a);
+  __CPROVER_assert(r == a, " r == a before");
+  __CPROVER_assert(*r == *a, "*r == *a before");
+}
diff --git a/regression/cbmc/Pointer_Assume2/test.desc b/regression/cbmc/Pointer_Assume2/test.desc
new file mode 100644
index 00000000000..9c96469df12
--- /dev/null
+++ b/regression/cbmc/Pointer_Assume2/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp
index 8cbe0038a13..f4d2fe9c1ae 100644
--- a/src/goto-symex/goto_state.cpp
+++ b/src/goto-symex/goto_state.cpp
@@ -92,19 +92,20 @@ void goto_statet::apply_condition(
     if(is_ssa_expr(rhs))
       std::swap(lhs, rhs);
 
-    if(is_ssa_expr(lhs) && goto_symex_can_forward_propagatet(ns)(rhs))
+    if(is_ssa_expr(lhs))
     {
       const ssa_exprt &ssa_lhs = to_ssa_expr(lhs);
       INVARIANT(
         !ssa_lhs.get_level_2().empty(),
         "apply_condition operand should be L2 renamed");
+      const ssa_exprt l1_lhs = remove_level_2(ssa_lhs);
 
       if(
-        previous_state.threads.size() == 1 ||
-        previous_state.write_is_shared(ssa_lhs, ns) !=
-          goto_symex_statet::write_is_shared_resultt::SHARED)
+        goto_symex_can_forward_propagatet(ns)(rhs) &&
+        (previous_state.threads.size() == 1 ||
+         previous_state.write_is_shared(ssa_lhs, ns) !=
+           goto_symex_statet::write_is_shared_resultt::SHARED))
       {
-        const ssa_exprt l1_lhs = remove_level_2(ssa_lhs);
         const irep_idt &l1_identifier = l1_lhs.get_identifier();
 
         level2.increase_generation(
@@ -118,6 +119,20 @@ void goto_statet::apply_condition(
 
         value_set.assign(l1_lhs, rhs, ns, true, false);
       }
+      else if(is_ssa_expr(rhs))
+      {
+        const ssa_exprt &ssa_rhs = to_ssa_expr(rhs);
+        INVARIANT(
+          !ssa_rhs.get_level_2().empty(),
+          "apply_condition operand should be L2 renamed");
+        const ssa_exprt l1_rhs = remove_level_2(ssa_rhs);
+
+        // We have a condition a == b. Make both a's and b's value sets the
+        // union of their previous value sets (the last "true" argument makes
+        // sure we add rather than replace value sets).
+        value_set.assign(l1_lhs, l1_rhs, ns, true, true);
+        value_set.assign(l1_rhs, l1_lhs, ns, true, true);
+      }
     }
   }
   else if(