Merge pull request #3041 from hannes-steffenhagen-diffblue/feature-invariant_cleanup-flattening-extractbits

Invariant cleanup in flattening/boolbv_extractbit.cpp and flattening/boolbv_extractbits.cpp

Author: tautschnig

src/solvers/flattening/boolbv_extractbit.cpp

@@ -12,81 +12,77 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <algorithm>
 
 #include <util/arith_tools.h>
+#include <util/exception_utils.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 
 literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
 {
-  const exprt::operandst &operands=expr.operands();
-
-  if(operands.size()!=2)
-    throw "extractbit takes two operands";
-
-  const bvt &bv0=convert_bv(operands[0]);
+  const bvt &src_bv = convert_bv(expr.src());
 
   // constant?
-  if(operands[1].is_constant())
+  if(expr.index().is_constant())
   {
-    mp_integer o;
-
-    if(to_integer(operands[1], o))
-      throw "extractbit failed to convert constant index";
+    mp_integer index_as_integer = numeric_cast_v<mp_integer>(expr.index());
 
-    if(o<0 || o>=bv0.size())
+    if(index_as_integer < 0 || index_as_integer >= src_bv.size())
       return prop.new_variable(); // out of range!
     else
-      return bv0[integer2size_t(o)];
+      return src_bv[integer2size_t(index_as_integer)];
   }
 
-  if(operands[0].type().id()==ID_verilog_signedbv ||
-     operands[0].type().id()==ID_verilog_unsignedbv)
+  if(
+    expr.src().type().id() == ID_verilog_signedbv ||
+    expr.src().type().id() == ID_verilog_unsignedbv)
   {
-    // TODO
-    assert(false);
+    throw unsupported_operation_exceptiont(
+      "extractbit expression not implemented for verilog integers in "
+      "flattening solver");
   }
   else
   {
-    std::size_t width_op0=boolbv_width(operands[0].type());
-    std::size_t width_op1=boolbv_width(operands[1].type());
+    std::size_t src_bv_width = boolbv_width(expr.src().type());
+    std::size_t index_bv_width = boolbv_width(expr.index().type());
 
-    if(width_op0==0 || width_op1==0)
+    if(src_bv_width == 0 || index_bv_width == 0)
       return SUB::convert_rest(expr);
 
-    std::size_t index_width = std::max(address_bits(width_op0), width_op1);
+    std::size_t index_width =
+      std::max(address_bits(src_bv_width), index_bv_width);
     unsignedbv_typet index_type(index_width);
 
     equal_exprt equality;
-    equality.lhs()=operands[1]; // index operand
+    equality.lhs() = expr.index();
 
     if(index_type!=equality.lhs().type())
       equality.lhs().make_typecast(index_type);
 
     if(prop.has_set_to())
     {
       // free variable
-      literalt l=prop.new_variable();
+      literalt literal = prop.new_variable();
 
       // add implications
-      for(std::size_t i=0; i<bv0.size(); i++)
+      for(std::size_t i = 0; i < src_bv.size(); i++)
       {
         equality.rhs()=from_integer(i, index_type);
-        literalt equal=prop.lequal(l, bv0[i]);
+        literalt equal = prop.lequal(literal, src_bv[i]);
         prop.l_set_to_true(prop.limplies(convert(equality), equal));
       }
 
-      return l;
+      return literal;
     }
     else
     {
-      literalt l=prop.new_variable();
+      literalt literal = prop.new_variable();
 
-      for(std::size_t i=0; i<bv0.size(); i++)
+      for(std::size_t i = 0; i < src_bv.size(); i++)
       {
         equality.rhs()=from_integer(i, index_type);
-        l=prop.lselect(convert(equality), bv0[i], l);
+        literal = prop.lselect(convert(equality), src_bv[i], literal);
       }
 
-      return l;
+      return literal;
     }
   }
 

src/solvers/flattening/boolbv_extractbits.cpp

@@ -12,62 +12,51 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
 {
-  std::size_t width=boolbv_width(expr.type());
+  const std::size_t bv_width = boolbv_width(expr.type());
 
-  if(width==0)
+  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());
 
-  mp_integer o1, o2;
-  const bvt &bv0=convert_bv(expr.op0());
+  auto const maybe_upper_as_int = numeric_cast<mp_integer>(expr.upper());
+  auto const maybe_lower_as_int = numeric_cast<mp_integer>(expr.lower());
 
   // We only do constants for now.
   // Should implement a shift here.
-  if(to_integer(expr.op1(), o1) ||
-     to_integer(expr.op2(), o2))
+  if(!maybe_upper_as_int.has_value() || !maybe_lower_as_int.has_value())
     return conversion_failed(expr);
 
-  if(o1<0 || o1>=bv0.size())
-  {
-    error().source_location=expr.find_source_location();
-    error() << "extractbits: second operand out of range: "
-            << expr.pretty() << eom;
-  }
+  auto upper_as_int = maybe_upper_as_int.value();
+  auto lower_as_int = maybe_lower_as_int.value();
 
-  if(o2<0 || o2>=bv0.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});
 
-  if(o2>o1)
-    std::swap(o1, o2);
+  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});
 
-  // now o2<=o1
+  if(lower_as_int > upper_as_int)
+    std::swap(upper_as_int, lower_as_int);
 
-  if((o1-o2+1)!=width)
-  {
-    error().source_location=expr.find_source_location();
-    error() << "extractbits: wrong width (expected " << (o1-o2+1)
-            << " but got " << width << "): " << expr.pretty() << eom;
-    throw 0;
-  }
+  // now lower_as_int <= upper_as_int
 
-  std::size_t offset=integer2unsigned(o2);
+  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});
 
-  bvt bv;
-  bv.resize(width);
+  const std::size_t offset = integer2unsigned(lower_as_int);
 
-  for(std::size_t i=0; i<width; i++)
-    bv[i]=bv0[offset+i];
+  bvt result_bv(src_bv.begin() + offset, src_bv.begin() + offset + bv_width);
 
-  return bv;
+  return result_bv;
 }