Lab 13 · Peephole engines: hand-written vs DSL, and checking the rules¶

Chapter: 13 · Local Optimization & Transformation Correctness · Lessons: 13.2, 13.3, 13.8, 13.9 · Time: 10–14 hours (+4 for ★ Part C) · Tests: ./course test 13 (labels ch13; the lab suite is the ctest test ch13.lab)

Goal¶

Exercise E2 made you write the peephole rules R1–R17 by hand in C++. In this lab you build the competing design, a rule-table engine driven by a small DSL (Part A), and check that it is the same optimizer: same rewrites, same final code, on a corpus of 4 824 instructions (Part D, where you also measure speed and code size). Then you build the tool that makes a rule set trustworthy: a bounded exhaustive refinement checker for straight-line integer functions with poison, UB and freeze (Part B), which plays Alive2's role at small bit widths (Lesson 13.9, Algorithm 13.9.6). The optional ★ Part C is a brute-force superoptimizer for short i8 sequences in Massalin's style (Lesson 13.3, Algorithm 13.3.3), whose answers your checker verifies.

Prerequisite: exercise E2 (pebble-peephole) passes its tests. Part B does not depend on anything else and can be done first.

Part A · `pebble-peephole-dsl`: the rules as data¶

Requirements: - A1. A function pass pebble-peephole-dsl, registered in the course plugin from a .cpp file in labs/ch13-peephole/dsl/ (every *.cpp there is compiled into PebblePasses, next to your pebble-peephole). - A2. The integer rules R1–R14 of exercise E2 (the add mul and or xor part of R1; not icmp/FP) are written as data: rule text in a language you design (in the .cpp as a string, or a separate file you embed), each rule with a name, a pattern, a result, an optional applicability condition and the flag conditions of the result. One generic matcher interprets them (or a generator you write compiles them). No rule may be special-cased in C++: adding a rule of the same shape must not require new C++. - A3. Same semantics as E2 on these rules: same conditions, same result flags (E2-R1), same priority order (E2-R2), same engine discipline (E2-R3). Consequently, on any input with only integer binary operators, your engine produces the same IR and the same rule counts as pebble-peephole. - A4. pebble-peephole-dsl<stats> prints to stderr, per function with at least one rewrite, one line per rule that fired, sorted by rule name: pebble-peephole-dsl: @<function> <rule-name> <count>, with E2's rule names. An unknown parameter is an error. - A5. Rules are indexed by root opcode, so an instruction is only tried against rules that can match it (Lesson 13.2's decision-tree idea at depth 1; a full decision tree, Algorithm 13.2.6, is a stretch goal).

A possible rule syntax (yours may differ):

sub-const     : (sub x C)  => (add x -C)            if nonzero(C)  nsw = nsw@0 & !smin(C)
add-add-const : (add (add x C1) C2) => (add x C1+C2) nsw = nsw@0 & nsw@1 & !sovf(C1,C2)

Part B · `ch13-rewrite-check`: bounded exhaustive refinement checking¶

Contract¶

// labs/ch13-peephole/include/lab13/Tools.h  (provided; do not change)
namespace lab13 {
/// `ch13-rewrite-check <file.ll>`: decides by exhaustive enumeration whether
/// @tgt refines @src. Returns the process exit code:
/// 0 valid, 1 invalid (a counterexample was printed), 2 usage or input error.
int rewriteCheckMain(int argc, char **argv);
}

labs/ch13-peephole/tools/RewriteCheck.cpp (provided) is the main that calls it; you implement it in labs/ch13-peephole/src/.

usage: ch13-rewrite-check <file.ll>

Input¶

An LLVM IR module (text) that defines two functions, @src and @tgt, with the same signature. Each has one basic block of the following instructions, on integer types of width 1 to 64:

binary operators add sub mul udiv sdiv urem srem shl lshr ashr and or xor, with any of their flags (nsw nuw exact disjoint);
icmp (all ten predicates, samesign), select (i1 condition), freeze, zext (nneg), sext, trunc (nuw nsw);
ret; operands are arguments, earlier results, integer constants and poison. Arguments may be noundef.

