Skip to content

symbolic_execute

Explore all possible execution paths through code using symbolic execution with Z3 solver, identifying edge cases and potential bugs.

Quick Reference

symbolic_execute(
    code: str,                   # Code to analyze
    max_depth: int = None,       # Max path depth
    max_paths: int = None        # Max paths to explore
) -> SymbolicResult

User Stories

Persona Story Tool Value
🛡️ Marcus (Security Engineer) "Explore execution paths systematically to find edge cases" Edge case discovery
🔧 Chris (OSS Contributor) "Generate tests for symbolic execution edge cases" Comprehensive test coverage
👥 David (Team Lead) "Identify untested code paths before release" Test completeness

→ See all user stories

Parameters

Parameter Type Required Default Description
code string Yes - Python code to analyze
max_depth int No tier-based Maximum execution depth
max_paths int No tier-based Maximum paths to explore

Response Schema

{
  "data": {
    "paths": [
      {
        "id": "integer",
        "constraints": ["string"],
        "result": "any",
        "is_error": "boolean",
        "error_type": "string | null",
        "variables": {
          "var_name": "value"
        }
      }
    ],
    "coverage": {
      "lines_covered": ["integer"],
      "branches_covered": ["integer"],
      "total_paths": "integer"
    },
    "potential_issues": [
      {
        "type": "string",
        "description": "string",
        "path_id": "integer",
        "constraints": ["string"]
      }
    ],
    "summary": {
      "total_paths": "integer",
      "error_paths": "integer",
      "success_paths": "integer"
    }
  },
  "tier_applied": "string",
  "duration_ms": "integer"
}

Examples

Analyze a Function

Symbolically execute this function to find edge cases:

def calculate_discount(price: int, quantity: int) -> int:
    if quantity < 0:
        raise ValueError("Invalid quantity")
    if price <= 0:
        return 0
    if quantity >= 10:
        return price * quantity * 0.9
    elif quantity >= 5:
        return price * quantity * 0.95
    else:
        return price * quantity

{
  "code": "def calculate_discount(price: int, quantity: int) -> int:\n    if quantity < 0:\n        raise ValueError(\"Invalid quantity\")\n    if price <= 0:\n        return 0\n    if quantity >= 10:\n        return price * quantity * 0.9\n    elif quantity >= 5:\n        return price * quantity * 0.95\n    else:\n        return price * quantity"
}

codescalpel symbolic-execute \
  --code "def calculate_discount(price: int, quantity: int) -> int:\n    if quantity < 0:\n        raise ValueError(\"Invalid quantity\")\n    if price <= 0:\n        return 0\n    if quantity >= 10:\n        return price * quantity * 0.9\n    elif quantity >= 5:\n        return price * quantity * 0.95\n    else:\n        return price * quantity"

{
  "data": {
    "paths": [
      {
        "id": 1,
        "constraints": ["quantity < 0"],
        "result": "ValueError('Invalid quantity')",
        "is_error": true,
        "error_type": "ValueError",
        "variables": {"price": "any", "quantity": -1}
      },
      {
        "id": 2,
        "constraints": ["quantity >= 0", "price <= 0"],
        "result": 0,
        "is_error": false,
        "variables": {"price": 0, "quantity": 5}
      },
      {
        "id": 3,
        "constraints": ["quantity >= 0", "price > 0", "quantity >= 10"],
        "result": "price * quantity * 0.9",
        "is_error": false,
        "variables": {"price": 100, "quantity": 10}
      },
      {
        "id": 4,
        "constraints": ["quantity >= 0", "price > 0", "quantity >= 5", "quantity < 10"],
        "result": "price * quantity * 0.95",
        "is_error": false,
        "variables": {"price": 100, "quantity": 7}
      },
      {
        "id": 5,
        "constraints": ["quantity >= 0", "price > 0", "quantity < 5"],
        "result": "price * quantity",
        "is_error": false,
        "variables": {"price": 100, "quantity": 3}
      }
    ],
    "coverage": {
      "lines_covered": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10],
      "branches_covered": [1, 2, 3, 4, 5],
      "total_paths": 5
    },
    "potential_issues": [],
    "summary": {
      "total_paths": 5,
      "error_paths": 1,
      "success_paths": 4
    }
  },
  "tier_applied": "community",
  "duration_ms": 85
}

