CerCo Cost Annotating Compiler
Roberto M. Amadio, Ayache Nicholas, Y. Régis Gianas, Ronan Saillard, B. K. Campbell, Dominic P. Mulligan, Paolo Tranquilli, Claudio Sacerdoti Coen · Archivio istituzionale della ricerca (Alma Mater Studiorum Università di Bologna) · 2013
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.