指针作为程序设计语言不可或缺的基本构成,广泛应用于各种软硬件程序的编制,如C语言中指针的显式声明和使用,或者像Java语言那样隐式的指针操作.指针程序的验证是目前学术界研究的热点和难点之一.如果程序中存在不当的指针操作,将会导致程序运行中出现严重的内存安全性错误,例如内存泄漏、空指针或者悬空指针的引用等.并且由于指针的灵活性所引发的别名问题,加大了程序的检测难度.此外,除了内存安全性,指针程序的时序性质也是亟需验证的一类重要性质.

分离逻辑^[1]是霍尔逻辑的变种和扩展,由Reynolds于2002年提出,其通过引入表达显式分离的逻辑操作符以及相应的推导规则,简化了对指针程序的验证工作.虽然基于分离逻辑的程序验证技术是目前学术界普遍认可的一种重要方法,但需要指出的是,分离逻辑只是在推理方式方面优于其他方法,即局部推理.而从表达能力的角度看,分离逻辑的某些片段并未突破一阶逻辑的范畴^[2],描述和验证内存时序性质的能力欠缺.另一方面,以线性时序逻辑(linear temporal logic,简称LTL)^[3]、计算树逻辑(computation tree logic,简称CTL)^[4]为代表的时序逻辑虽然能够表达时序性质,其缺点也显而易见,即,不能描述带有指针的程序的性质.

近些年来,学者们提出了一些用于指针程序验证的时序逻辑.Yahav等人提出的演化时序逻辑(evolution temporal logic,简称ETL)^[5]是一阶线性时序逻辑,用于描述指针程序的动态行为,包括内存的动态分配和释放.ETL最大的特点在于能够描述大粒度的内存对象与高层次的线程.Distefano等人用刻画指针的断言扩展了LTL,得到的逻辑称为导航时序逻辑(navigation temporal logic,简称NTL)^[6],并提出了基于Tableau的模型检测算法.Rieger提出了一种表达能力较强的指针时序逻辑(temporal pointer logic,简称TPL)^[7],该逻辑也扩展自LTL.然而,TPL是不可判定的,Rieger需要使用抽象技术来建立相应的模型检测算法.文献^[8]把LTL与CTL结合起来得到了一种二维逻辑,LTL用于描述时序(时间),而CTL用于描述内存(空间).由于两个维度都是利用时序逻辑来实现的,使得时间与空间维度之间的区别变得不够清晰,而且性质描述不够简单直观.Brochenin等人的研究^[9]将分离逻辑与LTL相结合,得到一种描述内存时序性质的逻辑LTL^mem.但是,Brochenin选用的分离逻辑片段不包含量词,这限制了LTL^mem的表达能力,使其不能描述复杂的指针结构.此外 ,文献^[9]主要从逻辑可判定性和计算复杂度的角度展开研究,缺少了相应的支持工具和实验结果.

本文介绍的二维逻辑PPTL^SL结合了分离逻辑的一个可判定子集与命题投影时序逻辑PPTL^[10],用于描述指针程序的时序性质,并且开发了工具SAT-PPTL^SL来检查任意PPTL^SL公式的可满足性.PPTL^SL的优点在于:

(1) 继承了分离逻辑的优势,能够以一种简洁直观的方式表达内存性质.同时,PPTL^SL使用的分离逻辑子集可以描述复杂的指针结构,如链表;

(2) 继承了PPTL的优势,PPTL能够表达完全正则语言^[11],其表达能力要强于LTL与CTL.PPTL^SL含有时序操作符“;”和“*”,前者可以刻画顺序事件的发生,而后者可以刻画循环性质.

SAT-PPTL^SL首先解析PPTL^SL公式,将其转换为等价可满足的PPTL^SL的严格子集,称为RPPTL^SL;然后,根据RPPTL^SL与PPTL的同构性质,重用PPTL的相关理论(逻辑规则以及判定过程等),从而完成公式的检查.工具SAT-PPTL^SL不仅得到了PPTL理论的支持,还通过调用SMT(satisfiability modulo theories)求解器实现了自动化检查,提高了工具的实际应用价值.

本文以一些简单的PPTL^SL公式为例,详细地阐述了PPTL^SL到PPTL的同构转换.另外,还以一个经典的指针程序(含有链表操作)为例,说明PPTL^SL如何描述该程序的时序性质,并详细地展示了SAT-PPTL^SL的执行过程;同时,通过实验分析了同构转换过程中所使用的一些参数对工具执行效率的影响.

