一种用于指针程序验证的指针逻辑 Pointer logic for verification of pointer programs

团购合买资源类别：文库，文档格式：PDF，文档页数：12，文件大小：396.9KB

ISSN 1000-9825,CODEN RUXUEW E-mail:jos@iscas.ac.cn Journal of Sofnare,Vol.21,No.3,March 2010,pp.415-426 http://www.jos.org.cn do:10.3724/SP.J.1001.2010.03620 Tel/Fax:+86-10-62562563 by Institute of Sofnare,the Chinese Academy of Sciences.All rights reserved. 一种用于指针程序验证的指针逻辑陈意云2，李光鹏，王志芳只，华保健中 (中国科学技术大学计算机科学与技术学院，安徽合肥230026) (中因科学技术大学苏州研究院软件安全实验室，江苏苏州215123) Pointer Logic for Verification of Pointer Programs CHEN Yi-Yun'2,LI Zhao-Peng 2+,WANG Zhi-Fang 2,HUA Bao-Jian2 (School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China) (Software Security Laboratory,Suzhou Institute for Advanced Study,University of Science and Technology of China,Suzhou 215123, China) Corresponding author:E-mail:zpli@mail.ustc.edu.cn Chen YY,Li ZP,Wang ZF,Hua BJ.Pointer logic for verification of pointer programs.Journal of Software, 2010,21(3):415-426.htp:/www.jos.org.cn/1000-9825/3620.htm Abstract:This paper improves and extends the pointer logic that has been designed for verifying pointer programs.Its main contribution is that a concept of legal sets of access paths is presented,which simplifies elementary operations on access paths and makes inference rules of the logic easier to understand.Furthermore,the logic with inference rules is extended for local reasoning and for function construction,making the logic used conveniently in the context of function calls. Key words:software safety;Hoare logic;pointer logic;proof-carrying code;certifying compiler 摘要：本文玫进并扩展先前为验证指针程序捉出的指针逻辑，主要页献是提出了合法访问路径集合的概念，极大地简化了访问路径上的基本运算，并使得指针逻辑推理规则变得易理解.另外，增加了局部推理规则和函数构造的推理规则，使得指针逻辑可以方便地用于有函数调用的场合. 关键词：软件安全；Hoare逻辑，指针逻辑；携带证明的代码，出具证明的编译器中图法分类号：TP301文献标识码：A 携带证明的代码(proof-carrying code,简称PCC)I作为一种新的代码范型(paradigm),给编程语言的研究领域带来了巨大挑战：其一是寻找表达力更强的逻辑或类型系统来规范或推理高级语言或低级语言程序的性质：其二是研究出具证明的编译技术，对于第1个挑战，类型化汇编语言四和类型细化的理论)是两种基于类型方式的典型研究，而PCC、携带基础逻辑证明的FPCC(foundational proof-carrying code)、经过验证的汇编编程CAP(certifying assembly programming)和基于栈的经过验证的汇编编程SCAP(stack-based certifying assembly programming)是基于逻辑方式的典型研究基于类型的技术和基于逻辑的技术是互补的，近年来，一些研究人员倾向于组合这两种技 ·Supported by the National Natural Science Foundation of China under Grant Nos.90718026,60928O04(国家自然科学基金) Received 2008-01-16;Accepted 2009-03-31 ©中国科学院软件研究所htp:wwv.c-s-a.org.cn

ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn Journal of Software, Vol.21, No.3, March 2010, pp.415−426 http://www.jos.org.cn doi: 10.3724/SP.J.1001.2010.03620 Tel/Fax: +86-10-62562563 © by Institute of Software, the Chinese Academy of Sciences. All rights reserved. 一种用于指针程序验证的指针逻辑∗ 陈意云 1,2, 李兆鹏 1,2+, 王志芳 1,2, 华保健 1,2 1 (中国科学技术大学计算机科学与技术学院,安徽合肥 230026) 2 (中国科学技术大学苏州研究院软件安全实验室,江苏苏州 215123) Pointer Logic for Verification of Pointer Programs CHEN Yi-Yun1,2, LI Zhao-Peng1,2+, WANG Zhi-Fang1,2, HUA Bao-Jian1,2 1 (School of Computer Science and Technology, University of Science and Technology of China, Hefei 230026, China) 2 (Software Security Laboratory, Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou 215123, China) + Corresponding author: E-mail: zpli@mail.ustc.edu.cn Chen YY, Li ZP, Wang ZF, Hua BJ. Pointer logic for verification of pointer programs. Journal of Software, 2010,21(3):415−426. http://www.jos.org.cn/1000-9825/3620.htm Abstract: This paper improves and extends the pointer logic that has been designed for verifying pointer programs. Its main contribution is that a concept of legal sets of access paths is presented, which simplifies elementary operations on access paths and makes inference rules of the logic easier to understand. Furthermore, the logic with inference rules is extended for local reasoning and for function construction, making the logic used conveniently in the context of function calls. Key words: software safety; Hoare logic; pointer logic; proof-carrying code; certifying compiler 摘要: 本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合. 关键词: 软件安全;Hoare 逻辑;指针逻辑;携带证明的代码;出具证明的编译器中图法分类号: TP301 文献标识码: A 携带证明的代码(proof-carrying code,简称 PCC)[1]作为一种新的代码范型(paradigm),给编程语言的研究领域带来了巨大挑战:其一是寻找表达力更强的逻辑或类型系统来规范或推理高级语言或低级语言程序的性质; 其二是研究出具证明的编译技术. 对于第 1 个挑战,类型化汇编语言[2]和类型细化的理论[3]是两种基于类型方式的典型研究,而 PCC、携带基础逻辑证明的 FPCC(foundational proof-carrying code)[4]、经过验证的汇编编程 CAP(certifying assembly programming)[5]和基于栈的经过验证的汇编编程 SCAP(stack-based certifying assembly programming)[6]是基于逻辑方式的典型研究.基于类型的技术和基于逻辑的技术是互补的,近年来,一些研究人员倾向于组合这两种技 ∗ Supported by the National Natural Science Foundation of China under Grant Nos.90718026, 60928004 (国家自然科学基金) Received 2008-01-16; Accepted 2009-03-31

