From 1b73ae592c90dc98750fe2508148cd3c231987fc Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 2 Jan 2021 22:46:03 +0000
Subject: [PATCH] Value sets must not be field sensitive for unions

Distinct fields in a union need not refer to distinct memory locations.
Thus treat all fields of a union the same, with pointers assigned to any
field being dereferenceable via another field.

Fixes: #5263
---
 regression/cbmc/union14/test.desc  |  7 +++----
 regression/cbmc/union16/main.c     | 29 +++++++++++++++++++++++++++++
 regression/cbmc/union16/test.desc  | 12 ++++++++++++
 src/pointer-analysis/value_set.cpp | 13 ++++++-------
 4 files changed, 50 insertions(+), 11 deletions(-)
 create mode 100644 regression/cbmc/union16/main.c
 create mode 100644 regression/cbmc/union16/test.desc

diff --git a/regression/cbmc/union14/test.desc b/regression/cbmc/union14/test.desc
index e6237ce4922..6dd0e558212 100644
--- a/regression/cbmc/union14/test.desc
+++ b/regression/cbmc/union14/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$
@@ -7,6 +7,5 @@ main.c
 --
 ^warning: ignoring
 --
-Value sets do not properly track pointers through byte-extract operations. Thus
-derferencing yields __CPROVER_memory, which results in a spurious verification
-failure.
+Value sets did not properly track pointers through unions. Thus derferencing
+yields __CPROVER_memory, which results in a spurious verification failure.
diff --git a/regression/cbmc/union16/main.c b/regression/cbmc/union16/main.c
new file mode 100644
index 00000000000..d8482fa7115
--- /dev/null
+++ b/regression/cbmc/union16/main.c
@@ -0,0 +1,29 @@
+typedef void (*callback_t)(void);
+
+struct xfer
+{
+  union { /*< FIX: union -> struct */
+    struct
+    {
+      int *buf;
+      callback_t callback; /*< FIX: remove */
+    } a;
+  };
+} g_xfer;
+
+int g_buf;
+
+int main()
+{
+  g_xfer = (struct xfer){{{&g_buf}}};
+
+  /* FIX, uncomment (only on cbmc develop 9ee5b9d6): */
+  // g_xfer.a.buf = &g_buf;
+
+  /* check the pointer was initialized properly */
+  assert(g_xfer.a.buf == &g_buf);
+
+  g_xfer.a.buf[0] = 42;          /* write a value via the pointer */
+  assert(g_xfer.a.buf[0] == 42); /* check it was written */
+  assert(g_buf == 42); /* the underlying value should also be updated */
+}
diff --git a/regression/cbmc/union16/test.desc b/regression/cbmc/union16/test.desc
new file mode 100644
index 00000000000..1b0b90e1916
--- /dev/null
+++ b/regression/cbmc/union16/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Value sets did not properly track pointers through unions. This regression test
+was provided in #5263, including comments about simplifications that make it
+work.
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 58ebd889a9f..91af16c9ead 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -1180,10 +1180,9 @@ void value_sett::assign(
 
   const typet &type=ns.follow(lhs.type());
 
-  if(type.id()==ID_struct ||
-     type.id()==ID_union)
+  if(type.id() == ID_struct)
   {
-    for(const auto &c : to_struct_union_type(type).components())
+    for(const auto &c : to_struct_type(type).components())
     {
       const typet &subtype = c.type();
       const irep_idt &name = c.get_name();
@@ -1212,10 +1211,10 @@ void value_sett::assign(
           "rhs.type():\n" +
             rhs.type().pretty() + "\n" + "lhs.type():\n" + lhs.type().pretty());
 
-        const struct_union_typet &rhs_struct_union_type =
-          to_struct_union_type(ns.follow(rhs.type()));
+        const struct_typet &rhs_struct_type =
+          to_struct_type(ns.follow(rhs.type()));
 
-        const typet &rhs_subtype = rhs_struct_union_type.component_type(name);
+        const typet &rhs_subtype = rhs_struct_type.component_type(name);
         rhs_member = simplify_expr(member_exprt{rhs, name, rhs_subtype}, ns);
 
         assign(lhs_member, rhs_member, ns, true, add_to_sets);
@@ -1284,7 +1283,7 @@ void value_sett::assign(
   }
   else
   {
-    // basic type
+    // basic type or union
     object_mapt values_rhs = get_value_set(rhs, ns, is_simplified);
 
     // Permit custom subclass to alter the read values prior to write: