【摘要】 在一个基于霍尔逻辑和形状图逻辑的C语言自动验证器中,设计并实现了对形状图中所含易变数据结构的形状检查方法.本工作在验证器的形状系统中实现了显式形状检查与隐式形状检查,并通过引入不同的形状级别,使验证器能够根据不同的严格程度及时发现程序中不符合形状定义的易变数据结构,避免对形状图逻辑的相关演算造成影响.此外,为分解易变数据结构中不同指针域带来的复杂性,形状检查方法引入了三阶段处理框架:形状分割、形状分析及形状推断,分别实现形状图的预处理,针对指针指向与节点类型等方面进行分析,以及根据相关规则推断易变数据结构的形状级别.更多还原

【Abstract】 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.更多还原