416 Journal of Software软件学报Vol.21,No.3,March2010 术.应用类型系统ATs将程序状态引入类型系统，依靠ATS与Hoare逻辑的相似性，以ATS来编码Hoare逻辑，从而可以在类型系统上模拟Hoare逻辑的推理」对于第2个挑战，Necula作为先驱者实现了一个叫作Touchstone的出具证明编译器(certifying compiler)I, 它包含一个类型安全的C语言小子集的传统编译器，还有为该编译器生成的汇编代码自动产生类型安全证明的证明器.Touchstone的主要限制是在指针类型和动态存储分配方面.随后，Colby等人实现了Special J例，这是 Java语言较大子集的一个出具证明编译器，它把Java字节代码编译成英特尔IA32体系结构的目标代码. 近年来，我们研究了将出具证明编译和携带证明代码的技术应用到有显式内存管理的编程语言.我们设计了有动态内存分配和回收机制的类C小语言PointerCl1ol,其基本安全策略要求程序运行时不出现通过NULL 指针或悬空指针(dangling pointer))进行存取指向对象的操作、不把NULL指针或悬空指针作为free函数调用的实在参数、不发生内存泄漏等.我们采用一种基于逻辑的和基于类型的技术相结合的方式来推导程序的性质.为了使类型系统简单并保证语言的安全性，我们在定型规则(yping rule)中增加了约束语法表达式的值的副条件.为了静态检查这些副条件，我们为PointerC语言设计了一种指针逻辑l,l,它是Hoare逻辑的一种拓展，新颖之处是，将精确的指针分析应用于程序验证指针逻辑可用来从前向后收集各指针是NULL指针、悬空指针还是有效指针(valid pointer,,有指向对象的指针)的信息，收集各有效指针之间相等与否的信息.所收集信息用来证明指针程序是否满足定型规则的副条件，以支持对指针程序的安全性验证和其他性质的验证，我们完成了 PointerC语言安全性和指针逻辑可靠性的证明]，并实现了PointerC出具证明编译器的一个原型2,1 本文是对指针逻辑前期设计的改进和扩展，主要贡献如下： (1)提出了合法(l©gal)访问路径集合的概念，极大地简化了访问路径上基本运算的定义，并使得指针逻辑推理规则变得直观和易理解： (2)增加了局部推理规则和函数构造的推理规则，使得指针逻辑可以方便地用于有函数调用的场合： (3)与广泛使用的分离逻辑进行了深入比较指针逻辑相当于高级语言层面的分离逻辑，其优于分离逻辑之处是能够防止内存泄漏本文全面介绍重新设计的指针逻辑：第1节介绍PointerC语言.第2节介绍指针逻辑的重新设计.第3节给出采用指针逻辑的一个证明实例第4节比较指针逻辑和分离逻辑第5节是相关工作的比较第6节是总结， 1 PointerC语言 PointerC是一个强调指针类型的类C小语言，它略去函数声明部分的语法（如图1所示），其类型系统可见文献[10]. (Program) program::=structdeclist vardeclist stmtlist (Structure Decl.List)structdeclist::=structdeclist structdeds (Structure Decl.) structdec::=struct id vardeclist; (Variable Decl.List) vardeclist::=vardeclist vardecs (Variable Decl.) vardec::=type idlist; (Identifier List) idlist::=idlist.idid (Type) type::=boolintstruct ids (Statement List) stmtlist:=stmtlist stmtstmt (Statement) stmt::=hval=exp,Ival=malloc(struct id);if boolexp)block else block while(boolexp)block free (al); (Block) block.:=stm叫{stmtlis (Expression) exp::=mumberlNULLVvall-explexp+explexp-explexpxexpl... (Bool Expression) boolexp::=truelfalselexp==explexp!=expl.. -boolexp boolexpAboolexp boolexpvboolexp (L-value) Ial::=idlval->id (Natual Number) number::=012... Fig.I Syntax of PointerC language 图1 PointerC语言语法在PointerC中，指针类型的变量只能用于赋值、相等与否比较、存取指向对象等运算以及作为函数的参数：指针算术和取地址运算(&)被禁止.malloc和free被看成是PointerC预定义的函数，并且满足安全程序的最基本 ©中国科学院软件研究所htp:wwv.c-s-a.org.cn

416 Journal of Software 软件学报 Vol.21, No.3, March 2010 术.应用类型系统 ATS[7]将程序状态引入类型系统,依靠 ATS 与 Hoare 逻辑的相似性,以 ATS 来编码 Hoare 逻辑, 从而可以在类型系统上模拟 Hoare 逻辑的推理. 对于第 2 个挑战,Necula 作为先驱者实现了一个叫作 Touchstone 的出具证明编译器(certifying compiler)[8], 它包含一个类型安全的 C 语言小子集的传统编译器,还有为该编译器生成的汇编代码自动产生类型安全证明的证明器.Touchstone 的主要限制是在指针类型和动态存储分配方面.随后,Colby 等人实现了 Special J[9],这是 Java 语言较大子集的一个出具证明编译器,它把 Java 字节代码编译成英特尔 IA32 体系结构的目标代码. 近年来,我们研究了将出具证明编译和携带证明代码的技术应用到有显式内存管理的编程语言.我们设计了有动态内存分配和回收机制的类 C 小语言 PointerC[10],其基本安全策略要求程序运行时不出现通过 NULL 指针或悬空指针(dangling pointer)进行存取指向对象的操作、不把 NULL 指针或悬空指针作为 free 函数调用的实在参数、不发生内存泄漏等.我们采用一种基于逻辑的和基于类型的技术相结合的方式来推导程序的性质.为了使类型系统简单并保证语言的安全性,我们在定型规则(typing rule)中增加了约束语法表达式的值的副条件.为了静态检查这些副条件,我们为 PointerC 语言设计了一种指针逻辑[11,12],它是 Hoare 逻辑的一种拓展,新颖之处是,将精确的指针分析应用于程序验证.指针逻辑可用来从前向后收集各指针是 NULL 指针、悬空指针还是有效指针(valid pointer,有指向对象的指针)的信息,收集各有效指针之间相等与否的信息.所收集信息用来证明指针程序是否满足定型规则的副条件,以支持对指针程序的安全性验证和其他性质的验证.我们完成了 PointerC 语言安全性和指针逻辑可靠性的证明[13],并实现了 PointerC 出具证明编译器的一个原型[12,14]. 本文是对指针逻辑前期设计的改进和扩展,主要贡献如下: (1) 提出了合法(legal)访问路径集合的概念,极大地简化了访问路径上基本运算的定义,并使得指针逻辑推理规则变得直观和易理解; (2) 增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合; (3) 与广泛使用的分离逻辑进行了深入比较.指针逻辑相当于高级语言层面的分离逻辑,其优于分离逻辑之处是能够防止内存泄漏. 本文全面介绍重新设计的指针逻辑:第 1 节介绍 PointerC 语言.第 2 节介绍指针逻辑的重新设计.第 3 节给出采用指针逻辑的一个证明实例.第 4 节比较指针逻辑和分离逻辑.第 5 节是相关工作的比较.第 6 节是总结. 1 PointerC 语言 PointerC 是一个强调指针类型的类 C 小语言,它略去函数声明部分的语法(如图 1 所示),其类型系统可见文献[10]. Fig.1 Syntax of PointerC language 图 1 PointerC 语言语法在 PointerC 中,指针类型的变量只能用于赋值、相等与否比较、存取指向对象等运算以及作为函数的参数; 指针算术和取地址运算(&)被禁止.malloc 和 free 被看成是 PointerC 预定义的函数,并且满足安全程序的最基本 (Program) program::=structdeclist vardeclist stmtlist (Structure Decl. List) structdeclist::=structdeclist structdec|ε (Structure Decl.) structdec::=struct id{vardeclist}; (Variable Decl. List) vardeclist::=vardeclist vardec|ε (Variable Decl.) vardec::=type idlist; (Identifier List) idlist::=idlist, id|id (Type) type::=bool|int|struct id∗ (Statement List) stmtlist::=stmtlist stmt|stmt (Statement) stmt::=lval=exp; |lval=malloc(struct id); |if (boolexp) block else block |while (boolexp) block |free (lval); (Block) block::=stmt|{stmtlist} (Expression) exp::=number|NULL|lval|−exp|exp+exp|exp–exp|exp×exp|… (Bool Expression) boolexp::=true|false|exp==exp|exp!=exp|… |¬boolexp|boolexp∧boolexp|boolexp∨boolexp (L-value) lval::=id|lval->id (Natual Number) number::=0|1|2|…

陈意云等：一种用于指针程序验证的指针逻辑 417 要求.例如，moc任何一次调用都能成功并且所分配空间同尚未释放空间无任何重叠.另外，布尔表达式不采用短路计算.以方便它们出现在断言中，因为短路的与和或运算都不是可交换运算，以指针类型声明变量开始的v称为访问路径.在本文中，访问路径的前缀（本文所说的前缀都是指真前缀）只指那些仍能构成访问路径的前缀，给访问路径加后缀只指加上后缀仍构成访问路径的情况，我们用表示指针类型访问路径的一个集合，用D表示指针类型访问路径的另一个集合，用表示指针类型访问路径的另外一组集合的每个集合中所有访问路径的类型相同，并且没有访问路径在中多次出现.用平作为它们的总称在语义模型上，用来表示程序点的NULL指针集合，D用来表示程序点的悬空指针集合，的每个集合表示程序点一组指向同一个对象的指针（即右值相等的指针类型访问路径），并且中不同集合的指针指向不同对象Ⅱ咯集合中的指针都称为有效指针.因此，阿以看成程序状态中所有指针的一种强调相等与否而不关心具体值的抽象.区分和D是因为程序可以通过判断访问路径是否等于NULL来区分NULL指针和悬空指针我们需要合法良形的平，因为并非任意的4都能表达上面的意思，先基于来定义访问路径的别名.出现在同一个集合中的访问路径加上同样后缀形成的访问路径互为别名，访问路径别名关系还是自反的按此定义，判断两条访问路径是否互为别名的谓词如下： alias(p,q)兰p=qv3s.3r,1,p',q.(s不是空串w和1属于的同一集合p=(p's)Aq=(gs)alias(p,)alias(g,), 其中，=表示语法上相同，·表示串并置.该定义说明，若p和q不相同，则忽略相同后缀s之后，判断它们的别名是否出现在的同一个集合中.若递归计算时出现再次判断p和g是否为别名，则计算将会不终止，这时也认为p和g 不是别名而停止计算，合法需要满足下面几个条件： (1)所有指针类型的声明变量都在中： (2)对7咯集合中的任何访问路径p,若p所指向结构类型有指针类型域r,则p->r的某个别名在中， (3)对中任何访问路径，中的任何其他访问路径都不是它的别名： (4)若访问路径p在中，则对p的每个前缀，它的一个别名在中与合法中的某条访问路径互为别名的访问路径都叫做合法的指针类型访问路径整型访问路径是合法的，若其各前缀都是合法的指针类型访问路径程序点的所有合法访问路径的集合用P表示. 若某访问路径的两个不同前缀都有别名出现在的同一个集合中，则称该访问路径带环.例如，若7识有两个集合{s,s->next-> next}和{s->next},和D都是空集，如图2所示，则s->ner1->nex-> next是带环的访问路径. Fig.2 Cyclic linked list with two nodes 无环访问路径称为最简访问路径，下面假定程序中仅出现最图2两个结点的循环链表简访问路径 2指针逻辑的设计为证明程序满足基本安全策略，我们除了为PointerC设计一个类型系统外，还为它设计了一个证明系统.因为该类型系统的某些定型规则中有副条件，例如，程序表达式中出现的访问路径必须是合法访问路径、操作不能引起内存泄漏等，这些副条件都不能由通常的类型系统来检查，我们用Hoae逻辑的一种扩展（称为指针逻辑)来证明它们本节介绍指针逻辑的重新设计，下面先介绍指针逻辑所用的断言语言 2.1断言语言断言语言的语法如图3所示.其中，exp,boolexp和val的语法见PointerC语法，{valset}用来表示访问路径集合，带下标N或D的分别表示集合和D集合.hval(->idp是断言语言增加的一种访问路径表示，s(->nex) 是s->nex->next…->nex1的缩写（其中，->nex1出现i次），若=0，则s(->next)就表示s. 在该文法的基础上，对断言的一些其他约束如下： ©中国科学院软件研究所htp:wwv.c-s-a.org.cn

陈意云等:一种用于指针程序验证的指针逻辑 417 要求.例如,malloc 任何一次调用都能成功并且所分配空间同尚未释放空间无任何重叠.另外,布尔表达式不采用短路计算,以方便它们出现在断言中,因为短路的与和或运算都不是可交换运算. 以指针类型声明变量开始的 lval 称为访问路径.在本文中,访问路径的前缀(本文所说的前缀都是指真前缀) 只指那些仍能构成访问路径的前缀,给访问路径加后缀只指加上后缀仍构成访问路径的情况. 我们用N表示指针类型访问路径的一个集合,用D表示指针类型访问路径的另一个集合,用Π表示指针类型访问路径的另外一组集合.Π的每个集合中所有访问路径的类型相同,并且没有访问路径在Π中多次出现.用Ψ 作为它们的总称.在语义模型上,N用来表示程序点的 NULL 指针集合,D用来表示程序点的悬空指针集合,Π的每个集合表示程序点一组指向同一个对象的指针(即右值相等的指针类型访问路径),并且Π中不同集合的指针指向不同对象.Π各集合中的指针都称为有效指针.因此,Ψ可以看成程序状态中所有指针的一种强调相等与否而不关心具体值的抽象.区分N和D是因为程序可以通过判断访问路径是否等于 NULL 来区分 NULL 指针和悬空指针.我们需要合法良形的Ψ,因为并非任意的Ψ都能表达上面的意思.先基于Π来定义访问路径的别名.出现在Π同一个集合中的访问路径加上同样后缀形成的访问路径互为别名,访问路径别名关系还是自反的.按此定义,判断两条访问路径是否互为别名的谓词如下: alias(p,q)p≡q∨∃s.∃r,t,p′,q′.(s 不是空串∧r 和 t 属于Π的同一集合∧p≡(p′⋅s)∧q≡(q′⋅s)∧alias(p′,r)∧alias(q′,t)), 其中,≡表示语法上相同,⋅表示串并置.该定义说明,若 p 和 q 不相同,则忽略相同后缀 s 之后,判断它们的别名是否出现在Π的同一个集合中.若递归计算时出现再次判断 p 和 q 是否为别名,则计算将会不终止,这时也认为 p 和 q 不是别名而停止计算. 合法Ψ需要满足下面几个条件: (1) 所有指针类型的声明变量都在Ψ中; (2) 对Π各集合中的任何访问路径 p,若 p 所指向结构类型有指针类型域 r,则 p->r 的某个别名在Ψ中; (3) 对Ψ中任何访问路径,Ψ中的任何其他访问路径都不是它的别名; (4) 若访问路径 p 在Ψ中,则对 p 的每个前缀,它的一个别名在Π中. 与合法Ψ中的某条访问路径互为别名的访问路径都叫做合法的指针类型访问路径.整型访问路径是合法的,若其各前缀都是合法的指针类型访问路径.程序点的所有合法访问路径的集合用P表示. 若某访问路径的两个不同前缀都有别名出现在Π的同一个集合中,则称该访问路径带环.例如,若Π只有两个集合{s,s->next-> next}和{s->next},N和D都是空集,如图 2 所示,则 s->next->next-> next 是带环的访问路径. 无环访问路径称为最简访问路径,下面假定程序中仅出现最简访问路径. 2 指针逻辑的设计为证明程序满足基本安全策略,我们除了为 PointerC 设计一个类型系统外,还为它设计了一个证明系统.因为该类型系统的某些定型规则中有副条件,例如,程序表达式中出现的访问路径必须是合法访问路径、free 操作不能引起内存泄漏等,这些副条件都不能由通常的类型系统来检查,我们用 Hoare 逻辑的一种扩展(称为指针逻辑)来证明它们.本节介绍指针逻辑的重新设计,下面先介绍指针逻辑所用的断言语言. 2.1 断言语言断言语言的语法如图 3 所示.其中,exp,boolexp 和 lval 的语法见 PointerC 语法,{lvalset}用来表示访问路径集合,带下标 N 或 D 的分别表示N集合和D集合.lval(->id) exp 是断言语言增加的一种访问路径表示,s(->next) i 是 s->next->next…->next 的缩写(其中,->next 出现 i 次),若 i=0,则 s(->next) i 就表示 s. 在该文法的基础上,对断言的一些其他约束如下: Fig.2 Cyclic linked list with two nodes 图 2 两个结点的循环链表 s

418 Journal of Software软件学报Vol.2l,No.3,March2010 (I)domain中的N和N分别是指自然数集和正整数集，exp.exp中的exp和作为访问路径上角标的exp 限制为最多含一个约束变元n的整型表达式壮b或b,其中，b可以是含程序变量和常量的只有加减运算的表达式； (2)当访问路径集合受多个量词约束时，存在量词约束出现在最左边： (3)访问路径集合之前不可以出现. 例如，i0.n-1.{s->(->r片是指{s->}A{s->->rA..A{s->(->r)-1},这些访问路径集合都是中☑的一个集合有了量词和带上角标的访问路径，图4中带头结点的双向循环链表用断言定义如下： dlist(s,n)e(k1.n.{s(->r)(->r)+1->)n{s,s(->r)1s->r->. 其中，s是struct ListNode{struct ListNode*r,*I,}类型的指针，n表示除头结点以外的结点数（非负整数）.全称量词所辖的最后一个集合可以写成{s(->r”,5->,以删掉s(>)+1>1中的环（这时k为n),上式是为了把它统一到全称量词辖域中因此，断言中的访问路径允许带环该定义的+1个访问路径集合将图2中2n+3个指针的相等关系表达得一清二楚.并且对图4的每个指针，该定义都从能够表示它的互为别名的访问路径中选择一条访问路径来表示它.注意，dis1定义中最后一个集合改写成{s,s->->r,s(>)时1}看上去是合理的，但这时该定义式不是一个合法的平因为{s,s->->r,(>)}中除了s以外，访问路径都是s->1..的形式，而其他有效指针集合中的访问路径都是s->r..的形式在>0时，在这些集合中找不到s->1->r的前缀s>1的别名 (Assertion)assertion::=-assertion assertionnassertion assertionvassertionVid:domain.assertion id:domain.assertion(assertion)id lval) boolexplvalsetalsetlvalsetp (Domain) domain:=NNl门exp.ep (L-value Set)lvalser::=hvalset.Ivalllyal 白江双 (L-value) lval::=...val->idy Fig.3 Syntax of assertion language Fig.4 Cyclic doubly-linked list 图3断言语言语法图4双向循环链表有些数据结构的断言定义需要引入归纳，例如二叉树的定义如下(s仍然是ListNode类型的指针)： tree(s)(s)((s)Atree(s->I)Iree(s->r)), 其中，{s}w表示空树，另一种情况{s}Aee(s->)nee(s->r)表示非空树，并且表达出该树上的指针都不相等，因为若把归纳定义的引用展开，代表有效指针的各访问路径都在的不同集合中， 2.2断言演算利用经典逻辑中有关入和的等价公理，可以把含访问路径集合的断言变换成析取范式，在变换过程中，每个访问路径集合看成一个逻辑常元在断言的析取范式中，每个子句中的访问路径集合部分构成一个平例如，上面二叉树归纳定义右部的断言就是一个析取范式，两个子句中的代表两种不同情况.注意，子句中可能还有其他断言，有些断言甚至和判断的合法性有关例如，数据结构归纳定义的引用，涉及访问路径上角标的断言。依据不丢失访问路径信息的原则，经典逻辑的蕴涵公理A入B一A在B含访问路径集合或归纳定义的引用时不可使用，因为使用它会导致访问路径信息的丢失，逻辑蕴涵公理A入B一B的情况类似我们还需要增加一些与有关的逻辑等价或蕴涵公理， 1)W和D的等价公理 MM台W(若(=MU2n(n=0), DAD3台D(若(D-=DUD)(DnD=) 这些等价性存在的依据是等价式两边包含同样的信息 2)非合法平公理引入量词和数据结构的归纳定义后，需要将先前合法的条件加以补充， (1)合法的检查是对析取范式的各子句分别进行， ©中国科学院软件研究所htp:wwv.c-s-a.org.cn

418 Journal of Software 软件学报 Vol.21, No.3, March 2010 (1) domain 中的 N 和 N+ 分别是指自然数集和正整数集,exp..exp 中的 exp 和作为访问路径上角标的 exp 限制为最多含一个约束变元 n 的整型表达式 n±b 或 b,其中,b 可以是含程序变量和常量的只有加减运算的表达式; (2) 当访问路径集合受多个量词约束时,存在量词约束出现在最左边; (3) 访问路径集合之前不可以出现¬. 例如,∀i:0..n−1.{s->l(->r) i }是指{s->l}∧{s->l->r}∧…∧{s->l(->r) n−1 },这些访问路径集合都是Ψ中Π的一个集合.有了量词和带上角标的访问路径,图 4 中带头结点的双向循环链表用断言定义如下: dlist(s,n)(∀k:1..n.{s(->r) k ,s(->r) k+1->l})∧{s,s(->r) n+1,s->r->l}. 其中,s 是 struct ListNode{struct ListNode*r,*l;}类型的指针,n 表示除头结点以外的结点数(非负整数).全称量词所辖的最后一个集合可以写成{s(->r) n ,s->l},以删掉 s(->r) k+1->l 中的环(这时 k 为 n),上式是为了把它统一到全称量词辖域中.因此,断言中的访问路径允许带环.该定义的 n+1 个访问路径集合将图 2 中 2n+3 个指针的相等关系表达得一清二楚.并且对图 4 的每个指针,该定义都从能够表示它的互为别名的访问路径中选择一条访问路径来表示它.注意,dlist 定义中最后一个集合改写成{s,s->l->r,s(->l) n+1}看上去是合理的,但这时该定义式不是一个合法的Ψ.因为{s,s->l->r,s(->l) n+1}中除了 s 以外,访问路径都是 s->l…的形式,而其他有效指针集合中的访问路径都是 s->r…的形式.在 n>0 时,在这些集合中找不到 s->l->r 的前缀 s->l 的别名. Fig.3 Syntax of assertion language Fig.4 Cyclic doubly-linked list 图 3 断言语言语法图 4 双向循环链表有些数据结构的断言定义需要引入归纳,例如二叉树的定义如下(s 仍然是 ListNode 类型的指针): tree(s){s}N∨({s}∧tree(s->l)∧tree(s->r)), 其中,{s}N 表示空树,另一种情况{s}∧tree(s->l)∧tree(s->r)表示非空树,并且表达出该树上的指针都不相等,因为若把归纳定义的引用展开,代表有效指针的各访问路径都在Π的不同集合中. 2.2 断言演算利用经典逻辑中有关∧和∨的等价公理,可以把含访问路径集合的断言变换成析取范式.在变换过程中,每个访问路径集合看成一个逻辑常元.在断言的析取范式中,每个子句中的访问路径集合部分构成一个Ψ.例如,上面二叉树归纳定义右部的断言就是一个析取范式,两个子句中的Ψ代表两种不同情况.注意,子句中可能还有其他断言,有些断言甚至和判断Ψ的合法性有关.例如,数据结构归纳定义的引用,涉及访问路径上角标的断言. 依据不丢失访问路径信息的原则,经典逻辑的蕴涵公理 A∧B⇒A 在 B 含访问路径集合或归纳定义的引用时不可使用,因为使用它会导致访问路径信息的丢失,逻辑蕴涵公理 A∧B⇒B 的情况类似. 我们还需要增加一些与Ψ有关的逻辑等价或蕴涵公理. 1) N和D的等价公理 N1∧N2⇔N (若(N==N1∪N2)∧(N1∩N2==∅)), D1∧D2⇔D (若(D==D1∪D2)∧(D1∩D2==∅)). 这些等价性存在的依据是等价式两边包含同样的信息. 2) 非合法Ψ公理引入量词和数据结构的归纳定义后,需要将先前合法Ψ的条件加以补充. (1) 合法Ψ的检查是对析取范式的各子句分别进行; (Assertion)assertion::= ¬assertion|assertion∧assertion |assertion∨assertion|∀id:domain.assertion |∃id:domain.assertion|(assertion)|id(lval) | boolexp|{lvalset}|{lvalset}N|{lvalset}D (Domain) domain::=N| N+ |exp..exp (L-value Set) lvalset::=lvalset,lval|lval (L-value) lval::=…|lval(->id) exp … s …

陈意云等：一种用于指针程序验证的指针逻辑 419 (2)量词的引入并不改变合法4的条件.它给哈法性的检查带来困难，该问题将另文加以讨论； (3)出现数据结构归纳定义的引用时，把每个引用式中作为变元的指针类型访问路径当成集合中的元素，然后按先前的条件来检查的合法性.不展开归纳定义的引用，意味着暂不关心未展开部分，而把变元看成的元素也就是在检查合法性时暂不管未展开部分； (4)数据结构的归纳定义必须是合法的也就是说，归纳定义右部析取范式的每个子句都必须是合法的可以把合法性的概念扩大到析取范式的完整子句，即除了以外，还有其他断言（用Q作为总称）.%Q是合法的，若4是合法的，并且Q中出现的任何访问路径也都是合法的，具体的蕴涵公理如下： →false(若平不是合法的)】 %Q→false(若域Q不是合法的). 3)等价公理 (I)在合法Ψ吓，若访问路径集合乃和乃满足p:.3q:乃.alias(p,q)A廿q:乃.3p:乃.alias(q,p),并且乃和的元素个数一样，则称它们等价.访问路径集合等价公理如下： R1台乃（若在合法乎吓，R和乃等价） (2)下面用S,…,品表示构成的n个访问路径集合，则合法的等价公理是 SAAS入M仄D一A.A入WAD(若左右两边都是合法的，并且各对应集合都基于左边等价)】 4)附布尔表达式的吸收或否定 Hoare逻辑中，条件语句和循环语句的推理规则会使程序中的布尔表达式p=WULL,pl=NULL,p==q和pl=q (炉和q都是指针类型)等出现在断言中若它们和无矛盾则被吸收，有矛盾则断言为假.下面列举一些这样的蕴涵公理其中记号S表示访问路径p的别名所在的集合，S9的含义类似. SiA...ASSPADAp==NULLAO-false. Sin...SPADAp--NULLNOSA...ASDnO, SA..An-1ASP”MMDp=NULLAO曰SA..ASn-MDnQ, A.AS-1AS99人MDp==qnQ台SA.…ASn-1AS9入MDnQ, SA...AS-SP A4AADAp!=gnO-false. 例如，对于先前的二叉树归纳定义，若p=ULL,则有 Iree(p)p=NULL=(ipwv({p}Atree(p->)ntree(p->r)p=NULL(=在此表示将定义展开) (p)NAP!=NULLV(p)Atree(p->DAtree(p->r)Ap!=NULL →falsev(p}ntree(p->D)Atree(p->r） pintree(p->Dntree(p->r). 2.3指针逻辑的推理规则先定义一些在推理规则中要用到的基本运算，它们的计算基于相应程序点的平 (I)删除访问路径：在访问路径集合冲删除访问路径p的别名或集合{P1,,P}中各访问路径的别名。 R-pg:alias(qp), 2-{P1,…Pn}(乃-p1-Pn). (2)增加访问路径：在访问路径集合中加入访问路径p或集合R中各访问路径 Rtp兰aU{p}, R+R兰RUR (3)前缀替换：对访问路径集合中以p的别名为前缀的每条访问路径q,都用它的一个别名④来代替，（不以p的别名为前缀，R中其余访问路径维持不变.下面定义中谓词peix(r,q)表示r是q的前缀. Rip where g:.(r.P(alias(rp)prefix(r,q))). ©中国科学院软件研究所htp:wwv.c-s-a.org.cm

陈意云等:一种用于指针程序验证的指针逻辑 419 (2) 量词的引入并不改变合法Ψ的条件.它给Ψ合法性的检查带来困难,该问题将另文加以讨论; (3) 出现数据结构归纳定义的引用时,把每个引用式中作为变元的指针类型访问路径当成N集合中的元素, 然后按先前的条件来检查Ψ的合法性.不展开归纳定义的引用,意味着暂不关心未展开部分,而把变元看成N的元素也就是在检查合法性时暂不管未展开部分; (4) 数据结构的归纳定义必须是合法的.也就是说,归纳定义右部析取范式的每个子句都必须是合法的. 可以把合法性的概念扩大到析取范式的完整子句,即除了Ψ以外,还有其他断言(用 Q 作为总称).Ψ∧Q 是合法的,若Ψ是合法的,并且 Q 中出现的任何访问路径也都是合法的. 具体的蕴涵公理如下: Ψ⇒false (若Ψ不是合法的), Ψ∧Q⇒false (若Ψ或 Q 不是合法的). 3) Ψ等价公理 (1) 在合法Ψ下,若访问路径集合R1 和R2 满足∀p:R1.∃q:R2.alias(p,q)∧∀q:R2.∃p:R1.alias(q,p),并且R1 和R2 的元素个数一样,则称它们等价.访问路径集合等价公理如下: R1⇔R2 (若在合法Ψ下,R1 和R2 等价). (2) 下面用S1,…,Sn 表示构成Π的 n 个访问路径集合,则合法Ψ的等价公理是 S1∧…∧Sn∧N∧D⇔ 1 S ′ ∧…∧ n S ′ ∧N ′ ∧D′ (若左右两边都是合法的,并且各对应集合都基于左边等价). 4) Ψ对布尔表达式的吸收或否定 Hoare 逻辑中,条件语句和循环语句的推理规则会使程序中的布尔表达式 p==NULL,p!=NULL,p==q 和 p!=q (p 和 q 都是指针类型)等出现在断言中.若它们和Ψ无矛盾则被吸收,有矛盾则断言为假.下面列举一些这样的蕴涵公理.其中记号Sp 表示访问路径 p 的别名所在的集合,Sp ,q 的含义类似. S1∧…∧Sn−1∧Sp∧N∧D∧p==NULL∧Q⇒false, S1∧…∧Sn∧Np∧D∧p==NULL∧Q⇒S1∧…∧Sn∧Np∧D∧Q, S1∧…∧Sn−1∧Sp∧N∧D∧p!=NULL∧Q⇒S1∧…∧Sn−1∧Sp∧N∧D∧Q, S1∧…∧Sn−1∧Sp ,q ∧N∧D∧p==q∧Q⇒S1∧…∧Sn−1∧Sp ,q ∧N∧D∧Q, S1∧…∧Sn−1∧Sp ,q ∧N∧D∧p!=q∧Q⇒false. 例如,对于先前的二叉树归纳定义,若 p!=NULL,则有 tree(p)∧p!=NULL≡({p}N∨({p}∧tree(p->l)∧tree(p->r)))∧p!=NULL(≡在此表示将定义展开) ⇒{p}N∧p!=NULL∨{p}∧tree(p->l)∧tree(p->r)∧p!=NULL ⇒false∨{p}∧tree(p->l)∧tree(p->r) ⇒{p}∧tree(p->l)∧tree(p->r). 2.3 指针逻辑的推理规则先定义一些在推理规则中要用到的基本运算,它们的计算基于相应程序点的Ψ. (1) 删除访问路径:在访问路径集合R中删除访问路径 p 的别名或集合{p1,..., pn}中各访问路径的别名. R−p{q:R|¬alias(q,p)}, R−{p1,...,pn}((R−p1)...−pn). (2) 增加访问路径:在访问路径集合R中加入访问路径 p 或集合R′中各访问路径. R+pR∪{p}, R+R′R∪R′. (3) 前缀替换:对访问路径集合R中以 p 的别名为前缀的每条访问路径 q,都用它的一个别名 q′来代替,q′不以 p 的别名为前缀;R中其余访问路径维持不变.下面定义中谓词 prefix(r,q)表示 r 是 q 的前缀. R/pR′ where R′⇔R∧∀q:R′.(¬∃r:P.(alias(r,p)∧prefix(r,q)))

420 Journal of Software软件学报Vol.2l,No.3,March2010 (4)测试内存泄漏leak(Sp) 删除集合中的访问路径p时（出现在对p赋值时），若S中所有访问路径都是p的别名或以p的别名为前缀，则会出现内存泄漏。 leak(Sp)g:S(alias(q.p)v3r:P.(alias(r.p)prefix(r,q))). 下面给出联系到PointerC各种语句的公理和推理规则这些规则体现了相应语句引起访问路径集合的增、删和替换在下面所有规则中，访问路径上的计算都是基于语句前那个程序点的平，并且Q中能被吸收的布尔表达式己被吸收， 1)指针类型赋值语句p=q和p=NULL 下面只列举几种情况下的规则，其他情况下的规则类似： (1)p和q都有别名在的同一个集合中 {SA..ASn1ASP4入仄DnQ}P=q{SA.AS-ASg4仄DQ} (2)p的别名在中，q的别名在的某个集合中。 (SiA...ASS9PADnO)p=qSi...(+p)(NP-p)DnO) (3)p的别名在的某个集合中，q的别名在中 (Sin...SISPDnO)p=gi Silpn..S-lpn(s lp-p)n(N Ip+p)nDpnOlp) (若对于赋值前的平，leak(S,p)为假). 其中，Qp的意思也是把Q中以p的别名为前缀的访问路径都用它们不以p的别名为前缀的别名替换， (4)赋值语句是p=WULL的形式且p的别名D冲 (Sin...SMADO)p=NULLISiN...S(N+p)(D-p)o) (S)p的别名和q别名在不同的中可以把该语句当作dhmm=p,p=NULL:p=dummy,dummy=NULL语句序列来证明，当然也可以设计专门的规则.每个函数可以看成有一个虚拟局部变量dummy,.初值是NULL,每次遇到这类赋值时都这么处理，在函数结束时将dumy从中去掉 2)非指针类型的赋值语句x=e 在此用的是正向的赋值公理，其中，FV表示变元中的自由变量集合. (Sin...ASADnO)x=e(Sin..AMADA(3x'.(x=-e[xe-x']nO[V-x]...[nx][xe-x'])), 1…yn是Q中出现的x的所有别名，x'E({UFV(e)UFVO) 3)复合、条件和循环语句的规则复合、条件和循环语句的规则以及推论规则等仍然使用Hoare逻辑的规则. 4)分配空间语句p=malloc(structt) 其中，1是结构类型，并假设r,厂是1的指针类型的域名.下面只列举两种情况： (1)p的别名在中 (S...ASPADAO)p=malloc(struct t)(SA...Sip)(NP-p)(Drip->r1....p->rO) (2)p的别名在的某个集合中可以把该语句看成语句序列p=NULL:P=malloc(struct)来进行证明，当然也可以设计专门的规则. 5)释放空间语句ree(p) 只有p在的某个集合中，才能使用fe函数.根据p所指对象的类型可以知道，其所有指针类型域的访问路径p->r1…p->rm把该语句当成语句序列p->r=NULL,…p->r。=NULL;free(p)来进行证明.这样做的目的是简化fee(p)的规则. {SA..ASx-AS入仄DO)free(p){SA.An-1A(仁{p->r1,…p->rn})(D4S)nQ(若Q中没有p的别名)， 6)分情况规则需要增加一条分情况证明规则，因为一个语句前条件的析取范式可能使分成多种情况.该规则如下： ©中国科学院软件研究所htp:wwv.c-s-a.org.cn

420 Journal of Software 软件学报 Vol.21, No.3, March 2010 (4) 测试内存泄漏 leak(S,p) 删除Π集合S中的访问路径 p 时(出现在对 p 赋值时),若S中所有访问路径都是 p 的别名或以 p 的别名为前缀,则会出现内存泄漏. leak(S,p)∀q:S.(alias(q,p)∨∃r:P.(alias(r,p)∧prefix(r,q))). 下面给出联系到 PointerC 各种语句的公理和推理规则.这些规则体现了相应语句引起访问路径集合的增、删和替换.在下面所有规则中,访问路径上的计算都是基于语句前那个程序点的Ψ,并且 Q 中能被Ψ吸收的布尔表达式已被吸收. 1) 指针类型赋值语句 p=q 和 p=NULL 下面只列举几种情况下的规则,其他情况下的规则类似: (1) p 和 q 都有别名在Π的同一个集合中. {S1∧…∧Sn−1∧Sp ,q ∧N∧D∧Q}p=q{S1∧…∧Sn−1∧Sp ,q ∧N∧D∧Q}. (2) p 的别名在N中,q 的别名在Π的某个集合中. {S1∧…∧Sn−1∧Sq∧Np∧D∧Q}p=q{S1∧…∧Sn−1∧(Sq +p)∧(Np −p)∧D∧Q}. (3) p 的别名在Π的某个集合中,q 的别名在N中. {S1∧…∧Sn−1∧Sp∧Nq∧D∧Q}p=q{S1/p∧…∧Sn−1/p∧(Sp /p−p)∧(Nq /p+p)∧D/p∧Q/p} (若对于赋值前的Ψ,leak(Sp ,p)为假). 其中,Q/p 的意思也是把 Q 中以 p 的别名为前缀的访问路径都用它们不以 p 的别名为前缀的别名替换. (4) 赋值语句是 p=NULL 的形式且 p 的别名D中. {S1∧…∧Sn∧N∧Dp∧Q}p=NULL{S1∧…∧Sn∧(Np +p)∧(Dp −p)∧Q}. (5) p 的别名和 q 别名在不同的Π中. 可以把该语句当作 dummy=p;p=NULL;p=dummy;dummy=NULL 语句序列来证明,当然也可以设计专门的规则.每个函数可以看成有一个虚拟局部变量 dummy,初值是 NULL,每次遇到这类赋值时都这么处理,在函数结束时将 dummy 从N中去掉. 2) 非指针类型的赋值语句 x=e 在此用的是正向的赋值公理,其中,FV 表示变元中的自由变量集合. {S1∧…∧Sn∧N∧D∧Q}x=e{S1∧…∧Sn∧N∧D∧(∃x′.(x==e[x←x′]∧Q[y1←x]…[yn←x][x←x′])), (y1,…,yn 是 Q 中出现的 x 的所有别名,x′∉({x}∪FV(e)∪FV(Q))). 3) 复合、条件和循环语句的规则复合、条件和循环语句的规则以及推论规则等仍然使用 Hoare 逻辑的规则. 4) 分配空间语句 p=malloc(struct t) 其中,t 是结构类型,并假设 r1,…,rn 是 t 的指针类型的域名.下面只列举两种情况: (1) p 的别名在N中 {S1∧…∧Sn∧Np∧D∧Q}p=malloc(struct t){S1∧…∧Sn∧{p}∧(Np −p)∧(D+{p->r1,…,p->rn})∧Q}. (2) p 的别名在Π的某个集合中可以把该语句看成语句序列 p=NULL;p=malloc(struct t)来进行证明,当然也可以设计专门的规则. 5) 释放空间语句 free(p) 只有 p 在Π的某个集合中,才能使用 free 函数.根据 p 所指对象的类型可以知道,其所有指针类型域的访问路径 p->r1,…,p->rn.把该语句当成语句序列 p->r1=NULL;…;p->rn=NULL;free(p)来进行证明.这样做的目的是简化 free(p)的规则. {S1∧…∧Sn−1∧Sp∧N∧D∧Q}free(p){S1∧…∧Sn−1∧(N−{p->r1,…,p->rn})∧(D+Sp )∧Q}(若 Q 中没有 p 的别名). 6) 分情况规则需要增加一条分情况证明规则,因为一个语句前条件的析取范式可能使Ψ分成多种情况.该规则如下:

