《计算机学报》：一种用于指针程序安全性证明的指针逻辑

第31卷第3期 计 算机学报 Vol.31 No.3 2008年3月 CHINESE JOURNAL OF COMPUTERS Mar.2008 一种用于指针程序安全性证明的指针逻辑 陈意云华保健葛 琳王志芳 (中国科学技术大学计算机科学与技术系合肥230026) (中国科学技术大学苏州研究院软件安全实验室江苏苏州215123) 摘要在高可信软件的各种性质中，安全性是被关注的重点，其中软件满足安全策略的证明方法是研究的热点 之一，文中根据作者所设想的安全程序的设计和证明框架，为类C语言的一个子集设计了一个指针逻辑系统.该逻 辑系统是Hoae逻辑系统的一种扩展，它用推理规则来表达每一种语句引起指针信息的变化情况.它可用来对指 针程序进行精确的指针分析，所获得的信息用来证明指针程序是否满足定型规则的附加条件，以支持程序的安全 性验证.该逻辑系统也可用来证明指针程序的其它性质. 关键词软件安全；指针逻辑；Hoare逻辑；指针分析：类型系统 中图法分类号TP301 A Pointer Logic for Safety Verification of Pointer Programs CHEN Yi-Yun HUA Bao-Jian GE Lin WANG Zhi-Fang (Department of Computer Science.University of Science and Technology of China.Hefei 230026) (So ftware Security Laboratory.Suzhou Institute for Advanced Study. University of Science and Technology of China.Suzhou.Jiangsu 215123) Abstract Safety is an important issue among the properties of high-assurance software and de- veloping the verification methods for software to meet safety policies is one of the hot research.In terms of the authors'sketch of design and verification of safety programs,a pointer logic system is designed for a subset of C-like language.This logic system is an extension of Hoare logic sys- tem and inference rules are designed to express the modification of pointer information for every kind of statements.It can be used for accurate pointer analysis of pointer programs.The informa- tion from the analysis can be used to verify if pointer programs satisfy the side conditions of typ- ing rules and then support safety verification for programs.The logic system can also be used to verify other properties of pointer programs. Keywords software safety;pointer logic;Hoare logic;pointer analysis;type system 引起危险、灾难的能力，而security是指软件系统对 引 数据和信息提供保密性、完整性、可用性、真实性保 障的能力.本文所讲的安全性主要是指safety,但是 在高可信的各种要求中，安全性（包括safety和 软件的safety和security是有联系的，黑客通常就 security)是关注的重点.Safety是指软件运行时不 是利用缓冲区溢出、数组访问越界、悬空指针访问等 收稿日期：2006-06-13：最终修改稿收到日期：2007-12-03.本课题得到国家自然科学基金(60673126)资助.陈意云，男，1946年生，教授， 博士生导师，主要研究领域为程序设计语言的理论和实现技术，形式描述技术、软件安全.E-mail:yiyun(@ustc.edu.cm.华保健，男，l979 年生，博士研究生，主要研究方向为程序验证、程序逻辑和软件安全.葛琳，女，19？9年生，博士研究生，主要研究方向为程序验证，软件 安全，类型理论和系统.王志芳，男，1982年生，博士研究生，主要研究方向为软件安全、程序逻辑和程序验证

