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

• 作者: 杨萍 王生原
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: CompCert 形式化验证的编译器 目标代码生成 编译器重定向
• 年，卷（期）: 2020,（9）
• 所属期刊栏目: 计算机软件
• 页码范围: 17-23
• 页数: 7页
• 分类号: TP314
• 语种: 中文
• DOI: 10.11896/jsjkx.200400018

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王生原		33	235	8.0	14.0
2	杨萍		5	10	3.0	3.0