陈意云等：一种用于指针程序验证的指针逻撰 421 出A9SΨAQ}A9SΨA2,} {AgV平2A22S3AQ3V平：AQ} 其中，S表示PointerC的程序段.Hoare逻辑原本没有这样的规则，因为{x=Ivax==2}这样的前条件虽然也可以看成两种不同情况，但Hoae逻辑赋值公理可以同时对该析取范式的两个子句进行语法代换， 7)结构规则(frame rule) 为了获得更有效的推理方法，有时需要拆分或合并合法平，若合法乎是SA.ASA人D,H和华分别是 SA..AS入AD和S+1A..AS人M5D,并且一，DAD一D若出对一部分指针类型声明变量来说是合法的，华对剩余的指针类型声明变量来说是合法的，则称阿拆分成出和华，出和华可合并成平显然，这时有一平A华.用于局部推理的规则如下：出AO)SIO HA平2AgΛQ2}SA平2AgAQ2} 其中，出AQ1和AQ2分别都是合法的例如，在函数调用点，H八Q1和八Q2分别可用来表示和被调用函数有关和无关的部分 2.4函数构造的推理规则 PointerC在第1节的文法基础上还有函数构造，本节讨论指针逻辑有关函数构造的规则.为突出重点并简化讨论，我们做如下限制或约定： (I)函数∫的声明形式是arg){vardeclist stmtlist),ag是∫唯一的并且是指针类型的参数，vardeclist和 stmtlist是∫的变量声明表和语句表.函数调用语句的形式是re=ac),act是实参.在下面的规则中，y1,,yk表示函数「声明的所有指针类型局部变量： (2)假定函数体中有一个局部变量res,它和用户声明的任何局部变量都不同名，函数体中的语句return e都变换成es=e,return res来进行推理，以使return的规则简单有了函数构造后，合法的检查以按作用域规则可见的全局和局部的指针类型声明变量为基础. 下面仅给出参数和返回值都是指针类型的推理规则，其他情况的规则比这些规则简单递归函数、过程和递归过程的规则都不难在此基础上得出 1)函数声明 ΨA{y,,k,resinO}stmtlistΨ'AQ {ΨAQ}f(arg){ardeclist stmtlist{Ψ'入Q'} 在%Q的基础上添加{v1·,Vk,es}作为函数语句表的前断言，这是因为这些指针类型局部变量和s在函数体执行前都被看成悬空指针」 2)函数调用语句 PargO)arg =act))f(arg)vardeclist stmtlistO') A{rei.Oret=f(ac)H(Ψ'Ag)res←re]} 参数为指针类型的函数调用必须体现进入被调用函数时，形参和实参在同一个指针集合中，这是通过在该规则的前提中显式增加一个指针赋值语句ag:=ac1来体现的对于返回值，也可以用类似的方法来解决在这里是调用前限制e1为NULL指针，调用后通过代换来使e1出现在断言中 3)return语句 )=NULL()...-=NULLO arg =NULL) oCoreturn res(N+-(v....varg) 函数终止时，指针类型局部变量1，，和形参ag不再能访问，因此应把中有关它们的信息删去 2.5指针逻辑的可靠性我们己经完成PointerC语言安全性的证明和指针逻辑早先版本对PointerC语言操作语义可靠的证明l], 本文对指针逻辑的完善只影响指针逻辑可靠的证明细节这里概述指针逻辑可靠的证明框架： ©中国科学院软件研究所htp:wwv.c-s-a.org.cn

陈意云等:一种用于指针程序验证的指针逻辑 421 11 3 32 2 4 4 112 2 3 3 4 4 { } { }{ } { } { }{ } QS Q QS Q Q QS Q Q Ψ ΨΨ Ψ ΨΨ Ψ Ψ ∧ ∧∧ ∧ ∧∨ ∧ ∧∨ ∧ , 其中,S 表示 PointerC 的程序段.Hoare 逻辑原本没有这样的规则,因为{x==1∨x==2}这样的前条件虽然也可以看成两种不同情况,但 Hoare 逻辑赋值公理可以同时对该析取范式的两个子句进行语法代换. 7) 结构规则(frame rule) 为了获得更有效的推理方法,有时需要拆分或合并合法Ψ.若合法Ψ是S1∧…∧Sn∧N∧D,Ψ1 和Ψ2 分别是 S1∧…∧Si∧N1∧D1 和Si+1∧…∧Sn∧N2∧D2,并且N1∧N2⇔N,D1∧D2⇔D,若Ψ1 对一部分指针类型声明变量来说是合法的,Ψ2 对剩余的指针类型声明变量来说是合法的,则称Ψ可拆分成Ψ1 和Ψ2,Ψ1 和Ψ2 可合并成Ψ.显然,这时有 Ψ⇔Ψ1∧Ψ2.用于局部推理的规则如下: 1 11 1212 1212 { }{ } { }{ } QS Q Q QS Q Q Ψ Ψ ΨΨ ΨΨ ∧ ∧′ ′ ∧∧∧ ∧∧∧ ′ ′ , 其中,Ψ1∧Q1 和Ψ2∧Q2 分别都是合法的. 例如,在函数调用点,Ψ1∧Q1 和Ψ2∧Q2 分别可用来表示和被调用函数有关和无关的部分. 2.4 函数构造的推理规则 PointerC在第 1 节的文法基础上还有函数构造,本节讨论指针逻辑有关函数构造的规则.为突出重点并简化讨论,我们做如下限制或约定: (1) 函数 f 的声明形式是 f(arg){vardeclist stmtlist},arg 是 f 唯一的并且是指针类型的参数,vardeclist 和 stmtlist 是 f 的变量声明表和语句表.函数调用语句的形式是 ret=f(act),act 是实参.在下面的规则中,v1,…,vk 表示函数 f 声明的所有指针类型局部变量; (2) 假定函数体中有一个局部变量 res,它和用户声明的任何局部变量都不同名,函数体中的语句 return e 都变换成 res=e;return res 来进行推理,以使 return 的规则简单. 有了函数构造后,合法Ψ的检查以按作用域规则可见的全局和局部的指针类型声明变量为基础. 下面仅给出参数和返回值都是指针类型的推理规则,其他情况的规则比这些规则简单.递归函数、过程和递归过程的规则都不难在此基础上得出. 1) 函数声明 1 { { ,..., , } } { } { } (arg){ }{ } k v v res Q stmtlist Q Q f vardeclist stmtlist Q Ψ Ψ Ψ Ψ ∧ ∧∧′ ′ ∧ ∧′ ′ D . 在Ψ∧Q 的基础上添加{v1,…,vk,res}D作为函数语句表的前断言,这是因为这些指针类型局部变量和 res 在函数体执行前都被看成悬空指针. 2) 函数调用语句 { {arg} }arg : { } { } (arg){ }{ } . { { } } ( ){( [ } ) ] D Q act Q Q f vardeclist stmtlist Q ret Q ret f act Q res ret Ψ Ψ Ψ Ψ Ψ Ψ 11 11 ∧∧=∧ ∧ ∧′ ′ ∧ ∧= ∧ ← ′ ′ N 参数为指针类型的函数调用必须体现进入被调用函数时,形参和实参在同一个指针集合中,这是通过在该规则的前提中显式增加一个指针赋值语句 arg:=act 来体现的.对于返回值,也可以用类似的方法来解决.在这里是调用前限制 ret 为 NULL 指针,调用后通过代换来使 ret 出现在断言中. 3) return 语句 0 01 1 1 1 1 1 1 00 1 11 1 1 { } { }...{ } { } { } { } { ( { ,..., , }) } k kk k k k k k k k kk Q v NULL Q Q v NULL Q arg NULL Q Q return res v v arg Q Ψ ΨΨ Ψ Ψ Ψ Π −− ++ + + ++ ∧= ∧ ∧ = ∧ = ∧ ∧ ∧ − ∧∧ N D . 函数终止时,指针类型局部变量 v1,…,vk 和形参 arg 不再能访问,因此应把Ψ中有关它们的信息删去. 2.5 指针逻辑的可靠性我们已经完成 PointerC 语言安全性的证明和指针逻辑早先版本对 PointerC 语言操作语义可靠的证明[13], 本文对指针逻辑的完善只影响指针逻辑可靠的证明细节.这里概述指针逻辑可靠的证明框架:

