Certified Run-Time Code Generation

Abstract. Cyclone is a programming language that provides explicit support for dynamic specialization based on runtime code generation. To generate specialized code quickly, our Cyclone compiler uses a tem-plate based strategy in which pre-compiled code fragments are stitched together at runtime. To achieve good performance, the pre-compiled frag-ments must be optimized. This paper describes a principled approach to achieving such optimizations. In particular, we generalize standard ow-graph intermediate representations to support templates, dene a formal mapping from (a subset of) Cyclone to this representation, and describe a data- ow analysis framework that supports standard optimizations. This extended version contains two mappings to the intermediate repre-sentation, a less formal one that emphasizes the novelties of our transla-tion strategy and a purely functional one that is better suited to formal reasoning.