Simplify byte_extract(constant, o, t) when sizeof(t) < sizeof(constant) #3974
Conversation
tautschnig
requested review from
kroening,
peterschrammel,
pkesseli and
smowton
as code owners
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 329decb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98810790
| { | ||
| int a[7] = {0}; | ||
|
|
||
| //CBMC reports wrong results for 256, -2147221455, -2147221455, -2147221455, 16, -2147483600, 16384 |
There was a problem hiding this comment.
Is this still true, or was this the bug report that we're exhibiting we've fixed?
There was a problem hiding this comment.
Indeed, too naive copying. I've updated the comment as well as the original file (main.c in the same directory).
src/util/simplify_expr.cpp
Outdated
| // flexible array members at the end of a struct | ||
| if(bits.has_value() && mp_integer(bits->size()) == *el_size + *offset * 8) | ||
| // make sure we don't lose bits with flexible struct members | ||
| const bool has_flexible_struct_member = has_subtype( |
There was a problem hiding this comment.
Nitpick: these appear to be called flexible array members elsewhere, so we might call this struct_has_flexible_array_member
tautschnig
force-pushed
the
simplify-byte-extract-ext
branch
from
329decb to
07e8b00
Compare
| // flexible array members at the end of a struct | ||
| if(bits.has_value() && mp_integer(bits->size()) == *el_size + *offset * 8) | ||
| // make sure we don't lose bits with structs containing flexible array members | ||
| const bool struct_has_flexible_array_member = has_subtype( |
There was a problem hiding this comment.
⛏ Might be worth factoring that out into a utility to avoid someone recoding that at the next occasion...
There was a problem hiding this comment.
I'll in this case not follow the advice for two reasons: 1) This is an over-approximating check, even struct_has_flexible_array_member == true need not mean that there genuinely are flexible array members (which is ok in this context, it just mean we don't simplify although we possibly could); 2) I haven't found any other bits of the code outside the C type checker that currently try to deal with this special case. Should a need for that arise, of course, we should refactor. I hope that's ok!
tautschnig
force-pushed
the
simplify-byte-extract-ext
branch
from
07e8b00 to
407992e
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 407992e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98928775
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
We previously restricted this case to sizeof(t) == sizeof(constant) to discard some cases of flexible arrays. It wasn't actually a sound way of detecting that case, and also disallowed many cases where we can safely simplify. Instead, look at the type and detect (possible) flexible array members.
tautschnig
force-pushed
the
simplify-byte-extract-ext
branch
from
407992e to
919d265
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 919d265).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99078961
We previously restricted this case to sizeof(t) == sizeof(constant) to discard
some cases of flexible arrays. It wasn't actually a sound way of detecting that
case, and also disallowed many cases where we can safely simplify. Instead, look
at the type and detect (possible) flexible array members.