论文分享_08_03

基于分离逻辑的局部形状分析

           本文是TACAS 2006的文章,题目是A Local Shape Analysis based on Separation Logic。

摘     要

         本文将从以下三个问题,简要阐述该文章的主要工作:

  1. 什么是形状分析(Shape Analysis)?其作用是什么?
  2. 什么是分离逻辑(Separation Logic)? 其作用是什么?
  3. 本文用分离逻辑做形状分析的基本思路是什么?

形状分析

       在含有堆的程序分析问题中,我们关心堆上内容的相关性质的分析,如空指针分析、May-Alias以及堆上数据结构的形状(Shape)等。这里的形状指的就是指针指向的内存对象,具体长什么样,是一个链表还是一棵树等。而形状分析(Shape Analysis)的主要作用是对程序执行的每个节点,给出指针指向的数据结构的形状信息。形状分析算法在本世纪初即得到了研究,Reinhard Wilheim等人提出了形状分析,其基本思想是用抽象的图模型来对内存中堆上内容的指向进行描述和刻画。
       下图是一个程序的例子,右侧是该程序运行时,内存上指针和具体内存内容的指向关系具体图。图中的程序的功能是实现对链表的反向操作,图的变化体现出该段程序运行时,程序是如何一步一步将链表的内容指向进行翻转并得到一个反向的链表。右图中方框代表指针变量,指向表示其指向的对上数据结构,指向箭头上方的记号表示数据结构的对应域,比如next指针等。
    传统的形状分析,在内存结构的表示上,会对指向图进行抽象,如对上述例子,用下图中(a)和(b)两个抽象的图,来分别表示长度大于1的链表和长度等于1的链表。而形状分析最终就是用这样的抽象图,对每个程序节点的内存格局进行上近似的刻画,从而能够从得到的抽象图中获取之前提到的空指针分析、别名分析等我们感兴趣的信息。

分离逻辑

        分离逻辑是Reynolds在2002年提出的对Hoare’s Logic 的扩展,旨在用分离逻辑公式对和内存中栈和堆上内容和结构相关的性质进行描述。也就是说,对于普通的Hoare三元组{P}C{Q},这里的P和Q都会变为分离逻辑公式,以表示内存相关的性质。而本文中考虑的程序C的定义如下:
    其中E是表达式,[E]表示将堆上地址为E处存储的值。关键字new以及dispose会在堆上分别分配和释放内存。而对于以上含有内存操作的程序的状态如下定义:
        这里程序的状态是一个二元组(s,h)分别表示栈和堆,栈是一个对变量赋值的函数,堆是将地址映射到地址处存储的值的偏函数。
       分离逻辑的语法和语义在描述内存结构上提供了相应的支持,例如表示两个空间约束在空间上不交的分离合取符号(*),地址指向的某个内容的指向符号(|→)以及一些表示内存结构的谓词如表示从地址x到地址y存在链表结构的ls(x,y)等,分离逻辑的语法语义的具体定义在文章中可以找到。以下为文章中考虑的分离逻辑公式。
        其中P和Q分别是表示普通的变量常量间的约束的公式和内存结构约束的公式。很自然的,分离逻辑公式的语义是使其成立的二元组(s,h)这样的状态集合,而这样的集合又能够对程序中的每个节点可能出现的状态集合作上近似。

基于分离逻辑的形状分析

        使用分离逻辑做形状分析,要做的事情就是需要利用分离逻辑的语义,对程序每个节点的语义作上近似。由于文章考虑了含有循环的程序,需要对循环的语义也进行考虑。如果不考虑循环,已有利用分离逻辑做符号执行的工作,利用分离逻辑公式的语义给出了程序的语义。本文因为考虑循环,需要通过计算不动点给出循环语义的上近似,即我们需要计算出利用分离逻辑来表示的循环不变式。本文的难点即为循环不变式的生成,主要贡献为确定了上述问题的抽象域、基于分离逻辑的符号执行的语义,给出了抽象域在程序执行时的语义,并证明了抽象域上的语义是具体语义的可靠近似。
       文章中考虑的抽象域是所有分离逻辑公式集合的幂集,记为P(SH). 其中的一个元素为分离逻辑公式的集合,其语义为满足其中某个分离逻辑公式的状态集合的并。由于所有分离逻辑公式的集合SH是一个无穷集合,文章为了使得不动点计算收敛,给出了分离逻辑公式的规范格式的定义,并证明了在该格式下的SH的子集CSH,在保持表达能力相同的情况下其元素个数是有限的,从而保证了在P(CSH)上做不动点计算时的终止性。
        最终文章上述方法进行了实现,并在构造的例子上用该方法进行了形状分析,在文中给出的例子上,本文的方法能够对循环给出一个分离逻辑公式表示的循环不变式。