Simplify bitwise operations over concatenation and a constant

Perform point-wise application of the bitwise operation and concatenate
the result: if some of the operands of the concatenation were constants
the bitwise operation will yield modified constants.

Author: tautschnig

src/util/simplify_expr_int.cpp

@@ -832,6 +832,48 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
   if(new_expr.operands().size() == 1)
     return new_expr.op0();
 
+  if(
+    new_expr.operands().size() == 2 &&
+    (new_expr.operands().front().is_constant() ||
+     new_expr.operands().back().is_constant()) &&
+    (new_expr.operands().front().id() == ID_concatenation ||
+     new_expr.operands().back().id() == ID_concatenation))
+  {
+    const exprt &constant = new_expr.operands().front().is_constant()
+                              ? new_expr.operands().front()
+                              : new_expr.operands().back();
+    const auto svalue = expr2bits(constant, true, ns);
+    CHECK_RETURN(svalue.has_value());
+    CHECK_RETURN(svalue->size() == width);
+
+    concatenation_exprt new_concat =
+      new_expr.operands().front().id() == ID_concatenation
+        ? to_concatenation_expr(new_expr.operands().front())
+        : to_concatenation_expr(new_expr.operands().back());
+    // the most-significant bit comes first in an concatenation_exprt, hence we
+    // count down
+    std::size_t offset = width;
+    for(auto &op : new_concat.operands())
+    {
+      auto op_width = pointer_offset_bits(op.type(), ns);
+      CHECK_RETURN(op_width.has_value());
+      CHECK_RETURN(*op_width > 0);
+      CHECK_RETURN(*op_width <= offset);
+      std::size_t op_width_int = numeric_cast_v<std::size_t>(*op_width);
+
+      std::string extracted_value =
+        svalue->substr(offset - op_width_int, op_width_int);
+
+      auto op_bits = bits2expr(extracted_value, op.type(), true, ns);
+      CHECK_RETURN(op_bits.has_value());
+      op = simplify_bitwise(multi_ary_exprt{op, expr.id(), *op_bits}).expr;
+
+      offset -= op_width_int;
+    }
+
+    return changed(simplify_concatenation(new_concat));
+  }
+
   if(no_change)
     return unchanged(expr);
   else

unit/util/simplify_expr.cpp

@@ -652,3 +652,67 @@ TEST_CASE("Simplify quantifier", "[core][util]")
     REQUIRE(simplify_expr(forall_exprt{a, true_exprt{}}, ns) == true_exprt{});
   }
 }
+
+
+TEST_CASE("Simplify double typecast over bv types", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  // (unsigned)(signed)x where x is unsigned and same width -> x
+  const unsignedbv_typet u32{32};
+  const signedbv_typet s32{32};
+  const symbol_exprt x{"x", u32};
+  const typecast_exprt inner{x, s32};
+  const typecast_exprt outer{inner, u32};
+  REQUIRE(simplify_expr(outer, ns) == x);
+}
+
+
+TEST_CASE("Simplify (x * n) % n", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  const unsignedbv_typet u32{32};
+  const symbol_exprt x{"x", u32};
+  const constant_exprt n = from_integer(7, u32);
+  const mult_exprt mul{x, n};
+  const mod_exprt mod{mul, n};
+  const auto result = simplify_expr(mod, ns);
+  REQUIRE(result == from_integer(0, u32));
+}
+
+
+TEST_CASE("Simplify all-zero constant in bitand", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  const bv_typet bv8{8};
+  const symbol_exprt x{"x", bv8};
+  const constant_exprt zero = bv8.all_zeros_expr();
+  const bitand_exprt band{x, zero};
+  const auto result = simplify_expr(band, ns);
+  REQUIRE(result == zero);
+}
+
+
+TEST_CASE("Simplify bitand over concatenation and constant", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  // (concat(a, b)) & 0x00FF -> concat(0x00, b & 0xFF)
+  const bv_typet bv8{8};
+  const bv_typet bv16{16};
+  const symbol_exprt a{"a", bv8};
+  const symbol_exprt b{"b", bv8};
+  const concatenation_exprt cat{{a, b}, bv16};
+  const constant_exprt mask = from_integer(0xFF, bv16);
+  const bitand_exprt band{cat, mask};
+  const auto result = simplify_expr(band, ns);
+  // Result should not contain the original bitand over concatenation
+  REQUIRE((result.id() != ID_bitand || result != band));
+}
+