Dynamic Path Pruning in Symbolic Execution

Abstract

To alleviate path explosion in symbolic execution, path pruning removes unsatisfiable paths at an early stage before they multiply. Although existing symbolic execution platforms have implemented several path pruning strategies to determine whether and when to check a path's satisfiability, it remains unclear how effective these strategies are because the time to check a path's satisfiability is non-negligible and may vary drastically. This work proposes dynamic path pruning (DPP), a strategy that aims to minimize the overall exploration time by dynamically adjusting the path checking rate. DPP assigns a higher checking rate to paths that are more likely to be unsatisfiable, and the likelihood is estimated based on the observed program's characteristics, such as the observed percentage of satisfiable paths. DPP is implemented on top of an open source symbolic execution platform in only a few hundred lines. Our evaluation confirms that DPP consistently achieves near-optimal exploration time for a wide spectrum of programs, whereas existing static path pruning strategies suffer from unacceptable worstcase performance due to their program-independent behaviors. Compared with static strategies, DPP performs best in 84% (110 out of 131) of CGC binaries, and the exploration time is within 100-124% of the best static strategy in 95% of the tested handcrafted and coreutils binaries.