Not showing all execution paths

[0xfarhaan]

Hey so I as testing out Pyrometer and used it against the backdoor example that the foundry fuzzer can't find in the hopes that it would pick up the constraints required to reach the execution path and show me the relevant bounds. Here is the contract code:

contract SymbolicTest {

    // https://github.com/foundry-rs/foundry/issues/2851
    function backdoor(uint256 x) external pure {
        uint256 number = 99;
        unchecked {
            uint256 z = x - 1;
            if (z == 6912213124124531) {
                number = 0;
            } else {
                number = 1;
            }
        }
        assert(number != 0);
    }

}

My terminal output

~/repositories/personal/forge-playground main ❯ pyrometer ./contracts/SymbolicTest.sol -vv                                          system
DONE ANALYZING IN: 1ms. Writing to cli...
Bounds: Bounds for function: function backdoor(uint256)
Bounds: Bounds for subcontext: backdoor(uint256) where:
1. (number != 0) == true
2. (z != 6912213124124531) == true
, killed: None
    ╭─[./contracts/SymbolicTest.sol:7:48]
    │
  7 │ ╭─▶     function backdoor(uint256 x) external pure {
  8 │ │           uint256 number = 99;
    │ │           ─────────┬─────────
    │ │                    ╰─────────── "number" == 99
    ┆ ┆
 10 │ │               uint256 z = x - 1;
    │ │               ────────┬────────
    │ │                       ╰────────── "z" ∈ [ 2**256 - 2, 2**256 - 1 ]
 11 │ │               if (z == 6912213124124531) {
    │ │                   ┬
    │ │                   ╰── "z" ∈ [ 2**256 - 2, 2**256 - 1 ] && ∉ { == 6912213124124531}
    ┆ ┆
 14 │ │                   number = 1;
    │ │                   ───┬──
    │ │                      ╰──── "number" == 1
    ┆ ┆
 18 │ ├─▶     }
    │ │
    │ ╰─────────── Entry function call

I would have expected a second trace where the constraint (z != 6912213124124531) == true isn't applied.

Note I did take the assert statement out and tried as well with the same result.

Is this just a limitation of the current implementation? Just trying to understand, I know halmos picks up the counter example value.

[plotchy]

Good find. I have a hunch it has something to do with unchecked {} as removing that scope makes it work as expected.

contract SymbolicTest {

    // https://github.com/foundry-rs/foundry/issues/2851
    function backdoor(uint256 x) external pure {
        uint256 number = 99;
        uint256 z = x - 1;
        if (z == 691221312412453) {
            number = 0;
        } else {
            number = 1;
        }
        assert(number != 0);
    }

}

[brockelmore]

fixed in #71

Also, by default reverting paths are hidden - use the flag --show-reverts true