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