Help understanding SlitherIR SSA form in loops with if/else branches

[almirmcunhajr]

Hi everyone,

I'm trying to understand how Slither builds its SSA form in the presence of loops with internal branching. I have two simple examples and I would appreciate clarification on how the IR is constructed.

First example (simple while loop)

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract Example {
    int x;

    constructor() {
        x = 10;

        while (x > 0) {
            x = x - 1;
        }
    }
}

Command:

slither test.sol --print slithir-ssa

Output:

Function Example.constructor()
    Expression: x = 10
    IRs:
        x_1(int256) := 10(int256)
    Expression: x > 0
    IRs:
        x_2(int256) := ϕ(['x_3', 'x_1'])
        TMP_0(bool) = x_2 > 0
        CONDITION TMP_0
    Expression: x = x - 1
    IRs:
        TMP_1(int256) = x_2 (c)- 1
        x_3(int256) := TMP_1(int256)

This makes sense to me: there's a phi node x_2 that merges the initial value x_1 and the updated one x_3, and it is used in the condition and body.

---

Second example (loop with if/else)

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract Example {
    int x;

    constructor() {
        x = 10;

        while (x > 0) {
            if (x % 2 == 0) {
                x = x - 2;
            } else {
                x = x - 1;
            }
        }
    }
}

Command:

slither test.sol --print slithir-ssa

Output:

Function Example.constructor()
    Expression: x = 10
    IRs:
        x_1(int256) := 10(int256)
    Expression: x > 0
    IRs:
        TMP_0(bool) = x_1 > 0
        CONDITION TMP_0
    Expression: x % 2 == 0
    IRs:
        TMP_1(int256) = x_1 % 2
        TMP_2(bool) = TMP_1 == 0
        CONDITION TMP_2
    Expression: x = x - 2
    IRs:
        TMP_3(int256) = x_1 (c)- 2
        x_2(int256) := TMP_3(int256)
    Expression: x = x - 1
    IRs:
        TMP_4(int256) = x_1 (c)- 1
        x_3(int256) := TMP_4(int256)
    IRs:
        x_4(int256) := ϕ(['x_2', 'x_3'])

In this second case, I'm trying to understand how the loop semantics are handled. Specifically:

• The phi node x_4 merges the two branches, but it doesn't appear to be used afterward.
• The condition x > 0 and the arithmetic expressions use x_1 instead of a value from a phi node representing the updated value across iterations, like in the first example.

In my understanding, this structure seems a bit confusing since the loop condition and arithmetic expressions continue to use the initial value x_1, it looks like the updated value (x_4) from the if/else branch isn't actually used in subsequent iterations.

Thanks in advance for any help understanding this case!

[mehvetero]

I dug into the SSA builder source (slither/slithir/utils/ssa.py) to answer this properly — the output you're seeing isn't broken, but it does expose a real subtlety in how Slither handles state variables vs locals in loops.

Why the first example works cleanly

Your first example has a textbook phi: x_2 = ϕ(x_1, x_3) at the loop header, merging the initial definition with the back-edge update. This is the standard SSA construction you'd expect.

What's happening in the second example

Two things are combining to produce confusing output:

1. x is a state variable, not a local.

Slither's SSA builder treats these differently. For locals, phi nodes are placed at dominance frontiers of definition sites — the classic algorithm. For state variables, the phi placement uses a slightly different path (lines 139-142 and 153-158 in ssa.py): state variable phis are inserted at the entry point if the variable is used later, and at dominance frontier nodes, but the is_used_later check (line 150) walks the CFG and stops at write sites.

For a state variable like x, the interaction between the "is it read downstream" check and the branching structure can cause the phi at the loop header to be suppressed — the builder sees the variable being written in both branches and determines the phi isn't needed at that point, even though semantically it should be there for the loop back-edge.

2. The --print slithir-ssa output is flat, but the CFG isn't.

The printed output shows IR in source order, but the actual CFG nodes have structure — there's a loop header node, branch nodes, and a merge point. The phi x_4 = ϕ(x_2, x_3) at the end is the if/else merge, which is correct. What's missing is the loop-back phi that should feed x_4 back into the condition check on the next iteration.

Is this a bug?

Partially. The condition x > 0 using x_1 on every iteration is semantically wrong — x_1 is the initial value (10), and if this were actually executed as SSA, the loop would never terminate because the condition never sees the updated value. In practice, Slither's analysis works on the non-SSA IR for most detectors and uses SSA selectively, so this doesn't usually cause incorrect detector results. But for anyone building analysis passes on top of the SSA form (which sounds like what you're doing), this is a real gap.

The root cause is in add_phi_origins (line 530-571): phi candidates are propagated along dominator tree successors, and the condition at line 561 gates phi insertion on len(node.dominator_successors) != 1. In the branching case, the interaction between the if/else dominator structure and the loop back-edge doesn't always produce the phi you need at the loop header.

If you need correct SSA for loop analysis, one workaround is to check whether the non-SSA IR's irs list on the loop header node references x — that gives you the ground truth for what the loop condition actually reads, even if the SSA version missed the phi.