Retrofitting Symbolic Holes to LLVM IR
summary
Implements untyped symbolic holes inside LLVM IR by encoding holes as calls to uninterpreted functions and introducing an unknown-type marker whole.t, plus intrinsic fallbacks for operations so arithmetic and bitwise ops can exist before types are chosen. Adds a safe primitive that replaces a hole with a concrete value and propagates its type by reconstructing affected IR (a typed RAUW-like operation). Integrates with LLVM passes, preserves dependency and use-before-def checks, and enables direct inlining of synthesized replacements into legacy code.
AI-written summary · about
chapters (5)
- 0:00Start
- 0:34What Is Solver Aided Programming
- 5:43Llvm Intermediate Representation
- 9:32Design Goals
- 15:20Implementation for the Add Function
related talks
20mTowards Removing Undef Values from LLVM IR
22mReconciling High-level Optimizations and Low-level Code in LLVM
23mInductive Program Synthesis by Meta-Analysis-Guided Hole Filling
06mLightning Talk: Keeping Up to LLVM IR: An Introduction to LLVM IR
29mPartially Evaluating Symbolic Interpreters for All
01h 05mSemantic Intermediate Representations for Sound Language Interoperability
16mSemiring Optimizations: Dynamic Elision of Expressions with Identity and Absorbing Elements
01h 05mAll the Languages Together