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.

Author: tautschnig

regression/cbmc/Empty_struct1/test.desc

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

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