一句话:提出高阶需求驱动程序分析 DDPA,将需求驱动查找扩展到高阶程序,保持流/上下文敏感与多项式复杂度。
针对高阶函数语言难以同时获得精确且高效程序分析的问题,论文提出高阶需求驱动程序分析(DDPA)。该方法将一阶分析中著名的需求驱动查找技术扩展到高阶程序,并针对非局部变量值的按需求值提出新机制。DDPA 具有流敏感和上下文敏感特性,且可证明为多项式时间。为高效实现,作者开发了新的下推自动机元编程框架——Pushdown Reachability 自动机。论文对分析进行了形式化并证明其可靠性,同时描述了实现;摘要未报告具体实验评估结果。
Developing accurate and efficient program analyses for languages with higher-order functions is known to be difficult. Here we define a new higher-order program analysis, Demand-Driven Program Analysis (DDPA), which extends well-known demand-driven lookup techniques found in first-order program analyses to higher-order programs. This task presents several unique challenges to obtain good accuracy, including the need for a new method for demand-driven lookup of non-local variable values. DDPA is flow- and context-sensitive and provably polynomial-time. To efficiently implement DDPA, we develop a novel pushdown automaton metaprogramming framework, the Pushdown Reachability automaton. The analysis is formalized and proved sound, and an implementation is described.
DOI 原文 ·
@article{paperbot708,
title = {Higher-order Demand-driven Program Analysis},
author = {Leandro Facchinetti and Zachary Palmer and Scott Smith},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {41},
number = {3},
year = {2019},
doi = {10.1145/3310340}
}