Uncaught errors in BitVecConstant constructor

[sam-xif]

Summary of the problem

Hello manticore community,

I am working as part of a research team developing a code analysis tool for Python. One of the issues the tool discovered in manticore's codebase is that the constructor for BitVecConstant has the potential to throw uncaught OverflowError, MemoryError, and ValueError. The OverflowError and MemoryError are caused by a very large positive value for the size argument, while the ValueError is caused by a negative value for the size argument.

If you are interested in learning more about the tool and how it found this issue, let me know down in the comments, or you can contact me at [email protected]. We are primarily curious about whether you find that this issue is legitimate and worth reporting and fixing. If not, we would be interested in understanding why.

Thank you for your consideration!

-Sam

Manticore version

Latest master (commit hash: 8861005)

Python version

Python 3.8

OS / Environment

Linux (kernel version 5.10.218)

Dependencies

N/A

Step to reproduce the behavior

Call BitVecConstant constructor with very large positive values or negative values for size.

Expected behavior

Assertion failure indicating that size should be nonnegative, and/or checks to ensure that size is not extremely large.

Actual behavior

Errors are thrown uncaught.

Any relevant logs

Stack traces:

Traceback (most recent call last):
  ...
  File ".../repos/manticore/manticore/core/smtlib/expression.py", line 547, in __init__
    MASK = (1 << size) - 1
ValueError: negative shift count

Traceback (most recent call last):
  ...
  File ".../repos/manticore/manticore/core/smtlib/expression.py", line 547, in __init__
    MASK = (1 << size) - 1
OverflowError: too many digits in integer

Traceback (most recent call last):
  ...
  File ".../repos/manticore/manticore/core/smtlib/expression.py", line 547, in __init__
    MASK = (1 << size) - 1
MemoryError