大学数据流分析课件

第2章数据流分析数据流分析的用途编译优化、程序维护程序安全性的检查和编译原理课程的区别基于源代码的结构化分析方法，而不是基于基本块和程序流图的分析从过程内讨论到过程间强调理论基础/sundae_meng第2章数据流分析数据流分析的用途http://www.d1第2章数据流分析数据流分析的正确性数据流分析所得结论同程序运行时的情况一致需要定义机器模型和操作语义，证明所得结论对操作语义可靠由于数据流分析收集的信息同基本块和控制流有关，通常和变量值无关，因此不同于一般的可靠性证明，例如Hoare逻辑的赋值公理是可靠的

{x=1}x:=x+1{x=2}/sundae_meng第2章数据流分析数据流分析的正确性http://www.2活跃变量分析活跃变量分析的正确性需要将该正确性概念形式地表达出来在活跃变量的初值相同的不同格局下S,1和S,2执行程序S的结果应该是一样的再细化一下，程序每执行一步，得到的不同格局S,1

和S,2

中，活跃变量的值都相同/sundae_meng活跃变量分析活跃变量分析的正确性http://www.doc3第2章数据流分析数据流分析的基础把各种数据流模式作为一个整体来抽象地研究，然后可以形式地回答数据流算法的下列几个基本问题：在什么情况下数据流分析中使用的迭代算法是正确的？该迭代算法所得解的精度如何？该迭代算法是否收敛？数据流方程的解的含义是什么？/sundae_meng第2章数据流分析数据流分析的基础http://www.d4第2章数据流分析为一类数据流模式建一个共同理论框架总结已讨论过的四种数据流分析模式整理出该框架的一些基本特征或原则规范框架中的性质空间要满足的特征规范框架中迁移函数要满足的性质给出框架的定义区分单调框架和分配框架的区别常量传播数据流模式不是分配的/sundae_meng第2章数据流分析为一类数据流模式建一个共同理论框架htt5第2章数据流分析位向量框架（Bitvectorframework）Single-bitrepresentationofeachdataflowpropertySeparabilityofsolution

Dataflowpropertiescanbeevaluated independently

MergeoperationisabitwiseANDorOR operationMonotonicbitfunction

Abitfunctioncannotnegateanybit/sundae_meng第2章数据流分析位向量框架（Bitvectorfra6第2章数据流分析分配性蕴涵单调性的证明l1

l2

并且f(l1

l2)=f(l1)

f(l2)蕴涵f(l1)

f(l2)证明

因为 f(l2)=f(l1

l2)=f(l1)

f(l2)所以 f(l1)

f(l2)/sundae_meng第2章数据流分析分配性蕴涵单调性的证明http://ww7第2章数据流分析常量传播框架的非分配性 说明常量传播框架没有分配性的例子B1EXITz=x+yx=2y=3B3B2x=3y=2/sundae_meng第2章数据流分析常量传播框架的非分配性 说明常量传播框架8第2章数据流分析整数格表示没有任何信息可用表示可能不是常量…3210123…/sundae_meng第2章数据流分析整数格…329第2章数据流分析用集合之间的包含关系来定义部分函数之间的偏序{0,1,1,1,2,1}常函数1阶乘函数{0,1,1,1,2,2}{0,1,1,1}{0,1}{0,5}......................../sundae_meng第2章数据流分析用集合之间的包含关系来定义部分函数之间的10第2章数据流分析数据流方程的求解IDEAL，基于程序所有可能执行路径的解，它少于或等于流图上的执行路径MeetOverallPaths(MOP)，不仅汇集了所有可能路径的数据流值，而且还包括了那些不可能被执行路径的数据流值MaximumFixedPoint(MFP)，由迭代算法得到的解迭代算法得到的MFP解总是安全的

MFPMOPIDEAL/sundae_meng第2章数据流分析数据流方程的求解http://www.d11第2章数据流分析MOP和MFP的比较由MOP的定义，有

MOPo[B4]=((fB3◦fB1)(fB3◦fB2))(vENTRY)在迭代算法(MFP)中，如果按B1，B2，B3和B4的次序访问结点，那么

MFPo[B4]=

fB3(fB1(vENTRY)

fB2(vENTRY))说明路径上较早汇合之影响的流图B1ENTRYB4B3B2/sundae_meng第2章数据流分析MOP和MFP的比较说明12第2章数据流分析敏感性分析路径敏感分析 根据条件分支语句中的谓词来计算不同路径上的信息，它能够区分控制流图上不同路径的信息路径不敏感分析 先前讨论的都是路径不敏感分析流不敏感分析 语句的执行次序对分析来说无关紧要，S1;S2和S2;S1的分析结果肯定一样流敏感分析

