Use byte-operator lowering when type to be extract is of non-const size

The test included made apparent that we weren't yet handling unbounded
byte extracts (out of a bounded object) in flattening.

Author: tautschnig

regression/cbmc/union17/main.c

@@ -0,0 +1,19 @@
+int main()
+{
+  // create a union type of non-constant, non-zero size
+  unsigned x;
+  __CPROVER_assume(x > 0);
+  union U
+  {
+    unsigned A[x];
+  };
+  // create an integer of arbitrary value
+  int i, i_before;
+  i_before = i;
+  // initialize a union of non-zero size from the integer
+  union U u = *((union U *)&i);
+  // reading back an integer out of the union should yield the same value for
+  // the integer as it had before
+  i = u.A[0];
+  __CPROVER_assert(i == i_before, "going through union works");
+}

regression/cbmc/union17/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Value sets did not properly track pointers through unions. Thus derferencing
+yields __CPROVER_memory, which results in a spurious verification failure.

src/solvers/flattening/boolbv.cpp

@@ -517,7 +517,31 @@ void boolbvt::set_to(const exprt &expr, bool value)
 
 bool boolbvt::is_unbounded_array(const typet &type) const
 {
-  if(type.id()!=ID_array)
+  if(type.id() == ID_struct_tag)
+    return is_unbounded_array(ns.follow_tag(to_struct_tag_type(type)));
+  else if(type.id() == ID_union_tag)
+    return is_unbounded_array(ns.follow_tag(to_union_tag_type(type)));
+  else if(type.id() == ID_struct)
+  {
+    for(const auto &component : to_struct_type(type).components())
+    {
+      if(is_unbounded_array(component.type()))
+        return true;
+    }
+
+    return false;
+  }
+  else if(type.id() == ID_union)
+  {
+    for(const auto &component : to_union_type(type).components())
+    {
+      if(is_unbounded_array(component.type()))
+        return true;
+    }
+
+    return false;
+  }
+  else if(type.id() != ID_array)
     return false;
 
   if(unbounded_array==unbounded_arrayt::U_ALL)

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -34,14 +34,18 @@ bvt map_bv(const endianness_mapt &map, const bvt &src)
 
 bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 {
+  const auto &width_opt = bv_width.get_width_opt(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_opt.has_value())
   {
     return convert_bv(lower_byte_extract(expr, ns));
   }
 
-  const std::size_t width = boolbv_width(expr.type());
+  const std::size_t width = *width_opt;
 
   // special treatment for bit-fields and big-endian:
   // we need byte granularity

src/solvers/flattening/boolbv_union.cpp

@@ -10,17 +10,20 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_union(const union_exprt &expr)
 {
-  std::size_t width=boolbv_width(expr.type());
+  const auto &width_opt = bv_width.get_width_opt(expr.type());
 
   const bvt &op_bv=convert_bv(expr.op());
 
   INVARIANT(
-    op_bv.size() <= width,
+    !width_opt.has_value() || op_bv.size() <= *width_opt,
     "operand bitvector width shall not be larger than the width indicated by "
     "the union type");
 
   bvt bv;
-  bv.resize(width);
+  if(width_opt.has_value())
+    bv.resize(*width_opt);
+  else
+    bv.resize(op_bv.size());
 
   endianness_mapt map_u = endianness_map(expr.type());
   endianness_mapt map_op = endianness_map(expr.op().type());