Galois transformers and modular abstract interpreters: reusable metatheory for program analysis
Galois transformers and modular abstract interpreters: reusable metatheory for program analysis
复制标题
伽罗瓦变换器和模块化抽象解释器：用于程序分析的可重用元理论
DOI：
10.1145/2814270.2814308
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
David Van Horn
中科院分区：
文献类型：
--
作者：
David Darais;M. Might;David Van Horn
静态分析仪的设计和实施已经变得越来越系统。然而，对于给定的语言或分析功能，通常需要乏味和错误的工作来实现分析仪并证明其声音。简而言之，静态分析功能及其音频证明并不能很好地构成，从而使实施和元数据均缺乏重复使用。我们通过引入Galois Transformers：传输Galois连接属性的单一变压器来解决系统构建静态分析仪的问题。我们与一本单调的解释器协同定义了一个单子变压器库，该库为经典分析参数（例如上下文，路径和堆（IN）灵敏度）实现构建块。此外，这些可以与所分析的语言无关。值得注意的是，可以一劳永逸地证明了Galois变压器的声音，这使其成为可重复使用的分析组件。随着新的分析特征和抽象的发展并混合在一起，不必重建声音证明，因为单调变压器堆栈的组成是根据其成分的声音。 Galois变形金刚为可重复使用且可组合的元曲提供了可行的基础，用于程序分析。最后，这些Galois变形金刚将分析设计和实施中的抽象水平转移到非专家可以在许多参数上合成声音分析仪的水平。
The design and implementation of static analyzers has become increasingly systematic. Yet for a given language or analysis feature, it often requires tedious and error prone work to implement an analyzer and prove it sound. In short, static analysis features and their proofs of soundness do not compose well, causing a dearth of reuse in both implementation and metatheory. We solve the problem of systematically constructing static analyzers by introducing Galois transformers: monad transformers that transport Galois connection properties. In concert with a monadic interpreter, we define a library of monad transformers that implement building blocks for classic analysis parameters like context, path, and heap (in)sensitivity. Moreover, these can be composed together independent of the language being analyzed. Significantly, a Galois transformer can be proved sound once and for all, making it a reusable analysis component. As new analysis features and abstractions are developed and mixed in, soundness proofs need not be reconstructed, as the composition of a monad transformer stack is sound by virtue of its constituents. Galois transformers provide a viable foundation for reusable and composable metatheory for program analysis. Finally, these Galois transformers shift the level of abstraction in analysis design and implementation to a level where non-specialists have the ability to synthesize sound analyzers over a number of parameters.