一个出具证明编译器后端的设计与实现

Design and Implementation of Certifying Compiler Back End

设计并实现一个类C语言PointerC的出具证明编译器后端。该后端采用最强后条件演算同步处理整型断言和指针断言实现整型验证条件和指针验证条件的证明,能够完全自动地产生目标级程序的指针安全性证明,处理常见递归数据结构中的非一致性别名问题。后端包括独立的定理检查器,能够检验携证明代码的完整性。

This paper introduces the design and implementation of a certifying complier back end for a C-like language. PointerC. The back end adopts the strongest post-conditions calculation for both integer assertion and pointer assertion synchronously, and proofs the verification conditions involving integers and pointers. It generates the proofs of pointer safety at the assembly level full-automatically, and solves the problem of the non-uniform alias analysis in commonly used data structures. The proof checker, which checks the integrity of proof-carrying code, is included in the back end.