Thu 18 Jun 2026 11:00 - 11:20 at Flatirons 4 - Semantics and Hyperproperty Reasoning Chair(s): Derek Dreyer

LLVM’s intermediate representation (IR) has two deferred undefined behavior (UB) values: undef and poison. The existence of these two values has been a persistent source of bugs. Reasoning about the correctness of analyses and optimizations for the regular cases is already tricky; ensuring that these are sound for all UB cases is highly non-trivial. Undef values, in particular, are one of the most misunderstood concepts of LLVM IR. On paper, the definition is simple: they represent an arbitrary value of the underlying type, and can yield a different value each time they are observed. However, this property makes even simple algebraic rewrites, such as replacing 2 × y with y + y, unsound in LLVM. Because reasoning about undef is hard, and the benefits of having it are limited, we have set a roadmap to eliminate it altogether from LLVM IR. The last remaining use of undef is the value of uninitialized memory, which has implications on the lowering of bitfields, as well as raw data copies and comparisons. In this paper, we propose an extension to LLVM IR that includes a raw memory value type and a freezing load. We show that these two constructs are sufficient to replace the remaining uses of undef in LLVM. Our implementation shows that these changes have minimal impact on both run-time and compile-time performance. By removing the final hurdle to eliminating undef from LLVM IR, this work paves the way for a simpler semantic model and easier reasoning about the soundness of IR analyses and optimizations.

Thu 18 Jun

Displayed time zone: Mountain Time (US & Canada) change

11:00 - 12:40
Semantics and Hyperproperty ReasoningPLDI Research Papers at Flatirons 4
Chair(s): Derek Dreyer MPI-SWS
11:00
20m
Talk
Towards Removing Undef Values from LLVM IRDistinguished Paper
PLDI Research Papers
Pedro Lobo INESC-ID; Instituto Superior Técnico - University of Lisbon, John McIver Virginia Tech, George Mitenkov Aptos, Juneyoung Lee AWS, Kirshanthan Sundararajah Virginia Tech, Nuno P. Lopes INESC-ID; Instituto Superior Técnico - University of Lisbon
DOI Pre-print
11:20
20m
Talk
The Downgrading Semantics of Memory Safety
PLDI Research Papers
René Rydhof Hansen Aalborg University, Andreas Stenbæk Larsen Aarhus University, Aslan Askarov Aarhus University
DOI
11:40
20m
Talk
Causality and Semantic Separation
PLDI Research Papers
Anna Zhang Massachusetts Institute of Technology, Qinglan Luo Wellesley College; Massachusetts Institute of Technology, London Bielicke University of California at Los Angeles, Eunice Jun University of California at Los Angeles, Adam Chlipala Massachusetts Institute of Technology
DOI Pre-print Media Attached
12:00
20m
Talk
Hyper Separation Logic
PLDI Research Papers
Trayan Gospodinov INSAIT at Sofia University St. Kliment Ohridski, Peter Müller ETH Zurich, Thibault Dardinier EPFL
DOI
12:20
20m
Talk
Pantomime: Constructive Leakage Proofs via Simulation
PLDI Research Papers
Robin Webbers Vrije Universiteit Amsterdam, Robert Schenck Northeastern University, Wind Wong Vrije Universiteit Amsterdam, Kristina Sojakova Vrije Universiteit Amsterdam, Klaus von Gleissenthall Vrije Universiteit Amsterdam
DOI