第八讲抽象解释基础格理论.

高级软件工程第八讲抽象解释基础:格理论第八讲抽象解释基础：格理论2/24高级软件工程内容第八讲抽象解释基础：格理论3/24高级软件工程一、偏序二、格三、不动点四、控制流图内容第八讲抽象解释基础：格理论4/24高级软件工程一个偏序是一个数学结构:L=(S,⊑)其中，S是一个集合，⊑(小于等于)是S上的一个二元关系，且满足如下条件：•自反(Reflexivity):∀x∈S:x⊑x•传递(Transitivity):∀x,y,z∈S:x⊑y∧y⊑z⇒x⊑z•反对称(Anti-symmetry):∀x,y∈S:x⊑y∧y⊑x⇒x=y一、偏序(partialorder)第八讲抽象解释基础：格理论5/24高级软件工程假设X⊆S.y∈S是X的上界(upperbound),记作X⊑y,如果：∀x∈X:x⊑y类似地：y∈S是X的下界(lowerbound),记作y⊑X,如果：∀x∈X:y⊑x定义最小上界（leastupperbound）⊔X:X⊑⊔X∧(∀y∈S:X⊑y⇒⊔X⊑y)定义最大下界（greatestlowerbound）⊓X：⊓X⊑X∧(∀y∈S:y⊑X⇒y⊑⊓X)第八讲抽象解释基础：格理论6/24高级软件工程二、格（Lattice）一个格是一个偏序集S，且满足：对于所有的子集X⊆S，⊔X与⊓X都存在一个格一定有：唯一的一个最大元素⊤(top)：⊤=⊔S唯一的一个最小元素⊥(bottom)：⊥=⊓S.由于最小上界和最大下界的唯一性，可以将求x和y的最小上界和最大下界定义为x和y的二元运算：最小上界:x⊔y最大下界:x⊓y为什么？第八讲抽象解释基础：格理论7/24高级软件工程哪些是格?第八讲抽象解释基础：格理论8/24高级软件工程对于任何一个有限集合A，可以定义一个格(2A,⊆),其中，⊥=∅,⊤=A,x⊔y=x∪y,x⊓y=x∩y格的高度是从⊥到⊤的最长路径。例如：上面幂集格的高度是4。一般地：格(2A,⊆)的高度是|A|.第八讲抽象解释基础：格理论9/24高级软件工程三、不动点（Fixed-Points）一个函数f:L→L是单调的(monotone),当:∀x,y∈S:x⊑y⇒f(x)⊑f(y)单调函数不一定是递增的:常量函数也是单调的多个单调函数的复合仍然是单调函数如果将⊔与⊓看作函数,则它们都是单调的第八讲抽象解释基础：格理论10/24高级软件工程对于一个高度有限的格L每个单调函数f有唯一的一个最小不动点:fix(f)=⊔fi(⊥)i0那么:f(fix(f))=fix(f)证明:1)⊥⊑f(⊥)2)f(⊥)⊑f2(⊥)3)⊥⊑f(⊥)⊑f2(⊥)⊑……4)L高度有限,因此对于某个k:fk(⊥)=fk+1(⊥)5)……第八讲抽象解释基础：格理论11/24高级软件工程计算一个不动点的时间复杂度依赖于3个因素:•格的高度•计算f的代价;•测试等价的代价.一个不动点的计算可以表示为格中,从⊥开始向上搜索的过程第八讲抽象解释基础：格理论12/24高级软件工程闭包性质(ClosureProperties)如果L1,L2,...,Ln是有限高度的格,那么乘积(product)为:L1×L2×...×Ln={(x1,x2,...,xn)|xi∈Li}其中⊑是逐点对应的.⊔与⊓可以被逐点计算height(L1×...×Ln)=height(L1)+...+height(Ln)第八讲抽象解释基础：格理论13/24高级软件工程和操作:L1+L2+...+Ln={(i,xi)|xi∈Li\{⊥,⊤}}∪{⊥,⊤}(i,x)⊑(j,y)当且仅当:i=j且x⊑y.height(L1+...+Ln)=max{height(Li)}.第八讲抽象解释基础：格理论14/24高级软件工程如果L是一个有限高度的格,那么lift(L)是:高度：height(lift(L))=height(L)+1.第八讲抽象解释基础：格理论15/24高级软件工程如果A是一个有限集合，那么flat(A):⊤a1a2…an⊥是一个高度为2的格第八讲抽象解释基础：格理论16/24高级软件工程有限高度的映射格（maplattice）定义为:A|→L={[a1|→x1,...,an|→xn]|xi∈L}height(A|→L)=|A|·height(L).第八讲抽象解释基础：格理论17/24高级软件工程如何利用不动点求解等式系统(systemsofequations)?假设L是一个高度有限的格,一个等式系统的形式为:x1=F1(x1,...,xn)x2=F2(x1,...,xn)...xn=Fn(x1,...,xn)xi是变量Fi:Ln→L是单调函数集合每个这样的系统有一个唯一的最小解,且是函数F的最小不动点.F:Ln→Lndefinedby:F(x1,...,xn)=(F1(x1,...,xn),...,Fn(x1,...,xn))第八讲抽象解释基础：格理论18/24高级软件工程我们还可以类似地求解不等式:x1⊑F1(x1,...,xn)x2⊑F2(x1,...,xn)...xn⊑Fn(x1,...,xn)通过观察:x⊑y等价于x=x⊓y这样，上述不等式可以转换为:x1=x1⊓F1(x1,...,xn)x2=x2⊓F2(x1,...,xn)...xn=xn⊓Fn(x1,...,xn)这是一个与前面类似的单调函数等式系统Why?第八讲抽象解释基础：格理论19/24高级软件工程四、控制流图（ControlFlowGraph：CFG）一个控制流图是一个有向图结点对应于程序中的点（语句）边对应与可能的控制流一个CFG总是有单个的入口和单个的出口如果v是一个CFG中的一个点，则：pred(v)是指该点前面点的集合succ(v)是指该点后面点的集合第八讲抽象解释基础：格理论20/24高级软件工程数据流分析与格传统的数据流分析从一个CFG和一个具有有限高度的格L开始对于CFG中的每个点v,我们赋予一个变量[v]，其取值范围是L中的元素.对于编程语言中的每个构造块，我们定义一个数据流约束（dataflowconstraint）该约束反映了一个点与其它点(特别是邻居)之间值的关系第八讲抽象解释基础：格理论21/24高级软件工程对于一个CFG，我们可以抽取变量的约束的集合如果所有的约束刚好是等式或者不等式（右边单调）我们就可以利用不动点算法求唯一的最小解如果所有的解对应于程序的正确信息，则数据流约束是“确定的”（sound）因为解可能或多或少地不精确，所以分析是“保守”的(conservative)但计算最小解将获得最大的精确度第八讲抽象解释基础：格理论22/24高级软件工程不动点算法如果一个CFG具有点V={v1,v2,...,vn},我们可以这样构造格Ln假定点vi产生数据流等式[vi]=Fi([v1],...,[vn])我们构造联合函数F:Ln→LnF(x1,...,xn)=(F1(x1,...,xn),...,Fn(x1,...,xn))第八讲抽象解释基础：格理论23/24高级软件工程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);迭代时重复计算量大许多等式已经不变！第八讲抽象解释基础：格理论24/24高级软件工程x1=⊥;...;xn=⊥;q=[v1,...,vn];while(q[]){assumeq=[vi,...];y=Fi(x1,...,xn);q=q.tail();if(yxi){for(v∈dep(vi))q.append(v);xi=y;}}实际使用的算法:dep(vi)是被Vi影响的点的集合