Echidna fails to get certain constants

[gustavo-grieco]

Echidna fails to find the input to break this property:

contract C {
    uint x;

    function f(uint i) public {
       x = i;
    }

    function echidna_test() public view returns (bool) {
        return x != uint(-2);
    }
}

This is an slither issue, originally found by @hacker-DOM

[montyly]

The slither printer gives:

    "constants_used_in_binary": {
        "C": {
            "echidna_test()": {
                "-": [
                    [
                        {
                            "value": "2",
                            "type": "uint256"
                        }
                    ],
                    [
                        {
                            "value": "0",
                            "type": "uint256"
                        }
                    ]
                ]
            }
        }
    },

So once Echidna integrates constants_used_in_binary, and mixes the different combinations, it should work.

It's similar to something like

contract C {
    uint x;

    function f(uint i) public {
       x = i;
    }

    function echidna_test() public view returns (bool) {
        return x != 2 * 2 ether;
    }
}

Where slither gives this info

        "C": {
            "echidna_test()": {
                "*": [
                    [
                        {
                            "value": "2000000000000000000",
                            "type": "uint256"
                        }
                    ],
                    [
                        {
                            "value": "2",
                            "type": "uint256"
                        }
                    ]
                ]
            }
        }

But is not currently used by Echidna.

In the short term, we could make slither's printer adds a couple of constant easy to detect in constants_used (from unary operator, simple binary operations, ..), if it's difficult to integrate constants_used_in_binary in Echidna

[gustavo-grieco]

The negative example is solved, but echidna is still not using 2 * 2 ether as a constant, so it won't break the second example.

[gustavo-grieco]

I think the best way to deal with this is just to precompute the value of binary/unary operations when the operads are constant. This should be done from the slither side, and add the result into constants_used. Echidna should be able to pick them without any modification.

[gustavo-grieco]

@agroce said in a previous issue:

Invert simple arithmetic operations, without using symbolic execution or anything costly/fancy. E.g., mine "4" (and nearby constants 3 and 5) from "if (x * 2) == 8".

[arcz]

Echidna can now break all the examples mentioned here.