Merge pull request #3196 from diffblue/get_bitvector_bit_width

get_bitvector_bit is now told the width

Author: tautschnig

src/solvers/flattening/boolbv_constant.cpp

@@ -91,7 +91,7 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
 
     for(std::size_t i=0; i<width; i++)
     {
-      const bool bit = get_bitvector_bit(value, i);
+      const bool bit = get_bitvector_bit(value, width, i);
       bv[i]=const_literal(bit);
     }
 

src/util/arith_tools.cpp

@@ -265,12 +265,17 @@ void mp_max(mp_integer &a, const mp_integer &b)
 
 /// Get a bit with given index from bit-vector representation.
 /// \param src: the bitvector representation
+/// \param width: the number of bits in the bitvector
 /// \param bit_index: index (0 is the least significant)
-bool get_bitvector_bit(const irep_idt &src, std::size_t bit_index)
+bool get_bitvector_bit(
+  const irep_idt &src,
+  std::size_t width,
+  std::size_t bit_index)
 {
   // The representation is binary, using '0'/'1',
   // most significant bit first.
-  PRECONDITION(bit_index < src.size());
+  PRECONDITION(bit_index < width);
+  PRECONDITION(src.size() == width);
   return src[src.size() - 1 - bit_index] == '1';
 }
 
@@ -302,8 +307,8 @@ irep_idt bitvector_bitwise_op(
   const std::size_t width,
   const std::function<bool(bool, bool)> f)
 {
-  return make_bvrep(width, [&a, &b, f](std::size_t i) {
-    return f(get_bitvector_bit(a, i), get_bitvector_bit(b, i));
+  return make_bvrep(width, [&a, &b, &width, f](std::size_t i) {
+    return f(get_bitvector_bit(a, width, i), get_bitvector_bit(b, width, i));
   });
 }
 
@@ -318,6 +323,7 @@ irep_idt bitvector_bitwise_op(
   const std::size_t width,
   const std::function<bool(bool)> f)
 {
-  return make_bvrep(
-    width, [&a, f](std::size_t i) { return f(get_bitvector_bit(a, i)); });
+  return make_bvrep(width, [&a, &width, f](std::size_t i) {
+    return f(get_bitvector_bit(a, width, i));
+  });
 }

src/util/arith_tools.h

@@ -164,7 +164,10 @@ mp_integer power(const mp_integer &base, const mp_integer &exponent);
 void mp_min(mp_integer &a, const mp_integer &b);
 void mp_max(mp_integer &a, const mp_integer &b);
 
-bool get_bitvector_bit(const irep_idt &src, std::size_t bit_index);
+bool get_bitvector_bit(
+  const irep_idt &src,
+  std::size_t width,
+  std::size_t bit_index);
 
 irep_idt
 make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f);

src/util/simplify_expr.cpp

@@ -144,7 +144,7 @@ bool simplify_exprt::simplify_popcount(popcount_exprt &expr)
       std::size_t result = 0;
 
       for(std::size_t i = 0; i < width; i++)
-        if(get_bitvector_bit(value, i))
+        if(get_bitvector_bit(value, width, i))
           result++;
 
       auto result_expr = from_integer(result, expr.type());

src/util/simplify_expr_int.cpp

@@ -744,8 +744,10 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
       UNREACHABLE;
 
     const irep_idt new_value =
-      make_bvrep(width, [&a_val, &b_val, &f](std::size_t i) {
-        return f(get_bitvector_bit(a_val, i), get_bitvector_bit(b_val, i));
+      make_bvrep(width, [&a_val, &b_val, &width, &f](std::size_t i) {
+        return f(
+          get_bitvector_bit(a_val, width, i),
+          get_bitvector_bit(b_val, width, i));
       });
 
     constant_exprt new_op(new_value, expr.type());
@@ -1278,9 +1280,10 @@ bool simplify_exprt::simplify_bitnot(exprt &expr)
       if(op.id()==ID_constant)
       {
         const auto &value = to_constant_expr(op).get_value();
-        const auto new_value = make_bvrep(width, [&value](std::size_t i) {
-          return !get_bitvector_bit(value, i);
-        });
+        const auto new_value =
+          make_bvrep(width, [&value, &width](std::size_t i) {
+            return !get_bitvector_bit(value, width, i);
+          });
         expr = constant_exprt(new_value, op.type());
         return false;
       }