Data Flow Analysis

Overview of Data Flow Analysis

• may analysis: outputs information that may be true(over-approximation) 可能正确，超出近似over-approximation
• must analysis: outputs information that must be true (under-approximation) 必须正确，under-approximation

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

Preliminaries of Data Flow Analysis

输入和输出状态：

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

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

这个应用中抽象出的所有值称为domain。

数据流分析是为所有语句s的IN和OUT找到一组近似安全的在约束规则下的解。

约束规则则是基于语句的语义即转移函数；约束规则基于控制流

• 前向分析
• 逆向分析

• 汇合运算符用于在不同路径的汇合处汇总来自不同路径的贡献。

Reaching Definitions Analysis

可达性：从p点上到定义d到q点是否可达条件如下：

• CFG中可达，存在路径
• 在这条路径上中间不能kill，即不能出现新的定义d

在控制流图（CFG）的入口处为每个变量v引入一个虚拟定义（dummy definition），如果v的虚拟定义在某个点p处到达，并且v在该点p被使用，那么v可能在定义之前被使用（因为未定义的值到达了v）。

这句话在讨论静态程序分析的概念，其中CFG是一种表示程序控制流的图形结构。变量v在CFG的入口处被引入一个虚拟定义，表示变量v的初始值或默认值。当控制流到达某个点p时，如果该点p之前的某个虚拟定义到达了变量v，那么变量v可能在该点p之前被使用，因为此时v可能具有未定义的值。

这个概念强调了在静态程序分析中，对于变量使用的分析需要考虑变量的定义情况，特别是在复杂的控制流结构中，确保变量在使用之前已经得到了正确的定义，以避免潜在的错误或未定义行为。

属于may analysis， 需要查全

用bit做abstraction

transfer函数以及control flow对constrain公式如下：

算法如下：

example:

B3: 0011 0110意思是，第3和第4，第5和第6个点可以到达B3这个基本块
 

为什么这个算法会停：

为什么用这个condition