pschanely / CrossHair

An analysis tool for Python that blurs the line between testing and type systems.
Other
1.04k stars 49 forks source link

python's `sum` function causes internal issues #322

Open Abhiram98 opened 4 days ago

Abhiram98 commented 4 days ago

I'm trying to use crosshair's diffbehavior analysis, to find the equivalence (or lack thereof) of these two functions:

def original(int_list: list[int]):
    count = 0
    for i in int_list:
       count +=i
    return count
def rewrite(int_list: list[int]):
    count = 0
    for sublist in int_list:
        count += sum(sublist)
    return count

Crosshair fails to find a conterexample, even though something simple like int_list=[123] would work. It seems like crosshair throws an internal error, which stops it from proceeding with its analysis. Here's a jist of the internal error

__exit__() Proxy intolerace: 'SymbolicInt' object is not iterable at Traceback (most recent call last):
  File "crosshair/diff_behavior.py", line 72, in describe_behavior
    ret = fn(*args.args, **args.kwargs)
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "temp/test.py", line 5, in original
    for i in int_list:
             ^^^^^^^^
  File "crosshair/objectproxy.py", line 332, in __iter__
    return iter(self._wrapped())
           ^^^^^^^^^^^^^^^^^^^^^
TypeError: 'SymbolicInt' object is not iterable

PS: Thank you for the awesome tool!