boolbv_width: distinguish zero from unknown size

Use optionalt to distinguish types of known-zero size from those with
unknown size, which previously had the default value of zero.

This makes it possible to support index expressions over zero bitwidth
arrays without mistaking the situation for an unknown size. (There is
not really anything wrong in having empty bitvectors, which we otherwise
already support (as of e021eef).)

Author: tautschnig

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);