处理指针相等关系不确定的指针逻辑 Pointer logic dealing with uncertain equality of pointers

ISSN 1000-9825,CODEN RUXUEW E-mail:jos@iscas.ac.cn Journal of Sofnware,Vol.21,No.2,February 2010,pp.334-343 http://www.jos.org.cn doi:10.3724/SP.J.1001.2010.03783 Tel/Fax:+86-10-62562563 by Institute of Softare,the Chinese Academy of Sciences.All rights reserved. 处理指针相等关系不确定的指针逻辑 梁红瑾，张星5，陈意云中，李光鹏，华保健5 '(中国科学技术大学计算机科学与技术学院，安徽合肥230026) (中因科学技术大学软件学院，安徽合肥230026) (中国科学技术大学苏州研究院软件安全实验室，江苏苏州215123) Pointer Logic Dealing with Uncertain Equality of Pointers LIANG Hong-Jin'3,ZHANG Yu'3,CHEN Yi-Yun'3,LI Zhao-Peng'3.HUA Bao-Jian23 (School of Computer Science and Technology,University of Science and Technology of China,Hefei230026,China) (School of Software Engineering,University of Science and Technology of China,Hefei 230026,China) (Software Security Lab.,Suzhou Institute for Advanced Study,University of Science and Technology of China,Suzhou 215123.China) +Corresponding author:E-mail:Ihj1018@mail.ustc.edu.cn,http://kyhcs.ustcszedu.cn Liang HJ,Zhang Y,Chen YY,Li ZP,Hua BJ.Pointer logic dealing with uncertain equality of pointers. Journal of Sofrware,2010,21(2):334-343.http://www.jos.org.cn/1000-9825/3783.htm Abstract:A pointer logic is designed for a C-like programming language PointerC.The pointer logic is an extension of Hoare logic,and it uses the idea of precise alias analysis in pointer program verification to support safety verification of programs in which equality of pointers is well-regulated.This paper presents an extension to the pointer logic by introducing a set of uncertain-equality pointer access path sets,so as to reason in the extended pointer logic about properties of programs which manipulate data structures like directed graph in which equality of pointers is uncertain. Key words:software safety;Hoare logic;pointer logic 摘要：为类C小语言PointerC设计的指针逻辑是Hoare逻辑的一种扩展，可用来对指针程序进行精确的指针分 析，以支持指针相等关系确定的程序的安全性验证通过增加相等关系不确定的指针类型访问路径集合，可扩展这种 指针逻辑，使得扩展后的指针逻辑可以应用于有向图等指针相等关系不确定的抽象数据结构上的指针程序性质 证明 关键词：软件安全；Hoare逻辑：指针逻辑 中图法分类号：TP311 文献标识码：A 随着软件日益广泛的使用，软件的安全性也日益重要形式程序验证技术为证明程序安全性提供了一种方 法.Hoare逻辑是目前使用广泛的证明命令式语言程序性质的方法，但是Hoare逻辑在处理赋值语句时的代换只 会影响断言中涉及的特定变元虽然可以很容易地扩展它，使它能够确定一些较简单的别名关系，但它很难处理 别名关系复杂的指针程序 Supported by the National Natural Science Foundation of China under Grant Nos.90718026,60928004(国家自然科学基金) Received 2009-06-14;Revised 2009-09-11;Accepted 2009-12-07 ©中国科学院软件研究所http:www.c-s-a.org.cn

ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn Journal of Software, Vol.21, No.2, February 2010, pp.334−343 http://www.jos.org.cn doi: 10.3724/SP.J.1001.2010.03783 Tel/Fax: +86-10-62562563 © by Institute of Software, the Chinese Academy of Sciences. All rights reserved. 处理指针相等关系不确定的指针逻辑∗ 梁红瑾1,3+, 张 昱1,3, 陈意云1,3, 李兆鹏1,3, 华保健2,3 1 (中国科学技术大学 计算机科学与技术学院,安徽 合肥 230026) 2 (中国科学技术大学 软件学院,安徽 合肥 230026) 3 (中国科学技术大学 苏州研究院 软件安全实验室,江苏 苏州 215123) Pointer Logic Dealing with Uncertain Equality of Pointers LIANG Hong-Jin1,3+, ZHANG Yu1,3, CHEN Yi-Yun1,3, LI Zhao-Peng1,3, HUA Bao-Jian2,3 1 (School of Computer Science and Technology, University of Science and Technology of China, Hefei 230026, China) 2 (School of Software Engineering, University of Science and Technology of China, Hefei 230026, China) 3 (Software Security Lab., Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou 215123, China) + Corresponding author: E-mail: lhj1018@mail.ustc.edu.cn, http://kyhcs.ustcsz.edu.cn Liang HJ, Zhang Y, Chen YY, Li ZP, Hua BJ. Pointer logic dealing with uncertain equality of pointers. Journal of Software, 2010,21(2):334−343. http://www.jos.org.cn/1000-9825/3783.htm Abstract: A pointer logic is designed for a C-like programming language PointerC. The pointer logic is an extension of Hoare logic, and it uses the idea of precise alias analysis in pointer program verification to support safety verification of programs in which equality of pointers is well-regulated. This paper presents an extension to the pointer logic by introducing a set of uncertain-equality pointer access path sets, so as to reason in the extended pointer logic about properties of programs which manipulate data structures like directed graph in which equality of pointers is uncertain. Key words: software safety; Hoare logic; pointer logic 摘 要: 为类 C 小语言 PointerC 设计的指针逻辑是 Hoare 逻辑的一种扩展,可用来对指针程序进行精确的指针分 析,以支持指针相等关系确定的程序的安全性验证.通过增加相等关系不确定的指针类型访问路径集合,可扩展这种 指针逻辑,使得扩展后的指针逻辑可以应用于有向图等指针相等关系不确定的抽象数据结构上的指针程序性质 证明. 关键词: 软件安全;Hoare 逻辑;指针逻辑 中图法分类号: TP311 文献标识码: A 随着软件日益广泛的使用,软件的安全性也日益重要.形式程序验证技术为证明程序安全性提供了一种方 法.Hoare 逻辑是目前使用广泛的证明命令式语言程序性质的方法,但是 Hoare 逻辑在处理赋值语句时的代换只 会影响断言中涉及的特定变元.虽然可以很容易地扩展它,使它能够确定一些较简单的别名关系,但它很难处理 别名关系复杂的指针程序. ∗ Supported by the National Natural Science Foundation of China under Grant Nos.90718026, 60928004 (国家自然科学基金) Received 2009-06-14; Revised 2009-09-11;Accepted 2009-12-07

