Overapproximate staticcall in case we can't resolve callee #620
Conversation
76d8ff2 to
b34f4f8
Compare
44e4323 to
af12cba
Compare
src/EVM.hs
Outdated
| -- overaapproximate by returning a symbolic value | ||
| freshVar <- use #freshVar | ||
| assign #freshVar (freshVar + 1) | ||
| pushSym (Var ("staticcall-result-stack-" <> (pack . show) freshVar)) |
There was a problem hiding this comment.
this symbol is the 0 or 1 returned by the staticcall right? Would it be useful to constraint it to those values?
There was a problem hiding this comment.
OH WOW, yes! Ill do it in the next 2h!
There was a problem hiding this comment.
Really-really cool find! I now added a constraint, and I also added a testcase, using YUL, to check that the return value is indeed constrained to 0/1:
uint success;
assemby {
...
success := staticcall(
gas(), // Forward all available gas
inputAddr, // Address to call
callData, // Input data location
68, // Input data size (4 bytes for function signature + 32 bytes each for x and y)
0, // Output data location (0 means we don't care about the output)
0 // Output data size
)
}
assert(success <= 1);This yul code is the only way to actually check that the returned value is constrained -- Solidity only allows you to assign the return value to a bool, and so it can't be checked (AFAIK?). Without the constraint, the above actually could fail. With the constraint, the above always succeeds -- since success cannot be larger than 1. So the constraint is there, and is effective, as checked by this test case.
Thanks for this!!
Co-authored-by: Emilio López <2642849+elopez@users.noreply.github.com>
Co-authored-by: Emilio López <2642849+elopez@users.noreply.github.com>
It can only be 0/1, as spotted by @elopez. Thanks! Also adding a test case that specifically checks for this
| @@ -2060,10 +2060,197 @@ tests = testGroup "hevm" | |||
| } | |||
| } | |||
| |] | |||
| let sig = Just (Sig "checkval(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256]) | |||
There was a problem hiding this comment.
This was actually an incorrect test case. Fixed.
Description
Overapproximate returned state when we can't figure out STATICCALL callee. In this case, set
returndataand the top of the stack to a symbolic value. Note that there are two cases we need to do fallback actions. Once when the address can't be forced into a (potentially symbolic) address, which is the "trivial"Nothingcase. However, when it can be forced, and the symbolic address is present in theenv.contracts, we should resolve and use it. Otherwise, we should fallback. So there are in fact two cases we should call fallback. Hence, I created a function to check if the address can be resolved, and check insideNothing.I also fixed a test and added tests specific for this use-case.
Checklist