The Trusted CerCo Cost Annotating Compiler is a (partially) certified compiler from a large subset of C to the object code of the 8051/8052 processor family. The code of the compiler is automatically extracted from a formalization in the proof assistant Matita of: 1) the semantics of the source code; 2) the semantics of the target code; 3) the semantics of a sequence of intermediate languages; 4) the code that implements the translation between consecutive languages in the compilation chain; 5) the proof that every compilation step preserves the semantics of the code, i.e. that the output code simulates the input. The main peculiarity of the compiler is that of returning in output also a copy of the source code annotated with the exact cost in clock cycles of every O(1) block. This information can later be exploited to bound the execution cost of the program. To obtain and certify this information, the formalization in Matita also includes an emulator of the 8051 microprocessor detailed to the clock cycle. The compiler also includes an optimizing assembler that tackles the branch displacement optimization problem. The code of the Trusted CerCo Cost Annotating Compiler is a formalization and a reimplementation from scratch of the CerCo Cost Annotating Compiler. Not every implementation available in the latter has been ported to the former yet.
J. Boender, B. Campbell, I. Gardner, J. McKinna, D. P. Mulligan, M. Piccolo, et al. (2013). Trusted CerCo Cost Annotating Compiler.
Trusted CerCo Cost Annotating Compiler
SACERDOTI COEN, CLAUDIO;
2013
Abstract
The Trusted CerCo Cost Annotating Compiler is a (partially) certified compiler from a large subset of C to the object code of the 8051/8052 processor family. The code of the compiler is automatically extracted from a formalization in the proof assistant Matita of: 1) the semantics of the source code; 2) the semantics of the target code; 3) the semantics of a sequence of intermediate languages; 4) the code that implements the translation between consecutive languages in the compilation chain; 5) the proof that every compilation step preserves the semantics of the code, i.e. that the output code simulates the input. The main peculiarity of the compiler is that of returning in output also a copy of the source code annotated with the exact cost in clock cycles of every O(1) block. This information can later be exploited to bound the execution cost of the program. To obtain and certify this information, the formalization in Matita also includes an emulator of the 8051 microprocessor detailed to the clock cycle. The compiler also includes an optimizing assembler that tackles the branch displacement optimization problem. The code of the Trusted CerCo Cost Annotating Compiler is a formalization and a reimplementation from scratch of the CerCo Cost Annotating Compiler. Not every implementation available in the latter has been ported to the former yet.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
