Solidity: [Yul] optimiser step CSE produces syntactically incorrect code

[bshastry]

Description

This test passes but it should not. Related to #9301 in that the fuzzer found this test case first which led @ekpyron to propose the test case in the related issue.

{
    let x_1
    x_1, x_1 := f()
    function f() -> o_1, o_2 {}
    let x_2, x_3 := f()
}
// ----
// step: commonSubexpressionEliminator
//
// {
//     let x_1
//     x_1, x_1 := f()
//     function f() -> o_1, o_2
//     { }
//     let x_2, x_3 := x_1
// }

Environment

• Compiler version: latest develop

Steps to Reproduce

// Copy test to test/libyul/yulOptimizerTests/CSE/test.yul
$ soltest -t yulOptimizerTests/CSE/test

[ekpyron]

For the record: even if we just syntactically disallow x_1, x_1 := f() (which would solve this issue), it may still be worth to independently have a look at the CSE to make sure that the cause of this is rendered harmless with disallowing it.

[ekpyron]

Or put differently: the CSE could use some kind of assertion here instead of just happily producing invalid code, no matter if we disallow these cases from ever occurring or not.

[bshastry]

For the record: even if we just syntactically disallow x_1, x_1 := f() (which would solve this issue), it may still be worth to independently have a look at the CSE to make sure that the cause of this is rendered harmless with disallowing it.

I think the syntactically invalid replacement happens here

https://github.com/ethereum/solidity/blob/d72aae20aa356c10a1966a1a2c7d6f36863a2381/libyul/optimiser/CommonSubexpressionEliminator.cpp#L107-L111

because of

• https://github.com/ethereum/solidity/blob/d72aae20aa356c10a1966a1a2c7d6f36863a2381/libyul/optimiser/SyntacticalEquality.cpp#L51-L55 returning true
• AND the function call being previously assigned to variable x_1 I think (but not sure)

Please also note that when https://github.com/ethereum/solidity/blob/d72aae20aa356c10a1966a1a2c7d6f36863a2381/libyul/optimiser/DataFlowAnalyzer.cpp#L79-L81 is executed

the assignment x_1, x_1 := f() in the code above gets treated as an assignment of a single variable (due to the type holding variable names being a set: https://github.com/ethereum/solidity/blob/d72aae20aa356c10a1966a1a2c7d6f36863a2381/libyul/optimiser/DataFlowAnalyzer.cpp#L79)

I'm not sure why the syntactic equality check is not triggered for

{
    let x_1, x_2
    x_1, x_2 := f()
    function f() -> o_1, o_2 {}
    let x_3, x_4 := f()
}

Shouldn't this be simplified to

{
    let x_1, x_2
    x_1, x_2 := f()
    function f() -> o_1, o_2 {}
    let x_3, x_4 := x_1, x_2
}

or is it because tuple assignments are disallowed in yul unless RHS is a function call?

[chriseth]

I don't understand this issue - the test _starts_ with x_1, x_1 := f(), right?

The issue here is that we do not have a good definition of the semantics of x_1, x_y := f() - is it?

[bshastry]

I don't understand this issue - the test _starts_ with x_1, x_1 := f(), right?

The issue here is that we do not have a good definition of the semantics of x_1, x_y := f() - is it?

I think the issue is that disallowing x_1, x_1 := f() as we now do, will not hide a more serious dormant issue somewhere in CSE.

I do not yet fully understand why CSE simplified let x_2, x_3 := f() with let x_2, x_3 := x_1

[bshastry]

I think the missing exception was
https://github.com/ethereum/solidity/blob/4e55759144535c6e58df37bc4c6ea67b26531d97/libyul/optimiser/DataFlowAnalyzer.cpp#L82

What happened was that the DFA treated x_1, x_1 := f() as if it were x_1 := f(). This was then used to simplify the RHS of let x_2, x_3 := f() into x_1 because that RHS is syntactically identical to the value assigned to x_1.

The need for this exception is now made redundant by #9321

[chriseth]

So can this be closed now or not?

[bshastry]

Fixed by #9321