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

Author: Daniel Kroening

src/util/arith_tools.cpp

@@ -262,3 +262,26 @@ 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 f: the functor
+irep_idt bitvector_bitwise_op(
+  const irep_idt &a,
+  const irep_idt &b,
+  const std::function<bool(bool, bool)> f)
+{
+  PRECONDITION(a.size() == b.size());
+
+  std::string result(' ', a.size());
+
+  for(std::size_t i = 0; i < result.size(); 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;
+}

src/util/arith_tools.h

@@ -164,4 +164,11 @@ 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);
 
+/// perform a binary bit-wise operation, given as a functor,
+/// on a bit-vector representation
+irep_idt bitvector_bitwise_op(
+  const irep_idt &,
+  const irep_idt &,
+  std::function<bool(bool, bool)>);
+
 #endif // CPROVER_UTIL_ARITH_TOOLS_H

src/util/simplify_expr_int.cpp

@@ -717,9 +717,6 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
 
   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, f);
 
     constant_exprt new_op(new_value, expr.type());