Bound Analysis using Backward Symbolic Execution

A fundamental problem that arises frequently in quantitative program analysis (e.g., resource usage analysis) is that of computing an upper bound for a given arithmetic expression at a given program location in terms of the procedure inputs. We refer to this problem as bound analysis. The problem is theoretically as well as practically challenging because of variable updates inside loops and presence of virtual methods.

Our solution to the bound analysis problem involves an inter-procedural (goal-directed) backward analysis built on top of an SMT solver. The analysis has the advantage of dealing with arbitrary operators that are understood by the underlying SMT solver. The analysis uses novel proof-rule based non-iterative technique to reason about updates inside loops, which makes it quite scalable. It uses user-defined abstract implementations to trace back across virtual methods arising from use of interfaces or extensible types.

We have implemented the analysis inside the SPEED tool, which computes symbolic computational complexity bounds for procedures. Our analysis is used to translate bounds on number of loop iterations and cost of method calls to respective bounds in terms of procedure inputs. We have evaluated the precision and scalability of the analysis over 4 .NET assemblies that together contained thousands of methods and resulted in 9152 queries to the analysis. The analysis was able to answer 90% of the queries on an average of 0.23 seconds per query.