Inconsistent treatment of constants by static analysis and constant evaluation

[blishko]

Description

The compiler exhibits an inconsistent treatment of constant expressions evaluation.

When applying bitwise negation on uint256 max value (0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF), the compiler reports error for some expressions, but does not report an error in others.

When the expression appears as part of division, an error is reported.

contract BitwiseSolver {
    uint256 constant largeConstant = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF;
    function test() public returns (uint256) {
        return 1/(~largeConstant);
    }
}

Error reported:

Error: Arithmetic error when computing constant value.
 --> test2.sol:5:19:
  |
5 |         return 1/(~largeConstant);
  |                   ^^^^^^^^^^^^^^

However, when the expression stands on its own, no error is reported.

contract BitwiseSolver {
    uint256 constant largeConstant = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF;
    function test() public returns (uint256) {
        return ~largeConstant;
    }
}

Note that if the definition is inlined and the bitwise negation is applied directly to a literal a conversion error is reported:

contract BitwiseSolver {
    function test() public returns (uint256) {
        return ~0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF;
    }
}

Error: Return argument type int_const -115...(71 digits omitted)...9936 is not implicitly convertible to expected type (type of first return variable) uint256. Cannot implicitly convert signed literal to unsigned type.
 --> test2.sol:3:16:
  |
3 |         return ~0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF;
  |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[blishko]

This has been distilled out of #15600 where the current behaviour of constant evaluation causes SMTChecker to crash.

[cameel]

The only reason it causes a crash is the fact that it does not report a fatal error properly. An exception is thrown but the error is not added to the error reporter. It would be just an ordinary compilation error. This needs to be fixed as well.

Though to be fair, this separate bug in error handling is probably the only reason this odd case was discovered :)

[cameel]

I investigated this and it's a clusterfuck of several small bugs.

1. ConstantEvaluator does not perform operations within the right type

It always treats operands as rational numbers with unlimited precision and converts them to the result type only after the operation. This sometimes gives a different result than a calculation with limited precision. For example ~0xff is -256 on rationals but 0 in uint8. And 255 + 1 is 256 on rationals but 0 on uint8 (in an unchecked block). It's that final conversion that results in a compilation error.

It affects constants because, unlike literals, they do not have unlimited precision. It's possible that it also affects some other expressions that can be evaluated at compilation time and work with operators (I don't remember how many of these we have left).

Fortunately, I can't think of a situation where this would actually result in a wrong result rather than a spurious error. Even for ~ the difference comes from truncation (e.g. ~255 has the same representation as -256 in every type that can hold the highest bits; uint8 can't so we only get the final zeros).

2. StaticAnalyzer does not silence errors in its division by zero check

The reason we're even running ConstantEvaluator in the examples from this issue is that StaticAnalyzer has a check for division by zero. The check is skipped if the operands cannot be evaluated by ConstantEvaluator, but it does not ignore errors reported during that evaluation. It's those errors that fail compilation even though they should just make StaticAnalyzer move on.

3. SMTEncoder does not completely silence the fatal errors either

This is what, combined with the above bugs, caused the ICE in #15600, #15601 and #15722.

SMTEncoder::isConstant() has the opposite problem to StaticAnalyzer. It does not give ConstantEvaluator its error reporter, but this means that when a FatalError is thrown, we end up with a discrepancy. To properly ignore errors it needs a try/catch block against FatalError.

Since this is the second place that gets it wrong, I think it's safe to say that the evaluator's interface just does not make the correct usage straightforward enough. I'd suggest defining something like ConstantEvaluator::tryEvaluate() that would both catch the exception and not have an argument for the user to pass in the wrong error reporter.

4. StaticAnalyzer unnecessarily checks division by zero for constants in runtime context

Apparently we disallow division by zero for literals and constants but not for variables:

contract C {
    uint constant N = 1;
    uint x = 1;

    function f() public view {
        // Runtime context:
        1 / 0; // Error: Built-in binary operator / cannot be applied to types int_const 1 and int_const 0.
        N / 0; // Error: Division by zero.
        x / 0; // OK

        // Compile-time context:
        uint[1 / 0] memory a; // Error: Operator / not compatible with types int_const 1 and int_const 0
        uint[N / 0] memory b; // Error: Invalid array length, expected integer literal or constant expression.
        uint[x / 0] memory c; // Error: Invalid array length, expected integer literal or constant expression.
    }
}

However, constants behave like variables in runtime context, i.e. the codegen does emit code for the division and it's performed at runtime. So it's inconsistent for them to be affected by this check. We should either check it for variables as well or stop doing it for constants.

On the other hand in compile-time context, where the value we use actually comes from ConstantEvaluator, the check does not kick in. Oddly, the only situation where it does are constants in the runtime context. In other cases division by zero triggers different errors.

5. The error message is wrong

Arithmetic error when computing constant value. is not accurate. There's no arithmetic error, it actually happens only if the evaluator managed to calculate the value. It should rather say something like The result of this operation ({}) cannot be converted to the target type "{}". But once we fix this, this should really be a message about underflow/overflow because I think this is the only thing that can realistically trigger it.

6. ConstantEvaluator ignores unchecked blocks

Not sure it's fair to call this a bug. It's more of an inconsistency in the design. Consider this example:

contract C {
    uint8 constant A = 2;
    uint8 constant B = 255;

    function f() public pure {
        unchecked {
            B + 3;                // (1) OK
            A / (B + 3);          // (2) Error: Arithmetic error when computing constant value.
            uint[B + 3] memory x; // (3) Error: Arithmetic error when computing constant value.
        }
    }
}

(1) works because it does not trigger the division by zero check and when we fix StaticAnalyzer (2) will stop being an error too.

However, for (3) when we fix the evaluator we have to decide whether to make it unchecked (wrap around) or checked (report overflow). Either will sometimes be inconsistent with runtime behavior and perhaps we should consider making it dependent on whether the code is inside an unchecked block or not.

[cameel]

We discussed it on the call today. A proper fix for handling constants in ConstantEvaluator would pretty much be full compile-time evaluation already (#3157). Until we tackle that, we can only work around its shortcomings.

There are some things we should do immediately:

• Deal with ICEs by handling errors from ConstantEvaluator properly.
• @blishko will try to remove the use of ConstantEvaluator from SMTChecker altogether.
• Adjust the error message from ConstantEvaluator.

In the longer term (unless we get #3157 by then) we may also:

• Make StaticAnalyzer just not run the division by zero check on expressions not evaluated at compilation time, especially those involving constants.
• Special-case those few cases where runtime calculation differs from compile-time evaluation and does not revert:
  • ~ on limited-precision integers.
  • Check if there are any others.

On the other hand we can live with errors in cases that would revert at runtime anyway (i.e. overflows and underflows).