Dynamic Path Pruning in Symbolic Execution

Path pruning can alleviate path explosion in symbolic execution by removing unsatisfiable paths at their early stages before they grow into many. Although existing symbolic execution tools have implemented several strategies to remove unsatisfiable paths, it remains unclear how effective these strategies are because checking a path''s satisfiability also takes non-negligible time. This work formulates the path pruning problem and demonstrates that existing path pruning strategies suffer from unacceptable worst-case performance due to their program-independent behaviors. To this end, we propose dynamic path pruning (DPP), a path pruning strategy that consistently achieves near-optimal exploration time for a wide spectrum of programs. The intuition behind DPP is assigning a higher checking rate to paths that are more likely to be unsatisfiable. DPP finds the optimal checking rate by solving an optimization problem and adjusts to the optimal checking rate based on the observed program''s characteristic, including the observed percentage of satisfiable paths. DPP is implemented on top of an open-source symbolic execution platform in only hundred of lines. Our evaluation shows that using DPP for analyzing the coreutils will always yield near-optimal exploration time. We can also adjust the checking range and timeout in DPP to get more optimized in future work.