本文第1节给出PPTL^SL的语法和语义.第2节简要介绍如何构建PPTL^SL与PPTL之间的同构关系以及PPTL^SL的判定过程.第3节详细介绍工具SAT-PPTL^SL,给出若干实例说明同构关系的构建和PPTL^SL公式的判定.第4节给出实验以及分析结果.最后一节总结全文并对研究内容提出进一步展望.

1 . 二维逻辑PPTL^SL 1.1 分离逻辑

本节简要介绍分离逻辑的一个可判定子集(简称为SL)^[12],SL的表达式与文献^[12]中的定义略有区别,但这并不影响其判定性的结论.令Var表示可数无穷的变量集合,Loc表示有限的内存地址集合,该集合的元素为大于0的自然数.常量0用于表示空指针,Var=Loc$\cup ${0}表示值的集合.根据分离逻辑的标准语义,内存状态s由栈I_s和堆I_h两部分构成,表示为二元组(I_s,I_h):

栈 I_s:Var Var;

堆 I_h:Loc Var.

表达式e和SL公式f的语法定义如下:

e::=n|x,

φ::=e1=e2|e1ae2|⌉f|f1∨φ2|φ1#φ2|$x:φ,

(1)

其中,n为自然数,x为变量.公式e₁ae₂描述了仅包含一个内存单元的堆,其地址是e₁,存储的内容为e₂.公式f₁#f₂

断言整个堆可以被分成两个不相交的子堆,其中,一个子堆使得φ₁成立,而另外一个子堆使得φ₂成立.

对于任意表达式e,其在状态(I_s,I_h)下的取值表示为(I_s,I_h)[e],具体定义为(I_s,I_h)[n]=n与(I_s,I_h)[x]=x.

下面给出SL公式的语义,采用可满足性关系符号_SL来定义.

函数f的定义域记作dom(f),对于部分函数f,dom(f)指的是使得f(x)有定义的那些变量x的集合.给定两个函数f₁和f₂,符号f₁^f₂表示f₁和f₂的定义域不相交,符号f₁× f₂表示f₁和f₂的并.函数更新符号f[x→v]定义为f[x→v](x)=v并且∀y≠x:f[x→v](y)=f(y).

SL还引入以下简写表示一些形式较为复杂的公式,在实际应用中能够描述较为常见的内存性质:

这里选择几个比较重要的公式进行解释.e₁∈e₂弱化了e₁ae₂的含义,表示除了e₁描述的内存单元外,堆中还有可能包含其他内存单元.alloc(e)说明当前堆中e指向的地址是已经被分配的.emp表示空堆,其中不含有任何有效内存地址.堆中至少含有n个有效的内存单元才能使得least(n)成立.ls(e₁,e₂)描述了一段以e₁为头部,e₂为尾部的链表片段.e₁→⁺e₂和e₁→e₂属于指针可达性谓词,表示从指针e₁开始,可以通过指针的指向关系到达e₂.如果将单域指针公式e₁ae₂扩展为多域指针公式ea{e₁,…,e_n},则SL可以描述其他指针结构,如双链表和二叉树等.

1.2 分离逻辑的时序扩展

PPTL^SL将SL作为状态公式,而把PPTL的时序算子作为时序公式的连接算子,从而能够描述指针程序的时序性质.设Prop为无限可数的原子命题集合,PPTL^SL公式P以及PPTL公式Q的语法定义如下:

P::=f|⌉P|P1∨P2|dP|(P1,…,Pm) prj P|P*,

Q::=q|⌉Q|Q1∨Q2|dQ|(Q1,…,Qm) prj Q|Q*,

其中,P∈Prop,f为SL公式,P₁,…,P_m(Q₁,…,Q_m)都是良好形式的PPTL^SL(PPTL)公式.“d”(next),“prj”(projection)和“*”(star)为时序算子.仅含时序算子的公式称为时序公式,否则称为状态公式.

