Documentation Index
Fetch the complete documentation index at: https://mintlify.com/Z3Prover/z3/llms.txt
Use this file to discover all available pages before exploring further.
Symbolic execution uses Z3 to analyze programs by tracking symbolic values instead of concrete values. This powerful technique enables comprehensive path exploration, automatic bug detection, and vulnerability discovery.
When to Use Symbolic Execution
Use symbolic execution with Z3 when you need to:
- Explore execution paths: Systematically analyze all possible program paths
- Find bugs: Automatically discover crashes, assertion violations, and logic errors
- Detect vulnerabilities: Identify security issues like buffer overflows and injection flaws
- Generate exploits: Create inputs that trigger specific program behaviors
- Verify assertions: Prove or disprove program assertions
- Analyze binary code: Understand behavior of compiled programs
Core Concepts
Symbolic Execution Workflow
- Initialize symbolic variables: Replace inputs with symbolic values
- Execute symbolically: Track constraints along execution paths
- Fork at branches: Create separate paths for each branch condition
- Check path feasibility: Use Z3 to determine if paths are reachable
- Generate concrete inputs: Solve constraints to produce test cases
Path Exploration Strategies
- Depth-first search (DFS): Explore one path completely before backtracking
- Breadth-first search (BFS): Explore all paths at depth k before depth k+1
- Heuristic-guided: Prioritize paths likely to reach specific locations
- Concolic execution: Mix symbolic and concrete execution
Example: Simple Symbolic Execution
Symbolically execute a simple function:
from z3 import *
def symbolic_execute_simple():
"""
Symbolically execute:
def foo(x, y):
z = x + y
if z > 10:
if x > 5:
return "Path A" # Bug: division by zero
else:
return "Path B"
else:
return "Path C"
"""
x = Int('x')
y = Int('y')
z = Int('z')
paths = []
# Symbolic execution
s = Solver()
s.add(z == x + y) # z = x + y
# Path 1: z > 10 and x > 5
s.push()
s.add(z > 10)
s.add(x > 5)
if s.check() == sat:
m = s.model()
paths.append({
'name': 'Path A',
'x': m[x].as_long(),
'y': m[y].as_long(),
'z': m[z].as_long()
})
s.pop()
# Path 2: z > 10 and x <= 5
s.push()
s.add(z > 10)
s.add(x <= 5)
if s.check() == sat:
m = s.model()
paths.append({
'name': 'Path B',
'x': m[x].as_long(),
'y': m[y].as_long(),
'z': m[z].as_long()
})
s.pop()
# Path 3: z <= 10
s.push()
s.add(z <= 10)
if s.check() == sat:
m = s.model()
paths.append({
'name': 'Path C',
'x': m[x].as_long(),
'y': m[y].as_long(),
'z': m[z].as_long()
})
s.pop()
return paths
for path in symbolic_execute_simple():
print(f"{path['name']}: x={path['x']}, y={path['y']}, z={path['z']}")
Example: Buffer Overflow Detection
Detect buffer overflow vulnerabilities:
from z3 import *
def detect_buffer_overflow():
"""
Detect buffer overflow in:
void copy_data(int index, int value) {
int buffer[10];
buffer[index] = value; // Potential overflow
}
"""
index = BitVec('index', 32)
value = BitVec('value', 32)
buffer_size = 10
s = Solver()
# Check for overflow: index out of bounds
print("Checking for buffer overflow...")
# Case 1: Negative index
s.push()
s.add(index < 0)
if s.check() == sat:
m = s.model()
print(f" Overflow found: negative index = {m[index].as_signed_long()}")
s.pop()
# Case 2: Index too large
s.push()
s.add(index >= buffer_size)
if s.check() == sat:
m = s.model()
print(f" Overflow found: index = {m[index].as_long()} >= {buffer_size}")
s.pop()
# Case 3: Valid access
s.push()
s.add(index >= 0)
s.add(index < buffer_size)
if s.check() == sat:
m = s.model()
print(f" Valid access: index = {m[index].as_long()}")
s.pop()
detect_buffer_overflow()
Example: Path Exploration with Arrays
Symbolically execute code with array operations:
from z3 import *
def symbolic_array_search():
"""
Symbolically execute binary search:
def binary_search(arr, target):
low, high = 0, len(arr) - 1
while low <= high:
mid = (low + high) // 2
if arr[mid] == target:
return mid
elif arr[mid] < target:
low = mid + 1
else:
high = mid - 1
return -1
"""
# Symbolic array and target
arr = Array('arr', IntSort(), IntSort())
target = Int('target')
# Assume sorted array of size 5
n = 5
s = Solver()
# Array is sorted
for i in range(n - 1):
s.add(Select(arr, i) <= Select(arr, i + 1))
# Explore path where target is found at position 2
print("Path: Target found at index 2")
s.push()
s.add(Select(arr, 2) == target)
s.add(Select(arr, 1) < target) # Went right from mid=1
if s.check() == sat:
m = s.model()
print(f" target = {m[target]}")
print(f" arr[0..4] = ", end="")
print([m.evaluate(Select(arr, i)) for i in range(n)])
s.pop()
# Explore path where target is not found
print("\nPath: Target not found")
s.push()
for i in range(n):
s.add(Select(arr, i) != target)
if s.check() == sat:
m = s.model()
print(f" target = {m[target]}")
print(f" arr[0..4] = ", end="")
print([m.evaluate(Select(arr, i)) for i in range(n)])
s.pop()
symbolic_array_search()
Example: Integer Overflow Detection
Find integer overflow bugs:
from z3 import *
def detect_integer_overflow():
"""
Detect overflow in:
int calculate_total(int price, int quantity) {
int total = price * quantity;
if (total < price) {
// Overflow occurred
return -1;
}
return total;
}
"""
# 32-bit integers
price = BitVec('price', 32)
quantity = BitVec('quantity', 32)
total = BitVec('total', 32)
s = Solver()
# Model the computation
s.add(total == price * quantity)
# Realistic constraints
s.add(price > 0)
s.add(quantity > 0)
# Find overflow: result is less than inputs
print("Searching for multiplication overflow...")
s.add(total < price)
if s.check() == sat:
m = s.model()
p = m[price].as_signed_long()
q = m[quantity].as_signed_long()
t = m[total].as_signed_long()
print(f" Overflow found!")
print(f" price = {p}")
print(f" quantity = {q}")
print(f" total = {t} (expected: {p * q})")
print(f" Overflow: {p} * {q} overflows to {t}")
else:
print(" No overflow found with given constraints")
detect_integer_overflow()
Example: Assertion Violation
Find inputs that violate assertions:
from z3 import *
def find_assertion_violation():
"""
Find inputs violating assertion:
def process(x, y, z):
result = x + 2*y - z
assert result >= 0 # Assertion to check
return result
"""
x = Int('x')
y = Int('y')
z = Int('z')
result = Int('result')
s = Solver()
# Model the computation
s.add(result == x + 2*y - z)
# Input constraints
s.add(x >= 0, x <= 100)
s.add(y >= 0, y <= 100)
s.add(z >= 0, z <= 100)
# Violate assertion: result < 0
s.add(result < 0)
if s.check() == sat:
m = s.model()
print("Assertion violation found!")
print(f" x = {m[x]}")
print(f" y = {m[y]}")
print(f" z = {m[z]}")
print(f" result = {m[result]} (violates result >= 0)")
else:
print("No assertion violation found")
find_assertion_violation()
Example: Concolic Execution
Mix concrete and symbolic execution:
from z3 import *
class ConcolicExecutor:
def __init__(self):
self.solver = Solver()
self.symbolic_vars = {}
self.path_constraints = []
def make_symbolic(self, name, concrete_value):
"""Create symbolic variable with concrete value"""
sym_var = Int(name)
self.symbolic_vars[name] = sym_var
return sym_var
def add_constraint(self, constraint):
"""Add constraint to current path"""
self.path_constraints.append(constraint)
self.solver.add(constraint)
def explore_alternate_path(self):
"""Generate input for unexplored path"""
# Try negating last constraint
if not self.path_constraints:
return None
s = Solver()
# Add all constraints except last
for c in self.path_constraints[:-1]:
s.add(c)
# Negate last constraint
s.add(Not(self.path_constraints[-1]))
if s.check() == sat:
return s.model()
return None
# Example usage
def concolic_demo():
executor = ConcolicExecutor()
# Concrete execution with symbolic tracking
x = executor.make_symbolic('x', 5)
y = executor.make_symbolic('y', 3)
# Path: x > y
executor.add_constraint(x > y)
z = x + y
executor.add_constraint(z > 10)
print("Current path constraints:", executor.path_constraints)
# Explore alternate path
alt_model = executor.explore_alternate_path()
if alt_model:
print("Alternate path input:")
for var in executor.symbolic_vars.values():
print(f" {var} = {alt_model[var]}")
concolic_demo()
Path Pruning Strategies
Optimize exploration by pruning infeasible paths:
from z3 import *
def prune_infeasible_paths():
"""Prune paths that are infeasible"""
x = Int('x')
y = Int('y')
# Path constraints accumulated during execution
path_constraints = [
x > 0,
y > 0,
x + y < 5,
]
s = Solver()
for c in path_constraints:
s.add(c)
# Before exploring further, check feasibility
if s.check() == unsat:
print("Path is infeasible - pruning")
return False
print("Path is feasible - continuing exploration")
# Try adding new constraint
s.push()
s.add(x > 10) # This makes path infeasible
if s.check() == unsat:
print("New branch is infeasible - pruning")
s.pop()
return False
s.pop()
return True
prune_infeasible_paths()
Best Practices
- Use incremental solving: Leverage push/pop for efficient backtracking
- Bound exploration depth: Limit path depth to prevent infinite loops
- Cache solver queries: Reuse previous results when possible
- Prioritize interesting paths: Use heuristics to guide exploration
- Handle symbolic loops: Use loop summarization or bounded unrolling
- Simplify path conditions: Use tactics to simplify constraints
- Mix concrete and symbolic: Use concolic execution for efficiency
Handling Complex Features
Symbolic Memory
Model memory symbolically using arrays:
memory = Array('mem', BitVecSort(32), BitVecSort(8))
address = BitVec('addr', 32)
value = Select(memory, address)
memory = Store(memory, address, value)
Function Calls
Model function calls with summaries:
# Instead of symbolically executing strlen:
string_length = Int('strlen_result')
s.add(string_length >= 0)
s.add(string_length < 1000) # Reasonable bound
Loops
Unroll loops to fixed depth:
# Symbolically execute: for i in range(n)
max_iterations = 5
for i in range(max_iterations):
# Symbolic iteration body
pass
Theory Solvers for Symbolic Execution
Further Reading
examples/python/bounded model checking/bubble_sort.py: Array verificationexamples/java/JavaExample.java: Bit-vector examples for overflow detection- Academic papers on symbolic execution engines like KLEE, Angr, and S2E
