Compositional Symbolic Execution using Fine-Grained Summaries

Abstract—Compositional symbolic execution has been pro-posed as a way to increase the efficiency of symbolic execution. Essentially, when a function is symbolically executed, a summary of the path that was executed is stored. This summary records the precondition and postcondition of the path, and on subsequent calls that satisfy that precondition, the corresponding postcon-dition can be returned instead of executing the function again. However, using functions as the unit of summarisation leaves the symbolic execution tool at the mercy of a program designer, essentially resulting in an arbitrary summarisation strategy. In this paper, we explore the use of fine-grained summaries, in which blocks within functions are summarised. We propose three types of summarisation and demonstrate how to generate these. At such a fine-grained level, symbolic execution of a path effectively becomes the concatenation of the summaries along that path. Using a prototype symbolic execution tool, we perform a preliminary experimental evaluation of our summary approaches, demonstrating that they can improve the speed of symbolic execution by reducing the number of calls sent to the underlying constraint solver. I