中国科学技术大学：《程序分析与程序验证》课程教学资源（PPT课件讲稿）第2章 数据流分析（补充）

第2章 数据流分析 内容概述 数据流分析推导的是数据沿着程序执行路 径流动的信息 -过程内的分析：可用表达式分析、到达一定值分 析等 一过程间分析 Shape分析 理论基础 -数据流方程的求解

第2章 数据流分析 • 内容概述 数据流分析推导的是数据沿着程序执行路 径流动的信息 – 过程内的分析：可用表达式分析、到达－定值分 析等 – 过程间分析 – Shape分析 – 理论基础 – 数据流方程的求解

第2章 数据流分析 数据流分析的用途 -编译优化、程序维护 -程序安全性的检查 和编译原理课程的区别 基于源代码的结构化分析方法，而不是基于基 本块和程序流图的分析 从过程内讨论到过程间 强调理论基础

第2章 数据流分析 • 数据流分析的用途 – 编译优化、程序维护 – 程序安全性的检查 • 和编译原理课程的区别 –基于源代码的结构化分析方法，而不是基于基 本块和程序流图的分析 –从过程内讨论到过程间 –强调理论基础

第2章 数据流分析 数据流分析的正确性 数据流分析所得结论同程序运行时的情况一致 需要定义机器模型和操作语义，证明所得结论 对操作语义可靠 由于数据流分析收集的信息同基本块和控制流 有关，通常和变量值无关，因此不同于一般的可 靠性证明，例如Ioare逻辑的赋值公理是可靠的 {x=1}x:=x+1{x=2

第2章 数据流分析 • 数据流分析的正确性 数据流分析所得结论同程序运行时的情况一致 –需要定义机器模型和操作语义，证明所得结论 对操作语义可靠 –由于数据流分析收集的信息同基本块和控制流 有关，通常和变量值无关，因此不同于一般的可 靠性证明，例如Hoare逻辑的赋值公理是可靠的 {x = 1} x := x + 1 {x = 2}

活跃变量分析 活跃变量分析的正确性 需要将该正确性概念形式地表达出来 在活跃变量的初值相同的不同格局下S,σ〉和 〈S,σ)执行程序S的结果应该是一样的 再细化一下，程序每执行一步，得到的不同格 局S,σ)和KS,σ>中，活跃变量的值都相同

活跃变量分析 • 活跃变量分析的正确性 –需要将该正确性概念形式地表达出来 –在活跃变量的初值相同的不同格局下S, 1  和 S, 2 执行程序S的结果应该是一样的 –再细化一下，程序每执行一步，得到的不同格 局S , 1  和S , 2 中，活跃变量的值都相同

第2章 数据流分析 数据流分析的基础 把各种数据流模式作为一个整体来抽象地研 究，然后可以形式地回答数据流算法的下列 几个基本问题： 在什么情况下数据流分析中使用的迭代算法是正 确的？ 该迭代算法所得解的精度如何？ 该迭代算法是否收敛？ 数据流方程的解的含义是什么？

第2章 数据流分析 • 数据流分析的基础 把各种数据流模式作为一个整体来抽象地研 究，然后可以形式地回答数据流算法的下列 几个基本问题： – 在什么情况下数据流分析中使用的迭代算法是正 确的？ – 该迭代算法所得解的精度如何？ – 该迭代算法是否收敛？ – 数据流方程的解的含义是什么？

第2章 数据流分析 为一类数据流模式建一个共同理论框架 总结已讨论过的四种数据流分析模式 整理出该框架的一些基本特征或原则 规范框架中的性质空间要满足的特征 规范框架中迁移函数要满足的性质 给出框架的定义 区分单调框架和分配框架的区别 常量传播数据流模式不是分配的

第2章 数据流分析 • 为一类数据流模式建一个共同理论框架 – 总结已讨论过的四种数据流分析模式 –整理出该框架的一些基本特征或原则 –规范框架中的性质空间要满足的特征 –规范框架中迁移函数要满足的性质 –给出框架的定义 –区分单调框架和分配框架的区别 –常量传播数据流模式不是分配的

第2章 数据流分析 位向量框架(Bit vector framework) Single-bit representation of each data flow property Separability of solution Data flow properties can be evaluated independently Merge operation is a bitwise AND or OR operation Monotonic bit function A bit function cannot negate any bit

第2章 数据流分析 • 位向量框架（Bit vector framework） – Single-bit representation of each data flow property – Separability of solution • Data flow properties can be evaluated independently • Merge operation is a bitwise AND or OR operation – Monotonic bit function • A bit function cannot negate any bit

第2章 数据流分析 ·分配性蕴涵单调性的证明 12并且f1 2)=1) 2)蕴涵1) 2) 证明 因为 2)= 2)=1)2) 所以 1)2)

第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 )

第2章 数据流分析 ·常量传播框架的非分配性 X=3 B2 三 2 Z=X十y B EXIT 说明常量传播框架没有分配性的例子

第2章 数据流分析 • 常量传播框架的非分配性 说明常量传播框架没有分配性的例子 B1 EXIT z = x + y x = 2 y = 3 B3 x = 3 B2 y = 2

第2章 数据流分析 整数格 一⊥表示没有任何信息可用 表示可能不是常量

第2章 数据流分析 • 整数格 – ⊥表示没有任何信息可用 – 表示可能不是常量 ⊥ … −3 −2 −1 0 1 2 3 …