Handle empty unions via dedicated expression

regression/cbmc/Union_Initialization2/main.c

@@ -0,0 +1,14 @@
+union U {
+};
+
+struct S
+{
+  int a;
+  union U u;
+  int b;
+} s;
+
+int main()
+{
+  __CPROVER_assert(0, "");
+}

regression/cbmc/Union_Initialization2/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+^Invariant check failed

src/solvers/flattening/boolbv.cpp

@@ -183,6 +183,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
     return convert_struct(to_struct_expr(expr));
   else if(expr.id()==ID_union)
     return convert_union(to_union_expr(expr));
+  else if(expr.id() == ID_empty_union)
+    return convert_empty_union(to_empty_union_expr(expr));
   else if(expr.id()==ID_string_constant)
     return convert_bitvector(
       to_string_constant(expr).to_array_expr());

src/solvers/flattening/boolbv.h

@@ -162,6 +162,7 @@ class boolbvt:public arrayst
   virtual bvt convert_let(const let_exprt &);
   virtual bvt convert_array_of(const array_of_exprt &expr);
   virtual bvt convert_union(const union_exprt &expr);
+  virtual bvt convert_empty_union(const empty_union_exprt &expr);
   virtual bvt convert_bv_typecast(const typecast_exprt &expr);
   virtual bvt convert_add_sub(const exprt &expr);
   virtual bvt convert_mult(const mult_exprt &expr);

src/solvers/flattening/boolbv_get.cpp

@@ -139,7 +139,8 @@ exprt boolbvt::bv_get_rec(
       const union_typet &union_type=to_union_type(type);
       const union_typet::componentst &components=union_type.components();
 
-      assert(!components.empty());
+      if(components.empty())
+        return empty_union_exprt(type);
 
       // Any idea that's better than just returning the first component?
       std::size_t component_nr=0;

src/solvers/flattening/boolbv_union.cpp

@@ -37,3 +37,8 @@ bvt boolbvt::convert_union(const union_exprt &expr)
 
   return bv;
 }
+
+bvt boolbvt::convert_empty_union(const empty_union_exprt &expr)
+{
+  return {};
+}

src/solvers/smt2/smt2_conv.cpp

@@ -2126,6 +2126,10 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     convert_expr(simplify_expr(to_count_trailing_zeros_expr(expr).lower(), ns));
   }
+  else if(expr.id() == ID_empty_union)
+  {
+    out << "()";
+  }
   else
     INVARIANT_WITH_DIAGNOSTICS(
       false,
@@ -4403,7 +4407,9 @@ void smt2_convt::set_to(const exprt &expr, bool value)
   if(expr.id() == ID_equal && value)
   {
     const equal_exprt &equal_expr=to_equal_expr(expr);
-    if(equal_expr.lhs().type().id() == ID_empty)
+    if(
+      equal_expr.lhs().type().id() == ID_empty ||
+      equal_expr.rhs().id() == ID_empty_union)
     {
       // ignore equality checking over expressions with empty (void) type
       return;
@@ -4891,7 +4897,9 @@ void smt2_convt::convert_type(const typet &type)
   else if(type.id() == ID_union || type.id() == ID_union_tag)
   {
     std::size_t width=boolbv_width(type);
-    CHECK_RETURN_WITH_DIAGNOSTICS(width != 0, "failed to get width of union");
+    CHECK_RETURN_WITH_DIAGNOSTICS(
+      to_union_type(ns.follow(type)).components().empty() || width != 0,
+      "failed to get width of union");
 
     out << "(_ BitVec " << width << ")";
   }

src/util/expr_initializer.cpp

@@ -208,51 +208,29 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
   }
   else if(type_id==ID_union)
   {
-    const union_typet::componentst &components=
-      to_union_type(type).components();
+    const union_typet &union_type = to_union_type(type);
 
-    union_typet::componentt component;
-    bool found=false;
-    mp_integer component_size=0;
-
-    // we need to find the largest member
-
-    for(const auto &c : components)
-    {
-      // skip methods
-      if(c.type().id() == ID_code)
-        continue;
-
-      auto bits = pointer_offset_bits(c.type(), ns);
-
-      if(bits.has_value() && *bits > component_size)
-      {
-        component = c;
-        found=true;
-        component_size = *bits;
-      }
-    }
-
-    if(!found)
+    if(union_type.components().empty())
     {
-      // stupid empty union
-      union_exprt value(irep_idt(), nil_exprt(), type);
+      empty_union_exprt value{type};
       value.add_source_location() = source_location;
       return std::move(value);
     }
-    else
-    {
-      auto component_value =
-        expr_initializer_rec(component.type(), source_location);
 
-      if(!component_value.has_value())
-        return {};
+    const auto &widest_member = union_type.find_widest_union_component(ns);
+    if(!widest_member.has_value())
+      return {};
 
-      union_exprt value(component.get_name(), *component_value, type);
-      value.add_source_location() = source_location;
+    auto component_value =
+      expr_initializer_rec(widest_member->first.type(), source_location);
 
-      return std::move(value);
-    }
+    if(!component_value.has_value())
+      return {};
+
+    union_exprt value{widest_member->first.get_name(), *component_value, type};
+    value.add_source_location() = source_location;
+
+    return std::move(value);
   }
   else if(type_id==ID_c_enum_tag)
   {

src/util/irep_ids.def

@@ -862,6 +862,7 @@ IREP_ID_TWO(vector_gt, vector->)
 IREP_ID_TWO(vector_lt, vector-<)
 IREP_ID_ONE(shuffle_vector)
 IREP_ID_ONE(count_trailing_zeros)
+IREP_ID_ONE(empty_union)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree

src/util/std_expr.h

@@ -1662,6 +1662,51 @@ inline union_exprt &to_union_expr(exprt &expr)
   return ret;
 }
 
+/// \brief Union constructor to support unions without any member (a GCC/Clang
+/// feature).
+class empty_union_exprt : public nullary_exprt
+{
+public:
+  explicit empty_union_exprt(typet _type)
+    : nullary_exprt(ID_empty_union, std::move(_type))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<empty_union_exprt>(const exprt &base)
+{
+  return base.id() == ID_empty_union;
+}
+
+inline void validate_expr(const empty_union_exprt &value)
+{
+  validate_operands(
+    value, 0, "Empty-union constructor must not have any operand");
+}
+
+/// \brief Cast an exprt to an \ref empty_union_exprt
+///
+/// \a expr must be known to be \ref empty_union_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref empty_union_exprt
+inline const empty_union_exprt &to_empty_union_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_empty_union);
+  const empty_union_exprt &ret = static_cast<const empty_union_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_empty_union_expr(const exprt &)
+inline empty_union_exprt &to_empty_union_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_empty_union);
+  empty_union_exprt &ret = static_cast<empty_union_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
 
 /// \brief Struct constructor from list of elements
 class struct_exprt : public multi_ary_exprt