SMTChecker triggers an ICE by not reporting Arithmetic error when computing constant value fatal error caused by constant negation

[Subway2023]

Environment

• Compiler version: 0.8.27
• Target EVM version (as per compiler settings): None
• Framework/IDE (e.g. Truffle or Remix): None
• EVM execution environment / backend / blockchain client: None
• Operating system: Linux

Steps to Reproduce

// SPDX-License-Identifier: MIT
contract BitwiseSolver {
    uint256 constant largeConstant = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF;
    event LogResult(uint256 result);
    constructor() {
        executeOperations(99);
    }
    function executeOperations(uint256 input) public {
        uint256 result = (input | largeConstant) & ~largeConstant;
        result = performShift(result + input);
        emit LogResult(result);
    }
    function performShift(uint256 value) internal pure returns (uint256) {
        for (uint8 i = 0; i < 256; i++) {
            value ^= (1 << i);
            if (i == 0) break;   // Ensures loop runs only once
        }
        return value;
    }
}

solc-0827 b.sol --model-checker-ext-calls trusted --model-checker-timeout 0 --model-checker-engine chc --model-checker-solvers z3   --model-checker-show-unproved 

Internal compiler error:
/solidity/libsolidity/interface/CompilerStack.cpp(502): Throw in function bool solidity::frontend::CompilerStack::analyze()
Dynamic exception type: boost::wrapexcept<solidity::langutil::InternalCompilerError>
std::exception::what: Unreported fatal error: std::exception
[solidity::util::tag_comment*] = Unreported fatal error: std::exception

However, the program can be successfully compiled into bytecode.

[cameel]

Note that the fact that this runs into Unreported fatal error is a bug in itself, separate from the underlying cause. FatalError should never be thrown without also reporting the message using an error reporter. This should be fixed.

I just pushed #15807, which makes the output in such cases more infomative and shows the original error as well:

Unreported fatal error:
/solidity/liblangutil/ErrorReporter.cpp(143): Throw in function void solidity::langutil::ErrorReporter::fatalError(solidity::langutil::ErrorId, solidity::langutil::Error::Type, const solidity::langutil::SourceLocation&, const std::string&)
Dynamic exception type: boost::wrapexcept<solidity::langutil::FatalError>
std::exception::what: Arithmetic error when computing constant value.
[solidity::util::tag_comment*] = Arithmetic error when computing constant value.

Internal compiler error:
/solidity/libsolidity/interface/CompilerStack.cpp(516): Throw in function bool solidity::frontend::CompilerStack::analyze()
Dynamic exception type: boost::wrapexcept<solidity::langutil::InternalCompilerError>
std::exception::what: Unreported fatal error.
[solidity::util::tag_comment*] = Unreported fatal error.

[cameel]

The repro can also be minimized to something like this:

contract C {
    uint256 constant N = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF;

    function f() public {
        ~N;
    }
}

I see that it's already included in the linked #15709. Perhaps we should close this one in favor of it?