added means to perform bit-wise operations on the bit-vector representation

Author: Daniel Kroening

src/util/arith_tools.cpp

@@ -262,3 +262,46 @@ void mp_max(mp_integer &a, const mp_integer &b)
   if(b>a)
     a=b;
 }
+
+/// 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)
+{
+  PRECONDITION(a.size() == width);
+  PRECONDITION(b.size() == width);
+
+  std::string result(width, ' ');
+
+  for(std::size_t i = 0; i < width; i++)
+  {
+    const bool bit_a = a[i] == '1';
+    const bool bit_b = b[i] == '1';
+    const bool bit_result = f(bit_a, bit_b);
+    result[i] = bit_result ? '1' : '0';
+  }
+
+  return result;
+}
+
+/// 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 bitvector_bitwise_op(a, a, width, [f](bool a, bool) { return f(a); });
+}

src/util/arith_tools.h

@@ -164,4 +164,15 @@ 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);
 
+irep_idt bitvector_bitwise_op(
+  const irep_idt &,
+  const irep_idt &,
+  const std::size_t width,
+  std::function<bool(bool, bool)>);
+
+irep_idt bitvector_bitwise_op(
+  const irep_idt &,
+  const std::size_t width,
+  std::function<bool(bool)>);
+
 #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,21 @@ 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 = bitvector_bitwise_op(a_val, b_val, width, f);
 
     constant_exprt new_op(new_value, expr.type());
 
@@ -1280,16 +1268,16 @@ 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 =
+          bitvector_bitwise_op(value, width, [](bool a) { return !a; });
+        expr = constant_exprt(new_value, op.type());
         return false;
       }
     }