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 {
+    unsigned 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

@@ -38,15 +38,15 @@ bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
 
 bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 {
+  const std::size_t width = boolbv_width(expr.type());
+
   // 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()) || width == 0)
   {
     return convert_bv(lower_byte_extract(expr, ns));
   }
 
-  const std::size_t width = boolbv_width(expr.type());
-
   // special treatment for bit-fields and big-endian:
   // we need byte granularity
   #if 0
@@ -63,9 +63,6 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   }
   #endif
 
-  if(width==0)
-    return conversion_failed(expr);
-
   // see if the byte number is constant and within bounds, else work from the
   // root object
   const auto op_bytes_opt = pointer_offset_size(expr.op().type(), ns);

src/solvers/flattening/boolbv_union.cpp

@@ -17,18 +17,15 @@ bvt boolbvt::convert_union(const union_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
-  if(width==0)
-    return conversion_failed(expr);
-
   const bvt &op_bv=convert_bv(expr.op());
 
   INVARIANT(
-    op_bv.size() <= width,
+    width == 0 || op_bv.size() <= width,
     "operand bitvector width shall not be larger than the width indicated by "
     "the union type");
 
   bvt bv;
-  bv.resize(width);
+  bv.resize(std::max(width, op_bv.size()));
 
   if(config.ansi_c.endianness==configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN)
   {