Skip to content

Backend responding with #Bottom makes the proof crash #22

@iFrostizz

Description

@iFrostizz

When the backend returns #Bottom, pyk sometimes crashes.
It originates when converting from kore to kast and fails when converting from kast to a CTerm in this function: https://github.com/runtimeverification/pyk/blob/ae809ee638103862cae101433c8f4a68708cf091/src/pyk/cterm.py#L50
And crashes when it reaches that point: https://github.com/runtimeverification/pyk/blob/ae809ee638103862cae101433c8f4a68708cf091/src/pyk/kast/manip.py#L261
An example of a response that triggers that crash is

{"jsonrpc":"2.0","id":56,"result":{"reason":"stuck","depth":377,"state":{"term":{"format":"KORE","version":1,"term":{"tag":"Bottom","sort":{"tag":"SortApp","name":"SortGeneratedTopCell","args":[]}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Bottom","sort":{"tag":"SortApp","name":"SortGeneratedTopCell","args":[]}}}}}}

which boils down to as kast to

KApply(
    label=KLabel(name='#And', params=(KSort(name='GeneratedTopCell'),)),
    args=(
        KApply(label=KLabel(name='#Bottom', params=(KSort(name='GeneratedTopCell'),)), args=()),
        KApply(label=KLabel(name='#Bottom', params=(KSort(name='GeneratedTopCell'),)), args=()),
    ),
)

It seems that this is not an issue on the booster backend, because the execution can be continued past that point while this branch becomes stuck and fail at a later point (due a bug that is probably not related).
It may be because of the new case of returning #Bottom for vacuous nodes: runtimeverification/haskell-backend#3637 and may not correctly be handled on pyk.
cc @goodlyrottenapple

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions