FormaliSE Conference 2023 Conference Paper
Formalizing Path Explosion for Recursive Functions via Asymptotic Path Complexity
- Eli Pregerson
- Shaheen Cullen-Baratloo
- David Chen
- Duy Lam
- Max Szostak
- Lucas Bang
Path coverage is of critical importance in software testing and verification. Furthermore, path explosion is a well-known challenge for automatic software analysis techniques like symbolic execution. Asymptotic Path Complexity (APC) is a code complexity metric that formalizes the quantitative measurement of path explosion and therefore measures the difficulty of achieving path coverage. Prior APC methods were not sufficiently expressive to model the path explosion behavior in recursive functions. Existing analyses simply ignored recursive calls and were unable to correctly compute APC for recursive functions. We present a novel method for computing asymptotic path complexity for recursive functions, which we call APC-R. Our approach is based on the analytic combinatorics of context-free grammars. We implemented our approach on top of the code complexity analysis tool METRINOME and evaluated our implementation on a set of benchmark programs written in the C programming language. Our experiments demonstrate that APC-R is a sound upper bound on the growth rate of the number of program paths explored as a function of increasing exploration depth when generating tests with the KLEE symbolic execution engine. Our APC-R implementation provides sound bounds on KLEE’S symbolic execution path explosion for recursive functions in cases where the original APC implementation did not, and APC-R matches the results of APC for non-recursive functions with only marginal computational overhead. That is, APC-R subsumes earlier APC work without significant performance cost.