Multiplex Symbolic Execution: Exploring Multiple Paths by Solving Once

Path explosion and constraint solving are two challenges to symbolic execution's scalability. Symbolic execution explores the program's path space with a searching strategy and invokes the underlying constraint solver in a black-box manner to check the feasibility of a path. Inside the constraint solver, another searching procedure is employed to prove or disprove the feasibility. Hence, there exists the problem of double searchings in symbolic execution. In this paper, we propose to unify the double searching procedures to improve the scalability of symbolic execution. We propose Multiplex Symbolic Execution (MuSE) that utilizes the intermediate assignments during the constraint solving procedure to generate new program inputs. MuSE maps the constraint solving procedure to the path exploration in symbolic execution and explores multiple paths in one time of solving. We have implemented MuSE on two symbolic execution tools (based on KLEE and JPF) and three commonly used constraint solving algorithms. The results of the extensive experiments on real-world benchmarks indicate that MuSE has orders of magnitude speedup to achieve the same coverage.