Title: The CakeML Compiler Explorer Visualizing how a verified compiler transforms expressions
Abstract: This report documents the development of a compiler explorer that provides insight
to the inner workings of the CakeML compiler. The compiler explorer can interactively
present information about an expression’s origin and descent at different
stages of compilation. The compiler explorer consists of a web application presenting
the expression information and the CakeML compiler with our additions that
enable the tracking of expressions. The CakeML compiler is developed in the HOL4
system; the web application user interface in React and the web server in PHP.
Getting insight into the inner workings of a compiler is difficult. Several tools
exist for other compilers that either explain how a section of the source code relates
to the compiled machine code or provide snapshots of different compiler phases.
While these features are useful by themselves, combining them would give better
insight into the compiler’s transformations. The compiler explorer provides such a
combination.
The gained insight provided by the compiler explorer can both help developers
of the CakeML compiler find new optimizations and improve education about the
compiler.
Publication Year: 2017
Publication Date: 2017-01-01
Language: en
Type: dissertation
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot