-
Notifications
You must be signed in to change notification settings - Fork 143
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
#badjumpdest? (Sorts K and NullStack incompatible) #192
Comments
I'm pretty sure this error has to with the #badJumpDest? rule, specifically clauses like this:
seem to be comparing JUMPDEST (with sort NullStackOp) with a general OP (of sort K) |
Hmmmm, we could add extra operator |
@MrChico I'm trying some other optimizations on another branch (just local for now), but I'm running into a (potentially) similar issue. Can you try changing |
Yes, @ehildenb , I did some experimentation with that before which did change the example. After spending some time thinking about this, my hypothesis is that this mainly becomes an issue in trying to prove very general specs that end up having the jumpdestination as a symbolic value, forcing K to evaluate whether an OP-code at an arbitrary position is a JUMPDEST or not. Another behavior I just noticed with #badjumpdest is that there is an unnecessary branching when checking #badJumpDest?[JUMPI ], see screenshots from @mhhf 's kdebugger (WIP) |
@yzhang90 has noticed the same. You can try out branch |
I believe this was solved by delaying checking for bad jump destinations until we semantic execution time (instead of a pre-check). |
We are trying to make the following circularity claim: https://github.com/dapphub/verified-smart-contracts/blob/dappsys/dappsys/exp-naive-circ-spec.k
but are given the following error
Does this error stem from something wrong in our spec? It looks like an error that has to do with the internal workings of K...
The text was updated successfully, but these errors were encountered: