梁红瑾等：处理指针相等关系不确定的指针逻辑 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 预定义的函数,并且满