Laurel Implementor Guide

4.3. Pass Dependency Graph🔗

The ordering constraints between passes, derived from the declarations above rather than written by hand. Each edge names the shape that ties the two passes together, and whether the later pass cannot handle that shape, and which pass removed it (removes → unsupported).

Dependency edges (A → B means A must run before B). Every edge is derived from the passes' declared node kinds:

  • CheckOverrideRefinement → LiftInstanceProcedures

    • via Pseudo.needsOverrideRules (removes → unsupported)

  • LiftInstanceProcedures → BindFieldReceivers

    • via StmtExpr.Call.receiver?.some (removes → unsupported)

  • CoroutineElaboration → BindFieldReceivers

    • via StmtExpr.Resume (removes → unsupported)

  • BindFieldReceivers → EliminateIncrDecrAndCompoundAssign

    • via Pseudo.unstableFieldReceiver (removes → unsupported)

  • EliminateIncrDecrAndCompoundAssign → CopyMutatedInputs

    • via StmtExpr.IncrDecr (removes → unsupported), StmtExpr.CompoundAssign (removes → unsupported)

  • LiftInstanceProcedures → EliminateValueInReturns

    • via CompositeType.instanceProcedures.cons (removes → unsupported)

  • EliminateValueInReturns → EliminateExceptions

    • via StmtExpr.Return.value.some (removes → unsupported)

  • MonomorphizeComposites → LowerComposite

    • via CompositeType.typeArgs.cons (removes → unsupported)

  • LiftInstanceProcedures → LowerComposite

    • via CompositeType.instanceProcedures.cons (removes → unsupported)

  • EliminateValueInReturns → ConstrainedTypeElim

    • via StmtExpr.Return.value.some (removes → unsupported)

  • BindFieldReceivers → ConstrainedTypeElim

    • via Pseudo.unstableFieldReceiver (removes → unsupported)

  • LiftInstanceProcedures → YieldElim

    • via StmtExpr.Call.receiver?.some (removes → unsupported)

  • LowerComposite → HeapParameterization

    • via TypeDefinition.Composite (removes → unsupported), StmtExpr.New (removes → unsupported)

  • ConstrainedTypeElim → HeapParameterization

    • via StmtExpr.IsType (removes → unsupported), StmtExpr.AsType (removes → unsupported), TypeDefinition.Constrained (removes → unsupported)

  • EliminateExceptions → HeapParameterization

    • via StmtExpr.Throw (removes → unsupported), StmtExpr.Try (removes → unsupported)

  • EliminateValueInReturns → HeapParameterization

    • via StmtExpr.Return.value.some (removes → unsupported)

  • BindFieldReceivers → HeapParameterization

    • via Pseudo.unstableFieldReceiver (removes → unsupported)

  • HeapParameterization → ModifiesClausesTransform

    • via Pseudo.implicitHeap (removes → unsupported)

  • LiftInstanceProcedures → GlobalParameterization

    • via CompositeType.instanceProcedures.cons (removes → unsupported)

  • EliminateValueInReturns → GlobalParameterization

    • via StmtExpr.Return.value.some (removes → unsupported)

  • EliminateExceptions → GlobalParameterization

    • via Procedure.throwsType.some (removes → unsupported)

  • InferHoleTypes → EliminateDeterministicHoles

    • via StmtExpr.Hole.type.none (removes → unsupported)

  • InferHoleTypes → UniqueOverloadNames

    • via StmtExpr.Hole.type.none (removes → unsupported)

  • EliminateExceptions → EliminateReturnStatements

    • via StmtExpr.Try.finally?.some (removes → unsupported)

  • RestructureGotos → LoopInvariantWellFormedness

    • via StmtExpr.Goto.destination.blockStart (removes → unsupported), StmtExpr.Block.invariants.cons (removes → unsupported), StmtExpr.Block.decreases.some (removes → unsupported)

  • EliminateReturnStatements → Contracts

    • via StmtExpr.Return (removes → unsupported)

  • GlobalParameterization → Contracts

    • via LaurelProgram.staticFields.cons (removes → unsupported)

  • UniqueOverloadNames → Contracts

    • via Pseudo.overload (removes → unsupported)

  • UniqueOverloadNames → Transparency

    • via Pseudo.overload (removes → unsupported)

  • DesugarShortCircuit → LiftImperativeExpressions

    • via Pseudo.imperativeShortCircuit (removes → unsupported)

  • EliminateIncrDecrAndCompoundAssign → LiftImperativeExpressions

    • via StmtExpr.IncrDecr (removes → unsupported), StmtExpr.CompoundAssign (removes → unsupported)

  • EliminateIncrDecrAndCompoundAssign → InlineLocalVariables

    • via StmtExpr.IncrDecr (removes → unsupported)

  • EliminateDoWhile → LaurelToCoreSchema

    • via StmtExpr.While.postTest.true (removes → unsupported)

  • RestructureGotos → LaurelToCoreSchema

    • via StmtExpr.Goto.destination.blockStart (removes → unsupported), StmtExpr.Block.invariants.cons (removes → unsupported), StmtExpr.Block.decreases.some (removes → unsupported)

  • EliminateIncrDecrAndCompoundAssign → LaurelToCoreSchema

    • via StmtExpr.IncrDecr (removes → unsupported), StmtExpr.CompoundAssign (removes → unsupported)

  • HeapParameterization → LaurelToCoreSchema

    • via StmtExpr.Var.var.Field (removes → unsupported), StmtExpr.PureFieldUpdate (removes → unsupported), StmtExpr.Old.label?.some (removes → unsupported)

  • ConstrainedTypeElim → LaurelToCoreSchema

    • via StmtExpr.IsType (removes → unsupported), StmtExpr.AsType (removes → unsupported)

  • LowerComposite → LaurelToCoreSchema

    • via StmtExpr.New (removes → unsupported)

  • PushOldInward → LaurelToCoreSchema

    • via Pseudo.oldExpr (removes → unsupported)

  • EliminateExceptions → LaurelToCoreSchema

    • via StmtExpr.Throw (removes → unsupported), StmtExpr.Try (removes → unsupported)

  • YieldElim → LaurelToCoreSchema

    • via StmtExpr.Yield (removes → unsupported), StmtExpr.OldGuarantee (removes → unsupported), StmtExpr.OldRelies (removes → unsupported)

  • CoroutineElaboration → LaurelToCoreSchema

    • via StmtExpr.Resume (removes → unsupported), StmtExpr.HasNext (removes → unsupported), Procedure.contracts.Coroutine (removes → unsupported)

  • EliminateDeterministicHoles → LaurelToCoreSchema

    • via StmtExpr.Hole.deterministic.true (removes → unsupported)

  • MonomorphizeComposites → LaurelToCoreSchema

    • via CompositeType.typeArgs.cons (removes → unsupported)

  • LiftImperativeExpressions → LaurelToCoreSchema

    • via Pseudo.statementExpression (removes → unsupported)

  • InlineLocalVariables → LaurelToCoreSchema

    • via Pseudo.letExpr (removes → unsupported)

  • LiftInstanceProcedures → LaurelToCoreSchema

    • via StmtExpr.Call.receiver?.some (removes → unsupported), CompositeType.instanceProcedures.cons (removes → unsupported), StmtExpr.This (removes → unsupported)

  • FunctionalRewritePass → LaurelToCoreSchema

    • via Pseudo.imperativeFunction (removes → unsupported)

  • Ordering → LaurelToCoreSchema

    • via Program.Unordered (removes → unsupported)

  • TypeAliasElim → LaurelToCoreSchema

    • via TypeDefinition.Alias (removes → unsupported)

  • LoopInvariantWellFormedness → LaurelToCoreSchema

    • via Pseudo.needsLoopInvariantChecks (removes → unsupported)

  • CopyMutatedInputs → LaurelToCoreSchema

    • via Pseudo.mutatedInput (removes → unsupported)