梁红瑾等：处理指针相等关系不确定的指针逻辑 335 分离逻辑四通过扩展Hoare逻辑，证明含有共享易变数据结构(shared mutable data structure,.即这类结构中的 域可以通过指针访问并更新)的命令式程序的性质在分离逻辑中，引入分离合取断言P*Q,使得断言P和Q分别 对堆中不相交的部分成立分离逻辑在汇编语言级程序验证中得到了广泛的应用.但它把堆视为互不影响的若 干部分，而不提供描述它们之间联系的机制」 为了研究指针程序的验证，我们设计了有动态内存分配和回收机制的类C小语言PointerCl四，其基本安全策 略要求程序运行时不出现通过NULL指针或悬空指针(dangling pointer)来存取所指向的对象的操作，不把NULL 指针或悬空指针作为free函数调用的实在参数，不发生内存泄漏等.我们采用一种基于逻辑的技术和基于类型 的技术相结合的方式来推导程序的性质.为使类型系统简单并保证语言的安全性，我们在定型规则(yping rule©) 中增加了约束语法表达式的值的副条件.为了静态检查这些副条件，我们为PointerC语言设计了一种指针逻辑 [3-它是Hoar逻辑的一种拓展，新颖之处是将精确的指针分析应用于程序验证.指针逻辑可用来从前向后收集 各指针是NULL指针、悬空指针还是有效指针(valid pointer,.有指向对象的指针)的信息，收集各有效指针之间相 等与否的信息所收集的信息用来证明指针程序是否满足定型规则的副条件，以支持对指针程序的安全性验证 和其他性质的验证.后来，我们又扩展了指针逻辑，允许有限制的指针算术运算，使得对一维动态数组操作的安 全性验证成为可能我们也完成了PointerC语言安全性和指针逻辑可靠性的证明)，并开发了相应的出具证明 编译器原型plcc,plcc生成携带证明的目标代码. 但是我们原有的指针逻辑只能处理指针相等关系确定的数据结构，如链表、二叉树等，尚不能描述指针相 等关系部分确定或完全不确定的数据结构.例如，有向图中的任意两个指针都可以指向同一个节点，但无法静态 确定是哪些指针同时指向了该节点；而原有的指针逻辑只能精确地收集指针间相等与否的信息，却没有任何机 制描述这种指针相等关系不确定的情况，所以无法支持诸如有向图这样的数据结构.另一方面，原有的指针逻辑 总是需要收集精确的指针相等信息，但是在证明程序性质的过程中常常并不需要如此精确的信息所以有必要 放宽限制，允许所收集的指针信息中存在一部分不确定的指针相等信息因此，我们引入相等关系不确定的一组 访问路径集合，每个这样的集合内的指针都是相等的，但它们还可能与其他这样的集合中的指针相等.放宽限制 带来的问题是，当某个这样的集合只含有1个元素P时，对p赋值可能会（但不是一定会）引起内存泄漏；当释放某 个这样的集合中的指针所指向的对象时，不能保证做到把所有指向该对象的指针都标注为悬空指针，如果程序 中不会出现这些情况，则原有的指针逻辑的规则都可以安全地使用.我们扩展原有的指针逻辑的目的是，当出现 这些情况时给出警告甚至放弃继续验证，而在其他时候则能按照原先的方式进行验证. 本文基于上面的想法对指针逻辑作出扩展，主要贡献如下 (1)在原有的访问路径集合的基础上增加相等关系不确定的访问路径集合，并在断言语言中引入指针不从 属断言的概念使得指针逻辑可以描述指针相等关系不确定的数据结构」 (2)首次将指针逻辑应用于非单一结构的实际程序验证中实际程序所使用的数据结构常常是多种典型数 据结构（如单向链表和双向链表）混合的复杂形态，将指针逻辑应用于这样的程序验证中展现了指针逻 辑的潜力和实用性 本文第1节介绍因引入指针相等关系部分不确定而引起的指针逻辑扩展.第2节给出采用指针逻辑进行程 序验证的两个证明实例.第3节介绍相关工作.第4节是总结」 1指针相等关系不确定的指针逻辑的设计 为了将指针相等关系不确定引入到指针逻辑中，需要引入相等关系不确定的访问路径集合，扩展断言语言 及推理规则，扩展规范语言及推理规则， 1.1 PointerC语言及指针逻辑简介 PointerC是一种强调指针类型的类C小语言，它使用以指针类型声明变量开始的访问路径表示指针.例如， s->r->l是一条长度为2的访问路径，在PointerC中，指针只能用于赋值、相等与否比较、存取指向对象等运算 以及作为函数的参数，指针算术和取地址运算(&)被禁止.malloc和free被看成是PointerC预定义的函数，并且满 ©中国科学院软件研究所 http://www.c-s-a.org.cn

