A Calculus for Unreachable Code

TL;DR

This paper introduces a formal calculus for unreachable code, providing a small set of rules that model compiler transformations related to unreachable segments, enhancing understanding and correctness verification.

Contribution

It presents the first formal calculus for unreachable code, capturing compiler transformations through simple, well-defined rewriting rules and proving their correctness.

Findings

Rules enable deletion of downstream unreachable code

Rules allow removal of effect-free upstream code

Correspondence with real compiler transformations in Racket and LLVM

Abstract

In Racket, the LLVM IR, Rust, and other modern languages, programmers and static analyses can hint, with special annotations, that certain parts of a program are unreachable. Same as other assumptions about undefined behavior; the compiler assumes these hints are correct and transforms the program aggressively. While compile-time transformations due to undefined behavior often perplex compiler writers and developers, we show that the essence of transformations due to unreachable code can be distilled in a surprisingly small set of simple formal rules. Specifically, following the well-established tradition of understanding linguistic phenomena through calculi, we introduce the first calculus for unreachable. Its term-rewriting rules that take advantage of unreachable fall into two groups. The first group allows the compiler to delete any code downstream of unreachable, and any effect-free code upstream of unreachable. The second group consists of rules that eliminate conditional expressions when one of their branches is unreachable. We show the correctness of the rules with a novel logical relation, and we examine how they correspond to transformations due to unreachable in Racket and LLVM.