fix bug in or patterns when used outside of a rewrite #340
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
traiansf
approved these changes
Mar 8, 2019
ehildenb
approved these changes
Mar 8, 2019
This was referenced Mar 18, 2024
Baltoli
pushed a commit
that referenced
this pull request
Apr 9, 2024
Currently, if we have a proof that reaches a branch-point, and the pre-branch state is subsumed into the target state, it will still compute the branches, and then check each post-branch state individually for subsumption into the target state. The branches are still subsumed into the target, but it makes the KCFG more complicated because it has the uneeded branch there. This PR: - Adds a test where subsumption happens at a branch point, and fails because we set it to only do one iteration of extending the prover (passes after these changes). - Factors out the final subsumption check into its own routine, and calls it on new frontier nodes as well as on new pre-branch nodes. - Adds a helper getter `CTerm.cell(...)` as a shortcut to `get_cell(CTerm.config, ...)` - Removes the unused parameter `simplify_init` to `AGProver.advance_proof(...)`. It has been tested on [this proof](https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/mcd/vat-addui-pass-spec.k), which is subsumed right at the branch point, and does indeed produce a smaller KCFG. This proof was introduced by @dkcumming in order to work on proof-reuse in the larger still-failing proofs in KEVM test-suite. With this change, we reduce the branching factor of the proof from 6 to 3. The overall runtime goes from ~4min to ~3min40s (not much change), and the number of queries to the RPC server goes from 26 to 25 (not much change). Overall this will increase the number of implication checks we make, but still not nearly as many as the original prover made. The test added fails before the change because with `--max-iterations=1` set, it never makes it to checking subsumption into the target state once it hits the branch point on the `if(...) ...` statement. But with this change, it checks subsumption into the target state as soon as it's made the first basic block, and the proof is discharged. --------- Co-authored-by: devops <devops@runtimeverification.com>
Baltoli
pushed a commit
that referenced
this pull request
Apr 9, 2024
Currently, if we have a proof that reaches a branch-point, and the pre-branch state is subsumed into the target state, it will still compute the branches, and then check each post-branch state individually for subsumption into the target state. The branches are still subsumed into the target, but it makes the KCFG more complicated because it has the uneeded branch there. This PR: - Adds a test where subsumption happens at a branch point, and fails because we set it to only do one iteration of extending the prover (passes after these changes). - Factors out the final subsumption check into its own routine, and calls it on new frontier nodes as well as on new pre-branch nodes. - Adds a helper getter `CTerm.cell(...)` as a shortcut to `get_cell(CTerm.config, ...)` - Removes the unused parameter `simplify_init` to `AGProver.advance_proof(...)`. It has been tested on [this proof](https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/mcd/vat-addui-pass-spec.k), which is subsumed right at the branch point, and does indeed produce a smaller KCFG. This proof was introduced by @dkcumming in order to work on proof-reuse in the larger still-failing proofs in KEVM test-suite. With this change, we reduce the branching factor of the proof from 6 to 3. The overall runtime goes from ~4min to ~3min40s (not much change), and the number of queries to the RPC server goes from 26 to 25 (not much change). Overall this will increase the number of implication checks we make, but still not nearly as many as the original prover made. The test added fails before the change because with `--max-iterations=1` set, it never makes it to checking subsumption into the target state once it hits the branch point on the `if(...) ...` statement. But with this change, it checks subsumption into the target state as soon as it's made the first basic block, and the proof is discharged. --------- Co-authored-by: devops <devops@runtimeverification.com>
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.
There was a bug where or patterns were appearing on the rhs of rules when an or pattern was used outside of a rewrite, despite them not being syntactically valid there. This fixes that issue by introducing a compiler pass that guards or patterns with an #as pattern so that or patterns used outside of any rewrite have an unambiguous substitution on the rhs.
We also fix a bug where anonymous variables could not be used in or patterns in the ocaml backend because of a compiler error in ocaml.