梁红瑾 等:处理指针相等关系不确定的指针逻辑 335 分离逻辑[1]通过扩展Hoare逻辑,证明含有共享易变数据结构(shared mutable data structure,即这类结构中的 域可以通过指针访问并更新)的命令式程序的性质.在分离逻辑中,引入分离合取断言P*Q,使得断言P和Q分别 对堆中不相交的部分成立.分离逻辑在汇编语言级程序验证中得到了广泛的应用,但它把堆视为互不影响的若 干部分,而不提供描述它们之间联系的机制. 为了研究指针程序的验证,我们设计了有动态内存分配和回收机制的类C小语言PointerC[2],其基本安全策 略要求程序运行时不出现通过NULL指针或悬空指针(dangling pointer)来存取所指向的对象的操作,不把NULL 指针或悬空指针作为free函数调用的实在参数,不发生内存泄漏等.我们采用一种基于逻辑的技术和基于类型 的技术相结合的方式来推导程序的性质.为使类型系统简单并保证语言的安全性,我们在定型规则(typing rule) 中增加了约束语法表达式的值的副条件.为了静态检查这些副条件,我们为PointerC语言设计了一种指针逻辑 [3−5].它是Hoare逻辑的一种拓展,新颖之处是将精确的指针分析应用于程序验证.指针逻辑可用来从前向后收集 各指针是NULL指针、悬空指针还是有效指针(valid pointer,有指向对象的指针)的信息,收集各有效指针之间相 等与否的信息.所收集的信息用来证明指针程序是否满足定型规则的副条件,以支持对指针程序的安全性验证 和其他性质的验证.后来,我们又扩展了指针逻辑,允许有限制的指针算术运算,使得对一维动态数组操作的安 全性验证成为可能[6].我们也完成了PointerC语言安全性和指针逻辑可靠性的证明[7],并开发了相应的出具证明 编译器原型plcc[4,8].plcc生成携带证明的目标代码. 但是,我们原有的指针逻辑只能处理指针相等关系确定的数据结构,如链表、二叉树等,尚不能描述指针相 等关系部分确定或完全不确定的数据结构.例如,有向图中的任意两个指针都可以指向同一个节点,但无法静态 确定是哪些指针同时指向了该节点;而原有的指针逻辑只能精确地收集指针间相等与否的信息,却没有任何机 制描述这种指针相等关系不确定的情况,所以无法支持诸如有向图这样的数据结构.另一方面,原有的指针逻辑 总是需要收集精确的指针相等信息,但是在证明程序性质的过程中常常并不需要如此精确的信息.所以有必要 放宽限制,允许所收集的指针信息中存在一部分不确定的指针相等信息.因此,我们引入相等关系不确定的一组 访问路径集合,每个这样的集合内的指针都是相等的,但它们还可能与其他这样的集合中的指针相等.放宽限制 带来的问题是,当某个这样的集合只含有 1 个元素 p 时,对 p 赋值可能会(但不是一定会)引起内存泄漏;当释放某 个这样的集合中的指针所指向的对象时,不能保证做到把所有指向该对象的指针都标注为悬空指针.如果程序 中不会出现这些情况,则原有的指针逻辑的规则都可以安全地使用.我们扩展原有的指针逻辑的目的是,当出现 这些情况时给出警告甚至放弃继续验证,而在其他时候则能按照原先的方式进行验证. 本文基于上面的想法对指针逻辑作出扩展,主要贡献如下: (1) 在原有的访问路径集合的基础上增加相等关系不确定的访问路径集合,并在断言语言中引入指针不从 属断言的概念,使得指针逻辑可以描述指针相等关系不确定的数据结构. (2) 首次将指针逻辑应用于非单一结构的实际程序验证中.实际程序所使用的数据结构常常是多种典型数 据结构(如单向链表和双向链表)混合的复杂形态,将指针逻辑应用于这样的程序验证中展现了指针逻 辑的潜力和实用性. 本文第 1 节介绍因引入指针相等关系部分不确定而引起的指针逻辑扩展.第 2 节给出采用指针逻辑进行程 序验证的两个证明实例.第 3 节介绍相关工作.第 4 节是总结. 1 指针相等关系不确定的指针逻辑的设计 为了将指针相等关系不确定引入到指针逻辑中,需要引入相等关系不确定的访问路径集合,扩展断言语言 及推理规则,扩展规范语言及推理规则. 1.1 PointerC语言及指针逻辑简介 PointerC 是一种强调指针类型的类 C 小语言,它使用以指针类型声明变量开始的访问路径表示指针.例如, s->r->l 是一条长度为 2 的访问路径,在 PointerC 中,指针只能用于赋值、相等与否比较、存取指向对象等运算 以及作为函数的参数;指针算术和取地址运算(&)被禁止.malloc 和 free 被看成是 PointerC 预定义的函数,并且满

