Merge pull request #929 from diffblue/aval-bval-bitwise

aval/bval encoding for bitwise operators

regression/verilog/expressions/bitwise1.desc

@@ -0,0 +1,7 @@
+CORE
+bitwise1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/expressions/bitwise1.sv

@@ -0,0 +1,16 @@
+module main;
+
+  assert final ((4'b0001 &  4'b1001) === 4'b0001);
+  assert final ((4'b1001 &  4'bx001) === 4'bx001);
+  assert final ((4'b1001 &  4'bz001) === 4'bx001);
+  assert final ((4'b0001 |  4'b1001) === 4'b1001);
+  assert final ((4'b0001 |  4'bx001) === 4'bx001);
+  assert final ((4'b0001 |  4'bz001) === 4'bx001);
+  assert final ((4'b0001 ^  4'b1001) === 4'b1000);
+  assert final ((4'b0001 ^  4'bx001) === 4'bx000);
+  assert final ((4'b0001 ^  4'bz001) === 4'bx000);
+  assert final ((4'b0001 ~^ 4'b1001) === 4'b0111);
+  assert final ((4'b0001 ~^ 4'bx001) === 4'bx111);
+  assert final ((4'b0001 ~^ 4'bz001) === 4'bx111);
+
+endmodule

src/verilog/aval_bval_encoding.cpp

@@ -355,6 +355,39 @@ exprt aval_bval(const bitnot_exprt &expr)
   return combine_aval_bval(aval, op_bval, lower_to_aval_bval(expr.type()));
 }
 
+exprt aval_bval_bitwise(const multi_ary_exprt &expr)
+{
+  auto &type = expr.type();
+  PRECONDITION(is_four_valued(type));
+  PRECONDITION(!expr.operands().empty());
+
+  for(auto &op : expr.operands())
+    PRECONDITION(is_aval_bval(op));
+
+  // x/z is done bit-wise.
+  // Any bit involving x/z is x.
+
+  // bval
+  exprt::operandst bval_disjuncts;
+
+  for(auto &op : expr.operands())
+    bval_disjuncts.push_back(bval(op));
+
+  auto bval = bitor_exprt{bval_disjuncts, bval_disjuncts.front().type()};
+
+  // aval
+  exprt::operandst aval_conjuncts;
+
+  for(auto &op : expr.operands())
+    aval_conjuncts.push_back(aval(op));
+
+  exprt aval = bitand_exprt{
+    multi_ary_exprt{expr.id(), aval_conjuncts, aval_conjuncts.front().type()},
+    bitnot_exprt{bval}}; // 0/1 case
+
+  return combine_aval_bval(aval, bval, lower_to_aval_bval(expr.type()));
+}
+
 exprt aval_bval(const power_exprt &expr)
 {
   PRECONDITION(is_four_valued(expr.type()));

src/verilog/aval_bval_encoding.h

@@ -49,6 +49,8 @@ exprt aval_bval(const verilog_logical_inequality_exprt &);
 exprt aval_bval(const not_exprt &);
 /// lowering for ~
 exprt aval_bval(const bitnot_exprt &);
+/// lowering for &, |, ^, ^~
+exprt aval_bval_bitwise(const multi_ary_exprt &);
 /// lowering for ==?
 exprt aval_bval(const verilog_wildcard_equality_exprt &);
 /// lowering for !=?

src/verilog/verilog_lowering.cpp

@@ -513,6 +513,18 @@ exprt verilog_lowering(exprt expr)
     else
       return expr; // leave as is
   }
+  else if(
+    expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_bitxor ||
+    expr.id() == ID_bitxnor)
+  {
+    auto &multi_ary_expr = to_multi_ary_expr(expr);
+
+    // encode into aval/bval
+    if(is_four_valued(expr.type()))
+      return aval_bval_bitwise(multi_ary_expr);
+    else
+      return expr; // leave as is
+  }
   else if(expr.id() == ID_verilog_iff)
   {
     auto &iff = to_verilog_iff_expr(expr);