Inconsistent results source vs bytecode

[gsalzer]

Description

Mythril reports different results when analyzing source code vs bytecode.

How to Reproduce

$ cat c.sol
// SPDX-License-Identifier: GPL-3.0
pragma solidity 0.8.24;
contract c {
    function t(int216 num) public payable  {
        num++;
    }
}
$ ./myth analyze c.sol
The analysis was completed successfully. No issues were detected.
$ solc --bin c.sol | tail -1 > c.hex
$ ./myth analyze -f c.hex
==== Integer Arithmetic Bugs ====
...
PC address: 266
...
$ solc --bin-runtime c.sol | tail -1 > c.rt.hex
$ ./myth analyze --bin-runtime -f c.rt.hex
==== Integer Arithmetic Bugs ====
...
PC address: 266
...

Expected behavior

Mythril generates the same output for c.sol as for c.hex.

Environment

• Mythril version: v0.24.8
• Solidity compiler and version: 0.8.24+commit.e11b9ed9.Linux.g++
• Python version: 3.10.12
• OS and Version: Ubuntu 22.04.4 LTS

[norhh]

Hi @gsalzer, this is because, for solidity versions with 0.8.0+ where there is a mandatory overflow/underflow checks added by the compiler. So, Mythril turns off the IntegerModule for this version, as checking for overflows is expensive and the most overflow/underflow 'bugs' found would be due to compiler optimisations.

Using the code generated by my compiler, I couldn't generate an overflow, so can you provide me with your bytecode?

[gsalzer]

$ cat c.hex
608060405234801561000f575f80fd5b506101588061001d5f395ff3fe60806040526004361061001d575f3560e01c8063cb92841314610021575b5f80fd5b61003b60048036038101906100369190610088565b61003d565b005b8080610048906100e0565b91505050565b5f80fd5b5f81601a0b9050919050565b61006781610052565b8114610071575f80fd5b50565b5f813590506100828161005e565b92915050565b5f6020828403121561009d5761009c61004e565b5b5f6100aa84828501610074565b91505092915050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f6100ea82610052565b91507a7fffffffffffffffffffffffffffffffffffffffffffffffffffff8203610117576101166100b3565b5b60018201905091905056fea26469706673582212202b749cfa10f1ebf7d71060d388d02f059c9e8ca3a0cc05ec92e48149aa447ff764736f6c63430008180033
$
$ cat c.rt.hex
60806040526004361061001d575f3560e01c8063cb92841314610021575b5f80fd5b61003b60048036038101906100369190610088565b61003d565b005b8080610048906100e0565b91505050565b5f80fd5b5f81601a0b9050919050565b61006781610052565b8114610071575f80fd5b50565b5f813590506100828161005e565b92915050565b5f6020828403121561009d5761009c61004e565b5b5f6100aa84828501610074565b91505092915050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f6100ea82610052565b91507a7fffffffffffffffffffffffffffffffffffffffffffffffffffff8203610117576101166100b3565b5b60018201905091905056fea26469706673582212202b749cfa10f1ebf7d71060d388d02f059c9e8ca3a0cc05ec92e48149aa447ff764736f6c63430008180033

[norhh]

That happens due to solidity's internal check for overflows. Solidity subtracts call data with 2^215-1 and checks if it's equal to 0, if true, then it jumps to the code that handles overflow (i.e., reverts, as 2^215 - 1 + 1 will overflow), but as you can see, calldata can be less than 2^215-1 when num is positive, so it leads to the underflow, although its an internal and doesn't have an effect.
Execution on source code with versions post 0.8.0 doesn't run overflow/underflow checks, as it is expensive and most "bugs" are due to internal overflows/underflows generated by the compiler.