Compositional Symbolic Execution with Memoized Replay
Rui Qiu, Guowei Yang, Corina S. Păsăreanu, Sarfraz Khurshid · Texas ScholarWorks (Texas Digital Library) · 2014
Abstract—Symbolic execution is a powerful, systematic analy-sis that has received much visibility in the last decade. Scalability however remains a major challenge for symbolic execution. Com-positional analysis is a well-known general purpose methodology for increasing scalability. This paper introduces a new approach for compositional symbolic execution. Our key insight is that we can summarize each analyzed method as a memoization tree that captures the crucial elements of symbolic execution, and leverage these memoization trees to efficiently replay the symbolic execution of the corresponding methods with respect to their calling contexts. Memoization trees offer a natural way to compose in the presence of heap operations, which cannot be dealt with by previous work that uses logical formulas as summaries for compositional symbolic execution. Our approach also enables efficient target oriented symbolic execution for error detection or program coverage. Initial experimental evaluation based on a prototype implementation in Symbolic PathFinder shows that our approach can be up to an order of magnitude faster than traditional non-compositional symbolic execution. I.