Precise Lazy Initialization for Programs with Complex Heap Inputs
Juan Manuel Copia, Facundo Molina, Nazareno Aguirre, Marcelo Fabian Frias, Alessandra Gorla, Pablo Ponzio · 2023
Lazy initialization enables symbolic execution for programs with heap-allocated inputs. It starts the program execution with a symbolic heap and concretizes it on demand as the program accesses it. However, the main challenge of lazy initialization is efficiently determining whether the current symbolic heap becomes infeasible with respect to the program’s precondition. Pruning infeasible heaps is crucial to avoid significant runtime overhead and false alarms.In this paper, we propose PLI (Precise Lazy Initialization), an approach that precisely decides whether there exists a concretization of the current symbolic heap that satisfies the program’s precondition. Unlike previous approaches, PLI also takes into account the constraints in the path condition to determine the feasibility of the current symbolic heap. Furthermore, PLI allows preconditions to be specified as standard operational predicates for concrete structures, eliminating the need for additional specifications tailored to symbolic heaps.In our empirical evaluation, PLI demonstrated comparable performance to existing lazy approaches while reducing the number of explored paths by 43% (all infeasible) and eliminating all false alarms in the analysis. Moreover, PLI exhibited faster execution and better scalability compared to "eager" (enumeration-based) approaches, achieving a 67% reduction in explored paths.