Merge pull request #1481 from diffblue/fix-bitand-bitor

Fix four-valued `|` and `&`

Author: tautschnig

CHANGELOG

@@ -1,5 +1,6 @@
 # EBMC 5.9
 
+* Verilog: fix for four-valued | and &
 * Verilog: fix for typed parameter ports
 * SystemVerilog: fix for type parameters
 * SystemVerilog: type parameter ports

regression/verilog/expressions/bitwise_and1.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 bitwise_and1.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This gives wrong answers.

regression/verilog/expressions/bitwise_or1.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 bitwise_or1.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This gives wrong answers.

regression/verilog/expressions/equality5.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 equality5.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This gives the wrong answer.

src/verilog/aval_bval_encoding.cpp

@@ -450,7 +450,85 @@ 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)
+exprt aval_bval_bitand(const bitand_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));
+
+  // All result bits are computed bit-wise.
+  // 0 is the dominating value.
+  // Otherwise, any bit involving x/z is x.
+
+  // A bit is zero of both aval and bval bits are zero.
+  exprt::operandst bit_is_zero_disjuncts;
+
+  for(auto &op : expr.operands())
+    bit_is_zero_disjuncts.push_back(
+      bitand_exprt{bitnot_exprt{aval(op)}, bitnot_exprt{bval(op)}});
+
+  auto bit_is_zero =
+    bitor_exprt{bit_is_zero_disjuncts, bit_is_zero_disjuncts.front().type()};
+
+  // bval: one if not bit_is_zero, and any bval bit is one
+  exprt::operandst bval_disjuncts;
+
+  for(auto &op : expr.operands())
+    bval_disjuncts.push_back(bval(op));
+
+  auto bval = bitand_exprt{
+    bitor_exprt{bval_disjuncts, bval_disjuncts.front().type()},
+    bitnot_exprt{bit_is_zero}};
+
+  // aval: one if not bit_is_zero and bval is zero
+  auto aval = bitand_exprt{bitnot_exprt{bit_is_zero}, bitnot_exprt{bval}};
+
+  return combine_aval_bval(aval, bval, lower_to_aval_bval(expr.type()));
+}
+
+exprt aval_bval_bitor(const bitor_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));
+
+  // All result bits are computed bit-wise.
+  // 1 is the dominating value.
+  // Otherwise, any bit involving x/z is x.
+
+  // A bit is one if the aval bit is one and the bval bit is zero.
+  exprt::operandst bit_is_one_disjuncts;
+
+  for(auto &op : expr.operands())
+    bit_is_one_disjuncts.push_back(
+      bitand_exprt{aval(op), bitnot_exprt{bval(op)}});
+
+  auto bit_is_one =
+    bitor_exprt{bit_is_one_disjuncts, bit_is_one_disjuncts.front().type()};
+
+  // bval: one if not bit_is_one, and any bval bit is one
+  exprt::operandst bval_disjuncts;
+
+  for(auto &op : expr.operands())
+    bval_disjuncts.push_back(bval(op));
+
+  auto bval = bitand_exprt{
+    bitor_exprt{bval_disjuncts, bval_disjuncts.front().type()},
+    bitnot_exprt{bit_is_one}};
+
+  // aval: one if bit_is_one
+  auto aval = bit_is_one;
+
+  return combine_aval_bval(aval, bval, lower_to_aval_bval(expr.type()));
+}
+
+exprt aval_bval_xor_xnor(const multi_ary_exprt &expr)
 {
   auto &type = expr.type();
   PRECONDITION(is_four_valued(type));

src/verilog/aval_bval_encoding.h

@@ -49,8 +49,12 @@ 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_bitand(const bitand_exprt &);
+/// lowering for |
+exprt aval_bval_bitor(const bitor_exprt &);
+/// lowering for ^, ^~
+exprt aval_bval_xor_xnor(const multi_ary_exprt &);
 /// lowering for reduction operators
 exprt aval_bval_reduction(const unary_exprt &);
 /// lowering for replication

src/verilog/verilog_lowering.cpp

@@ -570,15 +570,27 @@ 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)
+  else if(expr.id() == ID_bitand)
+  {
+    // encode into aval/bval
+    if(is_four_valued(expr.type()))
+      return aval_bval_bitand(to_bitand_expr(expr));
+    else
+      return expr; // leave as is
+  }
+  else if(expr.id() == ID_bitor)
+  {
+    // encode into aval/bval
+    if(is_four_valued(expr.type()))
+      return aval_bval_bitor(to_bitor_expr(expr));
+    else
+      return expr; // leave as is
+  }
+  else if(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);
+      return aval_bval_xor_xnor(to_multi_ary_expr(expr));
     else
       return expr; // leave as is
   }