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
+  unsigned u = ((union U *)&i)->A[0];
+  // reading back an integer out of the union should yield the same value for
+  // the integer as it had before
+  i = u;
+  __CPROVER_assert(i == i_before, "going through union works");
+}

regression/cbmc/union17/test.desc

@@ -0,0 +1,12 @@
+KNOWNBUG
+main.c
+--no-simplify
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test passes when simplification is enabled (which gets rid of
+byte-extracting a union of non-constant size), but yields the wrong verification
+outcome with both the SAT and SMT back-end otherwise.

src/solvers/flattening/boolbv.cpp

@@ -8,23 +8,25 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <algorithm>
-
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/floatbv_expr.h>
 #include <util/magic.h>
 #include <util/mp_arith.h>
+#include <util/namespace.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
 #include <util/string_constant.h>
 
 #include <solvers/floatbv/float_utils.h>
 
+#include <algorithm>
+
 endianness_mapt boolbvt::endianness_map(const typet &type) const
 {
   const bool little_endian =
@@ -534,6 +536,38 @@ bool boolbvt::is_unbounded_array(const typet &type) const
   return false;
 }
 
+bool boolbvt::has_unbounded_array(const typet &type) const
+{
+  if(type.id() == ID_struct_tag)
+    return has_unbounded_array(ns.follow_tag(to_struct_tag_type(type)));
+  else if(type.id() == ID_union_tag)
+    return has_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(has_unbounded_array(component.type()))
+        return true;
+    }
+
+    return false;
+  }
+  else if(type.id() == ID_union)
+  {
+    for(const auto &component : to_union_type(type).components())
+    {
+      if(has_unbounded_array(component.type()))
+        return true;
+    }
+
+    return false;
+  }
+  else if(type.id() != ID_array)
+    return false;
+
+  return is_unbounded_array(type);
+}
+
 binding_exprt::variablest boolbvt::fresh_binding(const binding_exprt &binding)
 {
   // to ensure freshness of the new identifiers

src/solvers/flattening/boolbv.h

@@ -251,6 +251,7 @@ class boolbvt:public arrayst
 
   // unbounded arrays
   bool is_unbounded_array(const typet &type) const override;
+  bool has_unbounded_array(const typet &type) const;
 
   // quantifier instantiations
   class quantifiert

src/solvers/flattening/boolbv_array.cpp

@@ -15,22 +15,18 @@ Author: Daniel Kroening, [email protected]
 /// Return an empty vector if the width is zero or the array has no elements.
 bvt boolbvt::convert_array(const exprt &expr)
 {
-  const std::size_t width = boolbv_width(expr.type());
   const exprt::operandst &operands = expr.operands();
 
-  if(operands.empty() && width == 0)
+  if(operands.empty())
     return bvt();
 
   if(expr.type().id()==ID_array)
   {
-    DATA_INVARIANT(
-      expr.has_operands(),
-      "the bit width being nonzero implies that the array has a nonzero size "
-      "in which case the array shall have operands");
-    const std::size_t op_width = width / operands.size();
+    const std::size_t op_width =
+      boolbv_width(to_array_type(expr.type()).element_type());
 
     bvt bv;
-    bv.reserve(width);
+    bv.reserve(op_width * operands.size());
 
     for(const auto &op : operands)
     {

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(
+    has_unbounded_array(expr.op().type()) || has_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_byte_update.cpp

@@ -19,8 +19,8 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
   // if we update (from) an unbounded array, lower the expression as the array
   // logic does not handle byte operators
   if(
-    is_unbounded_array(expr.op().type()) ||
-    is_unbounded_array(expr.value().type()))
+    has_unbounded_array(expr.op().type()) ||
+    has_unbounded_array(expr.value().type()))
   {
     return convert_bv(lower_byte_update(expr, ns));
   }

src/solvers/flattening/boolbv_union.cpp

@@ -10,17 +10,19 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_union(const union_exprt &expr)
 {
-  std::size_t width=boolbv_width(expr.type());
-
   const bvt &op_bv=convert_bv(expr.op());
 
+  const auto &width_opt = bv_width.get_width_opt(expr.type());
+  if(!width_opt.has_value())
+    return op_bv;
+
   INVARIANT(
-    op_bv.size() <= width,
+    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);
+  bv.resize(*width_opt);
 
   endianness_mapt map_u = endianness_map(expr.type());
   endianness_mapt map_op = endianness_map(expr.op().type());