Overflow analysis not respecting types smaller than uint256

[ezulkosk]

Description

Below I've listed two trivial contracts that are exactly the same, but one uses uint256 variables and the other uses uint80. An overflow is expected in both contracts but it is only detected in the one using uint256.

How to Reproduce

Here is the initial contract using uint256 where mythril correctly detects an overflow:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
contract A {
    function f(uint256 arg) public view returns(uint256) {
        uint256 res;
        unchecked{        
            res = 10_000_000_000 * arg; // detected overflow
        }
        return res;       
    }
}

This one uses uint80 and mythril finds no issues:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
contract B {
    function f(uint80 arg) public view returns(uint256) {
        uint80 res;
        unchecked{        
            res = 10_000_000_000 * arg; // undetected overflow
        }
        // assert(res > arg); // the assertion violation is correctly detected if added
        return res;       
    }
}

Environment

Using v0.23.25 (installed via pip3).

Additional Environment or Context

If this is indeed an issue, it might relate to 256 being hardcoded in many places, whereas it seems that the BitVector length should be type-dependent (e.g., 80 bits for uint80). As some examples, in integer.py module which defines the IntegerArithmetics analysis, 256 is hardcoded in several places. Further, the underlying BVMulNoOverflow function also uses 256.

[norhh]

Mythril is a bytecode analyzer, so all information pertaining to int80 is lost when it comes to bytecode. So this is something that's tricky to fix. EVM defaults to 256 bitwidth, so, when compiling, all this type information is lost.