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

杨萍; 王生原

首页> 中文期刊> 《计算机科学》 >CompCert编译器目标代码生成机制分析

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

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

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

著录项

来源
《计算机科学》 |2020年第9期|17-23|共7页
作者
杨萍; 王生原;
展开▼
作者单位

北京语言大学信息科学学院北京 100083;

清华大学计算机系北京 100084;

展开▼
原文格式 PDF
正文语种 chi
中图分类编译程序、解释程序;
关键词
CompCert; 形式化验证的编译器; 目标代码生成; 编译器重定向;

相似文献

中文文献
外文文献
专利

1. 在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程 [J] . 李凌 ,李璜华 ,王生原 . 计算机科学 . 2020,第006期
2. 面向媒体处理器可重定目标编译器的代码生成 [J] . 琚小明 ,张召 ,史册 . 计算机工程 . 2009,第011期
3. 多目标交叉编译技术——GCC与Zephyr编译器构造的分析与比较 [J] . 戴桂兰 ,张素琴 ,田金兰 . 计算机科学 . 2002,第006期
4. 构建高校学生党员保持先进性长效机制的思考与探索——从长效机制的目标、实施、保障三个层面分析 [J] . 姜维 . 吉林省教育学院学报.学术版 . 2007,第002期
5. “双碳”目标下的电能价值分析与市场机制设计 [J] . 陈皓勇 . 发电技术 . 2021,第002期
6. 基于硬件cache锁机制的Java虚拟机即时编译器优化 [C] . 敖琪 ,蔡嵩松 ,王剑 . 2011年第17届全国信息存储技术大会(IST 2011) . 2011
7. C编译器中间代码生成及其后端的设计与实现 [A] . 李磊 . 2016

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

摘要

著录项

相似文献

相关主题

期刊订阅