书 第３１卷 第３期 ２００８年３月 计 算 机 学 报 ＣＨＩＮＥＳＥＪＯＵＲＮＡＬＯＦＣＯＭＰＵＴＥＲＳ Ｖｏｌ．３１ Ｎｏ．３ Ｍａｒ．２００８ 收稿日期：２００６０６１３；最终修改稿收到日期：２００７１２０３．本课题得到国家自然科学基金（６０６７３１２６）资助．陈意云，男，１９４６年生，教授， 博士生导师，主要研究领域为程序设计语言的理论和实现技术、形式描述技术、软件安全．Ｅｍａｉｌ：ｙｉｙｕｎ＠ｕｓｔｃ．ｅｄｕ．ｃｎ．华保健，男，１９７９ 年生，博士研究生，主要研究方向为程序验证、程序逻辑和软件安全．葛 琳，女，１９７９年生，博士研究生，主要研究方向为程序验证、软件 安全、类型理论和系统．王志芳，男，１９８２年生，博士研究生，主要研究方向为软件安全、程序逻辑和程序验证． 一种用于指针程序安全性证明的指针逻辑 陈意云 华保健 葛 琳 王志芳 （中国科学技术大学计算机科学与技术系 合肥 ２３００２６） （中国科学技术大学苏州研究院软件安全实验室 江苏 苏州 ２１５１２３） 摘 要 在高可信软件的各种性质中，安全性是被关注的重点，其中软件满足安全策略的证明方法是研究的热点 之一．文中根据作者所设想的安全程序的设计和证明框架，为类 Ｃ语言的一个子集设计了一个指针逻辑系统．该逻 辑系统是 Ｈｏａｒｅ逻辑系统的一种扩展，它用推理规则来表达每一种语句引起指针信息的变化情况．它可用来对指 针程序进行精确的指针分析，所获得的信息用来证明指针程序是否满足定型规则的附加条件，以支持程序的安全 性验证．该逻辑系统也可用来证明指针程序的其它性质． 关键词 软件安全；指针逻辑；Ｈｏａｒｅ逻辑；指针分析；类型系统 中图法分类号 ＴＰ３０１ 犃犘狅犻狀狋犲狉犔狅犵犻犮犳狅狉犛犪犳犲狋狔犞犲狉犻犳犻犮犪狋犻狅狀狅犳犘狅犻狀狋犲狉犘狉狅犵狉犪犿狊 ＣＨＥＮ ＹｉＹｕｎ ＨＵＡＢａｏＪｉａｎ ＧＥＬｉｎ ＷＡＮＧＺｈｉＦａｎｇ （犇犲狆犪狉狋犿犲狀狋狅犳犆狅犿狆狌狋犲狉犛犮犻犲狀犮犲，犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犎犲犳犲犻 ２３００２６） （犛狅犳狋狑犪狉犲犛犲犮狌狉犻狋狔犔犪犫狅狉犪狋狅狉狔，犛狌狕犺狅狌犐狀狊狋犻狋狌狋犲犳狅狉犃犱狏犪狀犮犲犱犛狋狌犱狔， 犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犛狌狕犺狅狌，犑犻犪狀犵狊狌 ２１５１２３） 犃犫狊狋狉犪犮狋 Ｓａｆｅｔｙｉｓａｎｉｍｐｏｒｔａｎｔｉｓｓｕｅａｍｏｎｇｔｈｅｐｒｏｐｅｒｔｉｅｓｏｆｈｉｇｈａｓｓｕｒａｎｃｅｓｏｆｔｗａｒｅａｎｄｄｅ ｖｅｌｏｐｉｎｇｔｈｅｖｅｒｉｆｉｃａｔｉｏｎｍｅｔｈｏｄｓｆｏｒｓｏｆｔｗａｒｅｔｏｍｅｅｔｓａｆｅｔｙｐｏｌｉｃｉｅｓｉｓｏｎｅｏｆｔｈｅｈｏｔｒｅｓｅａｒｃｈ．Ｉｎ ｔｅｒｍｓｏｆｔｈｅａｕｔｈｏｒｓ′ｓｋｅｔｃｈｏｆｄｅｓｉｇｎａｎｄｖｅｒｉｆｉｃａｔｉｏｎｏｆｓａｆｅｔｙｐｒｏｇｒａｍｓ，ａｐｏｉｎｔｅｒｌｏｇｉｃｓｙｓｔｅｍ ｉｓｄｅｓｉｇｎｅｄｆｏｒａｓｕｂｓｅｔｏｆＣｌｉｋｅｌａｎｇｕａｇｅ．ＴｈｉｓｌｏｇｉｃｓｙｓｔｅｍｉｓａｎｅｘｔｅｎｓｉｏｎｏｆＨｏａｒｅｌｏｇｉｃｓｙｓ ｔｅｍａｎｄｉｎｆｅｒｅｎｃｅｒｕｌｅｓａｒｅｄｅｓｉｇｎｅｄｔｏｅｘｐｒｅｓｓｔｈｅｍｏｄｉｆｉｃａｔｉｏｎｏｆｐｏｉｎｔｅｒｉｎｆｏｒｍａｔｉｏｎｆｏｒｅｖｅｒｙ ｋｉｎｄｏｆｓｔａｔｅｍｅｎｔｓ．Ｉｔｃａｎｂｅｕｓｅｄｆｏｒａｃｃｕｒａｔｅｐｏｉｎｔｅｒａｎａｌｙｓｉｓｏｆｐｏｉｎｔｅｒｐｒｏｇｒａｍｓ．Ｔｈｅｉｎｆｏｒｍａ ｔｉｏｎｆｒｏｍｔｈｅａｎａｌｙｓｉｓｃａｎｂｅｕｓｅｄｔｏｖｅｒｉｆｙｉｆｐｏｉｎｔｅｒｐｒｏｇｒａｍｓｓａｔｉｓｆｙｔｈｅｓｉｄｅｃｏｎｄｉｔｉｏｎｓｏｆｔｙｐ ｉｎｇｒｕｌｅｓａｎｄｔｈｅｎｓｕｐｐｏｒｔｓａｆｅｔｙｖｅｒｉｆｉｃａｔｉｏｎｆｏｒｐｒｏｇｒａｍｓ．Ｔｈｅｌｏｇｉｃｓｙｓｔｅｍｃａｎａｌｓｏｂｅｕｓｅｄｔｏ ｖｅｒｉｆｙｏｔｈｅｒｐｒｏｐｅｒｔｉｅｓｏｆｐｏｉｎｔｅｒｐｒｏｇｒａｍｓ． 犓犲狔狑狅狉犱狊 ｓｏｆｔｗａｒｅｓａｆｅｔｙ；ｐｏｉｎｔｅｒｌｏｇｉｃ；Ｈｏａｒｅｌｏｇｉｃ；ｐｏｉｎｔｅｒａｎａｌｙｓｉｓ；ｔｙｐｅｓｙｓｔｅｍ １ 引 言 在高可信的各种要求中，安全性（包括ｓａｆｅｔｙ和 ｓｅｃｕｒｉｔｙ）是关注的重点．Ｓａｆｅｔｙ是指软件运行时不 引起危险、灾难的能力，而ｓｅｃｕｒｉｔｙ是指软件系统对 数据和信息提供保密性、完整性、可用性、真实性保 障的能力．本文所讲的安全性主要是指ｓａｆｅｔｙ，但是 软件的ｓａｆｅｔｙ和ｓｅｃｕｒｉｔｙ是有联系的，黑客通常就 是利用缓冲区溢出、数组访问越界、悬空指针访问等

3期 陈意云等：一种用于指针程序安全性证明的指针逻辑 373 低级的safety错误，来破坏系统和获取未经授权的 从前向后收集各指针是NULL指针、悬空指针 控制等.因此提高safety有助于保证security. (dangling pointer)还是有效指针（有指向对象的指 程序性质证明（而不是传统的程序正确性证明） 针)的信息，收集各有效指针之间相等与否的信息， 领域近十年来有了很大的发展，许多学者提出了不 所收集信息用来证明指针程序是否满足定型规则 同的思路，这些思路主要采取基于类型的或基于 (typing rule)的附加条件，以支持对指针程序的安 逻辑的方法，用于高级语言程序或低级语言程序 全性验证及其它性质的验证. 的性质证明.基于类型方法的典型研究有类型化 本文第2节介绍有关指针安全的一些基本概 汇编语言(Typed Assembly Language))和类型细 念；第3节是指针逻辑的设计：第4节给出一个证明 化(type refinement)理论[)的研究.基于逻辑方法 实例：第5节是相关工作比较；第6节是总结. 的典型研究有携带证明的代码(Proof-Carrying Code,PCC)t3]FPCC(Foundational Proof-Carrying 2 基本知识 Code)框架[).Shao的携带证明汇编编程项目CAP (Certified Assembly Programming)[)和基于栈的 首先介绍PointerC在指针运算方面的限制.在 CAP(SCAP)[6是典型的基于逻辑的研究项目.基 PointerC中，指针类型的变量只能用于赋值、相等和 于逻辑的方法和基于类型论的方法有很大的互补 不相等比较、存取指向对象等运算以及作为函数（包 性，近年来出现了一些结合这两种方法的研究.一种 括free)的参数，指针算术和取地址运算(&.)被禁 结合两者的研究是Xi等进行的ATS(Applied Type 止，malloc和free被看成是PointerC预定义的函 System)项目的研究[)，他们扩展类型系统，将程序 数，并且满足安全程序的最基本要求.例如malloc 状态引入类型系统，依靠ATS与Hoare逻辑的相 任何一次调用都能成功并且所分配空间与尚未释放 似性，以ATS来编码Hoare逻辑，从而可以在他们 空间无任何重叠. 的类型系统上模拟Hoare逻辑的推理， 上述限制的目的是为了便于静态检查程序的安 基于国际上这些研究，我们认为，对于那些有高 全性.程序运行时出现对NULL指针或悬空指针进 安全性要求的软件，程序设计和证明的一种新方式 行存取指向对象的操作、把NULL指针或悬空指针 将是： 作为free函数调用的实在参数、发生内存泄漏等都 (1)程序设计者将软件的安全策略等描述成程 被认为不满足基本安全策略（类型安全和内存安全 序应满足的规范，连同程序一起提交给编译器； 等).该语言定型规则中的附加条件就是用来禁止这 (2)编译器生成为证明程序满足规范所需的验 些情况的出现，本文指针逻辑的用途之一就是用来 证条件，并且利用内嵌的定理证明器自动地或交互 完成对这些附加条件的静态检查， 地证明这些验证条件； 下面明确本文有关指针类型的一些术语和约 (3)编译器在把源程序翻译成目标代码的同 定，程序中显式声明的变量称为声明变量，由malloc 时，将源程序满足规范的证明翻译成目标代码满足 函数显式和动态分配的空间称为动态对象.在程序 等效规范的证明，这样的编译器称为出具证明的编 中，动态对象的域只能通过指针类型的声明变量来访 译器(certifying compiler); 问，如s>data和s>next->prior等，这种把 (4)在目标代码一级由证明检验器利用代码所 脱引用(dereference)和域访问等组合的语法表达式 携带的证明自动进行代码满足规范的检验： 称为相应声明变量或动态对象域的访问路径，它是一 该框架的优点是，它向程序设计者提供源级而 个语法概念，是变量的名字.注意，若s是NULL指 不是目标级的程序性质证明方法，以提高安全程序 针或悬空指针时，s->next,s->data等在本文中 的开发效率，同时它将编译器、证明器等排除出受信 都不看成访问路径.下面用p,9和r作为代表一般访 任的计算基础(Trusted Computing Base,TCB),以 问路径的元变量，它们最简单的情况就是声明变量的 尽量缩小系统的TCB. 名字.若访问路径p的后面并置一个非空字符串后 本文介绍我们在这个框架的初步实现中，为类 形成访问路径q,则称p是q的前缀.在用此定义 C语言的一个子集PointerC设计的一个指针逻辑 时，需要把p这种语法形式看成p￥的形式.为方便 系统，它是Hoare逻辑的一种扩展，本质上是一种 起见，对访问路径中重复出现的部分使用缩写表示， 精确的指针分析(pointer analysis)工具.它可用来 如s(->next)用来表示s>next一>next…->

