Skip to content

Symbolic Execution Deep Dive

Time: 30 minutes | Tools: symbolic_execute | Tier: Pro

Learn how symbolic execution explores every possible path through your code.

What You'll Learn

  • How symbolic execution works
  • Finding edge cases automatically
  • Understanding path constraints
  • Generating test inputs

What is Symbolic Execution?

Instead of running code with actual values like x = 5, symbolic execution uses symbolic values that represent all possible inputs.

Concrete Execution

classify(5)  # Returns "positive"
# Only tested ONE path

Symbolic Execution

classify(x)  # x is symbolic
# Explores ALL paths:
# - x < 0 → "negative"
# - x == 0 → "zero"  
# - x > 0 → "positive"

Step 1: Basic Symbolic Execution

Consider this function:

def classify_age(age):
    if age < 0:
        return "invalid"
    elif age < 18:
        return "minor"
    elif age < 65:
        return "adult"
    else:
        return "senior"

Run symbolic execution:

"Explore all paths through the classify_age function"

{
  "tool": "symbolic_execute",
  "parameters": {
    "code": "def classify_age(age):\n    if age < 0:\n        return \"invalid\"\n    elif age < 18:\n        return \"minor\"\n    elif age < 65:\n        return \"adult\"\n    else:\n        return \"senior\""
  }
}

Step 2: Understand the Results

{
  "data": {
    "paths": [
      {
        "id": 1,
        "constraints": ["age < 0"],
        "result": "\"invalid\"",
        "concrete_example": {"age": -1},
        "path_trace": [
          "line 2: if age < 0 → True",
          "line 3: return \"invalid\""
        ]
      },
      {
        "id": 2,
        "constraints": ["age >= 0", "age < 18"],
        "result": "\"minor\"",
        "concrete_example": {"age": 10},
        "path_trace": [
          "line 2: if age < 0 → False",
          "line 4: elif age < 18 → True",
          "line 5: return \"minor\""
        ]
      },
      {
        "id": 3,
        "constraints": ["age >= 18", "age < 65"],
        "result": "\"adult\"",
        "concrete_example": {"age": 30},
        "path_trace": [
          "line 2: if age < 0 → False",
          "line 4: elif age < 18 → False",
          "line 6: elif age < 65 → True",
          "line 7: return \"adult\""
        ]
      },
      {
        "id": 4,
        "constraints": ["age >= 65"],
        "result": "\"senior\"",
        "concrete_example": {"age": 70},
        "path_trace": [
          "line 2: if age < 0 → False",
          "line 4: elif age < 18 → False",
          "line 6: elif age < 65 → False",
          "line 9: return \"senior\""
        ]
      }
    ],
    "total_paths": 4,
    "coverage": {
      "lines_covered": [2, 3, 4, 5, 6, 7, 8, 9],
      "branch_coverage": "100%"
    }
  }
}

What Each Path Tells You

Path Constraints Example Result
1 age < 0 -1 "invalid"
2 0 ≤ age < 18 10 "minor"
3 18 ≤ age < 65 30 "adult"
4 age ≥ 65 70 "senior"

Step 3: Find Edge Cases

Symbolic execution reveals boundary conditions:

def calculate_discount(amount, is_member):
    if amount <= 0:
        raise ValueError("Amount must be positive")

    if is_member:
        if amount >= 100:
            return amount * 0.20  # 20% discount
        else:
            return amount * 0.10  # 10% discount
    else:
        if amount >= 200:
            return amount * 0.05  # 5% discount
        else:
            return 0  # No discount

"Find all paths and edge cases in calculate_discount"

Edge cases found:

Path Conditions Example Risk
1 amount ≤ 0 (0, True) Exception path
2 member, amount ≥ 100 (100, True) Boundary: exactly 100
3 member, amount < 100 (99, True) Just below boundary
4 non-member, amount ≥ 200 (200, False) Boundary: exactly 200
5 non-member, amount < 200 (199, False) Just below boundary

Step 4: Detect Bugs

Consider buggy code:

def divide_rewards(total, num_people):
    """Divide rewards equally among people."""
    per_person = total / num_people
    return per_person

Run symbolic execution:

{
  "data": {
    "paths": [
      {
        "id": 1,
        "constraints": ["num_people != 0"],
        "result": "total / num_people",
        "concrete_example": {"total": 100, "num_people": 5}
      },
      {
        "id": 2,
        "constraints": ["num_people == 0"],
        "result": "EXCEPTION: ZeroDivisionError",
        "concrete_example": {"total": 100, "num_people": 0}
      }
    ],
    "warnings": [
      {
        "type": "POTENTIAL_EXCEPTION",
        "path": 2,
        "exception": "ZeroDivisionError",
        "message": "Division by zero when num_people == 0"
      }
    ]
  }
}

Bug found! No check for zero people.

Step 5: Multiple Variables

Symbolic execution handles multiple variables:

def shipping_cost(weight, distance, express):
    base = weight * 0.5

    if distance < 100:
        rate = 1.0
    elif distance < 500:
        rate = 1.5
    else:
        rate = 2.0

    cost = base * rate

    if express:
        cost *= 2

    return cost

Paths explored:

# weight distance express rate multiplier
1 any < 100 False 1.0 1
2 any < 100 True 1.0 2
3 any 100-499 False 1.5 1
4 any 100-499 True 1.5 2
5 any ≥ 500 False 2.0 1
6 any ≥ 500 True 2.0 2

Total: 6 paths (2 distance zones × 2 express options × ...)

Step 6: Loop Handling

Symbolic execution handles loops with bounded unrolling:

def sum_positive(numbers):
    total = 0
    for n in numbers:
        if n > 0:
            total += n
    return total

With max_depth=3, explores: - Empty list - 1 positive number - 1 negative number - 2 numbers (combinations) - 3 numbers (combinations)

Supported Types

Type Support Notes
int Full All operations
bool Full All operations
float Basic Comparisons, arithmetic
str Basic Length, equality
list Limited Length, index
dict — Not supported

Configuration Options

Limit Paths

{
  "tool": "symbolic_execute",
  "parameters": {
    "code": "...",
    "max_paths": 50  // Stop after 50 paths
  }
}

Limit Depth

{
  "tool": "symbolic_execute",
  "parameters": {
    "code": "...",
    "max_depth": 5  // Max recursion/loop depth
  }
}

Try It Yourself

Exercise 1: Find All Paths

def validate_password(password):
    if len(password) < 8:
        return "too_short"
    if len(password) > 100:
        return "too_long"
    has_digit = any(c.isdigit() for c in password)
    has_upper = any(c.isupper() for c in password)
    if not has_digit:
        return "needs_digit"
    if not has_upper:
        return "needs_upper"
    return "valid"

"What are all possible return values from validate_password?"

Exercise 2: Find Bugs

def get_element(items, index):
    return items[index]

"What edge cases could cause this to fail?"

Exercise 3: Complex Conditions

def categorize(value, threshold, strict):
    if strict:
        if value > threshold:
            return "above"
        elif value < threshold:
            return "below"
        else:
            return "equal"
    else:
        if value >= threshold:
            return "above_or_equal"
        else:
            return "below"

"How many paths are in categorize?"

Key Takeaways

  1. Symbolic execution explores all paths - not just the ones you think of
  2. Constraints show requirements - what must be true for each path
  3. Concrete examples are test inputs - ready to use in tests
  4. Warnings reveal bugs - division by zero, None access, etc.
  5. Bounded by depth and paths - prevents infinite exploration

Next Tutorial

Use the symbolic findings in a broader engineering workflow: