Add optional expected_width parameter to convert_bv

Author: danpoe

src/solvers/flattening/boolbv.cpp

@@ -113,7 +113,8 @@ bool boolbvt::literal(
   throw "found no literal for expression";
 }
 
-const bvt &boolbvt::convert_bv(const exprt &expr)
+const bvt &
+boolbvt::convert_bv(const exprt &expr, optionalt<std::size_t> expected_width)
 {
   // check cache first
   std::pair<bv_cachet::iterator, bool> cache_result=
@@ -126,18 +127,27 @@ const bvt &boolbvt::convert_bv(const exprt &expr)
   // Iterators into hash_maps supposedly stay stable
   // even though we are inserting more elements recursively.
 
-  cache_result.first->second=convert_bitvector(expr);
+  const bvt &bv = convert_bitvector(expr);
+
+  INVARIANT_WITH_DIAGNOSTICS(
+    !expected_width || bv.size() == *expected_width,
+    "bitvector width shall match the indicated expected width",
+    expr.find_source_location(),
+    expr.pretty());
+
+  cache_result.first->second = bv;
 
   // check
   forall_literals(it, cache_result.first->second)
   {
     if(freeze_all && !it->is_constant())
       prop.set_frozen(*it);
-    if(it->var_no()==literalt::unused_var_no())
-    {
-      error() << "unused_var_no: " << expr.pretty() << eom;
-      assert(false);
-    }
+
+    INVARIANT_WITH_DIAGNOSTICS(
+      it->var_no() != literalt::unused_var_no(),
+      "variable number must be different from the unused variable number",
+      expr.find_source_location(),
+      expr.pretty());
   }
 
   return cache_result.first->second;

src/solvers/flattening/boolbv.h

@@ -14,9 +14,10 @@ Author: Daniel Kroening, [email protected]
 // convert expression to boolean formula
 //
 
-#include <util/mp_arith.h>
-#include <util/expr.h>
 #include <util/byte_operators.h>
+#include <util/expr.h>
+#include <util/mp_arith.h>
+#include <util/optional.h>
 
 #include "bv_utils.h"
 #include "boolbv_width.h"
@@ -43,7 +44,10 @@ class boolbvt:public arrayst
   {
   }
 
-  virtual const bvt &convert_bv(const exprt &expr); // check cache
+  virtual const bvt &convert_bv( // check cache
+    const exprt &expr,
+    const optionalt<std::size_t> expected_width = nullopt);
+
   virtual bvt convert_bitvector(const exprt &expr); // no cache
 
   // overloading

src/util/optional.h

@@ -36,4 +36,6 @@ using optionalt=nonstd::optional<T>; // NOLINT template typedef
 
 typedef nonstd::bad_optional_access bad_optional_accesst;
 
+using nonstd::nullopt;
+
 #endif // CPROVER_UTIL_OPTIONAL_H