出具证明编译器中验证条件化简和编译优化的研究

摘要

程序验证用逻辑证明的方法证明程序满足其规范，是实现安全性的重要方法。出具证明编译器(Certifying Compiler)是编译器与验证器的结合。本文描述的出具证明编译器项目CComp让用户给出描述程序正确性的规范，并在源代码使用霍尔逻辑风格的推理规则产生验证条件(Verification Condition，VC)，经由证明器证明后产生证明项。然后将源代码和规范转化成底层的汇编代码和其上的规范，并利用源级证明项生成汇编代码级证明，最终生成携带证明代码。
　　 CComp由多人协作完成，本人承担项目中的断言语言设计以及验证条件生成和化简工作。实验室先前的项目PointerC[4]，过大的验证条件规模成为系统性能的瓶颈。因此CComp采用一系列的措施来化简VC，删除其中的冗余。
　　 实用的编译器会包含众多优化，以提高程序执行的效率。编译优化是一系列程序变换，对于出具证明编译中包含规范的程序，变换前的程序的规范可能无法正确或充分地描述变换后的程序，为此程序规范也应该随着代码优化一起转换。目前关于出具证明编译器的项目较少研究编译优化的影响，但编译优化是决定出具证明编译器是否能走向应用的关键因素之一。
　　 本文通过分析研究，针对以上两个重要问题分别提出了相应的解决方案，并实现了原型系统验证方法的合理性。本文的主要贡献为：
　　 1.为CComp项目设计了使用分离逻辑描述的断言语言和其推理规则，实现了相应的验证条件生成器；设计并实现了一个重写系统，实现了验证条件的化简，解决了验证条件过大的问题。
　　 2.通过研究数据流优化的基本行为，实现了一个包含多种优化和相应规范转换的编译器原型系统，利用数据流分析结果来变换规范，使各循环的循环不变式经过调整后，能作为优化后程序的相应循环的循环不变式。并初步总结出了通用的转换模式。
　　 本文第一部分工作是CComp项目的一部分。第二部分工作则较为独立，可作为未来对包含代码优化的出具证明编译器的研究基础。

目录

文摘

英文文摘

声明

第1章绪论

1.1程序验证与霍尔逻辑

1.2源级验证工具

1.3携带证明代码与出具证明编译器

1.4本文所介绍的工作

1.4.1 CComp

1.4.2本文的工作和贡献

第2章断言语言与验证条件生成

2.1输入源语言

2.2断言语言

2.2.1断言语言的定义

2.2.2断言语言的表示

2.3验证条件的生成规则

2.3.1演算规则

2.3.2规则的应用

2.4验证条件生成器的实现

第3章验证条件化简

3.1重写系统

3.2系统实现

3.3进一步化简

第4章代码优化与规范转换

4.1编译优化对断言的影响

4.2出具证明编译中的代码优化

4.3数据流优化与断言

4.3.1数据流优化的基本行为

4.3.2优化示例

4.4数据流优化与规范转换

4.4.1基本方法

4.4.2举例

4.4.3转换流程

4.4.4方法的合理性

4.5规范化简

4.6原型实现

4.6.1前端及中间语言的实现

4.6.2优化及断言转换的实现

4.6.3实验结果

第5章相关工作和总结

参考文献

致谢

攻读学位期间发表的论文及其它科研成果