0
# CrossHair
1

2
CrossHair is a Python analysis tool that uses symbolic execution and SMT solving to automatically find counterexamples for functions with type annotations and contracts. It blurs the line between testing and type systems by exploring viable execution paths through symbolic reasoning, making it a comprehensive solution for code correctness verification.
3

4
## Package Information
5

6
- **Package Name**: crosshair-tool
7
- **Language**: Python
8
- **Installation**: `pip install crosshair-tool`
9
- **License**: MIT
10
- **Console Commands**: `crosshair`, `mypycrosshair`
11

12
## Core Imports
13

14
```python
15
import crosshair
16
```
17

18
For symbolic execution and core functionality:
19

20
```python
21
from crosshair import (
22
    realize,
23
    deep_realize,
24
    register_type,
25
    register_patch,
26
    with_realized_args,
27
    SymbolicFactory,
28
    StateSpace,
29
    IgnoreAttempt
30
)
31
```
32

33
For tracing control:
34

35
```python
36
from crosshair import NoTracing, ResumedTracing
37
```
38

39
For debugging:
40

41
```python
42
from crosshair import debug
43
```
44

45
## Basic Usage
46

47
### Command Line Analysis
48

49
```bash
50
# Check a single function
51
crosshair check mymodule.py::my_function
52

53
# Check all functions in a module
54
crosshair check mymodule.py
55

56
# Watch for changes and auto-recheck
57
crosshair watch mymodule.py
58

59
# Generate unit tests
60
crosshair cover mymodule.py::my_function --coverage_type=pytest
61
```
62

63
### Programmatic Usage
64

65
```python
66
import crosshair
67
from crosshair import realize, SymbolicFactory, StateSpace
68

69
# Basic symbolic execution
70
def analyze_function(x: int) -> int:
71
    """
72
    pre: x > 0
73
    post: __return__ > x
74
    """
75
    return x + 1
76

77
# Using CrossHair's symbolic execution
78
from crosshair.core_and_libs import run_checkables
79
from crosshair.options import AnalysisOptions
80

81
options = AnalysisOptions()
82
# Analysis will find counterexamples if contracts can be violated
83
```
84

85
### Contract Verification
86

87
```python
88
from crosshair.register_contract import register_contract
89

90
def my_precondition(x):
91
    return x > 0
92

93
def my_postcondition(x, result):
94
    return result > x
95

96
# Register contract for function
97
register_contract(my_function, pre=my_precondition, post=my_postcondition)
98
```
99

100
## Architecture
101

102
CrossHair's symbolic execution engine consists of several key components:
103

104
- **StateSpace**: Manages SMT solver state and execution branches
105
- **SymbolicFactory**: Creates symbolic values for different types
106
- **Core Engine**: Handles symbolic execution, patching, and realization
107
- **Contract System**: Validates preconditions and postconditions
108
- **CLI Interface**: Provides command-line tools for analysis
109
- **LSP Server**: Enables IDE integration
110

111
The tool can analyze built-in types, user-defined classes, and much of the Python standard library through symbolic reasoning, making it comprehensive for code correctness verification.
112

113
## Capabilities
114

115
### Symbolic Execution Engine
116

117
Core symbolic execution functionality for creating and manipulating symbolic values, managing execution state, and converting between symbolic and concrete representations.
118

119
```python { .api }
120
def realize(value):
121
    """Convert symbolic values to concrete values."""
122

123
def deep_realize(value, memo=None):
124
    """Deeply convert symbolic values using copy mechanism."""
125

126
class SymbolicFactory:
127
    """Factory for creating symbolic values."""
128
    def __init__(self, space, pytype, varname): ...
129
    def __call__(self, typ, suffix="", allow_subtypes=True): ...
130

131
class StateSpace:
132
    """Holds SMT solver state and execution information."""
133
    def __init__(self, execution_deadline, model_check_timeout, search_root): ...
134
    def add(self, expr): ...
135
    def fork_parallel(self, false_probability, desc=""): ...
136
    def is_possible(self, expr): ...
137
```
138

139
[Symbolic Execution](./symbolic-execution.md)
140

141
### Command Line Interface
142

143
Comprehensive CLI tools for analyzing Python code, including checking contracts, watching for changes, generating tests, comparing function behaviors, and running an LSP server for IDE integration.
144

145
```python { .api }
146
def main(cmd_args=None):
147
    """Main CLI entry point."""
148

149
def check(args, options, stdout, stderr):
150
    """Check command implementation."""
151

152
def watch(args, options, max_watch_iterations=sys.maxsize):
153
    """Watch command implementation."""
154

155
def cover(args, options, stdout, stderr):
156
    """Cover command implementation."""
157

158
def diffbehavior(args, options, stdout, stderr):
159
    """Diff behavior command."""
160

161
def server(args, options, stdout, stderr):
162
    """LSP server implementation."""
163
```
164

165
[CLI Tools](./cli-tools.md)
166

167
### Contract Registration and Enforcement
168

169
System for registering and enforcing preconditions and postconditions on functions, enabling contract-based programming and verification.
170

171
```python { .api }
172
def register_contract(fn, *, pre=None, post=None, sig=None, skip_body=True):
173
    """Register contract for function."""
174

175
def clear_contract_registrations():
176
    """Clear all registered contracts."""
177

178
def get_contract(fn):
179
    """Get contract for function."""
180

181
class PreconditionFailed(BaseException):
182
    """Exception for precondition failures."""
183

184
class PostconditionFailed(BaseException):
185
    """Exception for postcondition failures."""
186

187
def WithEnforcement(fn):
188
    """Ensure conditions are enforced on callable."""
189
```
190

191
[Contract System](./contract-system.md)
192

193
### Behavioral Analysis and Comparison
194

195
Tools for analyzing and comparing the behavior of different function implementations, finding behavioral differences, and generating comprehensive behavior descriptions.
196

197
```python { .api }
198
def diff_behavior(*args):
199
    """Compare behaviors of functions."""
200

201
def describe_behavior(*args):
202
    """Describe function behavior."""
203

204
class BehaviorDiff:
205
    """Difference between function behaviors."""
206

207
class ExceptionEquivalenceType(enum.Enum):
208
    """Types of exception equivalence."""
209
    SAME_TYPE = ...
210
    SAME_TYPE_AND_MESSAGE = ...
211
    EXACT = ...
212
```
213

214
[Behavioral Analysis](./behavioral-analysis.md)
215

216
## Types
217

218
```python { .api }
219
class IgnoreAttempt(Exception):
220
    """Exception to ignore analysis attempts."""
221

222
class CrossHairInternal(Exception):
223
    """Internal CrossHair exception."""
224

225
class UnexploredPath(Exception):
226
    """Exception for unexplored execution paths."""
227

228
class NotDeterministic(Exception):
229
    """Exception for non-deterministic behavior."""
230

231
class PathTimeout(Exception):
232
    """Exception for path execution timeouts."""
233

234
class AnalysisKind(enum.Enum):
235
    """Types of analysis."""
236
    PEP316 = ...
237
    icontract = ...
238
    deal = ...
239
    hypothesis = ...
240
    asserts = ...
241

242
class AnalysisOptions:
243
    """Configuration options for analysis."""
244

245
class MessageType(enum.Enum):
246
    """Types of analysis messages."""
247
    CONFIRMED = ...
248
    CANNOT_CONFIRM = ...
249
    PRE_UNSAT = ...
250
    POST_FAIL = ...
251
    POST_ERR = ...
252
    EXEC_ERR = ...
253
    SYNTAX_ERR = ...
254
    IMPORT_ERR = ...
255
```