A Calculus for Unreachable Code
<|reference_start|>A Calculus for Unreachable Code: 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.<|reference_end|>
@article{zhong2024a,
    title={A Calculus for Unreachable Code},
    author={Peter Zhong and Shu-Hung You and Simone Campanoni and Robert Bruce
  Findler and Matthew Flatt and Christos Dimoulas},
    journal={arXiv preprint arXiv:2407.04917},
    year={2024},
    archivePrefix={arXiv},
    eprint={2407.04917},
    primaryClass={cs.PL}
}