Simple loop invariants #1022
Merged
Simple loop invariants #1022
Conversation
This file contains 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
generated inside the memory model.
broadly-applicable feature based directly on loop invariants.
robdockins
force-pushed
the
rwd/simple-loop-invariant
branch
from
713996b
to
4d94ba4
Compare
|
This feature still needs some error checking, but I think the basics are ready for review. In particular, we still need to check that the indicated loop is single-entry/single-exit, and we need to implement checking that the memory footprint is acceptable (i.e., reaches fixpoint). |
RyanGlScott
reviewed
Aug 16, 2022
travitch
reviewed
Aug 16, 2022
Comment on lines
+849
to
+860
| Set.difference | ||
| (foldMap | ||
| (\ (MapF.Pair _ e) -> | ||
| -- filter out the special "noSatisfyingWrite" boolean constants | ||
| -- that are generated as part of the LLVM memory model | ||
| Set.filter ( \ (C.Some x) -> | ||
| not (List.isPrefixOf "cnoSatisfyingWrite" | ||
| (show $ W4.printSymExpr x))) $ | ||
| Set.map (\ (C.Some x) -> C.Some (W4.varExpr sym x)) $ | ||
| (W4.exprUninterpConstants sym (bodyValue e))) | ||
| (MapF.toList (varSubst normal_substitution))) | ||
| (Set.fromList (MapF.keys (varSubst normal_substitution))) |
There was a problem hiding this comment.
This is a good candidate for factoring out with a bit of explanation
Typos and such Co-authored-by: Langston Barrett <[email protected]> Co-authored-by: Ryan Scott <[email protected]> Co-authored-by: Tristan Ravitch <[email protected]>
the loop in question. We now check the critical properties required for the fixpoint-finding procedure to work: the loop must be single-entry and have a single backedge.
RyanGlScott
reviewed
Aug 26, 2022
We don't need the widening varaibles to line up, just the shapes.
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 reworks the "simple loop fixpoint" feature to be based more directly on user-provided loop invariants instead.