Semantics¶

Exactly Lesson 13.8's (Definitions 13.8.1–13.8.5, following the LangRef): values are \(N\)-bit patterns or poison; flag violations and shift amounts \(\ge N\) give poison; udiv sdiv urem srem by zero or by poison, and sdiv/srem of INT_MIN by \(-1\), are immediate UB; a poison operand makes the result poison (a select with a poison condition is poison, otherwise it returns the chosen arm, poison or not); freeze of poison returns an arbitrary but fixed value; freeze of a value returns it.

Refinement (Definition 13.8.4). For an input \(\vec{x}\), let \(\mathcal{B}(f, \vec{x})\) be the set of outcomes of \(f\) over all choices of its freezes. @tgt refines @src iff for every input, either @src may have UB, or every outcome of @tgt is allowed: a value \(v\) is allowed if @src may return \(v\) or poison; poison is allowed only if @src may return poison; UB is never allowed.

Enumeration order (fixed, because the first counterexample is printed)¶

B1. Inputs are enumerated like an odometer whose last argument varies fastest. Each argument of width \(w\) takes the values \(0, 1, \ldots, 2^w - 1\) (bit patterns, in increasing unsigned order), then poison — except noundef arguments, which never take poison.
B2. For each input, all freeze choices of @src are enumerated (each freeze takes \(0, \ldots, 2^w - 1\), the first freeze of the function varying fastest) to compute its outcome set; then the freeze choices of @tgt in the same order, stopping at the first disallowed outcome.
B3. Limits: the total input space, \(\sum_i \log_2(\text{domain size of argument } i)\), is at most 24 bits; the freezes of each function have at most 16 bits in total. Beyond the limits the tool reports an error (exit 2).

Output¶

Valid (exit 0), where N is the number of inputs enumerated:

valid: @tgt refines @src (N inputs)

Invalid (exit 1): four lines for the first counterexample in the order of B1–B2.

invalid: <reason>
input: %x = <value>, %y = <value>
source: <outcome set of @src>
target: <the disallowed outcome of @tgt>

