Plugins

Plugins give you hooks to intercept CrossHair when it is about to create a symbolic value or invoke a function. Most commonly, plugin modules help CrossHair understand 3rd party packages that are implemented in C. (also known as “extension modules”)

CrossHair will generally understand 3rd party packages written in pure Python out-of-the-box.

Using Plugins

Just install the plugin package the same way you added “crosshair-tool”. CrossHair will detect its presence automatically, so that’s all there is to it!

If you write your own plugin, let us know so we can reference it here.

Note

You can also use a plugin on a per-execution basis by using the --extra_plugin command line option, followed by plugin module files.

Writing Plugins

You can author and distribute plugins as regular python packages. To let CrossHair know that your package is a plugin, define an “entry point” for your distribution with a key of crosshair.plugin. Here is an example setup.py for a hypothetical plugin module, “crosshair_plugin_bunnies”:

# setup.py

from setuptools import setup
setup(
    name="crosshair-plugin-bunnies",
    py_modules=["crosshair_plugin_bunnies"],
    entry_points={"crosshair.plugin": ["bunnies = crosshair_plugin_bunnies"]},
)

Reimplementing Classes and Functions

Typically, your plugin will re-implement the classes and functions of the native package, and then tell CrossHair to use those instead.

Here is an example plugin package that attempts to mimic a hypothetical native Python package called bunnies.

# crosshair_plugin_bunnies.py

from crosshair import register_patch, register_type, SymbolicFactory

# import the original, native implementations:
from bunnies import Bunny, introduce_bunnies

# Replicate the native "Bunny" class in pure Python:

class _Bunny:
    happiness: int
    def __init__(self, factory: SymbolicFactory):
        # CrossHair will pass your constructor a factory that you can use to create
        # more symbolic values of any other type.
        self.happiness = factory(int)

    def pet(self: _Bunny) -> None:
        self.happiness += 1

# Replicate functions too:

AnyBunny = Union[Bunny, _Bunny]  # arguments can be any kind of Bunny
def _introduce_bunnies(bunny1: AnyBunny, bunny2: AnyBunny) -> None:
    bunny1.happiness += 1
    bunny2.happiness += 1


# Tell CrossHair to use these implementations instead of the native ones:
register_type(bunnies.Bunny, _Bunny)
register_patch(bunnies.introduce_bunnies, _introduce_bunnies)

Adding Contracts to External Functions

Re-writing classes and functions certainly takes some time; alternatively, you can directly apply contracts to external functions without re-implementing them. During analysis, CrossHair will skip executing such functions. Instead, it will check if the preconditions hold and then assume the postconditions are satisfied.

Note

In addition to registering contracts for functions implemented in C, one might wish to register pure Python functions to account for nondeterministic behavior, or to simply reduce the amount of code that CrossHair has to execute. (this can be particularly useful when trying to use CrossHair for software verification )

As an example, suppose you want to use random.randint in your code but CrossHair cannot exhaustively verify it because of its non-deterministic behavior. You can register a contract for this function as follows:

from crosshair.register_contract import register_contract
from random import Random
register_contract(
    Random.randint,
    pre=lambda a, b: a <= b,
    post=lambda __return__, a, b: a <= __return__ <= b,
)

Note

The names a and b above come from the definition of randint. These names must be correct and CrossHair will throw an error if you register contracts with other argument names. In order to find the correct names, look for the source code or the documentation of the function.

If you register a function for which CrossHair cannot infer the signature, a ContractRegistrationError will be raised. In such cases, you need to register the signature for the function as well. As an example here, we will register the function numpy.random.randint (note that numpy is a C module):

from crosshair.register_contract import register_contract
import numpy as np
from inspect import Parameter, Signature
randint_sig = Signature(
    parameters=[
        Parameter("self", Parameter.POSITIONAL_OR_KEYWORD),
        Parameter("low", Parameter.POSITIONAL_OR_KEYWORD, annotation=int),
        Parameter("high", Parameter.POSITIONAL_OR_KEYWORD, annotation=int),
    ],
    return_annotation=int,
)
register_contract(
    np.random.RandomState.randint,
    pre=lambda low, high: low < high,
    post=lambda __return__, low, high: low <= __return__ < high,
    sig=randint_sig,
)

Now assume you write the following test:

import numpy as np
def myrandom(a: int) -> int:
    """
    pre: a < 10
    post: _ > a
    """
    return np.random.randint(a, 10)

When you run crosshair check on this test file, with the above plugin, you will see the fault:

error: false when calling myrandom(0)
with crosshair.patch_to_return(numpy.random.mtrand.RandomState.randint: [0]})

This is telling you that if you call myrandom(0) and randint returns 0, the postcondition fails. Indeed, the postcondition is wrong and should be _ >= a instead!

Note

The crosshair.patch_to_return(...) expression above may be used in a with statement to reproduce the failure.

Note

The code above was just an example to show how to register a signature along with the contract. In reality, numpy.random.randint is overloaded and you should register a list of signatures instead of only one.

Note

You might have noticed that we registered np.random.RandomState.randint and not np.random.randint. This is because the latter is a bound function (it is the method of a particular RandomState instance). However, we want to register the class function directly, so that our contract holds when calling randint on any RandomState instance. Note that for most functions, you will not have to think about this at all. For curious people: If you look into the source code of numpy.random.mtrand.pyx, you will see how the bound function is defined: _rand = RandomState() and then randint = _rand.randint. We indeed see that this is the method of a specific instance of RandomState.