[yul] optimizer's redundant assignment eliminator incorrectly removes non-redundant assignments in for loops containing a break/continue statement inside a nested branch statement

[bshastry]

Description

Found by LPM + libFuzzer + custom yul mutator (see #7947 )

{
        for {let i:= 0} lt(i,2) {i := add(i,1)}
        {
                // x is declared and implicitly
                // initialized to zero.
                let x
                // This assignment is not redundant
                // since it is used by mstore statement
                // that follows the if statement
                x := 1337
                if lt(i,1) {
                        // This assignment is redundant
                        x := 42
                        continue
                }
                mstore(0, x)
        }
}

is incorrectly optimized to

        {
            let i := 0
            for { } lt(i, 2) { i := add(i, 1) }
            {
                if lt(i, 1) { continue }
                mstore(0, 0)
            }
        }

mstore(0, 0) should be mstore(0, 1337) instead.

In the example above, the if statement could be replaced by another branching statement e.g., switch statement with the same result.

In general, this problem manifests while the redundant assignment eliminator is visiting a continue statement inside a branch inside a for loop: Assignments to a variable in the path leading to the branching statement are also removed apart from the correct redundant assignment within the branching statement.

For example, the yul optimizer also incorrectly marks (and subsequently removes) the assignment statement directly in the for loop below leading to mstore(0, 1337) although the correct optimization should be mstore(0, 31337)

{
        for {let i:= 0} lt(i,2) {i := add(i,1)}
        {
                let x := 1337
                // This assignment is incorrectly removed
                x := 31337
                if lt(i,1) {
                        // Redundant assignment eliminator removes all
                        // assignments to `x` in this path (including `x := 31337`)
                        // when it should be removing only `x := 42`
                        x := 42
                        continue
                }
                mstore(0, x)
        }
}

Unfortunately, this affects v0.6.0 and may warrant a bug list entry. I'm trying to understand why this was not found earlier. My intuition is that the custom mutator had a role to play by increasing the likelihood (during fuzzing) of insertion of continue statement inside for loops (which I undertook only recently).

Environment

• Compiler version: latest develop

Steps to Reproduce

$ solc --strict-assembly --optimize <test.yul>

[bshastry]

I'm wondering if the fix entails making m_assignments a vector of TrackedAssignments into which we push back assignments in a given scope. Subsequently, we finalize assignments only in the last scope.

[bshastry]

Notes: Issue is reproducible via break statement as well. Example:

{
        for {let i:= 0} lt(i,2) {i := add(i,1)}
        {
                let x
                // x is used by mstore post if statement
                x := 1337
                if gt(i, 0) { x := 42 break }
                mstore(0, x)
        }
}

should store 1337 in memory location 0 but it is optimized to

        {                   
            let i := 0        
            for { } lt(i, 2) { i := add(i, 1) }
            {                 
                if iszero(iszero(i)) { break }
                mstore(0, 0)
            }                                     
        }

which stores 0 in memory location 0.

[chriseth]

It is essential, that the variable x is declared inside the for loop, so this seems to be related with, as you say, finalizing a variable when exiting from the block while it is still "to be processed" by the continue statement.