低级的ｓａｆｅｔｙ错误，来破坏系统和获取未经授权的 控制等．因此提高ｓａｆｅｔｙ有助于保证ｓｅｃｕｒｉｔｙ． 程序性质证明（而不是传统的程序正确性证明） 领域近十年来有了很大的发展，许多学者提出了不 同的思路，这 些 思 路 主 要 采 取 基 于 类 型 的 或 基 于 逻辑的方法，用 于 高 级 语 言 程 序 或 低 级 语 言 程 序 的性质证明．基 于 类 型 方 法 的 典 型 研 究 有 类 型 化 汇编语言（ＴｙｐｅｄＡｓｓｅｍｂｌｙＬａｎｇｕａｇｅ）［１］和类型细 化（ｔｙｐｅｒｅｆｉｎｅｍｅｎｔ）理论［２］的研究．基于逻辑方法 的典 型 研 究 有 携 带 证 明 的 代 码 （ＰｒｏｏｆＣａｒｒｙｉｎｇ Ｃｏｄｅ，ＰＣＣ）［３］和ＦＰＣＣ（ＦｏｕｎｄａｔｉｏｎａｌＰｒｏｏｆＣａｒｒｙｉｎｇ Ｃｏｄｅ）框架［４］ ．Ｓｈａｏ的携带证明汇编编程项目 ＣＡＰ （ＣｅｒｔｉｆｉｅｄＡｓｓｅｍｂｌｙＰｒｏｇｒａｍｍｉｎｇ）［５］和基于栈的 ＣＡＰ（ＳＣＡＰ）［６］是典型的基于逻辑的研究项目．基 于逻辑的方法和基于类型论的方法有很大的互补 性，近年来出现了一些结合这两种方法的研究．一种 结合两者的研究是Ｘｉ等进行的 ＡＴＳ（ＡｐｐｌｉｅｄＴｙｐｅ Ｓｙｓｔｅｍ）项目的研究［７］，他们扩展类型系统，将程序 状态引入类型系统，依靠 ＡＴＳ与 Ｈｏａｒｅ逻辑的相 似性，以 ＡＴＳ来编码 Ｈｏａｒｅ逻辑，从而可以在他们 的类型系统上模拟 Ｈｏａｒｅ逻辑的推理． 基于国际上这些研究，我们认为，对于那些有高 安全性要求的软件，程序设计和证明的一种新方式 将是： （１）程序设计者将软件的安全策略等描述成程 序应满足的规范，连同程序一起提交给编译器； （２）编译器生成为证明程序满足规范所需的验 证条件，并且利用内嵌的定理证明器自动地或交互 地证明这些验证条件； （３）编译 器 在 把 源 程 序 翻 译 成 目 标 代 码 的 同 时，将源程序满足规范的证明翻译成目标代码满足 等效规范的证明，这样的编译器称为出具证明的编 译器（ｃｅｒｔｉｆｙｉｎｇｃｏｍｐｉｌｅｒ）； （４）在目标代码一级由证明检验器利用代码所 携带的证明自动进行代码满足规范的检验． 该框架的优点是，它向程序设计者提供源级而 不是目标级的程序性质证明方法，以提高安全程序 的开发效率，同时它将编译器、证明器等排除出受信 任的计算基础（ＴｒｕｓｔｅｄＣｏｍｐｕｔｉｎｇＢａｓｅ，ＴＣＢ），以 尽量缩小系统的 ＴＣＢ． 本文介绍我们在这个框架的初步实现中，为类 Ｃ语言的一个子集 ＰｏｉｎｔｅｒＣ 设计的一个指针逻辑 系统，它是 Ｈｏａｒｅ逻辑的一种扩展，本质上是一种 精确的指针分析（ｐｏｉｎｔｅｒａｎａｌｙｓｉｓ）工具．它可用来 从前 向 后 收 集 各 指 针 是 ＮＵＬＬ 指 针、悬 空 指 针 （ｄａｎｇｌｉｎｇｐｏｉｎｔｅｒ）还是有效指针（有指向对象的指 针）的信息，收集各有效指针之间相等与否的信息． 所收集信息用来证明指针程序是否满足定型规则 （ｔｙｐｉｎｇｒｕｌｅ）的附加条件，以支持对指针程序的安 全性验证及其它性质的验证． 本文第２节介绍有关指针安全的一些基本概 念；第３节是指针逻辑的设计；第４节给出一个证明 实例；第５节是相关工作比较；第６节是总结． ２ 基本知识 首先介绍 ＰｏｉｎｔｅｒＣ在指针运算方面的限制．在 ＰｏｉｎｔｅｒＣ中，指针类型的变量只能用于赋值、相等和 不相等比较、存取指向对象等运算以及作为函数（包 括ｆｒｅｅ）的参数，指针算术和取地址运算（＆）被禁 止．ｍａｌｌｏｃ和ｆｒｅｅ被看成是 ＰｏｉｎｔｅｒＣ 预定义的函 数，并且满足安全程序的最基本要求．例如 ｍａｌｌｏｃ 任何一次调用都能成功并且所分配空间与尚未释放 空间无任何重叠． 上述限制的目的是为了便于静态检查程序的安 全性．程序运行时出现对 ＮＵＬＬ指针或悬空指针进 行存取指向对象的操作、把 ＮＵＬＬ指针或悬空指针 作为ｆｒｅｅ函数调用的实在参数、发生内存泄漏等都 被认为不满足基本安全策略（类型安全和内存安全 等）．该语言定型规则中的附加条件就是用来禁止这 些情况的出现，本文指针逻辑的用途之一就是用来 完成对这些附加条件的静态检查． 下面明确本文有关指针类型的一些术语和约 定．程序中显式声明的变量称为声明变量，由 ｍａｌｌｏｃ 函数显式和动态分配的空间称为动态对象．在程序 中，动态对象的域只能通过指针类型的声明变量来访 问，如狊－＞犱犪狋犪 和狊 －＞狀犲狓狋－＞狆狉犻狅狉等，这种把 脱引用（ｄｅｒｅｆｅｒｅｎｃｅ）和域访问等组合的语法表达式 称为相应声明变量或动态对象域的访问路径，它是一 个语法概念，是变量的名字．注意，若狊是 ＮＵＬＬ 指 针或悬空指针时，狊－＞狀犲狓狋，狊－＞犱犪狋犪等在本文中 都不看成访问路径．下面用狆，狇和狉作为代表一般访 问路径的元变量，它们最简单的情况就是声明变量的 名字．若访问路径狆的后面并置一个非空字符串后 形成访问路径狇，则称 狆 是狇 的前缀．在用此定义 时，需要把狆这种语法形式看成狆的形式．为方便 起见，对访问路径中重复出现的部分使用缩写表示， 如狊（－＞狀犲狓狋）犻 用来表示狊 －＞狀犲狓狋－＞狀犲狓狋…－＞ ３ 期 陈意云等：一种用于指针程序安全性证明的指针逻辑 ３７３

