From f5133317f1438203a52cf65a08e2035ed082f639 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 5 Dec 2022 14:26:58 +0000 Subject: [PATCH] fixup! Simplify byte_extract(byte_update(...)) without overlap This fixes a bits/bytes confusing, resulting in missed optimisations of byte_extract(byte_update(...)) nestings when the byte_extract was at an offset higher than the update. Found while debugging https://github.com/model-checking/kani/issues/1958. --- src/util/simplify_expr.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index b52a738ffbbc..8e16f80fa079 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1727,7 +1727,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) const auto update_size = pointer_offset_bits(bu.value().type(), ns); if( update_size.has_value() && - *offset >= *update_offset * bu.get_bits_per_byte() + *update_size) + *offset * expr.get_bits_per_byte() >= + *update_offset * bu.get_bits_per_byte() + *update_size) { auto tmp = expr; tmp.op() = bu.op();