Heiko Becker

When working with optimizing compilers, it is sometimes beneficial to inspect intermediate results to figure out whether an optimization has fired or not. While taking a dive into LLVM’s fast-math semantics I recently encountered a subtle quirk that may affect others as well.

CakeML is an end-to-end verified compiler for a dialect of SML. Until recently it was not possible to write CakeML programs that used floating-point operations. While floating-point arithmetic was implemented throughout the backend of the compiler, it was not exposed on the frontend. Over the last weeks I have worked on a frontend implementation for CakeML, making floating-point arithmetic accessible to the end user.

When using gcc or clang, programmers commonly use so-called “fastmath” optimizations to aggressively optimize floating-point programs. So far, these optimizations have been out of reach for verified compilers like CompCert or CakeML.