New CopySlice rule that helps to avoid symbolic copyslice in case of overapproximation #667
Conversation
msooseth
changed the title
msooseth
force-pushed
the
no-overapprox-when-good-test
branch
2 times, most recently
from
e7e12a9 to
c76eaa2
Compare
msooseth
changed the title
msooseth
force-pushed
the
no-overapprox-when-good-test
branch
2 times, most recently
from
4c2ee69 to
ce5edb7
Compare
msooseth
force-pushed
the
no-overapprox-when-good-test
branch
from
ce5edb7 to
a0c1517
Compare
| -- go (CopySlice (Lit 0) (Lit 0) (BufLength (AbstractBuf k1)) | ||
| -- (CopySlice (Lit 0) (Lit 0) (BufLength (AbstractBuf k2)) (AbstractBuf k3) _) | ||
| -- (ConcreteBuf "")) | k1 == k2 && k2 == k3 = (AbstractBuf k1) | ||
| , test "overapproximates-undeployed-contract" $ do |
There was a problem hiding this comment.
Can this test be merged with the previous one?
It is doing the same work, no?
Only checks on the result are different.
There was a problem hiding this comment.
Actually, they are different, weirdly enough! The one above actually works without the simplifications. But this one does not. It's because Target was not deployed in this case, so it's abstracted over. Since we are not running a forge test, we don't have a setUp() and nothing is set up, so mm is actually not deployed. Weird, but true.
There was a problem hiding this comment.
Oh, I see now.
Yeah, that's pretty weird.
The state variable mm is never assigned.
Won't the variable have always value 0? Shouldn't we that call mm.get is always trying to call function on address 0?
There was a problem hiding this comment.
Oh good point, it is trying to call address 0. But there is nothing at 0, so it overapproximates. Which is OK in this case, I think. Although we could emit a warning for call to address zero. Let me create an issue to track this. Would be hepful to emit a warning probably. It can happen, but in this case, we can't really do much about it. However, it is likely unintended.
In the meanwhile, I'm merging, with a note that this is address 0, and the contract is obviously not deployed there...
There was a problem hiding this comment.
Documented here: #671
There was a problem hiding this comment.
One last note, sorry for distracting you.
But, if we know the call is to zero address, we know that it will revert, no?
I don't know if I understand correctly how EVM works, but the call will lead to revert, so the assertion will not be reached, no?
It seems to me from your description that the counterexamples show how the assertion can be reached, but these are spurious, no?
Let me know if I am misunderstanding something.
There was a problem hiding this comment.
Yeah, good point. This is getting to be bigger than I wanted... can we merge this and document that as part of #671 ?
There was a problem hiding this comment.
It's getting to be too much to keep in mind and work on at the same time...
Co-authored-by: Martin Blicha <[email protected]>
Co-authored-by: Martin Blicha <[email protected]>
|
Thanks for the review! Let me think about my idea to track that zero address as an issue to be addressed separately and then we can hopefully merge this :) |
Description
This allows us to skip the symbolic copyslice. Basically it's copying over a EMPTY concretebuf values that have been copied from an abstractbuf and ONLY those values. So the result is just the abstractbuf! This helps a lot in avoiding sybmolic copyslice.
Checklist