From 633875b9f37ab4b714c5d0f9e06e75576730d9ef Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 13 Nov 2022 09:12:15 +0000 Subject: [PATCH] Simplify non-trivial pointer subtraction We can also simplify the case where both pointers refer to the same object, as long as the pointers are at most one element beyond bounds. --- src/util/simplify_expr_int.cpp | 31 ++++++++++++++++++++++++++++--- 1 file changed, 28 insertions(+), 3 deletions(-) diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 8cfe93cf7c5..0cf375fa33e 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -595,10 +595,35 @@ simplify_exprt::simplify_minus(const minus_exprt &expr) is_number(minus_expr.type()) && operands[0].type().id() == ID_pointer && operands[1].type().id() == ID_pointer) { - // pointer arithmetic: rewrite "p-p" to "0" + exprt ptr_op0 = simplify_object(operands[0]).expr; + exprt ptr_op1 = simplify_object(operands[1]).expr; - if(operands[0]==operands[1]) - return from_integer(0, minus_expr.type()); + auto address_of = expr_try_dynamic_cast(ptr_op0); + if(ptr_op0 == ptr_op1 && address_of) + { + exprt offset_op0 = simplify_pointer_offset( + pointer_offset_exprt{operands[0], minus_expr.type()}); + exprt offset_op1 = simplify_pointer_offset( + pointer_offset_exprt{operands[1], minus_expr.type()}); + + const auto object_size = + pointer_offset_size(address_of->object().type(), ns); + auto element_size = + size_of_expr(to_pointer_type(operands[0].type()).base_type(), ns); + + if( + offset_op0.is_constant() && offset_op1.is_constant() && + object_size.has_value() && element_size.has_value() && + numeric_cast_v(to_constant_expr(offset_op0)) <= + *object_size && + numeric_cast_v(to_constant_expr(offset_op1)) <= + *object_size) + { + return changed(simplify_rec(div_exprt{ + minus_exprt{offset_op0, offset_op1}, + typecast_exprt{*element_size, minus_expr.type()}})); + } + } } return unchanged(expr);