Page 41 - 《软件学报》2024年第6期
P. 41

沈天琪 等: DDoop: 基于差分式     Datalog  求解的增量指针分析框架                                    2617


                 析选项, 我们可能需要准备数千个对应不同情况的                 DDlog  规则文件. 即使这种手动转换可以实现, 但是它会带来
                 巨大的工作量, 并导致规则库代码的严重膨胀. 更糟糕的是, 这种设计将会给后期对这些规则的维护带来巨大的
                 困难.
                    (2) 随着  Doop  框架的流行, 有相当一部分场景性的程序分析算法和新的指针分析算法实际上就是在                          Doop  框
                 架所提供的指针分析规则基础之上开发的. 从兼容性出发, 我们需要尽力支持这种类型的潜在代码. 然而, 如果我
                 们使用的是手动转换, 我们将无法做到这一点. 因               Datalog  引擎切换导致的兼容性破坏的一个例子是              Zipper  [12] ,
                 Zipper 是由  Li 等人提出的一种新的选择性上下文敏感指针分析算法, 在基于                  LogicBlox  引擎的旧版本  Doop  中实
                 现, 目前由于当前版本的       Doop  手动切换到了    Soufflé 引擎, 导致  Zipper 在当前版本的  Doop  中不可用  [21] .
                    面向这两项挑战, 我们设计了一个自动化的               Datalog  规则重写器. 这个自动化规则重写器是我们框架后端的
                 核心, 其设计目标是能够处理         Doop  框架内任何分析选项的组合产生的            Soufflé 指针分析规则. 通过规则重写器,
                 我们可以全自动化地将这些分析规则重写为                DDlog  引擎的格式, 而无需进行繁琐而容易出错的手工转换. 同时,
                 这个自动化重写器也使我们可以对基于              Doop  框架开发的其他分析进行兼容.

                 2.2.1    框架后端架构
                    因此, 我们的重写过程需要在这两种方言之间建立一个映射, 以克服两者之间的语法和拓展差异. 接下来, 我
                    我们框架的后端架构如图          5  所示. 其流程基于    Doop  框架的规则生成部分. 首先, 我们将分析选项输入             Doop
                 框架, 以获得对应的      Soufflé 规则文件. 然后, 这个规则文件会被输入到我们的自动化规则重写器中, 转换为语义等
                 价的  DDlog  规则. 最后, DDlog  工具链会将这些规则编译成支持增量评估的              DDlog  程序, 以响应前端生成的增量
                 输入事实.

                                                     语法结构  规则拓展   模块系统


                                 分析选项                                          增量分析程序
                                                       增量规则重写器




                                  规则库        Soufflé 规则            DDlog 规则    DDlog 编译器
                                                     图 5 框架后端架构

                    如前文所述, Soufflé 和  DDlog  是两种不同的    Datalog  方言, 它们在语法和拓展上都存在一系列的差异. 这些差
                 异主要可以分为      3  类.
                    (1) 第  1  类是语法结构差异. 在   Soufflé 和  DDlog  中很多语言结构的语义是相同的, 但是在具体的语法定义上
                 存在细微差异, 例如类型系统的命名、变量命名规范等. 另外, 在                  Soufflé 还存在一些仅用于辅助编译的注解等.
                    (2) 第  2  类是规则拓展差异. Soufflé 对  Datalog  规则的拓展比  DDlog  更为激进, 例如   Soufflé 规则中引入了析
                 取元素, 并允许输入关系的可变性.
                    (3) 第  3  类是模块系统差异. Soufflé 拥有组件结构, 这是一个相对完善的模块系统, 而              DDlog  中则不存在对应
                 的结构. 正因为有了这个组件系统, Doop         框架可以根据分析选项通过条件编译的方式组装出我们需要的规则.


                 们将分别针对这      3  类差异进行详细的介绍, 并提出相应的解决方案.

                 2.2.2    语法结构重写
                    根据语法结构的语义性质, 我们可以将语法结构的处理方式进一步细分为两种策略: “重写”和“忽略”.
                    “重写”策略主要针对那些在规则层面有实际意义的语法结构, 如类型系统的差异、文法格式的区别, 以及变
                 量命名规范的不同等. 处理这类差异的基本策略是对抽象语法树                      (AST) 的子树进行模式转换. 例如, 参考图         6  中
                 Soufflé 参考代码的第   1  行和  DDlog  参考代码中的第   5  行中的类型定义, 可以发现这两种语言在类型定义上的差
   36   37   38   39   40   41   42   43   44   45   46