Vellvm - Verifying the LLVM
summary
Vellvm formalizes LLVM IR semantics in Coq, extracts an OCaml interpreter that runs real .ll files, and implements a verified register‑promotion pipeline (a mem2reg variant) that plugs into LLVM. The work uses QuickChick and C Smith (which earlier found 202 LLVM bugs) to test and compare, shows machine‑checked proofs preventing miscompilations, and exposes heavy proof‑engineering costs and slower compiler‑build performance.
AI-written summary · about
chapters (21)
- 0:00Intro
- 0:22Collaborators
- 0:41PLAN • LLVM Intermediate Representation
- 1:27LLVM Compiler Infrastructure
- 7:01Other LLVM IR Features
- 8:49But... it's complex
- 9:47One Example: undef
- 14:03Interactions with Optimizations
- 15:37What's the problem?
- 17:32Compiler Bugs
- 20:41Deep Specifications
- 21:33Inspiration: CompCert
- 23:34The Vellvm Project
- 24:06Vellvm Framework
- 25:02LLVM IR Semantics
- 26:33Writing Interpreters in Coq
- 28:03Interaction Trees
- 30:47LLVM Interpreter in Cog
- 34:27mem2reg register promotion
- 36:35Caveats
- 38:55Getting started with Cog
related talks
16mImprovements to RISC-V Vector code generation in LLVM
48mWriting a compiler with LLVM
57mLLVM Optimization Remarks
39mDemystifying LLVM: Writing Your First Compiler - The Good, The Bad, The Ugly
01h 03mto pass and return, the story of functions, values and compilers
28mTshepang Lekhonkhobe: Behind The Scenes Of Producing An Executable
01h 01mVal: A Safe Language to Interoperate with C++
18mVerus: Verifying Rust Programs using Linear Ghost Types