 |
MimIR
MimIR is my Intermediate Representation
|
|
MimIR
MimIR is my Intermediate Representation
|
At a high level, a phase is a self-contained compiler transformation or analysis step. Phases are intended to do one thing at a time and compose in a straightforward sequence. See also the Rewriting Guide, since several phase families are built directly on top of Rewriter.
A Phase has a single entry point, run(), which wraps the actual implementation in start().
Phase is the minimal base class.
A phase provides:
A custom phase usually derives from Phase and implements start():
Run it with:
Analysis is the base class for phases that inspect the current world using the Rewriter traversal machinery. It inherits from both Phase and Rewriter, but unlike RWPhase, it rewrites into the same world. In practice, this means Rewriter is used as a structured, graph-aware traversal over ordinary MimIR Defs.
A central feature of Analysis is its lattice(), a Def2Def map that stores abstract information about old-world Defs.
This is often convenient because analysis information can itself be represented as ordinary MimIR Defs. As a result, existing IR machinery applies automatically, including:
So if your abstract domain fits naturally into MimIR, you can often encode it directly as Defs and store it in the analysis lattice.
An Analysis visits everything reachable from the external mutables. Axioms and mutable annexes other than Lams are opaque; see Annexes.
Typical usage:
The lattice follows these conventions:
Analysis provides the following accessors and mutators:
Analysis-specific sentinels should be ordinary Defs - e.g. a dedicated Proxy tag, as SEO uses for its GVN and pending-⊤ markers - never nullptr, which is reserved for absent.
Unlike RWPhase, an Analysis must traverse the entire reachable program without rebuilding it. For this reason, Analysis overrides rewrite_mut() to keep mutables in place and use the rewriter machinery as a graph-aware traversal over the existing world.
Immutables are still visited depth-first through the inherited Rewriter recursion, but mutables are visited breadth-first via an internal worklist. This matters because abstract values typically flow between mutables — e.g. from an App call site into the callee's binder vars. A breadth-first order tends to seed a mutable from all of its predecessors before its body is walked, so information propagates further per fixed-point round and convergence needs fewer rounds. Breadth-first traversal is safe here precisely because an Analysis never rebuilds a mutable: it maps every mutable to itself, so nothing depends on a mutable being fully rewritten before it is used (contrast the strict depth-first ordering an RWPhase needs, where a rebuilt binder's type/identity is consumed as it is constructed).
Once a batch of roots has been scheduled, Analysis::drain() pops mutables from the worklist and, for each, enters it for curr_mut() tracking and rewrites its dependencies. Rewriting those dependencies schedules any further mutables it reaches, so the worklist drains in breadth-first order.
The mut -> mut entry recorded in step 2 doubles as the per-round "already scheduled" marker: it lives in the rewriter map (see lookup()), which reset() clears at the start of every round. Hence each mutable's dependencies are walked at most once per fixed-point round, which also prevents cyclic (recursive) CFGs from recursing forever.
When a rewrite_imm_App override propagates abstract values from call arguments into a callee's binder vars, it should seed those lattice entries first and then rewrite() the callee. This schedules the callee (or does nothing if it is already scheduled), so its body is walked later during the drain, after the seeded facts — and any joins from sibling call sites — are in place. lattice(concr, abstr) conveniently pairs the two writes (lattice and rewriter map) that arise in this seeding pattern.
A full round traverses the whole World: start() first runs prepare(), then rewrites all external mutables, drains the worklist, and finally runs finalize(). Whenever lattice(concr, abstr) changes an entry it invalidates, requesting another round, and records curr_mut() as dirty.
The first round, and each certification round described below, is full. A follow-up round is sparse: it re-drains only dirty mutables — plus everything reachable from them — instead of walking the whole World. At the start of a sparse round the accumulated lattice is replayed into the rewriter map, so a dirty mutable's body sees the substitutions its (non-revisited) producers installed in earlier rounds. An analysis can taint() additional mutables when a change must re-visit more than the writer — e.g. SEO taints all call sites of a Lam whose abstract vars changed, which keeps its per-round join restart sound. A change that cannot be attributed to any mutable (e.g. in finalize()) forces the next round to be full.
Since dirt tracks writers — not readers — a sparse round may miss affected mutables. Hence, once sparse rounds quiesce, one final full round certifies the fixed point; if it discovers new facts, iteration continues sparsely from its dirt. Only full rounds run finalize(), so post-passes always see the complete abstract World. Use make_dense() to force whole-World rounds unconditionally.
If an analysis participates in a fixed-point loop, it should be ready to run multiple times. The base reset() clears the rewriter map (and hence the per-round "already scheduled" markers) and the worklist, and resets Phase::todo() for the next round, but preserves lattice() so that abstract values accumulated in earlier iterations remain available — this is what makes fixed-point convergence possible.
RWPhase is the base class for phases that rebuild the current world into a new one, thereby removing garbage. This is the standard base class for optimization phases that structurally transform IR. It is both a Phase and a Rewriter:
After the final swap, the rewritten world becomes the current one.
An RWPhase may be given an associated Analysis. If so, analyze() runs that analysis to a fixed point before rewriting begins.
This is a common pattern:
If no analysis is needed, analyze() can simply return false.
Once analyze() has run, the rewrite can query the analysis result through RWPhase::lattice().
RWPhase::lattice() provides access to the analysis lattice for old-world Defs. It returns the abstract value computed by the associated Analysis, or nullptr if no value is available.
This is the standard way to communicate fixed-point analysis results into the subsequent rewrite.
optimize() moves all annexes into the Driver::library(); a World imports an annex on first use. An RWPhase does not rewrite an axiom or a mutable annex but resolves it to the annex with the same flags in the new world, which imports it unchanged on demand. So a phase never alters such an annex - its shape is what normalizers and backends rely on. An immutable annex is just its value and is rewritten like any other immutable.
The exception is an annex Lam: it is code, so it passes through the phase like the rest of the program - as an ordinary Lam. A phase that wants to process a Lam it fetches itself - e.g. a priv *_impl it instantiates - builds the instance in old_world() and rewrites it (see tensor::phase::Lower).
rewrite_external() is the hook for rewrites that must exempt the externals. An external is the program's interface to the outside, so a phase that reshapes definitions usually has to leave the externals themselves alone; EtaConv uses it so that an external keeps its η-shape.
A rewrite hook may not be able to finish its work immediately. For example, a closure-converting phase must create a function stub eagerly so callers can refer to it, but can rewrite its body only after completing the enclosing scope. Push such work onto your own worklist and drain it in finalize(), which runs after all roots have been walked but still before the two worlds are swapped (see clos::phase::ClosConv).
Cleanup is simply an RWPhase with no custom rewrites. Because an RWPhase reconstructs only what is reachable from the world roots, rebuilding automatically eliminates dead and unreachable code.
A phase that drops or reorders the components of a mutable Sigma changes its number of ops, so it needs the index-mapping overload of rewrite_stub together with Sieve - see Reshaping Aggregates in the Rewriting Guide. SingleErasure is the canonical user.
Sieve is useful on its own, though: dropping the parameters of a Lam changes its type rather than its ops, so the SCCP transformation below only uses gather and operator[].
An RWPhase may change how values are represented - Scalarize flattens tuple parameters, SingleErasure drops information-free components. Such a phase cannot reshape everything: an Axm's signature is fixed, since normalizers and backends match on it, and an interface Lam (an external, an annex, or a foreign declaration) has callers outside the phase's reach.
So wherever a type is checked, every RWPhase coerce()s the rewritten value to the rewritten expected type:
Coercion matches value and type leaf by leaf: it explodes and reassembles tuples, η-wraps a function whose Pi differs, and drops or fills in components that have a sole inhabitant. Where nothing was reshaped, value and type are already assignable and coercion is the identity.
This lets the phase decide its representation per type instead of first pinning every shape that could meet a fixed one in an Analysis. To keep a shape fixed by its position, rewrite it with a nested Rewriter: Scalarize rewrites everything an interface Lam's signature mentions with its Keep rewriter, where no Pi gets flattened. The very same Pi elsewhere is flattened in context 0, and coercion bridges both wherever they meet.
Run it with:
PhaseMan organizes several phases into a pipeline.
It can run them:
A fixed-point PhaseMan reruns the pipeline as long as at least one phase invalidates. Because a phase's run is a deterministic function of the World's content, PhaseMan skips a phase when its last run was quiet and no later phase has changed the world. Consequently, tail iterations rerun only phases that may still make progress; the pipeline terminates without a final round that reruns every phase.
Before a rerun, the phase is recreated from its original configuration. This prevents phase-local state from leaking across rounds unless the phase explicitly reconstructs it.
Use a fixed-point pipeline when phases expose new optimization opportunities for one another.
ClosedMutPhase is a traversal helper for phases that visit all reachable, closed mutables in the world.
A mutable is relevant here if it is:
This is useful for local analyses or transformations naturally phrased as:
You override visit(M*), where M defaults to Def but may be restricted to a particular mutable subtype.
NestPhase builds on ClosedMutPhase and computes a Nest for each visited mutable.
Use it when your phase needs a structured view of nested control or binding structure rather than just the raw mutable.
Instead of overriding visit(M*), override:
This is convenient for analyses that reason about nesting, dominance-like structure, or hierarchical regions.
The provided Sparse Conditional Constant Propagation (SCCP) implementation is a good example of the intended phase structure. Its architecture is:
The SCCP analysis associates each lambda variable with a lattice value:
In the implementation, this lattice is stored in Analysis::lattice() as a Def2Def map. A nice aspect here is that the propagated value is itself a regular Def. This illustrates the benefit of building analysis on top of Rewriter: the abstract domain can live directly inside MimIR, so canonicalization and normalization come for free.
The join in propagate() is expressed entirely through the lattice API: lattice(var) reads the current abstract value, lattice(concr, abstr) overwrites it, and pin() resolves conflicting values to ⊤. No manual invalidate() bookkeeping is needed: every join step that gains information - including the ⊥ → value insert - triggers the next fixed-point round automatically via lattice(concr, abstr).
The analysis traverses the old world and updates the lattice when it sees applications of optimizable lambdas. Whenever this changes the lattice, the analysis reruns until stable - sparsely, re-draining only the dirty mutables in between full rounds. This is a textbook use of Analysis:
The conditional part of SCCP needs no code of its own. Wegman and Zadeck track which CFG edges are executable, so that an unreachable predecessor does not spoil a join. Here, the analysis rewrites each body into the abstract domain, and building that abstract body normalizes it. Once the condition of a branch (f, t)#c is abstracted to a literal, the extract folds to the taken target, and rewrite_imm_Extract only rewrites that op. The untaken target is never scheduled, so its call sites never contribute to a join. This works for any condition that normalizes to a literal - including one computed from a propagated expression rather than a plain constant.
Once the lattice is stable, the outer SCCP phase starts rewriting. During rewriting, it can query abstract values for old-world definitions through RWPhase::lattice().
When it sees an application of a lambda whose parameters have propagated values, it rebuilds a specialized lambda:
Which parameters survive is stated once as a Sieve over the old Vars, and all three rebuilds read it back: gather picks the surviving domains and arguments, while operator[] maps each old parameter either to its new Var or - on Gone - to its propagated value.
The invalidate() in the transformation is unrelated to the analysis' fixed point. It tells an enclosing fixed-point PhaseMan that this phase changed the program, so the other phases get another round.
So SCCP follows the standard RWPhase pattern:
Separating SCCP into analysis and rewrite keeps both parts simple:
This separation is the main design pattern to follow for nontrivial optimizations.
The very first line of propagate() is a guard that has no counterpart in the lattice algebra; a second one guards the ⊥ case of the join:
It is the MimIR analogue of the dominance side condition that a classical SSA-based SCCP has to enforce, so it is worth spelling out what it replaces.
Textbook SCCP only ever propagates constants. A constant is a literal: it has no operands and is available at every program point by construction. This is what makes classical SCCP so comfortable — specializing a call site to a constant is always valid, and there is simply no availability question to ask.
MimIR's SCCP is more ambitious: it propagates arbitrary expressions, not just constants (this is essentially copy/expression propagation folded into the same fixed point). The moment you propagate a whole expression, you inherit an obligation constants let you ignore: the expression you substitute must actually be available at the point where it lands. The guard is exactly that availability check.
Textbook SCCP runs on a CFG in SSA form. Every value has exactly one definition, control flow is made explicit by basic blocks and edges, and φ-nodes reconcile the values that arrive along the different predecessor edges of a join block. SCCP assigns each SSA value a lattice cell (⊥ / a constant / ⊤) and, once the fixed point is reached, substitutes the discovered constant at every use of that value.
That substitution is only sound because SSA comes with a dominator tree:
Dominance is exactly the structural guarantee "the value already exists at the program point where I want to use it". Without it, folding a value into a use could move a computation to a place where its operands are not yet defined.
MimIR has no CFG, no basic blocks, and no separate φ instructions. Control flow is expressed in CPS: a Lam is a basic block, its parameters are the φ-nodes, and every App of that Lam is one predecessor edge supplying the corresponding operands. So the SCCP analysis joins, per parameter, all the arguments flowing in from the call sites — precisely the φ-semantics — and stores the result in the lattice().
What is missing is the dominator tree. Its role — deciding whether a candidate value is available at the point where it would be substituted — is taken over by the scope/nesting relation Def::nests, computed structurally from free variables rather than from a precomputed CFG analysis. L->nests(def) holds iff def lives strictly inside L, i.e. it transitively depends on binders introduced below L; a def that only mentions things visible at L's level or further out is not nested.
Now the guard reads directly:
In other words, where classical SCCP walks a dominator tree to certify availability, MimIR asks scope questions: is this value visible at the binder it would replace, and at every caller? Def::nests and Def::in_scope are those availability oracles, and they fall straight out of the free-variable structure that MimIR maintains anyway — no auxiliary dominance computation required.
L->nests(def) only rules out values from below L. A value from a sibling scope passes it, and the join alone never notices when that is wrong:
y is bound by init's continuation, which does not nest exit, so exit happily joins v ↦ y. early passes ⊥, and y ⊔ ⊥ = y — but ⊥ is a contribution that says nothing, not a promise to be compatible with whatever the other sites send. Once y replaces v, exit's body mentions y, so exit now lives inside init's continuation — and early, outside of it, can no longer jump there.
So propagate() checks a ⊥-site, too: the joined value must be in scope at the calling mutable, i.e. cur->in_scope(caller) — every free Var of cur is bound by caller itself or by a mutable that nests caller. Otherwise var is pinned to ⊤. In dominance terms: the definition must dominate every predecessor edge, including the ones that carry no information.
The check needs no ordering: if the ⊥-site happens to be visited before cur arrives, the lattice change triggers another round, and the full round that certifies the fixed point revisits the ⊥-site with the final cur. mem.seo performs the very same ⊥-site check; there, it also catches a φ of an unrelated loop header flowing into a block that a ⊥-site jumps to as well.
The availability obligation is cheap to state but awkward to discharge in most IRs, and this is where MimIR's structural answer stands out.
MimIR sidesteps the dilemma without introducing syntactic scope: it is a scopeless IR. There are no lexical scoping brackets that a Lam opens over its body; instead, scope is implicit, emerging from how free variables nest. Def::nests reads availability straight off that implicit nesting — L nests def iff def transitively depends on a variable bound below L — so the containment a lexical language would spell out with explicit brackets is recovered purely from the free-variable structure MimIR maintains anyway. The query is structural and commits to no schedule, so MimIR gets a compelling, schedule-free answer to the availability question that dominance-based and sea-of-nodes IRs can only reconstruct by (partially) scheduling first.
The availability guard is not the only place where a classical dominance computation fails to materialize.
Contification turns a function that always returns to the same place into a continuation. Here is the canonical example of Fluet & Weeks, transcribed into Mim with their original in the comment.
Both calls to g return to the same continuation k, so g can become a continuation inside f. Their algorithm computes where the contified function goes from the dominator tree of the program's call graph, and proves that choice optimal within their framework. That placement is a real decision with a wrong answer: a continuation may only be jumped to from within its scope, so putting g too far in hides it from some of its call sites, and too far out is not expressible at all.
MimIR never makes the decision. A return continuation is an ordinary parameter, so the join described above already covers it: once every call site passes the same continuation, that parameter is propagated away and g's body transfers control straight to it. Contification is not a separate transformation here — it is what expression propagation looks like when the propagated expression happens to be a Cn.
Placement then takes care of itself, because where a Lam sits is a function of its free variables and not of anything a phase decides. Before propagation g is closed, so it belongs to the top level even when it was written inside f. After propagation g mentions f's continuation, so it belongs inside f. Neither move is carried out by anything; both are readings of the very free-variable structure that Def::nests already queries for availability.
The contrast with a scoped compiler is sharp. MLton runs contification after closure conversion, and Fluet & Weeks describe their own loop example as moving loop back inside sum after closure conversion took it out — a dominator analysis reconstructing a nesting that an earlier phase destroyed. A scopeless IR never loses that nesting, so there is no hoisting-versus-contification phase ordering to get right and no oracle to consult.
A useful rule of thumb is:
For most optimization phases, the preferred structure is:
This keeps analyses and transformations cleanly separated and fits naturally with MimIR's rewriting-based infrastructure.
A simple whole-world rewrite phase:
A simple analysis phase:
Using both:
You can also expose your custom phases as axioms in Mim via the compile plugin and build your own compilation pipeline. Mim's default compilation pipeline is defined in the opt plugin.
Phases are MimIR's main unit of compiler work.
The key design idea is that MimIR phases are built around structured traversal and rewriting. For substantial optimizations, the usual pattern is:
1.18.0