Empc: Effective Path Prioritization for Symbolic Execution with Path Cover

TL;DR

Empc tackles the path-explosion problem in symbolic execution by reframing path prioritization as a minimum path cover (MPC) problem on the program’s inter-procedural CFG. It computes multiple MPCs on transformed, acyclic subgraphs to constrain exploration to a compact, diverse set of paths, then guides runtime execution by matching subpaths against these MPCs and using program dependence cues to recover infeasible prefixes. Implemented as a KLEE searcher in C++/LLVM, Empc delivers substantial gains in code coverage (≈19.6% more basic blocks, ≈24.4% more lines), large memory savings (up to 93.5%), and improved bug detection (≈24 additional violations) with modest runtime overhead. The approach combines graph-theoretic MPC techniques with dependence-based infeasible-path handling to provide a principled, scalable boost to symbolic execution, and is released as open source for broader adoption and experimentation.

Abstract

Symbolic execution is a powerful program analysis technique that can formally reason the correctness of program behaviors and detect software bugs. It can systematically explore the execution paths of the tested program. But it suffers from an inherent limitation: path explosion. Path explosion occurs when symbolic execution encounters an overwhelming number (exponential to the program size) of paths that need to be symbolically reasoned. It severely impacts the scalability and performance of symbolic execution. To tackle this problem, previous works leverage various heuristics to prioritize paths for symbolic execution. They rank the exponential number of paths using static rules or heuristics and explore the paths with the highest rank. However, in practice, these works often fail to generalize to diverse programs. In this work, we propose a novel and effective path prioritization technique with path cover, named Empc. Our key insight is that not all paths need to be symbolically reasoned. Unlike traditional path prioritization, our approach leverages a small subset of paths as a minimum path cover (MPC) that can cover all code regions of the tested programs. To encourage diversity in path prioritization, we compute multiple MPCs. We then guide the search for symbolic execution on the small number of paths inside multiple MPCs rather than the exponential number of paths. We implement our technique Empc based on KLEE. We conduct a comprehensive evaluation of Empc to investigate its performance in code coverage, bug findings, and runtime overhead. The evaluation shows that Empc can cover 19.6% more basic blocks than KLEE's best search strategy and 24.4% more lines compared to the state-of-the-art work cgs. Empc also finds 24 more security violations than KLEE's best search strategy. Meanwhile, Empc can significantly reduce the memory usage of KLEE by up to 93.5%.

Figures (9)

• Figure 1: This figure shows a motivating example including sample code, its CFG, path explosion problem and our minimum path cover method. Our method only uses 3 paths to cover all basic blocks of this program with 3 branches while the number of paths $|P|=6$ if there is a path explosion problem.
• Figure 2: Workflow of Empc.
• Figure 3: Transform an iCFG with caller-callee cycles into two subgraphs. The original iCFG contains two callers and the edges in yellow and purple are calling and returning edges in Figure \ref{['subfig:func_trans_ori']}. We transform the iCFG by adding a virtual return node in red in Figure \ref{['subfig:func_trans_vnode']}. We remove the calling and returning edges for graph split and mark them as dotted lines in Figure \ref{['subfig:func_trans_split']}. The right subgraph is a one-entry-one-exit subgraph.
• Figure 4: Transform the iCFG with loop cycles into two subgraphs without cycles. The original iCFG contains a loop with a loop body and a back edge in Figure \ref{['subfig:loop_trans_ori']}. The iCFG is transformed by removing back edges and adding several virtual nodes in red in Figure \ref{['subfig:loop_trans_vnode']}. The loop body is represented by a virtual node in the transformed iCFG and the virtual exit nodes match up with the exit nodes respectively. The loop entering and exiting edges are removed for graph split and marked as dotted lines in Figure \ref{['subfig:loop_trans_split']} and the right subgraph is a loop subgraph.
• Figure 5: The arithmetic mean internal coverage of basic blocks of Empc and all KLEE baseline search strategies running for 10 hours on 12 benchmark programs and one standard deviation error bars over 10 runs. The basic block coverage is computed via KLEE internal coverage.

Theorems & Definitions (7)

• Definition 1: One-Entry-One-Exit Subgraph
• Theorem 1
• Definition 2: Loop Subgraph
• Theorem 2
• Theorem 3
• Definition 3: Data Dependence
• Definition 4: Potential Dependence