Abstract

This paper describes an inter-procedural technique for computing symbolic complexity bounds of programs in terms of their scalar inputs and user-defined quantitative attributes of input data-structures. One key challenge in this process is to compute bounds on number of loop iterations and recursive invocations of any recursive procedure, and then compose these in an inter-procedural bottom-up manner to obtain precise complexity bounds for any program. To do this, our technique instruments loops and recursive procedures with several counters and uses an abstract interpreter to infer invariants on those counters, followed by extracting bounds information from these invariants. In addition, we introduce techniques that allow a simple abstract interpreter over a linear arithmetic domain to compute precise non-linear bounds. The other key challenge is to compute, or even express, bounds in presence of recursive data-structures. To address this, we introduce the notion of user-defined base quantitative parameters for recursive data structures, and show how to perform abstract interpretation to compute invariants relating instrumented counter variables with such quantitative parameters. We also show how to generalize our algorithm for computing complexity bounds to computing general resource usage bounds. We present experimental numbers that demonstrate the feasibility of our technique for computing complexity bounds for a variety of example programs, including some from the C++ Standard Template Library (STL).