0
# Symbolic Execution Engine
1

2
CrossHair's symbolic execution engine provides the core functionality for creating and manipulating symbolic values, managing execution state, and performing symbolic reasoning. This system enables the tool to explore execution paths and find counterexamples automatically.
3

4
## Capabilities
5

6
### Value Realization
7

8
Convert symbolic values to concrete representations for inspection and debugging.
9

10
```python { .api }
11
def realize(value):
12
    """
13
    Convert symbolic values to concrete values.
14
    
15
    Parameters:
16
    - value: Any symbolic or concrete value
17
    
18
    Returns:
19
    Concrete representation of the value
20
    """
21

22
def deep_realize(value, memo=None):
23
    """
24
    Deeply convert symbolic values using copy mechanism.
25
    
26
    Parameters:
27
    - value: Value to realize
28
    - memo: Optional memoization dictionary to handle circular references
29
    
30
    Returns:
31
    Deeply realized value with all nested symbolic values converted
32
    """
33
```
34

35
**Usage Example:**
36

37
```python
38
from crosshair import realize, deep_realize
39

40
# Realize a simple symbolic value
41
concrete_val = realize(symbolic_int)
42

43
# Deep realization for complex nested structures
44
complex_data = {"items": [symbolic_list], "metadata": symbolic_dict}
45
concrete_data = deep_realize(complex_data)
46
```
47

48
### Symbolic Value Creation
49

50
Create symbolic values for different Python types to enable symbolic execution.
51

52
```python { .api }
53
class SymbolicFactory:
54
    """
55
    Factory for creating symbolic values of various types.
56
    
57
    The SymbolicFactory is the primary interface for creating symbolic values
58
    during symbolic execution. It maintains the connection to the StateSpace
59
    and handles type-specific symbolic value creation.
60
    """
61
    
62
    def __init__(self, space, pytype, varname):
63
        """
64
        Initialize symbolic factory.
65
        
66
        Parameters:
67
        - space: StateSpace instance managing solver state
68
        - pytype: Python type for the factory
69
        - varname: Base variable name for created symbols
70
        """
71
    
72
    def __call__(self, typ, suffix="", allow_subtypes=True):
73
        """
74
        Create symbolic value of given type.
75
        
76
        Parameters:
77
        - typ: Type to create symbolic value for
78
        - suffix: Optional suffix for variable name uniqueness
79
        - allow_subtypes: Whether to allow subtypes of the specified type
80
        
81
        Returns:
82
        Symbolic value of the specified type
83
        """
84
    
85
    def get_suffixed_varname(self, suffix):
86
        """
87
        Get unique variable name with suffix.
88
        
89
        Parameters:
90
        - suffix: Suffix to append
91
        
92
        Returns:
93
        Unique variable name string
94
        """
95
```
96

97
**Usage Example:**
98

99
```python
100
from crosshair import SymbolicFactory, StateSpace
101

102
# Create a symbolic factory
103
space = StateSpace(deadline, timeout, root)  
104
factory = SymbolicFactory(space, int, "x")
105

106
# Create symbolic integers
107
sym_int1 = factory(int)
108
sym_int2 = factory(int, suffix="alt")
109

110
# Create symbolic values for custom types
111
sym_custom = factory(MyCustomClass, allow_subtypes=False)
112
```
113

114
### Execution State Management
115

116
Manage SMT solver state and execution branching during symbolic execution.
117

118
```python { .api }
119
class StateSpace:
120
    """
121
    Holds SMT solver state and execution information.
122
    
123
    StateSpace manages the Z3 SMT solver instance, tracks execution branches,
124
    handles constraint solving, and provides utilities for symbolic execution.
125
    """
126
    
127
    def __init__(self, execution_deadline, model_check_timeout, search_root):
128
        """
129
        Initialize state space.
130
        
131
        Parameters:
132
        - execution_deadline: Maximum execution time
133
        - model_check_timeout: Timeout for SMT solver queries
134
        - search_root: Root node for execution tree
135
        """
136
    
137
    def add(self, expr):
138
        """
139
        Add constraint to solver.
140
        
141
        Parameters:
142
        - expr: Z3 expression to add as constraint
143
        """
144
    
145
    def fork_parallel(self, false_probability, desc=""):
146
        """
147
        Create execution fork with specified probability.
148
        
149
        Parameters:
150
        - false_probability: Probability of taking false branch (0.0-1.0)
151
        - desc: Optional description for debugging
152
        
153
        Returns:
154
        Boolean indicating which branch was taken
155
        """
156
    
157
    def is_possible(self, expr):
158
        """
159
        Check if expression could be true given current constraints.
160
        
161
        Parameters:
162
        - expr: Z3 expression to check
163
        
164
        Returns:
165
        True if expression is satisfiable, False otherwise
166
        """
167
    
168
    def choose_possible(self, expr_choices):
169
        """
170
        Choose from possible expressions based on satisfiability.
171
        
172
        Parameters:
173
        - expr_choices: List of Z3 expressions to choose from
174
        
175
        Returns:
176
        First satisfiable expression from the list
177
        """
178
    
179
    def find_model_value(self, expr):
180
        """
181
        Find model value for SMT expression.
182
        
183
        Parameters:
184
        - expr: Z3 expression to find value for
185
        
186
        Returns:
187
        Concrete value satisfying the expression in current model
188
        """
189
    
190
    def smt_fork(self, expr):
191
        """
192
        Fork execution based on SMT expression.
193
        
194
        Parameters:
195
        - expr: Z3 boolean expression to fork on
196
        
197
        Returns:
198
        Boolean indicating which branch (true/false) was taken
199
        """
200
    
201
    def defer_assumption(self, description, checker):
202
        """
203
        Defer assumption checking until later in execution.
204
        
205
        Parameters:
206
        - description: Human-readable description of assumption
207
        - checker: Callable that returns boolean for assumption validity
208
        """
209
    
210
    def rand(self):
211
        """
212
        Get random number generator.
213
        
214
        Returns:
215
        Random.Random instance for this execution path
216
        """
217
    
218
    def extra(self, typ):
219
        """
220
        Get extra data of specified type.
221
        
222
        Parameters:
223
        - typ: Type of extra data to retrieve
224
        
225
        Returns:
226
        Extra data instance of specified type
227
        """
228
    
229
    def uniq(self):
230
        """
231
        Get unique identifier.
232
        
233
        Returns:
234
        Unique integer identifier for this state space
235
        """
236
```
237

238
**Usage Example:**
239

240
```python
241
from crosshair import StateSpace
242
import z3
243

244
# Create state space
245
space = StateSpace(deadline=30.0, timeout=5.0, root=None)
246

247
# Add constraints
248
x = z3.Int('x')
249
space.add(x > 0)
250
space.add(x < 100)
251

252
# Check possibilities
253
if space.is_possible(x == 50):
254
    print("x could be 50")
255

256
# Fork execution
257
if space.smt_fork(x > 50):
258
    # Handle x > 50 case
259
    print("Exploring x > 50")
260
else:
261
    # Handle x <= 50 case  
262
    print("Exploring x <= 50")
263
```
264

265
### Function Patching and Registration
266

267
Register patches and custom symbolic types for extending symbolic execution capabilities.
268

269
```python { .api }
270
def register_patch(entity, patch_value):
271
    """
272
    Register a patch for a callable.
273
    
274
    Parameters:
275
    - entity: Callable to patch
276
    - patch_value: Replacement callable to use during symbolic execution
277
    """
278

279
def register_type(typ, creator):
280
    """
281
    Register custom symbolic value creator for a type.
282
    
283
    Parameters:
284
    - typ: Type to register creator for  
285
    - creator: Callback function that creates symbolic values of this type
286
    """
287

288
def with_realized_args(fn, deep=False):
289
    """
290
    Decorator that realizes function arguments before calling.
291
    
292
    Parameters:
293
    - fn: Function to wrap
294
    - deep: Whether to perform deep realization of arguments
295
    
296
    Returns:
297
    Wrapped function that realizes arguments before execution
298
    """
299

300
class patch_to_return:
301
    """
302
    Context manager for patching functions to return specific values.
303
    
304
    Allows temporary patching of functions during symbolic execution
305
    to control their return values for testing purposes.
306
    """
307
    
308
    def __init__(self, return_values):
309
        """
310
        Initialize patch context.
311
        
312
        Parameters:
313
        - return_values: Dict mapping callables to lists of return values
314
        """
315
    
316
    def __enter__(self):
317
        """Enter patch context."""
318
        
319
    def __exit__(self, *args):
320
        """Exit patch context and restore original functions."""
321
```
322

