论文部分内容阅读
PCC的数组边界检查存在着由于无法确定数组下标表达式符号值的范围,而造成拒绝执行一些安全的移动代码等问题.本文给出的一种数组边界检查的优化及生成算法,不仅能够比较好地解决了这一问题,同时还生成了循环不变式注解中的条件谓词.我们设计的编译器--认证编译器--已经实现了这些算法,并完成了从用C编程语言的类型安全子集编写的源程序到携带注解的Intel x86/linux汇编语言程序的编译过程.由于基于语言安全策略系统的证明是建立在携带注解的代码基础之上的,因此该认证编译器中实现的算法在移动代码安全检查中非常有用