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.Exit, 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.

• 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.InstanceCall, Pseudo.coroutineOverride

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

• 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: Program.staticProcedures.cons, StmtExpr.Assert, StmtExpr.Assume

  • Removes: Pseudo.needsOverrideRules

• 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: Program.staticProcedures.cons, StmtExpr.StaticCall

  • Removes: CompositeType.instanceProcedures.cons, StmtExpr.InstanceCall, StmtExpr.This, Pseudo.coroutineOverride

  • Unsupported: Pseudo.needsOverrideRules

• 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

• 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. Runs before heap parameterization.

  • Creates: TypeDefinition.Composite

  • Removes: CompositeType.typeArgs.cons

• 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.Exit, StmtExpr.IfThenElse, StmtExpr.StaticCall, StmtExpr.LiteralBool

  • Removes: StmtExpr.While.postTest.true

• 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.StaticCall, StmtExpr.Block, StmtExpr.Var

  • Removes: StmtExpr.IncrDecr, StmtExpr.CompoundAssign

• ConstrainedTypeElim: Eliminates constrained types by replacing them with their base types and generating constraint-checking procedures and witness procedures. Type tests against constrained types are rewritten to call the generated constraint procedure.

  • Creates: Program.staticProcedures.cons, StmtExpr.StaticCall

  • Removes: TypeDefinition.Constrained

• EliminateValueInReturns: Rewrites return expr into outParam := expr; return for imperative procedures that have an output parameter. This decouples the return-value assignment from the final Core translation, which no longer needs to know about output parameters when translating returns.

  • 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.Exit, TypeDefinition.Datatype, StmtExpr.StaticCall, 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

• 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.StaticCall, StmtExpr.Block, Pseudo.overload

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

  • Unsupported: StmtExpr.InstanceCall

• HeapParameterization: Transforms procedures that interact with the heap by adding explicit heap parameters. The heap is modeled as TotalMap Composite (TotalMap Field $Box). 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.StaticCall, Procedure.inputs.cons, Pseudo.totalMap, Pseudo.box, Pseudo.heapVar, Pseudo.oldExpr, Pseudo.generatedReturn, Pseudo.statementExpression, Program.staticFields.cons

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

  • Unsupported: CompositeType.typeArgs.cons, TypeDefinition.Constrained, StmtExpr.Throw, StmtExpr.Try, StmtExpr.Return.value.some

• TypeHierarchyTransform: Encodes the object-oriented type hierarchy (inheritance, dynamic dispatch, type tests, and casts) into explicit operations on a flat representation. Composite types with parents are flattened, and dynamic dispatch is resolved through type-test chains.

  • Creates: StmtExpr.StaticCall, StmtExpr.IfThenElse, Pseudo.typeTag

  • Removes: StmtExpr.IsType, StmtExpr.AsType, StmtExpr.New

  • Unsupported: Pseudo.implicitHeap

• 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

• 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: Program.staticFields.cons, Pseudo.heapVar

  • Unsupported: CompositeType.instanceProcedures.cons, StmtExpr.Return.value.some, Procedure.throwsType.some

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

  • Removes: Pseudo.overload

• 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: Program.staticProcedures.cons, StmtExpr.StaticCall

  • Removes: StmtExpr.Hole.deterministic.true

  • Unsupported: StmtExpr.Hole.type.none

• 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

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

  • Creates: StmtExpr.Exit, StmtExpr.Block

  • Removes: StmtExpr.Return, Pseudo.generatedReturn

  • Unsupported: StmtExpr.Try.finally?.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. Must run before the contract pass, which lowers the calls inside those invariants to precondition asserts.

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

• 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, Program.staticFields.cons, Pseudo.overload

• Transparency: Translate a Laurel program to the UnorderedCoreWithLaurelTypes IR.

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.StaticCall, Pseudo.unorderedDeclarations

• Removes: Pseudo.laurelProgram

• Unsupported: Pseudo.overload

• 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, 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 the output parameter — 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 an input parameter, 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.

  • Unsupported: Pseudo.laurelProgram

• 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

• 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

• Ordering: Produce a CoreWithLaurelTypes from a UnorderedCoreWithLaurelTypes 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: Pseudo.orderedDeclarations

  • Removes: Pseudo.unorderedDeclarations

• 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: Pseudo.core

  • Removes: Pseudo.orderedDeclarations

  • Unsupported: StmtExpr.While.postTest.true, 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.unorderedDeclarations, Pseudo.letExpr, StmtExpr.InstanceCall, CompositeType.instanceProcedures.cons, StmtExpr.This