区间s$ \buildrel \Delta \over = $〈s₀,s₁,…〉为一个状态序列,|s|表示区间长度.如果区间长度是无限的,则|s|=w;否则,它等于状态数减1.N₀指代非负整数集合,并定义N_ω $ \buildrel \Delta \over = $N₀$\cup ${w},°$ \prec $$ \buildrel \Delta \over = $≤{(ω,ω)}.区间s的子区间〈s_i,…,s_j〉用s_(i…j)(0≤i°j≤|s|)表示.此外,用s×s'表示由区间s的末状态和s'的首状态连接而成的新区间.PPTL的解释是三元组I$ \buildrel \Delta \over = $(s,k,j),其中,s是区间,k≤j≤|s|为整数.解释I=(s,k,j)满足P,记作I\vDashP.为定义投影算子的语义,需要辅助算子¯.设s=〈s₀,s₁,…〉是一个区间,r₀,…,r_h(h≥0)是整数,且有0≤r₀≤…≤r_h≤|s|,则s在r₀,…,r_h上的投影.其中,t₀,…,t_l是通过删除r₀,…,r_h中重复元素所得.例如,〈s₀,s₁,s₂〉¯(0,0,2,2,=〈s₀,s₂〉.PPTL^SL的可满足关系定义如下:

下面列出部分常用的PPTL^SL的导出公式:

e@⌉dtrue,

P1;P2@(P1,P2) prj e,

P+@P;P*,

◊P@true;P,

□P@⌉ ◊⌉P,

dnP@d(dn-1P),n≥1.

◊与□类似于LTL和CTL中的含义,只是多了有限模型的情况.e表示区间的结束,没有后续状态.P₁;P₂表示区间可以分为时间先后的两部分:第1部分满足P₁,第2部分满足P₂.P⁺和P*描述P在区间上反复成立,前者要求P至少成立一次,后者P可以成立0次.

2 PPTL与PPTL^SL之间的同构关系

本节概要介绍如何构建PPTL^SL与PPTL之间的同构关系.从语法结构的角度看,PPTL^SL与PPTL非常相似,只是状态公式有所区别.因此,二者之间存在着紧密的联系.为了构建这种联系,下面将定义PPTL^SL的一个严格子集RPPTL^SL,使其成为连接PPTL与PPTL^SL的纽带.RPPTL^SL公式P_s的语法定义如下:

${P_s}:: = {e_1} = {e_2}|\neg {P_s}|{P_{{s_1}}} \vee {P_{{s_2}}}|\bigcirc {P_s}|({P_{{s_1}}},...,{P_{{s_m}}}){\rm{ }}prj{\rm{ }}{P_s}|{P_s}*$

给定PPTL^SL公式P,从PPTL^SL到PPTL的转换需要两步:第1步,将P转换为与其等价可满足的RPPTL^SL公式P_s;第2步,把P_s再映射到与其同构的PPTL公式.第1步从PPTL^SL~RPPTL^SL的等价可满足转换的意义在于:使得我们只需要研究RPPTL^SL的性质即可,而且RPPTL ^SL的形式更为简单,有助于问题的简化.第2步说明RPPTL^SL完全可以重用PPTL的理论,从而证明PPTL^SL是可判定的.

令C(可包含上下标)表示含有n个变量对的向量,即C=((C_1,1,C_1,2),…,(C_n,1,C_n,2)).第1步转换需要利用C来模拟内存单元的地址和内容,通过函数f和F将PPTL^SL公式映射到RPPTL^SL公式,f负责状态公式f的转换,而F负责公式P的整体转换.

其中,$C = C'\Theta C'' \buildrel \Delta \over = \mathop \wedge \limits_{i \in \{ 1,...,|C|\} } (({C'_{i,1}} = {C_{i,1}} \wedge {C''_{i,1}} = 0 \wedge {C'_{i,2}} = {C_{i,2}}) \vee ({C''_{i,1}} = {C_{i,1}} \wedge {C'_{i,1}} = 0 \wedge {C''_{i,2}} = {C_{i,2}}))$,c₁和c₂是与C的基数相同的值对向量,ψ指代公式e₁=e₂,e₁ae₂,$x:φ或φ₁#φ₂.

借助文献^[2]中的定理1,可以证明经过F转换所得的公式保持了原有公式的可满足性.接下来第2步的转换比较直观,很容易看出,RPPTL^SL比PPTL^SL更接近于PPTL,因为二者只是原子公式有所不同.由此,根据公式的语法结构,下面给出公式同构的定义.直观的讲,公式同构是RPPTL^SL公式与PPTL公式在保证原子公式一一对应的前提下,语法结构上的同构.

定义1. 给定RPPTL^SL公式P_s和PPTL公式Q,称P_s与Q同构,记作P_s@Q,当且仅当:

(1) P_s@e₁=e₂,Qºq,q唯一对应于e₁=e₂,或

(2)${P_s} \equiv \neg {P_{{s_1}}},Q \equiv \neg {Q_1},{P_{{s_1}}} \cong {Q_1}$ ,或

(3)${P_s} \equiv {P_{{s_1}}} \vee {P_{{s_2}}},Q \equiv {Q_1} \vee {Q_2},{P_{{s_1}}} \cong {Q_1},{P_{{s_2}}} \cong {Q_2}$ ,或

(4)${P_s} \equiv \bigcirc {P_{{s_1}}},Q \equiv \bigcirc {Q_1},{P_{{s_1}}} \cong {Q_1}$ ,或

(5)${P_s} \equiv ({P_{{s_1}}},...,{P_{{s_m}}}){\rm{ }}prj{\rm{ }}{P_{{s_0}}},Q \equiv ({Q_1},...,{Q_m}){\rm{ }}prj{\rm{ }}{Q_0},{P_{{s_i}}} \cong {Q_i},0 \le i \le m$ ,或

(6)${P_s} \equiv {P_{{s_1}}}*,Q \equiv {Q_1}*,{P_{{s_1}}} \cong {Q_1}$ .

基于公式的语法结构,通过构造映射原子公式和完整公式的双射函数,可以证明同构关系确实存在于RPPTL^SL与PPTL之间,从而使得PPTL的理论可以被RPPTL^SL所重用,特别是PPTL的判定过程、逻辑规则和相关定义.例如,若dQ₁;Q₂ºd(Q₁;Q₂)是PPTL中有效的逻辑规则,那么$\bigcirc {P_{{s_1}}};{P_{{s_2}}} \equiv \bigcirc ({P_{{s_1}}};{P_{{s_2}}})$也是RPPTL^SL中有效的逻辑规则.下面简要概述PPTL^SL公式的判定过程.

定义2. 给定RPPTL^SL公式P_s,P₌表示P_s中出现的原子公式.称P_s处于范式(normal form)形式,如果P_s能够等价地转换为${P_s} \equiv \mathop \vee \limits_{j = 1}^{n'} ({P_{{e_j}}} \wedge \varepsilon ) \vee \mathop \vee \limits_{i = 1}^n ({P_{{c_i}}} \wedge \bigcirc {P'_{{s_i}}})$.其中,${P_{{e_j}}} \equiv \mathop \wedge \limits_{k = 1}^{m'} {e_{{j_k}}} \buildrel\textstyle.\over= {e'_{{j_k}}},{P_{{c_i}}} \equiv \mathop \wedge \limits_{h = 1}^m {e_{{i_h}}} \buildrel\textstyle.\over= {e'_{{i_h}}},{e_{{j_k}}} = {e'_{{j_k}}},{e_{{i_h}}} = {e'_{{i_h}}} \in {P_ = }$.对于任意e₁=e₂∈P₌,e₁Be₂表示e₁=e₂或e₁≠e₂,${P'_{{s_i}}}$是一个RPPTL^SL公式.

PPTL^SL公式的判定很大程度上依赖于范式这一良好的公式形式.大体上范式分为两部分,分别称作当前部分和未来部分.顾名思义,当前部分刻画的是区间的当前状态,未来部分刻画的则是除了当前状态的后续状态,如果没有后续状态,则用e表示.可以证明,任意RPPTL^SL公式都能够被转换为范式形式,证明过程类似文献^{[13, 14]}中的范式证明.此外,范式转换的算法也可以借鉴文献^{[13, 14]}中的算法.基于范式,还可以构建与RPPTL^SL公式相应的范式图(normal form graph,简称 NFG),其定义和构造方法同样可以借鉴PPTL理论.范式图的节点是RPPTL^SL公式,边是范式的当前部分,通过不断构造未来部分的范式,直至没有新的节点和边产生为止.简单地说,RPPTL^SL公式的判定过程就是构造公式的范式图,然后从其范式图中寻找从根节点出发的有效的有限或者无限路径的过程.一旦找到,说明公式可满足;反之,则公式不可满足.

3 . 原型工具SAT-PPTL^SL 3.1 工具架构

