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,37 @@ TEST_CASE("Simplify quantifier", "[core][util]")
     REQUIRE(simplify_expr(forall_exprt{a, true_exprt{}}, ns) == true_exprt{});
   }
 }
+
+TEST_CASE("Simplify lshr of concatenation", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  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};
+
+  // (concat(a, b)) >> 8 -> concat(0x00, a)
+  const lshr_exprt lshr{cat, from_integer(8, u16)};
+  const concatenation_exprt expected{{from_integer(0, bv_typet{8}), a}, u16};
+  REQUIRE(simplify_expr(lshr, ns) == expected);
+}
+
+TEST_CASE("Simplify shl of concatenation", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  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};
+
+  // (concat(a, b)) << 8 -> concat(b, 0x00)
+  const shl_exprt shl{cat, from_integer(8, u16)};
+  const concatenation_exprt expected{{b, from_integer(0, bv_typet{8})}, u16};
+  REQUIRE(simplify_expr(shl, ns) == expected);
+}