CrossHair

0.0.102 · active · verified Thu Apr 16

CrossHair is an analysis tool for Python that utilizes symbolic execution to blur the line between traditional testing and type systems. It works by repeatedly calling functions with symbolic inputs and employing an SMT solver to explore execution paths, finding counterexamples to contracts defined within docstrings. The library currently stands at version 0.0.102 and has a fairly active release cadence with frequent minor updates.

Common errors

```
CrossHair finds counterexamples for `float('nan')` or `float('inf')` where none were expected before.
```
cause As of version 0.0.102, CrossHair proactively tests float arguments with `math.nan`, `math.inf`, and `-math.inf` to find more robust counterexamples.

fix If your function is not expected to handle these special float values, add a precondition like `pre: math.isfinite(x)` to the function's contract. Alternatively, set the environment variable `CROSSHAIR_ONLY_FINITE_FLOATS=1` to disable this behavior.
```
The `crosshair cover` command with `--example_output_format=argument_dictionary` doesn't produce a dictionary output or gives a warning.
```
cause The option name for dictionary output was fixed/renamed in version 0.0.38.

fix Use the corrected option name: `crosshair cover --example_output_format=arg_dictionary`.
```
CrossHair analysis seems to ignore my function's `lru_cache` or `cache` decorator, leading to unexpected results or performance characteristics.
```
cause CrossHair intentionally disables `lru_cache` and `cache` decorators during symbolic execution to avoid non-deterministic behavior that can arise from caching in a symbolic context.

fix Adjust your contracts and expectations, recognizing that the caching mechanism will not be active during CrossHair's analysis. Ensure your function's core logic is correct without relying on the cache during formal verification.
```
Installation of `crosshair-tool` via pip is taking an unusually long time, seemingly stuck.
```
cause During installation, CrossHair often compiles its underlying SMT solver, Z3, from source. This process can be CPU-intensive and time-consuming on various platforms.

fix This is expected behavior. Allow sufficient time for the Z3 solver to compile. Ensure your system has a C++ compiler and related build tools installed, as these are typically required for the compilation.

Warnings

breaking CrossHair now tests float arguments with `math.nan`, `math.inf`, and `-math.inf` by default. This change in version 0.0.102 is likely to uncover new counterexamples in existing codebases that previously assumed finite float inputs.
Fix: Add `math.isfinite(x)` preconditions to your contracts for float arguments as appropriate, or set the environment variable `CROSSHAIR_ONLY_FINITE_FLOATS=1` to revert to previous behavior temporarily.
breaking The default stopping conditions have been fully re-worked. The `--per_condition_timeout` option is no longer the default. Instead, `--max_uninteresting_iterations=5` is used when no other stopping criteria are specified.
Fix: Adjust your command-line arguments to use `--max_uninteresting_iterations` instead of or in conjunction with `timeout` options, as it will adapt analysis time to problem difficulty.
deprecated The `--example_output_format=argument_dictionary` option for the `cover` command has been fixed and renamed to `--example_output_format=arg_dictionary`. The old option will issue a warning and be removed in future releases.
Fix: Update scripts to use `--example_output_format=arg_dictionary` when using the `cover` command.
gotcha CrossHair automatically disables `functools.lru_cache` and `functools.cache` decorators during analysis to prevent non-deterministic errors. Code relying on these caches for functional correctness might exhibit different behavior under analysis.
Fix: Be aware that caching will not be active during CrossHair analysis. Design contracts such that their correctness does not implicitly depend on the side effects or memoization provided by these caches during analysis.
gotcha Installation of `crosshair-tool` can take a significant amount of time on some platforms. This is due to the underlying Z3 SMT solver being compiled from source as part of the installation process.
Fix: Be patient during installation. Ensure you have the necessary build tools (e.g., C++ compiler) installed for your operating system.

Install

pip install crosshair-tool Install with pip

Imports

CLI tool
```
crosshair watch my_module.py
```
CrossHair is primarily used as a command-line interface (CLI) tool, not typically imported directly into Python code for analysis. Analysis is performed on Python files containing contracts.

Quickstart

Install CrossHair and then run it from the command line to watch your code for contract violations. Define post-conditions and other contracts within function docstrings. CrossHair will continuously analyze the specified files and report any counterexamples.

# my_code.py
def divide(a: int, b: int) -> float:
    """
    post: __return__ == a / b
    """
    return a / b

# Run CrossHair from your terminal:
# crosshair watch my_code.py

view raw JSON →