Merge pull request #6862 from tautschnig/cleanup/optional-size

boolbv_width: distinguish zero from unknown size

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, kroening@kroening.com
 
 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, kroening@kroening.com
 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);