一种验证指针程序的方法

摘　要: 利用形状图逻辑和形状系统来解决指针程序的分析和验证中的困难。该方法要求程序员声明各种递归结构体类型参与构建的数据结构的形状，并声明指针变量所指向的形状，以便程序分析工具能建立各程序点的形状图，并以此来支持程序验证。探讨了在指针相等关系静态可确定的情况下，避免在Hoare逻辑上做复杂扩展的指针程序验证方法。
关键词: Hoare逻辑; 形状图逻辑; 程序分析; 分离逻辑
       随着国家、社会和日常生活对软件系统的依赖程度日益增长，安全攸关软件的高可信成为保障国家安全、保持经济可持续发展和维护社会稳定的必要条件。
　形式验证是提高软件可信程度的重要方法。粗略地说，软件的形式验证有两种途径，第一种是模型检测，它通过遍历系统所有状态空间，能够对有穷状态系统进行自动验证，并自动构造不满足验证性质的反例。这种方法在工业界较流行。第二种是逻辑推理，它利用某种程序逻辑进行演算，对程序性质进行严格的推理，产生验证条件，再利用定理证明器进行证明。本文所讨论的方法是基于逻辑推理的方式。
　对于指针程序的推理，关键在于别名的判断和处理。通常所采用的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上角标的方式来表示。