The crosshair Package

crosshair.register_type(typ: Type, creator: Callable[[SymbolicFactory], object] | Callable[[SymbolicFactory, Type], object] | Callable[[SymbolicFactory, Type, Type], object] | Callable[[SymbolicFactory, Type, Type, Type], object] | Callable[[SymbolicFactory, Type, Type, Type, Type], object]) → None[source]

Register a custom creation function to create symbolic values for a type.

Parameters:

  • typ – The Python type (or typing annotation) to handle.

  • creator – A function that takes a SymbolicFactory instance and returns a symbolic value. When creating a parameterized type (e.g. List[int]), type parameters will be given to creator as additional arguments following the factory.

class crosshair.SymbolicFactory(space: StateSpace, pytype: object, varname: str)[source]

A callable object that creates symbolic values.

__call__(typ: Callable[[...], _T], suffix: str = '', allow_subtypes: bool = True) → _T[source]
__call__(typ: Any, suffix: str = '', allow_subtypes: bool = True) → Any

Create a new symbolic value.

Parameters:

  • typ (type) – The corresponding Python type for the returned symbolic.

  • suffix (str) – A descriptive suffix used to name variable(s) in the solver.

  • allow_subtypes (bool) – Whether it’s ok to return a subtype of given type.

Returns:

A new symbolic value.

class crosshair.StateSpace(execution_deadline: float, model_check_timeout: float, search_root: RootNode)[source]

Holds various information about the SMT solver’s current state.

Methods:

add(expr)

is_possible(expr)

add(expr: ExprRef) → None[source]
is_possible(expr: ExprRef) → bool[source]
class crosshair.NoTracing[source]
class crosshair.ResumedTracing[source]