[SMTChecker] Bug: Inconsistent Storage Array Bytes Writing

[sallywang147]

Thank you for building SMTChecker and Solidity -great work! As I'm experimenting, I found a compiler bug below. When you get a chance, would you mind confirming if this bug indeed exists and should be fixed? Thank you!

Environment

• Compiler version: pragma solidity >=0.7.0;
• Target EVM version (as per compiler settings): 0.7.0+commit.9e61f92b
• Framework/IDE (e.g. Truffle or Remix): the following trances are from running on Mac Terminal locally. Similar issues are observed on REMIX IDE too.
• EVM execution environment / backend / blockchain client: N/A
• Operating system: MacBook Air (Retina, 13-inch, 2018)

Steps to Reproduce

The following code passes assertion checks when it really shouldn't, because x[0] = 23 after reassigning at x = y;

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.7.0;
pragma experimental SMTChecker;

contract C {
    uint128[] x;
    function f() public {
        x.push(42); x.push(42); x.push(42); x.push(42);
        uint128[] memory y;// = new uint128[](1);
        y[0] = 23;
        // This will shrink the array x to one element.
        // Resizing the array to length 4.
        x = y;
        x.push(); x.push(); x.push();
        assert(x[0] == 0);
        assert(x[1] == 0);
        assert(x[2] == 0);
        assert(x[3] == 0);
        // After resizing the array, its contents are [0, 0, 0, 0],
        // instead of [23, 0, 0, 0]. Resizing can be also be done by
        // assigning to `.length` or by assigning to the `slot` member
        // inside inline assembly.
    }
}

It throws violations in the following code when it really shouldn't, because x[0] = 23 after reassigning at x = y;

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.7.0;
pragma experimental SMTChecker;

contract C {
    uint128[] x;
    function f() public {
        x.push(42); x.push(42); x.push(42); x.push(42);
        uint128[] memory y;// = new uint128[](1);
        y[0] = 23;
        // This will shrink the array x to one element.
        // Resizing the array to length 4.
        x = y;
        x.push(); x.push(); x.push();
        assert(x[0] == 23);
        assert(x[1] == 0);
        assert(x[2] == 0);
        assert(x[3] == 0);
        // After resizing the array, its contents are [0, 0, 0, 0],
        // instead of [23, 0, 0, 0]. Resizing can be also be done by
        // assigning to `.length` or by assigning to the `slot` member
        // inside inline assembly.
    }
}

If we use REMIX to reproduce the bug, it throws assertion violations in both scenarios in the code above:

[blishko]

Hi @sallywang147,

do I read it correctly that you are using solc 0.7.0? That is rather old version of the compiler, SMTChecker has matured significantly since then.

On the latest version, I see different results from SMTChecker. Can you check with the latest version and let us know if you still consider the answers incorrect?

One note about your examples:

uint128[] memory y;// = new uint128[](1);
y[0] = 23;

This is an access out of bounds, so the code would always revert at this point, making the assertions that follow always unreachable (and thus safe).

[sallywang147]

Hi @blishko, many thanks for your quick response! I totally agree that the newer compiler version (>=0.8.0) would prevent this issue. On 0.7.0, I think the root cause is not SMTChecker but the older compiler. For example, the 0.7.0 compiler generated x[0] = 0 when it really should've been x[0] = 23. That's why SMTChecker throws the violation when it executes the assertion assert(x[0]==23);. Is this explanation plausible? or in your view, is the issue caused by something else? Many thanks for your time!

[blishko]

I suspect that the SMTChecker warnings are independent of the code generated by the compiler. Unfortunately, we cannot afford to investigate the behaviour in the old version of the compiler when the new version does not suffer from this issue.

[sallywang147]

Ah no worries at all, many thanks again for your quick response! I'll close the comment.