GillianPlatform / Gillian

The Gillian Platform main repository
https://GillianPlatform.github.io
BSD 3-Clause "New" or "Revised" License
73 stars 11 forks source link

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

Closed NatKarmios closed 5 months ago

NatKarmios commented 6 months ago

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.

giltho commented 6 months ago

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 commented 6 months ago

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 commented 6 months ago

Oh!

NatKarmios commented 5 months ago

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