Extend DataFlowAnalyzer to not reset memory if memory ops use zero length

[chriseth]

trafficstars

The call opcode (and others) should not reset memory if it can be determined that the memory output area is zero.

The trigger for this is to improve the code generated from the following snippet:

contract MicroProxy {
  address immutable _master;
  constructor(address master_) { _master = master_; }
  fallback(bytes calldata) external returns (bytes memory returndata) {
    (,returndata) = _master.delegatecall(msg.data);
  }
}

Generated:

        code {
            {
                mstore(64, 128)
                if callvalue() { revert(0, 0) }
                let _1 := 0
                calldatacopy(128, _1, calldatasize())
                mstore(add(128, calldatasize()), _1)
                pop(delegatecall(gas(), loadimmutable("2"), 128, calldatasize(), _1, _1))
                let data := _1
                switch returndatasize()
                case 0 { data := 96 }
                default {
                    let result := and(add(returndatasize(), 63), not(31))
                    let memPtr := mload(64)
                    let newFreePtr := add(memPtr, result)
                    if or(gt(newFreePtr, 0xffffffffffffffff), lt(newFreePtr, memPtr))
                    {
                        mstore(_1, shl(224, 0x4e487b71))
                        mstore(4, 0x41)
                        revert(_1, 0x24)
                    }
                    mstore(64, newFreePtr)
                    data := memPtr
                    mstore(memPtr, returndatasize())
                    returndatacopy(add(memPtr, 0x20), _1, returndatasize())
                }
                return(add(data, 0x20), mload(data))
            }
        }

Note that if the delegatecall did not clear memory, the checks about mpmPtr can be removed.

[chriseth]

It might be the best solution to introduce new builtins that do not write to memory and replace them in a new optimizer step. Note that since the memory-modifying instructions do not return data, we cannot use a rule for the ExpressionSimplifier.

[chriseth]

On the other hand - we also want to detect if such an opcode writes to a memory area that is not overlapping with other known memory areas, so it might be fine to add a special case just like we do for mstore. The downside is that it only works when the function containing the call is inlined.

[hrkrshnn]

It might be possible to solve this using a Linear Program.

The important part of the above code is the following:

mstore(64, 128)
let _1 := 0
calldatacopy(128, _1, calldatasize())
mstore(add(128, calldatasize()), _1)
delegatecall(gas(), loadimmutable, 128, calldatasize(), _1, _1)

// We want to know if memPtr is 128
let memPtr := mload(64)

We can encode things this way. Call the memory location that we are interested in by m. (Here we have the equation m := 64)

Define a variable c := calldatasize() and constraint c >= 0.

The memory encodings:

1. calldatacopy(128, _1, calldatasize()): 128 <= m < 128 + c also 128 <= m + 31 < 128 + c
2. mstore(add(128, calldatasize()), _1): 128 + c <= m < 128 + c + 32 also 128 + c <= m + 31 < 128 + c + 32
3. delegatecall(gas(), loadimmutable, 128, calldatasize(), _1, _1): _1 <= m < _1 also _1 <= m + 31 < _1.

To check if mload(64) is invariant, all we need to do is to individually check if the linear equations are feasible. For example, for the first one, these are the equations:

1. m := 64
2. 128 <= m
3. m < 128 + c
4. c >= 0

This problem is infeasible. The other problems are infeasible too. So the value at 64 can be safely loaded.

[hrkrshnn]

BTW, mstore(add(128, calldatasize()), _1) will reset all the memory at that point (64 -> 128). So even if we don't clear memory for delegatecall(gas(), loadimmutable("2"), 128, calldatasize(), _1, _1), we still won't be able to resolve let memPtr := mload(64).

The smt based technique can now handle this https://github.com/ethereum/solidity/pull/10681/files#diff-a543663ab8a611118fb129bbe24b2def1b3c4c8f79948d42cd61b0d8122d3015

[chriseth]

This could be combined with the Operations from #11352

[ekpyron]

https://github.com/ethereum/solidity/pull/12762 pretty much showcases how this can be done with the recent more elaborate semantic information we have - so the same mechanism just needs to be transferred to the data flow analyzer.

[ekpyron]

Staging this as a task ready to be worked on for using the mechanism of https://github.com/ethereum/solidity/pull/12762 to determine when a memory-writing call has a length of zero and, based on that, to not clear memory knowledge in the data flow analyzer. (i.e. not for anything more fancy like the linear programming suggestion)

[github-actions[bot]]

This issue has been marked as stale due to inactivity for the last 90 days. It will be automatically closed in 7 days.

[github-actions[bot]]

Hi everyone! This issue has been automatically closed due to inactivity. If you think this issue is still relevant in the latest Solidity version and you have something to contribute, feel free to reopen. However, unless the issue is a concrete proposal that can be implemented, we recommend starting a language discussion on the forum instead.