Fix packed array of bytes1 #920
Conversation
Update comment Fix Update changelog
|
Why this is a partial fix? |
|
@gustavo-grieco only because it doesn't remove the trailing zeros... not sure they must be removed, but they probably could be removed. Either way, it definitely fixes the bigger issue, and the printing of the output will allow a user to just send in the counterexample that is short. |
| mstore(0x40, add(dataPtr, dataLen)) | ||
|
|
||
| // Perform the low-level call | ||
| success := call(gas(), target, 0, dataPtr, dataLen, 0, 0) |
There was a problem hiding this comment.
Can you explain what is this going to call?
There was a problem hiding this comment.
@gustavo-grieco came up with this example, I just copied it :)
@gustavo-grieco can you maybe give some context?
There was a problem hiding this comment.
I think the idea is to call inc()
There was a problem hiding this comment.
Yes, it calls inc in order to violate
assert(state == 0);
because:
cast keccak "inc()"
0x371303c051bff726100ad13871cababf50c20dd920fca137e519f98f089a74b4And indeed the correct CEX, is:
0x37, 0x13, 0x03, 0xc0
Which are the first 4 bytes of that keccak, i.e. the function selector.
So the idea is for the system to calculate the function it needs to call that increments the state so that the state == 0 no longer holds.
There was a problem hiding this comment.
OK, I now added this to the code, can you check again?
There was a problem hiding this comment.
Yes, this is correct. This was an experiment to make hevm/echidna run a symbolic transaction and perform some checks after that (e.g. calling a functions with no parameters). It can be generalized to more transactions.
Fixing indentation
msooseth
force-pushed
the
Fixing-RPC
branch
2 times, most recently
from
e022669 to
980d0a1
Compare
Update Update
| // Perform the low-level call | ||
| // this should call the inc() function, which has selector: | ||
| //``` | ||
| //cast keccak "inc()" | ||
| //0x371303c051bff726100ad13871cababf50c20dd920fca137e519f98f089a74b4 | ||
| //``` | ||
| // which happens to have the first 4 bytes as | ||
| // 0x37, 0x13 0x03, 0xc0 | ||
| // This will increment `state` by 1, thereby violating the property | ||
|
|
||
| success := call(gas(), target, 0, dataPtr, dataLen, 0, 0) |
There was a problem hiding this comment.
Oh, I see, this basically just calls this contract again, with the calldata passed in as argument to this function.
So the number 36 is rather arbitrary here, no?
4 would be sufficient, since we only need the selector (which has 4 bytes) to be able to call inc, no?
Why was 36 chosen as the magic number?
There was a problem hiding this comment.
Yes, sorry, the 36 was selected to allow at least one parameter, but here it can be reduced.
|
Ooops: and: |
|
I confirm this problem is not reproducible on main, so it must be introduced here. |
|
Yes, I know. I am working on it. |
This partially addresses #917 The issue is that bytes
bytes1[36]is packed as per ABI spec. From the ABI documentation: https://docs.soliditylang.org/en/latest/abi-spec.html#formal-specification-of-the-encodingHowever, we treated it as a regular Array, which is padded to 32B for each element.
Description
Checklist