Merge pull request #8944 from tautschnig/simplify/bitand-bitor-constants

Simplify all-zero or all-one constants in bitand/bitor

Author: kroening

src/util/simplify_expr_int.cpp

@@ -768,6 +768,33 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
     no_change = false;
   }
 
+  // 'all zeros' in bitand yields zero
+  if(new_expr.id() == ID_bitand)
+  {
+    const constant_exprt zero = new_expr.type().id() == ID_bv
+                                  ? to_bv_type(new_expr.type()).all_zeros_expr()
+                                  : from_integer(0, new_expr.type());
+    for(const auto &op : new_expr.operands())
+    {
+      if(op == zero)
+        return zero;
+    }
+  }
+
+  // 'all ones' in bitor yields all-ones
+  if(new_expr.id() == ID_bitor)
+  {
+    const constant_exprt all_ones =
+      new_expr.type().id() == ID_bv
+        ? to_bv_type(new_expr.type()).all_ones_expr()
+        : from_integer(power(2, width) - 1, new_expr.type());
+    for(const auto &op : new_expr.operands())
+    {
+      if(op == all_ones)
+        return all_ones;
+    }
+  }
+
   // now erase 'all zeros' out of bitor, bitxor
 
   if(new_expr.id() == ID_bitor || new_expr.id() == ID_bitxor)

unit/util/simplify_expr.cpp

@@ -8,6 +8,7 @@ Author: Michael Tautschnig
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/cmdline.h>
@@ -652,3 +653,51 @@ TEST_CASE("Simplify quantifier", "[core][util]")
     REQUIRE(simplify_expr(forall_exprt{a, true_exprt{}}, ns) == true_exprt{});
   }
 }
+
+TEST_CASE("Simplify all-zero constant in bitand", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  const unsignedbv_typet u8{8};
+  const symbol_exprt x{"x", u8};
+  const auto zero = from_integer(0, u8);
+  const bitand_exprt band{x, zero};
+  REQUIRE(simplify_expr(band, ns) == zero);
+}
+
+TEST_CASE("Simplify all-ones constant in bitor", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  const unsignedbv_typet u8{8};
+  const symbol_exprt x{"x", u8};
+  const auto ones = from_integer(255, u8);
+  const bitor_exprt bor{x, ones};
+  REQUIRE(simplify_expr(bor, ns) == ones);
+}
+
+TEST_CASE("Simplify all-zero constant in bitand with bv_typet", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  const bv_typet bv8{8};
+  const symbol_exprt x{"x", bv8};
+  const auto zero = bv8.all_zeros_expr();
+  const bitand_exprt band{x, zero};
+  REQUIRE(simplify_expr(band, ns) == zero);
+}
+
+TEST_CASE("Simplify all-ones constant in bitor with bv_typet", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  const bv_typet bv8{8};
+  const symbol_exprt x{"x", bv8};
+  const auto ones = bv8.all_ones_expr();
+  const bitor_exprt bor{x, ones};
+  REQUIRE(simplify_expr(bor, ns) == ones);
+}