pschanely / CrossHair

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

Unexpected counterexample when indexing a symbolic sequence by a object of unknown type #200

Open pschanely opened 1 year ago

pschanely commented 1 year ago

Expected vs actual behavior We'd expect a counterexample in this case, but not the one we get:

example:

from typing import Sequence
def try_index(dd: Sequence[int], idx=0) -> None:
    """
    post: True    
    """
    return dd[idx]

actual output:

/tmp/main.py:6: error: TypeError: indices must be integers or slices, not <class 'crosshair.libimpl.builtinslib.SymbolicObject'> when calling try_index((), idx = '')

It's ok for crosshair to try various types for the idx param (it has a default but can legitimately be any type), but we expect the counterexample to be some sort of regular Python type, not a CrossHair internal type.

To Reproduce https://crosshair-web.org/?crosshair=0.1&python=3.8&flags=verbose&gist=015bea7c81fa2ebaf9bb7d01ccb655d5