Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Abort when Kore's simplifier throws
DecidePredicateUnknown
(#392)
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 <goodlyrottenapple@gmail.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com>
- Loading branch information