Adapting Verified Compilation for Target-Language Errors

Abstract

Verified compilers have the potential to greatly improve users’ trust in their code by providing machine-checked proofs of compiler correctness. In recent years they have become increasingly sophisticated and practical, compiling programs from convenient high-level programming languages to realistic target architectures and platforms. Ideally, compiler correctness requires every externally visible behavior of the compiled code to also be a valid behavior of the source it was compiled from. However, modern compilers often translate between languages with very different semantics; in particular, the target language may have error conditions, such as memory exhaustion, integer overflow, and process interruption, that are not expressed or modeled at the source level. In this work, we explore and evaluate the design space faced by verified compiler writers when adapting their systems for target-language errors. We provide template compiler correctness theorems that account for target-language errors in different ways. We consider a variety of target-language errors that appear in real-world target platforms, examining ways to modify each component of the verified compiler to adapt for them. Among these errors, we include failure modes of external components of the system that affect the running compiled code, such as process interruption and I/O device failure. We describe adaptations to a standard compiler correctness proof technique that allow verified compiler writers to prove one of our proposed correctness theorems when the target language contains limited nondeterminism introduced by target-language errors. Finally, we discuss ways to weaken a traditional compiler correctness statement to obtain guarantees that hold for all executions, including those that encounter target-language errors. Our systematization helps verified compiler writers decide how to appropriately account for target-language errors, allowing them to expose correctness guarantees that more accurately reflect the real-world behavior of compiled code.