Skip to content

Commit

Permalink
fixup! Simplify byte_extract(byte_update(...)) without overlap
Browse files Browse the repository at this point in the history
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
model-checking/kani#1958.
  • Loading branch information
tautschnig committed Dec 5, 2022
1 parent 3302184 commit f513331
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/util/simplify_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down

0 comments on commit f513331

Please sign in to comment.