dapphub / dapptools

Dapp, Seth, Hevm, and more
https://dapp.tools
2.1k stars 325 forks source link

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

Open Eihcir0 opened 2 years ago

Eihcir0 commented 2 years ago

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

hellwolf commented 2 years ago

reproduced #919