Continuation Equivalence: a Correctness Critetion for Static Optimizations of Dynamic Analyses

Dynamic analyses reason about a program’s concrete heap and control flow and hence can report on actual program behavior with high or even perfect accuracy. But many dy-namic analyses require extensive program instrumentation, often slowing down the analyzed program considerably. In the past, researchers have hence developed specialized static optimizations that can prove instrumentation for a special analysis unnecessary at many program locations: the analysis can safely omit monitoring these locations, as their monitoring would not change the analysis results. Arguing about the correctness of such optimizations is hard, however, and ad-hoc approaches have lead to mistakes in the past. In this paper we present a correctness criterion called Continuation Equivalence, which allows researchers to prove static optimizations of dynamic analyses correct more eas-ily. The criterion demands that an optimization may alter instrumentation at a program site only if the altered instru-mentation produces a dynamic analysis configuration equiv-alent to the configuration of the un-altered program with respect to all possible continuations of the control flow. In previous work, we have used a notion of continuation-equivalent states to prove the correctness of static optimiza-tion for finite-state runtime monitors. With this work, we propose to generalize the idea to general dynamic analyses