【静态分析】静态分析笔记03 - 数据流分析（应用）

参考：

【课程笔记】南大软件分析课程3——数据流分析应用（课时3/4） - 简书

----------------------------------------------------------------------------

1. 数据流分析总览

may analysis: 输出可能正确的信息（需做 over-approximation 优化，才能成为 Safe-approximation 安全的近似，可以有误报)，注意大多数静态分析都是 may analysis
must analysis: 输出必须正确的信息（需做 under-approximation 优化，才能成为 Safe-approximation 安全的近似，可以有漏报）

不同的数据分析应用会有不同的数据抽象方法和不同的流安全近似策略，即不同的转换函数和控制流处理。

Nodes (BBs/statements)、Edges (control flows)、CFG (a program)

例如：

application-specific Data <- abstraction (+/-/0)

Nodes <- Transfer function

Edges <- Control-flow handling

不同的数据流分析有不同的数据抽象表达 和不同的安全近似策略，如不同的 转换规则 和 控制流处理。

2. 预备知识

输入/输出状态：程序执行前/执行后的状态（本质就是抽象表达的数据的状态，如变量的状态）。

每个 IR 块的执行将 input 转换为 output
input 与之前的 output 关联，output 与之后的 input 关联

每个数据流分析的应用中，将每个程序点关联一个数据流值(data-flow value)，这个值代表在那个点能观察到的所有可能的程序状态的抽象。

例如，我只关心x、y的值，我就用抽象来表示x、y所有可能的值的集合（输入/输出的值域/约束），就代表了该程序点的程序状态。

3. Reaching Definitions Analysis

Reaching Definitions Analysis 是一个 may analysis。

问题定义：给变量 v 一个定义 d（赋值），存在一条路径使得程序点 p 能够到达 q，且在这个过程中不能改变 v 的定义 d。

抽象表示：设程序有 n 条赋值语句，用 n 位向量来表示变量 v 的定义 d 能 reach 与不能 reach。

（1）公式分析

什么是definition？

D: v = x op y，op为operation，如 x + y。

Transfer Function：

解释：基本块 B 的输出 = 块 B 内的所有变量 v 的定义（赋值/修改）语句并上（块 B 的输入 - 整个程序中其它所有变量 v 的定义）。

Control Flow：

解释：基本块 B 的输入 = 块 B 所有前驱块 P 的输出的并集。注意，所有前驱块意味着只要有一条路径能够到达块B，就是它的前驱，包括条件跳转与无条件跳转。

（2）算法

目的：输入 CFG，计算好每个基本块的 killB 和 genB，输出每个基本块最终的 IN[B] 和 OUT[B]。

方法：

（3）实例

抽象表示：设程序有 n 条赋值语句，用 n 位向量来表示变量 v 的定义 d 能 reach 与不能 reach。

说明：红色-第1次遍历；蓝色-第2次遍历；绿色-第3次遍历。

结果：3次遍历之后，每个基本块的 OUT[B] 都不再变化。

最后得到了，每个程序点关联的数据流值（该点所有可能的程序状态的一个抽象表示，也就是这个 n 位向量）。

（4）算法会停止吗？

会。

genS 和 killS 是不变的，只有 IN[S] 在变化，而 IN[S] 只会在原来的基础上越来越大（与more facts 并集），所以 OUT[S] 只会越来越大，直到达到一个上限。

所以最终 changes to any OUT 不会再发生变化，算法就停止了。