Dataflow Analysis With Prophecy and History Variables

TL;DR

This paper introduces a novel approach to dataflow analysis using prophecy and history variables, inspired by state machine refinement, to enable more direct and streamlined reasoning about program behaviors.

Contribution

It is the first to apply prophecy variables to dataflow analysis, connecting static analysis results directly with program semantics without explicit abstraction functions.

Findings

Successfully applied to classical dataflow analyses like live variables and reaching definitions

Provides proofs demonstrating more streamlined reasoning processes

Eliminates the need for explicit abstraction and concretization functions

Abstract

Leveraging concepts from state machine refinement proofs, we use prophecy variables, which predict information about the future program execution, to enable forward reasoning for backward dataflow analyses. Drawing prophecy and history variables (concepts from the dynamic execution of the program) from the same lattice as the static program analysis results, we require the analysis results to satisfy both the dataflow equations and the transition relations in the operational semantics of underlying programming language. This approach eliminates explicit abstraction and concretization functions and promotes a more direct connection between the analysis and program executions, with the connection taking the form of a bisimulation relation between concrete executions and an augmented operational semantics over the analysis results. We present several classical dataflow analyses with this approach (live variables, very busy expressions, defined variables, and reaching definitions) along with proofs that highlight how this approach can enable more streamlined reasoning. To the best of our knowledge, we are the first to use prophecy variables for dataflow analysis.