323
**Usage Example:**
324

325
```python
326
from crosshair import register_patch, register_type, with_realized_args, patch_to_return
327

328
# Register a patch for a function
329
def mock_database_call():
330
    return "mocked_result"
331

332
register_patch(real_database_call, mock_database_call)
333

334
# Register custom type creator
335
def create_symbolic_custom_type(space, typ, varname):
336
    # Return symbolic instance of custom type
337
    return SymbolicCustomType(varname)
338

339
register_type(MyCustomType, create_symbolic_custom_type)
340

341
# Use argument realization decorator
342
@with_realized_args
343
def debug_function(x, y):
344
    print(f"Called with concrete values: {x}, {y}")
345
    return x + y
346

347
# Temporary function patching
348
with patch_to_return({expensive_function: [42, 100, -1]}):
349
    # expensive_function will return 42, then 100, then -1 on successive calls
350
    result1 = expensive_function()  # Returns 42
351
    result2 = expensive_function()  # Returns 100
352
```
353

354
### Tracing Control
355

356
Control symbolic execution tracing for performance and debugging.
357

358
```python { .api }
359
def NoTracing():
360
    """
361
    Context manager to disable tracing.
362
    
363
    Returns:
364
    Context manager that disables CrossHair's execution tracing
365
    """
366

367
def ResumedTracing():
368
    """
369
    Context manager to resume tracing.
370
    
371
    Returns:
372
    Context manager that re-enables CrossHair's execution tracing
373
    """
374

375
def is_tracing():
376
    """
377
    Check if currently tracing.
378
    
379
    Returns:
380
    True if tracing is currently enabled, False otherwise
381
    """
382
```
383

384
**Usage Example:**
385

386
```python
387
from crosshair import NoTracing, ResumedTracing, is_tracing
388

389
# Disable tracing for performance-critical sections
390
with NoTracing():
391
    # This code runs without CrossHair tracing overhead
392
    result = expensive_computation()
393

394
# Resume tracing when needed
395
with ResumedTracing():
396
    # This code runs with full tracing enabled
397
    analyzed_result = analyze_result(result)
398

399
# Check tracing status
400
if is_tracing():
401
    print("Tracing is active")
402
```
403

404
### Utility Functions
405

406
Additional utilities for type handling and debugging during symbolic execution.
407

408
```python { .api }
409
def python_type(obj):
410
    """
411
    Get the Python type of an object, handling symbolic objects.
412
    
413
    Parameters:
414
    - obj: Object to get type of
415
    
416
    Returns:
417
    Python type, properly handling symbolic value types
418
    
419
    For symbolic objects with __ch_pytype__ method, returns the actual
420
    Python type being symbolically represented rather than the symbolic
421
    wrapper type. Raises CrossHairInternal if called while tracing.
422
    """
423

424
def normalize_pytype(typ):
425
    """
426
    Normalize type annotations for symbolic execution.
427
    
428
    Parameters:
429
    - typ: Type to normalize
430
    
431
    Returns:
432
    Normalized type suitable for symbolic execution
433
    
434
    Handles TypeVar bounds (converting to bound type or object), 
435
    converts Any to object, and handles other type system complexities 
436
    to produce types suitable for symbolic value creation.
437
    """
438

439
def debug(*args):
440
    """
441
    Print debugging information in CrossHair's nested log output.
442
    
443
    Parameters:
444
    - *args: Arguments to print for debugging
445
    """
446
```
447

448
**Usage Example:**
449

450
```python
451
from crosshair import python_type, normalize_pytype, debug
452

453
# Get type of symbolic values
454
sym_val = create_symbolic_int()
455
actual_type = python_type(sym_val)  # Returns int, not symbolic wrapper type
456

457
# Normalize complex type annotations  
458
from typing import List, Optional
459
normalized = normalize_pytype(Optional[List[int]])
460

461
# Debug symbolic execution
462
debug("Current symbolic value:", sym_val, "Type:", actual_type)
463
```