Unexpected checking results for functions with/without type annotations

[eXceediDeaL]

Expected vs actual behavior

We found some unexpected outputs when we add/remove/modify the type annotations of functions, which might be confusing. Here are some minimalized examples and their behaviors.

def arithmetic_op(a, b):
    """
    post: True
    """
    result = a + b
    return result
# actual: /tmp/main.py:5: error: TypeError:  when calling arithmetic_op('', '')
# expect: counterexamples like arithmetic_op('', 0)

def arithmetic_op(a: list, b: str):
    """
    post: True
    """
    result = a + b
    return result
# actual: No counterexamples found.
# expect: counterexamples like arithmetic_op([], 0)

from typing import Optional
def arithmetic_op(a: 'int', b: 'Optional[complex]'):
    """
    post: True
    """
    result = a + b
    return result
# actual: No counterexamples found.
# expect: counterexamples like arithmetic_op(0, None)

def func(a: 'str'):
    """
    post: True
    """
    return a(1)
# actual: No counterexamples found.
# expect: counterexamples like func('')

def func2(a: 'int'):
    """
    post: True
    """
    return a(1)
# actual: exception raised, Numeric operation on symbolic while not tracing
# expect: counterexamples like func2(1)

[pschanely]

Thank you for the detailed reports!
I agree with your assessment about what should ideally happen in each case, and I consider the first and last examples to be outright bugs.

As a more general matter, CrossHair is meant to act as a compliment to a type checker like mypy, and I generally don't prioritize capabilities that would be subsumed by type checkers. (just because CrossHair is such a complex system; we need to take simplifying assumptions wherever we can find them)

It's been a busy week for me, but you can expect a more detailed update from me in a day or two. Please stand by!

[pschanely]

So, I've made fixes for examples 1 and 5 in v0.0.47. (Example 1 is a non-reproducible counterexample, and example 5 issues an internal error, both of which are always bugs)

As I alluded to earlier, examples 2, 3, and 4 should be detectable with a type checker, so I'm leaving them (and this ticket) open as nice-to-haves. Sadly, I likely won't prioritize them any time soon. (though I'm happy to walk someone through it if they want to attempt to make the changes themselves)

[eXceediDeaL]

Thank you for the rapid response and the fixes. It really works. I agree with the trade-off on the design of CrossHair and type checkers.

[pschanely]

Thanks! 😄 I hope you'll continue to stay in touch; either here in bugs/discussions or send me an email sometime and let me know what's working well and what isn't.

[pschanely]

BTW, examples 3 and 4 were fixed in v.0.0.79. That just leaves example 2 as still not yielding a counterexample.