Pipeline execution order (→ X: must run before X; ← X: must run after X):

1. EliminateStack
2. CoroutineElaboration → BindFieldReceivers → LaurelToCoreSchema
3. CheckOverrideRefinement → LiftInstanceProcedures
4. LiftInstanceProcedures → BindFieldReceivers → EliminateValueInReturns → LowerComposite → YieldElim → GlobalParameterization → LaurelToCoreSchema ← CheckOverrideRefinement
5. InlinePreconditionOf
6. TypeAliasElim → LaurelToCoreSchema
7. MonomorphizeComposites → LowerComposite → LaurelToCoreSchema
8. OpaqueUnusedTypeParams
9. EliminateDoWhile → LaurelToCoreSchema
10. BindFieldReceivers → EliminateIncrDecrAndCompoundAssign → ConstrainedTypeElim → HeapParameterization ← LiftInstanceProcedures ← CoroutineElaboration
11. EliminateIncrDecrAndCompoundAssign → CopyMutatedInputs → LiftImperativeExpressions → InlineLocalVariables → LaurelToCoreSchema ← BindFieldReceivers
12. CopyMutatedInputs → LaurelToCoreSchema ← EliminateIncrDecrAndCompoundAssign
13. EliminateValueInReturns → EliminateExceptions → ConstrainedTypeElim → HeapParameterization → GlobalParameterization ← LiftInstanceProcedures
14. EliminateExceptions → HeapParameterization → GlobalParameterization → EliminateReturnStatements → LaurelToCoreSchema ← EliminateValueInReturns
15. LowerComposite → HeapParameterization → LaurelToCoreSchema ← MonomorphizeComposites ← LiftInstanceProcedures
16. ConstrainedTypeElim → HeapParameterization → LaurelToCoreSchema ← EliminateValueInReturns ← BindFieldReceivers
17. YieldElim → LaurelToCoreSchema ← LiftInstanceProcedures
18. HeapParameterization → ModifiesClausesTransform → LaurelToCoreSchema ← LowerComposite ← ConstrainedTypeElim ← EliminateExceptions ← EliminateValueInReturns ← BindFieldReceivers
19. ModifiesClausesTransform ← HeapParameterization
20. GlobalParameterization → Contracts ← LiftInstanceProcedures ← EliminateValueInReturns ← EliminateExceptions
21. PushOldInward → LaurelToCoreSchema
22. InferHoleTypes → EliminateDeterministicHoles → UniqueOverloadNames
23. EliminateDeterministicHoles → LaurelToCoreSchema ← InferHoleTypes
24. UniqueOverloadNames → Contracts → Transparency ← InferHoleTypes
25. DesugarShortCircuit → LiftImperativeExpressions
26. EliminateReturnStatements → Contracts ← EliminateExceptions
27. RestructureGotos → LoopInvariantWellFormedness → LaurelToCoreSchema
28. LoopInvariantWellFormedness → LaurelToCoreSchema ← RestructureGotos
29. Contracts ← EliminateReturnStatements ← GlobalParameterization ← UniqueOverloadNames
30. Transparency ← UniqueOverloadNames
31. PackageFunctionOutputsPass
32. FunctionalRewritePass → LaurelToCoreSchema
33. LiftImperativeExpressions → LaurelToCoreSchema ← DesugarShortCircuit ← EliminateIncrDecrAndCompoundAssign
34. InlineLocalVariables → LaurelToCoreSchema ← EliminateIncrDecrAndCompoundAssign
35. Ordering → LaurelToCoreSchema
36. LaurelToCoreSchema ← EliminateDoWhile ← RestructureGotos ← EliminateIncrDecrAndCompoundAssign ← HeapParameterization ← ConstrainedTypeElim ← LowerComposite ← PushOldInward ← EliminateExceptions ← YieldElim ← CoroutineElaboration ← EliminateDeterministicHoles ← MonomorphizeComposites ← LiftImperativeExpressions ← InlineLocalVariables ← LiftInstanceProcedures ← FunctionalRewritePass ← Ordering ← TypeAliasElim ← LoopInvariantWellFormedness ← CopyMutatedInputs