Type specialization

Speed mode (-O2) uses inferred facts to remove runtime checks (proofs) and may clone a function into representation variants guarded by runtime tag checks. -O0 and --no-type-specialization produce generic code only: every check stays, every compound access goes through its runtime service.

Proofs

A proof comes only from facts that hold whenever the code runs:

• the facts of a local function's arguments joined from all its callers (Inference::inputs; exported functions and functions named by fun F/A have none);
• the recorded fact of an expression (an operand's fact is recorded before the operation that uses it narrows it);
• a shape test earlier in the same match plan: plan nodes run in a line, so a passed tuple or cons test dominates every later node.

Specifications never prove anything. term() and none() (code inference found unreachable) prove nothing; anonymous fun bodies get no proofs.

Facts reach patterns of function heads (caller-joined arguments), body matches (the right side) and case/try clauses (the scrutinee or try body value); element, head and tail facts follow extractions. An inline read is stored into a root slot like a service output, so frame lowering keeps it as a term across safepoints (reload rule). The only pointer conversions in generated code are these proven reads and the header loads of inline tuple shape tests (proven.cell). Layout constants come from abi/term.hpp; the runtime asserts them against its private cell layouts.

Variants

• Profiles come from call-site facts: an argument whose fact holds only small integers (singletons or ranges) proves a small-integer argument. Specs, broad integer(), unions with other kinds and unknowns stay generic.
• A variant is justified only if it removes an implemented check: an exact low-tag comparison of an argument word anywhere in the body (the argument array is never written, and a collection never changes a small integer).
• Limits: 3 variants per function, 32 per module, 128 per target. Estimated and then actual growth (clone + guards + dispatch + fallback) must stay within 2x the generic instruction count per function and module.
• Generic bodies are always kept. Over-budget drafts are discarded silently; the program never fails because of specialization.
• Selection is deterministic (module, symbol, profile order).

LLVM cloning/simplification replaces proven checks inside the clone. A bounded dispatcher tests every constrained tag and forwards context and arguments to a variant or the generic body; the public symbol and ABI do not change. No spec assumptions or fast-math flags are introduced.

Leaf inlining

At -O2 (codegen/lowering_leaf_inlining.cpp) a call of a small function of the same module that calls no Erlang code except other such leaves lowers the callee's clauses in place of the call. A call costs a frame push and a return through it (about 3 ns), often more than the leaf's own work, and a loop whose step calls a leaf becomes a loop without calls.

• Leaves. No calls except services (inline operations and builtins) and other leaves, nested at most three deep (a leaf, the leaves it calls, and theirs, which call none); no recursion. None of apply/2,3, the raise family (error, exit, throw, raise) or process_info; no funs, comprehensions, receive, try, catch or maybe.
• Budget. A leaf's size counts its expressions and those of the leaves it calls. Each generated function may grow by 48 expressions of inlined leaves; a leaf of at most 12 expressions is about the size of its call and is always inlined. A site the budget cannot pay for stays a call.
• Sites. Local calls and ?MODULE:f() (a remote call of the module itself), outside binary and float loops, also inside inlined funs and list loops.
• Clauses in place. The arguments are matched against the leaf's clauses with the caller's facts about them; the leaf's body runs in the caller's frame with the leaf's own bindings. When no clause matches, the function is called, so function_clause comes from its own code with its arguments.
• Observable cost: an error raised inside an inlined leaf (badarith, badmatch, a failing builtin) has no frame of the leaf in its stack trace (differences).

Constructions

At -O2 (codegen/lowering_constructions.cpp) a match of a tuple or a cons cell built in the same generated function reads the words it was built of instead of the cell; inlined leaves and funs make most such pairs ({Q, R} = divmod(X, 7), case lookup(K) of {ok, V} -> ..., the {Mapped, Acc} of a mapfoldl fun).

• Joins. A value joined from the clauses of an inlined leaf or fun, or of a case, is known when every clause's value is such a construction or an immediate (an atom, a small integer, []); shape tests then become constants per clause, which LLVM threads through.
• Allocation sinking. A cell whose word nothing reads any more is not built. An error that needs the value itself ({case_clause, V}, {badmatch, V}) builds a copy of it on its own path.
• Limits. Only tuples and the first cell of a list are known; a value a loop carries, or one passed in a binary loop, is read from its cell.

Current effect

Proofs act on real source: local functions whose callers pass small integers, tuples and lists lose their tag, shape and service checks (proofs, checked by CTest codegen_proofs and run as the executable golden executables_proofs). A variant must save more instructions than its dispatch costs; one removed tag test of an argument rarely does, so source variants are usually planned and then rejected by the growth limit. Focused LLVM fixtures inject repeated tag checks to exercise hits, fallbacks and growth rollback with native execution.

Executable goldens run under every policy in full mode; fast mode runs -O0 (generic) and -O2 with specialization (proofs).

codegen_measurements writes measurements/<config>/measurements.json in the codegen test build directory (compile time, IR/object bytes, variants, proven reads, native time). Times are descriptive, never thresholds.