Current compilers implement security features and optimizations that require nontrivial semantic reasoning about pointers and memory allocation: the program after the insertion of the security feature, or after applying the optimization, must simulate the original program despite a different memory layout. In this article, we illustrate such reasoning on pointer allocations through memory extensions and injections, as well as fine points on undefined values, by explaining how we implemented and proved correct two security features (stack canaries and pointer authentication) and one optimization (tail recursion elimination) in the CompCert formally verified compiler.

翻译：当前编译器实现的安全特性和优化需要对指针及内存分配进行非平凡的语义推理：在插入安全特性或应用优化后，尽管内存布局发生变化，程序仍需模拟原始程序的行为。本文通过解释如何在形式化验证编译器CompCert中实现并证明两项安全特性（栈保护与指针认证）及一项优化（尾递归消除）的正确性，阐述了通过内存扩展与注入进行指针分配时的此类推理过程，以及未定义值相关的细节要点。