Alpha | Eiskola

数据流分析

16 min read程序分析原理#程序分析#数据流分析

数据流分析

IMPORTANT

  数据流分析推导数据沿着程序执行路径流动的信息。

分类

分类依据具体分类简要解释
依据语句顺序流敏感分析考虑程序语句的执行顺序
流不敏感分析不考虑语句执行顺序
依据流的方向前向分析从程序入口开始，沿着执行路径向出口方向分析
后向分析从程序出口开始，逆着执行路径向入口方向分析
依据路径的量化信息May (Union) 分析考虑程序所有可能执行的路径
Must (Intersection) 分析考虑程序必然执行的路径
依据对过程的处理过程内分析仅分析单个过程（函数/方法）内部的逻辑
过程间分析分析多个过程间的调用关系

命令式程序语言 WHILE\mathrm{WHILE}

  在保证分析有效性的前提下，为了降低分析复杂度，通常会定义一种简化抽象的语言作为程序分析对象，从而剥离无关细节，避免陷入真实程序设计语言的细节泥潭。这里给出一种简单命令式语言（无过程或高级数据结构）—— WHILE\mathrm{WHILE} 语言。

语法

CategoryDomainMeta variable
NumbersNumbersZ={0,1,−1,… }\mathbb{Z} = \{0, 1, -1, \dots\}zz
TruthTruth valuesvaluesB={true,false}\mathbb{B} = \{\text{true}, \text{false}\}tt
VariablesVariablesVar={x,y,… }\text{Var} = \{x, y, \dots\}xx
ArithmeticArithmetic expressionsexpressionsAExpAExpaa
BooleanBoolean expressionsexpressionsBExpBExpbb
CommandsCommands (statements)(statements)CmdCmdcc
类别语法定义所属集合
Arithmetic expressions (AExpAExp)a::=z∣x∣a1+a2∣a1−a2∣a1∗a2∈AExpa ::= z \mid x \mid a_1+a_2 \mid a_1-a_2 \mid a_1*a_2 \in AExpAExpAExp
Boolean expressions (BExpBExp)b::=t∣a1=a2∣a1>a2∣¬b∣b1∧b2∣b1∨b2∈BExpb ::= t \mid a_1=a_2 \mid a_1>a_2 \mid \neg b \mid b_1\land b_2 \mid b_1\lor b_2 \in BExpBExpBExp
Commands (statements, CmdCmd)c::=skip∣x:=a∣c1;c2∣if b then c1 else c2∣while b do c∈Cmdc ::= \text{skip} \mid x := a \mid c_1;c_2 \mid \text{if}\ b\ \text{then}\ c_1\ \text{else}\ c_2 \mid \text{while}\ b\ \text{do}\ c \in CmdCmdCmd

示例

  下面是一个 WHILE\mathrm{WHILE} 语言示例：

x:=6;y:=7;z:=0;while x>0 dox:=x−1;v:=y;while v>0 dov:=v−1;z:=z+1\begin{align*} & x := 6; \\ & y := 7; \\ & z := 0; \\ & \text{while}\ x > 0\ \text{do} \\ & \quad x := x - 1; \\ & \quad v := y; \\ & \quad \text{while}\ v > 0\ \text{do} \\ & \quad \quad v := v - 1; \\ & \quad \quad z := z + 1 \\ \end{align*}

控制流表示

打标签的程序（Labelled Programs）

IMPORTANT

  为了标注分析信息所附着的位置信息，通常会为程序的每一条可执行语句、控制结构的关键节点（如循环判断、分支判断点）分配唯一的标签（LabelLabel）。

  对于 WHILE\mathrm{WHILE} 语言，数据流信息附着于 skipskip 语句、赋值语句、条件测试语句以及循环语句。即：

a::=z∣x∣a1+a2∣a1−a2∣a1∗a2∈AExpb::=t∣a1=a2∣a1>a2∣¬b∣b1∧b2∣b1∨b2∈BExpc::=[skip]l∣[x:=a]l∣c1;c2∣if [b]l then c1 else c2∣while [b]l do c∈Cmd\begin{align*} & a ::= z \mid x \mid a_1+a_2 \mid a_1-a_2 \mid a_1*a_2 \in AExp \\ & b ::= t \mid a_1=a_2 \mid a_1>a_2 \mid \neg b \mid b_1\land b_2 \mid b_1\lor b_2 \in BExp \\ & c ::= \textcolor{red}{[\text{skip}]^l} \mid \textcolor{red}{[x := a]^l} \mid c_1;c_2 \mid \text{if}\ \textcolor{red}{[b]^l}\ \text{then}\ c_1\ \text{else}\ c_2 \mid \text{while}\ \textcolor{red}{[b]^l}\ \text{do}\ c \in Cmd \end{align*}
TIP

  这里注意 c1;c2c_1;c_2 作为顺序复合语句，不需要标注，因为其中的 c1c_1 和 c2c_2 本身包含标签。