基于PPTL^SL理论,我们开发了求解PPTL^SL公式可满足性的原型工具,命名为SAT-PPTL^SL.SAT-PPTL^SL主要包括4个模块:转换器、范式图构造器、范式生成器以及路径查找器.这些模块共同完成了PPTL^SL公式的检查过程.工具将PPTL^SL公式P作为输入,解析后,利用转换器将P转换为等价的RPPTL^SL公式R.接着,R被传递给范式图构造器,构造其相应的范式图.在构造的过程中,SMT求解器Z3被调用,主要作用是检查范式图中各个边的可满足性,如果不满足,则不会生成相应的边.第3.3节将会详细介绍如何调用SMT求解器Z3.范式生成器也是范式图构造的时候所需要调用的,根据产生的范式来决定是否需要生成新的边和节点,并不断递归调用范式生成器,直至没有新的边和节点出现为止.最终,范式图交由路径查找器处理,由其负责判定是否存在有效的路径,从而给出肯定或否定的判断.如果结果是肯定的,说明P是可满足的;否则,P是不可满足的.

3.2 转换实例

本节通过几个实例详细地说明如何根据同构关系完成PPTL^SL公式到PPTL公式的转换,以及RPPTL^SL公式的范式及范式图构造.

例1:令PPTL^SL公式Pº◊x=y∨□x→0,参照第2节的转换过程,利用函数F将P转换成等价可满足的RPPTL^SL公式.首先,观察P的结构可知,P包含子公式x→0,说明若要满足该子公式,堆的大小至少为1.设变量向量C=((h,h')),转换过程如下:

$\eqalign{ &f(x \mapsto 0,C) = f(x \mapsto 0,C) \cr &{\rm{ }} = f(x \mapsto 0,(h,h')) \cr &{\rm{ }} = f(h \ne 0 \wedge h = x \wedge h' = 0) \cr &{\rm{ }} = h \ne 0 \wedge h = x \wedge h' = 0, \cr &F(P,C) = F(\diamondsuit x = y \vee {\rm{□}}x \mapsto 0,C) \cr &{\rm{ }} = F(\diamondsuit x = y,C) \vee F({\rm{□}}x \mapsto 0,C) \cr &{\rm{ }} = \diamondsuit F(x = y,C) \vee {\rm{□}}F(x \mapsto 0,C) \cr &{\rm{ }} = \diamondsuit f(x = y,(h,h')) \vee {\rm{□}}f(x \mapsto 0,(h,h')) \cr &{\rm{ }} = \diamondsuit x = y \vee {\rm{□}}(h \ne 0 \wedge h = x \wedge h' = 0). \cr} $

容易看出,F(P,C)是一个RPPTL^SL公式,然后可以找到与其同构的PPTL公式Q.设命题p₁,p₂,p₃,p₄分别唯一 对应于公式x=y,h=0,h=x,h'=0,那么Qº◊p₁∨□(⌉p₂∧p₃∧p₄).F(P,C)与Q在语法结构上完全相同,唯一的区别在于原子公式.图1给出了F(P,C)(图左)和Q(图右)的范式图.图中采用黑色公式标记节点,粗体公式标记边,双环圆形节点为起始节点,黑色实心节点为e节点.从图形的角度看,两个图也是同构的,揭示了两个公式的同构关系.另外,边上对应的状态公式也是同构的.

需要指出的是:PPTL^SL的等价可满足转换F含有量词展开的过程,这大大增加了转换所得公式的长度.为了解决这一问题,在实际范式的生成过程中,状态公式并未进行彻底转换.原因在于:范式的生成主要由时序操作符所主导,而状态公式只用于刻画当前状态的公式,且量词只在状态公式中出现.

例2:令PPTL^SL公式Pº(x≠0∨x=y)∧W(x→0#y→0),参照第2节的转换过程,利用函数F将P转换成等价可满足的RPPTL^SL公式F(P,C),然后构造F(P,C)的范式图. 首先,观察P的结构可知,P包含子公式x→0#y→0,说明若要满足子公式,堆的大小至少为2.设变量向量,转换过程如下:

$\eqalign{ &F(P,C){\rm{ }} = F((x \ne 0 \vee x = y) \wedge {\rm{□}}(x \mapsto 0\# y \mapsto 0),C) \cr &{\rm{ }} = F(x \ne 0 \vee x = y,C) \wedge F({\rm{□}}(x \mapsto 0\# y \mapsto 0),C) \cr &{\rm{ }} = F(x \ne 0 \vee x = y,C) \wedge {\rm{□}}F(x \mapsto 0\# y \mapsto 0,C) \cr &{\rm{ }} = (F(x \ne 0,C) \vee F(x = y,C)) \wedge {\rm{□}}F(x \mapsto 0\# y \mapsto 0,C) \cr &{\rm{ }} = (f(x \ne 0,C) \vee f(x = y,C)) \wedge {\rm{□}}f(x \mapsto 0\# y \mapsto 0,C) \cr &{\rm{ }} = (x \ne 0 \vee x = y) \wedge {\rm{□}}f(x \mapsto 0\# y \mapsto 0,C). \cr} $

需要注意的是:这里并未对□f(x→0#y→0,C)做进一步的转换,目的是避免展开量词.类似于PPTL构建范式图的方法,通过不断地递归构造未来部分的范式来得到范式图.首先,将Pº(x≠0∨x=y)∧W(x→0#y→0,C)转换为范式形式,转换过程如下:

$\eqalign{ &(x \ne 0 \vee x = y) \wedge {\rm{□}}f(x \mapsto 0\# y \mapsto 0,C) \cr & \equiv (x \ne 0 \vee x = y) \wedge (f(x \mapsto 0\# y \mapsto 0,C) \wedge \varepsilon \vee f(x \mapsto 0\# y \mapsto 0,C) \wedge \bigcirc {\rm{□}}f(x \mapsto 0\# y \mapsto 0,C)) \cr & \equiv f(x \ne 0 \wedge (x \mapsto 0\# y \mapsto 0),C) \wedge \varepsilon \vee f(x \ne 0 \wedge (x \mapsto 0\# y \mapsto 0),C) \wedge \bigcirc {\rm{□}}f(x \mapsto 0\# y \mapsto 0,C) \vee \cr &{\rm{ }}f(x = y \wedge (x \mapsto 0\# y \mapsto 0),C) \wedge \varepsilon \vee f(x = y \wedge (x \mapsto 0\# y \mapsto 0),C) \wedge \bigcirc {\rm{□}}f(x \mapsto 0\# y \mapsto 0,C). \cr} $

有新的节点□f(x→0#y→0,C)产生,紧接着,将其转换为范式形式,转换过程如下:

□f(x→0#ya0,C)≡f(x→0#y→0,C)∧e∨f(x→0#y→0,C)∧d□f(x→0#y→0,C).

因为已经没有新的节点产生,由此得到公式F(P,C)的范式图,如图2(图左)所示.

然而,标记为f(x=y∧(x→0#ya0),C)的边是不可满足的,因为x与y别名,即指向同一个内存单元,但是同一个内存单元不可能分离为两个不相交的部分(x→0#ya0).因此,凡是标记为f(x=y∧(x→0#ya0),C)的边都应该从范式图中删除,其对应的未来部分将不会参与继续构造范式图,正确的范式图如图2(图右)所示.

3.3 调用SMT求解器Z3

为了能够让工具自动地删除范式图中那些不可满足的边,SAT-PPTL^SL会调用SMT求解器完成这项工作.本节主要结合SAT-PPTL^SL介绍如何使用SMT理论检查边的可满足性.

比特向量逻辑(quantifier bit-vector logic,简称QBVL)^[15]是一阶逻辑的特例,它要求每个变量都是比特向量类型.由于每个全称量词(或存在量词)能够等价地展开为有限长度的合取(或析取)公式,因此,QBVL的可满足性问题是可判定的.但是在实际处理的过程中,量词展开的复杂度是指数级的,目前很多方法都尽量保留量词而不做量词的展开.构建范式的关键在于清晰地将当前部分与未来部分做一个区隔.为了在范式图中找到有限或者无限的从根节点出发的有效路径,需要判定当前部分(边)是否可满足.

PPTL^SL中变量的定义域是有限的,设每个变量为固定长度为n的比特向量类型,则变量的取值范围是[0,2ⁿ-1].因此,范式的当前部分属于QBVL的范畴,而SMT理论能够很好地支持QBVL的求解,构造范式图时便可以结合SMT理论来判定每条边是否可满足.

SMT求解器Z3^[16]是目前业界比较认可的性能优秀的求解器,工具SAT-PPTL^SL集成了Z3.下面简要介绍怎样将范式图的边转换为SMT求解器所能够接受的语言SMT-LIB 2.0.整个转换分为3个步骤:表达式的转换、当前部分公式的转换以及脚本文件的生成.

(1) 首先介绍表达式的转换.

表达式包括两部分:变量x与常量n.前者的转换比较直接,后者的转换需要将常量重写为二进制、十进制或十六进制的向量表示形式.符号Bv是一个函数,用于把常量转换为等价的比特向量形式.具体的转换实现为函数Texp(e):

Function Texp(e)

  case

   e is n: return Bv(n); e is x: return x;

  end case

end Function

(2) 然后介绍范式当前部分公式的转换.

变量向量C可能会表示非法的堆,因为相同的地址可能会出现多于一次,而堆中的地址都是唯一的.例如,设向量C=((C_1,1,C_1,2),(C_2,1,C_2,2)),满足(C_1,1=C_2,1)≠0,该向量就不能表示合法的堆.合法堆VH(C)的定义为

简单地说,VH(C)通过限制变量的取值使得堆中的地址唯一而保证C可以表示合法的堆.

范式当前部分转换的核心主要是状态公式的转换,算法1和算法2实现了该过程.

算法1. 将状态公式f转换为相应的QBVL.

Function TQBVL(f,C)

 case

   φ is true: return true;

   φ is e₁=e₂: return e₁=e₂;

   φ is e₁→e₂:return

   φ is φ₁#φ₂: return $C',C²:C'QC²∧φ(φ₁,C')∧φ(φ₂,C²);

   φ is ⌉φ₁ : return ⌉TQBVL(φ₁,C);

   φ is φ₁∨φ₂: return TQBVL(φ₁,C)∨TQBVL(φ₂,C);

   φ is φ₁∧φ₂: return TQBVL(φ₁,C)∧TQBVL(φ₂,C);

   φ is $x:φ₁: return $x:TQBVL(φ₁,C);

  φ is ∀x:φ₁: return ∀x:TQBVL(φ₁,C);

  end case

end Function

算法2. 将状态公式φ转换为相应的QBVL,同时要求变量向量C表示合法堆.

Function TQBVL_VH(φ,C)

  retrun TQBVL(φ,C)∧VH(C);

end Function

(3) 最后介绍如何生成Z3可接受的脚本文件,伪代码见算法3和算法4.

除了状态公式的转换,为了让Z3能够成功执行,脚本中还需要一些额外的信息(set-option命令)来配置Z3的行为.算法中,Loc是自定义类型,声明为长度为n的比特向量类型,即(_BitVec n).在SMT语言中,变量必须声明后才能被使用,因此,首先声明所有出现在公式中的自由变量;接着,利用函数write将配置信息、变量声明以及转换后的公式写入文件sat-formula.smt2.

算法3. 将QBVL公式f_b转换为SMT语言.

Function QBVL2SMT(φ_b)

case

φ_b is true : return true;

φ_b is e₁=e₂: return (=Texp(e₁) Texp(e₂));

φ_b is e₁≠e₂: return (distinct Texp(e₁) Texp(e₂));

φ_b is : return ;

φ_b is : return ;

φ_b is : return ;

φ_b is : return ;

φ_b is : return ;

end case

end Function

算法4. 将状态公式φ转换为SMT脚本文件,fv(φ)表示公式φ中的所有自由变量.

Function TSMT(φ,C)

  φ_b:=TQBVL_VH(φ,C);

  {x₁,…,x_m}:=φv(φ_b);

  R:=QBVL2SMT(φ_b);

  sat-formula.smt2:=write(sat-formula.smt2,((set-option: print-success true) (set-option:

    print-models true) (set-option: print-proofs true) (set-option: mbqi true)

    (define-sort Loc() (_BitVec n)) (declare-fun x₁ () Loc)…

    (declare-fun x_m () Loc) (assert R) (check-sat) (get-value (x₁,…,x_m))));

  return sat-formula.smt2;

end Function

4 . 实验与分析

当前版本的工具可以在Windows系统中运行,采用C++语言开发.我们将例2讨论的PPTL^SL公式以文本的形式输入给工具提供的编辑器,运行后生成的范式图如图3所示.

正如所期望的,范式图中并未包含标记为f(x=y∧(x→0#y→0),C)的边.最后,工具检测到范式图中存在有效的有限路径和无限路径:

· 前者如路径〈(x≠0∨x=y)∧□f(x→0#ya0,C),x≠0∧(x→0#ya0),e〉;

· 后者如路径〈(x≠0∨x=y)∧□f(x→0#ya0,C),x≠0∧(x→0#ya0),x→0#ya0,x→0#ya0,…〉.

从而判定公式是可满足的.

下面给出一个指针程序的伪代码,其主要功能是创建长度为n的链表,然后再释放其占用的内存.

本小节将展示PPTL^SL能够描述该程序的一些时序相关的性质,接着,将会用SAT-PPTL^SL工具求解这些性质的可满足性.

struct Node {struct Node *next;};

Function cre_dis() {

  Node *x:=NULL,*t:=NULL;

  while (n--) {t:=new(Node); t→next:=x; x:=t;}

  while (x!=NULL) {t:=x; x:=x→next; free(t);}

}

(1) ◊(ls(x,0)∧least(n));◊emp:此性质刻画了两个顺序事件,程序首先将会到达一个状态,该状态的堆中存在一个链表,并且至少包含n个内存单元,然后释放链表,最终内存不存在任何已经分配的内存单元;

(2) □(ls(x,0)#true∨x=0):在程序运行的过程中,指针x总会指向一个链表,或者为空指针;

(3) ◊($y:(ls(x,y)#ya0)∧y=t):指针t将会与链表的最后一个节点别名;

(4) □(∀y:alloc(y)→(x→*y∨t→*y)):此性质利用指针可达性谓词描述了程序不存在内存泄漏的情况;

(5) (◊(ls(x,0))*:此性质描述了一个循环事件的发生,程序中两个循环的每次完整执行,都会使得所有的内存单元都会组成一个以x为头指针的链表.更精确地,假设每个赋值语句的执行占用一个单位区间的

长度,则此性质可以写做(d³ls(x,0))*(每隔3个状态循环性质成立).

逻辑maLTL^[8]使用LTL描述程序的时序性质,同时利用CTL表达每个全局状态的指针结构.虽然文献^[8]可以用CTL描述链表,但是没有分离逻辑简单和直观,而且无法表达分离逻辑中的分离性质,不能精确地刻画内存的状态.从另外一个角度,LTL的表达能力要弱于PPTL,上述程序的某些时序性质难以用LTL表示,如顺序和循环性质.类似地,LTL^mem[9]在描述时序性质方面与PPTL^SL相比也略显不足,而且其结合的分离逻辑片段不含有量词,缺少描述复杂指针结构的能力.NTL^[6]与TPL^[7]采用相似的方法对操作单链表的指针程序进行抽象,并构建了相应的模型检测算法.由于二者属于一阶时序逻辑的范畴,表达能力要优于PPTL^SL,但是抽象技术使得某些情况下不能确定程序是否满足指定的性质.此外,文献^{[6, 7]}的抽象技术只能针对单链表程序,而PPTL^SL则可以描述更为复杂的指针结构(需扩展e₁ae₂为ea{e₁,…,e_n}).

我们通过实验来证明工具的可用性以及分析堆的大小对工具性能的影响,实验环境为Intel双核i3 CUP,3.20GHz,8GB内存.表1展示了实验结果,第1列为上面提到的用PPTL^SL公式表达的6个时序性质,它们描述了操作链表的指针程序的一些典型性质;第2列为公式转换时所需变量向量的大小,即对应于堆的大小;第3列记录了工具运行时间(包括SMT求解器调用时间和总计运行时间);最后一列给出了公式可满足性的检测结果.可以看出:随着堆的增长,工具的运行时间变得越长.这一现象与转换过程相一致,因为变量向量越大,转换的结果越复杂.公式转换的时间比较短,大部分时间花费在SMT求解器调用上.理论上,所有的公式都是可满足的,然而工具在某些情况下给出了否定的结果,这是由于堆的大小并不足以使得公式成立.例如,◊(ls(x,0)∧least(3));◊emp要求堆必须至少存在3个已分配的内存单元,因此在堆小于3的情况下是不可满足的.

5 . 结束语

本文结合二维(空间和时间)逻辑PPTL^SL介绍了支持工具SAT-PPTL^SL.相比现有的时序逻辑,PPTL^SL的表达能力较强,描述方式简单直观,能够描述操作链表的指针程序的时序性质,并且有着PPTL理论的强力支持. SAT-PPTL^SL利用SMT求解器实现了PPTL^SL公式可满足性的自动化检查.此外,本文还选取一些典型逻辑公式实例进行了实验,分析了关键参数对SAT-PPTL^SL执行效率的影响.在今后的工作中,我们将会研究基于PPTL^SL的统一模型检测方法^[17],并进一步扩展PPTL^SL,使其能够描述比单链表更为复杂的指针结构,从而验证现实世界的指针程序,如Windows驱动程序^[18],以及并发生产者-消费者算法^[6]、非阻塞栈(non-blocking stack)算法^[19]和锁耦合链表(lock-coupling list)算法^[20]等.