crosshair check --report_all is having a hard time checking dictionaries

[Maykeye]

Consider the simplest phonebook which is just a wrapper around dict

def top(phones: dict[str, str], name: str, phone: str):
    """
    post: name in phones
    post: implies(not __return__, len(phones) == len(__old__.phones))
    post: implies(__return__, len(phones) == len(__old__.phones) + 1)
    post: implies(__return__, phones[name] == phone)
    """
    if name in phones:
        return False
    phones[name] = phone
    return True

trying to verify it leads to nothing:

$ crosshair check --report_all   phone1.py
/home/fella/src/crosshair-test/phone1.py:3: info: Not confirmed.
/home/fella/src/crosshair-test/phone1.py:4: info: Not confirmed.
/home/fella/src/crosshair-test/phone1.py:5: info: Not confirmed.
/home/fella/src/crosshair-test/phone1.py:6: info: Not confirmed.

(though if postcondition is changed to be incorrect, eg post: implies(__return__, len(phones) == len(__old__.phones)), crosshair has no trouble to find counterexample)
Trying to use typing.Dict (and/or omit [str, str]) doesn't help.

[pschanely]

First off, apologies for the delay in my response, and thanks for asking questions!

I imagine you already know this, but for other people wandering across this issue, when you use --report_all, CrossHair can answer in three different ways: confirmed, refuted, and not confirmed. The "not confirmed" response essentially means that CrossHair did not find a counterexample, but did not exhaust all paths.

This kind of output is hidden under a command line option because your result will be highly dependent on CrossHair implementation details, and it is exceedingly rare to exhaust all paths in realistic code. CrossHair's goals align much more closely with being a "smart bug finder" than a verification tool.

In this case, the dictionary is modeled as a dictionary of concrete size but symbolic contents. There is an implicit path fork here that decides the size. Because there are infinitely many possible sizes, there are infinitely many paths, and you will never reach the "confirmed" result.

You might be interested to read discussion #156 as well.

[pschanely]

I'll add that this may be a different result than if you try something like dict[int, int] - in this case, CrossHair (currently) chooses a modeling that is an SMT array and can confirm the properties with just the two path executions that you might expect.

[Maykeye]

I see, thanks