Simplify shifts of concatenations

We may be able to drop some of the operands of the concatenation and use
all-zeros instead.

Author: tautschnig

src/util/simplify_expr_int.cpp

@@ -1033,6 +1033,54 @@ simplify_exprt::simplify_shifts(const shift_exprt &expr)
   if(*distance == 0)
     return expr.op();
 
+  if(
+    expr.op().id() == ID_concatenation &&
+    (expr.id() == ID_lshr || expr.id() == ID_shl))
+  {
+    mp_integer offset = to_bitvector_type(expr.op().type()).get_width();
+    mp_integer bits_seen = 0;
+    for(std::size_t i = 0; i < expr.op().operands().size(); ++i)
+    {
+      if(expr.id() == ID_lshr && offset == distance)
+      {
+        exprt::operandst new_operands;
+        new_operands.reserve(i + 1);
+        new_operands.push_back(
+          from_integer(0, bv_typet{numeric_cast_v<std::size_t>(*distance)}));
+        new_operands.insert(
+          new_operands.end(),
+          expr.op().operands().begin(),
+          expr.op().operands().begin() + i);
+        concatenation_exprt new_concat = to_concatenation_expr(expr.op());
+        new_concat.operands() = std::move(new_operands);
+        return changed(simplify_concatenation(new_concat));
+      }
+
+      auto op_width = pointer_offset_bits(expr.op().operands()[i].type(), ns);
+
+      if(!op_width.has_value() || *op_width <= 0)
+        return unchanged(expr);
+
+      offset -= *op_width;
+      bits_seen += *op_width;
+
+      if(expr.id() == ID_shl && bits_seen == distance)
+      {
+        exprt::operandst new_operands;
+        new_operands.reserve(expr.op().operands().size() - i);
+        new_operands.insert(
+          new_operands.end(),
+          expr.op().operands().begin() + i + 1,
+          expr.op().operands().end());
+        new_operands.push_back(
+          from_integer(0, bv_typet{numeric_cast_v<std::size_t>(*distance)}));
+        concatenation_exprt new_concat = to_concatenation_expr(expr.op());
+        new_concat.operands() = std::move(new_operands);
+        return changed(simplify_concatenation(new_concat));
+      }
+    }
+  }
+
   auto value = numeric_cast<mp_integer>(expr.op());
 
   if(

unit/util/simplify_expr.cpp

@@ -652,3 +652,85 @@ 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));
+}
+
+
+TEST_CASE("Simplify shift of concatenation", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  // (concat(a, b)) >> 8 where a and b are 8-bit
+  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 lshr_exprt shift{cat, from_integer(8, u16)};
+  const auto result = simplify_expr(shift, ns);
+  // Should simplify — the result should not be a shift of a concatenation
+  REQUIRE(result.id() != ID_lshr);
+}
+