A Symbolic Execution Method for Bounds Analysis
Joxan Jaffar, Andrew Santosa, D.H. Chu and Jorge Navas
Abstract
Given a program whose loops are bounded, we address the problem of
estimating the upper bound of a variable which is monotonically
increasing, and its typical application in annotating a program so
that bounds analysis produces an estimate of the worst-case resource
usage. The method presented is a systematic enumeration of symbolic
states of the program. The novelty is twofold: first, we use {\em
intermittent invariants}, each being a property that is true of some
but not all iterations of a loop. This allows for the discrimination
of analyses of different iterations while still providing an
abstraction so that the analysis can be practical. Second, we compute
the bound estimate by simulating the behavior of the loop using
a {\em dynamic programming} algorithm, relieving us from
discovering a closed form expression for the loop.
The analysis time of a loop, which reasons about {\em
all} inputs, is then proportional to the actual running time of the loop,
on {\em one} input. The method compared formally with prior work,
and evaluated empirically on benchmark programs.