dapptools
dapptools copied to clipboard
Symbolic execution tests passing in arguments outside the range of the typed parameter
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 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
reproduced #919