dapphub / dapphub/dapptools

Symbolic execution tests passing in arguments outside the range of the typed parameter

Open
#899 1 comment 1 reaction 0 assignees View on GitHub
Dominant language
Haskell
Stars
2.1k
Forks
320
PR merge metrics
No merged PRs in 30d

Description

tl;dr - If a symbolic execution "prove" test is set up with a `int128` parameter, `int256` numbers are being passed in causing it to revert

For my example, I cloned the [gakonst dapp-tools template](https://github.com/gakonst/dapptools-template) and added one simple test to the `Greeter.t.sol` file:
```
function provePleaseDontFail(int128 x) public {
// hello (note: I've also tried other stuff in here like `assertTrue(true);` but it never reaches this code)
}
```

Heres the result of running that test -- note at end we see that the reverting case was `170141183460469231731687303715884105728` (hex `0x80000000000000000000000000000000`) which is 1 greater than `type(int128).max`)

```
~/dev/dapptools-template $ dapp test -v 3 -m provePleaseDontFail
+ dapp clean
+ rm -rf out
Running 1 tests for src/test/Greeter.t.sol:Greet
[FAIL] provePleaseDontFail(int128)

Failure: provePleaseDontFail(int128)

Counterexample:

result: Revert
calldata: provePleaseDontFail(170141183460469231731687303715884105728)

src/test/Greeter.t.sol:Greet
├╴constructor
├╴setUp()
│ ├╴create Greeter@0xCe71065D4017F316EC606Fe4422e11eB2c47c246 (src/test/utils/GreeterTest.sol:35)
│ │ ├╴OwnershipTransferred() (lib/openzeppelin-contracts/contracts/access/Ownable.sol:69)
│ │ └╴← 3099 bytes of code
│ ├╴create User@0x185a4dc360CE69bDCceE33b3784B0282f7961aea (src/test/utils/GreeterTest.sol:36)
│ │ └╴← 1012 bytes of code
│ ├╴create User@0xEFc56627233b02eA95bAE7e19F648d7DcD5Bb132 (src/test/utils/GreeterTest.sol:37)
│ │ └╴← 1012 bytes of code
│ └╴call Greeter::transferOwnership(address)(User@0x185a4dc360CE69bDCceE33b3784B0282f7961aea) (src/test/utils/GreeterTest.sol:38)
│ ├╴OwnershipTransferred() (lib/openzeppelin-contracts/contracts/access/Ownable.sol:69)
│ └╴← 0x
└╴provePleaseDontFail(int128)

~/dev/dapptools-template $ seth --to-hex 170141183460469231731687303715884105728
0x80000000000000000000000000000000
~/dev/dapptools-template $ solidity-shell

🚀 Entering interactive Solidity ^0.8.10 shell. '.help' and '.exit' are your friends.
» type(int128).max
170141183460469231731687303715884105727
» .exit
💀 ganache-mgr: stopping temp. ganache instance
~/dev/dapptools-template $ seth --to-hex 170141183460469231731687303715884105727
0x7fffffffffffffffffffffffffffffff
```
fwiw - I've tried this with UINTs as well and had the same problem. However I did not see a problem with negative numbers being passed in to a UINT param

Contributor guide

No contributing guide indexed for this repository

Research direction

Reproduce the issue with the dapp-tools template and the provePleaseDontFail(int128) example in Greeter.t.sol using dapp test -v 3 -m provePleaseDontFail. Trace the symbolic execution argument generation to find why values outside the declared Solidity type range are tried, then add regression coverage showing typed parameters receive valid values and the test no longer reverts.

Written by the indexing model from the issue text.

Assessment

Tech stack
solidity
Domain
devtools, testing
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.