On the Construction of Correct Compiler Back-Ends: An ASM-Approach
Дата
Авторы
Zimmermann,Wolf
Gaul,Thilo
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
Existing works on the construction of correct compilers have at least one of the following drawbacks: (i) correct compilers do not compile into machine code of existing processors. Instead they compile into programs of an abstract machine which ignores limitations and properties of real-life processors. (ii) the code generated by correct compilers is orders of magnitudes slower than the code generated by unverified compilers. (iii) the considered source language is much less complex than real-life programming languages. This paper focuses on the construction of correct compiler backends which generate machine-code for real-life processors from realistic intermediate languages. Our main results are the following: (i) We present a proof approach based on abstract state machines for bottom-up rewriting system specifications (BURS) for back-end generators. A significant part of this proof can be parametrized with the intermediate and machine language. (ii) The performance of the code constructed by our approach is in the same order of magnitude as the code generated by non-optimizing unverified C-compilers.
Ключевые слова
Compiler , Operational Semantics , Verification , Abstract State Machine , Back-End Generator