This repository has been archived by the owner on Apr 25, 2024. It is now read-only.
Make KCFGExplore aware of aborting requests due to unknwon predicates #744
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
rv-jenkins
added a commit
to runtimeverification/hs-backend-booster
that referenced
this pull request
Dec 8, 2023
Fixes #373 This PR makes `kore-rpc-booster` return `"execute"` responses with `"reason": "aborted"` in cases when Kore's simplifier fails due to `DecidePredicateUnknown` in the post-exec simplification in `Proxy.hs`. **Scenario before** ``` "execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> JsonRpcError` ``` returning `JsonRpcError` resulted in loosing information gained by executing in booster for X steps + in kore for up to 1 step. **Scenario now** ``` "execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> ExecuteResult {reason=Aborted, unknownPredicate = <predicate>}` ``` this this change, we return the reached state (may be branching) and do not lose information anymore. Additionaly, we return the unknown predicate, so that `pyk` can decide what to do with these. PR to `pyk` that takes advantage of this feature by intrroducing `Undecided` nodes to KCFG: runtimeverification/pyk#744 --------- Co-authored-by: Samuel Balco <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
Merged
geo2a
force-pushed
the
georgy/prettier-unknown
branch
from
a07ca0a to
67cbf36
Compare
|
@tothtamas28 I've updated this PR following the merge of #773. Could you have a look? |
|
@palinatolmach this PR integrates the unknown predicate information that is returned by |
jberthold
pushed a commit
to runtimeverification/haskell-backend
that referenced
this pull request
Apr 10, 2024
Fixes runtimeverification/hs-backend-booster#373 This PR makes `kore-rpc-booster` return `"execute"` responses with `"reason": "aborted"` in cases when Kore's simplifier fails due to `DecidePredicateUnknown` in the post-exec simplification in `Proxy.hs`. **Scenario before** ``` "execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> JsonRpcError` ``` returning `JsonRpcError` resulted in loosing information gained by executing in booster for X steps + in kore for up to 1 step. **Scenario now** ``` "execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> ExecuteResult {reason=Aborted, unknownPredicate = <predicate>}` ``` this this change, we return the reached state (may be branching) and do not lose information anymore. Additionaly, we return the unknown predicate, so that `pyk` can decide what to do with these. PR to `pyk` that takes advantage of this feature by intrroducing `Undecided` nodes to KCFG: runtimeverification/pyk#744 --------- Co-authored-by: Samuel Balco <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
jberthold
pushed a commit
to runtimeverification/haskell-backend
that referenced
this pull request
Apr 10, 2024
Fixes runtimeverification/hs-backend-booster#373 This PR makes `kore-rpc-booster` return `"execute"` responses with `"reason": "aborted"` in cases when Kore's simplifier fails due to `DecidePredicateUnknown` in the post-exec simplification in `Proxy.hs`. **Scenario before** ``` "execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> JsonRpcError` ``` returning `JsonRpcError` resulted in loosing information gained by executing in booster for X steps + in kore for up to 1 step. **Scenario now** ``` "execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> ExecuteResult {reason=Aborted, unknownPredicate = <predicate>}` ``` this this change, we return the reached state (may be branching) and do not lose information anymore. Additionaly, we return the unknown predicate, so that `pyk` can decide what to do with these. PR to `pyk` that takes advantage of this feature by intrroducing `Undecided` nodes to KCFG: runtimeverification/pyk#744 --------- Co-authored-by: Samuel Balco <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
jberthold
pushed a commit
to runtimeverification/haskell-backend
that referenced
this pull request
Apr 10, 2024
Fixes runtimeverification/hs-backend-booster#373 This PR makes `kore-rpc-booster` return `"execute"` responses with `"reason": "aborted"` in cases when Kore's simplifier fails due to `DecidePredicateUnknown` in the post-exec simplification in `Proxy.hs`. **Scenario before** ``` "execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> JsonRpcError` ``` returning `JsonRpcError` resulted in loosing information gained by executing in booster for X steps + in kore for up to 1 step. **Scenario now** ``` "execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> ExecuteResult {reason=Aborted, unknownPredicate = <predicate>}` ``` this this change, we return the reached state (may be branching) and do not lose information anymore. Additionaly, we return the unknown predicate, so that `pyk` can decide what to do with these. PR to `pyk` that takes advantage of this feature by intrroducing `Undecided` nodes to KCFG: runtimeverification/pyk#744 --------- Co-authored-by: Samuel Balco <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
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 incorporates the information provided by
kore-rpc-boosterin anAbortedResult, which is returned now when the execute request has to be aborted due to a predicate that Z3 returns "unknown" on.Pending tasks:
kore-rpc-booster: Abort when Kore's simplifier throwsDecidePredicateUnknownhs-backend-booster#392Undecidednode. A very low--smt-timeoutcould be helpful.