Skip to content

References — Chapter 13 · Local Optimization & Transformation Correctness

Every source this chapter cites, grouped by kind. Lessons cite entries inline as [KEY]; each entry says why and when to read it. Core reading marks the entries the chapter assumes you will open.

Foundational and research papers

  • [AJU77] Alfred V. Aho, Stephen C. Johnson, and Jeffrey D. Ullman. Code Generation for Expressions with Common Subexpressions. Journal of the ACM 24(1), pp. 146–160, 1977.
    Why and when: Shows that generating optimal code from a DAG (unlike from a tree) is NP-complete, the reason block reassembly uses heuristics (Lesson 13.5 §5).
    Note: ACM Digital Library.
    Cited in: overview, 05-value-numbering-and-dags

  • [BA06] Sorav Bansal and Alex Aiken. Automatic Generation of Peephole Superoptimizers. ASPLOS XII, pp. 394–403, 2006.
    Why and when: Enumerate all short sequences once, index them by fingerprint, and harvest proven window→replacement rules from training programs (Algorithm 13.3.4). Read §3–4 after Lesson 13.3.
    Note: ACM Digital Library (ASPLOS '06).
    Cited in: overview, 03-superoptimization

  • [BB68] Jean-Loup Baer and Daniel P. Bovet. Compilation of Arithmetic Expressions for Parallel Computations. Proc. IFIP Congress 1968, pp. 340–346, 1968.
    Why and when: Early use of associativity and commutativity to reduce the height of expression trees for parallel evaluation (Lesson 13.6 §1). Historical.
    Note: IFIP Congress proceedings (North-Holland).
    Cited in: overview, 06-reassociation

  • [BC94] Preston Briggs and Keith D. Cooper. Effective Partial Redundancy Elimination. PLDI 1994, pp. 159–170, 1994.
    Why and when: Core reading. The origin of rank-based global reassociation (Definition 13.6.2, Algorithm 13.6.3): it reorders expressions so that partial redundancy elimination and code motion find more. Read the reassociation sections after Lesson 13.6.
    Note: ACM Digital Library (PLDI '94).
    Cited in: overview, 04-canonicalization-and-rewriting, 06-reassociation

  • [BCS97] Preston Briggs, Keith D. Cooper, and L. Taylor Simpson. Value Numbering. Software: Practice and Experience 27(6), pp. 701–724, 1997.
    Why and when: Local, superlocal, dominator-based and hash-based global value numbering compared experimentally. Read after Lessons 13.1 and 13.5 for the scope variants.
    Note: Wiley Online Library.
    Cited in: overview, 01-scopes-and-constant-folding, 05-value-numbering-and-dags

  • [Ber86] Robert Bernstein. Multiplication by Integer Constants. Software: Practice and Experience 16(7), pp. 641–652, 1986.
    Why and when: The search for the cheapest shift/add/subtract sequence for x * C that compilers adapted (Lesson 13.7 §1, §6). Read after Algorithm 13.7.2.
    Note: Wiley Online Library.
    Cited in: overview, 07-strength-reduction-and-division

  • [Bre74] Richard P. Brent. The Parallel Evaluation of General Arithmetic Expressions. Journal of the ACM 21(2), pp. 201–206, 1974.
    Why and when: Any expression with n operations can be evaluated in O(log n) parallel steps using distributivity too (Lesson 13.6 §6). Read after Corollary 13.6.11.
    Note: ACM Digital Library.
    Cited in: overview, 06-reassociation

  • [CFRWZ91] Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM TOPLAS 13(4), pp. 451–490, 1991. doi:10.1145/115372.115320
    Why and when: Besides SSA, the paper's dead-code elimination by marking from effects with control dependence is the "aggressive DCE" of Lesson 13.5 §6. Read §7 after Lesson 13.5.
    Cited in: 05-value-numbering-and-dags

  • [DF80] Jack W. Davidson and Christopher W. Fraser. The Design and Application of a Retargetable Peephole Optimizer. ACM TOPLAS 2(2), pp. 191–202, 1980.
    Why and when: Peephole rules derived from a machine description and applied to register transfers, the ancestor of GCC's combiner. Read after Lesson 13.2 §6 for the retargetable variant.
    Note: ACM Digital Library.
    Cited in: overview, 02-peephole-engines

  • [GJTV11] Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. Synthesis of Loop-free Programs. PLDI 2011, pp. 62–73, 2011.
    Why and when: Component-based synthesis with an SMT solver and counterexample-guided refinement, the technique Souper's synthesis builds on (Algorithm 13.3.6). Read §3 after Lesson 13.3.
    Note: ACM Digital Library (PLDI '11).
    Cited in: overview, 03-superoptimization

  • [GK92] Torbjörn Granlund and Richard Kenner. Eliminating Branches using a Superoptimizer and the GNU C Compiler. PLDI 1992, pp. 341–352, 1992.
    Why and when: The GNU superoptimizer and how its branch-free sequences went into GCC's code generator. Read after Lesson 13.3 §6; the tool is the one run in the Lesson 13.3 box.
    Note: ACM Digital Library (PLDI '92).
    Cited in: overview, 03-superoptimization

  • [GM94] Torbjörn Granlund and Peter L. Montgomery. Division by Invariant Integers using Multiplication. PLDI 1994, pp. 61–72, 1994. doi:10.1145/178243.178249
    Why and when: Core reading. The theorem behind every compiler's division by a constant (Theorem 13.7.4) and the signed and exact-division variants. Read §4 (unsigned) with Lesson 13.7 §2 and §5 for the signed case.
    Cited in: overview, 07-strength-reduction-and-division

  • [Gol76] Martin Charles Golumbic. Combinatorial Merging. IEEE Transactions on Computers C-25(11), pp. 1164–1167, 1976.
    Why and when: Merging with a max-plus cost, the setting of the greedy proof of Theorem 13.6.10. Optional background for Lesson 13.6 §4.
    Note: IEEE Xplore.
    Cited in: overview, 06-reassociation

  • [KB70] Donald E. Knuth and Peter B. Bendix. Simple Word Problems in Universal Algebras. In J. Leech (ed.), Computational Problems in Abstract Algebra, Pergamon Press, pp. 263–297, 1970.
    Why and when: Critical pairs and the completion procedure (Algorithm 13.4.5). Read after Lesson 13.4 §2 if you want the original; [BN98, Ch. 6–7] is the modern treatment.
    Note: Book chapter; reprinted in later collections of Knuth's papers.
    Cited in: overview, 04-canonicalization-and-rewriting

  • [Ler09] Xavier Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM 52(7), pp. 107–115, 2009. doi:10.1145/1538788.1538814
    Why and when: Core reading. CompCert: a C compiler proven correct in Coq, semantic preservation as simulation, and what is (and is not) in the trusted base; its CSE pass is the superlocal value numbering of Lesson 13.1. Read it after Lesson 13.9 §2 (Theorem 13.9.12).
    Cited in: overview, 01-scopes-and-constant-folding, 08-refinement-ub-and-fast-math, 09-verifying-transformations

  • [LHK+17] Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das, David Majnemer, John Regehr, and Nuno P. Lopes. Taming Undefined Behavior in LLVM. PLDI 2017, pp. 633–647, 2017. doi:10.1145/3062341.3062343
    Why and when: Core reading. Poison, undef and freeze made consistent, with refinement as the correctness criterion. Read §2–4 before Lesson 13.8; Proposition 13.8.12 is its central argument.
    Cited in: overview, 08-refinement-ub-and-fast-math

  • [LLM+21] Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr. Alive2: Bounded Translation Validation for LLVM. PLDI 2021, pp. 65–79, 2021. doi:10.1145/3453483.3454030
    Why and when: Core reading. Refinement for whole LLVM functions with undef, poison, memory and bounded loops, the exists-forall encoding of nondeterminism, and the bugs found by validating LLVM's tests. The tool used in the Lesson 13.8–13.9 boxes; read §3–5 after Lesson 13.9.
    Cited in: overview, 08-refinement-ub-and-fast-math, 09-verifying-transformations

  • [LMNR15] Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. Provably Correct Peephole Optimizations with Alive. PLDI 2015, pp. 22–32, 2015. doi:10.1145/2737924.2737965
    Why and when: Core reading. The Alive DSL and its SMT encoding of definedness, poison and values; the flag inference and the InstCombine bugs it found. Read §3–5 with Lesson 13.9 §2 (Algorithm 13.9.3).
    Cited in: overview, 02-peephole-engines, 08-refinement-ub-and-fast-math, 09-verifying-transformations

  • [Mas87] Henry Massalin. Superoptimizer: A Look at the Smallest Program. ASPLOS II (SIGPLAN Notices 22(10)), pp. 122–126, 1987.
    Why and when: Core reading. The origin of superoptimization: exhaustive search over 68020 instruction sequences, pruned and tested on sample inputs, with the famous branch-free signum. Read it with Lesson 13.3 §1 and compare its results with the GNU superoptimizer box.
    Note: ACM Digital Library (ASPLOS II proceedings).
    Cited in: overview, 03-superoptimization

  • [McK65] William M. McKeeman. Peephole Optimization. Communications of the ACM 8(7), pp. 443–444, 1965.
    Why and when: Names the peephole idea: look at a small window of generated code and replace it. Read it in five minutes before Lesson 13.2 to see how little the definition has changed.
    Note: Two pages in CACM, July 1965; available in the ACM Digital Library.
    Cited in: overview, 02-peephole-engines

  • [MN17] David Menendez and Santosh Nagarakatte. Alive-Infer: Data-Driven Precondition Inference for Peephole Optimizations in LLVM. PLDI 2017, pp. 49–63, 2017.
    Why and when: Learns weakest-like preconditions for Alive rules from positive and negative examples and verifies them (Algorithm 13.3.8). Read after Lesson 13.3 §6.
    Note: ACM Digital Library (PLDI '17).
    Cited in: overview, 03-superoptimization, 09-verifying-transformations

  • [MNG16] David Menendez, Santosh Nagarakatte, and Aarti Gupta. Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM. Static Analysis Symposium (SAS) 2016, LNCS 9837, pp. 317–337, 2016.
    Why and when: Extends Alive to floating point and fast-math flags, including the treatment of signed zeros and NaN. Read after Lesson 13.8 §2 (Definition 13.8.8) and Lesson 13.9 §7.
    Note: Springer LNCS 9837.
    Cited in: overview, 08-refinement-ub-and-fast-math, 09-verifying-transformations

  • [MR24] Manasij Mukherjee and John Regehr. Hydra: Generalizing Peephole Optimizations with Program Synthesis. Proc. ACM Program. Lang. 8 (OOPSLA1), 2024.
    Why and when: Turns Souper's concrete findings into rules with symbolic constants and synthesized preconditions, and emits compiler code. Read after Lesson 13.3 to see the whole pipeline "superoptimize, generalize, verify, implement".
    Note: ACM Digital Library (OOPSLA 2024).
    Cited in: overview, 03-superoptimization

  • [Nec00] George C. Necula. Translation Validation for an Optimizing Compiler. PLDI 2000, pp. 83–94, 2000. doi:10.1145/349299.349314
    Why and when: A translation validator for GCC's intermediate-level optimizations by symbolic evaluation. Read after Lesson 13.9 §6.
    Cited in: overview, 09-verifying-transformations

  • [New42] Maxwell H. A. Newman. On Theories with a Combinatorial Definition of "Equivalence". Annals of Mathematics 43(2), pp. 223–243, 1942.
    Why and when: The origin of Newman's lemma (Theorem 13.4.7). Historical; read the proof in Lesson 13.4 or [BN98, Ch. 2] instead.
    Note: JSTOR.
    Cited in: overview, 04-canonicalization-and-rewriting

  • [PSS98] Amir Pnueli, Michael Siegel, and Eli Singerman. Translation Validation. TACAS 1998, LNCS 1384, pp. 151–166, 1998. doi:10.1007/BFb0054170
    Why and when: The idea of validating each compiler run instead of the compiler (Definition 13.9.7). Read §1–3 after Lesson 13.9 §1.
    Cited in: overview, 09-verifying-transformations

  • [PTBD16] Phitchaya Mangpo Phothilimthana, Aditya Thakur, Rastislav Bodik, and Dinakar Dhurjati. Scaling up Superoptimization. ASPLOS 2016, pp. 297–310, 2016.
    Why and when: Combines enumerative, stochastic and symbolic search with a "lens" that prunes by equivalence classes. Optional, after Lesson 13.3 §6.
    Note: ACM Digital Library (ASPLOS '16).
    Cited in: 03-superoptimization

  • [Rei60] George W. Reitwiesner. Binary Arithmetic. Advances in Computers, vol. 1, Academic Press, pp. 231–308, 1960.
    Why and when: Introduces the non-adjacent form of signed-digit representations (Definition 13.7.1). Historical; Proposition 13.7.8 contains what the lesson needs.
    Note: Book chapter in Advances in Computers 1.
    Cited in: overview, 07-strength-reduction-and-division

  • [SCC+17] Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Gratian Lup, Jubi Taneja, and John Regehr. Souper: A Synthesizing Superoptimizer. arXiv:1711.04422, 2017. link
    Why and when: Core reading. How Souper extracts dataflow fragments from LLVM IR and synthesizes cheaper refinements with an SMT solver, and which missing LLVM optimizations it found. Read §2–4 after Lesson 13.3; the README of the Souper repository points to this paper.
    Cited in: overview, 03-superoptimization

  • [SSA13] Eric Schkufza, Rahul Sharma, and Alex Aiken. Stochastic Superoptimization. ASPLOS 2013, pp. 305–316, 2013.
    Why and when: STOKE: Metropolis–Hastings search over x86-64 programs with a cost of correctness plus performance (Algorithm 13.3.5, Theorem 13.3.10). Read §3 (the cost function and the proposal distribution) after Lesson 13.3.
    Note: ACM Digital Library (ASPLOS '13).
    Cited in: overview, 03-superoptimization

  • [WZ91] Mark N. Wegman and F. Kenneth Zadeck. Constant Propagation with Conditional Branches. ACM TOPLAS 13(2), pp. 181-210, 1991. doi:10.1145/103135.103136
    Why and when: Sparse conditional constant propagation, the global extension of constant folding mentioned in Lesson 13.1 §6; taught in full in Chapter 14.
    Cited in: 01-scopes-and-constant-folding

  • [YCER11] Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. Finding and Understanding Bugs in C Compilers. PLDI 2011, pp. 283–294, 2011. doi:10.1145/1993498.1993532
    Why and when: Csmith's random testing found hundreds of bugs in GCC and LLVM and none in CompCert's verified middle end: the empirical side of Lesson 13.9 §8's comparison.
    Cited in: overview, 09-verifying-transformations

Textbooks and monographs

  • [BN98] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Read: Ch. 2 (abstract reduction systems, Newman's lemma), Ch. 5 (termination), Ch. 6 (confluence and critical pairs), Ch. 7 (Knuth–Bendix completion).
    Why and when: The standard textbook for Lesson 13.4: read Ch. 2 for Theorem 13.4.7 and Ch. 6 for the critical-pair lemma (Theorem 13.4.8) before designing your own rule set.
    Cited in: overview, 04-canonicalization-and-rewriting

  • [Dragon2] Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools, 2nd ed.. Addison-Wesley, 2006. Read: §8.5 (Optimization of basic blocks: the DAG representation, local common subexpressions, dead code, algebraic identities, array references, reassembling basic blocks), §8.7 (Peephole optimization).
    Why and when: The DAG-based local optimization of Lesson 13.5 (Definition 13.5.6, Algorithms 13.5.7–13.5.8) and the Dragon book's peephole section. Read §8.5 with Lesson 13.5 §2.
    Cited in: overview, 05-value-numbering-and-dags

  • [EaC3] Keith D. Cooper and Linda Torczon. Engineering a Compiler, 3rd ed.. Morgan Kaufmann, 2022. Read: Ch. 8 (Introduction to Optimization: the scope of optimization, local value numbering, tree-height balancing, superlocal value numbering), Ch. 10 (Scalar Optimization: dead-code elimination).
    Why and when: Core reading. The best textbook treatment of this chapter's first half: scopes (Lesson 13.1), value numbering with its extensions (Lesson 13.5) and tree-height balancing (Lesson 13.6). Read Ch. 8 alongside Lessons 13.1 and 13.5.
    Cited in: overview, 01-scopes-and-constant-folding, 05-value-numbering-and-dags, 06-reassociation

  • [War13] Henry S. Warren and Jr.. Hacker's Delight, 2nd ed.. Addison-Wesley, 2013. Read: Ch. 10 (Integer Division by Constants), including Figure 10-1 (signed magic numbers); Ch. 8 (Multiplication).
    Why and when: Core reading. The algorithms LLVM's DivisionByConstantInfo cites, with proofs for signed and unsigned division by constants (Lesson 13.7, Theorem 13.7.10 and the magic-division drill). Read Ch. 10 with Lesson 13.7.
    Cited in: overview, 07-strength-reduction-and-division

Theses and technical reports

  • [CS70] John Cocke and Jacob T. Schwartz. Programming Languages and Their Compilers: Preliminary Notes. Courant Institute of Mathematical Sciences, New York University (2nd revised version), 1970.
    Why and when: The early source credited with value numbering over basic blocks (Lesson 13.5 §1). Of historical interest; learn the algorithm from Lesson 13.5 and [EaC3, Ch. 8].
    Note: Technical notes; scanned copies circulate in university libraries and archives.
    Cited in: overview, 01-scopes-and-constant-folding, 04-canonicalization-and-rewriting, 05-value-numbering-and-dags

Source code (pinned versions)

  • [ALIVE2-src] Alive2's translation validator (the commit built against LLVM 23.1.2 for this chapter) — tools/alive-tv.cpp in AliveToolkit/alive2 at 01a5ec4. Symbols: alive-tv, alive.
    Why and when: Build instructions: README.md; this commit is the last before an LLVM API change. The tool behind every alive-tv box of Lessons 13.3, 13.8 and 13.9.

  • [COMPCERT-CSE] CompCert's verified value numbering over extended basic blocks — backend/CSE.v in AbsInt/CompCert at v3.15. Symbols: transf_function, CSEproof.v transf_program_correct, driver/Compiler.v transf_c_program_correct.
    Why and when: A superlocal value-numbering pass with a Coq proof (Lessons 13.1 and 13.9). Read the header comment of CSE.v and the statement of transf_program_correct.

  • [Cranelift-ISLE] Cranelift's mid-end simplification rules in ISLE (and opts/cprop.isle) — cranelift/codegen/src/opts/arithmetic.isle in bytecodealliance/wasmtime at v37.0.2. Symbols: (rule (simplify (isub (ty_int ty) x x)) ...), cprop.isle push immediates to the right.
    Why and when: A typed term-rewriting DSL applied inside an acyclic e-graph (Lessons 13.2 and 13.4). Read arithmetic.isle and the canonicalization rules of cprop.isle.
    Cited in: overview, 02-peephole-engines, 04-canonicalization-and-rewriting

  • [GCC-fold-const] GCC's GENERIC constant folder — gcc/fold-const.cc in gcc-mirror/gcc at releases/gcc-15.1.0. Symbols: const_binop, int_const_binop, fold_binary_loc.
    Why and when: GCC's counterpart of ConstantFolding.cpp, including the TREE_OVERFLOW marking seen in the Lesson 13.1 box.
    Cited in: overview, 01-scopes-and-constant-folding

  • [GCC-matchpd] GCC's match-and-simplify rule file (compiled by gcc/genmatch.cc) — gcc/match.pd in gcc-mirror/gcc at releases/gcc-15.1.0. Symbols: (simplify (minus @0 @0) ...), genmatch.cc dt_node.
    Why and when: Thousands of simplification rules in a pattern DSL with preconditions (Lesson 13.2). Read the first 300 lines after the lesson, then the decision-tree comment in genmatch.cc.
    Cited in: overview, 02-peephole-engines

  • [GCC-reassoc] GCC's rank-based reassociation pass — gcc/tree-ssa-reassoc.cc in gcc-mirror/gcc at releases/gcc-15.1.0. Symbols: get_rank, reassociate_bb.
    Why and when: Ranks, linearization, merging of equal operands and constant folding (Lesson 13.6 §7). Read get_rank after the lesson.
    Cited in: overview, 06-reassociation

  • [GCC-sccvn] GCC's value numbering (FRE/PRE) — gcc/tree-ssa-sccvn.cc in gcc-mirror/gcc at releases/gcc-15.1.0. Symbols: do_rpo_vn, visit_nary_op.
    Why and when: Value numbering over SSA in RPO, with expression simplification in the table (Lesson 13.5 §7). Optional reading after Lesson 13.5.
    Cited in: 05-value-numbering-and-dags

  • [GSO-src] The GNU superoptimizer 2.5 (Granlund and Kenner), as maintained by Embecosm — README in embecosm/gnu-superopt at 3649aac8bbdaa721f26213e685bd99ccecac7ba6. Symbols: superopt.c, goal.def SGN.
    Why and when: Build it in a minute and run the signum search of the Lesson 13.3 box; the README's warning about unverified sequences motivates the full check of Theorem 13.3.9.

  • [LLVM-ConstantFolding] LLVM's target-aware constant folder (with llvm/lib/IR/ConstantFold.cpp for the target-independent part) — llvm/lib/Analysis/ConstantFolding.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: ConstantFoldInstruction, ConstantFoldBinaryOpOperands, ConstantFoldCall, ConstantFoldFP.
    Why and when: Read after Lesson 13.1: how folding uses the DataLayout, APFloat, and the host libm for intrinsics such as sin (ConstantFoldFP), and compare with your pebble-constfold (E1).
    Cited in: overview, 01-scopes-and-constant-folding

  • [LLVM-DCE] LLVM's worklist dead-code elimination (and ADCE.cpp for the aggressive variant) — llvm/lib/Transforms/Scalar/DCE.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: eliminateDeadCode, DCEInstruction.
    Why and when: Algorithm 13.5.10 in about 100 lines, using isInstructionTriviallyDead; compare with your pebble-dce (E4) and with ADCE.cpp.
    Cited in: overview, 05-value-numbering-and-dags

  • [LLVM-DivConst] LLVM's magic-number computation for division by constants (used by TargetLowering::BuildUDIV/BuildSDIV) — llvm/lib/Support/DivisionByConstantInfo.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: SignedDivisionByConstantInfo::get, UnsignedDivisionByConstantInfo::get.
    Why and when: Warren's algorithms in APInt, with LLVM's pre-shift and widen options (Lesson 13.7 §7); read after Theorem 13.7.6 and the unit test llvm/unittests/Support/DivisionByConstantTest.cpp.
    Cited in: overview, 07-strength-reduction-and-division

  • [LLVM-EarlyCSE] EarlyCSE, dominator-scoped value numbering with memory generations — llvm/lib/Transforms/Scalar/EarlyCSE.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: EarlyCSE, EarlyCSE::processNode, CurrentGeneration.
    Why and when: Scoped hash tables over the dominator tree (Lesson 13.1) and memory generations (Definition 13.5.4). Read processNode after Lesson 13.5.
    Cited in: overview, 01-scopes-and-constant-folding, 05-value-numbering-and-dags

  • [LLVM-GISelCombine] The GlobalISel combiner's TableGen rules — llvm/include/llvm/Target/GlobalISel/Combine.td in llvm/llvm-project at llvmorg-23.1.2. Symbols: GICombineRule, GICombinePatFrag, add_sub_reg.
    Why and when: Peephole rules as TableGen data, compiled into a matcher table (Lesson 13.2 §7). Read a dozen rules after the lesson.
    Cited in: overview, 02-peephole-engines

  • [LLVM-InstCombine] InstCombine's add/sub visitors (the driver is InstructionCombining.cpp, InstCombinerImpl::run) — llvm/lib/Transforms/InstCombine/InstCombineAddSub.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: InstCombinerImpl::visitAdd, InstCombinerImpl::visitSub, foldAddWithConstant.
    Why and when: A hand-written combiner (Lesson 13.2): read visitAdd top to bottom and find rules R2, R9 and R11 of E2 with their flag handling.
    Cited in: overview, 02-peephole-engines

  • [LLVM-MachineCombiner] Latency-driven reassociation and combining of machine instructions — llvm/lib/CodeGen/MachineCombiner.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: MachineCombiner::combineInstructions, TargetInstrInfo::getMachineCombinerPatterns.
    Why and when: Tree-height reduction with real latencies (Lesson 13.6 §7). Read combineInstructions after the lesson.
    Cited in: overview, 06-reassociation

  • [LLVM-PatternMatch] LLVM's embedded pattern-matching library — llvm/include/llvm/IR/PatternMatch.h in llvm/llvm-project at llvmorg-23.1.2. Symbols: match, m_Add, m_c_Add, m_Deferred, m_OneUse, m_APInt, m_Power2.
    Why and when: The matchers E2 is written with (Algorithm 13.2.5); read the definitions of m_c_Add and m_Deferred to see commutative and non-linear matching.
    Cited in: overview, 02-peephole-engines

  • [LLVM-Reassociate] LLVM's rank-based reassociation — llvm/lib/Transforms/Scalar/Reassociate.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: ReassociatePass::BuildRankMap, ReassociatePass::getRank, ReassociatePass::BuildPairMap.
    Why and when: Ranks as in Definition 13.6.2 (refined), linearization and the pair map. Read BuildRankMap and getRank after Lesson 13.6 §2.
    Cited in: overview, 06-reassociation

  • [LLVM-SelectionDAG] SelectionDAG construction with CSE through the CSEMap folding set — llvm/lib/CodeGen/SelectionDAG/SelectionDAG.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: SelectionDAG::getNode, CSEMap.
    Why and when: The per-block DAG of instruction selection (Lesson 13.5 §7): every getNode looks the node up first, which is DAG construction with value numbering.
    Cited in: overview, 05-value-numbering-and-dags

  • [MLIR-Rewrite] MLIR's greedy worklist pattern-rewrite driver — mlir/lib/Transforms/Utils/GreedyPatternRewriteDriver.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: applyPatternsGreedily, GreedyPatternRewriteDriver.
    Why and when: The same worklist engine as Algorithm 13.2.4 for MLIR patterns (C++, PDL or PDLL). Optional, after Lesson 13.2 §6.
    Cited in: 02-peephole-engines

  • [SOUPER-src] A Souper synthesis test (division by 515 as multiply and shift) — test/Infer/div_const.opt in google/souper at 963d4df436f3dc0b039cc0e47ada0577a26f5c4e. Symbols: infer, result.
    Why and when: The concrete result derived by CEGIS in Lesson 13.3 §3 and verified by Alive2 in §7; browse test/Infer for more synthesized optimizations.

  • [STOKE-src] STOKE's documentation of its search and cost function — README.md in StanfordPL/stoke at 98d8a0f028f2daf2052bfe607dbc32ec8d55ba9e. Symbols: src/search, src/cost.
    Why and when: The cost-function and proposal-mass options quoted in Lesson 13.3 §7; read the "Cost Function" section after Algorithm 13.3.5.

Official documentation and specifications

  • [Cranelift-ISLE-ref] ISLE language reference (Cranelift). wasmtime 37.0.2. link
    Why and when: Terms, extractors, constructors and rule priorities of ISLE. Read the "Rules" and "Priorities" sections after Lesson 13.2.
    Cited in: overview

  • [GCC-MaS] GCC Internals, "Match and Simplify". GCC 15. link
    Why and when: The match.pd language reference (simplify, match, for, :c, @@, if, with). Read with Lesson 13.2 §2 (external pattern DSLs).
    Cited in: overview

  • [IEEE754] IEEE Standard for Floating-Point Arithmetic (IEEE Std 754-2019). 754-2019. link
    Why and when: The formats, rounding and special values behind Definition 13.1.9 and Lesson 13.8's floating-point rules; §4 (rounding) and §6 (infinity, NaNs, signed zero).
    Cited in: overview, 01-scopes-and-constant-folding

  • [LLVM-ICGuide] InstCombine contributor guide. LLVM 23.1.2. link
    Why and when: Core reading. How LLVM wants peephole rules written: tests (negative, multi-use, commuted, flags), Alive2 proofs, the choice between InstSimplify and InstCombine, canonicalization and flag handling. Read it after Lesson 13.2 and before writing E2.
    Cited in: overview, 02-peephole-engines, 04-canonicalization-and-rewriting, 08-refinement-ub-and-fast-math, 09-verifying-transformations

  • [LLVM-LangRef] LLVM Language Reference Manual. LLVM 23.1.2. link
    Why and when: Core reading. Read "Poison Values", "Undefined Values", the freeze instruction, each instruction's flag semantics and "Fast-Math Flags" (with its rewrite-based flags) alongside Lesson 13.8.
    Cited in: overview, 08-refinement-ub-and-fast-math