Unable to meet precondition and too low coverage, why?

[LinqLover]

Pretty straightforward example:

def compare(version1, version2):
    """
    pre: isinstance(version1, str) and isinstance(version2, str) and len(version1) == 3 and len(version2) == 3

    post: __return__ in {-1, 0, 1}
    """
    v1 = version1.split(".")
    v2 = version2.split(".")
    for i in range(max(len(v1), len(v2))):
        v1i = int(v1[i]) if i < len(v1) else 0
        v2i = int(v2[i]) if i < len(v2) else 0
        if v1i > v2i:
            return 1
        elif v1i < v2i:
            return -1
    return 0

When I watch this file using the VS Code Extension, it says "Unable to meet precondition." If I remove the len() predicates, it works. I wonder why this is since these predicates should have a closed solution form.

Furthermore, I tried to generate tests for this method, but it only outputs a single test with two empty strings as arguments, which obviously covers a small part of the method only. This even happens when I raise both timeouts (per condition and per path) to 30 seconds.

I'm interested in understanding the functioning of this symbex engine and compare it to others. Thus, if I did not only make a stupid mistake in using CrossHair, I would also be very interested in a short explanation of these limitations. Thanks in advance!

[pschanely]

Thank you for the report! Running the check command via crosshair-web detects a ValueError, rather than "Unable to meet precondition": https://crosshair-web.org/?crosshair=0.1&python=3.8&flags=per_path_timeout%3D3&gist=10e6f5c07f97755618ce84851f30fe71 Possibly, you're just on a slightly older version of CrossHair?

But! Running crosshair cover, I agree that it fails to find important paths. Digging into this a bit, I believe you've hit a situation where we end up materializing some values sooner than is truly necessary. There is no fundamental reason CrossHair can't handle this kind of situation, and I think I can come up with a fairly straightforward fix (particularly if you aren't super concerned with the runtime) Life has been hectic recently, but I suspect I could knock something out by this weekend.

As you try out additional cases, I hope you'll continue to let me know about the ones that don't work that well! These kinds of examples are incredibly helpful.

[pschanely]

Among too many other things, this fell off my radar. But I've rediscovered it, and finally put a fix (for the failure to cover the function) in v0.0.45:

$ cat discussion195.py 
def compare(version1: str, version2: str):
    v1 = version1.split(".")
    v2 = version2.split(".")
    for i in range(max(len(v1), len(v2))):
        v1i = int(v1[i]) if i < len(v1) else 0
        v2i = int(v2[i]) if i < len(v2) else 0
        if v1i > v2i:
            return 1
        elif v1i < v2i:
            return -1
    return 0

$ crosshair cover discussion195.py --max_uninteresting_iterations=40 --example_output_format=pytest
from discussion195 import compare

def test_compare():
    assert compare('0', '0.1') == -1

def test_compare_2():
    assert compare('1', '0') == 1

def test_compare_3():
    assert compare('00', '0') == 0