RecursionError in AND and OR smtlib operators

[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 is the potential for RecursionError in the core.smtlib.operators.AND and core.smtlib.operators.OR functions.

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 xifaras.s@northeastern.edu. 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 AND/OR with a large number of arguments for the others star argument.

Expected behavior

No RecursionError (this can be achieved by revising these function to use a non-recursive implementation)

Actual behavior

Stack traces:

Traceback (most recent call last):
  ...
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 52, in AND
    b = AND(b, others[0], *others[1:])
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 52, in AND
    b = AND(b, others[0], *others[1:])
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 52, in AND
    b = AND(b, others[0], *others[1:])
  [Previous line repeated 2977 more times]
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 52, in AND
    b = AND(b, others[0], *others[1:])
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 52, in AND
    b = AND(b, others[0], *others[1:])
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 52, in AND
    b = AND(b, others[0], *others[1:])
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 51, in AND
    if len(others) > 0:
RecursionError: maximum recursion depth exceeded in comparison

Traceback (most recent call last):
  ...
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 63, in OR
    b = OR(b, others[0], *others[1:])
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 63, in OR
    b = OR(b, others[0], *others[1:])
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 63, in OR
    b = OR(b, others[0], *others[1:])
  [Previous line repeated 2977 more times]
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 63, in OR
    b = OR(b, others[0], *others[1:])
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 63, in OR
    b = OR(b, others[0], *others[1:])
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 63, in OR
    b = OR(b, others[0], *others[1:])
  File ".../repos/manticore/manticore/core/smtlib/operators.py", line 62, in OR
    if len(others) > 0:
RecursionError: maximum recursion depth exceeded in comparison