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:
o0: M0 ─────────────────────────────────────▶ M o1: M0 ─▶ promote ─▶ copy ─▶ local_storage ─▶ M
optimization_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 (all three passes), or passes(Names), an ordered subset of o1. Invalid selections fail. Checked or already-local IR stays unchanged.
Passes is the selected sequence. A selection can omit passes but cannot reorder or repeat them, or name an unknown pass.
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; - 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.