（计算机软件与理论专业论文）出具证明编译器中验证条件化简和编译优化的研究.pdf

摘要 摘要 程序验证用逻辑证明的方法证明程序满足其规范，是实现安全性的重要方法。 出具证明编译器( c e r t i f y i n gc o m p i l e r ) 是编译器与验证器的结合。本文描述的 出具证明编译器项目c c o m p 让用户给出描述程序正确性的规范，并在源代码使 用霍尔逻辑风格的推理规则产生验证条件( v e r i f i c a t i o nc o n d i t i o n ，v c ) ，经由证 明器证明后产生证明项。然后将源代码和规范转化成底层的汇编代码和其上的规 范，并利用源级证明项生成汇编代码级证明，最终生成携带证明代码。 c c o m p 由多人协作完成，本人承担项目中的断言语言设计以及验证条件生 成和化简工作。实验室先前的项目p o i n t e r c 4 ，过大的验证条件规模成为系统性 能的瓶颈。因此c c o m p 采用一系列的措施来化简v c ，删除其中的冗余。 实用的编译器会包含众多优化，以提高程序执行的效率。编译优化是一系列 程序变换，对于出具证明编译中包含规范的程序，变换前的程序的规范可能无法 正确或充分地描述变换后的程序，为此程序规范也应该随着代码优化一起转换。 目前关于出具证明编译器的项目较少研究编译优化的影响，但编译优化是决定出 具证明编译器是否能走向应用的关键因素之一。 本文通过分析研究，针对以上两个重要问题分别提出了相应的解决方案，并 实现了原型系统验证方法的合理性。本文的主要贡献为： 1 为c c o m p 项目设计了使用分离逻辑描述的断言语言和其推理规则，实 现了相应的验证条件生成器；设计并实现了一个重写系统，实现了验证 条件的化简，解决了验证条件过大的问题。 2 通过研究数据流优化的基本行为，实现了一个包含多种优化和相应舰范 转换的编译器原型系统，利用数据流分析结果来变换规范，使各循环的 循环不变式经过调整后，能作为优化后程序的相应循环的循环不变式。 并初步总结出了通用的转换模式。 本文第一部分工作是c c o m p 项目的一部分。第二部分工作则较为独立，可 作为未来对包含代码优化的出具证明编译器的研究基础。 关键字：程序验证，出具证明编译器，验证条件生成器，验证条件化简，编译优 化，数据流分析，规范转换 得渖：原水再函数的前条件和后条件仍作为优化后程序的前条件和后条件，岗为奉文的初步研究尚朱涉 及函数间的优化。 a b s t r a c t a b s t r a c t p r o g r a mv e r i f i c a t i o nw h i c hi sa l li m p o r ta p p r o a c ht oa c h i e v es e c u r i t y , u s el o g i c r u l e st o p r o v et h ep r o g r a ms a t i s f i e si t ss p e c i f i c a t i o n c e r t i f y i n gc o m p i l e rw h i c hi s c o m b i n e db yac o m p i l e ra n dac e r t i f i e ru s e st h i sa p p r o a c h t h ec e r t i 伽n gc o m p i l e r c c o m pw ep r o p o s e dh e r el e tt h eu s e rt op r o v i d et h es p e c i f i c a t i o nu s i n gs e p a r a t i o n l o g i ct oe x p r e s sm o r ep r o p e r t i e st h a nt y p es a f e t y t h ec o m p i l e rv e r i f i e sp r o g r a mi n s o u r c el e v e la n dt r a n s l a t et h ep r o o f st oa s s e m b l yl e v e l v e i l f y i n gi ns o u r c el e v e lc a n r e p o r te r r o r si nt i m e ，w h i l et a r g e tl e v e lp r o o f sc a nb eu s e dt op r o d u c ep c c c c o m pi s ac o r p o r a t i o np r o j e c t ic o n c e n t r a t eo nv e r i f i c a t i o nc o n d i t i o n g e n e r a t i o na n dr e d u c t i o n t h ep l c cc e r t i f y i n gc o m p i l e ro u rl a b o r a t o r yd e v e l o p e dh a s b e e ns u f f e r sf r o ml a r g ev e r i f i c a t i o nc o n d i t i o n s c c o m pu s es e v e r a lm e t h o d st o r e m o v et h er e d u n d a n ti no r d e rt or e d u c et h es c a l eo fv c s ap r a c t i c a lc o m p i l e ro f t e nh a sm a n yo p t i m i z a t i o n p a s s e st op r o d u c em o r e e f f i c i e n tc o d e c o d eo p t i m i z a t i o nw h i c hw eb e l i e v ei s s i g n i f i c a n tf o rc e r t i f y i n g c o m p i l e rt ob e c o m ep r a c t i c a li sl e s sc o n c e r n e db yt h ec o m m u n i t y c o d eo p t i m i z a t i o n i sc o m p o s e db ym a n yc o d et r a n s f o r m a t i o ns e q u e n c e s t h eo r i g i n a ls p e c i f i c a t i o no ft h e c o d em a yn o tc o r r e c t l yo ra d e q u a t e l yt od e s c r i b et h ep r o p e r t yo ft h eo p t i m i z e dc o d e s ot h es p e c i f i c a t i o n ss h o u l db et r a n s f o r m e da l o n gw i t ht h ec o d ed u r i n go p t i m i z a t i o n t h e s et w ot o p i c sa r eb o t hs i g n i f i c a n tt o c e r t i f y i n gc o m p i l e r i nt h i sp a p e rw e p r o p o s es o l u t i o n sf o rb o t h w eh a v ea l s oi m p l e m e n t e dp r o t o t y p es y s t e m st ov a l i do u r s o l u t i o n s t h ec o n t r i b u t i o n so ft h i sp a p e ra r el i s t e db e l o w 1 d e s i g nt h ea s s e r t i o nl a n g u a g eo fc c o m pc e r t i f y i n gc o m p i l e ra n di m p l e m e n t v e r i f i c a t i o nc o n d i t i o ng e n e r a t o rf o rt h es o u r c el e v e lv e r i f i c a t i o n w ea l s o d e v e l o p ar e w r i t es y s t e mt or e d u c et h er e d u n d a n to ft h e g e n e r a t e d v e r i f i c a t i o nc o n d i t i o n s 2 w e p r o p o s ead a t a f l o wa n a l y s i sb a s e dm e t h o dt ot r a n s f o r ms p e c i f i c a t i o n st o s u s t a i nt h ec o n s t r a i n to fo r i g i n a ls p e c i f i c a t i o n st ot h eo p t i m i z e dc o d e w e a l s od e v e l o pap r o t o t y p ec o m p i l e rw i t hm a n yi m p o r t a n to p t i m i z a t i o n st o d e m o n s t r a t et h ef e a s i b i l i t yo fo u ra p p r o a c h t h ef i r s tt o p i ci si m p l e m e n ta sap a r to ft h ec c o m pp r o j e c t ，w h i l et h es e c o n d c o n t r i b u t i o nc a nb eu s e da saf o u n d a t i o no fa no p t i m i z i n gc e r t i f y i n gc o m p i l e ri nt h e f u t u r e i i i a b s t r a c t k e yw o r d s ：p r o g r a mv e r i f i c a t i o n ，c e r t i f y i n gc o m p i l e r , v e r i f i c a t i o n c o n d i t i o n g e n e r a t i o n ，v e r i f i c a t i o nc o n d i t i o ng e n e r a t i o n ，c o d eo p t i m i z a t i o n ，d a t af l o wa n a l y s i s ， s p e c i f i c a t i o nt r a n s f o r m a t i o n i v 中国科学技术大学学位论文原创性声明 本人声明所呈交的学位论文，是本人在导师指导下进行研究工作所取得的成 果。除已特别加以标注和致谢的地方外，论文中不包含任何他人已经发表或撰写 过的研究成果。与我一同工作的同志对本研究所做的贡献均已在论文中作了明确 的说明。 作者签名：蜂 签字同期：二趁血洳牛日 中国科学技术大学学位论文授权使用声明 作为申请学位的条件之一，学位论文著作权拥有者授权中国科学技术大学拥 有学位论文的部分使用权，即：学校有权按有关规定向国家有关部门或机构送交 论文的复印件和电子版，允许论文被查阅和借阅，可以将学位论文编入中国学 位论文全文数据库等有关数据库进行检索，可以采用影印、缩印或扫描等复制 手段保存、汇编学位论文。本人提交的电子文档的内容和纸质论文的内容相一致。 保密的学位论文在解密后也遵守此规定。 母公开 口保密l 年) 作者签名：建查盛 签字同期：o 生l 旦年与旺蚴 导师躲隘主坌 第1 章绪论 第1 章绪论 随着信息科技的进步和发展，计算机已经被广泛地应用到国民经济和人民生 活的各个方面，计算机里运行的软件也已成为人们生产生活的基本设施，软件安 全也越来越重要。在一些领域，如航空航天、医疗、金融、能源、国防等领域， 软件缺陷可能能导致重大的经济损失，甚至威胁生命的安全。软件安全( s o f t w a r e s e c u r i t y ) 也越来越成为人们关注的热点。 软件规模的越来越大，复杂程度也越来越高，保障软件的可靠性也越来越困 难。传统的软件安全保障性方法是软件测试，但软件测试有不完备性，即使是最 详尽的测试也无法完全排除软件里的缺陷。 在研究领域，程序验i i e ( p r o g r a mc e r t i f i c a t i o n ) 使用逻辑证明的方法来证明程 序满足其规范所描述的性质，是实现安全性的一个重要方法。程序规范( p r o g r a m s p e c i f i c a t i o n ) 由一组用逻辑表达式构成的断言( a s s e r t i o n ) 组成，描述程序应具 有的性质。程序验证通过使用推理规则来验证程序，得到程序符合其规范的严格 的数学证明。 源级验证工具如s m a l l f o o t 2 】、b o o g i e 3 ，让程序员提供程序规范，描述应 满足的性质，使用霍尔逻辑风格的验证规则，在源代码级验证程序满足其规范。 但其好处之一是可以让程序员定义描述程序证确性的规范，而不仅仅是类型安全 性和内存安全性；另外一个好处是这些工具可以像类型检查器一样，能把错误及 时准确地报告给用户。但这些工具不能产生可以被检查的证明；而且只在源级验 证，编译器可能引入的错误不能被检测。 而出具证明编译器( c e r t i f y i n gc o m p i l e r ) 贝l j 解决了上述问题。出具证明编译器 是编译器和验证器的结合。n e c u l a 的t o u c h s t o n e 【l 】是最早关于出具证明编译器的 项目，能将c 语言一个类型安全的子集程序翻译成汇编程序和类型信息、循环 不变式等注释，然后使用一个验证器( c e r t i f i e r ) 来验证汇编程序的类型安全性 和内存安全性，最终生成携带证明的代码( p r o o f c a r r y i n gc o d e ，p c c ) 。p c c 的 一个重要的优势是在于它将编译器排除在被信任的软件基础之外( t r u s t e d c o m p u t i n gb a s e ，t c b ) 。 本文的介绍工作和上述工作有着较多的联系。本章将介绍程序验证、出具证 明编译器、源级验证系统等相关知识背景。第一节将绍程序验证，程序规范，霍 尔逻辑等有关程序验证的概念。第二节将会介绍出具证明编译器和p c c ，这一 节将会详细介绍出具证明编译器的特点和结构。第四节会介绍源级验证工具，并 介绍其典型项目s m a l l f o o t 2 和b o o g i e 3 。最后大概地介绍协作项目c c o m p 以 1 第1 章绪论 及本文所关注的课题。 1 1 程序验证与霍尔逻辑 程序验证技术在特定的形式系统( 通常是数理逻辑系统) 中对程序构造形式 化的模型，并在形式模型上对程序进行逻辑推理和证明。形式程序验证研究始于 h o a r e ( 1 9 6 9 ) 等提出的h o a r e 逻辑理论( 也被称为公里逻辑语义体系) 。经典的 描述程序部分正确性的h o a r e 三元组： ( p ) c ( q ) 是一个数理逻辑断言。标准的霍尔逻辑只证明部分正确性( p a r t i a lc o r r e c t n e s s ) ， 而中止性需要单独证明。因此这个三元组它表示程序代码c 从满足以程序状态 为参数的逻辑断言p 的状态开始执行，若执行中止，则中止时的状态将满足断言 q 。把状态断言对( p q ) 看做描述程序行为的规范，那么证明h o a r e 三元组为 真的数理逻辑证明也就是对应的程序满足其规范的证明。 霍尔三元组的证明依赖于定于程序语义的一组公理和一组推理规则 ( i n f e r e n c er u l e ) 。霍尔逻辑定义了一个简单的命令式语言，对于它所有的构造， 都提供了相应的推理规则。比如，对于赋值语句有规则： ( p e x 】x ：= e ( p ) 表示若赋值后的程序满足断言p ，那么在赋值语句前的程序应满足将p 中所有的 自由变量替换为e 的断言。下面是是一些推导示例： ( x + 1 = 4 3 y ：= x + 1p = 4 3 ( x + 1 n ) x ：= x + 1 ( x n ) 对于顺序执行的程序语句有下列的序列规则( s e q u e n c er u l e ) ： ( p ) s ( q ) ，( q ) t ( r ) ( p ) s ；t ( r ) 比如，考虑下面两个应用赋值语句规则的两个实例： ( x + 1 = 4 3 y ：= x + 1 ( y = 4 3 和 ( y = 4 3 z ：= y ( z = 4 3 使用序列规则可以得出： ( x + 1 = 4 3 y ：= x + 1 ；z ：= y ( z = 4 3 对于其他的语言构造也有对应的推理规则，下面列举出的分别是条件分支语 句，循环语句对应的规则，以及c o n s e q u e n c er u l e ： 2 第1 章绪论 ( bap ) s ( q ) ，( bap t ( r ) ( p ) i fbt h e nse l s ete n d i f ( q ) ( bap ) s ( p ) ( p ) w h i l ebd osd o n e ( bap ) p 7 _ p ，( p ) s ( q ) ，q q ( p ) s ( q ) 验证条件生成器( v e r i f i c a t i o nc o n d i t i o ng e n e r a t o r ，v c g e n ) 根据这些规 则演算生成验证条件。验证条件是一个逻辑命题，在一个验证系统里，可交付给 自动定理证明器证明，或通过工具交互式地证明。 比如根据上述演算规则，霍尔三元组( p ) v ：= e ( q ) 由得到的产生的验证条件 为p q e v 。比如( x = o ) x - x + 1 = 1 ) 产生的验证条件为x = 0 一( x + 1 ) = 1 。三元组( p ) i fst h e nce n d i f ( q ) 产生的验证条件分别为( pa s ) _ q 以及 由( pa s c ( q 】产生的验证条件。对于其它的语句，也分别有相应的规则对应。 在这个示例中，验证条件采用自前而后的推导策略，这个种演算叫做最弱前 条件演算。而自前而后的演算叫做最强后条件演算。 经典的霍尔逻辑也存在一些问题。经典h o a r e 逻辑理论上允许使用通用的数 理逻辑构造程序规范( 状态断言) ，具有有很强的表达能力。但程序f 确性往往 难以描述，可能需要定义非常长的程序规范。定理证明很难以自动化，目前自动 化推理只能处理一些简单的问题。为复杂的程序构造基于h o a r e 逻辑的正确性证 明至今仍是一个有待研究的问题。 1 2 源级验证工具 源代码级别验证工具使用形式化程序验证的的方法来验证程序满足其规范。 不同于程序分析工具，这些验证工具使用霍尔逻辑风格的规则来推理程序。源级 证明工具需要程序员提供程序规范，这些规范包括前条件、后条件、循坏不变式 等，然后根据相应的规则生成验证条件，由证明器来证明验证条件。 典型的源级验证工具有s m a l l f o o t 1 ，2 币1 1b o o g i e 6 等。b o o g i e 实质上是一个 验证条件生成器，它能接受多种源语言作为输入，包括s p e c # 、c 撑、c 等，以及 用一阶逻辑表达的程序规范。b o o g i e 可能会对输入程序做一些循环不变式推导， 然后使用最弱自订条件( w e a k e s tp r e c o n d i t i o n ) 演算得到验证条件。验证条件产生 后被传给s i m p l y 或z 3 定理证明器证明，得到程序是否满足规范的结论。 s m a l l f o o t 是一个使用分离逻辑( s e p a r a t i o nl o g i c ) 1 2 规范的自动化验证工 3 第1 章绪论 具，能验证操纵递归定义的动态创建的数据结构的串行程序以及并发程序。相比 先前的形式化方法，使用分离逻辑让程序规范以及程序证明变得简单。使用分离 逻辑描述的程序规范通常较“小 ，因为在规范中只关注程序当前模块正确执行 相关的资源( 比如内存堆) ，而不必提及其它的模块使用的资源。s m a l l f o o t 使用 轻量级的断言来描述数据结构的形状，而不是它们的具体内容。这些限制使得推 导完全自动化。s m a l l f o o t 的输入语言包含函数、结构体，能进行分配、释放内 存堆单元以及对内存堆修改的操作。s m a l l f o o t 内建了一些数据结构的形状谓词， 如链表段、双向链表段，二叉树等固定几个谓词。 s m a l l f o o t 定义了一套规范的演算的规则用于生成验证条件，验证条件采用 最强后条件的方式，从前往后演算。验证条件生成之后，并不传给证明器证明， 而是使用定义的一组n o r m o l i z a t i o n 和r e d u c t i o n 规则化简验证条件，直至将验证 条件的两边的断言完全消去。 源级验证工具能像类型检查器一样，在源代码级别检查程序，并将验证结果 报告给程序员。这这种方法的好处是可以及时精确地报告错误，而且可以在源级 规范中能更直观地表达更丰富的程序性质。但这些工具不在汇编级验证，从而把 出具排除在被信任软件基础之外；也不能产生证明项和携带证明代码，以减少被 信任软件基础。 1 3 携带证明代码与出具证明编译器 携带证明代码( p r o o f - c a r t i n g c o d e ，p c c ) 是霍尔逻辑在底层代码上的应用。 在p c c 中，代码( 通常是汇编代码) 和代码证明打包在一起。代码消费方，通 代码绑定的形式化证明项，来验证一个应用程序的性质。消费方的验证系统可以 快速地验证证明项的正确性，然后将证明的结论和自己的安全策略做对比来决定 应用程序是否能安全地执行。这种机制在确保内存安全性方面较为有用，比如能 避免内存泄露、栈溢出，悬空指针访问等常见的问题。 携带证明代码在1 9 9 6 年最早被g e o r g en e c u l a 和p e t e rl e e 3 提出。n e c u l a 还设计实现了一个p c c 的产生系统和验证系统t o u c h s t o n e 。p c c 系统的工作流 程为： 1 在代码生产方，代码并由出具证明编译器生成相应的汇编代码和一定的 程序注释。 2 由验证条件生成器从安全性规范和汇编代码中生成相应的验证条件 ( v e r i f i c a t i o nc o n d i t i o n v c ) 。 3 代码生产方使用自动或半自动推理工具生成该验证条件的证明。汇编代 4 第1 章绪论 码和安全性证明一起构成了一个p c c 包。 4 代码消费方接收到p c c 包后，根据安全性规范和汇编代码重新生成v c ， 并将v c 和p c c 包中的证明交由证明检查器判断。如果判断通过，p c c 包中的代码就可以安全地在代码消费方的硬件上执行了。 n e c u l a 提出的出具证明编译器( c e r t i f y i n gc o m p i l e r ) 是p c c 的产生系统， 和普通的编译器不同的是，出具证明编译器将源语言的类型信息在编译的过程中 保留下来，变成程序注释( a n n o t a t i o n ) ，并在汇编级别产生程序满足安全性规范 的证明。出具证明编译器关注的是程序安全性而不是正确性。由于安全性的定义 较为简单，所以在大多数情况下，安全性证明都可以用定理证明工具自动地完成。 出具证明编译器和p c c 系统解决了源级证明工具不产生证明项，且t c b 过 大的问题。但也有自身的问题，出具证明编译器验证的程序性质往往局限于验证 类型和内存安全性等有限性质。而源级验证工具却能允许程序员自行定义关于程 序正确性的性质。 1 4 本文所介绍的工作 我们实验室的对出具证明编译器的研究项目，尝试在遵循现有p c c 系统以 及出具证明编译器框架的自订提下，引入源级验证系统的优点，让用户在源代码级 提供程序规范，构建一个能验证除安全性以外更多关于程序正确性出具证明编译 器。这种编译器模型中很多课题需要研究。比如逻辑的设计、自动定理证明器、 规范翻译、证明复用、代码优化等课题。 实验室先前的出具证明编泽器项目p o i n t e r c 4 主要用于验证指针的安全性。 p o i n t e r c 使用指针逻辑来描述描述和推导指针的性质，能精确分析指针，并能验 证关于指针程序的各种性质，能检查程序中如数组越界和悬空指针引用等问题。 而新项目c c o m p 迸一步研究了出具编译器中的许多课题。 本文所介绍的工作分为两部分：第一部分介绍在协作的编译器项目中验证条 件的生成与化简的设计与实现；第二部分则介绍对出具证明编译器中的代码优化 以及对应规范转换的研究工作。两部分均是出具证明编译器中的重要课题。其中 第一部分工作是实验室协作项目c c o m pt 作的一部分，第二部分则独立于 c c o m p 项目，是一个较为独立的课题，旨在为下一轮的研究的做准备。 1 4 1 c c o m p 本文第一部分中描述的出具证明编译器是我们实验室协作的出具证明编译 器项目c c o m p 。在这个项目旱我们研究开发出具证明编译器各项重要组件，比 如验证框架、自动定理证明器等，并实现一个完整的出具证明编译器c c o m p 。 5 第1 章绪论 c c o m p 遵循典型的出具证明编译框架，输入是一个类c 的小语言c l i k e ，生 成携带证明的汇编代码。但借鉴了上节所表述的源级验证系统的优点，让用户提 供使用逻辑表达式描述程序正确性( 而不仅仅是安全性) 的规范，并在源代码级 使用霍尔逻辑风格的推理规则产生验证条件，经由自动定理证明器证明后产生证 明项。然后将源代码和规范转化成底层的汇编代码和其上的规范，并复用源级的 证明项生成汇编代码满足其规范的证明，最终生成p c c 。图1 1 展示了c c o m p 出具证明编译器大致的结构。 图1 1c c o m p 出具证明编译器结构图 和p o i n t e r c 项目相比，c c o m p 使用分离逻辑( s e p e r a t i o nl o g i c ) 1 2 】描述程 序规范，能描述更多关于程序正确性的性质。生成的p c c 使用类s c a p 1 5 的汇 编级验证框架。分离逻辑和s c a p 已经被用于实验室其它的研究课题，如垃圾收 集器 1 3 】、操作系统验 = j e 1 4 等的验证工作中。另外，这个项目罩首次研究了关 于自动定理证明、证明复用、验证条件化简等课题。 1 4 2 本文的工作和贡献 本文描述的第一部分工作是c c o m p 项目的一部分。在这个项目中，本文主 要关注源级的断言语言以及推理规则的设计，并实现相应的验证条件生成器；以 6 第1 章绪论 及如何简化生成的验证条件，删除其中的冗余项，使验证条件更易证明。 验证条件化简在先前的项目中并未涉及，但却是出具证明编译器中一个非常 重要的课题，在一些出具证明编译器系统中，尤其是规范使用经典霍尔逻辑描述 的系统中，由验证条件生成器生成的验证条件的规模较大，可能成为系统性能的 瓶颈。c c o m p 在验证条件生成过程中，及时地抛去证伪的命题，并在验证条件 生成后通过一个重写系统简化验证条件中的项并减少项的数目，从而得到了较简 化的验证条件。 ，本文描述的第二部分工作则是研究在一个源级包含程序规范的出具证明编 译器中，编译优化对程序规范的影响。实用的编译器会包含众多优化，以提高程 序执行的效率。先前关于出具证明编译器的项目较少研究编译优化的影响，但编 译优化是决定出具证明编译器是否能走向应用的关键因素之一。编译优化是一系 列程序变换，变换前的程序规范可能无法正确或充分地描述变换后的程序，为此 程序规范也应该随着代码优化一起转换。 本文将介绍如何在代码优化的同时转换程序规范，在一个包含多种优化的编 译器中将源级程序规范的约束准确而充分地施加于优化后的代码。这部分的工作 独立于协作的项目，且提出的方法有一定的通用性，与断言语言无关，可作为以 后关于包含代码优化出具证明编译器的研究基础。 本文介绍的两项工作的贡献分别为： 1 为c c o m p 设计了使用分离逻辑描述的断言语言，实现了验证条件生成 器；并实现了验证条件的化简一个重写系统以减小生成的验证条件规模。 2 实现了一个包含多种优化编译器原型系统，能利用数据流分析结果来变 换程序规范，使原规范的约束准确而充分地施加于优化后的代码。通过 研究数据流优化的基本行为，初步总结出了通用的转换模式。 在接下来的章节中，本文会分别对两项课题的问题、方法、结论、原型实现 等分别展开介绍和讨论。本文的第一章介绍国内外关于程序验证、出具证明编译 器以及源级验证系统的相关研究，以让读者了解本文的研究课题的研究背景，并 大概介绍本文的的主要工作。第二章介绍c c o m p 中断言语言、推理规则的设计、 验证条件生成器的设计和实现，第三章介绍验证条件化简。第四部分介绍出具证 明器中的编译优化和规范转换。最后给出对比和总结。 7 第2 章断言语言和验证条件生成 第2 章断言语言与验证条件生成 本章将介绍出具证明编译器c c o m p 中断言语言的设计，以及验证条件生成 器的设计和实现， c c o m p 的源语言c l i k e 的抽象语法树( a s t ) 过于复杂，因为过于复杂的 c l i k e 语法以及a s t 中包含了众多信息。而验证条件生成器是语法制导的符号演 算( s y m b o l i ce x e c u t i o n ) ，为了方便，本文为验证条件生成器专门设计了一个中间 表示v c g e n a s t 。这个中间表示和c l i k e 的a s t 一样，都是抽象语法树，但忽 略了一些不必要的信息而变得较简单，更利于验证条件生成器利用推理规则演算。 验证条件生成器首先转换c l i k e 的a s t 到这个简化的语法树，然后在此语法树上 推理演算，生成验证条件。 断言语言应该有足够的表达能力，以让用户能充分描述程序的性质。但断言 的设计会受到定理证明器自动证明能力的约束。表达能力越强，描述的性质越多， 越难以自动化证明。因此断言语言的设计经常要在表达能力和自动化证明两者之 问权衡。为c c o m p 设计的断言语言参考了源代码验证工具s m a l l f o o t 中断言语言 的设计，使用分离逻辑来描述程序性质。同时c c o m p 扩展了s m a l l f o o t 的断言语 言的表达能力：引入了更多的逻辑运算符、让用户自定义谓词。这样虽不能保证 完备性，但却大大扩展了断言语言的表达能力，使得用户描述更多的程序性质。 配合验证条件生成器和验证器，c c o m p 能验证比s m a l l f o o t 更复杂的程序和更复 杂的舰范。 验证条件生成器采用了最弱f j f 条件演算的方法，自前向后进行符号演算。因 为断言语言允许更多的逻辑运算符和自定义谓词，这给验证条件生成器带来一定 困难。为此采用了一些方法，比如在验证条件生成过程中调用证明器，根据证明 结果来采用不同的规则在推理规则罩增加了一条规则，让谓词在推理过程中根据 需要自动地展丌，而不需要人为干预。 c c o m p 采用了分离逻辑描述程序规范，这使得程序规范通常较为简练，而 且在验证条件生成过程中，及时地抛去证伪的命题。因此生成的验证条件的规模 不至于过大。结合第三章所描述的验证条件化简，解决了验证条件过大的问题， 使得验证条件较为简化，更易证明。 本章第一节会介绍用于v c 生成的抽象语法树。第二节介绍断言语言的设计， 以及其实现时的表示。第三节介绍规范的演算规则。第四节介绍验证条件生成器 的实现。 9 第2 章断言语言和验证条件生成 2 1 输入源语言 验证条件生成器的输入并不是源语言c l i k e ，因为在c l i k e 的语法树中包含了 许多不必要的信息，如位置信息以供类型检查时报错。这些信息在验证条件生成 时是不必要的。另外c l i k e 的语法树并不区分各种赋值语句。比如结构体里域的 读写、数组的某个位置元素的读写、以及普通的变量赋值，这些在c l i k e 的语法 树罩均表示为赋值语句，而这些赋值在验证条件产生时却分别对应不同的规则。 一些语法结构的语义过于复杂。比如表达式r n e x t n e x t ，这个表达式连续两 次访问结构体。多维数组访问页有同样的问题a i 】d 】，要两次访问内存。而v c g e n 确期望每个语句有较简单的语义，以比较容易地建立和推理规则的对应关系。 为了方便推理规则的设计以及验证条件生成器的实现，本文设计了一个中间 表示，叫做v c g e n a s t ，这个语法树拥有较简化的语言结构，在推导验证条件 时更容易建立起规则和语句一对一的关系。源语言先翻译到这个中问表示上，然 后再使用验证条件生成器生成验证条件。 这样做有另外一个好处：不仅c l i k e 的语法树能翻译到这个中间表示，其它 语言的的语法树也能翻译到这个表示。事实上在c c o m p 的实现中，中间代码 c m i n o r 语言也翻译到这个中间表示，使用同一个v c g e n 来生成验证条件。这样 就不必要因为源语言的变动而重新编写v c g e n 。 v c g e n a s t 中语句的定义如下： d a t as t m t = s s k i p s a s s i q ni d e n te x p r s c a l l ( m a y b ee x p r ) i d e n t 【e x p r 】 s n e wi d e n ti n t s f r e ei d e n ti n t s 1 0 0 k u pi d e n t i d e n te x p r s a r r a v l o o k u p 工d e n ti d e n te x p r s a r r a y m u a t a t e 工d e n ti n ti d e n t s m u a t a t ei d e n te x p r e x p r s if t h e n e l s ec o n d e x p r s t m t 】 【s t m t 】 s w h i l ea s s e r t i o nc o n d e x p r s t m t 】 s b r e a k s c o n ti n u e s r e t u r n ( m a y b ee x p r ) s g o t ol a b e l s 1 a b e ll a b e l ( m a v b ea s s e r t i o n ) 其中表达式的定义如下： 1 0 第2 章断言语言和验证条件生成 d a t ae x p r = e c o n s ti n t i e v a ri d e n t ie b i o pe x p rb i o pe x p r l e n e ge x p r t y p ec o n d e x p r = ( e x p r ，c o m p a r a t i o n ，e x p r ) d a t ac o m p a r a t i o n = e qln e i g t i g e l l t i l e 这个中间表示既有比较高级的控制结构如w h i l e 语句，又有比较低级的控制 结构如g o t o ，所以较高级的语言c l i k e 或较低级c m i n o r 的语言均可翻译成此中 间表示。其中w h i l e 含有循环不变式，而基本块的入口也可能含有断言，包含在 s l a b e l 中。 一个函数由函数名、参数、函数的前后条件以及一个语句序列来构成。一个 程序由若干个函数组成。中间表示中函数的定义如下，其中a s s e r t i o n 是断占， 将在下一节描述： d a t af u n c = f i d：i d e n t p a r a s：【i d e n t 】 s t m t s ： s t m t 】 p r e ：a s s e r t i o n p o s t ：a s s e r t i o n 2 2 断言语言 2 2 i 断言语言的定义 分离逻辑( s e p a r a t i o nl o g i c ) 为包含指针的程序提供了一种推理方式，因为 在规范中只关注程序当前模块正确执行相关的资源( 比如内存堆) ，而不必提及 其它的模块使用的资源，因此常常具有比先前的其他形式化的方式更简洁的规范， 以及更简短的证明 1 2 】。c c o m p 使用分离逻辑的一个片段来定义断言语言，这个 定义事实上是对s m a l l f o o t 的断言语言。的一个扩展，主要增强了逻辑表达式和自 定义谓词。图2 1 是断言语言的定义。 第2 章断言语言和验证条件生成 i i ：= f a l s ei t r u eieoeli iai i o ：= = i i l i ：= e 卜eip r e d ( 司i 宰ie m p f ：= i i ： a：=fvf 图2 1 断言语言定义 公式( f o r m u l a ) 由两部分组成，分别为p u r ef o r m u l a 和s p a t i a lf o r m u l a ，分 别是由、连接起来的纯布尔类型的表达式和由事连接起来的关于堆( h e a p ) 的谓词 而构成。二元运算符宰是分离逻辑中的符号，叫做分离连接符( s e p e r a t i n g e o n j u n c t i o n ) ，表示内存堆可以被分成两个不相交的部分，两个部分分别能让连 接符的两个参数所定义的断言成立。e m p 表示堆为空。箭头符号一是一个二元运 算符，接受两个参数，左边参数是一个地址，右边参数是一个值。断言p v 表 示内存堆只定义了p 一个地址，而p 指向的内容的值和v 相等。 上述的构造参考了s m a l l f o o t 中的断言语言的定义，但这罩断言语言的定义 对s m a l l f o o t 中的断言语言进行了几个扩展： 1 用户自定义谓词。p r e d 是用户自定谓词，可接受任意数量参数，描述堆 的性质。而在s m a l l f o o t 只有l i s t ，t r e e 等有限个固定的数据结构谓词。 2 增强了逻辑运算符。s m a l l f o o t 的二元逻辑运算符只有相等和不等关系= 和，而c c o m p 的断言语言中则有各种不等关系，如 、。 3 断言是由若干公式的析取。而s m a l l f o o t 中的断言只是f o r m u l a ，而不能 是由析取运算符v 连接的若干个公式。 这些扩展大大地增强了断言语言的表述能力。 系统允许用户使用断言语言自定义谓词，谓词的定义如下j p r e d d e f ：= e x i s t sef o r m u l aip r e d d e fvp r e d d e f 用户自定义谓词由若干个由分支析取而成，每个分支由一个公式构成，表示 一个可能的c a s e 。每一个公式前可能有存在量词引入一些变量。下面是一个用户 自定义谓词的示例，分别定义了表段和表。 p r e d1 s e g( s t r t a c tl i s t n o d e h e a d ； s t r u c t1 i s t n o d e t a i l ) =head=taili e m p t y vj ( s t r u e l ：l i s t n o d e n ) ， h e a d t aj 1 lh e a d 卜( ，n ) l s e g ( n ，t a i z ) p r e dl i s t ( s t r u c tl i s t ：n o d e r o o t ) = 1 s e g ( r o o t ，n u l l ) 1 2 第2 章断言语言和验证条件生成 上述的标段i s e g 有两个参数，分别表示头指针和尾指针。标段或者为空，或 者为一个头节点和其后续标段组合而成，要求头节点里的n e x t 域要和后续表段 的头指针相同。而链表则是用表段来表示，其尾指针为n u l l ，表示最后一个节点 的n e x t 域为n u l l 。注意，上面定义中标段的参数h e a d 和t a i l 用分号分开，而不 是逗号。这是因为验证条件生成时需要展开谓词，这个符号有特殊作用。本文将 在下节介绍这个问题。 因为c c o m p 的断言语言扩展了逻辑运算符，使