Path-optimal symbolic execution of heap-manipulating programs
Pietro Braione, Giovanni Denaro, Luca Guglielmo
TL;DR
This work tackles path explosion in symbolic execution for heap-manipulating programs by introducing POSE, a path-optimal symbolic execution algorithm that forks traces only at actual decision points. POSE encodes heap aliasing and distinctness with comprehensive ITE-based symbolic values, avoiding unnecessary trace forking and achieving a near-linear correspondence between traces and program paths. The authors formalize POSE for a small object-oriented language, implement a Java-bytecode prototype, and compare it to traditional lazy initialization on a SBST-derived benchmark, showing orders-of-magnitude reductions in traces and substantial improvements in constraint solving and test-generation efficiency. The results suggest that path-optimal symbolic execution can meaningfully improve the scalability and practicality of symbolic analysis for heap-oriented software, with future work aimed at integrating POSE with state-merging techniques for even greater efficiency.
Abstract
Symbolic execution is at the core of many techniques for program analysis and test generation. Traditional symbolic execution of programs with numeric inputs enjoys the property of forking as many analysis traces as the number of analyzed program paths, a property that in this paper we refer to as path optimality. On the contrary, current approaches for symbolic execution of heap-manipulating programs fail to satisfy this property, thereby incurring crucial path explosion effects. This paper introduces POSE, path-optimal symbolic execution, a symbolic execution algorithm that originally achieves path optimality against heap-manipulating programs. We formalize the POSE algorithm and experiment it against a benchmark of programs that take data structures as inputs, supporting the potential of POSE for improving on the state of the art of symbolic execution of heap-manipulating programs.