一种验证指针程序的方法

随着国家、社会和日常生活对软件系统的依赖程度日益增长，安全攸关软件的高可信成为保障国家安全、保持经济可持续发展和维护社会稳定的必要条件。
　形式验证是提高软件可信程度的重要方法。粗略地说，软件的形式验证有两种途径，第一种是模型检测，它通过遍历系统所有状态空间，能够对有穷状态系统进行自动验证，并自动构造不满足验证性质的反例。这种方法在工业界较流行。第二种是逻辑推理，它利用某种程序逻辑进行演算，对程序性质进行严格的推理，产生验证条件，再利用定理证明器进行证明。本文所讨论的方法是基于逻辑推理的方式。
　对于指针程序的推理，关键在于别名的判断和处理。通常所采用的Hoare逻辑的一个重要限制是程序中不同的名字代表不同的程序对象，即不允许出现别名。
　对于指针别名判断的一种解决办法是采用分离逻辑。使用分离逻辑的一个问题是，通常的自动定理证明器都不能证明带分离合取连接词（*，Separating Conjunction）的验证条件，必须为分离逻辑设计专用的自动定理证明工具。
　本文提出一种利用形状图信息来消除访问路径别名，使得指针程序仍然可以用Hoare逻辑来进行验证的方法。
1 PointerC语言和形状图逻辑
1.1 PointerC语言
　PointerC是一个强调指针类型并增加形状声明的类C小语言，详细的语法信息请见参考文献[1]。在结构体声明中，通过指针域指向形状的声明来确定这种结构体用来构造什么形状的数据结构，同时也限定了该结构体类型的指针所能指向的形状。这是对应形状分析的需求所做的语言扩展，所允许的形状有单链表、循环单链表、双向链表、循环双向链表。
1.2 形状图和形状逻辑
　程序验证之前，首先基于形状图逻辑对程序进行形状分析，形状分析为每个程序点构建形状图，这些形状图构成程序验证所需要的指针信息。在此通过举例来介绍形状图[1]。
　以图1（参考文献[1]中有序链表节点插入函数循环不变式的形状图）为例说明形状图和程序点指针等信息的联系。在图1中，圆节点表示指针类型的声明变量；虚边框的矩形节点不代表任何程序元素；矩形节点表示由malloc生成的结构体变量；灰色矩形节点是浓缩节点，表示若干个（可以是0个）相邻的、属于同一数据结构的、同类型的结构体变量，下侧可以有无代表被浓缩节点个数的整型表达式以及约束该表达式的断言。若没有，则表示被浓缩节点个数是某个自然数，但和任何变量或常数联系不起来。由图1可知，head == ptr1，ptr == ptr1->next，head指向链表的长度是m，ptr指向浓缩节点代表m-1个节点，可用head(->next)m-1上角标的方式来表示。

可见，形状图可以作为程序断言，它是该图所能表达的指针相等、不相等和别名断言等的合取，包括其中谓词节点和浓缩节点下侧有关表长或被浓缩节点个数的整型数据断言。
　　形状图逻辑就是基于上面观点来设计的Hoare逻辑的一种扩展。程序规范的形式是{G∧Q}S{G′∧Q′}，其中G是形状图，Q是表达程序其他性质的符号断言，两部分的合取G∧Q作为程序点完整的断言。本文程序验证器的第一步工作，在无需程序员提供有关形状的函数前后条件和循环不变式的情况下，利用形状图逻辑对程序进行形状分析。由于从一个语句前的G推导该语句后的G′不受Q的影响，因此形状分析时，把程序规范简化为{G}S{G′}，以此来使用形状图逻辑的推理规则，建立各程序点的形状图G。在形状分析的过程中，还利用循环不变式推断算法得出各循环的循环不变形状图[2]。
　在完成形状分析后，程序验证器进行程序其他性质Q的验证。在{G∧Q}S{G′∧Q′}中，若S不是指针操作语句，则G′和G一样，但Q′可能不同于Q。若S是指针操作语句（指针赋值、分配空间和释放空间等），则除了G′和G可能不同外，Q′和Q可能也有一些细微的区别。下面是本文关注的部分。
2 指针程序的验证方法
　程序点数据结构构成的形状有多种可能时，则G表示为G1∨G2∨…∨Gn。同样，Q也可能是Q1∨Q2∨…∨Qm的析取形式。完整的断言可以整理成析取范式（Disjunctive Normal Form）G1∧Q1∨G2∧Q2∨…∨Gk∧Qk的形式。根据形状图逻辑，可以用析取范式的一种情况为例来讨论，写成G∧Q，G和Q分别都是合取形式。
程序验证器基于形状图逻辑[2]进行最强后条件演算并产生验证条件，验证条件由证明器Z3[3]自动证明。
2.1 形状图和符号断言之间的联系
　符号断言Q中允许出现指针是否等于NULL或两个指针是否相等的断言。即使函数前后条件和循环不变式中没有这样的断言，它们也会因为出现在条件语句或循环语句的布尔表达式中，而在最强后条件演算过程中被加到Q中。
　Q中指针等于NULL或两个指针相等的断言会因为和G中的信息重复而被吸收，或因有矛盾而使得G∧Q为假。
　Q中访问路径的合法性依赖于G。例如，在Q中若出现非指针型的访问路径p -> … -> data，则忽略->data所剩下的前缀应该是G上到达某个结构节点的一条访问路径，若是到达悬空节点、null节点或不存在这样的路径则都非法的，若是到达谓词节点则视谓词节点展开后的情况决定。
　Q中的访问路径之间是否有别名，Q中的访问路径和下一条语句S中的访问路径之间,以及S中的访问路径之间是否有别名都依赖于G，即利用G可以判断。
　在指针操作语句中，在对指针u赋值时可能会影响符号断言：符号断言中若有以u或u为前缀的访问路径，则要用和u相等但不是别名的u′来代换u。另一个影响符号断言的场合是，在free语句之后应该删除涉及被释放节点上数据的原子断言。
　G中也会有符号断言，附加在浓缩节点上，用来限制它代表结构节点的个数。G的符号断言和Q的符号断言不会有矛盾，但前者有时会给出更准确的信息。