336 Journal of Software软件学报Vol.2l,No.2,February2010 足安全程序的最基本要求，例如，malloc任何一次调用都能成功并且所分配空间同尚未释放空间无任何重叠.另 外，PointerC中允许布尔表达式，但不采用短路计算，以方便它们出现在断言中，因为短路的“与”和“或”运算都不 是可交换运算 在原有的为PointerC语言设计的指针逻辑中，使用指针集合表示内存状态.我们设计了3种指针类型访问 路径的集合：表示NULL指针集合的W、表示悬空指针集合的D以及表示一组有效指针集合的7.I中的每个 集合表示在某程序点处一组指向同一个对象的指针（即右值相等的指针类型访问路径），并且，Ⅱ中不同集合的 指针指向不同对象 我们可以用指针逻辑所定义的访问路径集合实现数据结构的归纳定义.例如，二叉树可以如下定义： tree(s)s(siAtree(s->DAtree(s->r)). 其中，s是指向struct BTNode{struct BTNode*r,*l,}类型的指针，{s}w表示空树.另一种情况{s}Aree(s->)A te(s->r)表示非空树，并且表达出该树上的指针都不相等.因为若把归纳定义的引用展开，则代表有效指针的各 访问路径都在的不同集合中 1.2相等关系不确定的访问路径集合 在图等数据结构中，指针相等与否并无规律，即有效指针的相等关系存在不确定的情况.原有的指针逻辑难 以描述这种指针相等关系不确定的数据结构，因此，我们在原有的指针逻辑的基础上增加相等关系不确定的指 针类型访问路径的一组集合，用以表示在语义模型上，以中的每个集合表示在某程序点处一组指向同一个对象 的指针，但是与Ⅱ不同的是，∥中不同集合的指针可能指向同一对象.Ⅱ和∥中各集合内的指针都称为有效指 针.用平作为W,D,Π，∥的总称注意，虽然我们称其为相等关系不确定的访问路径集合，但是所谓的不确定性仅 存在于这种集合之间，而每个集合内的指针都是确定相等的这种做法可以理解为放宽了原先对Ⅱ集合的要求. 并非任意一组指针类型访问路径经随意划分形成的都能表达上面的意思因此，我们需要定义能够描述 数据结构的合法的平.引入∥集合后，需要在原有的合法的定义的基础上，考虑∥中访问路径的特点，如∥中 访问路径以Π或以中的访问路径为前缀等，以及以中的集合与其他集合之间的关系，如Π中访问路径的前缀不 会在∥中等 首先需要扩展访问路径的别名的定义，以处理增加的∥集合.出现在Ⅱ或∥的同一个集合中的各访问路径 加上同一后缀形成的访问路径互为别名按此定义，判断两条访问路径是否互为别名的谓词如下： aliast(p,q)兰p=qv3s.3r.31.(s不是空串r和1属于或∥中的同一集合p=(p's)Aq=(gs)Kalias(p,r)Kalias(g,). 其中，=表示语法上相同，“”表示串并置该定义是说，若p和q不相同，则忽略相同后缀s之后，判断它们的别名是 否出现在Ⅱ或∥中的同一个集合中若递归计算时出现再次判断p和q是否为别名，则计算不终止，这时也认为 p和q不是别名.该谓词和文献[5]中的谓词有不同的表现：由于∥中指针相等关系不确定，∥中不同集合的指针 也可能互为别名因此，该谓词可靠但不完备，不过它不影响下面的合法的定义 扩展后的合法需要满足下面几个条件： (1)所有声明为指针类型的变量都在中 (2)对Ⅱ中的任何访问路径p,若p所指向的结构类型有指针类型域r,则p->r的某个别名在中. (3)对Π，W和D中的任何访问路径，Ⅱ，W和D中的任何其他访问路径都不是它的别名. (4)若访问路径p在中，则对p的每个前缀，它的一个别名在Π或∥中 (⑤)对M中的任何访问路径p,若p所指向的结构类型有指针类型域r,则p->r的某个别名在∥，W或D中 1.3断言语言的扩展 我们在原有的指针逻辑1的断言语言基础上作出扩展，以支持引入从集合.另外，还需要在允许描述两个指 针相等或不相等关系基础上，增加表达∥中的一个指针不从属其他∥集合的断言，以表达己知的∥中不同集合 的指针之间的不相等关系， 扩展后的断言语言如下： ©中国科学院软件研究所 http://www.c-s-a.org.cn

336 Journal of Software 软件学报 Vol.21, No.2, February 2010 足安全程序的最基本要求,例如,malloc 任何一次调用都能成功并且所分配空间同尚未释放空间无任何重叠.另 外,PointerC 中允许布尔表达式,但不采用短路计算,以方便它们出现在断言中,因为短路的“与”和“或”运算都不 是可交换运算. 在原有的为PointerC语言设计的指针逻辑[5]中,使用指针集合表示内存状态.我们设计了 3 种指针类型访问 路径的集合:表示 NULL 指针集合的N 、表示悬空指针集合的D以及表示一组有效指针集合的Π .Π 中的每个 集合表示在某程序点处一组指向同一个对象的指针(即右值相等的指针类型访问路径),并且,Π 中不同集合的 指针指向不同对象. 我们可以用指针逻辑所定义的访问路径集合实现数据结构的归纳定义.例如,二叉树可以如下定义: tree(s){s}N∨({s}∧tree(s->l)∧tree(s->r)), 其中,s是指向struct BTNode{struct BTNode *r,*l;}类型的指针,{s}N表示空树.另一种情况{s}∧tree(s->l)∧ tree(s->r)表示非空树,并且表达出该树上的指针都不相等.因为若把归纳定义的引用展开,则代表有效指针的各 访问路径都在Π的不同集合中. 1.2 相等关系不确定的访问路径集合 在图等数据结构中,指针相等与否并无规律,即有效指针的相等关系存在不确定的情况.原有的指针逻辑难 以描述这种指针相等关系不确定的数据结构,因此,我们在原有的指针逻辑的基础上增加相等关系不确定的指 针类型访问路径的一组集合,用U 表示.在语义模型上,U 中的每个集合表示在某程序点处一组指向同一个对象 的指针,但是与Π 不同的是,U 中不同集合的指针可能指向同一对象.Π 和U 中各集合内的指针都称为有效指 针.用Ψ作为N ,D ,Π ,U 的总称.注意,虽然我们称其为相等关系不确定的访问路径集合,但是所谓的不确定性仅 存在于这种集合之间,而每个集合内的指针都是确定相等的.这种做法可以理解为放宽了原先对Π 集合的要求. 并非任意一组指针类型访问路径经随意划分形成的Ψ都能表达上面的意思.因此,我们需要定义能够描述 数据结构的合法的Ψ.引入U 集合后,需要在原有的合法Ψ的定义[5]的基础上,考虑U 中访问路径的特点,如U 中 访问路径以Π 或U 中的访问路径为前缀等,以及U 中的集合与其他集合之间的关系,如Π 中访问路径的前缀不 会在U 中等. 首先需要扩展访问路径的别名的定义,以处理增加的U 集合.出现在Π 或U 的同一个集合中的各访问路径 加上同一后缀形成的访问路径互为别名.按此定义,判断两条访问路径是否互为别名的谓词如下: alias(p,q)p≡q∨∃s.∃r.∃t.(s 不是空串∧r 和 t 属于Π或U 中的同一集合∧p≡(p′⋅s)∧q≡(q′⋅s)∧alias(p′,r)∧alias(q′,t)). 其中,≡表示语法上相同,“⋅”表示串并置.该定义是说,若 p 和 q 不相同,则忽略相同后缀 s 之后,判断它们的别名是 否出现在Π 或U 中的同一个集合中.若递归计算时出现再次判断 p 和 q 是否为别名,则计算不终止,这时也认为 p 和 q 不是别名.该谓词和文献[5]中的谓词有不同的表现:由于U 中指针相等关系不确定,U 中不同集合的指针 也可能互为别名.因此,该谓词可靠但不完备,不过它不影响下面的合法Ψ的定义. 扩展后的合法Ψ需要满足下面几个条件: (1) 所有声明为指针类型的变量都在Ψ中. (2) 对Π 中的任何访问路径 p,若 p 所指向的结构类型有指针类型域 r,则 p->r 的某个别名在Ψ中. (3) 对Π ,N 和D 中的任何访问路径,Π ,N 和D 中的任何其他访问路径都不是它的别名. (4) 若访问路径 p 在Ψ中,则对 p 的每个前缀,它的一个别名在Π 或U 中. (5) 对U 中的任何访问路径 p,若 p 所指向的结构类型有指针类型域 r,则 p->r 的某个别名在U ,N 或D 中. 1.3 断言语言的扩展 我们在原有的指针逻辑[5]的断言语言基础上作出扩展,以支持引入U 集合.另外,还需要在允许描述两个指 针相等或不相等关系基础上,增加表达U 中的一个指针不从属其他U 集合的断言,以表达已知的U 中不同集合 的指针之间的不相等关系. 扩展后的断言语言如下:

梁红瑾等：处理指针相等关系不确定的指针逻辑 337 assertion::=boolexp-assertion assertionnassertion assertionvassertionident:domain.assertion 3ident:domain.assertion(assertion)ident(Ivalset)lvalsetlvalsetlvalsetp [lvalset lvaleidentIval)lalglvalset domain::=Nexp..exp lvalset::=lvalset,lval lal lval::=ident lval->ident lval(->ident) 其中，boolexp是PointerC语法中的布尔表达式，hval是指针类型访问路径.注意{valset)和新增加的[valset]的区 别，前者表示Π的一个集合，后者表示∥的一个集合，带下标N或D的仍然分别表示W集合和D集合.新增加的 val任ident(valset)和al堡[valset]是指针不从属断言，其中，ident(valset)通常是数据结构形状谓词，如前面定义 的二叉树tree(s)等，可以根据定义加以展开peident(lvalset)的含义是，将iden(valset)展开得到的任意一个访问 路径集合都不含有p的别名p[valset的含义是，lI集合[valset不含有p的别名. 直观上，指针不从属断言是对∥集合的一种限制，它可以部分消除指针关系的不确定性，是沟通∥集合和7 集合的桥梁例如，二叉有向无环图的定义为 dag(p)p)(Ip]ndag(p->I)dag(p->r)pdag(p->I)pdag(p->r)), 其中，{p}v表示空图.另一种情况[p]Adag(p->)Adag(p->r)pdag(p->)pedag(p->r)表示非空图，并且表达出p可 能与其他指针相等，但却不会与p的左右子图内的指针相等.pedag(p->)是指p的别名不在归纳定义dag(p->)所 展开的有效指针集合中.当dag(p->)不是空图时，有 pedag(p->1)-pep->Ipe dag(p->1->I)pedag(p->l->r). 指针不从属新言之前不允许使用一，因为常用数据结构的定义中没有这个需求」 1.4断言演算的扩展 在原有的指针逻辑1中，设计了一些与平有关的逻辑等价或蕴涵公理，包括：1)W和D的等价公理：两个V 集合（或D集合）与合并后的.W集合（或D集合）等价，2)非合法平公理：含有非合法乎的断言为假；3)4等价公理： 当两个合法的对应访问路径集合等价时，合法等价：4)对布尔表达式的吸收或否定：若断言中的布尔表达 式p=NULL,Pl=NULL,p==q和pl=q(p和q都是指针类型)等和y无矛盾则被吸收，有矛盾则整个断言（包括布 尔表达式和为假 在增加了∥集合和指针不从属断言后，这些公理也需要进行相应扩展，如对原先的4)部分： 4)对布尔表达式的吸收或否定 用S1…,S表示构成·的n个访问路径集合，用I,,Tm表示构成/的m个访问路径集合，用Q作为除了平 以外的其他断言的总称记号SP表示访问路径的别名所在的集合，SP9,P,TP9的含义类似注意到，在这部分 规则中，∥集合与Ⅱ集合的地位是平等的.所以，原来关于Π集合的规则]可以几乎原样复制为关于以集 合的规则.下面列举一些这样的蕴涵公理： iA...mPAIIADAp==NULLAO-false TIA...ATIAIIPADAp==NULLAO-TIN...ATIAIIMPADAO TiN...ATmITPAIINADAP!=NULLAO-TIN...ATmITPAIINADAO TI...Tm-ITPAAIINADAP==qNO-Ti...Tm-ITPAAINADAO T1A..ATm-1AP9AΠ入VADNP!-=qAQ=false 此外，针对p的别名与q的别名分属于Ⅱ的集合与∥的集合的情况，需要增加了两条规则 SIA..ASISPATIA...ATm-ITADAp==gnO-false S...SSPATIN...T-TNADApI=qnO-S...ASSPATIN...TmTNADnO ∥集合和不从属断言的特殊性导致还需要为它们增加一些公理.与的别名和g的别名属于不同的Ⅱ集合 的情形不同，当p的别名和q的别名属于不同的M集合时，断言p=q引起它们分处的两个∥集合合并，而这个合 ©中国科学院软件研究所 http://www.c-s-a.org.cn

