Symbolic execution and search should apply rules correctly #2234
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
ttuegel
reviewed
Nov 6, 2020
ttuegel
reviewed
Nov 6, 2020
… a total clean-up
ana-pantilie
commented
Nov 10, 2020
ana-pantilie
changed the title
--strategy all is ignored…fallback' into strategy-all-ignored
ttuegel
suggested changes
Nov 17, 2020
kore/app/exec/Main.hs
Outdated
Comment on lines
350
to
351
| [ ("any", Any) | ||
| , ("all", All) |
There was a problem hiding this comment.
Because this uses an enumeration type now, there is no reason to keep the String part of the tuple.
kore/src/Kore/Exec.hs
Outdated
| -> ([Rewrite] -> [Strategy (Prim Rewrite)]) | ||
| -- ^ The strategy to use for execution; see examples in "Kore.Step.Step" | ||
| -> ExecutionMode | ||
| -- ^ The execution mode |
There was a problem hiding this comment.
I don't think this documentation is helpful. The reader can always jump to the documentation for ExecutionMode!
Suggested change
| -- ^ The execution mode |
kore/src/Kore/Step.hs
Outdated
| data Prim rewrite = Simplify | Rewrite !rewrite | ||
| {- | The program's state during symbolic execution. | ||
| -} | ||
| data ProgramState a = Start !a | Rewritten !a | Remaining !a |
There was a problem hiding this comment.
Could you please add documentation for each constructor?
kore/src/Kore/Step.hs
Outdated
| data Prim | ||
| = Begin | ||
| | Simplify | ||
| | ApplyRewrites |
There was a problem hiding this comment.
Unless this name is already taken, I suggest changing to a simple imperative verb to match the other constructors:
Suggested change
| | ApplyRewrites | |
| | Rewrite |
kore/src/Kore/Step.hs
Outdated
Comment on lines
150
to
158
| transitionRuleWorker All ApplyRewrites (Remaining patt) = | ||
| transitionAllRewrite patt | ||
| transitionRuleWorker All ApplyRewrites (Start patt) = | ||
| transitionAllRewrite patt | ||
| transitionRuleWorker Any ApplyRewrites (Remaining patt) = | ||
| transitionAnyRewrite patt | ||
| transitionRuleWorker Any ApplyRewrites (Start patt) = | ||
| transitionAnyRewrite patt | ||
| transitionRuleWorker _ ApplyRewrites state = pure state |
There was a problem hiding this comment.
We can reduce duplication with a simple helper function. Explicitly matching on all the ProgramState constructors makes the logic clearer and protects us if we ever add constructors to ProgramState.
Suggested change
| transitionRuleWorker All ApplyRewrites (Remaining patt) = | |
| transitionAllRewrite patt | |
| transitionRuleWorker All ApplyRewrites (Start patt) = | |
| transitionAllRewrite patt | |
| transitionRuleWorker Any ApplyRewrites (Remaining patt) = | |
| transitionAnyRewrite patt | |
| transitionRuleWorker Any ApplyRewrites (Start patt) = | |
| transitionAnyRewrite patt | |
| transitionRuleWorker _ ApplyRewrites state = pure state | |
| transitionRuleWorker mode ApplyRewrites (Remaining patt) = | |
| transitionRewrite mode patt | |
| transitionRuleWorker mode ApplyRewrites (Start patt) = | |
| transitionRewrite mode patt | |
| transitionRuleWorker _ ApplyRewrites state@(Rewritten patt) = pure state | |
| transitionRewrite All = transitionAllRewrite | |
| transitionRewrite Any = transitionAnyRewrite |
ttuegel
approved these changes
Nov 19, 2020
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.
Fixes #2205
Needs #2231Needs #2261Reviewer checklist
stack test --coveragestack haddock