4.2. Passes🔗

The following passes make up the compilation of Laurel to Core.

Each pass declares how it affects the shapes present in the program, using the vocabulary of NodeKind. A shape is usually an AST constructor, but it can be finer: a constructor together with a condition on one of its fields. StmtExpr.While.postTest.true is a While whose postTest field is true — a do … while loop — and is a shape distinct from a pre-test While. Names read as a path, Owner.field.Leaf, and are qualified by their owner because the same field name occurs on several structures.

Three declarations describe a pass:

creates

Shapes the pass might introduce — it does not always emit one. EliminateDoWhile creates StmtExpr.Goto, because the loop it emits leaves through a labelled exit, but a program with no do … while gets none.

removes

Shapes that are gone once the pass has run. EliminateDoWhile removes StmtExpr.While.postTest.true: afterwards every loop is pre-test.

unsupported

Shapes the pass cannot handle, and which must therefore already be gone. LaurelToCoreSchema declares StmtExpr.While.postTest.true unsupported, matching the diagnostic it raises if one reaches it.

These declarations are what constrains the pipeline order, and they are checked on every build. The check folds the set of live shapes over the passes, starting from the shapes an authored program can contain and applying (live ∖ removes) ∪ creates at each step. Before a pass runs, nothing in its unsupported list may be live. A violation fails the build, naming the pass and the shape.

creates earns its keep through that same check: if a pass re-creates a shape after another has removed it, and a later pass declares it unsupported, the shape is live again when that pass runs and the build fails. So a creates declaration is what forces a pass emitting a shape to precede the pass that eliminates it.

Two limits are worth knowing. The declarations are not verified against the passes themselves — a removes claim is documentation, and several are known to hold only of procedure bodies rather than of a whole program. And shapes named Pseudo.* are not AST constructors at all: they are labels for things like a generated $heap global or the relation between two overloaded procedures, which no traversal can look for. They exist to carry an ordering constraint, and the intent is to remove them as the AST grows the structure to express them directly.

• EliminateStack: Turns Laurel's operand stack into locals: each Stack := e declares a fresh $stack_N, each read of Stack reads the local its statement takes in push order, a value pushed in both arms of an if is copied into one local declared before it, and a push whose value an old(...) reads is evaluated in the pre-state. Runs first, so no later pass sees a Stack; it needs the types resolution gives each push.

  • Creates: StmtExpr.Assign, StmtExpr.Var, StmtExpr.Block, StmtExpr.LiteralBool

  • Removes: StmtExpr.Var.var.Stack

