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

@@ -813,6 +813,17 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
       else
         it++;
     }
+
+    // x & 0 -> 0
+    for(const auto &op : new_expr.operands())
+    {
+      if(
+        op.is_constant() &&
+        bvrep2integer(to_constant_expr(op).get_value(), width, false) == 0)
+      {
+        return constant_exprt(integer2bvrep(0, width), new_expr.type());
+      }
+    }
   }
 
   // two operands that are syntactically the same
@@ -832,6 +843,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,37 @@ 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 constant_exprt zero = from_integer(0, u8);
+  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 unsignedbv_typet u8{8};
+  const unsignedbv_typet u16{16};
+  const symbol_exprt a{"a", u8};
+  const symbol_exprt b{"b", u8};
+  const concatenation_exprt cat{{a, b}, u16};
+  const constant_exprt mask = from_integer(0xFF, u16);
+  const bitand_exprt band{cat, mask};
+  const auto result = simplify_expr(band, ns);
+
+  // Expect concat(0x00, b) because a & 0x00 -> 0x00 and b & 0xFF -> b
+  const constant_exprt zero8 = from_integer(0, u8);
+  const concatenation_exprt expected{{zero8, b}, u16};
+  REQUIRE(result == expected);
+}