Learning to Prune Infeasible Paths in Generalized Symbolic Execution

Symbolic execution allows one to systematically explore program paths by executing programs on symbolic inputs, and constructing path conditions that can be analyzed using constraint solving. When programs handle heap-allocated structures, and executions are assumed to begin in states satisfying a property like a precondition or invariant, symbolic execution not only needs to maintain path conditions, but also partially concrete heaps. Partially concrete heaps are increasingly concretized as symbolic execution progresses, and their feasibility (i.e., deciding whether they can be extended to fully concrete structures that satisfy the precondition) needs to be determined, to deem a path realizable and continue execution. This latter task generally requires the manual provision of routines to check the feasibility of partially concrete structures, which are often imprecise (e.g., do not detect all infeasible structures), and increase the cost of symbolic execution. In this paper, we improve the above situation by proposing an automated machine learning technique for determining whether a partially symbolic structure can be extended into a concrete structure satisfying a given invariant. Our approach does not require additional, manually provided routines for checking structure feasibility. It is based on recognizing feasible/infeasible partially symbolic structures by using a neural network, which is trained with automatically generated partially symbolic structures. These structures can be obtained by either symbolically executing the assumed invariant, or by generating and mutating structures using assumed-correct building routines. Our experiments, based on a benchmark of heap-allocated data structures of varying complexities, show that by incorporating our learned symbolic invariants as a pruning mechanism within Symbolic PathFinder, path infeasibility detection is greatly improved, as well as symbolic execution running times.