Skip to main content

A static analysis tool for Python using symbolic execution.

Project description

CrossHair

Join the chat at https://gitter.im/Cross_Hair/Lobby codecov Build Status

A static analysis tool for Python that blurs the line between testing and type systems.

THE LATEST NEWS: Now you can try out CrossHair in your browser at crosshair-web.org!

If you have functions with type annotations and add some checks in a PEP 316-inspired syntax, CrossHair will attempt to find counterexamples for you:

Animated GIF demonstrating the verification of a python function

CrossHair works by repeatedly calling your functions with symbolic inputs. It uses an SMT solver (a kind of theorem prover) to explore viable execution paths and find counterexamples for you. This is not a new idea; an approach for Python was first described in this paper. However, to my knowledge, CrossHair is the most complete implementation of the idea: it supports symbolic lists, dictionaries, sets, and custom/mutable objects.

NOTE: CrossHair is in a highly experimental state right now. You can help though - keep reading!

Contents
Why Should I Use CrossHair?
How to Write Contracts
Get Started
IDE Integrations
Limitations
How Can I Help?
Contributors
Related Work

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:

Image showing an average function

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.

Image showing CrossHair caller and callee

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

Image showing CrossHair constract and inheritance

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

Image showing CrossHair constract and inheritance

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

Image showing mypy and CrossHair together

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

Image showing the equivalence of optimized an unoptimized 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.

Image showing a comment block with doctest and CrossHair conditions

How to Write Contracts

CrossHair largely follows the PEP 316 syntax for expressing "contracts." In short:

  • Place contracts inside the docstrings for functions.
  • Declare your post-conditions (what you expect to be true of the function's return value) like this:
    post: __return__ > 0
    • If you like, you can use a single underscore (_) as a short-hand for __return__.
  • Functions are checked if they have at least one post-condition line in their docstring.
  • Declare your pre-conditions (what you expect to be true of the function's inputs) like this:
    pre: x < y
  • Declare that your function mutates arguments with square brackets after the post keyword.
    • When doing so, the old values of the arguments are available in a special object called __old__:
      post[x]: x > __old__.x
    • Comparison for the purposes of mutation checking is a "deep" comparison.
    • Use empty square brackets to assert that the function does not mutate any argument.
  • If your function can validly raise certain exceptions, declare them like this:
    raises: IndexError, ZeroDivisionError
  • Declare class invariants in the class's docstring like this:
    inv: self.foo < self.bar
    • Class invariants apply additional pre- and post-conditions to each member function.
  • Note: Unlike contracts on standalone functions, contracts on class methods often encourage/require contracts on the entire class.
    • This is because you usually need invariants on the class to describe what states are valid, and then every method must be shown to preserve those invariants.

You can find examples in the examples/ directory and try it in your browser at crosshair-web.org.

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:

Image showing terminal output

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.

How Can I Help?

  • Try it out on your own python project! Be communicative about what does and doesn't work.
  • Participate (or just lurk) in the gitter chat.
  • File an issue.
  • Ask a question on stackoverflow.
  • Make a pull request. There aren't contributing guidlines yet - just check in on gitter to coordinate.
  • Help me evangalize: Share with your friends and coworkers. If you think it's neato, star the repo. :star:
  • Contact me at pschanely@gmail.com or Twitter... even if it's just to say that you'd like me to cc you on future CrossHair-related develoments.

Contributors

Name GitHub
Phillip Schanely @pschanely
Edward Haigh @oneEdoubleD

Related Work

Technology Relation
dependent types, refinement types CrossHair aims to provide many of the same capabilities as these advanced type systems. CrossHair is easier to learn (because it is just python), but is incomplete (it can't always tell you whether a condition holds).
design by contract Unlike other systems and tools for contracts, CrossHair statically attempts to verify pre- and post-conditions.
fuzz testing, QuickCheck, property testing, Hypothesis CrossHair has many of the same goals as these tools. However, CrossHair uses an SMT solver to find inputs rather than the (typically) randomized approaches that these tools use.
concolic testing State-of-the-art fuzz testers employ SMT solvers in a similar fashion as CrossHair.
SMT solvers SMT solvers power many of the tools in this table. CrossHair uses Z3.
angr, klee Symbolic execution of binary code. Unlike these tools, CrossHair models the semantics of Python directly.
PyExZ3, pySim, PEF Take approaches that are very similar to CrossHair, in various states of completeness. CrossHair is generally more perscriptive or product-like than these tools.

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Files for crosshair-tool, version 0.0.1
Filename, size File type Python version Upload date Hashes
Filename, size crosshair_tool-0.0.1-py3-none-any.whl (92.0 kB) File type Wheel Python version py3 Upload date Hashes View
Filename, size crosshair-tool-0.0.1.tar.gz (84.8 kB) File type Source Python version None Upload date Hashes View

Supported by

Pingdom Pingdom Monitoring Google Google Object Storage and Download Analytics Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN DigiCert DigiCert EV certificate StatusPage StatusPage Status page