第39卷第12期 计 算机 学报 Vol.39 No.12 2016年12月 CHINESE JOURNAL OF COMPUTERS Dec,2016 形状图理论的定理证明 张昱陈意云李兆鹏 (中国科学技术大学计算机科学与技术学院合肥230026) (中国科学技术大学苏州研究院软件安全实验室江苏苏州215123) 摘要验证操作易变数据结构的指针程序仍面临很多挑战.数据结构中严重的指针别名显著地复杂化对操作这 些结构的程序的推理.为分析和验证操作易变数据结构的指针程序，文中提出了形状图逻辑.形状图是描述程序中 静态声明的堆指针变量和动态分配的结构体中指针域变量的指向的一种有向图，能准确表达指针的有效性和指针 之间的相等性，可用于判断两个访问表达式是否是别名.形状图逻辑是Hoa©逻辑的一种扩展，是一种直接将形状 图作为程序中指针断言集的程序逻辑.该文研究形状图的等价理论和蕴含理论以及它们的判定方法和应用.首先， 把形状图及其等价规则和蕴含规则分别类比为代数项及其等式规则和重写规则，像研究代数规范的理论那样来研 究形状图理论.该文定义了形状图的语法理论和语义理论，定义了形状图重写系统及其终止性、局部合流性和合流 性，然后得到基于形状图重写的形状图等价判定和蕴含判定的方法.其次，提出循环不变形状图和递归函数前后形 状图的自动推断方法，借助形状图理论的判定方法，该文把一个基于抽象解释的推断循环不变式的一般方法改编 成推断循环不变形状图的方法，由于计算终止的递归函数总有非递归的出口，可以先通过非递归路径得到函数的 后形状图的初值，然后再在递归路径上迭代求解.从而，可以像推断循环不变形状图那样来推断递归函数的前后形 状图.第三，参照Nelson-Oppen框架，提出形状图理论和整数理论组合的一种判定方法.对易变数据结构，除了关 心数据结构各节点是否连成预定的形状外，往往还关心数据在这些节点间的排列等特性，它们不能脱离易变数据 结构的形状特征而单独验证.为此，所提出的组合判定方法针对这类程序的验证条件的特点，利用程序分析阶段得 到的形状图对验证条件的前件中的符号断言按形状图的节点分组：然后运用整数理论为各节点推导出尽可能多的 性质：最后才交由定理证明器Z3去自动验证.这种方式有效地避免验证条件证明过程的不终止.基于形状图逻辑 以及文中的工作，我们所开发的程序验证系统原型减轻了自动定理证明器的负担，并且能验证易变数据结构上较 为复杂的程序，如有序循环双向链表、二叉排序树、伸展树、树堆、二叉平衡树和AA树的插入和删除函数 关键词形状图逻辑；形状分析：程序验证：自动定理证明：循环不变式的推断 中图法分类号TP311 D0I号10.11897/SP.J.1016.2016.02460 Theorem Proving for a Theory of Shape Graphs ZHANG Yu CHEN Yi-Yun LI Zhao-Peng (School of Computer Science and Technology,University of Science and Technology of China.Hefei 230026) (Softuure Security Laboratory.Suzhou Institute for Adwanced Study.University of Science and Technology of China.Suzhou.Jiangsu 215123) Abstract Programs manipulating mutable data structures present a challenge for verification. Deep aliasing inside data structures dramatically complicates reasoning statements manipulating these structures.To analyze and verify programs manipulating mutable data structures,we proposed the shape graph logic.Shape graphs describe point-to relations of statically declared heap pointer variables and pointer fields of heap objects.They precisely express the validity of pointers and the equalities between pointers,and can be used to judge whether two access expressions 收稿日期：2014-11-14：在线出版日期：2015-05-29.本课题得到国家“八六三”高技术研究发展计划项目基金(2012AA010901)、国家自然 科学基金(61170018,61229201)资助.张昱，女，1972生，博士，副教授，中国计算机学会(CCF)高级会员，主要研究方向为程序设计语 言的理论和实现技术、程序验证、确定性并行编程模型与运行时系统.E-mail:yuzhangt@ustc.edu.cn.陈意云，男，l946年生，教授，博士 生导师，中国计算机学会(CC℉)高级会员，主要研究领域为程序设计语言的理论和实现技术，程序验证、软件安全等.李兆鹏，男，1978年 生，博士，副研究员，中国计算机学会(CC℉)会员，主要研究方向为程序语言、程序验证、出具证明的编译器、自动定理证明.书 第３９卷第１２期 ２０１６年１２月 计 算 机 学 报 ＣＨＩＮＥＳＥＪＯＵＲＮＡＬＯＦＣＯＭＰＵＴＥＲＳ Ｖｏｌ．３９Ｎｏ．１２ Ｄｅｃ．２０１６ 收稿日期：２０１４１１１４；在线出版日期：２０１５０５２９．本课题得到国家“八六三”高技术研究发展计划项目基金（２０１２ＡＡ０１０９０１）、国家自然 科学基金（６１１７００１８，６１２２９２０１）资助．张昱，女，１９７２生，博士，副教授，中国计算机学会（ＣＣＦ）高级会员，主要研究方向为程序设计语 言的理论和实现技术、程序验证、确定性并行编程模型与运行时系统．Ｅｍａｉｌ：ｙｕｚｈａｎｇ＠ｕｓｔｃ．ｅｄｕ．ｃｎ．陈意云，男，１９４６年生，教授，博士 生导师，中国计算机学会（ＣＣＦ）高级会员，主要研究领域为程序设计语言的理论和实现技术、程序验证、软件安全等．李兆鹏，男，１９７８年 生，博士，副研究员，中国计算机学会（ＣＣＦ）会员，主要研究方向为程序语言、程序验证、出具证明的编译器、自动定理证明． 形状图理论的定理证明 张昱陈意云李兆鹏 （中国科学技术大学计算机科学与技术学院合肥２３００２６） （中国科学技术大学苏州研究院软件安全实验室江苏苏州２１５１２３） 摘要验证操作易变数据结构的指针程序仍面临很多挑战．数据结构中严重的指针别名显著地复杂化对操作这 些结构的程序的推理．为分析和验证操作易变数据结构的指针程序，文中提出了形状图逻辑．形状图是描述程序中 静态声明的堆指针变量和动态分配的结构体中指针域变量的指向的一种有向图，能准确表达指针的有效性和指针 之间的相等性，可用于判断两个访问表达式是否是别名．形状图逻辑是Ｈｏａｒｅ逻辑的一种扩展，是一种直接将形状 图作为程序中指针断言集的程序逻辑．该文研究形状图的等价理论和蕴含理论以及它们的判定方法和应用．首先， 把形状图及其等价规则和蕴含规则分别类比为代数项及其等式规则和重写规则，像研究代数规范的理论那样来研 究形状图理论．该文定义了形状图的语法理论和语义理论，定义了形状图重写系统及其终止性、局部合流性和合流 性，然后得到基于形状图重写的形状图等价判定和蕴含判定的方法．其次，提出循环不变形状图和递归函数前后形 状图的自动推断方法．借助形状图理论的判定方法，该文把一个基于抽象解释的推断循环不变式的一般方法改编 成推断循环不变形状图的方法．由于计算终止的递归函数总有非递归的出口，可以先通过非递归路径得到函数的 后形状图的初值，然后再在递归路径上迭代求解．从而，可以像推断循环不变形状图那样来推断递归函数的前后形 状图．第三，参照ＮｅｌｓｏｎＯｐｐｅｎ框架，提出形状图理论和整数理论组合的一种判定方法．对易变数据结构，除了关 心数据结构各节点是否连成预定的形状外，往往还关心数据在这些节点间的排列等特性，它们不能脱离易变数据 结构的形状特征而单独验证．为此，所提出的组合判定方法针对这类程序的验证条件的特点，利用程序分析阶段得 到的形状图对验证条件的前件中的符号断言按形状图的节点分组；然后运用整数理论为各节点推导出尽可能多的 性质；最后才交由定理证明器Ｚ３去自动验证．这种方式有效地避免验证条件证明过程的不终止．基于形状图逻辑 以及文中的工作，我们所开发的程序验证系统原型减轻了自动定理证明器的负担，并且能验证易变数据结构上较 为复杂的程序，如有序循环双向链表、二叉排序树、伸展树、树堆、二叉平衡树和ＡＡ树的插入和删除函数． 关键词形状图逻辑；形状分析；程序验证；自动定理证明；循环不变式的推断 中图法分类号ＴＰ３１１ 犇犗犐号１０．１１８９７／ＳＰ．Ｊ．１０１６．２０１６．０２４６０ 犜犺犲狅狉犲犿犘狉狅狏犻狀犵犳狅狉犪犜犺犲狅狉狔狅犳犛犺犪狆犲犌狉犪狆犺狊 ＺＨＡＮＧＹｕＣＨＥＮＹｉＹｕｎＬＩＺｈａｏＰｅｎｇ （犛犮犺狅狅犾狅犳犆狅犿狆狌狋犲狉犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔，犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犎犲犳犲犻２３００２６） （犛狅犳狋狑犪狉犲犛犲犮狌狉犻狋狔犔犪犫狅狉犪狋狅狉狔，犛狌狕犺狅狌犐狀狊狋犻狋狌狋犲犳狅狉犃犱狏犪狀犮犲犱犛狋狌犱狔，犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犛狌狕犺狅狌，犑犻犪狀犵狊狌２１５１２３） 犃犫狊狋狉犪犮狋Ｐｒｏｇｒａｍｓｍａｎｉｐｕｌａｔｉｎｇｍｕｔａｂｌｅｄａｔａｓｔｒｕｃｔｕｒｅｓｐｒｅｓｅｎｔａｃｈａｌｌｅｎｇｅｆｏｒｖｅｒｉｆｉｃａｔｉｏｎ． Ｄｅｅｐａｌｉａｓｉｎｇｉｎｓｉｄｅｄａｔａｓｔｒｕｃｔｕｒｅｓｄｒａｍａｔｉｃａｌｌｙｃｏｍｐｌｉｃａｔｅｓｒｅａｓｏｎｉｎｇｓｔａｔｅｍｅｎｔｓｍａｎｉｐｕｌａｔｉｎｇ ｔｈｅｓｅｓｔｒｕｃｔｕｒｅｓ．Ｔｏａｎａｌｙｚｅａｎｄｖｅｒｉｆｙｐｒｏｇｒａｍｓｍａｎｉｐｕｌａｔｉｎｇｍｕｔａｂｌｅｄａｔａｓｔｒｕｃｔｕｒｅｓ，ｗｅ ｐｒｏｐｏｓｅｄｔｈｅｓｈａｐｅｇｒａｐｈｌｏｇｉｃ．Ｓｈａｐｅｇｒａｐｈｓｄｅｓｃｒｉｂｅｐｏｉｎｔｔｏｒｅｌａｔｉｏｎｓｏｆｓｔａｔｉｃａｌｌｙｄｅｃｌａｒｅｄ ｈｅａｐｐｏｉｎｔｅｒｖａｒｉａｂｌｅｓａｎｄｐｏｉｎｔｅｒｆｉｅｌｄｓｏｆｈｅａｐｏｂｊｅｃｔｓ．Ｔｈｅｙｐｒｅｃｉｓｅｌｙｅｘｐｒｅｓｓｔｈｅｖａｌｉｄｉｔｙｏｆ ｐｏｉｎｔｅｒｓａｎｄｔｈｅｅｑｕａｌｉｔｉｅｓｂｅｔｗｅｅｎｐｏｉｎｔｅｒｓ，ａｎｄｃａｎｂｅｕｓｅｄｔｏｊｕｄｇｅｗｈｅｔｈｅｒｔｗｏａｃｃｅｓｓｅｘｐｒｅｓｓｉｏｎｓ