Echidna printer is not precise enough when showing the location of asserts in a codebase

[gustavo-grieco]

Describe the desired feature

Currently, the echidna printer shows which functions directly or indirectly call assert. For instance:

    "assert": {
        "FullMathEchidnaTest": [
            "checkMulDivRoundingUp(uint256,uint256,uint256)"
        ]
    },

However, in order to know if an assertion was reached or not, we need to know at least the pair of filename and line where it is located in the source code. Moreover, a single function can contain many asserts, so this needs to be expanded to include a list of the code locations. I tried to modify the echidna printer code, but there is a blocker:

def _extract_assert(slither: SlitherCore) -> Dict[str, List[str]]:
    ret: Dict[str, List[str]] = {}
    for contract in slither.contracts:
        functions_using_assert = []
        for f in contract.functions_entry_points:
            for v in f.all_solidity_calls():
                if v == SolidityFunction("assert(bool)"):          
                    functions_using_assert.append(_get_name(f))
                    ...

Every value v from f.all_solidity_calls() has no source_mapping information: all of them are None. We need that information in order to map back to the source code.

Finally, if we implement this approach, will have a limitation when the code is inlined:

if (...) { assert(..); }

Here Echidna will incorrectly assume that the line number will imply that the assertion is reached. In order to provide a more precise position, we will need the opIx mapping of each expression (which can be observed in the output of solc --asm file.sol) but this is not available from slither.

[0xalpharush]

We need to coordinate adding it because it breaks the interop, and I removed it for this release #2185

[gustavo-grieco]

There is a refactoring pending that currently blocks this feature, we should be able to merge once that's solved