Incorrect SSA for conditional state variable mutation

[aaronyoo]

Slither gives incorrect SSA for the following program involving a state variable:

contract State {
    int state = 0;
    function f(int a) public returns (int) {
        if (a < 1) {
            state += 1;
        }
        return state;
    }
}

Here is the resulting SSA:

f:
	state_1(int256) := ϕ(['state_0', 'state_2'])
	TMP_0(bool) = a_1 < 1
	CONDITION TMP_0
		state_2(int256) = state_1 + 1
	RETURN state_2

The return instruction relies on state_2 which is only conditionally defined. If a_1 < 1 evaluates to false I would say this SSA form crashes (or the logical equivalent). An alternative SSA might look like:

f:
	state_1(int256) := ϕ(['state_0', 'state_2'])
	TMP_0(bool) = a_1 < 1
	CONDITION TMP_0
		state_2(int256) = state_1 + 1
	state_3 = ϕ(['state_1', 'state_2'])
	RETURN state_2

[pgoodman]

I think the correct alternative SSA is in fact:

f:
	state_1(int256) := ϕ(['state_0', 'state_3'])
	TMP_0(bool) = a_1 < 1
	CONDITION TMP_0
		state_2(int256) = state_1 + 1
	state_3 = ϕ(['state_1', 'state_2'])
	RETURN state_3

[aaronyoo]

After a bit of digging I think I have found the source of the problem but I am not sure what a good solution would be. Slither creates its SSA in two steps. First, generating the SSA with "generate_ssa_irs" (step 1) and then "fixing the phi nodes" (step 2). Before the "fixing the phi nodes" all of the phi nodes are nonsensical. Thus, after "generate_ssa_irs" but before "fixing the phi nodes" the program looks something like this:

f:
	state_0(int256) = ϕ[]  // unresolved phi node
	TMP_0(bool) = a_1 < 1
	CONDITION TMP_0
		state_2(int256) = state_1 + 1
	RETURN state_2

Here, we have already made a mistake since we didn't produce a phi node after the conditional block and consequently, the non-existent phi node will never be resolved. The reason that didn't happen is because the analysis thinks that there is only one write to state. Since the first phi node isn't resolved, it doesn't count as a write to state. Thus we hit a circular dependency where we need the phi node to be resolved to generate correct SSA but we need the SSA to actually know that we should produce a phi node in the first place.

The solution to this problem is a bit unclear. Even if we did recognize that the initial entry phi node was a write to state, we wouldn't immediately know what to put in the phi node: state_3 = ϕ(['__don't know__', 'state_2']) since the unresolved phi node gives us no useful information; namely, it doesn't tell us the name of the lvalue. Somewhere in the analysis, it knows how to fix the phi node to correctly become state_1 = ϕ[...] so I think I need to find out where that is.

[aaronyoo]

I have a short fix working locally. I will try to submit a PR soon.