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

Author: tautschnig

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

regression/cbmc/Pointer_Assume2/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

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(