Merge pull request #3105 from diffblue/hex-bitvectors6

simplify_exprt::simplify_bitwise is now independent of bitvector representation

Author: Daniel Kroening

src/util/arith_tools.cpp

@@ -273,3 +273,51 @@ bool get_bitvector_bit(const irep_idt &src, std::size_t bit_index)
   PRECONDITION(bit_index < src.size());
   return src[src.size() - 1 - bit_index] == '1';
 }
+
+/// construct a bit-vector representation from a functor
+/// \param width: the width of the bit-vector
+/// \param f: the functor -- the parameter is the bit index
+/// \returns new bitvector representation
+irep_idt
+make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)
+{
+  std::string result(width, ' ');
+
+  for(std::size_t i = 0; i < width; i++)
+    result[width - 1 - i] = f(i) ? '1' : '0';
+
+  return result;
+}
+
+/// perform a binary bit-wise operation, given as a functor,
+/// on a bit-vector representation
+/// \param a: the representation of the first bit vector
+/// \param b: the representation of the second bit vector
+/// \param width: the width of the bit-vector
+/// \param f: the functor
+/// \returns new bitvector representation
+irep_idt bitvector_bitwise_op(
+  const irep_idt &a,
+  const irep_idt &b,
+  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));
+  });
+}
+
+/// perform a unary bit-wise operation, given as a functor,
+/// on a bit-vector representation
+/// \param a: the bit-vector representation
+/// \param width: the width of the bit-vector
+/// \param f: the functor
+/// \returns new bitvector representation
+irep_idt bitvector_bitwise_op(
+  const irep_idt &a,
+  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)); });
+}

src/util/arith_tools.h

@@ -166,4 +166,7 @@ void mp_max(mp_integer &a, const mp_integer &b);
 
 bool get_bitvector_bit(const irep_idt &src, std::size_t bit_index);
 
+irep_idt
+make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f);
+
 #endif // CPROVER_UTIL_ARITH_TOOLS_H

src/util/simplify_expr_int.cpp

@@ -713,13 +713,10 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
 
   // try to merge constants
 
-  std::size_t width=to_bitvector_type(expr.type()).get_width();
+  const std::size_t width = to_bitvector_type(expr.type()).get_width();
 
   while(expr.operands().size()>=2)
   {
-    const irep_idt &a_str=expr.op0().get(ID_value);
-    const irep_idt &b_str=expr.op1().get(ID_value);
-
     if(!expr.op0().is_constant())
       break;
 
@@ -732,30 +729,24 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
     if(expr.op1().type()!=expr.type())
       break;
 
-    INVARIANT(
-      a_str.size() == b_str.size(),
-      "bitvectors of the same type have the same size");
+    const auto &a_val = to_constant_expr(expr.op0()).get_value();
+    const auto &b_val = to_constant_expr(expr.op1()).get_value();
 
-    std::string new_value;
-    new_value.resize(width);
+    std::function<bool(bool, bool)> f;
 
     if(expr.id()==ID_bitand)
-    {
-      for(std::size_t i=0; i<width; i++)
-        new_value[i]=(a_str[i]=='1' && b_str[i]=='1')?'1':'0';
-    }
+      f = [](bool a, bool b) { return a & b; };
     else if(expr.id()==ID_bitor)
-    {
-      for(std::size_t i=0; i<width; i++)
-        new_value[i]=(a_str[i]=='1' || b_str[i]=='1')?'1':'0';
-    }
+      f = [](bool a, bool b) { return a | b; };
     else if(expr.id()==ID_bitxor)
-    {
-      for(std::size_t i=0; i<width; i++)
-        new_value[i]=((a_str[i]=='1')!=(b_str[i]=='1'))?'1':'0';
-    }
+      f = [](bool a, bool b) { return a ^ b; };
     else
-      break;
+      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));
+      });
 
     constant_exprt new_op(new_value, expr.type());
 
@@ -1280,16 +1271,17 @@ bool simplify_exprt::simplify_bitnot(exprt &expr)
      expr.type().id()==ID_unsignedbv ||
      expr.type().id()==ID_signedbv)
   {
+    const auto width = to_bitvector_type(expr.type()).get_width();
+
     if(op.type()==expr.type())
     {
       if(op.id()==ID_constant)
       {
-        std::string value=op.get_string(ID_value);
-
-        for(auto &ch : value)
-          ch=(ch=='0')?'1':'0';
-
-        expr = constant_exprt(value, op.type());
+        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);
+        });
+        expr = constant_exprt(new_value, op.type());
         return false;
       }
     }