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.

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.
2013
R. M. Amadio; N. Ayache; Y. Régis-Gianas; R. Saillard; B. Campbell; D. Mulligan; P. Tranquilli; C. Sacerdoti Coen
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/399544
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact