Replace throws with invariants in boolbv_extractbits

Also removes one throw that guards against violation of extractbits_expr
invariants

Author: hannes-steffenhagen-diffblue

src/solvers/flattening/boolbv_extractbits.cpp

@@ -17,13 +17,6 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
   if(bv_width == 0)
     return conversion_failed(expr);
 
-  if(expr.operands().size()!=3)
-  {
-    error().source_location=expr.find_source_location();
-    error() << "extractbits takes three operands" << eom;
-    throw 0;
-  }
-
   auto const &src_bv = convert_bv(expr.src());
 
   auto const maybe_upper_as_int = numeric_cast<mp_integer>(expr.upper());
@@ -37,34 +30,29 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
   auto upper_as_int = maybe_upper_as_int.value();
   auto lower_as_int = maybe_lower_as_int.value();
 
-  if(upper_as_int < 0 || upper_as_int >= src_bv.size())
-  {
-    error().source_location=expr.find_source_location();
-    error() << "extractbits: second operand out of range: "
-            << expr.pretty() << eom;
-  }
-
-  if(lower_as_int < 0 || lower_as_int >= src_bv.size())
-  {
-    error().source_location=expr.find_source_location();
-    error() << "extractbits: third operand out of range: "
-            << expr.pretty() << eom;
-    throw 0;
-  }
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    upper_as_int >= 0 && upper_as_int < src_bv.size(),
+    "upper end of extracted bits must be within the bitvector",
+    expr.find_source_location(),
+    irep_pretty_diagnosticst{expr});
+
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    lower_as_int >= 0 && lower_as_int < src_bv.size(),
+    "lower end of extracted bits must be within the bitvector",
+    expr.find_source_location(),
+    irep_pretty_diagnosticst{expr});
 
   if(lower_as_int > upper_as_int)
     std::swap(upper_as_int, lower_as_int);
 
   // now lower_as_int <= upper_as_int
 
-  if((upper_as_int - lower_as_int + 1) != bv_width)
-  {
-    error().source_location=expr.find_source_location();
-    error() << "extractbits: wrong width (expected "
-            << (upper_as_int - lower_as_int + 1) << " but got " << bv_width
-            << "): " << expr.pretty() << eom;
-    throw 0;
-  }
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    (upper_as_int - lower_as_int + 1) == bv_width,
+    "the difference between upper and lower end of the range must have the "
+    "same width as the resulting bitvector type",
+    expr.find_source_location(),
+    irep_pretty_diagnosticst{expr});
 
   const std::size_t offset = integer2unsigned(lower_as_int);