[SMTChecker] Compile panic in 0.8.17: memory access out of bounds

[LiRiu]

Description

solc crashes when a specific contract is compiled.

Environment

• Compiler version: 0.8.17+commit.8df45f5f
• Target EVM version (as per compiler settings):
• Framework/IDE (e.g. Truffle or Remix): Remix
• EVM execution environment / backend / blockchain client: VM or test chain
• Operating system: MacOS Monterey 12.2

Steps to Reproduce

I just try to compile this contract which find in solifity_fuzz_corpus

pragma experimental SMTChecker;

contract C
{
        uint y;
    mapping (uint => uint) map;
    function f(address a, bytes memory data) public {
        map[0] = 0;
                y = 0;
        (bool success, bytes memory ret) = a.staticcall(data);
        assert(success);
        assert(map[0] == 0);
                assert(y == 0);
    }
}

error on Remix

error on solc-bin

compile on 0.8.16 solc is ok compile on 0.8.17 solc without pragma experimental SMTChecker; is ok I suspect the crash caused by SMTChecker module, with specific variable assert?

[leonardoalt]

Thanks for reporting! Yep looks like an SMTChecker bug.

[cameel]

I can confirm that this crashes with a segmentation fault for me.

Also, removing pretty much anything from the repro other than the assert(map[0] == 0); line makes it not crash so it does not seem to be caused by one specific thing in the example.

[leonardoalt]

Yea it's weird. The example is quite simple so there's nothing that immediately strikes me as the issue, which is worrying.

[leonardoalt]

I actually could not reproduce the issue. I tried with the pragma, and without the pragma with the model checker compiler options.

[cameel]

I think it's due to Z3 version on Arch. It segfaults for me with 4.11.0-1. Works with the current 4.11.2-1.

[leonardoalt]

I checked z3 4.11.0 and indeed managed to reproduce it. Unfortunately the crash is inside z3 itself:

Program received signal SIGSEGV, Segmentation fault.
0x00007ffff796ed76 in spacer::hypothesis_reducer::reduce_core (this=0x7fffffffa9a0, pf=<optimized out>) at /home/leo/devel/z3/src/muz/spacer/spacer_proof_utils.cpp:621
621             p = todo.back();
(gdb) bt
#0  0x00007ffff796ed76 in spacer::hypothesis_reducer::reduce_core (this=0x7fffffffa9a0, pf=<optimized out>)
    at z3/src/muz/spacer/spacer_proof_utils.cpp:621

z3 4.11.2 seems to have fixed the crash. We should make sure the next release ships linked with z3 4.11.2 since it fixes the issue.