COMPSPEN:对形状性质与数据约束进行融合推理的分离逻辑求解器  

COMPSPEN:Separation Logic Solver for Integrated Reasoning about Shape Properties and Data Constraints

作　　者：苏婉昀 高冲 古新才 吴志林[1,2] SU Wan-Yun;GAO Chong;GU Xin-Cai;WU Zhi-Lin(State Key Laboratory of Computer Science(Institute of Software,Chinese Academy of Sciences),Beijing 100190,China;University of Chinese Academy of Sciences,Beijing 100049,China;Program Language Lab,HUAWEI Technologies Co.Ltd.,Beijing 100085,China;Department of Automatic Driving Technology,Baidu Inc.,Beijing 100193,China)

机构地区：[1]计算机科学国家重点实验室(中国科学院软件研究所),北京100190 [2]中国科学院大学,北京100049 [3]华为技术有限公司编程语言实验室,北京100085 [4]百度自动驾驶技术部,北京100193

出　　处：《软件学报》2023年第5期2181-2195,共15页Journal of Software

基　　金：广东省科技厅新一代人工智能项目(2018B010107004);国家自然科学基金面上基金(61872340);法国INRIA-中国科学院国际合作项目VIP。

摘　　要：分离逻辑是经典霍尔逻辑的针对操作指针和动态数据结构的扩展,已经广泛用于对基础软件(比如操作系统内核等)的分析与验证.分离逻辑约束自动求解是提升对操作指针和动态数据结构的程序的验证的自动化程度的重要手段.针对动态数据结构的验证一般同时涉及形状性质(比如单链表、双链表、树等)和数据性质(比如有序性、数据不变性等).主要介绍能对动态数据结构的形状性质与数据约束进行融合推理的分离逻辑求解器COMPSPEN.首先介绍COMPSPEN的理论基础,包括能够同时描述线性动态数据结构的形状性质和数据约束的分离逻辑子集SLIDdata、SLIDdata的可满足性和蕴涵问题的判定算法.然后,介绍COMPSPEN工具的基本框架.最后,使用COMPSPEN工具进行了实例研究.收集整理了600个测试用例,在这600个测试用例上将COMPSPEN与已有的主流分离逻辑求解器Asterix、S2S、Songbird、SPEN进行了比较.实验结果表明COMPSPEN是唯一能够求解含有集合数据约束的分离逻辑求解器,而且总体来讲,能对线性数据结构上的同时含有形状性质和线性算术数据约束的分离逻辑公式的可满足性问题进行高效的求解,另外,也能对蕴涵问题进行求解.Separation logic is an extension of the classical Hoare logic for reasoning about pointers and dynamic data structures,and has been extensively used in the formal analysis and verification of fundamental software,including operating system kernels.Automated constraint solving is one of the key means to automate the separation-logic based verification of these programs.The verification of programs manipulating dynamic data structures usually involves both the shape properties,e.g.,singly or doubly linked lists and trees,and data constraints,e.g.,sortedness and the invariance of data sets/multisets.This paper introduces COMPSPEN,a separation logic solver capable of simultaneously reasoning about the shape properties and data constraints of linear dynamic data structures.First,the theoretical foundations of COMPSPEN are introduced,including the definition of separation logic fragment SLIDdata as well as the decision procedures of the satisfiability and entailment problems of SLIDdata.Then,the implementation and the architecture of the COMPSPEN tool are presented.At last,the experimental results for COMPSEN are reported.600 test cases are collected and the performance of COMPSPEN is compared with the state-of-the-art separation logic solvers,including Asterix,S2S,Songbird,and SPEN.The experimental results show that COMPSPEN is the only tool capable of solving separation logic formulae involving set data constraints,and in overall,it is able to efficiently solve the satisfiability problem of separation logic formulas involving both shape properties and linear arithmetic data constraints on linear dynamic data structures,and is also capable of solving the entailment problem.

关 键 词：分离逻辑 形状性质 线性算术数据约束 集合数据约束 可满足性问题 蕴涵问题 约束求解器 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]