CrossHair
A static analysis tool for Python that blurs the line between testing and type systems.
If you have functions with type annotations and add some checks in PEP 316-inspired syntax, CrossHair will attempt to find counterexamples for you:
Why Should I Use CrossHair?
More precision. Commonly, we care about more than just the type. Is it really any integer, or is it a positive integer? Is it any list, or does it have to be a non-empty list? CrossHair gives you that precision:
Interprocedural analysis. CrossHair (1) validates the pre-conditions of called functions and (2) uses post-conditions of called functions to help it prove post-conditions in the caller.
Verify across all implementations. Contracts are particularly helpful when applied to base classes / interfaces: all implementations will be verified against them:
Catch errors. Setting a trivial post-condition of "True" is enough to enable analysis, which will find exceptions like index out-of-bounds errors:
Support your type checker. CrossHair is a nice companion to mypy. Assert statements divide work between the two systems:
Optimize with Confidence. Using post-conditions, CrossHair ensures that optimized code continues to behave like equivalent naive code:
Cover doctest's blind spots. Doctest is great
for illustrative examples and CrossHair can document behavior more holistically. Some kinds of
projects may be able to skip unittest/pytest entirely.
Get Started
NOTE: CrossHair is in a highly experimental state right now. If you're using it, it's because you want it to succeed, want to help, or are just interested in the technology.
Inside the development environment of the code you want to analyze (virtual environment, conda environment, etc), install:
pip install git+https://github.com/pschanely/crosshair
CrossHair works best when it sits in its own window and thinks about your code while you work on it. Open such a window, activate your development environment, and run:
crosshair watch [directory with code to analyze]
You should then see perodically updating text as CrossHair analyzes the contracts in your code. It will watch for changes as re-analyze as appropriate. When it detects an issue, you'll see something like this:
Hit Ctrl-C to exit.
IDE Integrations
As mentioned above, CrossHair wants to run in the background so it can have plenty of time to think. However, IDE integrations can still be used to catch easy cases.
If you make a plugin for your favorite editor (please do!), submit a pull request to add it above. The crosshair check [FILENAME]
command will yield results in the same format as the mypy type checker. (a non-zero exit for for errors, and lines formatted as {FILENAME}:{LINE_NUMBER}:error:{MESSAGE}
)
Limitations
A (wildly incomplete) list of present limitations. Some of these will be lifted over time (your help is welcome!); some may never be lifted.
- Symbolic values are implemented as Python proxy values. CrossHair monkey-patches the system to maintain a good illusion, but the illusion is not complete. For example,
- Code that cares about the identity values (x is y) may not be correctly analyzed.
- Code that cares about the types of values may not be correctly analyzed.
- Only function and class definitions at the top level are analyzed. (i.e. not when nested inside other functions/classes)
- Only deteministic behavior can be analyzed. (your code always does the same thing when starting with the same values)
- CrossHair may produce a
NotDeterministic
error when it detects this.
- CrossHair may produce a
- Comsuming values of an iterator/generator in a pre- or post-condition will produce unexpected behavior.
- Be aware that the absence of a counterexample does not guarantee that the property holds.
- SMT sovlers have very different perspectives on hard problems and easy problems than humans.
- Be prepared to be surprised both by what CrossHair can tell you, and what it cannot.