IMPORTANT

  对于程序 cc 中被打标签的片段称为块，记作 BlkcBlk_c。

  对于前面的示例代码，对其标注标签后：

[x:=6]1;[y:=7]2;[z:=0]3;while [x>0]4 do[x:=x−1]5;[v:=y]6;while [v>0]7 do[v:=v−1]8;[z:=z+1]9\begin{align*} & \textcolor{red}{[\text{x} := 6]^1}; \\ & \textcolor{red}{[\text{y} := 7]^2}; \\ & \textcolor{red}{[\text{z} := 0]^3}; \\ & \text{while}\ \textcolor{red}{[\text{x} > 0]^4}\ \text{do} \\ & \quad \textcolor{red}{[\text{x} := \text{x} - 1]^5}; \\ & \quad \textcolor{red}{[\text{v} := \text{y}]^6}; \\ & \quad \text{while}\ \textcolor{red}{[\text{v} > 0]^7}\ \text{do} \\ & \quad \quad \textcolor{red}{[\text{v} := \text{v} - 1]^8}; \\ & \quad \quad \textcolor{red}{[\text{z} := \text{z} + 1]^9} \\ \end{align*}

控制流表示

IMPORTANT

  每个打标签的语句有一个单入口（initial labels\mathrm{initial}\ \mathrm{labels}）和可能的多个出口（final labels\mathrm{final}\ \mathrm{labels}）。

init\mathrm{init} 映射

  对于程序语句存在映射：

init: Cmd→Lab\mathrm{init}:\ Cmd \rightarrow Lab

其中，CmdCmd 表示程序中的语句集合，LabLab 表示标签集合。init\mathrm{init} 映射是一个全函数，即 ∀c∈Cmd, ∃l∈Lab\forall c \in Cmd,\ \exist l \in Lab 使得 init(c)=l\mathrm{init}(c) = l，其中 ll 表示语句 cc 的唯一入口。

  针对 WHILE\mathrm{WHILE} 语言，定义 init\mathrm{init} 映射为：

init([skip]l):=linit([x:=a]l):=linit(c1;c2):=init(c1)init(if [b]l then c1 else c2):=linit(while [b]l do c):=l\begin{align} & \mathrm{init}([\text{skip}]^l) &:= l \\ & \mathrm{init}([x := a]^l) &:= l \\ & \mathrm{init}(c_1; c_2) &:= \textcolor{red}{\mathrm{init}(c_1)} \\ & \mathrm{init}(\text{if}\ [b]^l\ \text{then}\ c_1\ \text{else}\ c_2) &:= l \\ & \mathrm{init}(\text{while}\ [b]^l\ \text{do}\ c) &:= l \\ \end{align}

其中，(3)(3) 表示复合语句应递归地获取该复合语句第一条语句的入口作为整个符合语句的入口。

final\mathrm{final} 映射

  此外，程序语句存在映射：

final: Cmd→2Lab\mathrm{final}:\ Cmd \rightarrow \textcolor{red}{2^{Lab}}
TIP

  这里的 2Lab2^{Lab} 表示 LabLab 标签集合的幂集，其每个元素均为 LabLab 集合的子集，即 ∀l∈2Lab, l⊆Lab\forall l \in 2^{Lab},\ l \subseteq Lab。

其中，CmdCmd 表示程序中的语句集合，LabLab 表示标签集合。final\mathrm{final} 映射同样是一个全函数，∀c∈Cmd,∃l∈2Lab\forall c \in Cmd, \exist l \in 2^{Lab} 使得 final(c)=l\mathrm{final}(c) = l，其中 ll 表示语句 cc 所有可能的出口集合。

  对于 WHILE\mathrm{WHILE} 语言，定义 final\mathrm{final} 映射为：

final([skip]l):={l}final([x:=a]l):={l}final(c1;c2):=final(c2)final(if [b]l then c1 else c2):=final(c1)∪final(c2)final(while [b]l do c):={l}\begin{align} & \mathrm{final}([\text{skip}]^l) &:= \{l\} \\ & \mathrm{final}([x := a]^l) &:= \{l\} \\ & \mathrm{final}(c_1; c_2) &:= \textcolor{red}{\mathrm{final}(c_2)} \\ & \mathrm{final}(\text{if}\ [b]^l\ \text{then}\ c_1\ \text{else}\ c_2) &:= \textcolor{red}{\mathrm{final}(c_1) \cup \mathrm{final}(c_2)} \\ & \mathrm{final}(\text{while}\ [b]^l\ \text{do}\ c) &:= \textcolor{red}{\{l\}} \\ \end{align}

