arabelatso/symbolic-execution-assistant
> Performs symbolic execution to detect potential errors by exploring execution paths, solving path constraints, and generating test inputs. Use when you need to analyze code for bugs like null dereferences, division by zero, buffer overflows, or assertion violations. Also use to generate test inputs that exercise different code paths, find edge cases, or explore all reachable program states. Supports Python, Java, and C/C++ through manual symbolic execution techniques and integration with tools like KLEE, angr, Z3, and Symbolic PathFinder.
npx skills add https://github.com/ArabelaTso/Skills-4-SE --skill symbolic-execution-assistantPerform symbolic execution analysis to detect errors and generate test inputs by exploring program paths with symbolic variables.
Symbolic execution executes code with symbolic values (representing any possible value) instead of concrete values. This allows exploring multiple execution paths simultaneously and detecting errors that might only occur with specific inputs.
Key Concepts:
Select the function and determine what to analyze for.
Questions to ask:
Example:
def calculate_discount(price, customer_type):
"""Calculate discount based on customer type."""
if customer_type == "premium":
discount = price * 0.2
elif customer_type == "regular":
discount = price * 0.1
else:
discount = 0
final_price = price - discount
return final_price
Analysis goals:
Replace concrete inputs with symbolic variables.
Manual Symbolic Execution:
Input: price = α (symbolic), customer_type = β (symbolic)
Initial constraints: α ∈ ℝ, β ∈ String
Initial state: { price: α, customer_type: β }
Using Python with Z3:
from z3 import *
# Create symbolic variables
price = Real('price')
customer_type = String('customer_type')
# Create solver
solver = Solver()
Using Java with Symbolic PathFinder (SPF):
// Annotate symbolic inputs
public static void calculate_discount(double price, String customer_type) {
// SPF will make these symbolic via configuration
}
Using C with KLEE:
#include <klee/klee.h>
int main() {
float price;
char customer_type[20];
klee_make_symbolic(&price, sizeof(price), "price");
klee_make_symbolic(customer_type, sizeof(customer_type), "customer_type");
calculate_discount(price, customer_type);
return 0;
}
Trace through code, tracking constraints for each branch.
Manual Execution Example:
State 0: { price: α, customer_type: β }
Path constraint: (none)
Branch 1: customer_type == "premium"
State 1a: { discount: α * 0.2, final_price: α - (α * 0.2) }
Path constraint: β = "premium"
Branch 2: customer_type == "regular"
State 1b: { discount: α * 0.1, final_price: α - (α * 0.1) }
Path constraint: β ≠ "premium" ∧ β = "regular"
Branch 3: else
State 1c: { discount: 0, final_price: α }
Path constraint: β ≠ "premium" ∧ β ≠ "regular"
Path Tree Visualization:
[Initial State]
price = α
customer_type = β
|
+----------------+----------------+
| | |
β = "premium" β = "regular" else
| | |
discount=α*0.2 discount=α*0.1 discount=0
Path 1 Path 2 Path 3
For detailed path tree construction techniques, see references/path_exploration.md.
Look for states where errors could occur.
Common Error Patterns:
| Error Type | Check For | Example Constraint |
|------------|-----------|-------------------|
| Division by zero | denominator == 0 | x / y where y = 0 |
| Null dereference | variable == null | obj.method() where obj = null |
| Buffer overflow | index >= array.length | arr[i] where i ≥ len(arr) |
| Assertion violation | assertion condition false | assert x > 0 where x ≤ 0 |
| Integer overflow | result > MAX_INT | a + b > 2³¹-1 |
| Negative array index | index < 0 | arr[i] where i < 0 |
Example with Division by Zero:
def safe_divide(a, b):
if b != 0:
return a / b
else:
return None
Symbolic execution:
State 0: { a: α, b: β }
Branch 1: b != 0
Path constraint: β ≠ 0
Result: α / β (safe)
Branch 2: b == 0
Path constraint: β = 0
Result: None (safe)
ERROR CHECK: Division by zero?
Constraint: β = 0 AND execution reaches "a / b"
Result: NO (the if-check prevents it)
Example with Null Dereference:
public int getLength(String str) {
if (str != null) {
return str.length();
}
return 0;
}
Symbolic execution:
State 0: { str: α }
Branch 1: str != null
Path constraint: α ≠ null
Result: α.length() (safe)
Branch 2: str == null
Path constraint: α = null
Result: 0 (safe)
ERROR CHECK: Null dereference?
Constraint: α = null AND execution reaches str.length()
Result: NO (protected by null check)
Use constraint solver to find concrete values that exercise each path or trigger errors.
Manual Constraint Solving:
For simple constraints, solve manually:
Path 1 constraint: β = "premium"
Solution: price = 100, customer_type = "premium"
Path 2 constraint: β ≠ "premium" ∧ β = "regular"
Solution: price = 100, customer_type = "regular"
Path 3 constraint: β ≠ "premium" ∧ β ≠ "regular"
Solution: price = 100, customer_type = "guest"
Using Z3 Solver (Python):
from z3 import *
# Define symbolic variables
price = Real('price')
customer_type = String('customer_type')
# Solve for Path 1: premium customer
solver = Solver()
solver.add(customer_type == StringVal("premium"))
solver.add(price > 0) # Add reasonable constraints
if solver.check() == sat:
model = solver.model()
print(f"Test input for Path 1: price={model[price]}, customer_type={model[customer_type]}")
# Solve for Path 2: regular customer
solver2 = Solver()
solver2.add(customer_type == StringVal("regular"))
solver2.add(price > 0)
if solver2.check() == sat:
model = solver2.model()
print(f"Test input for Path 2: price={model[price]}, customer_type={model[customer_type]}")
Using Z3 for Error Detection:
# Check for division by zero
a = Int('a')
b = Int('b')
solver = Solver()
solver.add(b == 0) # Error condition: divisor is zero
solver.add(a > 0) # Additional context
if solver.check() == sat:
model = solver.model()
print(f"ERROR: Division by zero possible with a={model[a]}, b={model[b]}")
For comprehensive constraint solving techniques, see references/constraint_solving.md.
Convert solved constraints into executable test cases.
Test Case Template:
import pytest
class TestCalculateDiscount:
# Path 1: Premium customer
def test_premium_customer(self):
"""Test premium customer path."""
# Generated from constraint: customer_type = "premium"
result = calculate_discount(100, "premium")
assert result == 80 # 100 - 20% discount
# Path 2: Regular customer
def test_regular_customer(self):
"""Test regular customer path."""
# Generated from constraint: customer_type = "regular"
result = calculate_discount(100, "regular")
assert result == 90 # 100 - 10% discount
# Path 3: Other customer type
def test_other_customer(self):
"""Test other customer type path."""
# Generated from constraint: customer_type ∉ {"premium", "regular"}
result = calculate_discount(100, "guest")
assert result == 100 # No discount
Java Test Cases:
import org.junit.Test;
import static org.junit.Assert.*;
public class TestCalculateDiscount {
@Test
public void testPremiumCustomer() {
// Path 1: Premium customer
double result = calculateDiscount(100.0, "premium");
assertEquals(80.0, result, 0.01);
}
@Test
public void testRegularCustomer() {
// Path 2: Regular customer
double result = calculateDiscount(100.0, "regular");
assertEquals(90.0, result, 0.01);
}
@Test
public void testOtherCustomer() {
// Path 3: Other customer
double result = calculateDiscount(100.0, "guest");
assertEquals(100.0, result, 0.01);
}
}
Document discovered paths, errors, and generated tests.
Report Template:
# Symbolic Execution Report: calculate_discount
## Function Analyzed
`calculate_discount(price, customer_type)`
## Paths Discovered
- **Path 1**: Premium customer (customer_type = "premium")
- Constraint: β = "premium"
- Behavior: 20% discount applied
- Test input: price=100, customer_type="premium"
- **Path 2**: Regular customer (customer_type = "regular")
- Constraint: β ≠ "premium" ∧ β = "regular"
- Behavior: 10% discount applied
- Test input: price=100, customer_type="regular"
- **Path 3**: Other customer types
- Constraint: β ∉ {"premium", "regular"}
- Behavior: No discount
- Test input: price=100, customer_type="guest"
## Errors Detected
None. All paths are safe.
## Generated Test Cases
3 test cases generated (see test_calculate_discount.py)
## Coverage
- Branch coverage: 100% (all 3 branches)
- Path coverage: 100% (all 3 paths)
## Recommendations
- Consider validating customer_type against known values
- Add explicit error handling for negative prices
Z3 Theorem Prover:
pip install z3-solver
angr (Binary Analysis Framework):
pip install angr
Crosshair (Symbolic Testing):
pip install crosshair-tool
Symbolic PathFinder (SPF):
JDart:
KLEE:
# Uses LLVM bitcode
clang -emit-llvm -c program.c -o program.bc
klee program.bc
Symbolic Execution Engine (SEE):
For detailed tool setup and usage, see references/tool_integration.md.
Path explosion occurs when the number of paths grows exponentially.
Mitigation Strategies:
# Limit loop iterations
for i in range(min(len(array), 10)): # Max 10 iterations
process(array[i])
if not is_feasible(path_constraint):
prune_path()
# Merge states with same program counter
if state1.pc == state2.pc:
merged_state = merge(state1, state2)
# Prioritize paths with error conditions
if contains_error_check(path):
explore_first(path)
# Start with concrete value, switch to symbolic when needed
x = 5 # Concrete initially
if complex_condition(x):
x = make_symbolic(x) # Switch to symbolic
1. Bug Detection
2. Test Generation
3. Security Analysis
4. Equivalence Checking
For detailed information on specific topics:
Take arabelatso/symbolic-execution-assistant from the repository into ~/.claude/skills for personal
use, or into .claude/skills inside a project.
The agent identifies a skill by the name field in its header. Two skills with the
same name cannot sit side by side — one of them will be ignored.
The instructions reference pip.
Without those the skill loads but fails at the first command.