张健等:程序分析研究进展 一个通用的框架并从理论上保证了所构建的程序分析的终止性和可靠性(即考虑了所有的程序行为)基于抽 象解释来设计程序分析,本质上是通过对程序语义进行不同程度的抽象,以在分析精度和计算效率之间取得权 衡这种由某种语义抽象及其上的操作所构成的数学结构称为抽象域抽象解释采用 Galois连接来刻画具体域 与抽象域之间的关系设D)和D,=)是两个给定的偏序集函数aD→D及yD→D构成的函数对(a)称为D 与D之间的 Galois连接,当且仅当vx∈D,x∈D,a(x)=”x2xx(x2),其中,D,)称为具体域(D",=)称为抽象域a 称为抽象化函数称为具体化函数由定义中的性质a(x)=x(亦即xxx)可知x是x的可靠抽象(又称上近 似)给定具体域(D,)和抽象域DP,)之间的 Galois连接(a外,对于具体域D上的函数∫和抽象域D"上的函数 f,当Vx∈D,(y(x)c(y/")(x)时我们称f是∫的可靠抽象抽象解释理论的一个重要思想是通过在抽象域上 计算程序的抽象不动点来表达程序的抽象语义在程序分析中,程序状态集合通过抽象域中的域元素来近似而 程序语义动作(如赋值、条件测试等)通过抽象域中的域操作(如迁移函数)来可靠建模此外,为了加速抽象域上 不动点迭代的收敛速度并保证不动点迭代的终止性抽象解释框架提供了加宽算子( widening)抽象解释框架能 够保证抽象域上迭代求得的抽象不动点是程序最小不动点(对应程序的具体聚集语义)的上近似换言之,抽象 解释提供了严格的理论来保证基于上近似抽象的推理的可靠性即:所有基于上近似抽象推理得出的性质在原 程序中也必然成立但是由于抽象带来的精度损失,不保证所有在原程序中成立的性质都能基于上近似抽象推 里得到 抽象域是抽象解释框架下的核心要素,一般是面向某类特定性质设计的到目前为止,已出现了数十种面向 不同性质的抽象域其中,具有代表性的抽象域包括区间抽象域、八边形抽象域、多面体抽象域等数值抽象域 此外还出现了若干开源的抽象域库,如 APRON、 ELINA、PP山等基于抽象解释的程序分析工具也不断 涌现,出现了 Polypase!2 Astree1等商业化工具和 Frama-C≌ alue analysis!、 CCCheck(code contract static checker) 51、 Interpol1等学术界工具随着这些工具的日益完善,抽象解释在工业界大规模软件尤其是嵌入式 软件的分析与验证中得到了成功应用典型的应用案例是, Astre成功应用于空客A340(约13.2万行C代码) A380(约35万行C代码)等系列飞机飞行控制软件的自动分析并实现了分析的零误报最近Asre的扩展版 本 street支持多线程C程序中运行时错误、数据竞争、死锁等的检测,并成功应用于 ARINC653航空电子 应用软件(约220万行代码)的分析总体而言基于抽象解释的程序分析主要面临提高分析精度、可扩展性两 方面的挑战 在提高分析精度方面,基于加宽的不动点迭代过程所导致的分析精度损失问题和抽象域本身表达能力的 !性是当前面临的主要问题 ·在缓解加宽所导致的精度损失方面,近年来的研究进展大致可以分为两种思路:(1)使用基于策略迭 代或抽象加速1的不动点迭代过程来取代传统的基于加宽的不动点迭代过程,以获得更精确的分 析结果,但是,该方法只适用于一些特殊类别的程序和抽象域(2)改进加宽/变窄算子及其迭代序列如 结合加宽变窄算子的交叠迭代策略21 ·在弥补抽象域本身表达能力的局限性方面最近的研究进展可分为3类:(1)将符号化方法与抽象方法 合起来利用SMT求解器2)、插值等技术来计算程序中语句迁移函数的最佳抽象,以改进抽象 域在语句迁移函数上的精度损失、(2)提高抽象域的析取表达能力如基于区间线性代数、绝对值约 束、集合差、非格结构、决策树等方法构造的非凸抽象域26,(3)提高抽象域的非线性表达能力,如 基于组合递推分析p28将符号化分析与抽象解释结合起来以生成多项式、指数、对数等形式非线性 不变式基于椭圆幂集来生成二次不变式等 在提高可扩展性方面如何有效降低分析过程中抽象状态表示与计算的时空开销是目前考虑的主要问题 在这方面最近的研究进展包括: 利用变量访问的局部性原理,降低当前抽象环境中所涉及的变量维数,并根据数据流依赖的稀疏性, 降低抽象状态的存储开销和传播开销基于该思想,最近Oh等人提出了一种通用的全局稀疏分析框 架,在不损失分析精度的前提下能够显著降低时空开销,并在静态分析工具 Sparrow上进行了应用,取张健 等:程序分析研究进展 83 一个通用的框架[8],并从理论上保证了所构建的程序分析的终止性和可靠性(即考虑了所有的程序行为).基于抽 象解释来设计程序分析,本质上是通过对程序语义进行不同程度的抽象,以在分析精度和计算效率之间取得权 衡.这种由某种语义抽象及其上的操作所构成的数学结构称为抽象域.抽象解释采用 Galois 连接来刻画具体域 与抽象域之间的关系.设D,⊑和D# ,⊑# 是两个给定的偏序集,函数:DD# 及:D# D构成的函数对(,)称为 D 与 D# 之间的 Galois 连接,当且仅当xD,x# D# ,(x)⊑# x# x⊑(x# ),其中,D,⊑称为具体域,D# ,⊑# 称为抽象域, 称为抽象化函数,称为具体化函数.由定义中的性质(x)⊑# x# (亦即 x⊑(x# ))可知,x# 是 x 的可靠抽象(又称上近 似).给定具体域D,⊑和抽象域D# ,⊑# 之间的 Galois 连接(,),对于具体域 D 上的函数 f 和抽象域 D# 上的函数 f # ,当x# D# ,(f)(x# )⊑(f # )(x# )时,我们称 f # 是 f 的可靠抽象.抽象解释理论的一个重要思想是,通过在抽象域上 计算程序的抽象不动点来表达程序的抽象语义.在程序分析中,程序状态集合通过抽象域中的域元素来近似,而 程序语义动作(如赋值、条件测试等)通过抽象域中的域操作(如迁移函数)来可靠建模.此外,为了加速抽象域上 不动点迭代的收敛速度并保证不动点迭代的终止性,抽象解释框架提供了加宽算子(widening).抽象解释框架能 够保证抽象域上迭代求得的抽象不动点是程序最小不动点(对应程序的具体聚集语义)的上近似.换言之,抽象 解释提供了严格的理论来保证基于上近似抽象的推理的可靠性,即:所有基于上近似抽象推理得出的性质,在原 程序中也必然成立.但是,由于抽象带来的精度损失,不保证所有在原程序中成立的性质都能基于上近似抽象推 理得到. 抽象域是抽象解释框架下的核心要素,一般是面向某类特定性质设计的.到目前为止,已出现了数十种面向 不同性质的抽象域.其中,具有代表性的抽象域包括区间抽象域、八边形抽象域、多面体抽象域等数值抽象域. 此外,还出现了若干开源的抽象域库,如 APRON[9]、ELINA[10]、PPL[11]等.基于抽象解释的程序分析工具也不断 涌现,出现了 PolySpace[12]、Astrée[13]等商业化工具和 Frama-C Value Analysis[14]、CCCheck(code contract static checker)[15]、Interproc[16]等学术界工具.随着这些工具的日益完善,抽象解释在工业界大规模软件,尤其是嵌入式 软件的分析与验证中得到了成功应用.典型的应用案例是,Astrée 成功应用于空客 A340(约 13.2 万行 C 代码)、 A380(约 35 万行 C 代码)等系列飞机飞行控制软件的自动分析并实现了分析的零误报[17].最近,Astrée 的扩展版 本 AstréeA 支持多线程 C 程序中运行时错误、数据竞争、死锁等的检测,并成功应用于 ARINC 653 航空电子 应用软件(约 220 万行代码)的分析[18].总体而言,基于抽象解释的程序分析主要面临提高分析精度、可扩展性两 方面的挑战. 在提高分析精度方面,基于加宽的不动点迭代过程所导致的分析精度损失问题和抽象域本身表达能力的 局限性是当前面临的主要问题.  在缓解加宽所导致的精度损失方面,近年来的研究进展大致可以分为两种思路:(1) 使用基于策略迭 代[19]或抽象加速[20]的不动点迭代过程来取代传统的基于加宽的不动点迭代过程,以获得更精确的分 析结果,但是,该方法只适用于一些特殊类别的程序和抽象域;(2) 改进加宽/变窄算子及其迭代序列,如 结合加宽变窄算子的交叠迭代策略[21].  在弥补抽象域本身表达能力的局限性方面,最近的研究进展可分为 3 类:(1) 将符号化方法与抽象方法 结合起来,利用 SMT 求解器[22,23]、插值[24]等技术来计算程序中语句迁移函数的最佳抽象,以改进抽象 域在语句迁移函数上的精度损失;(2) 提高抽象域的析取表达能力,如基于区间线性代数、绝对值约 束、集合差、非格结构、决策树等方法构造的非凸抽象域[25,26];(3) 提高抽象域的非线性表达能力,如 基于组合递推分析[27,28]将符号化分析与抽象解释结合起来以生成多项式、指数、对数等形式非线性 不变式,基于椭圆幂集来生成二次不变式[29]等. 在提高可扩展性方面,如何有效降低分析过程中抽象状态表示与计算的时空开销是目前考虑的主要问题. 在这方面,最近的研究进展包括:  利用变量访问的局部性原理,降低当前抽象环境中所涉及的变量维数,并根据数据流依赖的稀疏性, 降低抽象状态的存储开销和传播开销.基于该思想,最近,Oh 等人提出了一种通用的全局稀疏分析框 架,在不损失分析精度的前提下能够显著降低时空开销,并在静态分析工具 Sparrow 上进行了应用,取