  Analyzing the behavior of a program running on a processor that supports
speculative execution is crucial for applications such as execution time
estimation and side channel detection. Unfortunately, existing static analysis
techniques based on abstract interpretation do not model speculative execution
since they focus on functional properties of a program while speculative
execution does not change the functionality. To fill the gap, we propose a
method to make abstract interpretation sound under speculative execution. There
are two contributions. First, we introduce the notion of virtual control flow
to augment instructions that may be speculatively executed and thus affect
subsequent instructions. Second, to make the analysis efficient, we propose
optimizations to handle merges and loops and to safely bound the speculative
execution depth. We have implemented and evaluated the proposed method in a
static cache analysis for execution time estimation and side channel detection.
Our experiments show that the new method, while guaranteed to be sound under
speculative execution, outperforms state-of-the-art abstract interpretation
techniques that may be unsound.
