The Cost Annotating Compiler is a special compiler from a very large subset of Standard C to the object code for the 8051/8052 microprocessor family. The peculiarity of the compiler is that of returning also a copy of the source program annotated with the exact cost (in clock cycles) of the execution of every O(1) program fragment. This information can be later exploited to compute precise upper bounds for the execution time of the program on generic inputs. The compiler is entirely written in OCaml. It performs the usual most basic analyses and optimizations (e.g. constant propagations, register allocation, liveness analysis, etc.) and some more complex loop optimizations (hoisting, unrolling). It also includes an optimizing assembler for the 8051. In particular, the assembler tackles the branch displacement problem with an iterative approximation algorithm.
R. M. Amadio, N. Ayache, Y. Régis-Gianas, R. Saillard, B. Campbell, D. Mulligan, et al. (2013). CerCo Cost Annotating Compiler.
CerCo Cost Annotating Compiler
SACERDOTI COEN, CLAUDIO
2013
Abstract
The Cost Annotating Compiler is a special compiler from a very large subset of Standard C to the object code for the 8051/8052 microprocessor family. The peculiarity of the compiler is that of returning also a copy of the source program annotated with the exact cost (in clock cycles) of the execution of every O(1) program fragment. This information can be later exploited to compute precise upper bounds for the execution time of the program on generic inputs. The compiler is entirely written in OCaml. It performs the usual most basic analyses and optimizations (e.g. constant propagations, register allocation, liveness analysis, etc.) and some more complex loop optimizations (hoisting, unrolling). It also includes an optimizing assembler for the 8051. In particular, the assembler tackles the branch displacement problem with an iterative approximation algorithm.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.