Support byte extract and update for new SMT backend #7285
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
esteffin
force-pushed
the
esteffin/byte-extraction-update-2
branch
6 times, most recently
from
10eac99 to
6fdc582
Compare
Codecov ReportBase: 78.24% // Head: 78.28% // Increases project coverage by
Additional details and impacted files@@ Coverage Diff @@
## develop #7285 +/- ##
===========================================
+ Coverage 78.24% 78.28% +0.03%
===========================================
Files 1642 1642
Lines 189752 189976 +224
===========================================
+ Hits 148479 148714 +235
+ Misses 41273 41262 -11
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 at Codecov. |
esteffin
force-pushed
the
esteffin/byte-extraction-update-2
branch
from
6fdc582 to
48a85bd
Compare
src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
Outdated
Show resolved
Hide resolved
esteffin
force-pushed
the
esteffin/byte-extraction-update-2
branch
6 times, most recently
from
5e3004e to
8f62a0e
Compare
esteffin
requested review from
peterschrammel,
NlightNFotis,
TGWDB and
chris-ryder
as code owners
esteffin
force-pushed
the
esteffin/byte-extraction-update-2
branch
from
8f62a0e to
8b3820f
Compare
TGWDB
approved these changes
Nov 8, 2022
thomasspriggs
suggested changes
Nov 8, 2022
There was a problem hiding this comment.
I think we should get the following sorted before merging -
- Fixing the one unit test which is squashed into the wrong commit.
- Adding commit message bodies. The commits now (mostly) say what they do, which is great. But some of the pre-requisite fixes are still missing the context as to why they are needed. I am happy to go through adding these with you.
| smt_bit_vector_theoryt::make_or( | ||
| smt_bit_vector_theoryt::make_and( | ||
| original_int_term, | ||
| smt_bit_vector_constant_termt{18446744073709486335UL, 64}), |
There was a problem hiding this comment.
⛏️ I think this mask would be easier to interpret as a hex literal.
| smt_bit_vector_theoryt::make_and( | ||
| original_int_term, | ||
| smt_bit_vector_constant_termt{18446744073709486335UL, 64}), | ||
| smt_bit_vector_constant_termt{2816UL, 64})); |
There was a problem hiding this comment.
⛏️ I think the literal 2816UL may be easier to read as 11UL << 8. This would make it clearer that it corresponds to the 11 in the input expression.
| } | ||
| } | ||
|
|
||
| TEST_CASE( |
There was a problem hiding this comment.
👍 Looks like a good test to me.
esteffin
force-pushed
the
esteffin/byte-extraction-update-2
branch
from
8b3820f to
9ec53d1
Compare
added 2 commits
November 8, 2022 17:39
As `with_exprt` can be used as a multy-ary operatior (with more than 3 arguments) we need to introduce an index smt_identifier_termt for each index used by the expression.
Lowering of the byte extraction and byte update expressions can yield non-integer bitvector typed operands. Because we do not require a numeric interpretation of them we can relax the requirement of integer-typed operands for bitwise operators.
esteffin
force-pushed
the
esteffin/byte-extraction-update-2
branch
from
9ec53d1 to
6ad772c
Compare
added 2 commits
November 8, 2022 18:02
When the input program includes non-aligned memory accesses the decision procedure is passed expressions including byte_extract and byte_update operators. To support such programs in the decision procedure we need to lower such operators to operators we support.
esteffin
force-pushed
the
esteffin/byte-extraction-update-2
branch
from
6ad772c to
424bed5
Compare
thomasspriggs
approved these changes
Nov 8, 2022
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.
This PR adds support for byte_extract_exprt and byte_update_exprt for the new incremental SMT backend.