CompCert编译器目标代码生成机制分析

摘要：

CompCert是著名的C语言可信编译器,是经过形式化验证的编译器的杰出代表,近年来被广泛应用于学术界和工业界的许多研发工作中.CompCert编译器的当前版本支持多种目标机结构.文中对CompCert编译器目标代码生成机制进行剖析,主要介绍其设计逻辑、翻译过程、语义保持性以及代码结构,并给出了CompCert编译器重定向设计的要点.文中工作有助于实现CompCert重定向,比如实现面向重要国产处理器的后端.

关键词：CompCert、形式化验证的编译器、目标代码生成、编译器重定向

所属期刊栏目：47

分类号：TP314(计算技术、计算机技术)

资助基金：国家核高基重大专项2017ZX01030-301-003

在线出版日期：2020-09-25（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：17-23