Page 35 - 《软件学报》2024年第6期
P. 35
沈天琪 等: DDoop: 基于差分式 Datalog 求解的增量指针分析框架 2611
为运行时程序地址空间中的内存地址, 即它“指向”了内存中的某个位置 (或对象). 在 Java 这样的面向对象语言中,
指针可以是局部变量或实例字段, 而内存位置通常对应堆对象. 从指针到对象的这种指向关系被称为指针的指向
信息, 指向信息是编译优化和静态程序分析的基础. 指针分析是一种用来静态计算程序中指针 (或引用) 在运行时
的指向信息的上近似的静态程序分析技术. 经过 40 余年的发展, 指针分析已经是一个积累了大量文献 [5,18] 的研究
领域, 但鉴于其基础地位和重要性, 指针分析仍然是静态程序分析学术研究的重点.
在本节我们主要介绍针对 Java 语言的指针分析. 形式化地说, 我们可以将 Java 指针分析视为一个映射集为
pt : (V ∪ H × F) → P(H) , 其中 V 代表待分析程序中的局部变量集合, F 代表待分析程序中的实例字段集合, H 代表
待分析程序中的抽象堆对象集合. 在 Java 程序中, 由于存在循环和递归, 因此在执行过程中可以无限地创建堆对
象. 为了可判定性和可扩展性, 指针分析必须使用堆抽象, 将无限大小的堆划分为有限数量的抽象堆对象. 指针分
析 pt 将一个局部变量 x ∈ V 或一个实例字段 (o i , f) ∈ H × F 映射到一个抽象堆对象集合 s ∈ P(H) , 这个抽象堆对象
集合即指针分析结果, 被称为指针的指向集.
上述形式化定义的 Java 指针分析是上下文不敏感指针分析. 上下文不敏感指针分析的定义和实现相对简单,
并且针对大规模程序的可扩展性更好. 然而上下文不敏感指针分析未对程序中的方法调用上下文进行建模, 在分
(how to do).
析过程中会合并不同过程间动态执行路径上的行为, 导致较大的分析精度损失. 实践证明, 上下文敏感性对于提
高 Java 程序指针分析精度很有用. 上下文敏感指针分析对不同调用上下文下的相同方法和堆对象分别进行分析,
从而区分不同过程间动态执行路径上的行为. 理论上, 调用上下文可以概括为与调用点的控制流相关的程序状态
的某种抽象. 因此, 可以通过使用的不同上下文元素来区分上下文, 得到上下文敏感性的不同变体. 对于 Java 等面
向对象语言, 通常使用 3 种上下文敏感性, 即调用点敏感性、对象敏感性以及类型敏感性, 它们的上下文元素分别
是调用点、抽象堆对象 (分配点) 和类型.
上下文敏感指针分析同样可以形式化定义为一个从指针到指向集的映射. 其与上下文不敏感指针分析的定义
的不同之处在与其中的指针和抽象堆对象都是带上下文限定的. 具体来说, 上下文敏感指针分析是一个映射
cpt : (C ×V ∪ HC × H × F) → P(HC × H) , 其中, C 代表方法上下文, 而 HC 代表堆上下文. 上下文敏感指针分析 cpt
(hc,o i , f) ∈ HC × H × F 映射到一个带上下文限定的抽
会将一个带上下文限定的局部变量 (c, x) ∈ C ×V 或实例字段
象堆对象集合 cs ∈ P(HC × H) , 即上下文敏感指向集.
除上下文敏感性外, 指针分析中还有其他几个影响精度的维度: 流敏感性、字段敏感性、堆模型等. 一般来
说, 某个维度不敏感必然牺牲算法的一部分精度, 而某个维度敏感必然增加算法复杂度, 降低算法实现的效率. 指
针分析当前研究工作面临的主要问题是, 在保证算法精度的同时平衡时间/空间上的消耗, 设计并实现可扩展的、
高精度的指针分析算法.
1.2 Datalog
Datalog 是一种基于逻辑编程的声明式查询语言, 其在语法上是 Prolog 的一个子集. Datalog 被广泛用于处理
结构化数据, 并在数据库管理、人工智能、声明式网络和程序分析等领域中发挥着重要作用. 这些领域使用
Datalog 语言作为查询图和关系结构以及实现迭代和递归的声明式抽象, Datalog 提供了一个声明式接口, 允许程
序员专注于任务 (what to do) 而非低级细节
Datalog 语言的语法非常简洁. 一个 Datalog 程序由一组 Datalog 规则组成, 规则包含规则头和规则体两部分.
规则格式如公式 (1) 所示.
(1)
A :- B 1 , B 2 ,...,B n
其中, A 和 B i 表示 Datalog 中的谓词, A 是这条规则的规则头, 而 B 1 , B 2 ,…, B n 的合取构成规则体. Datalog 的逻辑
基础源自一阶谓词逻辑, 每条规则都是一个蕴含式, 例如公式 (1) 对应的蕴含式为 B 1 ∧ B 2 ∧...∧ B n → A . 一个谓词
可以带有参数, 如 P(e 1 ,e 2 ,...,e k ) 表示一个元谓词. 谓词的实例元组被称为事实.
reachable(X,Y) :- edge(X,Y)
(2)
reachable(X,Y) :- edge(X,Z),reachable(Z,Y)