Find Division by Zero

Check this function for potential division by zero:

def calculate_average(total: int, count: int) -> float:
    if count == 0:
        return 0
    return total / count

{
  "code": "def calculate_average(total: int, count: int) -> float:\n    if count == 0:\n        return 0\n    return total / count"
}

codescalpel symbolic-execute \
  --code "def calculate_average(total: int, count: int) -> float:\n    if count == 0:\n        return 0\n    return total / count"

{
  "data": {
    "paths": [
      {
        "id": 1,
        "constraints": ["count == 0"],
        "result": 0,
        "is_error": false,
        "variables": {"total": "any", "count": 0}
      },
      {
        "id": 2,
        "constraints": ["count != 0"],
        "result": "total / count",
        "is_error": false,
        "variables": {"total": 100, "count": 5}
      }
    ],
    "potential_issues": [],
    "summary": {
      "total_paths": 2,
      "error_paths": 0,
      "success_paths": 2
    }
  }
}

Detect Unreachable Code

Analyze this code for unreachable paths:

def process(x: int) -> str:
    if x > 10:
        if x < 5:  # Unreachable!
            return "impossible"
        return "large"
    return "small"

{
  "code": "def process(x: int) -> str:\n    if x > 10:\n        if x < 5:\n            return \"impossible\"\n        return \"large\"\n    return \"small\""
}

codescalpel symbolic-execute \
  --code "def process(x: int) -> str:\n    if x > 10:\n        if x < 5:\n            return \"impossible\"\n        return \"large\"\n    return \"small\""

{
  "data": {
    "paths": [
      {
        "id": 1,
        "constraints": ["x > 10"],
        "result": "large",
        "is_error": false
      },
      {
        "id": 2,
        "constraints": ["x <= 10"],
        "result": "small",
        "is_error": false
      }
    ],
    "potential_issues": [
      {
        "type": "UNREACHABLE_CODE",
        "description": "Branch 'x < 5' inside 'x > 10' is never satisfiable",
        "line": 3,
        "constraints": ["x > 10", "x < 5"]
      }
    ],
    "coverage": {
      "lines_covered": [1, 2, 5, 6],
      "unreachable_lines": [3, 4]
    }
  }
}

Complex Conditions

Explore all paths through this validation function:

def validate_user(age: int, has_license: bool, score: int) -> str:
    if age < 18:
        return "too_young"
    if not has_license:
        return "no_license"
    if score < 70:
        return "failed"
    if score >= 90:
        return "excellent"
    return "passed"

{
  "code": "def validate_user(age: int, has_license: bool, score: int) -> str:\n    if age < 18:\n        return \"too_young\"\n    if not has_license:\n        return \"no_license\"\n    if score < 70:\n        return \"failed\"\n    if score >= 90:\n        return \"excellent\"\n    return \"passed\""
}

codescalpel symbolic-execute \
  --code "def validate_user(age: int, has_license: bool, score: int) -> str:\n    if age < 18:\n        return \"too_young\"\n    if not has_license:\n        return \"no_license\"\n    if score < 70:\n        return \"failed\"\n    if score >= 90:\n        return \"excellent\"\n    return \"passed\""

{
  "data": {
    "paths": [
      {
        "id": 1,
        "constraints": ["age < 18"],
        "result": "too_young",
        "variables": {"age": 17, "has_license": "any", "score": "any"}
      },
      {
        "id": 2,
        "constraints": ["age >= 18", "has_license == False"],
        "result": "no_license",
        "variables": {"age": 25, "has_license": false, "score": "any"}
      },
      {
        "id": 3,
        "constraints": ["age >= 18", "has_license == True", "score < 70"],
        "result": "failed",
        "variables": {"age": 25, "has_license": true, "score": 50}
      },
      {
        "id": 4,
        "constraints": ["age >= 18", "has_license == True", "score >= 70", "score >= 90"],
        "result": "excellent",
        "variables": {"age": 25, "has_license": true, "score": 95}
      },
      {
        "id": 5,
        "constraints": ["age >= 18", "has_license == True", "score >= 70", "score < 90"],
        "result": "passed",
        "variables": {"age": 25, "has_license": true, "score": 80}
      }
    ],
    "summary": {
      "total_paths": 5,
      "error_paths": 0,
      "success_paths": 5
    }
  }
}

Supported Types

Type Status Notes
int ✅ Full Integer arithmetic and comparisons
bool ✅ Full Boolean logic
str ✅ Basic String operations (length, equality)
float ✅ Basic Floating point (approximations)
list ⚠️ Limited Fixed-size lists only
dict ⚠️ Limited Basic operations
Custom objects ❌ Not supported

Tier Limits

symbolic_execute capabilities vary by tier:

Feature Community Pro Enterprise
Max paths 50 Unlimited Unlimited
Max depth 10 100 Unlimited
Constraint types int, bool, string, float + list, dict All + custom
Loop unrolling 5 iterations 20 iterations Configurable
String constraints Basic ✅ Advanced ✅ Advanced
Smart path prioritization ❌ ✅ ✅
Concolic execution ❌ ✅ ✅
Timeout 30 seconds 120 seconds 600 seconds

Community Tier

  • ✅ Explore up to 50 execution paths
  • ✅ Support for int, bool, string, float constraints
  • ✅ Basic loop unrolling (5 iterations)
  • ✅ Detect edge cases and potential bugs
  • ⚠️ Max 50 paths - May miss some edge cases
  • ⚠️ Max depth 10 - Shallow analysis
  • ⚠️ Limited types - No list/dict support
  • ❌ No smart path prioritization

Pro Tier

  • ✅ All Community features
  • ✅ Unlimited paths - Complete path exploration
  • ✅ Max depth 100 - Deep analysis
  • ✅ List and dict support - Complex data structures
  • ✅ Advanced string constraints - Better string analysis
  • ✅ Smart path prioritization - Focus on likely bugs
  • ✅ Concolic execution - Hybrid concrete/symbolic
  • ✅ 120 second timeout - Handle complex functions

Enterprise Tier

  • ✅ All Pro features
  • ✅ Unlimited depth - No analysis limits
  • ✅ All constraint types - Including custom objects
  • ✅ Configurable loop unrolling - Fine-tune analysis
  • ✅ 600 second timeout - Very complex functions
  • ✅ Distributed execution - Parallel path exploration
  • ✅ Custom solvers - Use domain-specific solvers

Key Difference: Path Coverage and Type Support - Community: 50 paths, depth 10, basic types - Quick edge case detection - Pro: Unlimited paths, depth 100, list/dict - Thorough analysis - Enterprise: Unlimited, all types, configurable - Complete verification

→ See tier comparison

Potential Issues Detected

Issue Type Description
DIVISION_BY_ZERO Possible divide by zero
INDEX_OUT_OF_BOUNDS Array index may be invalid
UNREACHABLE_CODE Code that can never execute
NULL_DEREFERENCE Potential None access
INTEGER_OVERFLOW Large integer operations
INFINITE_LOOP Loop may not terminate

Best Practices

  1. Keep functions focused - Smaller functions = better analysis
  2. Use type hints - Helps symbolic execution understand types
  3. Check potential_issues - These highlight real bugs
  4. Review edge cases - Generated test values reveal boundaries
  5. Use with generate_unit_tests - Convert paths to test cases