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)
+      {
+        // Operand is entirely below the extracted range.
+        // Adjust new_index to account for the removed operand.
+        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,40 @@ TEST_CASE("Simplify quantifier", "[core][util]")
     REQUIRE(simplify_expr(forall_exprt{a, true_exprt{}}, ns) == true_exprt{});
   }
 }
+
+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);
+}
+
+TEST_CASE("Simplify extractbits dropping trailing operand", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  // extractbits(concat(a, b, c), start=23, end=8) where a,b,c are 8-bit
+  // should drop c and simplify to concat(a, b) or equivalent
+  const unsignedbv_typet u8{8};
+  const unsignedbv_typet u16{16};
+  const unsignedbv_typet u24{24};
+  const symbol_exprt a{"a", u8};
+  const symbol_exprt b{"b", u8};
+  const symbol_exprt c{"c", u8};
+  const concatenation_exprt cat{{a, b, c}, u24};
+  const extractbits_exprt extract{cat, from_integer(8, u24), u16};
+  const auto result = simplify_expr(extract, ns);
+  // c is entirely below the extracted range and should be dropped
+  const concatenation_exprt expected{{a, b}, u16};
+  REQUIRE(result == expected);
+}