Merge pull request #5713 from tautschnig/value-set-union

Value sets must not be field sensitive for unions

Author: tautschnig

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.

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 */
+}

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.

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: