Symbolic execution queue #906
Conversation
msooseth
force-pushed
the
queue-symbolic-exec5
branch
2 times, most recently
from
bd18f0e to
b07c460
Compare
Cleanup More generic interpret Update Making progress Making progress Update Update Update Making progress Update Now typecheck Update Making progress Update Better now Making progress Update Typechecks now Update Better Some improvement? Better I think Update Update Making progress Update to fix changes Fixing Update Better Let's hope this works Cleaner Update Update Less noise Update Much better Update Fixing Update Update Update QED change Qed fixing still Fixed Qed Update to fix cli Ooops, fixing bug Better printing Cleanup Cleanup Cleanup Cleanup Trying to rebase on top of main Add changelog Less braces Less change Much better display
msooseth
force-pushed
the
queue-symbolic-exec5
branch
from
b07c460 to
96bb9cd
Compare
Thanks to @blishko for pointing these out
msooseth
force-pushed
the
queue-symbolic-exec5
branch
from
8d67a30 to
e068dc1
Compare
blishko
left a comment
blishko
left a comment
There was a problem hiding this comment.
Looks good!
I left a few comments and questions.
src/EVM/SymExec.hs
Outdated
| conf <- readConfig | ||
| (ra, vma) <- liftIO $ stToIO $ runStateT (continue v) frozen { result = Nothing, exploreDepth = newDepth } | ||
| let vmConst = vma { constraints = (PEq v expr) : vma.constraints } |
There was a problem hiding this comment.
The first three lines are the same in both cases. Maybe we can split the cases only after the common point?
Also, we now add a constraint to the constraints of the VM, but we did were not doing that before.
I actually think this is correct!
Seems like previously we might have been missing some information?
There was a problem hiding this comment.
Ah shit. It's already added here:
pushTo #constraints $ Expr.simplifyProp (addrExpr .== val)
for runAllPaths. Same for runBothPaths:
runBothPaths loc _ (Case v) = do
assign #result Nothing
pushTo #constraints $ if v then Expr.simplifyProp (Lit 0 ./= condSimpConc)
else Expr.simplifyProp (Lit 0 .== condSimpConc)
So adding the constraint is not needed I think. Removing.
There was a problem hiding this comment.
Wow... that thing was wrong. This: Expr.simplifyProp (Lit 0 ./= condSimpConc) when replaced by PNeg (PEq (Lit 0) cond) it actually works. Otherwise, nope. Ooops. Fixing. And then we can remove adding this condition, since it's added correctly by all continue-s, i.e. for runAllPaths and for runBothPaths. Nice, thanks!
There was a problem hiding this comment.
Regarding the shared code... I think they are subtly different? I nevertheless tried to contract things, especially around newT. Let me know what you think!
Co-authored-by: blishko <[email protected]>
Co-authored-by: blishko <[email protected]>
blishko
left a comment
blishko
left a comment
There was a problem hiding this comment.
I think this looks good!
Can you rebase on top of current main?
I think you will have to remove some RealWorld parameters to be compatible with current main.
I would like to run a few experiments afterwards to have some performance numbers.
yes plz |
Done! I merged main into this, which is sometimes easier to do. Looks very similar anyway in the git history. I hope it's good :) We can also squash-merge (when merging the PR), if you like, then it will look like a single commit. |
|
(oops, my merge was a bit bad, sorry, I'll fix soon) |
Fixing Fixing
msooseth
force-pushed
the
queue-symbolic-exec5
branch
from
802d0c3 to
0ba7790
Compare
|
I have now fixed the biggest issue. I'll fix the 2 tests that fail tonight when I have more time & better internet. |
Description
A queue for symbolic execution threads. Currently the number of processors, but should be easy to adjust. Returns
[Expr End], and now theITEis gone. When asking for reachability, we return a full set of leafs (i.e.Expr End-s). All tests pass.Checklist