Debug information can be insufficient

[ggrieco-tob]

When echidna generates inputs or finds a property failure, it will be nice to have additional information on what Echidna is doing or the state of the contract. Some ideas for this:

• Show generated function calls (too slow)
• Show events emitted by generated function calls.
• Show events emitted by the property failure.
• Show how and why the property failed (returned false, reverted, self-destruction)
• Show the state of the contract after a failure (it can be large)

[alexon1234]

I would be really interested in the last point Show the state of the contract after a failure
Because there are contracts that have methods like function XXX() public returns (uint) { where all the calculation is done using state variables.

If we run echidna to test this method, we won't get much information about the state of the contract when it failed. This information would improve the debugging.

[alexon1234]

Hi,
I would like to propose to add the intermediate results of the operations in the coverage file that is generated.
So for example instead of having:

    uint256 internal x;

*   |    function setX(uint256 _x) public {
*   |        x = _x;
    }

    function echidna_check_normalization() public returns (bool) {
        bytes16 z = _denormalize(x);
        unit result = _normalize(z);
        return result == x;
    }

Have something like:

    uint256 internal x;

*   |    function setX(uint256 _x) public {
*   |        x = _x;
    }

    function echidna_check_normalization() public returns (bool) {
        // x = XXXX
        bytes16 z = _denormalize(x);
        // z = XXXXXXXXXXXX
        unit result = _normalize(z);
       // result = XXXXXXXXX
        return result  == x;
    }

[ggrieco-tob]

You mean, when a property fails, right?

[alexon1234]

Yes, when the echidna_ function fails.

[rappie]

Showing events for all calls in the sequence would really help me out.

It is especially useful when using helper functions that modify the value, for example using modulo to get values in a small range. Currently I work around this by storing the modified value by the helper function and logging it in the final call.