SMTChecker: doesn't recognize "OR" as arithmetic.

[drortirosh]

The following sample is based on the standard "overflow" sample of the SMTChecker. There is an added "require" which makes sure the addition can never overflow - but the SMTChecker doesn't recognize it.

running the normal solc overflow.sol --model-checker-targets "underflow,overflow" --model-checker-engine all --model-checker-show-unproved Fails and claims that "Overflow can happen here" with parameter _y = 2**256 - 1

The SMT failed to see that checking an "OR'ed" value is equivalent to checking them separately (actually, I compare them to type(uint128).max, which mean I can even multiply them without overflow..

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Overflow {
    uint immutable x;
    uint immutable y;

    function add(uint _x, uint _y) internal pure returns (uint) {
        return _x + _y;
    }

    constructor(uint _x, uint _y) {
        // added "require": this makes sure that both values are small enough, and are allowed to be added with no overflow
    require(  (_x | _y) < type(uint128).max );
        (x, y) = (_x, _y);
    }

    function stateAdd() public view returns (uint) {
        return add(x, y);
    }
}

[leonardoalt]

Hi @drortirosh , thanks for the issue!

The tool does in fact recognize the extra require, but:

• The BMC engine only looks at each function separately, regardless of the previous states. So it doesn't really know of any constraints that were added in previous transactions, in this case the said require.
• The CHC engine says "might happen here", which means that the underlying solver could not prove nor disprove the property. This property is hard because it mixes integer and bitvector (because of the bitwise operation) reasoning, where the constructor constraint you mentioned does influence the correctness of the property. So this would force the underlying Horn solver to find an inductive invariant over the state of the contract mixing integer and bitvector reasoning, which is pretty hard.

It is unfortunate that such a small property becomes a complicated problem behind the scenes. If you switch the require to an arithmetic instead of a bitwise operation you might have better luck.