`unexpected symbolic argument` for prove tests with two `uint` args

[d-xo]

This test fails with hevm: unexpected symbolic argument:

    function proveSmth(uint x, uint y) public {}

This one doesn't :thinking:

    function proveSmth(uint x) public {}

Both run fine the debugger, it's just when running as a command line unit test that we run into issues....

[transmissions11]

@d-xo Maybe it's because I'm on the latest dapp/hevm but I don't see this issue in solmate (even tho the tests are copied nearly identically from dappsysv2 :p)

https://github.com/Rari-Capital/solmate/blob/main/src/tests/FixedPointMath.t.sol

[endophysics]

I just ran into the same error message with a single arg function, function proveSmth(uint256 amount) public {}

I'm on

dapp 0.34.0
solc, the solidity compiler commandline interface
Version: 0.7.4+commit.3f05b770.Darwin.appleclang
hevm 0.48.1

[endophysics]

I did some more digging and came up with this small example. The addition of {value: amount} being what triggers it.

Tt.t.sol:

// SPDX-License-Identifier: GPL-3.0-or-later
pragma solidity ^0.8.6;

import "ds-test/test.sol";

import "./Tt.sol";

contract TtTest is DSTest {
    Tt tt;

    function setUp() public {
        tt = new Tt();
    }

    function proveFoobar(uint256 amount) public {
	tt.foobar{value: amount}();
    }
}

Tt.sol

// SPDX-License-Identifier: GPL-3.0-or-later
pragma solidity ^0.8.6;

contract Tt {
	function foobar() public payable {
		// NOP
	}
}

[MrChico]

There's a couple of things that can trigger unexpected symbolic argument (look for basically any invocation of forceLit in the code), but yes, symbolic value for internal calls is definitely one of the unsupported areas of symbolic execution atm

[MrChico]

It wouldn't be too hard to add, but it does require adding another place to branch (based on whether the sender has enough funds avail or not) – currently we are only ever branching on JUMPI opcodes. Much of the same structure would work for arbitrary branching points I bet if it were to be generalized.