《基于格理论的数据流分析.ppt》由会员分享，可在线阅读，更多相关《基于格理论的数据流分析.ppt（49页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、高级软件工程高级软件工程第十讲第十讲基于格理论的数据流分析基于格理论的数据流分析基于格理论的数据流分析基于格理论的数据流分析 2/49高级软件工程高级软件工程内内 容容一、控制流图一、控制流图二、活性分析二、活性分析三、可用表达式三、可用表达式 四、很忙表达式四、很忙表达式五、可达定义五、可达定义六、初始化变量六、初始化变量七、符号分析七、符号分析八、常量分析八、常量分析九、区间分析九、区间分析2基于格理论的数据流分析基于格理论的数据流分析 3/49高级软件工程高级软件工程一、控制流图一、控制流图（Control Flow Graph：CFG）类型分析主要通过语法树进行是流不敏感的(flow
2、insensitive)S1;S2 的分析结果与 S2;S1 的结果相同深入的分析是流敏感的(flow sensitive)需要结束控制流图3基于格理论的数据流分析基于格理论的数据流分析 4/49高级软件工程高级软件工程一个控制流图是一个有向图一个控制流图是一个有向图结点对应于程序中的点（语句）结点对应于程序中的点（语句）边对应与可能的控制流边对应与可能的控制流一个一个 CFG 有单个的入口和单个的出口有单个的入口和单个的出口如果如果 v 是是 一个一个CFG中中 的一个点，则：的一个点，则：pred(v)是指该点直接前面点的集合是指该点直接前面点的集合 succ(v)是指该点直接后面点的集合
3、是指该点直接后面点的集合4基于格理论的数据流分析基于格理论的数据流分析 5/49高级软件工程高级软件工程数据流分析与格传统的数据流分析传统的数据流分析(我们要讨论的内容我们要讨论的内容)从一个从一个 CFG 和一个具有有限高度的格和一个具有有限高度的格 L 开始开始对于对于 CFG 中的每个点中的每个点 v,我们赋予一个变量我们赋予一个变量 v，其取值范，其取值范围围 是是 L 中的元素中的元素.对于编程语言中的每个构造块，对于编程语言中的每个构造块，我们定义一个数据流约束（我们定义一个数据流约束（dataflow constraint）该约束反映了一个点与其它点该约束反映了一个点与其它点(特
4、别是邻居特别是邻居)之间值的关之间值的关系系5基于格理论的数据流分析基于格理论的数据流分析 6/49高级软件工程高级软件工程对于一个CFG，我们可以抽取变量的约束的集合如果所有的约束刚好是等式或者不等式（右边单调）我们就可以利用不动点算法求唯一的最小解如果所有的解对应于程序的正确信息，则数据流约束是“确定的”（sound）因为解可能或多或少地不精确，所以分析是“保守”的(conservative)但计算最小解将获得最大的精确度6基于格理论的数据流分析基于格理论的数据流分析 7/49高级软件工程高级软件工程不动点算法如果一个 CFG 具有点 V=v1,v2,.,vn,我们可以这样构造格Ln假定点
5、 vi 产生数据流等式产生数据流等式vi=Fi(v1,.,vn)我们构造联合函数 F:Ln LnF(x1,.,xn)=(F1(x1,.,xn),.,Fn(x1,.,xn)7基于格理论的数据流分析基于格理论的数据流分析 8/49高级软件工程高级软件工程 x=(,.,);do t=x;x=F(x);while(x t);计算不动点计算不动点 x 的直观算法的直观算法:x1=;.;xn=;do t1=x1;.;tn=xn;x1=F1(x1,.,xn);.xn=Fn(x1,.,xn);while(x1 t1 .xn tn);每个语句未利用每个语句未利用以前语句的结果以前语句的结果X1:第第i个结点结束
6、时个结点结束时 的值集合的值集合迭代时重复计算量大迭代时重复计算量大许多等式已经不变！许多等式已经不变！改进改进:利用以前语句的结果利用以前语句的结果8基于格理论的数据流分析基于格理论的数据流分析 9/49高级软件工程高级软件工程 x1=;.;xn=;q=v1,.,vn;while(q )assume q=vi,.;y=Fi(x1,.,xn);q=q.tail();if(y xi)for(v dep(vi)q.append(v);xi=y;实际使用的算法实际使用的算法:dep(vi)是被是被Vi影响的点的集合影响的点的集合9基于格理论的数据流分析基于格理论的数据流分析 10/49高级软件工程高
7、级软件工程二、活性（Liveness）分析一个变量在程序的某个点是活跃的，如果：它的当前值在后面程序执行时可能被读取我们的分析借助于一个幂集格(powerset lattice)其元素是程序中的变量10基于格理论的数据流分析基于格理论的数据流分析 11/49高级软件工程高级软件工程var x,y,z;x=input;while(x1)y=x/2;if(y3)x=x-y;z=x-4;if(z0)x=x/2;z=z-1;output x;考虑如下的程序考虑如下的程序:构造格:L=(2x,y,z,)Whats the meaning?x,y,zx,y x,z y,zx y z11基于格理论的数据流分
8、析基于格理论的数据流分析 12/49高级软件工程高级软件工程对任何一个对任何一个CFG 结点结点 v，我们引入一个约束变量，我们引入一个约束变量 v v 代表在该结点前活跃的程序变量集代表在该结点前活跃的程序变量集我们引入一个辅助定义我们引入一个辅助定义:JOIN(v)=w wsucc(v)对于退出结点，约束为：对于退出结点，约束为：exit=对对“条件条件”和和“输出输出”语句，约束为语句，约束为:v=JOIN(v)vars(E)对于赋值语句，约束为对于赋值语句，约束为:v=JOIN(v)id vars(E)对于变量声明，约束为对于变量声明，约束为:v=JOIN(v)id1,.,idn最后，
9、对所有其它结点，约束为最后，对所有其它结点，约束为:v=JOIN(v)其中：其中：vars(E)表示出现在表示出现在 E 中的变量中的变量 “”表示减去：原来的值不再起作用表示减去：原来的值不再起作用这些约束明显是单调的（这些约束明显是单调的（为什么？为什么？）F(x1,.,xn)12基于格理论的数据流分析基于格理论的数据流分析 13/49高级软件工程高级软件工程var x,y,z;=x=input x,y,zx=input=x1 xx1=(y=x/2 output x)xy=x/2=(y3 y)xy3=x=x-y z=x-4 yx=x-y=(z=x-4 x)x,yz=x-4=(z0 z)xz
10、0=x=x/2 z=z-1 zx=x/2=(z=z-1 x)xz=z-1=(x1 z)zoutput x=exit xexit=var x,y,z;x=input;while(x1)y=x/2;if(y3)x=x-y;z=x-4;if(z0)x=x/2;z=z-1;output x;Program Constraints13基于格理论的数据流分析基于格理论的数据流分析 14/49高级软件工程高级软件工程var x,y,z;=x=input x,y,zx=input=x1 xx1=(y=x/2 output x)xy=x/2=(y3 y)xy3=x=x-y z=x-4 yx=x-y=(z=x-4
11、 x)x,yz=x-4=(z0 z)xz0=x=x/2 z=z-1 zx=x/2=(z=z-1 x)xz=z-1=(x1 z)zoutput x=exit xexit=Constraintsentry=var x,y,z;=x=input=x1=xy=x/2=xy3=x,yx=x-y=x,yz=x-4=xz0=x,zx=x/2=x,zz=z-1=zoutput x=xexit=entry=var x,y,z;=x=input=x1=y=x/2=y3=x=x-y=z=x-4=z0=x=x/2=z=z-1=output x=exit=第一次迭代结果第一次迭代结果14基于格理论的数据流分析基于格理论
12、的数据流分析 15/49高级软件工程高级软件工程entry=var x,y,z;=x=input=x1=xy=x/2=xy3=x,yx=x-y=x,yz=x-4=xz0=x,zx=x/2=x,zz=z-1=x,zoutput x=xexit=entry=var x,y,z;=x=input=x1=xy=x/2=xy3=x,yx=x-y=x,yz=x-4=xz0=x,zx=x/2=x,zz=z-1=zoutput x=xexit=第一次迭代结果第一次迭代结果var x,y,z;=x=input x,y,zx=input=x1 xx1=(y=x/2 output x)xy=x/2=(y3 y)xy
13、3=x=x-y z=x-4 yx=x-y=(z=x-4 x)x,yz=x-4=(z0 z)xz0=x=x/2 z=z-1 zx=x/2=(z=z-1 x)xz=z-1=(x1 z)zoutput x=exit xexit=Constraints第二次迭代结果第二次迭代结果15基于格理论的数据流分析基于格理论的数据流分析 16/49高级软件工程高级软件工程entry=var x,y,z;=x=input=x1=xy=x/2=xy3=x,yx=x-y=x,yz=x-4=xz0=x,zx=x/2=x,zz=z-1=x,zoutput x=xexit=entry=var x,y,z;=x=input=
14、x1=xy=x/2=xy3=x,yx=x-y=x,yz=x-4=xz0=x,zx=x/2=x,zz=z-1=x,zoutput x=xexit=第二次迭代结果第二次迭代结果var x,y,z;=x=input x,y,zx=input=x1 xx1=(y=x/2 output x)xy=x/2=(y3 y)xy3=x=x-y z=x-4 yx=x-y=(z=x-4 x)x,yz=x-4=(z0 z)xz0=x=x/2 z=z-1 zx=x/2=(z=z-1 x)xz=z-1=(x1 z)zoutput x=exit xexit=Constraints第三次迭代结果第三次迭代结果16基于格理论的
15、数据流分析基于格理论的数据流分析 17/49高级软件工程高级软件工程从该信息，一个聪明的编译器可以发现从该信息，一个聪明的编译器可以发现 y 和和 z 从来没有同时活跃，从来没有同时活跃，z=z-1 中的赋值从未被用过。中的赋值从未被用过。因此，该程序可以被优化：因此，该程序可以被优化：var x,y,z;x=input;while(x1)y=x/2;if(y3)x=x-y;z=x-4;if(z0)x=x/2;z=z-1;output x;节省了一个赋值语句！节省了一个赋值语句！寄存器分配更合理！寄存器分配更合理！var x,yz;x=input;while(x1)yz=x/2;if(yz3)
16、x=x-yz;yz=x-4;if(yz0)x=x/2;output x;冗余赋值！17基于格理论的数据流分析基于格理论的数据流分析 18/49高级软件工程高级软件工程三、可用表达式（Available expression）一个重要的表达式是可用的，如果 它的当前值已经计算过对应的幂集格，元素是程序中出现过的所有表达式 比较关系是反的（“以前”：从上到下）程序例子：var x,y,z,a,b;z=a+b;y=a*b;while(y a+b)a=a+1;x=a+b;18基于格理论的数据流分析基于格理论的数据流分析 19/49高级软件工程高级软件工程其中含 4 个表达式，对应的格为：L=(2a+b
17、,a*b,ya+b,a+1,)重要表达式19基于格理论的数据流分析基于格理论的数据流分析 20/49高级软件工程高级软件工程定义定义:JOIN(v)=w wpred(v)对于入口，约束为：对于入口，约束为：entry=如果如果 v 包含一个条件表达式包含一个条件表达式 E,约束为：约束为：v=JOIN(v)exps(E)如果如果 v 包含输出语句包含输出语句 E,约束为：约束为：v=JOIN(v)exps(E)如果如果 v 包含赋值语句包含赋值语句 id=E,约束为约束为:v=(JOIN(v)exps(E)id id 表示移除所有包含指向变量表示移除所有包含指向变量 id 的表达式的表达式对所
18、有其它结点，约束为：对所有其它结点，约束为：v=JOIN(v)20基于格理论的数据流分析基于格理论的数据流分析 21/49高级软件工程高级软件工程函数 exps 定义为:exps(intconst)=exps(id)=exps(input)=exps(E1opE2)=E1 op E2 exps(E1)exps(E2)op 是任何二元操作符 entry=var x,y,z,a,b;=entry z=a+b=exps(a+b)zy=a*b=(x=a+b exps(a*b)yya+b=(y=a*b x=a+b)exps(ya+b)a=a+1=(ya+b exps(a+1)ax=a+b=(a=a+1
19、exps(a+b)xexit=ya+b对于前面的例子程序，约束为：对于前面的例子程序，约束为：var x,y,z,a,b;z=a+b;y=a*b;while(y a+b)a=a+1;x=a+b;21基于格理论的数据流分析基于格理论的数据流分析 22/49高级软件工程高级软件工程运用不动点算法，可以得到：which confirms our assumptions about a+b.entry=var x,y,z,a,b;=z=a+b=a+by=a*b=a+b,a*bya+b=a+b,a*b,ya+ba=a+1=x=a+b=a+bexit=a+b22基于格理论的数据流分析基于格理论的数据流分析
20、 23/49高级软件工程高级软件工程优化程序：var x,y,z,a,b;z=a+b;y=a*b;while(y a+b)a=a+1;x=a+b;var x,y,z,a,b,aplusb;aplusb=a+b;z=aplusb;y=a*b;while(y aplusb)a=a+1;aplusb=a+b;x=aplusb;23基于格理论的数据流分析基于格理论的数据流分析 24/49高级软件工程高级软件工程四、很忙表达式(Very Busy Expression)一个表达式一个表达式“很忙很忙”，如果：，如果：它的值改变之前被再次计算它的值改变之前被再次计算定义的格与定义的格与“可用表达式可用表达
21、式”相同。相同。对于图中的点对于图中的点 v，v 表示那些在该点前忙的表达式表示那些在该点前忙的表达式24基于格理论的数据流分析基于格理论的数据流分析 25/49高级软件工程高级软件工程定义：定义：JOIN(v)=w wsucc(v)出口点的约束为出口点的约束为:exit=条件与输出语句的约束为：条件与输出语句的约束为：v=JOIN(v)exps(E)赋值语句的约束为：赋值语句的约束为：v=JOIN(v)id exps(E)其它语句的约束为其它语句的约束为:v=JOIN(v)25基于格理论的数据流分析基于格理论的数据流分析 26/49高级软件工程高级软件工程var x,a,b;x=input;
22、a=x-1;b=x-2;while(x0)output a*b-x;x=x-1;output a*b;var x,a,b,atimesb;x=input;a=x-1;b=x-2;atimesb=a*b;while(x0)output atimesb-x;x=x-1;output atimesb;例子：例子：分析揭示：分析揭示：a*b 在循环中很忙在循环中很忙26基于格理论的数据流分析基于格理论的数据流分析 27/49高级软件工程高级软件工程五、到达定义（Reaching Definitions）给定一个程序点，“到达定义”是可能定义了当前变量值的那些赋值语句需要的幂集格中，元素是所有的赋值语句
23、27基于格理论的数据流分析基于格理论的数据流分析 28/49高级软件工程高级软件工程对应的格:L=(2x=input,y=x/2,x=x-y,z=x-4,x=x/2,z=z-1,)例子：例子：var x,y,z;x=input;while(x1)y=x/2;if(y3)x=x-y;z=x-4;if(z0)x=x/2;z=z-1;output x;28基于格理论的数据流分析基于格理论的数据流分析 29/49高级软件工程高级软件工程定义：定义：JOIN(v)=w wpred(v)对于赋值语句，约束为对于赋值语句，约束为:v=JOIN(v)id v其它语句的约束为其它语句的约束为:v=JOIN(v)
24、其中，其中，id 移除所有给变量移除所有给变量 id 的赋值的赋值.可以用来构造变量的定义可以用来构造变量的定义-使用图使用图(CFG的子图的子图)用来进一步分析用来进一步分析 dead code,code moion29基于格理论的数据流分析基于格理论的数据流分析 30/49高级软件工程高级软件工程var x,y,z;x=input;while(x1)y=x/2;if(y3)x=x-y;z=x-4;if(z0)x=x/2;z=z-1;output x;定义-使用图30基于格理论的数据流分析基于格理论的数据流分析 31/49高级软件工程高级软件工程对四类经典分析的总结前向后向 可能 可达定义可
25、达定义活性活性一定可用表达式可用表达式很忙表达式很忙表达式31基于格理论的数据流分析基于格理论的数据流分析 32/49高级软件工程高级软件工程l正向分析 对每个程序点，计算过去的行为信息可用表达式可用表达式可达定义可达定义l反向分析 对每个程序点，计算将来的行为信息活性活性很忙表达式很忙表达式前向与后向32基于格理论的数据流分析基于格理论的数据流分析 33/49高级软件工程高级软件工程可能与必须l可能分析 描述可能为真的信息：计算上限近似活性活性可达定义可达定义l必须分析 描述一定为真的信息：计算下限近似可用表达式很忙表示式33基于格理论的数据流分析基于格理论的数据流分析 34/49高级软件工
26、程高级软件工程六、初始化变量(Initialized Variables)l对于每个程序点，保证已初始化的变量集合l格是程序中变量的集合l初始化是过去的属性，需要用正向分析l是“必须”34基于格理论的数据流分析基于格理论的数据流分析 35/49高级软件工程高级软件工程在入口点的约束为：entry=辅值语句的约束为：v=w id wpred(v)其它语句的约束为：v=w wpred(v)对于每一个变量的使用，检查是否在“已初始化”的集合中35基于格理论的数据流分析基于格理论的数据流分析 36/49高级软件工程高级软件工程七、符号分析（Sign Analysis）l如何决定各个表达式的符号(+,0
27、,-)?可以解决的例子：是否除数是可以解决的例子：是否除数是0l构造符号格:?+0 其中:?表示符号值不是常量（已知道）表示值未知The full lattice for our analysis is the map lattice:Vars|Signwhere Vars is the set of variables occurring in the given program.36基于格理论的数据流分析基于格理论的数据流分析 37/49高级软件工程高级软件工程对每一个对每一个 CFG 结点结点 v，令，令 v 代表在该点所有变量的符号（代表在该点所有变量的符号（-,0,+）对于变量声明，
28、我们引入常数映射，并返回对于变量声明，我们引入常数映射，并返回?:v=id1|?,.,idn|?对于赋值语句，约束为：对于赋值语句，约束为：v=JOIN(v)id|eval(JOIN(v),E)其它语句约束为：其它语句约束为：v=JOIN(v)其中：其中：JOIN(v)=w wpred(v)eval 对表达式进行抽象估计对表达式进行抽象估计:eval(,id)=(id)eval(,intconst)=sign(intconst)eval(,E1 op E2)=opp(eval(,E1),eval(,E2)其中，其中，sign 给出整数的符号给出整数的符号opp 给出一个操作的抽象估计（见下页）
29、给出一个操作的抽象估计（见下页）37基于格理论的数据流分析基于格理论的数据流分析 38/49高级软件工程高级软件工程不同操作符的抽象估计不同操作符的抽象估计38基于格理论的数据流分析基于格理论的数据流分析 39/49高级软件工程高级软件工程有时候还可以提高精度例如，表达式(20)=1 的分析结果是?+/+的分析结果是?而不是+，因为 1/2 被归到 0 中我们可以在格中引入新元素 1,+0,以及-0 以获得精确的抽象值这样，抽象表需要是 8 8?+0 -0 +0 -139基于格理论的数据流分析基于格理论的数据流分析 40/49高级软件工程高级软件工程八、常量传播（Constant Propag
30、ation）在任何一个程序点，计算变量的值是否是确定的分析过程与符号分析类似，基本格换为:?-3 -2 -1 0 1 2 3 操作符的抽象方式：操作符的抽象方式：以加法为例：以加法为例：n m.if(n?m?)n+m else?40基于格理论的数据流分析基于格理论的数据流分析 41/49高级软件工程高级软件工程var x,y,z;x=27;y=input;z=2*x+y;if(x 0)y=z-3;else y=12;output y;分析例子分析例子:var x,y,z;x=27;y=input;z=54+y;if(0)y=z-3;else y=12;output y;var y;y=inpu
31、t;output 12;41基于格理论的数据流分析基于格理论的数据流分析 42/49高级软件工程高级软件工程区间分析为整数变量分析取值范围：下限和上限格描述单个变量的取值范围：Interval=lift(l,h|l,h N l h)其中:N=,.,2,1,0,1,2,.,是含无限点的整数集合，区间顺序定义为：l1,h1 l2,h2 l2 l1 h1 h2全部是闭区间九、区间分析（Interval Analysis）42基于格理论的数据流分析基于格理论的数据流分析 43/49高级软件工程高级软件工程对应的格：对应的格：很明显，这是一个高度无限的格很明显，这是一个高度无限的格43基于格理论的数据流
32、分析基于格理论的数据流分析 44/49高级软件工程高级软件工程对于入口结点，应用常量函数（返回）：entry=x.,对于赋值语句，约束为：v=JOIN(v)id|eval(JOIN(v),E)其它语句的约束为：v=JOIN(v)其中:JOIN(v)=w wpred(v)44基于格理论的数据流分析基于格理论的数据流分析 45/49高级软件工程高级软件工程eval 进行表达式的抽象估计：eval(,id)=(id)eval(,intconst)=intconst,intconsteval(,E1 opE2)=opp(eval(,E1),eval(,E2)抽象算术操作定位为：opp(l1,h1,l2
33、,h2)=抽象比较操作定位为：opp(l1,h1,l2,h2)=0,145基于格理论的数据流分析基于格理论的数据流分析 46/49高级软件工程高级软件工程格的高度无限，因此不能用单调框架格的高度无限，因此不能用单调框架(算法可能不终止算法可能不终止)应用应用“加宽加宽”（widening）技术：）技术：引入函数引入函数 w:Ln Ln 使得使得:(F w)i(,.,)收敛在一个不动点上收敛在一个不动点上从而给出一个关于程序的确定信息从而给出一个关于程序的确定信息w将区间映射到一个有限子集将区间映射到一个有限子集“B”:B N，且包含，且包含 与与 典型地，典型地，B 的初值是出现在给定程序的所
34、有整数常数的初值是出现在给定程序的所有整数常数也可以使用一些启发式方法也可以使用一些启发式方法对于一个单个区间：对于一个单个区间：w(l,h)=maxi B|i l,mini B|h i如何如何“加宽加宽”？46基于格理论的数据流分析基于格理论的数据流分析 47/49高级软件工程高级软件工程“加宽加宽”（Widening）用于解决）用于解决“无限无限”的问题的问题“收缩收缩”（narrowing）用于改进结果）用于改进结果定义定义:fix=Fi(,.,)fixw=(F w)i(,.,)则：则：fix fixw不仅如此：不仅如此：fix F(fixw)fixw对对 F 的应用可以精化结果，且仍然
35、是的应用可以精化结果，且仍然是“确定的确定的”(sound)该技术被成为该技术被成为“收缩收缩”技术，且可以被迭代使用技术，且可以被迭代使用fix Fi+1(fixw)Fi(fixw)fixw47基于格理论的数据流分析基于格理论的数据流分析 48/49高级软件工程高级软件工程y=0;while(input)x=7;x=x+1;y=y+1;如果没有如果没有“加宽加宽”,下面的分析将是发散下面的分析将是发散的的:x|,y|x|8,8,y|0,1x|8,8,y|0,2x|8,8,y|0,3.应用应用“加宽加宽”,构造集合构造集合 B=,0,1,7,可以得到收敛结果：可以得到收敛结果：x|,y|x|7,y|0,1x|7,y|0,7x|7,y|0,48基于格理论的数据流分析基于格理论的数据流分析 49/49高级软件工程高级软件工程但对但对 x 的结果不好的结果不好应用应用“收缩收缩”，可以得到，可以得到:x|8,8,y|0,注意注意:fixw F(fixw)F2(fixw)F3(fixw).不保证收敛不保证收敛必须应用启发方法决定必须应用启发方法决定“收缩收缩”多少次多少次x|,y|x|7,y|0,1x|7,y|0,7x|7,y|0,49