<reason> is one of target has undefined behavior where source does not, target is more poisonous than source, value mismatch (a well-defined target value that the source can't produce, the source not being poison).
A value prints as its signed decimal interpretation at its width (-64, not 192); i1 values print as true/false; poison as poison. input: lists the arguments in order as %name = value, separated by ,; with no arguments it prints input: (none).
The source set prints as a single element if it has one (-128, poison), otherwise one of {v1, v2, poison} with values in increasing unsigned order and poison last; more than 8 values print as one of N values (still followed by , poison inside braces if poison is possible: one of {one of 256 values, poison}). UB prints as undefined behavior.

Example (tests/ch13/lab/Inputs/invalid-add-self-nuw.ll):

define i8 @src(i8 %x) {
  %r = add nsw i8 %x, %x
  ret i8 %r
}
define i8 @tgt(i8 %x) {
  %r = shl nuw i8 %x, 1
  ret i8 %r
}

invalid: target is more poisonous than source
input: %x = -64
source: -128
target: poison

Errors (exit 2) print a message to stderr and nothing to stdout: no arguments or more than one (usage: ch13-rewrite-check <file.ll>), a parse error (LLVM's diagnostic), and, as one line error: <message>, a missing @src/@tgt (error: the module must define @src and @tgt), different signatures (error: @src and @tgt must have the same signature), an unsupported instruction or type (floating point, memory, more than one block, undef), or the limits of B3.

Performance¶

B4. Two i8 arguments (66 049 inputs) check in well under a second (the reference: 0.03 s); the whole lab suite runs in a few seconds.

Part C ★ · `ch13-superopt`: a brute-force superoptimizer (optional)¶

/// `ch13-superopt [--max-len=L] <file.ll>`: finds a shortest straight-line
/// replacement for @src. Returns the exit code:
/// 0 found, 1 nothing within the length bound, 2 usage or input error.
int superoptMain(int argc, char **argv);

C1. Input: a module defining @src with one or two arguments of type iN and result iN, \(N \le 8\), in the instruction set of Part B, without freeze. --max-len=L bounds the length (\(0 \le L \le 4\), default 3).
C2. Search space: straight-line programs of \(0, 1, \ldots, L\) instructions over the flag-free operations add sub mul and or xor shl lshr ashr, whose operands are the arguments, earlier results and the constants \(1\), \(-1\), \(N - 1\) and, for every constant \(c\) of @src: \(c\), \(c \pm 1\), \(-c\) and \(\lnot c\) (zero excluded). Every instruction but the last must be used. Length 0 means returning an argument or any constant.
C3. Correctness: an answer refines @src on every input, poison included (Part B's criterion). Test vectors may reject candidates early; the final check must be exhaustive.
C4. Optimality: lengths are tried in increasing order; the first answer found has minimal length within the search space (Theorem 13.3.9).
C5. Output (exit 0): a comment line, then the function named @opt with results named %t0, %t1, …, and constants printed as signed decimals:

; ch13-superopt: 2 instructions (was 4), <candidates> candidates, <seconds> s
define i8 @opt(i8 %x) {
  %t0 = mul i8 %x, 3
  %t1 = mul i8 %t0, 3
  ret i8 %t1
}

"was" counts @src's instructions without the ret; "instruction" is singular for length 1. With nothing found (exit 1): ; ch13-superopt: nothing of length <= L found (<candidates> candidates). Errors as in Part B (exit 2). - C6. The output must be accepted by llvm-link next to its input after renaming @opt to @tgt (the tests then run your checker on the pair).

Part D · Measurement¶

labs/ch13-peephole/measure.py (provided) runs both engines on corpus/programs.ll (70 instructions from corpus/programs.c), corpus/synthetic.ll (300 generated functions, 4 824 instructions; corpus/make_corpus.py, seed 13) and a 30× replica, and prints instruction counts before/after, rule applications per rule, wall time (best of --repeat runs, with a no-op column for opt's own start-up, parsing and printing), and the source lines of each engine.

uv run python labs/ch13-peephole/measure.py --build build/<preset> --repeat 7

Fill in this table in your notes, and answer: where does the DSL engine spend its extra time? What would compiling the rules (like genmatch or ISLE) change? How many lines does a new rule cost in each design?

Corpus	Before	After (hand-written)	After (DSL)	Hand-written ms − no-op	DSL ms − no-op
programs.ll	70
synthetic.ll	4 824
synthetic-x30.ll	144 720

Reference solutions on Linux x86-64 (three runs, best of 7–11 each; your numbers will differ): both engines leave 60, 4 185 and 125 550 instructions and apply the same rules (1 355 applications on synthetic.ll); the hand-written engine takes 25–40 ms and the interpreted DSL engine 75–95 ms beyond a 225–250 ms no-op run on the 30× corpus; 286 source lines for the hand-written pass vs 403 for the DSL pass including its parser and interpreter (29 lines of rules).

Provided infrastructure¶

File	What it gives you
`include/lab13/Tools.h`	the two CLI contract functions (above)
`tools/RewriteCheck.cpp`, `tools/Superopt.cpp`	the `main`s of `ch13-rewrite-check` and `ch13-superopt`
`src/Stub.cpp`	the contract functions, each stopping with `TODO(ch13)`: replace or delete it
`corpus/`	the measurement corpus and its generators
`measure.py`	Part D's measurement driver
`pebble/lib/Passes/LocalOpt/Ch13Provided.cpp`	`print<pebble-icount>` (instruction counts per function)

Everything else is yours: src/ for Parts B and C (Part B's IR interpreter is shared with Part C; design it once), dsl/ for Part A. Add any files you like; they're compiled automatically.

What the tests check¶

Test	Checks
`tests/ch13/lab/dsl-rules.test`	Part A: your DSL engine passes each rule file R1–R14 of E2 (`tests/ch13/lit/peephole-*.ll`, integer functions only)
`tests/ch13/lab/compare.test`	Parts A + D: on `synthetic.ll` and `programs.ll` both engines give the same instruction count for every function and the same `<stats>` lines (after renaming the pass); the DSL pass is registered
`tests/ch13/lab/rewrite-check.test`	Part B: 8 valid rewrites (input counts 257, 66 049, 17, 256…) and 9 invalid ones with the exact four-line counterexample (flags, `i1` corner, `sdiv` vs `ashr`, UB, duplicated `freeze`, poison input, `samesign`); exit codes 0/½ and the signature error
`tests/ch13/lab/rewrite-check-llvm.test`	Part B vs LLVM: whatever `opt -passes=instcombine` (LLVM 23.1.2) does to 8 small functions, your checker says `valid`
`tests/ch13/lab/superopt.test`	Part C: shortest answers for four inputs (length 1, 1, 1, 2), nothing for signum within length 2 (exit 1), usage error (exit 2), and two answers verified by your checker

Part C's test is part of the suite; if you skip Part C, ch13.lab fails only on superopt.test.

Milestones¶

Checker, values only (Lesson 13.9 §3): arguments and constants, add sub mul, ret; valid-two-args.ll and invalid-value.ll — build/<preset>/bin/pebble-lit -v tests/ch13/lab/rewrite-check.test shows the first failures move down the file.
Checker, poison and UB: flags, shifts, division, icmp, casts, select, poison inputs — the invalid cases of rewrite-check.test.
Checker, freeze: outcome sets; valid-freeze-dup.ll and invalid-freeze-dup.ll. Then rewrite-check-llvm.test.
DSL engine: parse the rules, match, build results, flags — pebble-lit -v tests/ch13/lab/dsl-rules.test.
Same optimizer: pebble-lit -v tests/ch13/lab/compare.test; then run measure.py and fill in the table.
★ Superoptimizer: pebble-lit -v tests/ch13/lab/superopt.test.

Hints¶

Hint 1 — where to start

For Part B, read Lesson 13.9 §2 (Definition 13.9.5, Algorithm 13.9.6) and write the interpreter first: one function that runs a straight-line function on an input vector and a vector of freeze choices and returns "UB" or a value-or-poison. Everything else (enumerating inputs, outcome sets, the verdict) is a loop around it. For Part A, write down R1–R14 in your syntax on paper before writing the parser: the syntax must be able to express R9's two-instruction pattern and its flag conditions.

Hint 2 — the key idea

Refinement is asymmetric, and the order of the checks decides the reason printed: if the source may have UB, skip the input; otherwise a target UB, then a target poison (when the source can't be poison), then a value not in the source set (when the source can't be poison). Poison is not a value you can compare: carry it as a separate bit. For Part A, the DSL rules are a list of data; the engine's worklist loop can be literally the one you wrote for E2 — if you copy it, the counts agree by construction.

Hint 3 — a design sketch

Part B: struct Val { uint64_t Bits; bool Poison; }, masking every result to its width; a Behaviors { bool UB, Poison; std::set<uint64_t> Values; }; the odometer as a vector of indices where index \(2^w\) means poison. The bug the tests catch most often is a wrong signed interpretation at small widths (ashr, sdiv, icmp slt on i4): write toSigned(bits, w) once. Part A: a pattern is a small tree of nodes (opcode, variable, constant variable, literal); matching fills two maps (variables → Value *, constants → APInt); conditions and flag expressions are small ASTs evaluated on the constant map and on the flags of the matched instructions numbered in preorder. Part C: keep a pool of value vectors (one entry per test input) so that each candidate costs one vector operation; verify survivors with the Part B interpreter.

Stretch goals ★¶

Compile the rule set into a decision tree (Algorithm 13.2.6) and measure the matcher again.
Check every DSL rule with your checker at widths 1–8 by instantiating its constants exhaustively (a miniature Alive-Infer, Lesson 13.3 §6); report the rule and width of any failure.
Add a --width=N option to the checker that re-instantiates a width-generic rule at another width, and find a rule that is valid at 8 bits but not at 1 (Proposition 13.9.11).