SymExec: Pre-filter safe branches #833
Conversation
blishko
force-pushed
the
filer-safe-branches
branch
from
d63023d to
b9d64a8
Compare
Not long ago, we were pre-filtering branches that could not lead to postcondition violation. This relied on calling simplification and the constraints being simplified to [PBool False]. However, recently (in c34d4d6), the code changed and it no longer simplified the constraints before sending them further down the pipeline, and thus the statically safe branches were no longer filtered before we started asking about their feasibility. I believe we should bring back the filtering, if only to have an information about how many branches lead to Failure that we are interested in.
blishko
force-pushed
the
filer-safe-branches
branch
from
b9d64a8 to
6d644d2
Compare
msooseth
left a comment
msooseth
left a comment
There was a problem hiding this comment.
This is good!
I just want to note that the simplification and check before running the SMT solver will take place in checkSatWithProps -- it doesn't dispatch it to the SMT solver in case the concKeccak simplification returns a PBool False. That also means that the simplifications take place in a thread, concurrently so it's kinda nice. However, we do construct some Prop array and that's unnecessary. Note that in the old code, in c34d4d6 we actually simplified, too, and checked that for PBool False, so it was better than this version. However, this is much faster in many cases, I'm sure. So this is definitely an improvement, however, it's kinda different than the original code, and ultimately the PBool False will be filtered out before it hitting the SMT solver.
BTW, this could also be:
canBeSat (a, _) = not (PBool False `elem` a)
Which should be more complete I think?
Indeed, the constraints are simplified in
This is true. But I don't really think our encoding produces |
Description
Not long ago, we were pre-filtering branches that could not lead to postcondition violation. This relied on calling simplification and the constraints being simplified to [PBool False]. However, recently (in c34d4d6), the code changed and it no longer simplified the constraints before sending them further down the pipeline, and thus the statically safe branches were no longer filtered before we started asking about their feasibility.
I believe we should bring back the filtering, if only to have an information about how many branches lead to Failure that we are interested in.
Checklist