##
Symbolic Simulation on Complicated Loops for WCET Path Analysis

Duc-Hiep Chu and Joxan Jaffar
#### Abstract

We address the Worst-Case Execution Time (WCET) Path Analysis problem for bounded programs,
formalized as discovering a tight upper bound of a resource variable.
A key challenge is posed by complicated loops whose iterations exhibit
non-uniform behavior. We adopt a brute-force strategy by simply unrolling them,
and show how to make this scalable while preserving accuracy.
Our algorithm performs symbolic simulation of the pro- gram. It
maintains accuracy because it preserves, at critical points,
path-sensitivity. In other words, the simulation detects infeasible
paths. Scalability, on the other hand, is dealt with by using
summarizations, compact representations of the analyses of loop
iterations. They are obtained by a judi- cious use of abstraction
which preserves critical information flowing from one iteration to
another. These summariza- tions can be compounded in order for the
simulation to have linear complexity: the symbolic execution can in
fact be asymptotically shorter than a concrete execution. Finally, we
present a comprehensive experimental evaluation using a standard
benchmark suite. We show that our algorithm is fast, and importantly,
we often obtain not just accurate but exact results.