Skip to content
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

When debugging, fresh s-vars can break G_Interpreter #278

Closed
NatKarmios opened this issue Mar 13, 2024 · 4 comments · Fixed by #279
Closed

When debugging, fresh s-vars can break G_Interpreter #278

NatKarmios opened this issue Mar 13, 2024 · 4 comments · Fixed by #279
Assignees
Labels
bug Something isn't working debugger Relating to Gillian's debugger

Comments

@NatKarmios
Copy link
Contributor

This WISL code causes an error when debugging:

fresh x;
assume (x > 0);

This is because the internal function for > dynamically checks types, and since x is completely unrestricted, the branch for it being a list is sat, but then errors as it's being compared to an int.
This should be reported as an error during lifting, but the error result is somehow lost in the interpreter, and can't be found when trying to step.

@NatKarmios NatKarmios added bug Something isn't working debugger Relating to Gillian's debugger labels Mar 13, 2024
@NatKarmios NatKarmios self-assigned this Mar 13, 2024
@giltho
Copy link
Contributor

giltho commented Mar 13, 2024

This is because expression evaluation is not allowed to error in GIL, while it should.
The signature of expression evaluation is basically Store.t -> Expr.t -> Val.t, when it should be Store.t -> Expr.t -> Val.t result. In case where it fails, Gillian just crashes instead of propagating the error.

@NatKarmios
Copy link
Contributor Author

NatKarmios commented Mar 13, 2024

I think we fixed this before when it was a general engine problem; running this code under regular WPST works fine, it gives the expected result.
This problem seems to only pop up when debugging, so I think it's something specific to how G_Interpreter stores confs or results in this context (read: I think it's my fault 😛).

@giltho
Copy link
Contributor

giltho commented Mar 13, 2024

Oh!

@NatKarmios
Copy link
Contributor Author

So! It turns out that #270 just broke any errors being displayed in the debugger :)
Fixed in #279

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working debugger Relating to Gillian's debugger
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants