Symbolic Execution (Z3 SMT Solver)

pip install z3-solver

TaintPropagator (enable_symbolic_execution=True)
    │
    ├─ find_taint_paths()  →  raw taint paths
    │
    └─ PathConstraintTracker.filter_infeasible_paths()
        │
        ├─ _collect_constraints(start, end)
        │   ├─ Walk CFG edges, extract branch conditions from CDG
        │   └─ _determine_branch_direction() via CFG successors
        │
        ├─ _parse_condition(code, z3_vars, state)
        │   └─ Recursive descent: or → and → not → comparison → additive → atom
        │       ├─ Variables: z3.Int('x')
        │       ├─ Functions: strlen(s) → fresh Int with domain constraints
        │       └─ NULL: z3.Bool('ptr_is_null')
        │
        └─ z3.Solver().check()  (with timeout)
            ├─ sat     → path feasible (confidence 0.9)
            ├─ unsat   → path infeasible, FILTER OUT (confidence 0.95)
            └─ unknown → conservative, keep path (confidence 0.4)

@dataclass
class PathConstraint:
    node_id: int       # CPG node ID of the branch
    condition: str     # Condition expression (e.g., "x > 100")
    location: str      # File:line location
    negated: bool      # True if this is the else-branch

@dataclass
class SymbolicExecutionConfig:
    enabled: bool = True
    max_constraints: int = 20
    solver_timeout_ms: int = 500        # QF_LIA queries
    solver_timeout_uf_ms: int = 2000    # Queries with uninterpreted functions
    max_parse_depth: int = 10           # Recursive descent depth limit
    enable_function_models: bool = True # strlen, sizeof, len models
    enable_arithmetic: bool = True      # +, -, * in conditions

class PathConstraintTracker:
    def __init__(self, cpg_service, max_constraints: int = 20,
                 config: Optional[SymbolicExecutionConfig] = None):
        """
        Args:
            cpg_service: CPGQueryService instance for graph queries
            max_constraints: Maximum constraints per path (default: 20).
                Paths with more constraints are assumed feasible to avoid solver timeout.
            config: Optional configuration for solver timeouts and features.
        """

    def is_path_feasible(self, start_node: int, end_node: int) -> Tuple[bool, float]:
        """
        Check if a path between two nodes is feasible.

        Returns:
            (is_feasible, confidence) — confidence ranges from 0.0 to 1.0
        """

    def filter_infeasible_paths(
        self, paths: List[Any], min_confidence: float = 0.8
    ) -> List[Any]:
        """
        Filter a list of taint paths, removing infeasible ones.

        Args:
            paths: List of taint path objects (must have .path_nodes attribute —
                   list of node IDs; first element = source, last = sink)
            min_confidence: Minimum confidence to consider a result reliable (default: 0.8)

        Returns:
            Filtered list with only feasible paths
        """

    def get_statistics(self) -> Dict[str, Any]:
        """
        Get solver statistics.

        Returns:
            Dictionary with keys:
            - z3_available (bool): Whether Z3 solver is installed
            - max_constraints (int): Maximum constraints per path
            - solver_timeout_ms (int): LIA query timeout
            - solver_timeout_uf_ms (int): UF query timeout
            - enable_function_models (bool): Function models enabled
            - enable_arithmetic (bool): Arithmetic enabled
            - supported_functions (list): Known function models
        """

from src.analysis.dataflow.symbolic_execution import PathConstraintTracker

tracker = PathConstraintTracker(cpg_service, max_constraints=20)

# Check a single path
is_feasible, confidence = tracker.is_path_feasible(node_123, node_456)
if not is_feasible and confidence > 0.9:
    print("Path is infeasible — likely false positive")

# Filter a batch of taint paths
feasible_paths = tracker.filter_infeasible_paths(all_paths, min_confidence=0.8)

from src.analysis.dataflow.taint_analysis import TaintPropagator

propagator = TaintPropagator(
    cpg_service,
    enable_symbolic_execution=True  # Enables Z3 path filtering
)

# Symbolic execution is applied automatically after taint propagation
paths = propagator.find_taint_paths(
    sources=["recv", "getenv"],
    sinks=["strcpy", "sprintf"]
)
# paths already filtered — infeasible paths removed

symbolic_execution:
  enabled: true
  max_constraints: 20
  solver_timeout_ms: 500
  solver_timeout_uf_ms: 2000
  max_parse_depth: 10
  enable_function_models: true
  enable_arithmetic: true