先前讨论的都是流敏感分析/sundae_meng第2章数据流分析敏感性分析http://www.doci13第2章数据流分析敏感性分析上下文不敏感分析 组合所有调用点的状态信息，对过程体仅分析一次，返回状态集合的信息用于所有的返回点上下文敏感分析 区分带不同上下文信息的不同调用/sundae_meng第2章数据流分析敏感性分析http://www.doci14第2章数据流分析过程间分析的关注点上下文敏感分析 要注意调用和返回的匹配，注意上下文信息的传递参数传递的方式 仅考虑传值和传结果方式 其他如传引用，会引起别名过程作为参数

在此不考虑/sundae_meng第2章数据流分析过程间分析的关注点http://www.15第2章数据流分析数据流分析的用途编译优化、程序维护程序安全性的检查和编译原理课程的区别基于源代码的结构化分析方法，而不是基于基本块和程序流图的分析从过程内讨论到过程间强调理论基础/sundae_meng第2章数据流分析数据流分析的用途http://www.d16第2章数据流分析数据流分析的正确性数据流分析所得结论同程序运行时的情况一致需要定义机器模型和操作语义，证明所得结论对操作语义可靠由于数据流分析收集的信息同基本块和控制流有关，通常和变量值无关，因此不同于一般的可靠性证明，例如Hoare逻辑的赋值公理是可靠的

{x=1}x:=x+1{x=2}/sundae_meng第2章数据流分析数据流分析的正确性http://www.17活跃变量分析活跃变量分析的正确性需要将该正确性概念形式地表达出来在活跃变量的初值相同的不同格局下S,1和S,2执行程序S的结果应该是一样的再细化一下，程序每执行一步，得到的不同格局S,1

和S,2

中，活跃变量的值都相同/sundae_meng活跃变量分析活跃变量分析的正确性http://www.doc18第2章数据流分析数据流分析的基础把各种数据流模式作为一个整体来抽象地研究，然后可以形式地回答数据流算法的下列几个基本问题：在什么情况下数据流分析中使用的迭代算法是正确的？该迭代算法所得解的精度如何？该迭代算法是否收敛？数据流方程的解的含义是什么？/sundae_meng第2章数据流分析数据流分析的基础http://www.d19第2章数据流分析为一类数据流模式建一个共同理论框架总结已讨论过的四种数据流分析模式整理出该框架的一些基本特征或原则规范框架中的性质空间要满足的特征规范框架中迁移函数要满足的性质给出框架的定义区分单调框架和分配框架的区别常量传播数据流模式不是分配的/sundae_meng第2章数据流分析为一类数据流模式建一个共同理论框架htt20第2章数据流分析位向量框架（Bitvectorframework）Single-bitrepresentationofeachdataflowpropertySeparabilityofsolution

Dataflowpropertiescanbeevaluated independently

MergeoperationisabitwiseANDorOR operationMonotonicbitfunction

Abitfunctioncannotnegateanybit/sundae_meng第2章数据流分析位向量框架（Bitvectorfra21第2章数据流分析分配性蕴涵单调性的证明l1

l2

并且f(l1

l2)=f(l1)

f(l2)蕴涵f(l1)

f(l2)证明

因为 f(l2)=f(l1

l2)=f(l1)

f(l2)所以 f(l1)

f(l2)/sundae_meng第2章数据流分析分配性蕴涵单调性的证明http://ww22第2章数据流分析常量传播框架的非分配性 说明常量传播框架没有分配性的例子B1EXITz=x+yx=2y=3B3B2x=3y=2/sundae_meng第2章数据流分析常量传播框架的非分配性 说明常量传播框架23第2章数据流分析整数格表示没有任何信息可用表示可能不是常量…3210123…/sundae_meng第2章数据流分析整数格…3224第2章数据流分析用集合之间的包含关系来定义部分函数之间的偏序{0,1,1,1,2,1}常函数1阶乘函数{0,1,1,1,2,2}{0,1,1,1}{0,1}{0,5}......................../sundae_meng第2章数据流分析用集合之间的包含关系来定义部分函数之间的25第2章数据流分析数据流方程的求解IDEAL，基于程序所有可能执行路径的解，它少于或等于流图上的执行路径MeetOverallPaths(MOP)，不仅汇集了所有可能路径的数据流值，而且还包括了那些不可能被执行路径的数据流值MaximumFixedPoint(MFP)，由迭代算法得到的解迭代算法得到的MFP解总是安全的

MFPMOPIDEAL/sundae_meng第2章数据流分析数据流方程的求解http://www.d26第2章数据流分析MOP和MFP的比较由MOP的定义，有

MOPo[B4]=((fB3◦fB1)(fB3◦fB2))(vENTRY)在迭代算法(MFP)中，如果按B1，B2，B3和B4的次序访问结点，那么

MFPo[B4]=

fB3(fB