Use the SMT solver to convert symbolic to concrete value(s) #629
Conversation
| pathconds <- use #constraints | ||
| query $ PleaseGetSol ewordExpr pathconds $ \case | ||
| Just concVal -> do | ||
| assign #result Nothing |
There was a problem hiding this comment.
Can you remind me what is #result and why do you need to assign it here?
There was a problem hiding this comment.
Honestly, that's the ONE thing I don't understand. But that result definitely needs to be set. I'd need to dig deeper what that thing really is. If I don't set it, it never advances the PC (program counter) and we go into an infinite loop.
There was a problem hiding this comment.
Maybe it should be cleared to Nothing even when it fails, actually, so not only here Just concVal -> ... but also at Nothing -> ... It's a bit mysterious. I think it contains the thing it's currently doing, and normally it's Nothing, but when something needs to happen, then it gets set to something like HandleEffect, or when it fails, VMFailure
There was a problem hiding this comment.
Let me see if we need to assign Nothing there, too. I have a feeling that we do, actually.
Thanks! I'll double-check this |
Description
This uses an SMT solver to solve a symbolic value. If it can ONLY be solved into a single value, then it gives that back and we can continue running. This should get rid of a number of cases where we run in to symbolic expression(s) for JUMP (but also other cases, see [1]). Note that the architecture is such that it should be possible to eventually move to a version where more than one solution is possible and so we branch out to explore all. That should fix the issue with #581 . In fact, this code can compute one of the potential addresses (or all addresses), and jump to the first (or any), but with probably small changes, it can support everything needed for #581 That would be really cool, and may make @charles-cooper happy 😄
Currently, if more than one value is possible, the result is still as before -- we output a warning and don't continue at all. Obviously, this is suboptimal, and will change with an upcoming PR. If no value at all is possible, that means we are already in an UNSAT branch, and the execution should stop. That should also be an upcoming PR. Currently, we also handle that with the warning, as before.
In other words, I think this PR is basically the beginning of something a bit more serious :) I hope you like it!
[1] I have bumped into a case where we got a symbolic expression for the cheatcode ABI. This PR fixes that too -- if the ABI can only be a single value, it will now simply work.
Checklist