Improve precision of value_set on unions by extending and using the simplifier

Author: Daniel Kroening

regression/cbmc/union11/union_list.c

@@ -0,0 +1,30 @@
+#include <assert.h>
+
+struct list_item
+{
+  struct list_item *previous;
+};
+
+struct List
+{
+  unsigned something;
+  struct list_item *index;
+  struct list_item end;
+};
+
+union U
+{
+  struct List my_list;
+};
+
+int main()
+{
+  union U u;
+
+  u.my_list.index = &(u.my_list.end);
+  u.my_list.end.previous = u.my_list.index;
+  struct list_item *p1 = u.my_list.index;
+  struct list_item *p2 = p1->previous;
+  struct list_item *p3 = p2->previous;
+  assert(p3 != 0); // should pass
+}

regression/cbmc/union11/union_list.desc

@@ -0,0 +1,8 @@
+CORE
+union_list.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/pointer-analysis/value_set.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/base_type.h>
+#include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
@@ -1203,9 +1204,9 @@ void value_sett::assign(
                 "type:\n"+type.pretty();
 
         rhs_member=make_member(rhs, name, ns);
-
-        assign(lhs_member, rhs_member, ns, is_simplified, add_to_sets);
       }
+
+      assign(lhs_member, rhs_member, ns, false, add_to_sets);
     }
   }
   else if(type.id()==ID_array)
@@ -1756,7 +1757,7 @@ exprt value_sett::make_member(
   }
 
   // give up
-  typet subtype=struct_union_type.component_type(component_name);
+  const typet subtype = struct_union_type.component_type(component_name);
   member_exprt member_expr(src, component_name, subtype);
 
   return member_expr;

src/util/simplify_expr_struct.cpp

@@ -172,6 +172,25 @@ bool simplify_exprt::simplify_member(exprt &expr)
 
       return false;
     }
+    else if(op_type.id() == ID_union)
+    {
+      // rewrite byte_extract(X, 0).member to X
+      // if the type of X is that of the member
+      const auto &byte_extract_expr = to_byte_extract_expr(op);
+      if(byte_extract_expr.offset().is_zero())
+      {
+        const union_typet &union_type = to_union_type(op_type);
+        const typet subtype = union_type.component_type(component_name);
+
+        if(subtype == byte_extract_expr.op().type())
+        {
+          exprt tmp = byte_extract_expr.op();
+          expr.swap(tmp);
+
+          return false;
+        }
+      }
+    }
   }
   else if(op.id()==ID_union && op_type.id()==ID_union)
   {