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:

duplicate_list

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:

average

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.

zipped_pairs

Verify across all implementations. Contracts are particularly helpful when applied to base classes / interfaces: all implementations will be verified against them:
chess_pieces

Catch errors. Setting a trivial post-condition of "True" is enough to enable analysis, which will find exceptions like index out-of-bounds errors:

index_bounds

Support your type checker. CrossHair is a nice companion to mypy. Assert statements divide work between the two systems:

pair_with_mypy

Optimize with Confidence. Using post-conditions, CrossHair ensures that optimized code continues to behave like equivalent naive code:

csv_first_column

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.

even_fibb

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:

example_error

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.
  • 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.

GitHub