4. Compilation to Core
To enable its verification analyses, Laurel compiles to Core. Compilation happens over many passes.
A compilation pass may not change the semantics of the program. User errors may only be reported
during resolution (resolve, which the pipeline re-runs after passes that set needsResolves),
never by a pass — there are no exceptions to this rule. Every diagnostic emitted by a pass is a bug
report (MessageKind.strataBug), where a "bug" includes features that are planned but not yet
supported: for example, InlineLocalVariables reporting an assignment to a variable it has inlined.
A compilation pass may only refer to AST nodes that relate to its business
logic: it may not define AST traversals without using helper methods, to allow adding new AST nodes
without breaking existing compilation passes. The generic traversal helpers live in
MapStmtExpr.lean: mapStmtExprM (bottom-up monadic rewrite of a StmtExpr tree),
mapStmtExprPrePostM (pre- and post-order rewrite), foldStmtExprM/foldStmtExpr (accumulate over
every node), and collectStmtExprList (gather a list from every node). The same file lifts these to
the surrounding structure with mapProcedureBodiesM, mapProgramM, and the *HighTypes* variants
(e.g. mapStmtExprHighTypesM, mapProgramHighTypesM) that rewrite the HighType annotations. A
pass pattern-matches the handful of constructors it cares about in the function it passes to one of
these and falls through for the rest, so it never spells out the full StmtExpr case split.
If new references or definitions are created during compilation, the program must be re-resolved to
get a complete model. A pass does not call Resolution.resolve itself; instead it sets
needsResolves := true in its definition, and the pipeline driver
(LaurelCompilationPipeline.lean) runs resolve after the pass and threads the refreshed
SemanticModel into the next pass. The passes YieldElim,
HeapParameterization, TypeHierarchy, and ModifiesClauses (in pipeline order) are
logically one step: all but the last set needsResolves := false to suppress the intermediate
re-resolutions, and the last member (ModifiesClauses) sets needsResolves := true, so the group
is re-resolved once at its end. The coroutine lowering relies on this: YieldElim emits transient
Snapshot/labeled-Old artifacts (and a havocHeap() call) that have no resolution support
and must reach HeapParameterization — which lowers them — without an intervening re-resolve.
Eliminated constructs stay eliminated
Several passes exist to eliminate a construct: after EliminateReturnStatements no Return
occurs, after EliminateIncrDecrAndCompoundAssign no IncrDecr or CompoundAssign, and after the
hole passes (InferHoleTypes types every hole, EliminateDeterministicHoles replaces deterministic
holes with fresh opaque $hole_N procedures, LiftImperativeExpressions havocs the
non-deterministic ones) no .Hole. Later passes rely on these facts, so a pass must not reintroduce
a construct past its elimination point. Breaking this rarely fails at the offending pass; it
surfaces where the reliance is, which can be as late as the Core translation — a leaked hole is
reported there as holes should have been eliminated before translation, far from the pass that
leaked it. The same distance applies to the other eliminated constructs.