CrossHair Documentation

A common plugin pattern involves re-implementing the classes and functions of a native package in pure Python, then telling CrossHair to use these implementations instead of the originals.

Key API components:

• register_type(original_class, replacement_class): Maps an original class to your pure-Python replacement.
• register_patch(original_function, replacement_function): Maps an original function to your pure-Python replacement.
• SymbolicFactory: Passed to your replacement class's __init__ method. You can use it to create symbolic values for other types (e.g., factory(int)).

from crosshair import register_patch, register_type, SymbolicFactory
from bunnies import Bunny, introduce_bunnies

class _Bunny:
    happiness: int
    def __init__(self, factory: SymbolicFactory):
        self.happiness = factory(int)

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

def _introduce_bunnies(bunny1: AnyBunny, bunny2: AnyBunny) -> None:
    bunny1.happiness += 1
    bunny2.happiness += 1

register_type(bunnies.Bunny, _Bunny)
register_patch(bunnies.introduce_bunnies, _introduce_bunnies)

When using CrossHair for property-based testing, be aware of the following constraints to avoid false confidence or unexpected results:

• Absence of counterexamples: If CrossHair does not find a counterexample, it does not guarantee that the property holds. It only means no counterexample was found within the current search space/constraints.
• Symbolic value identity: Symbolic values are implemented as Python proxy values. While CrossHair attempts to maintain the illusion of real values, identity checks (e.g., x is y) may not be correctly analyzed.
• Scope of analysis: CrossHair only analyzes function and class definitions located at the top level. It does not analyze nested functions or classes.
• Determinism requirement: CrossHair can only analyze deterministic behavior. If the code produces different results for the same input, CrossHair may raise a NotDeterministic error.
• Iterator and Generator consumption: Consuming values from an iterator or a generator within a pre-condition or post-condition will result in unexpected behavior.

CrossHair uses a concolic-style approach to explore code paths without performing AST or bytecode analysis. Instead, it repeatedly calls your target function using special proxy objects that mimic standard Python types but hold underlying Z3 SMT solver expressions.

Type Mapping

CrossHair maps Python types to specific symbolic types and Z3 sorts:

Path Exploration Mechanism

When the Python interpreter encounters a conditional (e.g., if symbolic_x > 0:), it calls the __bool__ method on the resulting symbolic boolean object. CrossHair then:

1. Consults Z3 to see if the expression is forced to be True or False by current constraints.
2. If the outcome is ambiguous, it makes a decision (randomly) and adds that decision as a new constraint to the current execution path.
3. This allows CrossHair to explore different branches in subsequent executions.

When a target state is reached (like an unhandled exception or a failed postcondition), CrossHair requests a model from Z3 to provide a concrete counterexample.

CrossHair performs symbolic execution by actually executing your contracted functions, but it uses special symbolic arguments and intercepts standard Python behaviors.

Important considerations for developers:

• Side Effects: Never target code that causes side effects (e.g., disk or network access). While CrossHair uses sys.addaudithook to attempt to block these, it is not foolproof, especially with C-based modules.
• Printing: Avoid using print() on symbolic values. Printing forces symbolic values to take on concrete values, which can significantly hamper CrossHair's ability to perform effective analysis.
• Execution Flow: CrossHair may or may not execute preconditions/postconditions, and it may execute subroutines out-of-order.
• Bypassing Protections: If running in a containerized or isolated environment, you can use the --unblock command-line option to bypass CrossHair's internal protections.