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

@@ -85,8 +85,11 @@ bvt boolbvt::conversion_failed(const exprt &expr)
   ignoring(expr);
 
   // try to make it free bits
-  std::size_t width=boolbv_width(expr.type());
-  return prop.new_variables(width);
+  // TODO we likely end up in this path when an earlier call to boolbv_width
+  // failed
+  const auto &width_opt = boolbv_width(expr.type());
+  CHECK_RETURN(width_opt.has_value());
+  return prop.new_variables(*width_opt);
 }
 
 /// Converts an expression into its gate-level representation and returns a
@@ -234,11 +237,12 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
 
 bvt boolbvt::convert_array_comprehension(const array_comprehension_exprt &expr)
 {
-  std::size_t width=boolbv_width(expr.type());
-
-  if(width==0)
+  const auto &width_opt = boolbv_width(expr.type());
+  if(!width_opt.has_value())
     return conversion_failed(expr);
 
+  const std::size_t width = *width_opt;
+
   const exprt &array_size = expr.type().size();
 
   const auto size = numeric_cast<mp_integer>(array_size);
@@ -276,7 +280,9 @@ bvt boolbvt::convert_array_comprehension(const array_comprehension_exprt &expr)
 bvt boolbvt::convert_symbol(const exprt &expr)
 {
   const typet &type=expr.type();
-  std::size_t width=boolbv_width(type);
+  const auto &width_opt = boolbv_width(type);
+  CHECK_RETURN(width_opt.has_value());
+  const std::size_t width = *width_opt;
 
   const irep_idt &identifier = expr.get(ID_identifier);
   CHECK_RETURN(!identifier.empty());
@@ -304,7 +310,9 @@ bvt boolbvt::convert_function_application(
   functions.record(expr);
 
   // make it free bits
-  return prop.new_variables(boolbv_width(expr.type()));
+  const auto &width_opt = boolbv_width(expr.type());
+  CHECK_RETURN(width_opt.has_value());
+  return prop.new_variables(*width_opt);
 }
 
 
@@ -515,12 +523,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 = boolbv_width(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;
@@ -564,7 +572,9 @@ boolbvt::offset_mapt boolbvt::build_offset_map(const struct_typet &src)
   for(const auto &comp : components)
   {
     dest.push_back(offset);
-    offset += boolbv_width(comp.type());
+    const auto &comp_width_opt = boolbv_width(comp.type());
+    CHECK_RETURN(comp_width_opt.has_value());
+    offset += *comp_width_opt;
   }
   return dest;
 }

src/solvers/flattening/boolbv.h

@@ -98,7 +98,7 @@ class boolbvt:public arrayst
     return map;
   }
 
-  virtual std::size_t boolbv_width(const typet &type) const
+  virtual optionalt<std::size_t> boolbv_width(const typet &type) const
   {
     return bv_width(type);
   }

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

@@ -30,11 +30,12 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
      type.id()!=ID_vector)
     return conversion_failed(expr);
 
-  std::size_t width=boolbv_width(type);
-
-  if(width==0)
+  const auto &width_opt = boolbv_width(type);
+  if(!width_opt.has_value())
     return conversion_failed(expr);
 
+  const std::size_t width = *width_opt;
+
   const exprt::operandst &operands=expr.operands();
 
   DATA_INVARIANT(
@@ -73,8 +74,10 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
     if(type.id()==ID_vector || type.id()==ID_complex)
     {
-      std::size_t sub_width =
+      const auto &sub_width_opt =
         boolbv_width(to_type_with_subtype(type).subtype());
+      CHECK_RETURN(sub_width_opt.has_value());
+      const std::size_t sub_width = *sub_width_opt;
 
       INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
       INVARIANT(
@@ -158,11 +161,12 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
     return conversion_failed(expr);
   }
 
-  std::size_t width = boolbv_width(type);
-
-  if(width == 0)
+  const auto &width_opt = boolbv_width(type);
+  if(!width_opt.has_value())
     return conversion_failed(expr);
 
+  const std::size_t width = *width_opt;
+
   DATA_INVARIANT(
     expr.lhs().type() == type && expr.rhs().type() == type,
     "saturating add/sub with mixed types:\n" + expr.pretty());
@@ -184,7 +188,10 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
   if(type.id() != ID_vector && type.id() != ID_complex)
     return bv_utils.saturating_add_sub(bv, op, subtract, rep);
 
-  std::size_t sub_width = boolbv_width(to_type_with_subtype(type).subtype());
+  const auto &sub_width_opt =
+    boolbv_width(to_type_with_subtype(type).subtype());
+  CHECK_RETURN(sub_width_opt.has_value());
+  const std::size_t sub_width = *sub_width_opt;
 
   INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
   INVARIANT(

src/solvers/flattening/boolbv_array.cpp

@@ -15,7 +15,10 @@ 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 auto &width_opt = boolbv_width(expr.type());
+  CHECK_RETURN(width_opt.has_value());
+  const std::size_t width = *width_opt;
+
   const exprt::operandst &operands = expr.operands();
 
   if(operands.empty() && width == 0)

src/solvers/flattening/boolbv_array_of.cpp

@@ -23,17 +23,13 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
   if(is_unbounded_array(array_type))
     return conversion_failed(expr);
 
-  std::size_t width=boolbv_width(array_type);
+  const auto &width_opt = boolbv_width(array_type);
+  if(!width_opt.has_value())
+    return conversion_failed(expr);
+  else if(*width_opt == 0)
+    return bvt{};
 
-  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();
-  }
+  const std::size_t width = *width_opt;
 
   const exprt &array_size=array_type.size();
 

src/solvers/flattening/boolbv_bitreverse.cpp

@@ -12,10 +12,12 @@ Author: Michael Tautschnig
 
 bvt boolbvt::convert_bitreverse(const bitreverse_exprt &expr)
 {
-  const std::size_t width = boolbv_width(expr.type());
-  if(width == 0)
+  const auto &width_opt = boolbv_width(expr.type());
+  if(!width_opt.has_value())
     return conversion_failed(expr);
 
+  const std::size_t width = *width_opt;
+
   bvt bv = convert_bv(expr.op(), width);
 
   std::reverse(bv.begin(), bv.end());

src/solvers/flattening/boolbv_bitwise.cpp

@@ -12,10 +12,12 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_bitwise(const exprt &expr)
 {
-  const std::size_t width = boolbv_width(expr.type());
-  if(width==0)
+  const auto &width_opt = boolbv_width(expr.type());
+  if(!width_opt.has_value())
     return conversion_failed(expr);
 
+  const std::size_t width = *width_opt;
+
   if(expr.id()==ID_bitnot)
   {
     const exprt &op = to_bitnot_expr(expr).op();