梁红瑾 等:处理指针相等关系不确定的指针逻辑 337 assertion::=boolexp|¬assertion|assertion∧assertion|assertion∨assertion|∀ident:domain.assertion| ∃ident:domain.assertion|(assertion)|ident(lvalset)|{lvalset}|{lvalset}N|{lvalset}D| [lvalset]|lval∉ident(lval)|lval∉[lvalset] domain::=N|exp..exp lvalset::=lvalset,lval|lval lval::=ident|lval->ident|lval(->ident) exp 其中,boolexp 是 PointerC 语法中的布尔表达式,lval 是指针类型访问路径.注意{lvalset}和新增加的[lvalset]的区 别,前者表示Π 的一个集合,后者表示U 的一个集合,带下标 N 或 D 的仍然分别表示N 集合和D 集合.新增加的 lval∉ident(lvalset)和 lval∉[lvalset]是指针不从属断言.其中,ident(lvalset)通常是数据结构形状谓词,如前面定义 的二叉树 tree(s)等,可以根据定义加以展开.p∉ident(lvalset)的含义是,将 ident(lvalset)展开得到的任意一个访问 路径集合都不含有 p 的别名.p∉[lvalset]的含义是,U 集合[lvalset]不含有 p 的别名. 直观上,指针不从属断言是对U 集合的一种限制,它可以部分消除指针关系的不确定性,是沟通U 集合和Π 集合的桥梁.例如,二叉有向无环图的定义为 dag(p){p}N∨([p]∧dag(p->l)∧dag(p->r)∧p∉dag(p->l)∧p∉dag(p->r)), 其中,{p}N表示空图.另一种情况[p]∧dag(p->l)∧dag(p->r)∧p∉dag(p->l)∧p∉dag(p->r)表示非空图,并且表达出p可 能与其他指针相等,但却不会与p的左右子图内的指针相等.p∉dag(p->l)是指p的别名不在归纳定义dag(p->l)所 展开的有效指针集合中.当dag(p->l)不是空图时,有 p∉dag(p->l)=p∉[p->l]∧p∉dag(p->l->l)∧p∉dag(p->l->r). 指针不从属断言之前不允许使用¬,因为常用数据结构的定义中没有这个需求. 1.4 断言演算的扩展 在原有的指针逻辑[5]中,设计了一些与Ψ有关的逻辑等价或蕴涵公理,包括:1) N 和D 的等价公理:两个N 集合(或D 集合)与合并后的N 集合(或D 集合)等价;2) 非合法Ψ公理:含有非合法Ψ的断言为假;3) Ψ等价公理: 当两个合法Ψ的对应访问路径集合等价时,合法Ψ等价;4) Ψ对布尔表达式的吸收或否定:若断言中的布尔表达 式 p==NULL,p!=NULL,p==q 和 p!=q(p 和 q 都是指针类型)等和Ψ无矛盾则被吸收,有矛盾则整个断言(包括布 尔表达式和Ψ)为假. 在增加了U 集合和指针不从属断言后,这些公理也需要进行相应扩展,如对原先的 4)部分: 4) Ψ对布尔表达式的吸收或否定 用S 1,…,S n表示构成Π 的n个访问路径集合,用T 1,…,T m表示构成U 的m个访问路径集合,用Q作为除了Ψ 以外的其他断言的总称.记号S p 表示访问路径p的别名所在的集合,S p,q ,T p ,T p,q 的含义类似.注意到,在这部分 规则中,U 集合与Π 集合的地位是平等的.所以,原来关于Π 集合的规则[5]可以几乎原样复制为关于U 集 合的规则.下面列举一些这样的蕴涵公理: T 1∧…∧T m−1∧T p ∧Π∧N ∧D∧p==NULL∧Q⇒false T 1∧…∧T m∧Π ∧N p ∧D∧p==NULL∧Q⇒T 1∧…∧T m∧Π ∧N p ∧D∧Q T 1∧…∧T m−1∧T p ∧Π ∧N ∧D∧p!=NULL∧Q⇒T 1∧…∧T m−1∧T p ∧Π ∧N ∧D∧Q T 1∧…∧T m−1∧T p,q ∧Π ∧N ∧D∧p==q∧Q⇒T 1∧…∧T m−1∧T p,q ∧Π ∧N ∧D∧Q T 1∧…∧T m−1∧T p,q ∧Π ∧N ∧D∧p!=q∧Q⇒false 此外,针对 p 的别名与 q 的别名分属于Π 的集合与U 的集合的情况,需要增加了两条规则: S 1∧…∧S n−1∧S p ∧T 1∧…∧T m−1∧T q ∧N∧D∧p==q∧Q⇒false S 1∧…∧S n−1∧S p ∧T 1∧…∧T m−1∧T q ∧N ∧D∧p!=q∧Q⇒S 1∧…∧S n−1∧S p ∧T 1∧…∧T m−1∧T q ∧N ∧D∧Q U 集合和不从属断言的特殊性导致还需要为它们增加一些公理.与 p的别名和 q的别名属于不同的Π 集合 的情形不同,当 p 的别名和 q 的别名属于不同的U 集合时,断言 p==q 引起它们分处的两个U 集合合并,而这个合

