Skip to content

Branch returned although one of the next states simplifies to #bottom #3764

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
1 of 2 tasks
jberthold opened this issue Apr 10, 2024 · 2 comments
Open
1 of 2 tasks
Assignees

Comments

@jberthold
Copy link
Member

jberthold commented Apr 10, 2024

On slack, Petar reported a problem where a branch result returned by (both kore-rpc and) kore-rpc-booster contains two next-states, but one of them simplifies to #Bottom with an isolated simplify request.
This is caused by kore-rpc execution not discovering the #Bottom-ness of this state, otherwise execution would continue.

Observed behaviour:

  • Execution stops and a Branching result is returned. One of the states in next-states simplifies to #Bottom in a subsequent simplify request.

Expected behaviour:

  • Execution should continue with the non-bottom alternative of the branch.
  • to protect against this behaviour in kore-rpc-booster, modify the postExecSimplify mechanism to detect this case and continue execution.
  • reproduce this result with kore-rpc and investigate why the bottom state is not found
@jberthold jberthold self-assigned this Apr 10, 2024
@jberthold jberthold added the booster Relates to booster code label Apr 10, 2024
@jberthold jberthold removed the booster Relates to booster code label Apr 11, 2024
@jberthold
Copy link
Member Author

There were once known issues with spurious branches at depth 0 in kore-rpc earlier, so this behaviour should be tested this with a noop step before the branch, too. The reason appears to be that the simplifier is not called for branch results at depth 0. This should be investigated.

@jberthold
Copy link
Member Author

I have confirmed with tests that in this case, it makes no difference whether kore-rpc has performed an execution step before the bogus Branching result is obtained.

jberthold added a commit that referenced this issue Apr 15, 2024
…3765)

Part of #3764 (work-around in booster, not fixing kore)

When `kore-rpc` returns a `Branching` result where all but one of the
branches are actually `#Bottom` (when simplified), execution in
`kore-rpc-booster` should continue.
Such a case was observed in the wild, see #3764
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant