Incoherent overflow detection

[gsalzer]

Description

Consider the following Solidity source c.sol:

// SPDX-License-Identifier: UNLICENCED
pragma solidity 0.4.26;
// pragma solidity 0.8.25;
contract c {
  int256 num = 2**255 - 1;
  // int248 num = 2**247 - 1;
  // uint256 num = 2**256 - 1;
  // uint248 num = 2**248 - 1;
  function t() public payable  {
    num = num + 5;
    // num = num * 5;
  }
}

These are 16 source files (2 compilers, 4 types, 2 operations).

solc 0.4.26

Running the commands

./myth a c.sol
./myth a -c `solc --bin c.sol | tail -1`

yields

	+	*
int256	no issues	OVERFLOW
int248	no issues	no issues
uint256	OVERFLOW	OVERFLOW
uint248	no issues	no issues

The command

./myth a --bin-runtime -c `solc --bin-runtime c.sol | tail -1`

yields no issues for all variants (probably to be expected), whereas

./myth a --bin-runtime --unconstrained-storage -c `solc --bin-runtime c.sol | tail -1`

yields

	+	*
int256	OVERFLOW	OVERFLOW
int248	OVERFLOW	OVERFLOW
uint256	OVERFLOW	OVERFLOW
uint248	no issues	no issues

solc 0.8.25

For this compiler version, the two tables from above look like

	+	*
int256	no issues	no issues
int248	no issues	no issues
uint256	no issues	no issues
uint248	no issues	no issues

	+	*
int256	OVERFLOW	OVERFLOW
int248	OVERFLOW	OVERFLOW
uint256	no issues	no issues
uint248	no issues	no issues

Expected behavior

I'd expected Mythril to detect overflows more consistently, maybe just for (u)int256 and not for (u)int248 (if it is not able to infer the smaller type size), or just for addition and not multiplication, but not this patchwork.

Environment

Mythril: 0.24.8
Python: 3.10.12
Solc: 0.4.26+commit.4563c3fc.Linux.g++ / 0.8.25+commit.b61c2a91.Linux.g++
OS: Ubuntu Linux 22.04

[norhh]

Hi @gsalzer, this is because, for all important overflows, solc versions post 0.8.0 adds an assert to check for violations. Hence, 0.8.0 does not detect any overflow issues. I get no issues for versions post 0.8.0 irrespective of using --unconstrained-storage. Can you check it if that's the case?

[gsalzer]

@norhh Re 0.8.x: Yes, I know about the overflow and underflow checks, so the table

	+	*
int256	no issue	no issue
int248	no issue	no issue
uint256	no issue	no issue
uint248	no issue	no issue

is the one to be expected.

However, for solc 0.8.25 and runtime code, i.e., the command

./myth a --bin-runtime --unconstrained-storage -c `solc --bin-runtime c.sol | tail -1`

I get indeed

	+	*
int256	Int.Ar.Bugs	Int.Arith.Bugs
int248	Int.Ar.Bugs	Int.Arith.Bugs
uint256	no issue	no issue
uint248	no issue	no issue

So it seems that Mythril handles int and uint types differently: For the first, it detects an overflow without taking into account the surrounding check, whereas it either does not detect the overflow for uint or it does, but notices the surrounding overflow check as well.

If you get different results: I'm using Z3 version 4.12.5 - 64 bit and Mythril commit a4f51d0af. The runtime codes (solc --bin-runtime --no-cbor-metadata):
int248, add: 60806040526004361061001d575f3560e01c806392d0d15314610021575b5f80fd5b61002961002b565b005b60055f8054906101000a9004601e0b61004491906100d6565b5f806101000a8154817effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0219169083601e0b7effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff160217905550565b5f81601e0b9050919050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f6100e08261009d565b91506100eb8361009d565b925082820190507fff8000000000000000000000000000000000000000000000000000000000000081127e7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff82131715610146576101456100a9565b5b9291505056
int248, mul: 60806040526004361061001d575f3560e01c806392d0d15314610021575b5f80fd5b61002961002b565b005b60055f8054906101000a9004601e0b61004491906100d6565b5f806101000a8154817effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0219169083601e0b7effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff160217905550565b5f81601e0b9050919050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f6100e08261009d565b91506100eb8361009d565b92508282026100f98161009d565b915082820584148315176101105761010f6100a9565b5b509291505056
int256, add: 608060405260043610601b575f3560e01c806392d0d15314601f575b5f80fd5b60256027565b005b60055f54603391906070565b5f81905550565b5f819050919050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f607882603a565b9150608183603a565b92508282019050828112155f8312168382125f84121516171560a45760a36043565b5b9291505056
int256, mul: 608060405260043610601b575f3560e01c806392d0d15314601f575b5f80fd5b60256027565b005b60055f54603391906070565b5f81905550565b5f819050919050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f607882603a565b9150608183603a565b9250828202608d81603a565b91507f800000000000000000000000000000000000000000000000000000000000000084145f8412161560c15760c06043565b5b828205841483151760d35760d26043565b5b509291505056

[gsalzer]

@norhh Re 0.4.26: It does not matter that the compiler is outdated, as the point is to analyze Mythril's capability to analyze bytecode. The unsystematic results may point to a weakness of Mythril's static analysis, either the method or its implementation. Even if we assume that Z3 behaves differently for addition and multiplication, uint and int, 256 and 248 (it most certainly does), the irregular matrix is surprising.