Fixing checking assert failure #753
Conversation
5b3a960 to
31a10d8
Compare
e0a2c13 to
bfcd1b0
Compare
|
OK, I think this is finally ready for review :) I added a number of test cases, and removed badVault. We can come back to badVault later. |
99c8f7a to
1a6a476
Compare
src/EVM/UnitTest.hs
Outdated
| -- We need to drop the selector (4B), the offset value (aligned to 32B), and the length of the string (aligned to 32B) | ||
| -- NOTE: assertTrue/assertFalse does not have the double colon after "assertion failed" | ||
| let assertFail = selector "Error(string)" `BS.isPrefixOf` b && "assertion failed" `BS.isPrefixOf` (BS.drop (4+32+32) b) | ||
| in if assertFail || b == panicMsg 0x01 then PBool False | ||
| else PBool True | ||
| b -> b ./= ConcreteBuf (panicMsg 0x01) |
There was a problem hiding this comment.
we should run the prefix check in the symbolic case too
|
The commit be2a5eb now also handles the symbolic case when the prefix is a concrete "assertion failed" of the symbolic string. We currently don't handle when the string returned doesn't have a concrete prefix matching "assertion failed" |
c16aca9 to
be2a5eb
Compare
src/EVM/UnitTest.hs
Outdated
| symbolicFail e = | ||
| let text = V.fromList $ map (fromIntegral . ord) "assertion failed" | ||
| panic = e == ConcreteBuf (panicMsg 0x01) | ||
| assertFail = V.take (length text) (Expr.concretePrefix e) == text |
There was a problem hiding this comment.
I don't think this is sound? What if we have a symbolic prefix that could still be "assertion failed"?
There was a problem hiding this comment.
Yeah, that would give us a false positive. But we provide the CEX, so it can be checked. I think it's not a likely problem to come up. But I'm OK with removing it, of course -- I just don't know what to put in its place. Should we just ignore this kind of symbolic fail and simply have
symbolicFail e =
let panic = e == ConcreteBuf (panicMsg 0x01)
in PBool (not panic)What do you think?
There was a problem hiding this comment.
I think that's probably fine? I would prefer to be sound as a default, I'm also fine to keep the existing concrete prefix extraction as a special case optimization and have this fully symbolic case as a fallback?
There was a problem hiding this comment.
and unless I'm misunderstanding, right now a symbolic prefix that could still be "assertion failed" would not be considered as an assertion (since concretePrefix wouldn't find it), and we would be missing potentially failing branches?
There was a problem hiding this comment.
are we even able to test this case? we probably need to use assembly actually and like pass some symbolic memory region into revert directly?
There was a problem hiding this comment.
I had a go at this :) Can you please check if it's what you were thinking of?
The test case I will write later, good catch!
7fe1166 to
6d3b75c
Compare
20e5dd2 to
da3dd14
Compare
|
TODO: add tests cases -- especially for symbolic return values. |
4d4b984 to
b10e62e
Compare
require(bool,string) was also considered a FAIL, and revert(string) also, etc. Also added a number of tests for all of these.
Adding a note about checkAssertions Ooops
b10e62e to
a266a8b
Compare
a266a8b to
cd2bf74
Compare
cd2bf74 to
c6c5927
Compare
Description
As per discussion on the public matrix channel and the issue #751 we have a problem with
revert()/revert("message")/assertintest` mode. Fixes:require(a==b, "str")is no longer considered a FAILrevert(string)is no longer considered a FAILAs before, all
assert-s are considered a FAIL. Also, as before,revert()is not considered a fail.The
badVaultcode seems to PASS now. It used to fail on therequire(stuff, "string")which should not have been a cause for FAIL. It may actually be a good vault, and so maybe the PASS is correct.We now also print a yellow WARNING in case it's FAIL because of Cex or Warnings -- but ALSO everything reverted. So at least we indicate that there's more than just the issue with the FAIL.
Checklist