Byte-extract lowering: do not blindly use offsets #7669
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
When unpacking an array we must not create 0 bytes up until an offset when the source array can never be as large. Doing so when within a struct would spuriously produce a larger member. The test case highlighted a problem in the SMT2 back-end: the first operand of a struct was not correctly flattened and instead used default expression conversion (which is only ok when the array theory is never being used). To avoid this problem creeping in again, factor out the operand conversion into a lambda and invoke that lambda each time. Fixes: diffblue#7654
tautschnig
force-pushed
the
bugfixes/7654-byte-extract
branch
from
30e72b7 to
d4e61f8
Compare
tautschnig
requested review from
kroening,
martin-cs,
peterschrammel,
thomasspriggs,
NlightNFotis and
TGWDB
as code owners
Codecov ReportPatch coverage:
Additional details and impacted files@@ Coverage Diff @@
## develop #7669 +/- ##
===========================================
+ Coverage 78.43% 78.52% +0.08%
===========================================
Files 1674 1674
Lines 191939 191951 +12
===========================================
+ Hits 150546 150723 +177
+ Misses 41393 41228 -165
... and 12 files with indirect coverage changes Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here. ☔ View full report in Codecov by Sentry. |
peterschrammel
approved these changes
Apr 18, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
When unpacking an array we must not create 0 bytes up until an offset when the source array can never be as large. Doing so when within a struct would spuriously produce a larger member.
Fixes: #7654