338 Journal of Software软件学报Vol.21,No.2.February2010 并会引起以p的别名和q的别名为前缀的访问路径所在集合的继续合并；断言p=q则保证了它们分处的两个∥ 集合的指针一定不相等，可转化为用不从属断言表示.此外，还需要为不从属断言设计专门的等价或蕴涵公理. 下面是其中部分新增公理 5)∥集合合并公理 当断言p==q为真时，引起集合TP和T9合并，包括删除合并后集合中的别名，蕴涵公理如下： TiN..ATm2NTAT9ANADAp-==qNO- T1AATm-2k-2A(TT出T)ATP1A7l入…A7tA7AⅡWnDp->rl=q->rlA.p->rk=g->rkAg 其中，出表示合并两个集合并删除其中的别名，1，，k是所指向对象的指针类型域名.从这里看出，还需要继续 合并T>”和7>”(=1，，k).该合并过程持续到相等的指针出现在D集合中或√集合中为止.限于篇幅，相应规 则略去 6)指针不从属断言的等价公理 pe(assertionlAassertion2peassertionIApeassertion2 p(ident:domain.assertion)ident:domain.(peassertion) pg刀台qeTT台pl=q 7)指针不从属断言对布尔表达式的吸收或否定 TiN...ATm-ITAIINADAp==gnpe TO-false TIN...ATmINTIAIINADApl=gnpe TNO-TIN...ATm-INTIAIIAADAPE TNO 当p被限定为l∥中的某个有效指针时，还可以给出p任{valset,pE{Ivalset;w和pE{Ivalset p等化简至true或 false的蕴涵公理 1.5指针逻辑的规范和推理规则的扩展 我们使用一种Hoare风格的程序规范{PS{Q;,其中：S是程序片段，通常是语句；P和Q分别是它的前、后 条件.用Hoa©逻辑风格的推理规则来表达指针信息的变化就可以把这些信息用于证明程序的性质，同时把程 序分析、类型检查和程序验证联系起来，有更好的表达能力. 在原有的指针逻辑中，我们定义了一些基本运算以表达指针逻辑的推理规则如删除访问路径“-”、增加 访问路径“+”、前缀替换“P”、测试内存泄漏leak(S,p)其中，前缀替换的含义是：对访问路径集合冲以p的别 名为前缀的每条访问路径q,都用q的同一个别名4来代替，q不以p的别名为前缀，R中其余访问路径维持不变 下面所列规则中仍然使用这些基本运算 引入相等关系不确定的访问路径集合后，对内存泄漏的判定引入了不确定性：当访问路径p的别名在Ⅱ中 集合S内，删除p的别名时（出现在对p赋值时），若存在某个集合，其中所有访问路径都是p的别名或以p的别名 为前缀，则会出现内存泄漏；但当p的别名在∥中集合内，删除p的别名时，若存在某个集合，其中所有访问路径 都是p的别名或以p的别名为前缀，则可能会出现内存泄漏，但不是一定会出现，因为可能存在其他M集合的指 针与p指向同一个对象. 下面给出处理指针相等关系不确定的指针逻辑在原先的推理规则上的扩展除了某些情况下难以判断 是否有内存泄漏和难以标注悬空指针以外，这些推理规则与原来的指针逻辑的推理规则类似，因为∥的每个集 合与的每个集合具有相似的特征，只是∥的集合之间存在不确定的指针相等关系， 1)指针类型赋值语句p=q和p=NULL 对于绝大部分情况，原来关于Ⅱ集合的规则问可以几乎原样复制为关于∥集合的规则但是对于以下两种 情况，由于对内存泄漏的判定出现了不确定性，所以需要特别处理： (1)p的别名在Ⅱ或∥的某个集合中，q的别名在W中 S...ASSPAUNDnO)p=q{Silpn...Snpn(SPlp-p)nlllpn(NIptp)nDpnOlp) 即对于赋值前的平，leak(SPp)为假 ©中国科学院软件研究所 http://www.c-s-a.org.cn

338 Journal of Software 软件学报 Vol.21, No.2, February 2010 并会引起以 p 的别名和 q 的别名为前缀的访问路径所在集合的继续合并;断言 p!=q 则保证了它们分处的两个U 集合的指针一定不相等,可转化为用不从属断言表示.此外,还需要为不从属断言设计专门的等价或蕴涵公理. 下面是其中部分新增公理. 5) U 集合合并公理 当断言p==q为真时,引起集合T p 和T q 合并,包括删除合并后集合中的别名,蕴涵公理如下: T 1∧…∧T m−2∧T p ∧T q ∧Π ∧N ∧D∧p==q∧Q⇒ T 1∧…∧T m−2k−2∧(T p ƒT q )∧T p->r1 ∧T q->r1 ∧…∧T p->rk∧T q->rk∧Π ∧N ∧D∧p->r1==q->r1∧…∧p->rk==q->rk∧Q 其中,ƒ表示合并两个集合并删除其中的别名,r1,...,rk是p所指向对象的指针类型域名.从这里看出,还需要继续 合并T p->ri和T q->ri(i=1,...,k).该合并过程持续到相等的指针出现在D集合中或N 集合中为止.限于篇幅,相应规 则略去. 6) 指针不从属断言的等价公理 p∉(assertion1∧assertion2)⇔p∉assertion1∧p∉assertion2 p∉(∀ident:domain.assertion)⇔∀ident:domain.(p∉assertion) p∉T q ⇔q∉T p ⇔p!=q 7) 指针不从属断言对布尔表达式的吸收或否定 T 1∧…∧T m−1∧T q ∧Π ∧N ∧D∧p==q∧p∉T q ∧Q⇒false T 1∧…∧T m−1∧T q ∧Π ∧N ∧D∧p!=q∧p∉T q ∧Q⇒T 1∧…∧T m−1∧T q ∧Π∧N∧D∧p∉T q ∧Q 当p被限定为U 中的某个有效指针时,还可以给出p∉{lvalset},p∉{lvalset}N和p∉{lvalset}D等化简至true或 false的蕴涵公理. 1.5 指针逻辑的规范和推理规则的扩展 我们使用一种 Hoare 风格的程序规范{P}S{Q},其中:S 是程序片段,通常是语句;P 和 Q 分别是它的前、后 条件.用 Hoare 逻辑风格的推理规则来表达指针信息的变化就可以把这些信息用于证明程序的性质,同时把程 序分析、类型检查和程序验证联系起来,有更好的表达能力. 在原有的指针逻辑[5]中,我们定义了一些基本运算以表达指针逻辑的推理规则.如删除访问路径“−”、增加 访问路径“+”、前缀替换“/”、测试内存泄漏 leak(S ,p).其中,前缀替换的含义是:对访问路径集合R中以 p 的别 名为前缀的每条访问路径 q,都用 q 的同一个别名 q′来代替,q′不以 p 的别名为前缀;R中其余访问路径维持不变. 下面所列规则中仍然使用这些基本运算. 引入相等关系不确定的访问路径集合后,对内存泄漏的判定引入了不确定性:当访问路径 p 的别名在Π 中 集合S 内,删除 p 的别名时(出现在对 p 赋值时),若存在某个集合,其中所有访问路径都是 p 的别名或以 p 的别名 为前缀,则会出现内存泄漏;但当 p 的别名在U 中集合T内,删除 p 的别名时,若存在某个集合,其中所有访问路径 都是 p 的别名或以 p 的别名为前缀,则可能会出现内存泄漏,但不是一定会出现,因为可能存在其他U 集合的指 针与 p 指向同一个对象. 下面给出处理指针相等关系不确定的指针逻辑在原先的推理规则[5]上的扩展.除了某些情况下难以判断 是否有内存泄漏和难以标注悬空指针以外,这些推理规则与原来的指针逻辑的推理规则类似,因为U 的每个集 合与Π的每个集合具有相似的特征,只是U 的集合之间存在不确定的指针相等关系. 1) 指针类型赋值语句 p=q 和 p=NULL 对于绝大部分情况,原来关于Π 集合的规则[5]可以几乎原样复制为关于U 集合的规则.但是对于以下两种 情况,由于对内存泄漏的判定出现了不确定性,所以需要特别处理:. (1) p 的别名在Π 或U 的某个集合中,q 的别名在N 中. {S 1∧…∧S n−1∧S p ∧U ∧N q ∧D∧Q}p=q{S 1/p∧…∧S n−1/p∧(S p /p−p)∧U /p∧(N q /p+p)∧D/p∧Q/p} 即对于赋值前的Ψ,leak(S p ,p)为假