dapphub / dapphub/dapptools

hevm weird reverts

Open
#844 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
Haskell
Stars
2.1k
Forks
320
PR merge metrics
No merged PRs in 30d

Description

```
pragma solidity ^0.8.6;

import "ds-test/test.sol";

contract HevmbugTest is DSTest {

// Passes
function prove_dog(uint8[255] memory dog) public {}
// Reverts
function prove_cat(uint8[256] memory cat) public {}

// Passes
function prove_egg(uint8 egg) public {}
// Reverts
function prove_cheese(bytes1 cheese) public {}
}

$ dapp test
```

So there are a few weird things here.

- In the first group, things get weird when the length > 1 byte. This also happens for `bytes1`.

```
Failure: prove_cat(uint8[256])

Counterexample:

result: Revert
calldata: prove_cat([256, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])
```

I'm not sure what to make of this cex calldata. It looks like it's trying to show a structured cex following the Solidity type (static array), but it also shows the length in the first byte *[ohhhh] which is the case in the actual calldata byte stream but not in the structured case.
[ohhhh] When writing the above it occurred to me that maybe the length is being added as the first byte, but since it's > 1 byte maybe the length check fails??

- In the second part, the `uint8` version passes, whereas the `bytes1` version reverts with

```
Failure: prove_cheese(bytes1)

Counterexample:

result: Revert
calldata: prove_cheese(«»)
```
The cex calldata seems to point to hevm thinking the calldata is dynamic here, and empty in this case. However that's not possible since `bytes1` is a value type (same as `uint8` as far as the ABI is concerned).

Contributor guide

No contributing guide indexed for this repository

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.