Fix shadow memory missing aggregation on non-compound bitvector types #7935
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
esteffin
requested review from
kroening,
tautschnig and
peterschrammel
as code owners
esteffin
force-pushed
the
esteffin/sm-aggregate-on-non-byte-bv
branch
2 times, most recently
from
3d6294e to
aa39c40
Compare
Codecov ReportAll modified lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@
## develop #7935 +/- ##
===========================================
- Coverage 78.62% 78.62% -0.01%
===========================================
Files 1701 1701
Lines 195987 195975 -12
===========================================
- Hits 154097 154087 -10
+ Misses 41890 41888 -2
☔ View full report in Codecov by Sentry. |
peterschrammel
approved these changes
Oct 4, 2023
|
|
||
| // Iterator for the other elements in the collection in the interval denoted | ||
| // by `expr_iterator` and `end`. | ||
| std::vector<exprt>::const_iterator expr_to_compare_to = expr_iterator + 1; |
| member_exprt(expr, component), field_type, ns, log, is_union, max); | ||
| } | ||
| return max; | ||
| // TODO: sure unsigned_long_int_type()? |
There was a problem hiding this comment.
yes! char won't be enough
| /// \param field_type the type of the shadow memory field to return | ||
| /// \param ns the namespace to perform type-lookups into | ||
| /// \return the aggregated max byte-sized value contained in expr | ||
| /// Note that the expr type size must be known at compile time. |
There was a problem hiding this comment.
In an invariant of boolbv_widtht::operator() that we use to get the size here.
It would be nice to avoid the invariant by doing a check earlier, but unfortunately that's harder to do as it would involve a recursive check on the type structure.
If necessary it is possible to add it in, but I would defer it to a future PR
| __CPROVER_set_field(a + 1, "uninitialized", 1); | ||
|
|
||
| assert(__CPROVER_get_field(a, "uninitialized") == 0); | ||
| assert(__CPROVER_get_field(a + 1, "uninitialized") == 1); |
There was a problem hiding this comment.
I'd check the remaining bytes too that they are 0.
When using duplicate_per_byte with signed bv, if the bv was casted to a bigger unsigned bv the sign-extension was performed, so the obtained bv was non-zero on the least significant part and interfeering with the replicated value.
NlightNFotis
force-pushed
the
esteffin/sm-aggregate-on-non-byte-bv
branch
from
aa39c40 to
5e0547e
Compare
esteffin
force-pushed
the
esteffin/sm-aggregate-on-non-byte-bv
branch
from
5e0547e to
055621d
Compare
Fix missing aggregation when the shadow memory element type is a non-compound bitvector of size > 1 byte.
esteffin
force-pushed
the
esteffin/sm-aggregate-on-non-byte-bv
branch
from
055621d to
e555d0d
Compare
added 2 commits
October 4, 2023 13:12
Fix shadow memory regression tests that was not aggregating correctly when the type of the element is a non-compound bit vector of size > 1 byte. Also added extra checks on the regression test.
esteffin
force-pushed
the
esteffin/sm-aggregate-on-non-byte-bv
branch
from
e555d0d to
3251ce4
Compare
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.
Fix shadow memory missing
maxaggregation when the type is a non-compound bitvector of size > 1 byte.Fix bug in
duplicate_per_bytewhen theinit_exprhas signed type.Fix wrong regression and unit tests.