Simplify byte-extract from struct or union expressions

With rewrite_union introducing rewriting union accesses to byte-extract
operations, simplifying such expressions must cover as many cases as
possible. Constants were mostly already being rewritten via expr2bits,
but that wouldn't be able to handle expressions involving pointers (even
when they are effectively constants when using address-of operations).
The additional simplification rules mimic what lower_byte_extract
already did at a later stage, but such late rewrites would not benefit
constant propagation done by goto-symex.

Author: tautschnig

regression/cbmc/simplify-union/main.c

@@ -0,0 +1,49 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct O
+{
+  char *ptr;
+  unsigned len;
+};
+
+struct E
+{
+  int e;
+};
+
+union U {
+  struct O ok;
+  struct E err;
+};
+
+struct S
+{
+  union U u;
+  _Bool success;
+};
+
+void alloc(struct S *s, unsigned size)
+{
+  char *p = malloc(sizeof(char) * size);
+  if(p != 0)
+  {
+    s->u.ok = (struct O){p, size};
+    s->success = 1;
+  }
+  else
+  {
+    s->success = 0;
+  }
+}
+
+int main()
+{
+  struct S s;
+  alloc(&s, 2);
+  if(s.success)
+  {
+    assert(s.u.ok.len == 2);
+    s.u.ok.ptr = "a";
+  }
+}

regression/cbmc/simplify-union/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^Generated 1 VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The len member should constant propagate with the help of simplification.

scripts/expected_doxygen_warnings.txt

@@ -92,7 +92,7 @@ warning: Included by graph for 'invariant.h' not generated, too many nodes (187)
 warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'namespace.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (101), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (102), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/pointer-analysis/value_set.cpp

@@ -784,6 +784,11 @@ void value_sett::get_value_set_rec(
         get_value_set_rec(*it, dest, suffix, original_type, ns);
     }
   }
+  else if(expr.id() == ID_union)
+  {
+    get_value_set_rec(
+      to_union_expr(expr).op(), dest, suffix, original_type, ns);
+  }
   else if(expr.id()==ID_with)
   {
     const with_exprt &with_expr = to_with_expr(expr);

src/util/pointer_offset_size.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include "c_types.h"
 #include "invariant.h"
 #include "namespace.h"
+#include "pointer_expr.h"
 #include "simplify_expr.h"
 #include "ssa_expr.h"
 #include "std_expr.h"
@@ -681,6 +682,27 @@ optionalt<exprt> get_subexpression_at_offset(
       }
     }
   }
+  else if(
+    object_descriptor_exprt(expr).root_object().id() == ID_union &&
+    source_type.id() == ID_union)
+  {
+    const union_typet &union_type = to_union_type(source_type);
+
+    for(const auto &component : union_type.components())
+    {
+      const auto m_size_bits = pointer_offset_bits(component.type(), ns);
+      if(!m_size_bits.has_value())
+        continue;
+
+      // if this member completely contains the target, recurse into it
+      if(offset_bytes * 8 + *target_size_bits <= *m_size_bits)
+      {
+        const member_exprt member(expr, component.get_name(), component.type());
+        return get_subexpression_at_offset(
+          member, offset_bytes, target_type_raw, ns);
+      }
+    }
+  }
 
   return byte_extract_exprt(
     byte_extract_id(),

src/util/simplify_expr.cpp

@@ -1709,6 +1709,71 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
       return std::move(*tmp);
   }
 
+  // push byte extracts into struct or union expressions, just like
+  // lower_byte_extract does (this is the same code, except recursive calls use
+  // simplify rather than lower_byte_extract)
+  if(expr.op().id() == ID_struct || expr.op().id() == ID_union)
+  {
+    if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
+    {
+      const struct_typet &struct_type = to_struct_type(ns.follow(expr.type()));
+      const struct_typet::componentst &components = struct_type.components();
+
+      bool failed = false;
+      struct_exprt s({}, expr.type());
+
+      for(const auto &comp : components)
+      {
+        auto component_bits = pointer_offset_bits(comp.type(), ns);
+
+        // the next member would be misaligned, abort
+        if(
+          !component_bits.has_value() || *component_bits == 0 ||
+          *component_bits % 8 != 0)
+        {
+          failed = true;
+          break;
+        }
+
+        auto member_offset_opt =
+          member_offset_expr(struct_type, comp.get_name(), ns);
+
+        if(!member_offset_opt.has_value())
+        {
+          failed = true;
+          break;
+        }
+
+        exprt new_offset = simplify_rec(
+          plus_exprt{expr.offset(),
+                     typecast_exprt::conditional_cast(
+                       member_offset_opt.value(), expr.offset().type())});
+
+        byte_extract_exprt tmp = expr;
+        tmp.type() = comp.type();
+        tmp.offset() = new_offset;
+
+        s.add_to_operands(simplify_byte_extract(tmp));
+      }
+
+      if(!failed)
+        return s;
+    }
+    else if(expr.type().id() == ID_union || expr.type().id() == ID_union_tag)
+    {
+      const union_typet &union_type = to_union_type(ns.follow(expr.type()));
+      auto widest_member_opt = union_type.find_widest_union_component(ns);
+      if(widest_member_opt.has_value())
+      {
+        byte_extract_exprt be = expr;
+        be.type() = widest_member_opt->first.type();
+        return union_exprt{widest_member_opt->first.get_name(),
+                           simplify_byte_extract(be),
+                           expr.type()};
+      }
+    }
+  }
+
   // try to refine it down to extracting from a member or an index in an array
   auto subexpr =
     get_subexpression_at_offset(expr.op(), *offset, expr.type(), ns);