安全C语言验证器中形状系统的形状检查方法  

Shape Checking Method for the Shape System of Safe C Verifier

作　　者：孙科 罗奇鸣[1] 李薛剑[1] 陈意云[1] SUN Ke;LUO Qi-ming;LI Xue-jian;CHEN Yi-yun(Department of Computer Science and Technology,University of Science and Technology of China,Heifei 230026,China)

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230026

出　　处：《小型微型计算机系统》2019年第1期133-140,共8页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61170018;61229201)资助

摘　　要：在一个基于霍尔逻辑和形状图逻辑的C语言自动验证器中,设计并实现了对形状图中所含易变数据结构的形状检查方法.本工作在验证器的形状系统中实现了显式形状检查与隐式形状检查,并通过引入不同的形状级别,使验证器能够根据不同的严格程度及时发现程序中不符合形状定义的易变数据结构,避免对形状图逻辑的相关演算造成影响.此外,为分解易变数据结构中不同指针域带来的复杂性,形状检查方法引入了三阶段处理框架:形状分割、形状分析及形状推断,分别实现形状图的预处理,针对指针指向与节点类型等方面进行分析,以及根据相关规则推断易变数据结构的形状级别.In an automatic verifier for C programs based on Hoare logic and Shape Graph Logic,we have designed and implemented an approach for checking the shapes of mutable data structures in shape graphs. In particular,we have implemented both explicit shape checking and implicit shape checking in the shape system of the verifier. By introducing different shape levels,the verifier is capable of identifying mutable data structures which do not conform to the shape definitions in time with different levels of rigor,so that the computation of shape graph logic will not be affected. Furthermore,in order to reduce the complexity caused by different pointer field types of mutable data structures,the proposed approach utilizes a three-phase processing framework: shape splitting,shape analysis and shape deduction. The three phases perform the following three tasks,respectively: preprocessing graphs,analyzing " points-to" information of pointers and the type of nodes,and deducing the shape levels for mutable data structures according to related rules.

关 键 词：程序验证 形状图逻辑 形状系统 形状检查 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]