Symbolic execution tests passing in arguments outside the range of the typed parameter
- 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