374 计算 机学 报 2008年 next(其中>next出现i次)，若i=0,则s(->next)i 形成访问路径，则结果互为别名； 就表示s (3)互为别名的访问路径的值一定相等； 各种类型的指针变量（包括动态对象中的指针 (4)访问路径的别名关系满足自反性、传递性 类型的域)都简称为指针，NULL指针和悬空指针 和对称性 统称为无效指针，有指向对象的指针称为有效指针 在Hoare逻辑的公式{P}S{Q}中，S是语法结 (effective pointer).区分NULL指针和悬空指针是 构，通常是语句，P和Q分别是它的前后条件.下面 由程序通过判断指针是否等于NULL来区别的.访 考虑两种语句，首先是指针类型的赋值语句p=q, 问路径为p和q的两个有效指针相等时，访问路径 Hoare逻辑的正向赋值公理是 *p和*g(或p->next和q>next等)互为别名 {Q}p=q{3p.(p=q[p←p]∧Q[pp'])}, (alias).由于PointerC对指针运算的限制，再加上 其中p'任{p}UFV(q)UFV(Q),FV是得到变元中 函数的参数都是传值方式，一个声明变量的名字不 自由变量集合的函数.考虑p是有效指针的情况， 会和其它变量的名字互为别名（本文没有讨论数组 下面的约束得到满足时才能使用该公理， 元素的动态别名问题)：当两个有效指针的值相等 (1)前条件Q没有p的其它别名（其它别名指 时，在代表它们的访问路径上添加公共后缀后，所得 不是p本身).若不满足，可以尝试用上面提到的基 两条访问路径形成别名，显然，若能掌握有效指针相 本规则把Q变换到满足这个条件， 等与否的信息，就能判断两条访问路径是否互为别 (2)访问路径q也不以p的其它别名为前缀 名并且帮助选择访问路径的别名. (在此对程序加这点限制是为了简化讨论). (3)前条件Q中一定有p==r这样的断言(r 3 指针逻辑的设计 不是p的别名).这是为了保证该赋值不会引起内 存泄漏。 为证明程序满足基本安全策略，除了要为Point- 再考虑为free(p)设计推理规则，这里仅考虑p erC设计一个类型系统外，还需要设计一个证明系 所指向对象不含有效指针这种比较简单的情况.考 统.因为该类型系统的某些定型规则中有附加条件， 虑该规则的前条件和使用该规则的约束： 例如，下标表达式不能越界，s>next必须是一条 (1)p应该是有效指针.它直接出现在该规则的 访问路径等，它们不能由通常的类型系统来检查，本 前条件中 文采用一个证明系统来证明这些附加条件， (2)前条件中没有以p(或与p相等的访问路 我们可通过对Hoare逻辑的扩展来设计这样 径)为前缀的访问路径，除非出现在p>ext== 一个证明系统，因为我们在目标语言级采用CAP方 NULL或p->data==e(e是整型表达式)这样 式.CAP证明目标程序的性质所采用的办法是：把 的断言中， Hoare逻辑的方法直接绑定到目标机器的操作语义 该规则要能体现：前条件中涉及p(包括和p相 上[s-刃.我们在源语言级使用Hoare逻辑方式有助 等的访问路径)的基本断言，在后条件中都被删除 于证明的翻译.该逻辑系统也需要类型系统的支持， 这样的要求难以仅用语法代换来表达。 例如，不同类型的赋值语句需采用不同的推理规则. 例如，若当前程序点的断言是p==aN effec- 我们把Hoare逻辑的这个扩展称为指针逻辑， tive(p)Ap->next==NULL Ap->data== 它的设计基于下面的考虑. 10,下一个语句是free(p),则期望该语句后程序点 由于别名问题，Hoare逻辑不能直接用于有指 的断言是dangling(p)∧langling(q). 针类型的语言，需要对Hoare逻辑的规则增加一些 要想完成上述两种语句中的约束检查和断言删 约束并且需要增加一些规则来解决问题.增加一些 除等，需要寻找新的方式来表达推理规则.指针逻辑 基本规则来表达值相等的访问路径或互为别名的访 的推理规则设计基于下面的考虑： 问路径的性质是简单的，下面是这类性质的一些 (1)若在某程序点能区分有效指针、NULL指 例子： 针和悬空指针，并且知道有效指针之间是否相等，则 (1)值相等的访问路径中，若其中一个代表有 就能判断有关指针的操作是否安全，还可以得出经 效指针，则其它的也都是； 过这步操作后指针信息的变化， (2)给值相等的访问路径添加同样的后缀，若 (2)推理规则的设计要有利于用工具来进行自

狀犲狓狋（其中－＞狀犲狓狋出现犻次），若犻＝０，则狊（－＞狀犲狓狋）犻 就表示狊． 各种类型的指针变量（包括动态对象中的指针 类型的域）都简称为指针，ＮＵＬＬ 指针和悬空指针 统称为无效指针，有指向对象的指针称为有效指针 （ｅｆｆｅｃｔｉｖｅｐｏｉｎｔｅｒ）．区分 ＮＵＬＬ指针和悬空指针是 由程序通过判断指针是否等于 ＮＵＬＬ来区别的．访 问路径为狆和狇 的两个有效指针相等时，访问路径 狆 和 狇（或狆 －＞狀犲狓狋和狇 －＞狀犲狓狋等）互为别名 （ａｌｉａｓ）．由于 ＰｏｉｎｔｅｒＣ 对指针运算的限制，再加上 函数的参数都是传值方式，一个声明变量的名字不 会和其它变量的名字互为别名（本文没有讨论数组 元素的动态别名问题）；当两个有效指针的值相等 时，在代表它们的访问路径上添加公共后缀后，所得 两条访问路径形成别名．显然，若能掌握有效指针相 等与否的信息，就能判断两条访问路径是否互为别 名并且帮助选择访问路径的别名． ３ 指针逻辑的设计 为证明程序满足基本安全策略，除了要为Ｐｏｉｎｔ ｅｒＣ设计一个类型系统外，还需要设计一个证明系 统．因为该类型系统的某些定型规则中有附加条件， 例如，下标表达式不能越界，狊－＞狀犲狓狋必须是一条 访问路径等，它们不能由通常的类型系统来检查，本 文采用一个证明系统来证明这些附加条件． 我们可通过对 Ｈｏａｒｅ逻辑的扩展来设计这样 一个证明系统，因为我们在目标语言级采用 ＣＡＰ方 式．ＣＡＰ证明目标程序的性质所采用的办法是：把 Ｈｏａｒｅ逻辑的方法直接绑定到目标机器的操作语义 上［６７］ ．我们在源语言级使用 Ｈｏａｒｅ逻辑方式有助 于证明的翻译．该逻辑系统也需要类型系统的支持． 例如，不同类型的赋值语句需采用不同的推理规则． 我们把 Ｈｏａｒｅ逻辑的这个扩展称为指针逻辑， 它的设计基于下面的考虑． 由于别名问题，Ｈｏａｒｅ逻辑不能直接用于有指 针类型的语言，需要对 Ｈｏａｒｅ逻辑的规则增加一些 约束并且需要增加一些规则来解决问题．增加一些 基本规则来表达值相等的访问路径或互为别名的访 问路径的 性 质 是 简 单 的，下 面 是 这 类 性 质 的 一 些 例子： （１）值相等的访问路径中，若其中一个代表有 效指针，则其它的也都是； （２）给值相等的访问路径添加同样的后缀，若 形成访问路径，则结果互为别名； （３）互为别名的访问路径的值一定相等； （４）访问路径的别名关系满足自反性、传递性 和对称性． 在 Ｈｏａｒｅ逻辑的公式｛犘｝犛｛犙｝中，犛 是语法结 构，通常是语句，犘 和犙 分别是它的前后条件．下面 考虑两种语句，首先是指针类型的赋值语句狆＝狇， Ｈｏａｒｅ逻辑的正向赋值公理是 ｛犙｝狆＝狇｛狆′．（狆＝狇［狆←狆′］∧犙［狆←狆′］）｝， 其中狆′｛狆｝∪犉犞（狇）∪犉犞（犙），犉犞 是得到变元中 自由变量集合的函数．考虑狆 是有效指针的情况， 下面的约束得到满足时才能使用该公理． （１）前条件 犙 没有狆 的其它别名（其它别名指 不是狆本身）．若不满足，可以尝试用上面提到的基 本规则把犙 变换到满足这个条件． （２）访问路径狇 也不以狆 的 其 它 别 名 为 前 缀 （在此对程序加这点限制是为了简化讨论）． （３）前条件犙 中一定有狆＝＝狉这样的断言（狉 不是狆 的别名）．这是为了保证该赋值不会引起内 存泄漏． 再考虑为犳狉犲犲（狆）设计推理规则，这里仅考虑狆 所指向对象不含有效指针这种比较简单的情况．考 虑该规则的前条件和使用该规则的约束： （１）狆应该是有效指针．它直接出现在该规则的 前条件中． （２）前条件中没有以 狆（或与 狆 相等的访问路 径）为前缀的访问路径，除非出现在狆 －＞狀犲狓狋＝＝ ＮＵＬＬ或狆 －＞犱犪狋犪＝＝犲（犲是整型表达式）这样 的断言中． 该规则要能体现：前条件中涉及狆（包括和狆 相 等的访问路径）的基本断言，在后条件中都被删除． 这样的要求难以仅用语法代换来表达． 例如，若当前程序点的断言是狆＝＝狇∧犲犳犳犲犮 狋犻狏犲（狆）∧狆 －＞狀犲狓狋＝ ＝ ＮＵＬＬ∧狆 －＞犱犪狋犪＝ ＝ １０，下一个语句是犳狉犲犲（狆），则期望该语句后程序点 的断言是犱犪狀犵犾犻狀犵（狆）∧犱犪狀犵犾犻狀犵（狇）． 要想完成上述两种语句中的约束检查和断言删 除等，需要寻找新的方式来表达推理规则．指针逻辑 的推理规则设计基于下面的考虑： （１）若在某程序点能区分有效指针、ＮＵＬＬ 指 针和悬空指针，并且知道有效指针之间是否相等，则 就能判断有关指针的操作是否安全，还可以得出经 过这步操作后指针信息的变化． （２）推理规则的设计要有利于用工具来进行自 ３７４ 计 算 机 学 报 ２００８年

3期 陈意云等：一种用于指针程序安全性证明的指针逻辑 375 动推导. else let s1·s2·…sm-l·sn=pin (3)把相等的指针表达在一个集合中，便于在 com pression(e.r pansion(closure(s·s2·…·sm-i)·sw), 推理规则中表示语句执行所引起的指针信息变化， 其中，length(p)计算访问路径p的长度，它是指p 本文主要介绍证明指针性质的推理规则的 由几个有语法意义的部分组成，而不是指p的字符 设计. 个数，例如t->next->data的长度为3. 3.1基本运算的定义 ex pansion(S)用来在别名集合S中加入与其中 在指针逻辑中，程序点的NULL指针集合用W 访问路径相等的访问路径，其定义如下： 表示，悬空指针的集合用D表示，有效指针集合用Ⅱ expansion(S)△ 表示.Ⅱ中指针的具体值并不重要，重要的是它们是 if 3s':(IUUD)).(sns!=) 否相等，因此基于相等与否把它们划分成若干等价 then let(p1,..p.)=S'-S 集合.例如，若Ⅱ中有等价集合{p,q},则它表示p where S'∈（ⅡU{WU{D})AS∩S'I= 和g是相等的有效指针，并且它们不等于其它集合 in SUclosure(p1)U..Uclosure(p.) 中的指针.一个等价集合不能删掉任何元素，也不能 else☑. 分成若干子集，因为这样做都会使指针信息发生变 compression(S)用来删除别名集合S中带环的 化.因此，在指针逻辑的断言演算中，Ⅱ中的等价集 访问路径，其定义如下： 合被看成命题常元；同样，W和D也都被看成命题常 com pression(S)△S-S 元.这些集合只能用本节为指针赋值等设计的推理 where(S'CS)∧(s1·s2·sa)∈S'iff 规则来改变，在语法结构的前后条件中，Ⅱ中的等价 (s1I=e)∧(s2I=e)八(s3I=e)八 集合、W和D虽以集合方式出现，但本质上是逻辑表 ((s1·s3)∈S)Λ(s1·s2=s1). 达式，因此用“八”连接它们.作为缩写，有时用亚表 为清晰起见，上面给出的是closure的一个定 示ⅡANAD. 义，而不是closure的实现算法，例如，该定义没有考 访问路径是满足一定语法要求的字符串，本文 虑面临双向循环链表等带环数据结构时，递归计算 所说的串都是指构成访问路径的串或子串，并用 的终止问题.在closure的实现中是不难把计算的终 Paths表示访问路径集合.若访问路径p是q的前 止等问题考虑进去的.有了closure函数，也很容易 缀，则谓词prefix(p,q)等于true,否则等于false, 删掉访问路径中的环，为方便讨论，我们认为程序中 符号“·”用于两个串的连接；它也用于串的集合S 给出的都是最简访问路径. 和串s的连接，使得S中的每个串连接s: (2)访问路径的单个别名函数alias(p,q) S·s△S'where s'·s∈S'iff s'∈S 该函数从访问路径p的别名集合中任取p',满 若1·s2和s1(s1和s2都不是空串)是值相等的 足p'不以访问路径q的别名为前缀.若找不到这样 访问路径，则称s2是访问路径s·s2·s(s也不是 的p',则结果仍是p. 空串)中的环.符号=表示语法上等同，==表示语 alias(p,q)△ 法上等同测试. let S=(p':closure(p) 下面先定义访问路径上的一些函数，它们都以 Yq':closure(q).-prefix(g',p')} 程序点的指针信息平或Ⅱ为参数，下面统一都将参 in if S==☑then p else p'where p'∈S. 数忽略.这些定义中出现的关键字在一些软件语言 (3)访问路径所在等价集合函数equals(p) 中都出现过，在此忽略它们的解释.需要强调一下， 若p的别名出现在某个等价集合中，则返回该 访问路径p和q在本文中几乎总是指称指针，因此 集合，否则返回空集。 本文也经常直接称它们为指针：但是，在下面的函数 equals(p)△ 中，使用的是它们的语法表达式（访问路径） if3S:Ⅱ.(S∩closure(p)！=)then (1)别名集合的计算 S where S∈ⅡAS∩closure(p)！=☑ closure(p)计算访问路径p的最简别名集合， else☑. 称为p的闭包，它包含且仅包含p所有的无环别名. 下面介绍在推理规则中直接使用的运算或谓 closure(p)△ 词，这些运算表达语句后条件中的平是如何从前条 if length(p)==1 then (p) 件的亚得到的

动推导． （３）把相等的指针表达在一个集合中，便于在 推理规则中表示语句执行所引起的指针信息变化． 本文 主 要 介 绍 证 明 指 针 性 质 的 推 理 规 则 的 设计． ３１ 基本运算的定义 在指针逻辑中，程序点的 ＮＵＬＬ指针集合用! 表示，悬空指针的集合用"表示，有效指针集合用Π 表示．Π 中指针的具体值并不重要，重要的是它们是 否相等，因此基于相等与否把它们划分成若干等价 集合．例如，若Π 中有等价集合｛狆，狇｝，则它表示狆 和狇 是相等的有效指针，并且它们不等于其它集合 中的指针．一个等价集合不能删掉任何元素，也不能 分成若干子集，因为这样做都会使指针信息发生变 化．因此，在指针逻辑的断言演算中，Π 中的等价集 合被看成命题常元；同样，! 和"也都被看成命题常 元．这些集合只能用本节为指针赋值等设计的推理 规则来改变．在语法结构的前后条件中，Π 中的等价 集合、! 和"虽以集合方式出现，但本质上是逻辑表 达式，因此用“∧”连接它们．作为缩写，有时用 Ψ 表 示Π∧!∧"． 访问路径是满足一定语法要求的字符串，本文 所说的串 都 是 指 构 成 访 问 路 径 的 串 或 子 串，并 用 Ｐａｔｈｓ表示访问路径集合．若访问路径狆 是狇 的前 缀，则谓词狆狉犲犳犻狓（狆，狇）等于ｔｒｕｅ，否则等于ｆａｌｓｅ． 符号“·”用于两个串的连接；它也用于串的集合犛 和串狊的连接，使得犛中的每个串连接狊： 犛·狊犛′ｗｈｅｒｅ狊′·狊∈犛′ｉｆｆ狊′∈犛． 若狊１·狊２和狊１（狊１和狊２都不是空串）是值相等的 访问路径，则称狊２是访问路径狊１·狊２·狊３（狊３也不是 空串）中的环．符号≡表示语法上等同，≡≡ 表示语 法上等同测试． 下面先定义访问路径上的一些函数，它们都以 程序点的指针信息 Ψ 或Π 为参数，下面统一都将参 数忽略．这些定义中出现的关键字在一些软件语言 中都出现过，在此忽略它们的解释．需要强调一下， 访问路径狆和狇 在本文中几乎总是指称指针，因此 本文也经常直接称它们为指针；但是，在下面的函数 中，使用的是它们的语法表达式（访问路径）． （１）别名集合的计算 犮犾狅狊狌狉犲（狆）计算访问路径狆 的最简别名集合， 称为狆的闭包，它包含且仅包含狆所有的无环别名． 犮犾狅狊狌狉犲（狆） ｉｆ犾犲狀犵狋犺（狆）＝＝ １ｔｈｅｎ｛狆｝ ｅｌｓｅｌｅｔ狊１·狊２·…·狊狀－１·狊狀≡狆ｉｎ 犮狅犿狆狉犲狊狊犻狅狀（犲狓狆犪狀狊犻狅狀（犮犾狅狊狌狉犲（狊１·狊２·…·狊狀－１））·狊狀）， 其中，犾犲狀犵狋犺（狆）计算访问路径狆 的长度，它是指狆 由几个有语法意义的部分组成，而不是指狆 的字符 个数，例如狋－＞狀犲狓狋－＞犱犪狋犪的长度为３． 犲狓狆犪狀狊犻狅狀（犛）用来在别名集合犛中加入与其中 访问路径相等的访问路径，其定义如下： 犲狓狆犪狀狊犻狅狀（犛） ｉｆ犛′：（Π∪｛!｝∪｛"｝）．（犛∩犛′！＝） ｔｈｅｎｌｅｔ｛狆１，…，狆狀｝＝犛′－犛 ｗｈｅｒｅ犛′∈（Π∪｛!｝∪｛"｝）∧犛∩犛′！＝ ｉｎ犛∪犮犾狅狊狌狉犲（狆１）∪…∪犮犾狅狊狌狉犲（狆狀） ｅｌｓｅ． 犮狅犿狆狉犲狊狊犻狅狀（犛）用来删除别名集合犛 中带环的 访问路径，其定义如下： 犮狅犿狆狉犲狊狊犻狅狀（犛）犛－犛′ ｗｈｅｒｅ（犛′犛）∧（（狊１·狊２·狊３）∈犛′ｉｆｆ （狊１！＝ε）∧（狊２！＝ε）∧（狊３！＝ε）∧ （（狊１·狊３）∈犛）∧（狊１·狊２＝狊１））． 为清晰起见，上面给出的是ｃｌｏｓｕｒｅ的一个定 义，而不是ｃｌｏｓｕｒｅ的实现算法，例如，该定义没有考 虑面临双向循环链表等带环数据结构时，递归计算 的终止问题．在ｃｌｏｓｕｒｅ的实现中是不难把计算的终 止等问题考虑进去的．有了ｃｌｏｓｕｒｅ函数，也很容易 删掉访问路径中的环，为方便讨论，我们认为程序中 给出的都是最简访问路径． （２）访问路径的单个别名函数犪犾犻犪狊（狆，狇） 该函数从访问路径狆的别名集合中任取狆′，满 足狆′不以访问路径狇 的别名为前缀．若找不到这样 的狆′，则结果仍是狆． 犪犾犻犪狊（狆，狇） ｌｅｔ犛＝｛狆′：犮犾狅狊狌狉犲（狆）｜ 狇′：犮犾狅狊狌狉犲（狇）．狆狉犲犳犻狓（狇′，狆′）｝ ｉｎｉｆ犛＝＝ｔｈｅｎ狆ｅｌｓｅ狆′ｗｈｅｒｅ狆′∈犛． （３）访问路径所在等价集合函数犲狇狌犪犾狊（狆） 若狆的别名出现在某个等价集合中，则返回该 集合，否则返回空集． 犲狇狌犪犾狊（狆） ｉｆ犛：Π．（犛∩犮犾狅狊狌狉犲（狆）！＝）ｔｈｅｎ 犛 ｗｈｅｒｅ犛∈Π∧犛∩犮犾狅狊狌狉犲（狆）！＝ ｅｌｓｅ． 下面介绍在推理规则中直接使用的运算或谓 词，这些运算表达语句后条件中的 Ψ 是如何从前条 件的Ψ 得到的． ３ 期 陈意云等：一种用于指针程序安全性证明的指针逻辑 ３７５

376 计算 机 学 报 2008年 (4)有效指针的替换和删除运算 -把q加到Ⅱ中p所在的等价集合. 若S是Ⅱ的一个等价集合，p是一个有效指 (8)有效指针删除是否引起内存泄漏的测试 针，则S/p表示对S中以p的别名为前缀的每个指 leak(p) 针q都用alias(q,p)寻找一个别名来代替它，然后 对有效指针p所在等价集合S进行S/p计算， 将S中出现的p的别名和以它们为前缀的访问路 结果为空集合时则表示会出现内存泄漏；否则不会， 径都删除. leak(p)△equals(p)/p==⑦. S/p△ (9)一些基本谓词的定义 let S'=(q:SI Yp':closure(p).-prefix(p', 下面这些谓词用来测试指针p的别名是否在 q))U(g':Paths|3q:S.3p':closure(p). 某个集合中 (prefix(p',q)∧ p<:Ⅱ△3S:Ⅱ.(S∩closure(p)！=0)； alias(q,p))) p<:S△S∩closure(p)！=⑦ in{q:S'l一(q∈closure(p))A (S是Ⅱ中的一个等价集合)： Yp':closure(p).-prefix(p',q)). p<:W≌(W∩closure(p))I=; 若需要对Ⅱ中每个S进行替换和删除p的运 p<:D△(D∩closure(p)I=; 算，则用Ⅱ/p表示. p<:平亚≌(p<:Ⅱ)V(p<:W)V(p<:D). 当有效指针q被赋予一个不等于q的值时，q 3.2断言演算 和以q为前缀的访问路径都需要从原来的等价集合 把指针集合看成常元，断言上的演算基本上仍 中删除，例如，若Ⅱ={s,t->prior},{t,s> 遵守经典逻辑的演算，只是对于指针集合，不能使用 next},则Ⅱ/t={{s,s->next->prior},{s-> AAB→A和A∧B→B,因为这会丢失指针信息. next}〉. 另外，对指针集合需要引入一些专用的规则，受 (5)无效指针替换运算 篇幅限制，在此只列举部分规则。 W\p和D列p分别用来表示将N和D中以p的 (1)判断Ψ是否有矛盾 别名为前缀的访问路径用它们的其它别名来代替 例如，下面的规则表示一个有效指针不能同时 W\△ 出现在两个不同的等价集合中。 (q:NI Yp':closure(p).-prefix(p',q))U 3p:Paths..3S1:Ⅱ.3S2:Ⅱ. q':Pathsl3q:N.3p':closure(p).(prefix(p', (p<:S)∧(p<:S2)A(S!=S2) →false q）Aq'==alias(q,p)}. D八p的定义类似， (2)吸收指针相等关系断言 (6)无效指针删除运算 在PointerC的程序中，条件语句和循环语句的 NIp和D/p分别用来表示将N和D中出现的p 规则会把p==NULL和p==q等形式的断言分 的别名副除。 别引入两条件分支和循环体前程序点的断言中.需 要一些规则来把它们吸收到指针集合中或者推导出 Wlp△{q:W|7(q∈closure(p))}: 矛盾，下面列出其中的一部分： N/八p1,p2,…,p.}△(N/p1)/p2)…/pn). (p<:Ⅱ) D/p的定义类似， (7)指针添加运算 业A(p!=NULL)→业 (p<:W) 并集算符“U”直接用来表示向指针集合中添加 ΨA(p！=NULL)→false 一个指针，例如SU{p}.我们为Ⅱ中等价集合的增 <:N 加、剔除和替换使用新的记号，它们基于集合运算符 业A(p==NULL)→亚： 号“U”和“一”及它们的组合来定义。 p<:Ⅱ Ⅱ+p△ΠU{{p}} Ψ∧(p==NULL)→false 一把仅由p构成的等价集合加到Ⅱ中； (3)别名替换 Ⅱ-p△Ⅱ-{equals(p)} 有时需要用下面的规则来进行别名替换： 一删掉Ⅱ中p所在的等价集合； q∈closure(p) Ⅱadd g to p△（Ⅱ-p)U{equals(p)U{q}} Ψ∧Q→Ψ∧Q[p←-q]

（４）有效指针的替换和删除运算 若犛 是Π 的一个 等 价 集 合，狆 是 一 个 有 效 指 针，则犛／狆表示对犛 中以狆 的别名为前缀的每个指 针狇都用犪犾犻犪狊（狇，狆）寻找一个别名来代替它，然后 将犛 中出现的狆 的别名和以它们为前缀的访问路 径都删除． 犛／狆  ｌｅｔ犛′＝｛狇：犛｜狆′：犮犾狅狊狌狉犲（狆）．狆狉犲犳犻狓（狆′， 狇）｝∪｛狇′：犘犪狋犺狊｜狇：犛．狆′：犮犾狅狊狌狉犲（狆）． （狆狉犲犳犻狓（狆′，狇）∧ 狇′≡≡犪犾犻犪狊（狇，狆））｝ ｉｎ｛狇：犛′｜（狇∈犮犾狅狊狌狉犲（狆））∧ 狆′：犮犾狅狊狌狉犲（狆）．狆狉犲犳犻狓（狆′，狇）｝． 若需要对Π 中每个犛 进行替换和删除狆 的运 算，则用Π／狆表示． 当有效指针狇被赋予一个不等于狇 的值时，狇 和以狇 为前缀的访问路径都需要从原来的等价集合 中删 除，例 如，若 Π＝ ｛｛狊，狋 －＞狆狉犻狅狉｝，｛狋，狊 －＞ 狀犲狓狋｝｝，则 Π／狋＝｛｛狊，狊－＞狀犲狓狋－＞狆狉犻狅狉｝，｛狊－＞ 狀犲狓狋｝｝． （５）无效指针替换运算 !＼狆 和"＼狆 分别用来表示将! 和"中以狆 的 别名为前缀的访问路径用它们的其它别名来代替． !＼狆 ｛狇：!｜狆′：犮犾狅狊狌狉犲（狆）．狆狉犲犳犻狓（狆′，狇）｝∪ ｛狇′：犘犪狋犺狊｜狇：!．狆′：犮犾狅狊狌狉犲（狆）．（狆狉犲犳犻狓（狆′， 狇）∧狇′≡≡犪犾犻犪狊（狇，狆））｝． "＼狆的定义类似． （６）无效指针删除运算 !／狆和"／狆分别用来表示将! 和"中出现的狆 的别名删除． !／狆｛狇：!｜（狇∈犮犾狅狊狌狉犲（狆））｝； !／｛狆１，狆２，…，狆狀｝（（（!／狆１）／狆２）…／狆狀）． "／狆的定义类似． （７）指针添加运算 并集算符“∪”直接用来表示向指针集合中添加 一个指针，例如犛∪｛狆｝．我们为Π 中等价集合的增 加、删除和替换使用新的记号，它们基于集合运算符 号“∪”和“－”及它们的组合来定义． Π＋狆Π∪｛｛狆｝｝ ———把仅由狆构成的等价集合加到Π 中； Π－狆Π－｛犲狇狌犪犾狊（狆）｝ ———删掉Π 中狆 所在的等价集合； Πａｄｄ狇ｔｏ狆（Π－狆）∪｛犲狇狌犪犾狊（狆）∪｛狇｝｝ ———把狇加到Π 中狆 所在的等价集合． （８）有效 指 针 删 除 是 否 引 起 内 存 泄 漏 的 测 试 犾犲犪犽（狆） 对有效指针狆所在等价集合犛 进行犛／狆 计算， 结果为空集合时则表示会出现内存泄漏；否则不会． 犾犲犪犽（狆）犲狇狌犪犾狊（狆）／狆＝＝． （９）一些基本谓词的定义 下面这些谓词用来测试指针狆 的别名是否在 某个集合中． 狆＜：Π犛：Π．（犛∩犮犾狅狊狌狉犲（狆）！＝）； 狆＜：犛犛∩犮犾狅狊狌狉犲（狆）！＝ （犛是Π 中的一个等价集合）； 狆＜：!（! ∩犮犾狅狊狌狉犲（狆））！＝； 狆＜："（"∩犮犾狅狊狌狉犲（狆））！＝； 狆＜：Ψ（狆＜：Π）∨（狆＜：! ）∨（狆＜："）． ３２ 断言演算 把指针集合看成常元，断言上的演算基本上仍 遵守经典逻辑的演算，只是对于指针集合，不能使用 犃∧犅犃 和犃∧犅犅，因为这会丢失指针信息． 另外，对指针集合需要引入一些专用的规则，受 篇幅限制，在此只列举部分规则． （１）判断 Ψ 是否有矛盾 例如，下面的规则表示一个有效指针不能同时 出现在两个不同的等价集合中． 狆：犘犪狋犺狊．犛１：Π．犛２：Π． （（狆＜：犛１）∧（狆＜：犛２）∧（犛１！＝犛２）） Ψｆａｌｓｅ ． （２）吸收指针相等关系断言 在 ＰｏｉｎｔｅｒＣ的程序中，条件语句和循环语句的 规则会把狆＝＝ＮＵＬＬ 和狆＝＝狇等形式的断言分 别引入两条件分支和循环体前程序点的断言中．需 要一些规则来把它们吸收到指针集合中或者推导出 矛盾，下面列出其中的一部分： （狆＜：Π） Ψ∧（狆！＝ＮＵＬＬ）Ψ ； （狆＜：! ） Ψ∧（狆！＝ＮＵＬＬ）ｆａｌｓｅ； 狆＜：! Ψ∧（狆＝＝ＮＵＬＬ）Ψ ； 狆＜：Π Ψ∧（狆＝＝ＮＵＬＬ）ｆａｌｓｅ． （３）别名替换 有时需要用下面的规则来进行别名替换： 狇∈犮犾狅狊狌狉犲（狆） Ψ∧犙 Ψ∧犙［狆←狇］． ３７６ 计 算 机 学 报 ２００８年