Simplify more cases of extractbits over concatenation

We may be able to drop some of the operands of a concatenation.

Author: tautschnig

src/util/simplify_expr_int.cpp

@@ -1205,30 +1205,64 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr)
 
     return std::move(*result);
   }
+  else if(*end == 0 && *start + 1 == *width)
+  {
+    typecast_exprt tc{expr.src(), expr.type()};
+    return changed(simplify_typecast(tc));
+  }
   else if(expr.src().id() == ID_concatenation)
   {
     // the most-significant bit comes first in an concatenation_exprt, hence we
     // count down
     mp_integer offset = *width;
 
+    exprt::operandst new_operands;
+    new_operands.reserve(expr.src().operands().size());
+    mp_integer new_index = *end;
+    mp_integer new_concat_width = 0;
+
     for(const auto &op : expr.src().operands())
     {
       auto op_width = pointer_offset_bits(op.type(), ns);
 
       if(!op_width.has_value() || *op_width <= 0)
         return unchanged(expr);
 
-      if(*start < offset && offset <= *end + *op_width)
+      // current value of offset is the index (within the concatenated
+      // expression) of the most-significant bit of op plus 1
+      if(*end > offset)
+      {
+        // keep checking that remaining operands have a positive width, so
+        // incrementally update new_index and do not use `break`
+        new_index += *op_width;
+      }
+      else if(offset - *op_width <= *start)
       {
-        extractbits_exprt result = expr;
-        result.src() = op;
-        result.index() =
-          from_integer(*end - (offset - *op_width), expr.index().type());
-        return changed(simplify_extractbits(result));
+        new_operands.push_back(op);
+        new_concat_width += *op_width;
       }
 
       offset -= *op_width;
     }
+
+    if(new_operands.size() == 1)
+    {
+      extractbits_exprt result = expr;
+      result.src() = new_operands.front();
+      result.index() = from_integer(new_index, expr.index().type());
+      return changed(simplify_extractbits(result));
+    }
+    else if(
+      !new_operands.empty() &&
+      new_operands.size() < expr.src().operands().size())
+    {
+      extractbits_exprt result = expr;
+      result.src().operands() = new_operands;
+      to_bitvector_type(result.src().type())
+        .set_width(numeric_cast_v<std::size_t>(new_concat_width));
+      result.index() = from_integer(new_index, expr.index().type());
+      return changed(simplify_extractbits(result));
+    }
   }
   else if(auto eb_src = expr_try_dynamic_cast<extractbits_exprt>(expr.src()))
   {
@@ -1242,11 +1276,6 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr)
       return changed(simplify_extractbits(result));
     }
   }
-  else if(*end == 0 && *start + 1 == *width)
-  {
-    typecast_exprt tc{expr.src(), expr.type()};
-    return changed(simplify_typecast(tc));
-  }
 
   return unchanged(expr);
 }

unit/util/simplify_expr.cpp

@@ -652,3 +652,101 @@ 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);
+}
+
+
+TEST_CASE("Simplify extractbits over concatenation", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  // extractbits(concat(a, b), 0, u8) where a,b are 8-bit -> b
+  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 extractbits_exprt extract{cat, from_integer(0, u16), u8};
+  const auto result = simplify_expr(extract, ns);
+  REQUIRE(result == b);
+}