opt.pl
The middle end's entry points for the driver, and the comparison the interpreter uses to validate it.
optimize/3 runs the passes at a level, or an explicit ordered subset:
o1Inline, SimplifyM0 → inline → promote → copy → simplify → local_storage → Moptimization_passes/2 names that sequence. optimize_pass/3 runs one member, so the playground can time it and show its actual output without implementing another optimizer. passespromote, copy, for example, leaves local storage off. Ordering stays fixed: local storage introduces a vocabulary the earlier passes do not consume.
refines/2 relates the outcome of a program to the outcome of its optimized version. The driver's difftest and the unit tests validate the optimized IR, rather than repeating that work on every compilation. These passes consume unchecked IR only. A checked module supplied directly (even with -O) is left unchanged: promotion and substitution do not understand proofs or flight projections.
Options is o0 (the reference path), o1 (promote, copy and local storage), o1(small) (inlining of small static functions first, --inline=small), o1(Inline, Simplify) with Inline none, small, wide or wide(Attributes) (--inline=wide, Attributes from c_module/3) and Simplify none or full (the cheap middle end after copy, --simplify=full), or passes(Names), an ordered subset of all five. Invalid selections fail. Checked or already-local IR stays unchanged.
optimize_pass/3, then the stacks back to what is live. SWI's limit counts what is allocated, and each pass leaves a module's worth of garbage: on SQLite the global stack had grown to 1 GB with 250 MB live, so collections were rare and the trail between them doubled to 0.5 GB, overflowing the 1 GB default.
Passes is the selected sequence. A selection can omit passes but cannot reorder or repeat them, or name an unknown pass.
With simplification, inlining's second round takes simplified callees (inline.pl's prepared/3).
Run one named transformation on unchecked, ordinary-address IR. Each pass transports its source contexts alongside executable IR. Unknown names fail; all guards remain in the existing pass modules.
Named local objects are already the storage pass's product. Earlier passes consume ordinary addresses, not this lowered vocabulary.
After is an outcome the original program allows, given that the original's outcome was Before, both from interp:run/5 on the same inputs:
- undefined behaviour allows anything; - running out of memory allows anything: whether an allocation is refused is the runtime's choice (Runtime.v's `alloc` may refuse any), so a program that allocates less may run on; - an unknown result (read of uninitialized bytes in plain mode) allows any value consistent with its constraints; - otherwise the outcomes must be equal. A pointer into an alloc compares by its offset in the object, because removing allocs moves the ones left; data and function addresses do not move.