Merge pull request #7250 from tautschnig/feature/simp-empty

Simplify byte extract of empty union or struct

Author: tautschnig

src/solvers/smt2/smt2_conv.cpp

@@ -965,12 +965,17 @@ static bool is_zero_width(const typet &type, const namespacet &ns)
     return true;
   else if(type.id() == ID_struct_tag)
     return is_zero_width(ns.follow_tag(to_struct_tag_type(type)), ns);
-  else if(type.id() == ID_struct)
-    return to_struct_type(type).components().empty();
   else if(type.id() == ID_union_tag)
     return is_zero_width(ns.follow_tag(to_union_tag_type(type)), ns);
-  else if(type.id() == ID_union)
-    return to_union_type(type).components().empty();
+  else if(type.id() == ID_struct || type.id() == ID_union)
+  {
+    for(const auto &comp : to_struct_union_type(type).components())
+    {
+      if(!is_zero_width(comp.type(), ns))
+        return false;
+    }
+    return true;
+  }
   else
     return false;
 }

src/util/simplify_expr.cpp

@@ -1705,6 +1705,19 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
     }
   }
 
+  if(
+    (expr.type().id() == ID_union || expr.type().id() == ID_union_tag) &&
+    to_union_type(ns.follow(expr.type())).components().empty())
+  {
+    return empty_union_exprt{expr.type()};
+  }
+  else if(
+    (expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag) &&
+    to_struct_type(ns.follow(expr.type())).components().empty())
+  {
+    return struct_exprt{{}, expr.type()};
+  }
+
   // no proper simplification for expr.type()==void
   // or types of unknown size
   if(!el_size.has_value() || *el_size == 0)

src/util/simplify_utils.cpp

@@ -264,6 +264,9 @@ optionalt<exprt> bits2expr(
     const union_typet &union_type = to_union_type(type);
     const union_typet::componentst &components = union_type.components();
 
+    if(components.empty() && bits.empty())
+      return empty_union_exprt{type};
+
     for(const auto &component : components)
     {
       auto val = bits2expr(bits, component.type(), little_endian, ns);