Assert post-conditions not recognized

[dslinger-a2]

Expected vs actual behavior
A clear and concise description of what you expected to happen.
I'm experiencing a number of instances of assert post-conditions not being recognized. The documentation is a bit sparse on assert post-conditions, so maybe there's something I am doing wrong.

To Reproduce
If appropriate, enter your test case into crosshair-web.org, create a gist, and link to it here!
Please try to minimize the size/complexity of your test case. Thanks!
Two examples recreated with crosshair-web:
https://crosshair-web.org/?gist=aea70ac11fac42fcabda865357349beb&crosshair=0.1&python=3.8&flags=verbose%2Creport_all%2Canalysis_kind%3Dasserts

https://crosshair-web.org/?gist=c07aef7fb924625e4e2730e8b54b026a&crosshair=0.1&python=3.8&flags=verbose%2Creport_all%2Canalysis_kind%3Dasserts

[pschanely]

@dslinger-a2: Hi! Thanks for trying out crosshair and especially for filing issues when you notice issues!

Assert-based contracts are a little odd, and you are not the first person to hit this particular stumbling block.

So that crosshair doesn't accidentally analyze functions that aren't meant to be tested, there are restrictions on what functions are considered. The key thing to know is that your function's first statement must be an assert statement. Often this will be a precondition, but when you have no preconditions, you'll still have to add an assert True at the top.

Although this requirement is buried in the docs, I think something needs to be updated to make it more obvious.

Another usability improvement idea: issue an error message when the crosshair command fails to find any testable targets.

I'll leave this issue open to consider these ideas; let me know if you have some too!

[dslinger-a2]

@pschanely That makes sense! I understood that any precondition asserts had to come first, but I didn't think of using assert True when there weren't preconditions. One option to consider would be extending the PEP316 docstring structure to have a focus like Deal's pure decorator. That would allow for a standard way of noting what functions are intended to be pure (and then make it very clear what functions can be run in crosshair). I liked Deal's ability to have that but the issue I had with Deal is how it alters the traceback of the function, so the intended exception is no longer raised (and then pytest tests have to be altered to accommodate the new exceptions). An additional option could be having a separate dedicated library for marking pure functions with a decorator like how Deal does but not take on the rest of what Deal focuses on.

I have a separate clarification that maybe belongs in a separate ticket but it may relate to the considerations here. If the PEP316 docstring specifies the expected raised exceptions (like a ValueError), what happens if a different ValueError is possible than the expected one? Does crosshair recognize the difference between exceptions raised directly in the function and other unforeseen exceptions?

[pschanely]

@pschanely That makes sense! I understood that any precondition asserts had to come first, but I didn't think of using assert True when there weren't preconditions. One option to consider would be extending the PEP316 docstring structure to have a focus like Deal's pure decorator. That would allow for a standard way of noting what functions are intended to be pure (and then make it very clear what functions can be run in crosshair). I liked Deal's ability to have that but the issue I had with Deal is how it alters the traceback of the function, so the intended exception is no longer raised (and then pytest tests have to be altered to accommodate the new exceptions). An additional option could be having a separate dedicated library for marking pure functions with a decorator like how Deal does but not take on the rest of what Deal focuses on.

I like these ideas. I'd call out that there might be other reasons you don't want to analyze pure functions. Sometimes, you have a helper function that can fail in ways that are difficult to describe with preconditions, but when zooming out to a caller function, the preconditions become expressable. I guess this relates to some of your questions below.

If the PEP316 docstring specifies the expected raised exceptions (like a ValueError), what happens if a different ValueError is possible than the expected one?

CrossHair will detect and report any exceptions that aren't declared as expected. Note that subclasses of the declared exception are also ignored, so you can say something like raises: Exception to ignore all exceptions.

Does crosshair recognize the difference between exceptions raised directly in the function and other unforeseen exceptions?

No. CrossHair will report any exception that is raised at any depth during the execution of the function under analysis. Partly, this is because the concolic approach that CrossHair employs needs us to actually run all of that code anyway. Which is also part of why you might want to be a little selective about what "entry points" you give to CrossHair.

[dslinger-a2]

@pschanely Thank you for being receptive! Just throwing some ideas out there for consideration and totally understand deciding against them!

One additional thought I have from that feedback is creating a custom precondition exception. I just tried creating one (called PreConditionError). It seems to be hitting a potential bug though with crosshair with some functions. (ValueError: wrong parameter order: keyword-only parameter before variadic positional parameter) It might be worth considering making a PreConditionError part of crosshair. Then if that is raised it definitely won't hide other exceptions like specifying ValueError or TypeError would. I have a preference for making most preconditions exceptions, as they shouldn't happen (and I think can easily be understood by other developers). The only kind of preconditions that I would prefer not to be an exception are when the arguments to the function are already the output of post-conditions of another function, in which case it gets a bit repetitive (but would potentially be simplified with #201 ).

One other thought about a PEP316 change for function purity would be naming it Side-Effects:. I can see your point about instances of pure functions not wanting to be tested, but I would think the combo of having that in the docstring and having some other form of post-condition makes it pretty clear what should and shouldn't be ran in crosshair. (And in the case of asserts, requiring --analysis_kind=asserts)

Thank you for your work on crosshair! It's really cool!

EDIT: Nevermind about the error I thought I had. Think that's resolved.