boolbv_width: distinguish zero from unknown size

regression/cbmc/dynamic_sizeof1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-z3-smt-backend
 main.c
 
 ^EXIT=0$

regression/cbmc/vla1/test.desc

@@ -1,8 +1,11 @@
-CORE
+CORE broken-cprover-smt-backend
 main.c
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+The SMT back-end does not correctly support structs with non-constant size,
+unless named data types are used (as is the case with Z3).

src/solvers/flattening/boolbv.cpp

@@ -242,22 +242,16 @@ bvt boolbvt::convert_array_comprehension(const array_comprehension_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
-  if(width==0)
-    return conversion_failed(expr);
-
   const exprt &array_size = expr.type().size();
 
-  const auto size = numeric_cast<mp_integer>(array_size);
-
-  if(!size.has_value())
-    return conversion_failed(expr);
+  const auto size = numeric_cast_v<mp_integer>(to_constant_expr(array_size));
 
   typet counter_type = expr.arg().type();
 
   bvt bv;
   bv.resize(width);
 
-  for(mp_integer i = 0; i < *size; ++i)
+  for(mp_integer i = 0; i < size; ++i)
   {
     exprt counter=from_integer(i, counter_type);
 
@@ -266,7 +260,7 @@ bvt boolbvt::convert_array_comprehension(const array_comprehension_exprt &expr)
     const bvt &tmp = convert_bv(body);
 
     INVARIANT(
-      *size * tmp.size() == width,
+      size * tmp.size() == width,
       "total bitvector width shall equal the number of operands times the size "
       "per operand");
 
@@ -521,12 +515,12 @@ bool boolbvt::is_unbounded_array(const typet &type) const
   if(unbounded_array==unbounded_arrayt::U_ALL)
     return true;
 
-  const std::size_t size = boolbv_width(type);
-  if(size == 0)
+  const auto &size_opt = bv_width.get_width_opt(type);
+  if(!size_opt.has_value())
     return true;
 
   if(unbounded_array==unbounded_arrayt::U_AUTO)
-    if(size > MAX_FLATTENED_ARRAY_SIZE)
+    if(*size_opt > MAX_FLATTENED_ARRAY_SIZE)
       return true;
 
   return false;

src/solvers/flattening/boolbv_abs.cpp

@@ -16,11 +16,6 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_abs(const abs_exprt &expr)
 {
-  const std::size_t width = boolbv_width(expr.type());
-
-  if(width==0)
-    return conversion_failed(expr);
-
   const bvt &op_bv=convert_bv(expr.op());
 
   if(expr.op().type()!=expr.type())

src/solvers/flattening/boolbv_add_sub.cpp

@@ -32,9 +32,6 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
   std::size_t width=boolbv_width(type);
 
-  if(width==0)
-    return conversion_failed(expr);
-
   const exprt::operandst &operands=expr.operands();
 
   DATA_INVARIANT(
@@ -160,9 +157,6 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
 
   std::size_t width = boolbv_width(type);
 
-  if(width == 0)
-    return conversion_failed(expr);
-
   DATA_INVARIANT(
     expr.lhs().type() == type && expr.rhs().type() == type,
     "saturating add/sub with mixed types:\n" + expr.pretty());

src/solvers/flattening/boolbv_array_of.cpp

@@ -24,28 +24,17 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
     return conversion_failed(expr);
 
   std::size_t width=boolbv_width(array_type);
-
-  if(width==0)
-  {
-    // A zero-length array is acceptable;
-    // an element with unknown size is not.
-    if(boolbv_width(array_type.element_type()) == 0)
-      return conversion_failed(expr);
-    else
-      return bvt();
-  }
+  if(width == 0)
+    return bvt{};
 
   const exprt &array_size=array_type.size();
 
-  const auto size = numeric_cast<mp_integer>(array_size);
-
-  if(!size.has_value())
-    return conversion_failed(expr);
+  const auto size = numeric_cast_v<mp_integer>(to_constant_expr(array_size));
 
   const bvt &tmp = convert_bv(expr.what());
 
   INVARIANT(
-    *size * tmp.size() == width,
+    size * tmp.size() == width,
     "total array bit width shall equal the number of elements times the "
     "element bit with");
 

src/solvers/flattening/boolbv_bitreverse.cpp

@@ -13,8 +13,6 @@ Author: Michael Tautschnig
 bvt boolbvt::convert_bitreverse(const bitreverse_exprt &expr)
 {
   const std::size_t width = boolbv_width(expr.type());
-  if(width == 0)
-    return conversion_failed(expr);
 
   bvt bv = convert_bv(expr.op(), width);
 

src/solvers/flattening/boolbv_bitwise.cpp

@@ -13,8 +13,6 @@ Author: Daniel Kroening, [email protected]
 bvt boolbvt::convert_bitwise(const exprt &expr)
 {
   const std::size_t width = boolbv_width(expr.type());
-  if(width==0)
-    return conversion_failed(expr);
 
   if(expr.id()==ID_bitnot)
   {

src/solvers/flattening/boolbv_case.cpp

@@ -18,9 +18,6 @@ bvt boolbvt::convert_case(const exprt &expr)
 
   std::size_t width=boolbv_width(expr.type());
 
-  if(width==0)
-    return conversion_failed(expr);
-
   // make it free variables
   bvt bv = prop.new_variables(width);
 

src/solvers/flattening/boolbv_complex.cpp

@@ -14,9 +14,6 @@ bvt boolbvt::convert_complex(const complex_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
-  if(width==0)
-    return conversion_failed(expr);
-
   DATA_INVARIANT(
     expr.type().id() == ID_complex,
     "complex expression shall have complex type");
@@ -41,9 +38,6 @@ bvt boolbvt::convert_complex_real(const complex_real_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
-  if(width==0)
-    return conversion_failed(expr);
-
   bvt bv = convert_bv(expr.op(), width * 2);
 
   bv.resize(width); // chop
@@ -55,9 +49,6 @@ bvt boolbvt::convert_complex_imag(const complex_imag_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
-  if(width==0)
-    return conversion_failed(expr);
-
   bvt bv = convert_bv(expr.op(), width * 2);
 
   bv.erase(bv.begin(), bv.begin()+width);

src/solvers/flattening/boolbv_concatenation.cpp

@@ -15,9 +15,6 @@ bvt boolbvt::convert_concatenation(const concatenation_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
-  if(width==0)
-    return conversion_failed(expr);
-
   const exprt::operandst &operands=expr.operands();
 
   DATA_INVARIANT(

src/solvers/flattening/boolbv_cond.cpp

@@ -16,9 +16,6 @@ bvt boolbvt::convert_cond(const cond_exprt &expr)
 
   std::size_t width=boolbv_width(expr.type());
 
-  if(width==0)
-    return conversion_failed(expr);
-
   bvt bv;
 
   DATA_INVARIANT(operands.size() >= 2, "cond must have at least two operands");

src/solvers/flattening/boolbv_constant.cpp

@@ -14,9 +14,6 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
-  if(width==0)
-    return conversion_failed(expr);
-
   bvt bv;
   bv.resize(width);
 

src/solvers/flattening/boolbv_div.cpp

@@ -19,9 +19,6 @@ bvt boolbvt::convert_div(const div_exprt &expr)
 
   std::size_t width=boolbv_width(expr.type());
 
-  if(width==0)
-    return conversion_failed(expr);
-
   if(expr.op0().type().id()!=expr.type().id() ||
      expr.op1().type().id()!=expr.type().id())
     return conversion_failed(expr);

src/solvers/flattening/boolbv_extractbits.cpp

@@ -15,9 +15,6 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
 {
   const std::size_t bv_width = boolbv_width(expr.type());
 
-  if(bv_width == 0)
-    return conversion_failed(expr);
-
   auto const &src_bv = convert_bv(expr.src());
 
   auto const maybe_upper_as_int = numeric_cast<mp_integer>(expr.upper());

src/solvers/flattening/boolbv_get.cpp

@@ -48,12 +48,9 @@ exprt boolbvt::bv_get_rec(
   std::size_t offset,
   const typet &type) const
 {
-  std::size_t width=boolbv_width(type);
-
-  assert(bv.size()>=offset+width);
-
   if(type.id()==ID_bool)
   {
+    PRECONDITION(bv.size() > offset);
     // clang-format off
     switch(prop.l_get(bv[offset]).get_value())
     {
@@ -76,10 +73,14 @@ exprt boolbvt::bv_get_rec(
         return bv_get_unbounded_array(expr);
 
       const typet &subtype = array_type.element_type();
-      std::size_t sub_width=boolbv_width(subtype);
+      const auto &sub_width_opt = bv_width.get_width_opt(subtype);
 
-      if(sub_width!=0)
+      if(sub_width_opt.has_value() && *sub_width_opt > 0)
       {
+        const std::size_t width = boolbv_width(type);
+
+        std::size_t sub_width = *sub_width_opt;
+
         exprt::operandst op;
         op.reserve(width/sub_width);
 
@@ -131,9 +132,7 @@ exprt boolbvt::bv_get_rec(
         const member_exprt member{expr, c.get_name(), subtype};
         op.push_back(bv_get_rec(member, bv, offset + new_offset, subtype));
 
-        std::size_t sub_width = boolbv_width(subtype);
-        if(sub_width!=0)
-          new_offset+=sub_width;
+        new_offset += boolbv_width(subtype);
       }
 
       return struct_exprt(std::move(op), type);
@@ -160,9 +159,12 @@ exprt boolbvt::bv_get_rec(
     }
     else if(type.id()==ID_vector)
     {
+      const std::size_t width = boolbv_width(type);
+
       const auto &vector_type = to_vector_type(type);
       const typet &element_type = vector_type.element_type();
       std::size_t element_width = boolbv_width(element_type);
+      CHECK_RETURN(element_width > 0);
 
       if(element_width != 0 && width % element_width == 0)
       {
@@ -183,21 +185,25 @@ exprt boolbvt::bv_get_rec(
     }
     else if(type.id()==ID_complex)
     {
-      const typet &subtype = to_complex_type(type).subtype();
-      std::size_t sub_width=boolbv_width(subtype);
+      const std::size_t width = boolbv_width(type);
 
-      if(sub_width!=0 && width==sub_width*2)
-      {
-        const complex_exprt value(
-          bv_get_rec(complex_real_exprt{expr}, bv, 0 * sub_width, subtype),
-          bv_get_rec(complex_imag_exprt{expr}, bv, 1 * sub_width, subtype),
-          to_complex_type(type));
-
-        return value;
-      }
+      const typet &subtype = to_complex_type(type).subtype();
+      const std::size_t sub_width = boolbv_width(subtype);
+      CHECK_RETURN(sub_width > 0);
+      DATA_INVARIANT(
+        width == sub_width * 2,
+        "complex type has two elements of equal bit width");
+
+      return complex_exprt{
+        bv_get_rec(complex_real_exprt{expr}, bv, 0 * sub_width, subtype),
+        bv_get_rec(complex_imag_exprt{expr}, bv, 1 * sub_width, subtype),
+        to_complex_type(type)};
     }
   }
 
+  const std::size_t width = boolbv_width(type);
+  PRECONDITION(bv.size() >= offset + width);
+
   // most significant bit first
   std::string value;
 

src/solvers/flattening/boolbv_index.cpp

@@ -34,11 +34,6 @@ bvt boolbvt::convert_index(const index_exprt &expr)
     const array_typet &array_type=
       to_array_type(array_op_type);
 
-    std::size_t width=boolbv_width(expr.type());
-
-    if(width==0)
-      return conversion_failed(expr);
-
     // see if the array size is constant
 
     if(is_unbounded_array(array_type))
@@ -57,9 +52,11 @@ bvt boolbvt::convert_index(const index_exprt &expr)
         if(
           final_array.id() == ID_symbol || final_array.id() == ID_nondet_symbol)
         {
-          std::size_t width = boolbv_width(array_type);
+          const auto &array_width_opt = bv_width.get_width_opt(array_type);
           (void)map.get_literals(
-            final_array.get(ID_identifier), array_type, width);
+            final_array.get(ID_identifier),
+            array_type,
+            array_width_opt.value_or(0));
         }
 
         // make sure we have the index in the cache
@@ -68,15 +65,16 @@ bvt boolbvt::convert_index(const index_exprt &expr)
       else
       {
         // free variables
-        bv = prop.new_variables(width);
+        bv = prop.new_variables(boolbv_width(expr.type()));
 
         record_array_index(expr);
 
         // record type if array is a symbol
         if(array.id() == ID_symbol || array.id() == ID_nondet_symbol)
         {
-          std::size_t width = boolbv_width(array_type);
-          (void)map.get_literals(array.get(ID_identifier), array_type, width);
+          const auto &array_width_opt = bv_width.get_width_opt(array_type);
+          (void)map.get_literals(
+            array.get(ID_identifier), array_type, array_width_opt.value_or(0));
         }
 
         // make sure we have the index in the cache
@@ -208,6 +206,7 @@ bvt boolbvt::convert_index(const index_exprt &expr)
     // one or more of the above encoding strategies.
 
     // get literals for the whole array
+    const std::size_t width = boolbv_width(expr.type());
 
     const bvt &array_bv =
       convert_bv(array, numeric_cast_v<std::size_t>(array_size * width));
@@ -290,9 +289,6 @@ bvt boolbvt::convert_index(
 
   std::size_t width = boolbv_width(array_type.element_type());
 
-  if(width==0)
-    return conversion_failed(array);
-
   // TODO: If the underlying array can use one of the
   // improvements given above then it may be better to use
   // the array theory for short chains of updates and then