Byte-operator lowering: Add support for byte-extracting unions

We already had support for structs, arrays, vectors in place; add unions
following the same approach. This is required for some SV-COMP device
driver benchmarks, including
ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--scsi--qla2xxx--tcm_qla2xxx.ko-entry_point.cil.out.i
Adding a test also made apparent that we weren't yet handling unbounded
byte extracts (out of a bounded object) in flattening.

Author: tautschnig

regression/cbmc/union14/main.c

@@ -0,0 +1,13 @@
+int main()
+{
+  unsigned x;
+  __CPROVER_assume(x > 0);
+  union U {
+    char A[x];
+  };
+  int i, i_before;
+  i_before = i;
+  union U u = *((union U *)&i);
+  i = u.A[0];
+  __CPROVER_assert(i == i_before, "going through union works");
+}

regression/cbmc/union14/test.desc

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

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -43,7 +43,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 {
   // array logic does not handle byte operators, thus lower when operating on
   // unbounded arrays
-  if(is_unbounded_array(expr.op().type()))
+  if(is_unbounded_array(expr.op().type()) || is_unbounded_array(expr.type()))
   {
     try
     {

src/solvers/lowering/byte_operators.cpp

@@ -108,6 +108,46 @@ static struct_exprt bv_to_struct_expr(
   return struct_exprt{std::move(operands), struct_type};
 }
 
+/// Convert a bitvector-typed expression \p bitvector_expr to a union-typed
+/// expression. See \ref bv_to_expr for an overview.
+static union_exprt bv_to_union_expr(
+  const exprt &bitvector_expr,
+  const union_typet &union_type,
+  const endianness_mapt &endianness_map,
+  const namespacet &ns)
+{
+  const union_typet::componentst &components = union_type.components();
+
+  if(components.empty())
+  {
+    // deal with empty unions the same way zero_initializer does
+    return union_exprt{irep_idt{}, nil_exprt{}, union_type};
+  }
+
+  // we will use the first component, unless we can find a member that
+  // definitively is larger
+  mp_integer max_width = 0;
+  typet max_comp_type = components.front().type();
+  irep_idt max_comp_name = components.front().get_name();
+
+  for(const auto &comp : components)
+  {
+    auto element_width = pointer_offset_bits(comp.type(), ns);
+
+    if(!element_width.has_value() || *element_width <= max_width)
+      continue;
+
+    max_width = *element_width;
+    max_comp_type = comp.type();
+    max_comp_name = comp.get_name();
+  }
+
+  return union_exprt{
+    std::move(max_comp_name),
+    bv_to_expr(bitvector_expr, max_comp_type, endianness_map, ns),
+    union_type};
+}
+
 /// Convert a bitvector-typed expression \p bitvector_expr to an array-typed
 /// expression. See \ref bv_to_expr for an overview.
 static array_exprt bv_to_array_expr(
@@ -296,6 +336,21 @@ static exprt bv_to_expr(
     result.type() = target_type;
     return std::move(result);
   }
+  else if(target_type.id() == ID_union)
+  {
+    return bv_to_union_expr(
+      bitvector_expr, to_union_type(target_type), endianness_map, ns);
+  }
+  else if(target_type.id() == ID_union_tag)
+  {
+    union_exprt result = bv_to_union_expr(
+      bitvector_expr,
+      ns.follow_tag(to_union_tag_type(target_type)),
+      endianness_map,
+      ns);
+    result.type() = target_type;
+    return std::move(result);
+  }
   else if(target_type.id() == ID_array)
   {
     return bv_to_array_expr(