ethereum/formal-methods

<ehildenb> Not sure if the above makes sense, but this new heuristic:

def kevmShouldSubsume(constrainedTerm1, constrainedTerm2):
    if all([getCell(constrainedTerm1, cn) == getCell(constrainedTerm2, cn) for cn in ['PC_CELL', 'K_CELL', 'CALLDATA_CELL', 'PROGRAM_CELL', 'JUMPDESTS_CELL']]):
        jumpDests   = [ i['args'][0] for i in flattenLabel('_Set_', getCell(constrainedTerm1, 'JUMPDESTS_CELL')) ]
        (state1, _) = splitConfigAndConstraints(constrainedTerm1)
        (state2, _) = splitConfigAndConstraints(constrainedTerm2)
        stateDelta  = pushDownRewrites(KRewrite(state1, state2))
        rewrites    = []
        def _collectRewrites(_k):
            if isKRewrite(_k) and isKToken(_k['lhs']) and isKToken(_k['rhs']):
                rewrites.append((_k['lhs'], _k['rhs']))
            return _k
        traverseBottomUp(stateDelta, _collectRewrites)
        return not any([(i != j) and (i in jumpDests) and (j in jumpDests) for (i, j) in rewrites])
    return False

checks that:

• All of the <pc>, <k>, <callData>, <program>, and <jumpDests> cells are identical (could probably also add <callDepth> to this one)
• There are no deltas in the state between two integers that are valid jump destinations.

This correctly identifies the loop in this code:

    function sum(uint n) external pure returns (uint s) {
        s = 0;
        uint i = n;
        while (0 < i) {
            s = s + i;
            i = i - 1;
        }
        return s;
    }

while correctly not identifying a loop in this code:

    function twoAddress(address a1, address a2) public pure returns (uint256) {
        if (a1 == a2) {
            return 0;
        }
        return 1;
    }