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

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -108,6 +108,40 @@ 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();
+
+  mp_integer max_width = 0;
+  typet max_comp_type;
+  irep_idt max_comp_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();
+  }
+
+  exprt operand = nil_exprt{};
+
+  if(max_width > 0)
+    operand = bv_to_expr(bitvector_expr, max_comp_type, endianness_map, ns);
+
+  return union_exprt{std::move(max_comp_name), std::move(operand), 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 +330,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(