需要注意第 (10)(10) 条，对于循环语句，跳出循环前要判断循环条件 bb 不成立。

（控制）流关系

IMPORTANT

  前面定义了程序语句的位置标签、init\mathrm{init} 与 final\mathrm{final} 映射，于是可以定义程序（控制）流关系：

flow(c)⊆Lab×Lab\mathrm{flow}(c) \subseteq Lab \times Lab

其中，Lab×LabLab \times Lab 即笛卡尔积。对于笛卡尔积 A×BA \times B 有， ∀<a,b>∈A×B\forall <a, b> \in A \times B ，其中 a∈Aa \in A 且 b∈Bb \in B。

  对于 flow(c)\mathrm{flow}(c) ，∀<l,l′>∈flow(c)\forall <l, l^{'}> \in \mathrm{flow}(c) ，则 <l,l′><l, l^{'}> 表示在程序语句 cc 中，存在控制流从位置标签 ll 流向了 l′l^{'}。

  对于 WHILE\mathrm{WHILE} 语言，定义 flow\mathrm{flow} 为：

flow([skip]l):=∅flow([x:=a]l):=∅flow(c1;c2):=flow(c1)∪flow(c2)∪{(l,init(c2))∣l∈final(c1)}flow(if [b]l then c1 else c2):=flow(c1)∪flow(c2)∪{(l,init(c1)),(l,init(c2))}flow(while [b]l do c):=flow(c)∪{(l,init(c))}∪{(l′,l)∣l′∈final(c)}\begin{align} & \mathrm{flow}([\text{skip}]^l) := \emptyset \\ & \mathrm{flow}([x := a]^l) := \emptyset \\ & \mathrm{flow}(c_1; c_2) := \mathrm{flow}(c_1) \cup \mathrm{flow}(c_2) \cup \textcolor{red}{\{ (l, \mathrm{init}(c_2)) \mid l \in \mathrm{final}(c_1) \}} \\ & \mathrm{flow}(\text{if}\ [b]^l\ \text{then}\ c_1\ \text{else}\ c_2) := \mathrm{flow}(c_1) \cup \mathrm{flow}(c_2) \cup \textcolor{red}{\{ (l, \mathrm{init}(c_1)), (l, \mathrm{init}(c_2)) \}} \\ & \mathrm{flow}(\text{while}\ [b]^l\ \text{do}\ c) := \mathrm{flow}(c) \cup \textcolor{red}{\{ (l, \mathrm{init}(c)) \} \cup \{ (l', l) \mid l' \in \mathrm{final}(c) \}} \\ \end{align}
TIP

  关注标红部分，对于顺序复合语句 c1;c2c_1;c_2，需要增加从语句 c1c_1 到 c2c_2 的控制流边；对于条件判断语句 if [b]l then c1 else c2\text{if}\ [b]^l\ \text{then}\ c_1\ \text{else}\ c_2 需要增加由判断条件 [b]l[b]^l 到语句 c1c_1 以及 判断条件 [b]l[b]^l 到语句 c2c_2 的控制流边；对于循环判断语句 while [b]l do c\text{while}\ [b]^l\ \text{do}\ c 则不仅需要添加判断条件 [b]l[b]^l 到语句 cc 的控制流边，还需添加语句 cc 所有可能出口到判断条件 [b]l[b]^l 的控制流边。

示例

c=[z:=1]1;while [x>0]2 do[z:=z∗y]3;[x:=x−1]4\begin{align*} c = &[z := 1]^1; \\ &\text{while}\ [x > 0]^2\ \text{do} \\ &\quad [z := z*y]^3; \\ &\quad [x := x-1]^4 \end{align*}

计算 init\mathrm{init}、final\mathrm{final} 映射以及控制流关系：

init(c)=1final(c)={2}flow(c)={(1,2),(2,3),(3,4),(4,2)}\begin{align*} & \mathrm{init}(c) &= &1 \\ & \mathrm{final}(c) &= &\{2\} \\ & \mathrm{flow}(c) &= &\{(1, 2), (2, 3), (3, 4), (4, 2)\} \\ \end{align*}

从而根据上述信息可以构建控制流图：

控制流图
控制流图
NOTE

  数据流分析本质上都是把程序看成是一个图，分析算法都是基于图表示的。

Related

Comments