出具证明编译器中代码优化与程序规范转换  

Code Optimization and Specification Transformation in Certifying Compiler

作　　者：范大威[1,2] 李兆鹏[1,2] 蒋信予[1,2] 

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230026 [2]中国科学技术大学苏州研究院软件安全实验室,江苏苏州215123

出　　处：《小型微型计算机系统》2011年第7期1400-1405,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(90718026;60928004)资助

摘　　要：出具证明编译器在软件安全研究得到越来越多的关注,是程序验证研究的一个重要方向.但目前关于出具证明编译器的研究主要是在程序逻辑设计和定理自动化证明方面,很少关注编译优化对规范的影响.而编译优化是决定出具证明编译器是否能走向应用的关键因素之一.通过研究数据流优化的基本行为,提出利用数据流分析结果来变换规范的方法,以使原规范的约束准确而充分地施加于优化后的代码,并实现了一个包含多种优化和相应规范转换的编译器原型系统,展示了方法的可行性.As an important research field of program verification, certifying compiler is an increasing concern by many researchers of software security. However, current researches mostly focus on the design of program logic and automated theorem proving, while code optimization which we believe is significant for certifying compiler to become practical, is less concerned by the community. In this paper, we propose a dataflow analysis based method to transform specification to pass the constraint of original specification to the optimized code. We also develop a prototype compiler with multiple optimizations to demonstrate the feasibility of our approach.

关 键 词：规范转换 代码优化 数据流分析 出具证明编译器 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]