Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
Eihcir0 opened this issue Jan 1, 2022 · 1 comment

Comments

@Eihcir0
Copy link

Eihcir0 commented Jan 1, 2022

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
Copy link

hellwolf commented Mar 8, 2022

reproduced #919

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants