使用预言和历史变量的数据流分析
Dataflow Analysis With Prophecy and History Variables
摘要：
利用状态机细化证明的概念，我们使用预言变量，预测未来程序执行的信息，使向后的递归分析的前向推理。从与静态程序分析结果相同的格中提取预言和历史变量（来自程序动态执行的概念），我们要求分析结果同时满足基本程序设计语言的操作语义中的卡诺方程和迁移关系。这种方法消除了显式的抽象和具体化功能，并促进了分析和程序执行之间的更直接的连接，与具体的执行和增强的操作语义的分析结果之间的互模拟关系的形式的连接。我们提出了几个经典的Escherlow分析与这种方法（活变量，非常繁忙的表达式，定义的变量，并达到定义），以及证明，强调这种方法可以实现更精简的推理。据我们所知，我们是第一个使用预言变量进行预测分析的。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