2.2 程序推理规则的扩展
　在使用推理规则从语句S的前条件G∧Q产生后条件G′∧Q′时，要保证Q合法、Q和G无重复与矛盾。
　先考虑S是指针操作语句。修改指针型数据的简单语句会引起指针值的变化，或者是存储堆块的增减，因而导致形状图的变化。根据2.1节的介绍知道，对Q的影响是访问路径的替换或者删除部分断言。先假定Q和S无别名，有别名的情况在考虑非指针操作语句时介绍。下面给出各种语句规则。
　(1)指针型赋值语句u=v
　若u既不是null指针也不是悬空指针，则按下面规则得到后断言。
　{G∧Q} u = v {G′∧Q[u′/u]}
其中G′是由形状分析得到的形状图，Q[u′/u]表示Q中作为访问路径（包括作为前缀情况）的u和其相等且不互为别名的访问路径u′代换。
　(2)对指针赋值的其他语句
　分配空间语句u=malloc(t)和函数调用语句ret=f(act)有关Q的处理同上面赋值语句的规则一样。
　(3)释放空间语句free(u)
　释放u指向的节点后，Q中含u或u的别名的原子断言不应再存在，因此规则如下：
{G∧Q} free(u) {G′∧Q′}
其中Q′由把Q中含u或u的别名的原子断言都删除而得到。
　很容易明白，若Q无别名，则这些语句的规则不会导致Q′出现别名，因为它们对Q做的小修改都不会引入别名。
　再考虑非指针操作语句。只要前断言Q和语句S中无别名，则使用Hoare的赋值公理就是可靠的。若有别名，则可以先用G的信息来消除别名（把互为别名的访问路径改成都用其中同一条访问路径），然后再用赋值公理。定义eliminate_aliases函数为(S′,Q′)=eliminate_aliases(G, S, Q),它根据G消除S和Q中的别名，得到S′和Q′。
　把Hoare逻辑的赋值公理限定为无别名时才能使用，并增加下面的消除别名推理规则，就可以对含访问路径别名的程序进行推理。
对于修改指针型数据的语句，其前断言Q可能是程序员提供的，例如不排除循环不变式中 Q存在别名，因此有时也需要这条规则。
　复合、条件和循环语句的规则以及推论规则的形式和Hoare逻辑相应规则的形式一致。

3 系统原型
　基于形状图逻辑，实现了PointerC语言的一个程序验证器[1]，它能够验证使用图1所定义的各种形状的程序。除了验证形状外，还能验证节点上数据的一些性质。本文对有序链表插入节点的函数进行了验证。
　该验证器分成下面几个模块，按所列次序顺序执行：
　(1)普通编译器的前端。对源程序进行词法分析、语法分析和静态语义检查后，生成抽象语法树。
　(2)形状分析。遍历抽象语法树，根据形状声明和形状图逻辑来生成各程序点的形状图。
　(3)验证条件的生成。遍历抽象语法树，根据程序员提供的函数前后条件和循环不变式，按最强后条件演算方式为各函数生成验证条件。
　(4)验证条件的证明。将生成的各验证条件G∧Q?圯Q′，按照上一节所介绍的方法翻译成P∧Q?圯Q′的形式，逐个交给证明器进行证明。
本文提出一种利用形状图信息来消除访问路径别名，使得指针程序仍然可以用Hoare逻辑来进行验证的方法，并利用可自动定理证明器的支持，开发了一个PointerC语言的程序验证器原型，展示了该方法的可行性。
参考文献
[1] ZHANG Y, LI Z P, CHEN Y Y, et al. Shape graph logic and A shape system (Extended Verison).URL:http://ssg.ustcsz.edu.cn/content/shape-graph-logic.2010(11).
[2] NECULA G. Proof-carrying code,In Proc.24th ACM Symp.On Principles of Prog.Lang. New York, 1997(1):106-119.
[3] MOURA L D, BJORNER N. Z3: An Efficient SMT solver, conference on tools and algorithms for the construction and analysis of Systems(TACAS). Budapest, Hungary, volume 4963 of LNCS, 2008:337-340.