Monadic abstract interpreters
Monadic abstract interpreters
复制标题
一元抽象解释器
DOI：
10.1145/2491956.2491979
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Frank Piessens
中科院分区：
文献类型：
--
作者：
Ilya Sergey;Dominique Devriese;M. Might;Jan Midtgaard;David Darais;D. Clarke;Frank Piessens
抽象解释器系统构建的最新发展暗示了静态分析中概念广泛统一的可能性。我们通过展示上下文敏感性、多变量、流敏感性、可达性修剪、堆克隆和基数限制来实现这种统一，使其独立于任何特定的语义。 Monad 成为这些概念和语义之间的统一媒介。例如，通过将相同的“上下文不敏感单子”插入到 Java 或 lambda 演算的单子参数化语义中，它会产生预期的上下文不敏感分析。为了实现这种统一，我们开发了一种系统方法，用于将具体语义转换为单参数化抽象机。改变 monad 就会改变机器的行为。通过更改 monad，我们恢复了一系列机器——从原始的具体语义到具有单线程堆和弱更新的单变量、流和上下文不敏感的静态分析。一元参数化还建议对静态分析中普遍存在的单调定点计算进行抽象。这种抽象使得使用高级策略（例如抽象垃圾收集和扩展）来进行分析变得更加简单，以提高精度和性能。虽然本文本身运行连续传递风格的开发，但我们的通用实现会针对直接风格的 lambda 演算和 Featherweight Java 重放它以支持通用性。
Recent developments in the systematic construction of abstract interpreters hinted at the possibility of a broad unification of concepts in static analysis. We deliver that unification by showing context-sensitivity, polyvariance, flow-sensitivity, reachability-pruning, heap-cloning and cardinality-bounding to be independent of any particular semantics. Monads become the unifying agent between these concepts and between semantics. For instance, by plugging the same "context-insensitivity monad" into a monadically-parameterized semantics for Java or for the lambda calculus, it yields the expected context-insensitive analysis. To achieve this unification, we develop a systematic method for transforming a concrete semantics into a monadically-parameterized abstract machine. Changing the monad changes the behavior of the machine. By changing the monad, we recover a spectrum of machines---from the original concrete semantics to a monovariant, flow- and context-insensitive static analysis with a singly-threaded heap and weak updates. The monadic parameterization also suggests an abstraction over the ubiquitous monotone fixed-point computation found in static analysis. This abstraction makes it straightforward to instrument an analysis with high-level strategies for improving precision and performance, such as abstract garbage collection and widening. While the paper itself runs the development for continuation-passing style, our generic implementation replays it for direct-style lambda-calculus and Featherweight Java to support generality.