422 Journal of Software 软件学报 Vol.21, No.3, March 2010 (1) 建立基于栈和堆的抽象机器模型,定义 PointerC 语言的操作语义; (2) 给出断言语言在模型上的解释,包括几种访问路径集合的含义.并证明有关访问路径集合的蕴涵和等价公理在该模型上是可靠的; (3) 证明指针逻辑的每条推理规则对该模型及操作语义可靠. 3 证明实例利用 PointerC 语言出具证明编译器的初步实现[12,14],我们证明了单链表、双向链表和二叉树等数据结构的一些函数的安全性或正确性.本节以带头结点的双向循环链表(图 4)的结点插入函数 insert(p,i)的安全性证明为例,展示指针逻辑的应用.其中,p 是链表的指针,i 是插入位置,链表的长度为 n. 该函数对空表和非空表采用统一的代码,但是下面的证明一开始就分成两种情况,然后每种情况又分成两种子情况,这是因为不同情况的访问路径集合不一样,很难用统一的方式来表达它们. (1) 插在表的非尾部(10∧i==n+1). 限于篇幅,下面程序中某些程序点的断言被忽略. 在所列出的断言中,很多地方只给出析取范式的一种情况. {dlist(p,n)∧n>=0∧1r) k ,p(->r) k+1->l}∧{p,p(->r) n+1,p->r->l}∧{q,s}D∧n>=0∧1r; {(∀k:1..j−1.{p(->r) k ,p(->r) k+1->l}∧{q,p(->r) j ,p(->r) j+1->l}∧∀k:j+1..n.{p(->r) k ,p(->r) k+1->l}∧ {p,p(->r) n+1,p->r->l}∧{s}D∧n>=0∧1r) k ,p(->r) k+1->l}∧ {q,p,p(->r) n+1,p->r->l}∧{s}D∧n>=0∧j==n+1)} /*循环不变式,分成 1r; {(∀k:1..j.{p(->r) k ,p(->r) k+1->l}∧{q,p(->r) j+1,(p->r) j+2->l}∧∀k:j+2...n.{p(->r) k ,p(->r) k+1->l}∧ {p,p(->r) n+1,p->r->l}∧{s}D∧n>=0∧1r) k ,p(->r) k+1->l}∧{q,p(->r) j ,(p->r) j+1->l}∧ ∀k:j+1...n.{p(->r) k ,p(->r) k+1->l}∧{p,p(->r) n+1,p->r->l}∧{s}D∧n>=0∧1r) k ,p(->r) k+1->l}∧{q,p(->r) i ,p(->r) i+1->l}∧ ∀k:i+1..n.{p(->r) k ,p(->r) k+1->l}∧{p,p(->r) n+1,p->r->l}∧{s}D∧n>=0∧1r) k ,p(->r) k+1->l}∧{q,p(->r) i ,p(->r) i+1->l}∧∀k:i+1..n.{p(->r) k ,p(->r) k+1->l}∧ {p,p(->r) n+1,p->r->l}∧{s}∧{s->r,s->l}D∧n>=0∧1l=q->l; /*下面仅给出 1r) k ,p(->r) k+1->l}∧{s->l,p(->r) i−1 ,p(->r) i ->l}∧ {q,p(->r) i ,p(->r) i+1->l}∧∀k:i+1..n.{p(->r) k ,p(->r) k+1->l}∧

陈意云等：一种用于指针程序验证的指针逻辑 423 (pp(->r)"p->r->In(s)A{s->r)DN>=OnI1->=S /q->1->r和p(->r)互为别名，于是一些访问路径需要用它们的别名代替/ 【k1.i-2.{p->ryp->r1->l}{s->l,p->r,q->{q,q->r->}n k:itl.n.{q(->r,q(>r）-1>}{p,q(->r-p->r->} (p(->r),s)A(s->r)oNn>=0AI=q 【.v(k:l.i-2.{p->r,p->r）)+1->}A{s->l,p->r,q->}A{s->r,9,9->r->}n ki+1.n.{q(->r)-,q(->r)-1->}A{p,q(->r）-1p->r->}n (p(->r),s)Nn>=0AI1=s, 【vk1.i-2.p(->r）,p->+1->{s->lp->r}{s->r,qqr>r->0} kit1n.{q(->r)-,q(->r）-1->A{p,q->ry-p->r->} ip(->r),g->I.s)Nn>=0AIr'p->r+1>}{p->r)p->r->Ap(->rp(->r2>A kit1.n.p->r）1p(->r）+2>{p,p(->ryt2p->r->}A fp(->r)p(->r)>fg.sivn>=001=0} return p; 如果语句=insert(s,)的前断言是dis1(s,n)A{r}Nw>=OAl=0. 4与分离逻辑的比较指针逻辑和分离逻辑I都是Hoare逻辑的一种扩展，都可用来对使用共享可变数据结构(shared mutable data structure)的命令式程序进行推理.分离逻辑在汇编语言级程序验证中得到广泛应用，但是它不适于对高级语言编写的程序进行推理在分离逻辑中，分离合取断言P*Q中的P和Q分别对可访问存储的不相交部分成立，这导致在与分离逻辑相关联的编程语言中，脱引用(dereference)操作序列不能出现在表达式中，而这样的操作在高级语言程序中经常出现例如，下面的C程序段取自删除单链表元素的函数： s=1->next,1->next=1->next->next,free(s); 其中的表达式1->nex1->nex!关联到两个分离的堆块.分离逻辑没有应用到这种表达式的推理规则.虽然把该程序段变换成s=1->next,=s->nert,->nex=r:free(s;后能被分离逻辑接受.但是若想对一般程序完成这种变换，则需要对程序进行别名分析」分离逻辑的断言语言不太适合于描述带环的数据结构.本文用指针逻辑给出图4双向循环链表的清晰定义.而Reynolds用分离逻辑定义双向循环链表时1，首先引入带4个参数（头结点指针1、尾结点指针s,1->1和 s>)的双向链表段的归纳定义.在该定义中，->1和s>r同表段中其他结点的联系没有定义，以便于规范在表段上的插入和删除操作进一步定义双向循环链表时，还需要加入==>r和==1->1两个断言显然，这种定义双向循环链表的方式不是很直观.另外，在分离逻辑中，二叉树的定义需要借助Ls即语言首先采用的S表达式，在扩展Hoa逻辑时，分离逻辑的策略可以这样理解：所有指针被假定有可能指向同一个对象，除非它们显式地表达为指向不同对象.于是，分离逻辑需要引入像分离合取“*”这样的连接词我们认为，在对指针程序进行推理时，最重要的是掌握每个程序点的有效指针相等信息，基于这些信息可以推导出两条访问路径是否互为别 ©中国科学院软件研究所htp:wwv.c-s-a.org.cm

陈意云等:一种用于指针程序验证的指针逻辑 423 {p,p(->r) n+1,p->r->l}∧{s}∧{s->r}D∧n>=0∧1l->r=s; /*q->l->r 和 p(->r) i 互为别名,于是一些访问路径需要用它们的别名代替*/ {…∨(∀k:1..i−2.{p(->r) k ,p(->r) k+1->l}∧{s->l,p(->r) i−1 ,q->l}∧{q,q->r->l}∧ ∀k:i+1..n.{q(->r) k−i ,q(->r) k−i+1->l}∧{p,q(->r) n−i+1,p->r->l}∧ {p(->r) i ,s}∧{s->r}D∧n>=0∧1r=q; {…∨(∀k:1..i−2.{p(->r) k ,p(->r) k+1->l}∧{s->l,p(->r) i−1 ,q->l}∧{s->r,q,q->r->l}∧ ∀k:i+1..n.{q(->r) k−i ,q(->r) k−i+1->l}∧{p,q(->r) n−i+1,p->r->l}∧ {p(->r) i ,s}∧n>=0∧1l=s; {…∨(∀k:1..i−2.{p(->r) k ,p(->r) k+1->l}∧{s->l,p(->r) i−1 }∧{s->r,q,q->r->l}∧ ∀k:i+1..n.{q(->r) k−i ,q(->r) k−i+1->l}∧{p,q(->r) n−i+1,p->r->l}∧ {p(->r) i ,q->l,s}∧n>=0∧1r) k ,p(->r) k+1->l}∧{p(->r) i−1 ,p(->r) i ->l}∧{p(->r) i+1,p(->r) i+2->l}∧ ∀k:i+1..n.{p(->r) k+1,p(->r) k+2->l}∧{p,p(->r) n+2,p->r->l}∧ {p(->r) i ,p(->r) i+1->l}∧{q,s}N∧n>=0∧1=0} return p; } 如果语句 r=insert(s,j)的前断言是 dlist(s,n)∧{r}N∧n>=0∧1=0. 4 与分离逻辑的比较指针逻辑和分离逻辑[15]都是 Hoare 逻辑的一种扩展,都可用来对使用共享可变数据结构(shared mutable data structure)的命令式程序进行推理.分离逻辑在汇编语言级程序验证中得到广泛应用,但是它不适于对高级语言编写的程序进行推理.在分离逻辑中,分离合取断言 P*Q 中的 P 和 Q 分别对可访问存储的不相交部分成立, 这导致在与分离逻辑相关联的编程语言中,脱引用(dereference)操作序列不能出现在表达式中,而这样的操作在高级语言程序中经常出现.例如,下面的 C 程序段取自删除单链表元素的函数: s=t->next; t->next=t->next->next; free(s); 其中的表达式 t->next->next 关联到两个分离的堆块.分离逻辑没有应用到这种表达式的推理规则.虽然把该程序段变换成 s=t->next;r=s->next;t->next=r;free(s);后能被分离逻辑接受.但是若想对一般程序完成这种变换,则需要对程序进行别名分析. 分离逻辑的断言语言不太适合于描述带环的数据结构.本文用指针逻辑给出图 4 双向循环链表的清晰定义.而 Reynolds 用分离逻辑定义双向循环链表时[15],首先引入带 4 个参数(头结点指针 t、尾结点指针 s,t->l 和 s->r)的双向链表段的归纳定义.在该定义中,t->l 和 s->r 同表段中其他结点的联系没有定义,以便于规范在表段上的插入和删除操作.进一步定义双向循环链表时,还需要加入 t==s->r 和 s==t->l 两个断言.显然,这种定义双向循环链表的方式不是很直观.另外,在分离逻辑中,二叉树的定义需要借助 Lisp 语言首先采用的 S 表达式. 在扩展 Hoare 逻辑时,分离逻辑的策略可以这样理解:所有指针被假定有可能指向同一个对象,除非它们显式地表达为指向不同对象.于是,分离逻辑需要引入像分离合取“*”这样的连接词.我们认为,在对指针程序进行推理时,最重要的是掌握每个程序点的有效指针相等信息,基于这些信息可以推导出两条访问路径是否互为别

424 Journal of Software软件学报Vol.21,No.3,March2010 名，因而可以克服别名给Hoare逻辑带来的困难.我们扩展Hoare逻辑的出发点是，不同的访问路径被认为是代表不同的指针，除非能够证明它们互为别名指针逻辑的推理规则用来从语句前那个程序点的指针信息来推导该语句后那个程序点的指针信息」分离逻辑不像指针逻辑那样能够防止内存泄漏，它的推理规则不能排除会引起内存泄漏的语句通常，内存泄漏是指存在不能被程序访问的并且尚未释放的堆块.例如，下面程序段的前后断言可以用分离逻辑验证1，但是，由于对赋值x:=il采用通常的Hoare逻辑赋值公理，该段程序引起的内存泄漏未被发现 {emp}x=cons(10),{x→l0}x=nil{3x.→10}. 为了解决这个问题，Reynolds等人提出了精确断言(precise assertion)概念l1,但它的定义基于抽象机器，而不是基于断言的语法特征。指针逻辑的最大问题是，其推理规则需要使用一些比语法代换复杂得多的基本运算，使得它难以用于手工验证.若对PointerC语言和断言语言val的语法添加下面两点限制，本质上得到分离逻辑的另一种表示形式.有了这两点限制，指针逻辑的别名计算被大大简化： (I)PointerC的val限制为hval:=idid->id,并且赋值语句的左右两边不同时出现id->id的形式： (2)断言语言的val不使用val(->idp的形式指针逻辑的这种形式区别于分离逻辑之处在于： (1)存在一些高级语言特征：类型化、按域名访问而不是按偏移访问等： (2)断言中采用访问路径集合，而不需要分离合取连接词等. 与分离逻辑比，其优点是： (1)新言演算的规则比分离逻辑的简单清晰； (2)能够验证程序是否会出现内存泄漏， 5相关工作指针逻辑本质上是一种精确指针分析的方法，其不同于一般指针分析方法的显著优点是，它用访问路径集合来表示程序点的指针信息，用Hoa爬风格的推理规则来表示语句引起的指针信息变化.这样，它可用于高级语言程序的Hoare风格程序验证中，采用访问路径集合方式来表示指针信息源于Jonkers用无存储语义(storeless semantics)来抽象内存地址)在无存储语义中，每个动态分配的对象由一组能够到达它的访问路径来表示，整个堆的无存储表示就由所有访问路径集合的一个划分来表示在无存储表示中，互为别名的访问路径出现在同一个集合中近年来，使用无存储语义的研究820仍然采用这种冗余的表示方式.而我们只在访问路径集合中保留互为别名路径中的一条路径，通过推导得到其他访问路径（若需要的话），并且，我们的方法能够较好地表示出像双向循环链表这样带环的数据结构在证明程序性质方面，Bornat也使用Hoare风格来推导指针程序的性质2，把堆看成由指针索引的一群对象，并把每个对象看成由域名索引的一组成员，这样，堆上对象成员的引用对应到两次索引他基于域名相同与否引入了对象成员代换公理，由此扩展了Hoar逻辑的赋值公理，用于证明指针程序的性质在用高阶逻辑系统 Isabelle/HOL2证明指针程序性质时，Mehta和Nipkow采用类似的办法.Marche等人在他们的原型工具 Caduceus2]中也是这样Bornat的方法和我们的方法都可以看成使用两次索引来解决别名，但方式上有较大区别.Bornat所引入的公理和推理规则比较简洁，它们用于逆向的最弱前条件演算中.我们的公理和推理规则不如 Bornat的那么简洁，但是它们以正向方式收集更多的指针信息.与Bornat的方法相比，我们的方法有下列优势： (I)PointerC提供显式的释放堆空间函数fee,指针逻辑用来发现潜在的内存泄漏，但是Bornat的方式只能用在依赖垃圾收集器进行堆管理的场合， (2)我们可以管理带环的数据结构，但Bornat假定数据结构无环； (3)在我们的方式中，数据结构的归纳定义比Bornat的方式简单得多，例如，单链表和二叉树的定义分别 ©中国科学院软件研究所htp:wwv.c-s-a.org.cn

424 Journal of Software 软件学报 Vol.21, No.3, March 2010 名,因而可以克服别名给 Hoare 逻辑带来的困难.我们扩展 Hoare 逻辑的出发点是,不同的访问路径被认为是代表不同的指针,除非能够证明它们互为别名.指针逻辑的推理规则用来从语句前那个程序点的指针信息来推导该语句后那个程序点的指针信息. 分离逻辑不像指针逻辑那样能够防止内存泄漏,它的推理规则不能排除会引起内存泄漏的语句.通常,内存泄漏是指存在不能被程序访问的并且尚未释放的堆块.例如,下面程序段的前后断言可以用分离逻辑验证[16],但是,由于对赋值 x:=nil 采用通常的 Hoare 逻辑赋值公理,该段程序引起的内存泄漏未被发现. {emp} x:=cons(10); {x610} x:=nil {∃x.x610}. 为了解决这个问题,Reynolds 等人提出了精确断言(precise assertion)概念[16],但它的定义基于抽象机器,而不是基于断言的语法特征. 指针逻辑的最大问题是,其推理规则需要使用一些比语法代换复杂得多的基本运算,使得它难以用于手工验证.若对 PointerC 语言和断言语言 lval 的语法添加下面两点限制,本质上得到分离逻辑的另一种表示形式.有了这两点限制,指针逻辑的别名计算被大大简化: (1) PointerC 的 lval 限制为 lval::=id|id->id,并且赋值语句的左右两边不同时出现 id->id 的形式; (2) 断言语言的 lval 不使用 lval(->id) exp 的形式. 指针逻辑的这种形式区别于分离逻辑之处在于: (1) 存在一些高级语言特征:类型化、按域名访问而不是按偏移访问等; (2) 断言中采用访问路径集合,而不需要分离合取连接词等. 与分离逻辑比,其优点是: (1) 断言演算的规则比分离逻辑的简单清晰; (2) 能够验证程序是否会出现内存泄漏. 5 相关工作指针逻辑本质上是一种精确指针分析的方法,其不同于一般指针分析方法的显著优点是,它用访问路径集合来表示程序点的指针信息,用 Hoare 风格的推理规则来表示语句引起的指针信息变化.这样,它可用于高级语言程序的 Hoare 风格程序验证中. 采用访问路径集合方式来表示指针信息源于 Jonkers 用无存储语义(storeless semantics)来抽象内存地址[17].在无存储语义中,每个动态分配的对象由一组能够到达它的访问路径来表示,整个堆的无存储表示就由所有访问路径集合的一个划分来表示.在无存储表示中,互为别名的访问路径出现在同一个集合中.近年来,使用无存储语义的研究[18−20]仍然采用这种冗余的表示方式.而我们只在访问路径集合中保留互为别名路径中的一条路径,通过推导得到其他访问路径(若需要的话).并且,我们的方法能够较好地表示出像双向循环链表这样带环的数据结构. 在证明程序性质方面,Bornat 也使用 Hoare 风格来推导指针程序的性质[21],把堆看成由指针索引的一群对象,并把每个对象看成由域名索引的一组成员,这样,堆上对象成员的引用对应到两次索引.他基于域名相同与否引入了对象成员代换公理,由此扩展了 Hoare 逻辑的赋值公理,用于证明指针程序的性质.在用高阶逻辑系统 Isabelle/HOL[22]证明指针程序性质时,Mehta 和 Nipkow 采用类似的办法.Marché 等人在他们的原型工具 Caduceus[23]中也是这样.Bornat 的方法和我们的方法都可以看成使用两次索引来解决别名,但方式上有较大区别.Bornat 所引入的公理和推理规则比较简洁,它们用于逆向的最弱前条件演算中.我们的公理和推理规则不如 Bornat 的那么简洁,但是它们以正向方式收集更多的指针信息.与 Bornat 的方法相比,我们的方法有下列优势: (1) PointerC 提供显式的释放堆空间函数 free,指针逻辑用来发现潜在的内存泄漏,但是 Bornat 的方式只能用在依赖垃圾收集器进行堆管理的场合; (2) 我们可以管理带环的数据结构,但 Bornat 假定数据结构无环; (3) 在我们的方式中,数据结构的归纳定义比 Bornat 的方式简单得多,例如,单链表和二叉树的定义分别

点击进入文档下载页（PDF格式）

共12页，试读已结束，阅读完整版请下载

点击下载（PDF格式）

浏览记录