SymEx: Always require postcondition in verify* methods #900
Conversation
blishko
force-pushed
the
symex-cleanup
branch
from
7c99d64 to
f2412c2
Compare
msooseth
left a comment
msooseth
left a comment
There was a problem hiding this comment.
LGTM! I added a comment, more as a reminder than anything else :)
| exploreContract :: forall m . App m | ||
| => SolverGroup | ||
| -> Maybe Fetch.Session | ||
| -> ByteString | ||
| -> Maybe Sig | ||
| -> [String] | ||
| -> VeriOpts | ||
| -> Maybe (Precondition RealWorld) | ||
| -> Maybe (Postcondition RealWorld) | ||
| -> m (Expr End, [VerifyResult]) | ||
| verifyContractWithSession solvers sess theCode signature' concreteArgs opts maybepre maybepost = do | ||
| -> m (Expr End) | ||
| exploreContract solvers theCode signature' concreteArgs opts maybepre = do | ||
| calldata <- mkCalldata signature' concreteArgs | ||
| preState <- liftIO $ stToIO $ abstractVM calldata theCode maybepre False | ||
| let fetcher = Fetch.oracle solvers sess opts.rpcInfo | ||
| verify solvers fetcher opts preState maybepost | ||
| let fetcher = Fetch.oracle solvers Nothing opts.rpcInfo | ||
| executeVM fetcher opts.iterConf preState | ||
|
|
There was a problem hiding this comment.
this is only used in one test. It will also need to be removed when we return an [Expr End], rather than an Expr End with a bunch of ITE's in it. So we can also remove it now, if you like, along with the test.
There was a problem hiding this comment.
We can keep it for now and remove/adjust later.
|
I guess I should add a changelog entry, since we are changing the signature of a function exposed to the outside world. |
I think we should always add a changelog entry unless it's a trivial PR :) But yeah. And then we can merge :) |
To make the core method simpler we always require postcondition to be given. If there is no postcondition, we are not really "verifying". However, there is a use case where we don't want to verify anything, we just want to explore a contract. For such use case, we provide a new helper method to do exactly that. `exploreContract` executes the contract symbolically, and returns its Expr representation.
blishko
force-pushed
the
symex-cleanup
branch
from
f2412c2 to
dbc6476
Compare
Description
To make the core method simpler we always require postcondition to be given.
If there is no postcondition, we are not really "verifying". However, there is a use case where we don't want to verify anything, we just want to explore a contract.
For such use case, we provide a new helper method to do exactly that.
exploreContractexecutes the contract symbolically, and returns its Expr representation.Checklist