• CoroutineElaboration: Replaces each coroutine declaration with a generated state-machine composite (with resume and has_next instance procedures) and a spawn constructor, and rewrites callers (resume(co[, v]) → co#resume([v]), has_next(co) → co#has_next(), type annotations co: c → co: cState). Must run before LiftInstanceProcedures so the generated instance calls are lifted. Under verifyCoroutine, elaborates instead for the rely/guarantee verification path (see YieldElim).

  • Creates: TypeDefinition.Composite, CompositeType.instanceProcedures.cons, StmtExpr.Call.receiver?.some, Pseudo.coroutineOverride, StmtExpr.OldGuarantee, StmtExpr.OldRelies

  • Removes: Procedure.contracts.Coroutine, StmtExpr.Resume, StmtExpr.HasNext

  • Unsupported: LaurelProgram.staticFunctions.cons, Program.Ordered

• CheckOverrideRefinement: For every composite method that overrides an ancestor method, emits synthetic checker procedures that verify behavioral subtyping: the override's precondition is no stronger than the parent's (Parent.pre ⇒ Child.pre) and its postcondition is no weaker (Child.post ⇒ Parent.post). A failing checker is a Liskov violation. Purely additive; runs before LiftInstanceProcedures. This is the soundness prerequisite for dynamic dispatch.

  • Creates: LaurelProgram.staticProcedures.cons, StmtExpr.Assert, StmtExpr.Assume

  • Removes: Pseudo.needsOverrideRules

  • Unsupported: LaurelProgram.staticFunctions.cons, Program.Ordered

• LiftInstanceProcedures: Lifts every procedure declared inside a composite block to a top-level static procedure named <CompositeName>$<methodName> and rewrites call sites resolved to an instance procedure (including obj#method(args) surface syntax) to point at the lifted name. Clears instanceProcedures on every composite. Must run before HeapParameterization.

  • Creates: LaurelProgram.staticProcedures.cons, StmtExpr.Call

  • Removes: CompositeType.instanceProcedures.cons, StmtExpr.Call.receiver?.some, StmtExpr.This, Pseudo.coroutineOverride

  • Unsupported: Pseudo.needsOverrideRules, LaurelProgram.staticFunctions.cons, Program.Ordered

• InlinePreconditionOf: Replaces each contractOf(precondition, f(args)) with f's checked preconditions, conjoined, its parameters substituted by args. Runs after LiftInstanceProcedures, so every call names a static procedure.

  • Creates: StmtExpr.Call, StmtExpr.LiteralBool

  • Unsupported: Program.Ordered

• TypeAliasElim: Eliminates type aliases by replacing all UserDefined references to alias names with their resolved target types. Chained aliases are resolved transitively. Alias entries are removed from the type list.

  • Removes: TypeDefinition.Alias

  • Unsupported: LaurelProgram.staticFunctions.cons, Program.Ordered

• MonomorphizeComposites: Lowers generic composites (composite Box<T>) by emitting one concrete composite per used instantiation and rewriting Box<int> type references and new Box allocations to the monomorphic name. Each instantiation extends a field-free family parent that names their shared heap fields. Runs before heap parameterization.

  • Creates: TypeDefinition.Composite

  • Removes: CompositeType.typeArgs.cons

  • Unsupported: LaurelProgram.staticFunctions.cons, Program.Ordered

• OpaqueUnusedTypeParams: Replaces each procedure type parameter that occurs in neither an input type nor an output type by a fresh opaque type, declared in the program, and drops it from the procedure's type parameters. The thrown type counts as an output. A call could not determine such a parameter.

  • Unsupported: LaurelProgram.staticFunctions.cons, Program.Ordered

• EliminateDoWhile: Lowers post-test While loops (the do … while form) into the pre-test loop { while(true) invariant I { BODY; if (!COND) exit L } } L, with a fresh $-prefixed exit label L. Runs early so no later pass observes a post-test loop; the invariant is checked at the loop head, matching while.

  • Creates: StmtExpr.While, StmtExpr.Block, StmtExpr.Goto, StmtExpr.IfThenElse, StmtExpr.Call, StmtExpr.LiteralBool

  • Removes: StmtExpr.While.postTest.true

• BindFieldReceivers: Binds a field access's receiver to a fresh $receiver local, ahead of the access, unless the receiver only reads locals and fields that the access does not change, so that the passes after it may repeat or delay any receiver of known type outside a loop's condition.

  • Creates: StmtExpr.Assign, StmtExpr.Block, StmtExpr.Var, Pseudo.statementExpression, Pseudo.imperativeShortCircuit

  • Removes: Pseudo.unstableFieldReceiver

  • Unsupported: StmtExpr.Call.receiver?.some, StmtExpr.Resume, LaurelProgram.staticFunctions.cons, Program.Ordered

• EliminateIncrDecrAndCompoundAssign: Lowers Java-style increment/decrement operators (++x, x++, --x, x--) and C-style compound assignments (x += e, -=, *=, /=, %=, ^=) into existing Laurel assignment and arithmetic constructs. Prefix ++/-- and compound assignment yield the new value; postfix ++/-- yield the old value. Runs early so that no later pass observes an .IncrDecr or .CompoundAssign node.

  • Creates: StmtExpr.Assign, StmtExpr.Call, StmtExpr.Var, StmtExpr.Var.var.Field

  • Removes: StmtExpr.IncrDecr, StmtExpr.CompoundAssign

  • Unsupported: Pseudo.unstableFieldReceiver

• CopyMutatedInputs: Rewrites a body that assigns to an input parameter (legal Laurel, illegal in Core) to assign to a fresh $mutable_… local initialized from the input, renaming the body's references (but not old(...) subtrees or the procedure's specifications, which keep the entry-value reading). Inout inputs — also present in the outputs — are left alone, and a coroutine whose relies/guarantees — or body oldGuarantee/oldRelies — mention a reassigned input is rejected (the body and caller lowerings would read different states). Runs after EliminateIncrDecrAndCompoundAssign so every write is a plain Assign.

  • Creates: StmtExpr.Assign, StmtExpr.Var, StmtExpr.Block

  • Removes: Pseudo.mutatedInput

  • Unsupported: StmtExpr.IncrDecr, StmtExpr.CompoundAssign

• EliminateValueInReturns: Rewrites return expr into outParam := expr; return for imperative procedures that have an output parameter, and return e1, …, en into one assignment per declared output. This decouples the return-value assignment from the final Core translation, which no longer needs to know about output parameters when translating returns. A multi-output return parks its values in temporaries first, so the writes are simultaneous rather than sequential.

  • Creates: StmtExpr.Assign, StmtExpr.Block, StmtExpr.Return

  • Removes: StmtExpr.Return.value.some

  • Unsupported: CompositeType.instanceProcedures.cons

• EliminateExceptions: Lowers the exceptional channel (throw, try/catch/finally, throws/throwsOn) into ordinary Laurel: labeled blocks, exits, and Result datatype construction. A throws T procedure returns a single Result<Val, T>; the in-flight exception rides in $thrown and a per-try $exc_<i> typed at that try's least-common-ancestor exception type, and the result is assembled after the body. Exception contracts become ordinary postconditions over $result. After this pass no Throw/Try remains and the throws type and the cases' postconditions are gone (each case's guard and frame targets are left for ModifiesClauses, which builds the per-case frames and the exhaustiveness claim).

  • Creates: StmtExpr.Block, StmtExpr.Goto, TypeDefinition.Datatype, StmtExpr.Call, StmtExpr.Assign, StmtExpr.IfThenElse, Body.postconditions.cons, Procedure.throwsOn.cons

  • Removes: StmtExpr.Throw, StmtExpr.Try, StmtExpr.Try.finally?.some, Procedure.throwsType.some

  • Unsupported: StmtExpr.Return.value.some, LaurelProgram.staticFunctions.cons, Program.Ordered

• LowerComposite: Lowers composite types to the flat Composite datatype: every composite field becomes a heap field with a qualified name, accessed on the int reference of a Composite; allocation becomes MkComposite($allocate(), C_TypeTag()); each composite type becomes a free constrained type over Composite whose constraint is its tag being one of its descendants'; and reference equality compares the references.

  • Creates: StmtExpr.Call, Procedure.inputs.cons, Procedure.preconditions.cons, Pseudo.typeTag, LaurelProgram.heapFields.cons, TypeDefinition.Constrained

  • Removes: StmtExpr.New, TypeDefinition.Composite

  • Unsupported: CompositeType.typeArgs.cons, CompositeType.instanceProcedures.cons, LaurelProgram.staticFunctions.cons, Program.Ordered

• ConstrainedTypeElim: Eliminates constrained types by replacing them with their base types and generating constraint-checking procedures and witness procedures. A free constraint is assumed wherever a value of its type enters and never asserted. Type tests against constrained types are rewritten to call the generated constraint procedure, and casts to a downcast$T helper that requires it.

  • Creates: LaurelProgram.staticProcedures.cons, StmtExpr.Call

  • Removes: TypeDefinition.Constrained, StmtExpr.IsType, StmtExpr.AsType

  • Unsupported: LaurelProgram.staticFunctions.cons, StmtExpr.Return.value.some, Pseudo.unstableFieldReceiver, Program.Ordered

• YieldElim: Lowers coroutine old-semantics. Body path (verifyCoroutine only): replaces every yield with an inline assert ⋀guarantees; Snapshot $old_heap; havocHeap(); assume ⋀relies; Snapshot $old_heap block. Caller path (always): threads the per-instance $h_rely_old (H1) snapshot heap through resume procedures and callers. Both lower oldGuarantee/oldRelies to labeled Old / Snapshot for HeapParameterization to consume (declaring the snapshot locals and threading $heap); resolution is disabled after this pass.

  • Creates: StmtExpr.Assert, StmtExpr.Assume, StmtExpr.Snapshot, StmtExpr.Old.label?.some, StmtExpr.Call, StmtExpr.Block, Pseudo.overload

  • Removes: StmtExpr.Yield, StmtExpr.OldGuarantee, StmtExpr.OldRelies

  • Unsupported: StmtExpr.Call.receiver?.some, LaurelProgram.staticFunctions.cons, Program.Ordered

• HeapParameterization: Transforms procedures that interact with the heap by adding explicit heap parameters. The heap is modeled as TotalMap int (TotalMap Field $Box), keyed by the reference of a Composite. Procedures that write the heap receive both an input and output heap parameter; procedures that only read the heap receive an input heap parameter. Field reads and writes are rewritten to use readField and updateField functions.

  • Creates: StmtExpr.Call, Procedure.inputs.cons, Pseudo.totalMap, Pseudo.box, Pseudo.heapVar, Pseudo.oldExpr, Pseudo.generatedReturn, Pseudo.statementExpression, LaurelProgram.staticFields.cons

  • Removes: Pseudo.implicitHeap, StmtExpr.Var.var.Field, StmtExpr.PureFieldUpdate, StmtExpr.Snapshot, StmtExpr.Old.label?.some, LaurelProgram.heapFields.cons

  • Unsupported: TypeDefinition.Composite, StmtExpr.New, StmtExpr.IsType, StmtExpr.AsType, TypeDefinition.Constrained, StmtExpr.Throw, StmtExpr.Try, StmtExpr.Return.value.some, LaurelProgram.staticFunctions.cons, Pseudo.unstableFieldReceiver, Program.Ordered

• ModifiesClausesTransform: Translate modifies clauses into frame conditions on the contract.

  • Creates: Body.postconditions.cons, Pseudo.oldExpr, Pseudo.overload

  • Removes: Body.modifies.cons, Procedure.throwsOn.cons

  • Unsupported: Pseudo.implicitHeap, LaurelProgram.staticFunctions.cons, Program.Ordered

• GlobalParameterization: Threads file-scope globals through procedure inputs and writer outputs (entry procedures instead declare them as body-prologue locals initialized from the declaration initializers), then clears staticFields.

  • Creates: StmtExpr.Var, StmtExpr.Assign, Procedure.inputs.cons, Pseudo.statementExpression

  • Removes: LaurelProgram.staticFields.cons, Pseudo.heapVar

  • Unsupported: CompositeType.instanceProcedures.cons, StmtExpr.Return.value.some, Procedure.throwsType.some, LaurelProgram.staticFunctions.cons, Program.Ordered

• PushOldInward: Distributes old(...) over its subexpressions until each old immediately wraps an inout variable. No-op old(...) usage is diagnosed by Resolution.

  • Creates: StmtExpr.Old.value.Var.Local

  • Removes: Pseudo.oldExpr

• InferHoleTypes: Annotates every verification hole (.Hole) in the program with a type inferred from context. This type information is needed by subsequent passes that replace holes with uninterpreted functions or nondeterministic values. TODO: this pass should be removed by improving Resolution to assign a concrete type to every hole during type checking (see the module doc for the type-variable approach), making this pass obsolete.

  • Creates: StmtExpr.Hole.type.some

  • Removes: StmtExpr.Hole.type.none

• EliminateDeterministicHoles: Replaces every deterministic hole with a call to a freshly generated uninterpreted function. After this pass the program contains only non-deterministic holes. Assumes InferHoleTypes has already annotated holes with types.

  • Creates: LaurelProgram.staticProcedures.cons, StmtExpr.Call

  • Removes: StmtExpr.Hole.deterministic.true

  • Unsupported: StmtExpr.Hole.type.none, LaurelProgram.staticFunctions.cons, Program.Ordered

• UniqueOverloadNames: Renames overloaded static procedures to unique names so downstream name-keyed passes don't see collisions.

  • Removes: Pseudo.overload

  • Unsupported: LaurelProgram.staticFunctions.cons, StmtExpr.Hole.type.none, Program.Ordered

• DesugarShortCircuit: Rewrites a short-circuit boolean operator (&&, ||, =>) into a conditional expression when its guarded operand contains an assignment or an imperative call. Short-circuits over pure operands are left alone, and the Core translator handles them. This must precede LiftImperativeExpressions, which would otherwise hoist the imperative call out of the branch that guards it.

  • Creates: StmtExpr.IfThenElse, Pseudo.statementExpression

  • Removes: Pseudo.imperativeShortCircuit

  • Unsupported: LaurelProgram.staticFunctions.cons, Program.Ordered

• EliminateReturnStatements: Lower return statements to exit statements. Wrap each procedure body with a 'return' block

  • Creates: StmtExpr.Goto, StmtExpr.Block

  • Removes: StmtExpr.Return, Pseudo.generatedReturn

  • Unsupported: StmtExpr.Try.finally?.some

• RestructureGotos: Lowers a labelled block that some goto jumps back into to { while(true) invariant I decreases D { { S'; exit L } $goto_start_n } } L, where S' redirects each goto L to exit $goto_start_n. A labelled block with invariants but no backward jump asserts them on entry instead. Afterwards Core sees only structured control flow: forward exits and while loops.

  • Creates: StmtExpr.While, StmtExpr.Block, StmtExpr.Goto, StmtExpr.LiteralBool, StmtExpr.Assert

  • Removes: StmtExpr.Goto.destination.blockStart, StmtExpr.Block.invariants.cons, StmtExpr.Block.decreases.some

• LoopInvariantWellFormedness: Emits if * { havoc(loop targets); assume each invariant in order; assume false } before each loop carrying invariants, so invariant well-formedness is checked at the loop head (where the invariant is assumed) rather than in the loop's pre-state (where more is known and the obligation can be vacuously discharged). Assuming each invariant in turn lets a later invariant's well-formedness rely on the earlier ones.

  • Creates: StmtExpr.IfThenElse, StmtExpr.Hole.deterministic.false, StmtExpr.Assign, StmtExpr.Assume

  • Removes: Pseudo.needsLoopInvariantChecks

  • Unsupported: StmtExpr.Goto.destination.blockStart, StmtExpr.Block.invariants.cons, StmtExpr.Block.decreases.some

• Contracts: Lowers pre and postcondition to assertions and assumptions around call-sites and procedure bodies

  • Creates: StmtExpr.Assert, StmtExpr.Assume

  • Removes: Procedure.preconditions.cons, Body.postconditions.cons

  • Unsupported: StmtExpr.Return, LaurelProgram.staticFields.cons, Pseudo.overload, LaurelProgram.staticFunctions.cons, Program.Ordered

• Transparency: Split a Laurel program's procedures into staticFunctions (Core functions) and staticProcedures (Core procedures).

This pass has three modes:

• Execute

• Verify

• BothSuboptimally

BothSuboptimally mode allows the translated program to be used both for interpretation and for verification, but it won't perform as well when verified, sometimes letting the SMT solver return UNKNOWN instead of SAT. For interpretation it'll execute performantly, but the compilation time will be unnecessarily long since Core functions will be created but not used.

For each procedure, BothSuboptimally mode will:

• Generate a function with the same signature, named foo$asFunction. The procedure and associated function are called a twin.

• If transparent, the function gets a functional body (assertions erased, all calls are to functional siblings)

• If the function has a body, add a free postcondition equating the procedure output to the function. This postcondition is called the 'bridge' and it's this bridge that regresses verification performance because it introduces additional quantifiers.

Execute mode will create as few procedures as necessary. When interpreting, all calls will be to procedures. Currently execute mode still creates some functions because calls from quantifiers can only be to functions and can't be lifted, but this may change.

Verify mode will change all calls to be to functions and no longer generate the bridges between twins. Currently, verify mode still needs some calls to be to procedures, because:

• We are not yet able to generate function twins for procedures with multiple output parameters

• There is a bug in Core's partial evaluator that causes its runtime to become exponential when calling bodiless functions.

Since execute mode tries not to generate any functions, it could work well even if the heap is still implicit. Maybe instead of the transparency pass we should define a separate 'Execute' and 'Verify' pass, where only the latter needs to come after the heap encoding.

• Creates: Pseudo.asFunctionTwin, Condition.mode.Assume, StmtExpr.Call, LaurelProgram.staticFunctions.cons, Pseudo.statementExpression, Pseudo.letExpr, Pseudo.imperativeFunction

• Unsupported: Pseudo.overload, Program.Ordered

• PackageFunctionOutputsPass: Rewrites a function that yields several outputs into one that yields a single value of a generated datatype holding all of them: it declares the datatype, holding all of that function's outputs in a single constructor, replaces the output list with a single output of that datatype's type, declares each output it drops as a bare local at the top of the body (reusing that output's uniqueId, and skipping an inout, which shares an input's binding), and rewrites a call filling several targets into one call binding the packaged value plus one projection per target. Runs before FunctionalRewrite, which rejects an assignment to several targets, and which places the constructor call the body evaluates to — reading the outputs' names, types and order back off the datatype declared here.

  • Creates: StmtExpr.Assign, StmtExpr.Call

  • Unsupported: Program.Ordered

• FunctionalRewritePass: Rewrites a function body from imperative form into a single pure expression by continuation passing: an assignment becomes a shadowing declaration whose scope is the statements that follow it, an exit $return becomes a reference to the output parameter (or, for a function whose outputs PackageFunctionOutputs replaced with a single packaged one, a call to that datatype's constructor over the outputs it dropped), an exit L becomes the continuation of the block labelled L, and an if-then-else becomes an if-expression whose branches each end in the continuation, and every variable the body leaves uninitialized — a declaration without an initializer, and each output parameter that is not an inout — is bound at the top of the body to a deterministic hole (a call to a generated uninterpreted function), so reading one yields an arbitrary-but-fixed value and an assignment shadows it. This removes the label mechanism and so supports early exits and exits to user labels. A body containing a construct with no functional form (a loop, an assignment to several targets) is reported as a user error; a construct an earlier pass should have eliminated (an assert, an assume, a call, a field assignment) is reported as a Strata bug.

  • Creates: Pseudo.letExpr

  • Removes: Pseudo.imperativeFunction

  • Unsupported: Program.Ordered

• LiftImperativeExpressions: Lifts assignments, assertions, assumptions and calls to a configurable list of procedures, that appear in expression contexts, to preceding statements. Lifting is necessary because Strata Core does not support assignments, assumes, asserts and calls to Core procedures within expressions. The pass introduces fresh temporary variables where needed. Lifting expressions that occur in conditional control flow that is also in an expression, can require duplicating some of that control flow. If we do not encode the heap before the lifting pass, we will need to lift any calls to heap mutating procedures, since they are implicitly mutating. The Laurel resolver should be able to tell us which procedures are heap mutating, so this is simple.

  • Creates: StmtExpr.Var, StmtExpr.Assign, StmtExpr.Block

  • Removes: Pseudo.statementExpression

  • Unsupported: Pseudo.imperativeShortCircuit, StmtExpr.IncrDecr, StmtExpr.CompoundAssign, Program.Ordered

• InlineLocalVariables: Inlines local variable declarations of the form var <name> := <expr> in function bodies. References to the variable after its declaration are replaced with the initializer expression, and the declaration is removed. Assignments to an inlined variable emit a diagnostic. Operates only on functions, which are pure and cannot carry local variable declarations into Core.

  Currently, Core does not support encoding let expression, even using lambda applications, which is why this pass exists. When Core does support encoding let expression, this pass should be removed.

  • Removes: Pseudo.letExpr

  • Unsupported: StmtExpr.IncrDecr, Program.Ordered

• Ordering: Produce a CoreWithLaurelTypes from a LaurelProgram by computing a combined ordering of functions and proofs using the call graph, then collecting datatypes and constants. Functions are grouped into SCCs (for mutual recursion). Proofs are emitted as individual procedure decls. Both participate in the topological ordering so that axioms are available to functions that need them.

  • Creates: Program.Ordered, OrderedProgram.WithLaurelTypes

  • Removes: Program.Unordered

• LaurelToCoreSchema: Produce a Core program from a CoreWithLaurelTypes program. Intended to be dumb 1-to-1 translation. However, there are several smart translations still happening:

  • The @[cases] parameter is inferred for recursive functions.

  • Laurel parameter definitions are translated to Core ones.

  • Laurel calling conventions are translated to Core ones.

  • Creates: OrderedProgram.Core

  • Removes: OrderedProgram.WithLaurelTypes

  • Unsupported: StmtExpr.While.postTest.true, StmtExpr.Goto.destination.blockStart, StmtExpr.Block.invariants.cons, StmtExpr.Block.decreases.some, StmtExpr.IncrDecr, StmtExpr.CompoundAssign, StmtExpr.Var.var.Field, StmtExpr.PureFieldUpdate, StmtExpr.IsType, StmtExpr.AsType, StmtExpr.New, StmtExpr.Old.label?.some, Pseudo.oldExpr, StmtExpr.Throw, StmtExpr.Try, StmtExpr.Yield, StmtExpr.Resume, StmtExpr.HasNext, StmtExpr.Hole.deterministic.true, CompositeType.typeArgs.cons, Pseudo.statementExpression, Pseudo.letExpr, StmtExpr.Call.receiver?.some, CompositeType.instanceProcedures.cons, StmtExpr.This, Pseudo.imperativeFunction, Program.Unordered, TypeDefinition.Alias, Pseudo.needsLoopInvariantChecks, Pseudo.mutatedInput, Procedure.contracts.Coroutine, StmtExpr.OldGuarantee, StmtExpr.OldRelies

V starts holding here   | holds, and is carried on   + required here, holds, and is carried on
' was holding, and is dropped here   : not holding, but would be carried   (blank) not holding, and would not be carried
S: LaurelProgram.staticFunctions.cons   O: Program.Ordered   N: Pseudo.needsOverrideRules
C: StmtExpr.Call.receiver?.some   R: StmtExpr.Resume   U: Pseudo.unstableFieldReceiver
I: StmtExpr.IncrDecr   Co: StmtExpr.CompoundAssign   Ic: CompositeType.instanceProcedures.cons
Rv: StmtExpr.Return.value.some   T: CompositeType.typeArgs.cons   tC: TypeDefinition.Composite
Ne: StmtExpr.New   Is: StmtExpr.IsType   A: StmtExpr.AsType
tO: TypeDefinition.Constrained   Th: StmtExpr.Throw   Tr: StmtExpr.Try
Im: Pseudo.implicitHeap   Ts: Procedure.throwsType.some   H: StmtExpr.Hole.type.none
Tf: StmtExpr.Try.finally?.some   G: StmtExpr.Goto.destination.blockStart   B: StmtExpr.Block.invariants.cons
Bd: StmtExpr.Block.decreases.some   Re: StmtExpr.Return   Sc: LaurelProgram.staticFields.cons
Ov: Pseudo.overload   pI: Pseudo.imperativeShortCircuit   W: StmtExpr.While.postTest.true
V: StmtExpr.Var.var.Field   P: StmtExpr.PureFieldUpdate   Ol: StmtExpr.Old.label?.some
pO: Pseudo.oldExpr   Y: StmtExpr.Yield   Ha: StmtExpr.HasNext
Hd: StmtExpr.Hole.deterministic.true   St: Pseudo.statementExpression   L: Pseudo.letExpr
sT: StmtExpr.This   pM: Pseudo.imperativeFunction   Un: Program.Unordered
Al: TypeDefinition.Alias   pN: Pseudo.needsLoopInvariantChecks   M: Pseudo.mutatedInput
CC: Procedure.contracts.Coroutine   sO: StmtExpr.OldGuarantee   sL: StmtExpr.OldRelies

                                      S   N   R   I   Ic  T   Ne  A   Th  Im  H   G   Bd  Sc  pI  V   Ol  Y   Hd  L   pM  Al  M   sO
phase                                   O   C   U   Co  Rv  tC  Is  tO  Tr  Ts  Tf  B   Re  Ov  W   P   pO  Ha  St  sT  Un  pN  CC  sL
 1 EliminateStack                     | | : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : | : : : : : | : | : : : : : : :
 2 CoroutineElaboration               + + :   V : : :   : :   : : : : : : : : : : : : : : : : : : : : | : : V : : | : | : : : : V
 3 CheckOverrideRefinement            + + V : | : : : : : : : : : : : : : : : : : : : : : : : : : : : | : : | : : | : | : : : : | : :
 4 LiftInstanceProcedures             + + + V | : : : V : : : : : : : : : : : : : : : : : : : : : : : | : : | : : | V | : : : : | : :
 5 InlinePreconditionOf               | + | | | : : : | : : : : : : : : : : : : : : : : : : : : : : : | : : | : : | | | : : : : | : :
 6 TypeAliasElim                      + + | | | : : : | : : : : : : : : : : : : : : : : : : : : : : : | : : | : : | | | : V : : | : :
 7 MonomorphizeComposites             + + | | | : : : | : V   : : : : : : : : : : : : : : : : : : : : | : : | : : | | | : | : : | : :
 8 OpaqueUnusedTypeParams             + + | | | : : : | : | : : : : : : : : : : : : : : : : : : : : : | : : | : : | | | : | : : | : :
 9 EliminateDoWhile                   | | | | | : : : | : | : : : : : : : : : : : : : : : : : : V : : | : : | : : | | | : | : : | : :
10 BindFieldReceivers                 + + | + + V : : | : | : : : : : : : : : : : : : : : : :   | : : | : : | :   | | | : | : : | : :
11 EliminateIncrDecrAndCompoundAssign | | | | | + V V | : | : : : : : : : : : : : : : : : : : : |   : | : : | : : | | | : | : : | : :
12 CopyMutatedInputs                  | | | | | | + + | : | : : : : : : : : : : : : : : : : : : | : : | : : | : : | | | : | : V | : :
13 EliminateValueInReturns            | | | | | | | | + V | : : : : : : : : : : : : : :   : : : | : : | : : | : : | | | : | : | | : :
14 EliminateExceptions                + + | | | | | | | + | : : : : : V V : V : V : : : : : : : | : : | : : | : : | | | : | : | | : :
15 LowerComposite                     + + | | | | | | + | + V V : :   | | : | : | : : : : : : : | : : | : : | : : | | | : | : | | : :
16 ConstrainedTypeElim                + + | | | + | | | + | | | V V V | | : | : | : : : : : : : | : : | : : | : : | | | : | : | | : :
17 YieldElim                          + + | + | | | | | | | | | | | | | | : | : | : : : : :   : | : : ' : V | : : | | | : | : | | V V
18 HeapParameterization               + + | | | + | | | + | + + + + + + + V | : | : : : :   : : | V V V   | | :   | | | : | : | | | |
19 ModifiesClausesTransform           + + | | | | | | | | | | | | | | | | + | : | : : : : :   : | | | |   | | : : | | | : | : | | | |
20 GlobalParameterization             + + | | | | | | + + | | | | | | | | | + : | : : : : V : : | | | | : | | :   | | | : | : | | | |
21 PushOldInward                      | | | | | | | | | | | | | | | | | | | | : | : : : : | : : | | | | V | | : : | | | : | : | | | |
22 InferHoleTypes                     | | | | | | | | | | | | | | | | | | | | V | : : : : | : : | | | | | | | : : | | | : | : | | | |
23 EliminateDeterministicHoles        + + | | | | | | | | | | | | | | | | | | + | : : : : | : : | | | | | | | V : | | | : | : | | | |
24 UniqueOverloadNames                + + | | | | | | | | | | | | | | | | | | + | : : : : | V : | | | | | | | | : | | | : | : | | | |
25 DesugarShortCircuit                + + | | | | | | | | | | | | | | | | | | | | : : : : | | V | | | | | | | |   | | | : | : | | | |
26 EliminateReturnStatements          | | | | | | | | | | | | | | | | | | | | | + : : : V | | | | | | | | | | | : | | | : | : | | | |
27 RestructureGotos                   | | | | | | | | | | | | | | | | | | | | | | V V V | | | | | | | | | | | | : | | | : | : | | | |
28 LoopInvariantWellFormedness        | | | | | | | | | | | | | | | | | | | | | | + + + | | | | | | | | | | | | : | | | : | V | | | |
29 Contracts                          + + | | | | | | | | | | | | | | | | | | | | | | | + + + | | | | | | | | | : | | | : | | | | | |
30 Transparency                       ' + | | | | | | | | | | | | | | | | | | | | | | | | | + | | | | | | | | |   ' | ' : | | | | | |
31 PackageFunctionOutputsPass         : + | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | : : | : : | | | | | |
32 FunctionalRewritePass              : + | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | :   | V : | | | | | |
33 LiftImperativeExpressions          : + | | | | + + | | | | | | | | | | | | | | | | | | | | + | | | | | | | | V : | | : | | | | | |
34 InlineLocalVariables               : + | | | | + | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | V | | : | | | | | |
35 Ordering                           : ' | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | V | | | | | |
36 LaurelToCoreSchema                 : : | + + | + + + | + | + + + | + + | | | | + + + | | | | + + + + + + + + + + + + + + + + + + +