From a03ea65d736ec7fee1c745d7ceb8fda5a4fd9a48 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 10 Sep 2022 14:06:38 +0200 Subject: [PATCH] refactor: monadic compiler test framework style + new pass manager --- src/Lean/Compiler/LCNF/PassManager.lean | 16 +- src/Lean/Compiler/LCNF/Testing.lean | 216 ++++++++++++------ tests/lean/CompilerCSE.lean | 4 +- tests/lean/CompilerCSE.lean.expected.out | 8 +- tests/lean/CompilerFindJoinPoints.lean | 4 +- .../CompilerFindJoinPoints.lean.expected.out | 9 +- tests/lean/CompilerPullInstances.lean | 4 +- .../CompilerPullInstances.lean.expected.out | 8 +- tests/lean/CompilerSimp.lean | 4 +- tests/lean/CompilerSimp.lean.expected.out | 12 +- 10 files changed, 187 insertions(+), 98 deletions(-) diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean index c2254a2f4d..e3a0a9ccde 100644 --- a/src/Lean/Compiler/LCNF/PassManager.lean +++ b/src/Lean/Compiler/LCNF/PassManager.lean @@ -18,10 +18,10 @@ inductive Phase where | /-- Here we still carry most of the original type information, most of the dependent portion is already (partially) erased though. -/ base -| /-- Here all types have been turned into `Any`. -/ - untyped -| /-- The lambda RC representation use for reference counting optimizations. -/ - rc +| /-- In this phase polymorphism has been eliminated. -/ + mono +| /-- In this phase impure stuff such as RC or efficient BaseIO transformations happen. -/ + impure deriving Inhabited /-- @@ -74,8 +74,8 @@ namespace Phase def toNat : Phase → Nat | .base => 0 -| .untyped => 1 -| .rc => 2 +| .mono => 1 +| .impure => 2 instance : LT Phase where lt l r := l.toNat < r.toNat @@ -89,8 +89,8 @@ instance {p1 p2 : Phase} : Decidable (p1 ≤ p2) := Nat.decLe p1.toNat p2.toNat instance : ToString Phase where toString | .base => "base" - | .untyped => "untyped" - | .rc => "rc" + | .mono => "mono" + | .impure => "impure" end Phase diff --git a/src/Lean/Compiler/LCNF/Testing.lean b/src/Lean/Compiler/LCNF/Testing.lean index 90dc18e2f6..9b1bec490c 100644 --- a/src/Lean/Compiler/LCNF/Testing.lean +++ b/src/Lean/Compiler/LCNF/Testing.lean @@ -28,50 +28,144 @@ where namespace Testing +structure TestInstallerContext where + passUnderTestName : Name + testName : Name + +structure TestContext where + passUnderTest : Pass + testName : Name + +structure SimpleAssertionContext where + decls : Array Decl + +structure InOutAssertionContext where + input : Array Decl + output : Array Decl + +abbrev TestInstallerM := ReaderM TestInstallerContext +abbrev TestInstaller := TestInstallerM PassInstaller + +abbrev TestM := ReaderT TestContext CompilerM +abbrev SimpleAssertionM := ReaderT SimpleAssertionContext TestM +abbrev InOutAssertionM := ReaderT InOutAssertionContext TestM +abbrev SimpleTest := SimpleAssertionM Unit +abbrev InOutTest := InOutAssertionM Unit + +def TestInstaller.install (x : TestInstaller) (passUnderTestName testName : Name) : PassInstaller := + x { passUnderTestName, testName } + +def TestM.run (x : TestM α) (passUnderTest : Pass) (testName : Name) : CompilerM α := + x { passUnderTest, testName } + +def SimpleAssertionM.run (x : SimpleAssertionM α) (decls : Array Decl) (passUnderTest : Pass) (testName : Name) : CompilerM α := + x { decls } { passUnderTest, testName } + +def InOutAssertionM.run (x : InOutAssertionM α) (input output : Array Decl) (passUnderTest : Pass) (testName : Name) : CompilerM α := + x { input, output } { passUnderTest, testName } + +def getTestName : TestM Name := do + return (←read).testName + +def getPassUnderTest : TestM Pass := do + return (←read).passUnderTest + +def getDecls : SimpleAssertionM (Array Decl) := do + return (←read).decls + +def getInputDecls : InOutAssertionM (Array Decl) := do + return (←read).input + +def getOutputDecls : InOutAssertionM (Array Decl) := do + return (←read).output + /-- If `property` is `false` throw an exception with `msg`. -/ -def assert (property : Bool) (msg : String) : CompilerM Unit := do +def assert (property : Bool) (msg : String) : TestM Unit := do unless property do throwError msg -/-- -Install an assertion pass right after a pass. --/ -def assertConditionAfter (passUnderTestName : Name) (testName : Name) (assertion : Array Decl → CompilerM Unit) : PassInstaller := - let assertion := { +private def assertAfterTest (test : SimpleTest) : TestInstallerM (Pass → Pass) := do + let testName := (←read).testName + return fun passUnderTest => { + phase := passUnderTest.phase name := testName run := fun decls => do - trace[Compiler.test] s!"Starting post condition test {testName} for {passUnderTestName}" - assertion decls - trace[Compiler.test] s!"Post condition test {testName} for {passUnderTestName} successful" + trace[Compiler.test] s!"Starting post condition test {testName} for {passUnderTest.name} occurence {passUnderTest.occurence}" + test.run decls passUnderTest testName + trace[Compiler.test] s!"Post condition test {testName} for {passUnderTest.name} occurence {passUnderTest.occurence} successful" return decls } - .installAfter passUnderTestName assertion - -def assertForEachDeclAfterM (passUnderTestName : Name) (testName : Name) (assertion : Decl → CompilerM Unit) : PassInstaller := - assertConditionAfter passUnderTestName testName (·.forM assertion) - -def assertForEachDeclAfter (passUnderTestName : Name) (testName : Name) (assertion : Decl → Bool) (msg : String) : PassInstaller := - assertConditionAfter passUnderTestName testName (Array.forM (fun decl => assert (assertion decl) msg)) /-- -Replace a pass with a wrapper one that allows the user to provide an assertion which -takes into account both the declarations that were sent to and produced by the pass -under test. +Install an assertion pass right after a specific occurence of a pass, +default is first. -/ -def assertConditionAround (passUnderTestName : Name) (testName : Name) (assertion : Array Decl → Array Decl → CompilerM Unit) : PassInstaller := - let assertion := fun passUnderTest => pure { - name := passUnderTestName +def assertAfter (test : SimpleTest) (occurence : Nat := 0): TestInstaller := do + let passUnderTestName := (←read).passUnderTestName + let assertion ← assertAfterTest test + return .installAfter passUnderTestName assertion occurence + +/-- +Install an assertion pass right after each occurence of a pass. +-/ +def assertAfterEachOccurence (test : SimpleTest) : TestInstaller := do + let passUnderTestName := (←read).passUnderTestName + let assertion ← assertAfterTest test + return .installAfterEach passUnderTestName assertion + +/-- +Install an assertion pass right after a specific occurence of a pass, +default is first. The assertion operates on a per declaration basis. +-/ +def assertForEachDeclAfter (assertion : Pass → Decl → Bool) (msg : String) (occurence : Nat := 0) : TestInstaller := + let assertion := do + let pass ← getPassUnderTest + (←getDecls).forM (fun decl => assert (assertion pass decl) msg) + assertAfter assertion occurence + +/-- +Install an assertion pass right after the each occurence of a pass. The +assertion operates on a per declaration basis. +-/ +def assertForEachDeclAfterEachOccurence (assertion : Pass → Decl → Bool) (msg : String) : TestInstaller := + assertAfterEachOccurence <| do + let pass ← getPassUnderTest + (←getDecls).forM (fun decl => assert (assertion pass decl) msg) + +private def assertAroundTest (test : InOutTest) : TestInstallerM (Pass → Pass) := do + let testName := (←read).testName + return fun passUnderTest => { + phase := passUnderTest.phase + name := passUnderTest.name run := fun decls => do - trace[Compiler.test] s!"Starting condition test {testName} for {passUnderTestName}" + trace[Compiler.test] s!"Starting wrapper test {testName} for {passUnderTest.name} occurence {passUnderTest.occurence}" let newDecls ← passUnderTest.run decls - assertion decls newDecls - trace[Compiler.test] s!"Condition test {testName} for {passUnderTestName} successful" + test.run decls newDecls passUnderTest testName + trace[Compiler.test] s!"Wrapper test {testName} for {passUnderTest.name} occurence {passUnderTest.occurence} successful" return newDecls } - .replacePass passUnderTestName assertion +/-- +Replace a specific occurence, default is first, of a pass with a wrapper one that allows +the user to provide an assertion which takes into account both the +declarations that were sent to and produced by the pass under test. +-/ +def assertAround (test : InOutTest) (occurence : Nat := 0) : TestInstaller := do + let passUnderTestName := (←read).passUnderTestName + let assertion ← assertAroundTest test + return .replacePass passUnderTestName assertion occurence + +/-- +Replace all occurences of a pass with a wrapper one that allows +the user to provide an assertion which takes into account both the +declarations that were sent to and produced by the pass under test. +-/ +def assertAroundEachOccurence (test : InOutTest) : TestInstaller := do + let passUnderTestName := (←read).passUnderTestName + let assertion ← assertAroundTest test + return .replaceEachOccurence passUnderTestName assertion private def throwFixPointError (err : String) (firstResult secondResult : Array Decl) : CompilerM Unit := do let mut err := err @@ -87,65 +181,57 @@ Insert a pass after `passUnderTestName`, that ensures, that if `passUnderTestName` is executed twice in a row, no change in the resulting expression will occur, i.e. the pass is at a fix point. -/ -def assertIsAtFixPoint (passUnderTestName : Name) : PassInstaller where - install passes := do - let some idx := passes.findIdx? (·.name == passUnderTestName) | throwError s!"{passUnderTestName} not found in pass list" - let passUnderTest := passes[idx]! - let assertion : Pass := { - name := passUnderTestName.append `isFixPoint - run := fun decls => do - trace[Compiler.test] s!"Running fixpoint test for {passUnderTestName}" - let secondResult ← passUnderTest.run decls - if decls.size < secondResult.size then - let err := s!"Pass {passUnderTestName} did not reach a fixpoint, it added declarations on further runs:\n" - throwFixPointError err decls secondResult - else if decls.size > secondResult.size then - let err := s!"Pass {passUnderTestName} did not reach a fixpoint, it removed declarations on further runs:\n" - throwFixPointError err decls secondResult - else if decls != secondResult then - let err := s!"Pass {passUnderTestName} did not reach a fixpoint, it either changed declarations or their order:\n" - throwFixPointError err decls secondResult - trace[Compiler.test] s!"Fixpoint test for {passUnderTestName} successful" - return decls - } - return passes.insertAt (idx + 1) assertion - -/-- -Compare the overall sizes of the input and output of `passUnderTest` with `assertion`. --/ -def assertSizeM (passUnderTestName : Name) (testName : Name) (assertion : Nat → Nat → CompilerM Unit) : PassInstaller := - let sumDeclSizes := fun decls => decls.map Decl.size |>.foldl (init := 0) (· + ·) - assertConditionAround passUnderTestName testName (fun inp out => assertion (sumDeclSizes inp) (sumDeclSizes out)) +def assertIsAtFixPoint : TestInstaller := + let test := do + let passUnderTest ← getPassUnderTest + let decls ← getDecls + let secondResult ← passUnderTest.run decls + if decls.size < secondResult.size then + let err := s!"Pass {passUnderTest.name} did not reach a fixpoint, it added declarations on further runs:\n" + throwFixPointError err decls secondResult + else if decls.size > secondResult.size then + let err := s!"Pass {passUnderTest.name} did not reach a fixpoint, it removed declarations on further runs:\n" + throwFixPointError err decls secondResult + else if decls != secondResult then + let err := s!"Pass {passUnderTest.name} did not reach a fixpoint, it either changed declarations or their order:\n" + throwFixPointError err decls secondResult + assertAfterEachOccurence test /-- Compare the overall sizes of the input and output of `passUnderTest` with `assertion`. If `assertion inputSize outputSize` is `false` throw an exception with `msg`. -/ -def assertSize (passUnderTestName : Name) (testName : Name) (assertion : Nat → Nat → Bool) (msg : String) : PassInstaller := - assertSizeM passUnderTestName testName (fun beforeS afterS => Testing.assert (assertion afterS beforeS) msg) +def assertSize (assertion : Nat → Nat → Bool) (msg : String) : TestInstaller := + let sumDeclSizes := fun decls => decls.map Decl.size |>.foldl (init := 0) (· + ·) + let assertion := (fun inputS outputS => Testing.assert (assertion inputS outputS) s!"{msg}: input size {inputS} output size {outputS}") + assertAroundEachOccurence (do assertion (sumDeclSizes (←getInputDecls)) (sumDeclSizes (←getOutputDecls))) /-- Assert that the overall size of the `Decl`s in the compilation pipeline does not change after `passUnderTestName`. -/ -def assertPreservesSize (passUnderTestName : Name) (testName : Name) (msg : String) : PassInstaller := - assertSize passUnderTestName testName (· == ·) msg +def assertPreservesSize (msg : String) : TestInstaller := + assertSize (· == ·) msg /-- Assert that the overall size of the `Decl`s in the compilation pipeline gets reduced by `passUnderTestName`. -/ -def assertReducesSize (passUnderTestName : Name) (testName : Name) (msg : String) : PassInstaller := - assertSize passUnderTestName testName (· < ·) msg +def assertReducesSize (msg : String) : TestInstaller := + assertSize (· > ·) msg /-- Assert that the overall size of the `Decl`s in the compilation pipeline gets reduced or stays unchanged by `passUnderTestName`. -/ -def assertReducesOrPreservesSize (passUnderTestName : Name) (testName : Name) (msg : String) : PassInstaller := - assertSize passUnderTestName testName (· ≤ ·) msg +def assertReducesOrPreservesSize (msg : String) : TestInstaller := + assertSize (· ≥ ·) msg -def assertDoesNotContainConstAfter (passUnderTestName : Name) (testName : Name) (constName : Name) (msg : String) : PassInstaller := - assertForEachDeclAfter passUnderTestName testName (fun decl => !decl.value.containsConst constName) msg +/-- +Assert that the pass under test produces `Decl`s that do not contain +`Expr.const constName` in their `Code.let` values anymore. +-/ +def assertDoesNotContainConstAfter (constName : Name) (msg : String) : TestInstaller := + assertForEachDeclAfterEachOccurence (fun _ decl => !decl.value.containsConst constName) msg end Testing end Lean.Compiler.LCNF diff --git a/tests/lean/CompilerCSE.lean b/tests/lean/CompilerCSE.lean index c582d90730..be616f278a 100644 --- a/tests/lean/CompilerCSE.lean +++ b/tests/lean/CompilerCSE.lean @@ -9,11 +9,11 @@ open Lean.Compiler.LCNF #eval Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo] @[cpass] -def cseFixTest : PassInstaller := Testing.assertIsAtFixPoint `cse +def cseFixTest : PassInstaller := Testing.assertIsAtFixPoint |>.install `cse `cseFix @[cpass] def cseSizeTest : PassInstaller := - Testing.assertReducesOrPreservesSize `cse `cseSizeLeq "CSE increased size of declaration" + Testing.assertReducesOrPreservesSize "CSE increased size of declaration" |>.install `cse `cseSizeLeq set_option trace.Compiler.test true in #eval Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo] diff --git a/tests/lean/CompilerCSE.lean.expected.out b/tests/lean/CompilerCSE.lean.expected.out index 12e0668f25..003e41d422 100644 --- a/tests/lean/CompilerCSE.lean.expected.out +++ b/tests/lean/CompilerCSE.lean.expected.out @@ -1,5 +1,5 @@ -[Compiler.test] Starting condition test cseSizeLeq for cse -[Compiler.test] Condition test cseSizeLeq for cse successful -[Compiler.test] Running fixpoint test for cse -[Compiler.test] Fixpoint test for cse successful +[Compiler.test] Starting wrapper test cseSizeLeq for cse occurence 0 +[Compiler.test] Wrapper test cseSizeLeq for cse occurence 0 successful +[Compiler.test] Starting post condition test cseFix for cse occurence 0 +[Compiler.test] Post condition test cseFix for cse occurence 0 successful diff --git a/tests/lean/CompilerFindJoinPoints.lean b/tests/lean/CompilerFindJoinPoints.lean index d5b035a54f..8b9ae51d77 100644 --- a/tests/lean/CompilerFindJoinPoints.lean +++ b/tests/lean/CompilerFindJoinPoints.lean @@ -8,11 +8,11 @@ open Lean.Compiler.LCNF #eval Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo, ``Lean.MetavarContext.MkBinding.collectForwardDeps] @[cpass] -def findJoinPointFixTest : PassInstaller := Testing.assertIsAtFixPoint `findJoinPoints +def findJoinPointFixTest : PassInstaller := Testing.assertIsAtFixPoint |>.install `findJoinPoints `findJoinPointsFix @[cpass] def cseSizeTest : PassInstaller := - Testing.assertReducesOrPreservesSize `findJoinPoints `findJoinPointsSizeLeq "findJoinPoints increased size of declaration" + Testing.assertReducesOrPreservesSize "findJoinPoints increased size of declaration" |>.install `findJoinPoints `findJoinPointsSizeLeq set_option trace.Compiler.test true in #eval Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo, ``Lean.MetavarContext.MkBinding.collectForwardDeps] diff --git a/tests/lean/CompilerFindJoinPoints.lean.expected.out b/tests/lean/CompilerFindJoinPoints.lean.expected.out index 1644479746..9b58e211af 100644 --- a/tests/lean/CompilerFindJoinPoints.lean.expected.out +++ b/tests/lean/CompilerFindJoinPoints.lean.expected.out @@ -1,5 +1,4 @@ - -[Compiler.test] Starting condition test findJoinPointsSizeLeq for findJoinPoints -[Compiler.test] Condition test findJoinPointsSizeLeq for findJoinPoints successful -[Compiler.test] Running fixpoint test for findJoinPoints -[Compiler.test] Fixpoint test for findJoinPoints successful +[Compiler.test] Starting wrapper test findJoinPointsSizeLeq for findJoinPoints occurence 0 +[Compiler.test] Wrapper test findJoinPointsSizeLeq for findJoinPoints occurence 0 successful +[Compiler.test] Starting post condition test findJoinPointsFix for findJoinPoints occurence 0 +[Compiler.test] Post condition test findJoinPointsFix for findJoinPoints occurence 0 successful diff --git a/tests/lean/CompilerPullInstances.lean b/tests/lean/CompilerPullInstances.lean index 696057e772..2d419e91e9 100644 --- a/tests/lean/CompilerPullInstances.lean +++ b/tests/lean/CompilerPullInstances.lean @@ -9,11 +9,11 @@ open Lean.Compiler.LCNF #eval Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo] @[cpass] -def pullInstancesFixTest : PassInstaller := Testing.assertIsAtFixPoint `pullInstances +def pullInstancesFixTest : PassInstaller := Testing.assertIsAtFixPoint |>.install `pullInstances `pullInstancesFix @[cpass] def pullInstancesSizeTest : PassInstaller := - Testing.assertPreservesSize `pullInstances `pullInstancesSizeEq "Pulling instances changed size" + Testing.assertPreservesSize "Pulling instances changed size" |>.install `pullInstances `pullInstancesSizeEq set_option trace.Compiler.test true in #eval Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo] diff --git a/tests/lean/CompilerPullInstances.lean.expected.out b/tests/lean/CompilerPullInstances.lean.expected.out index 26194f245e..0ce3ec761e 100644 --- a/tests/lean/CompilerPullInstances.lean.expected.out +++ b/tests/lean/CompilerPullInstances.lean.expected.out @@ -1,5 +1,5 @@ -[Compiler.test] Starting condition test pullInstancesSizeEq for pullInstances -[Compiler.test] Condition test pullInstancesSizeEq for pullInstances successful -[Compiler.test] Running fixpoint test for pullInstances -[Compiler.test] Fixpoint test for pullInstances successful +[Compiler.test] Starting wrapper test pullInstancesSizeEq for pullInstances occurence 0 +[Compiler.test] Wrapper test pullInstancesSizeEq for pullInstances occurence 0 successful +[Compiler.test] Starting post condition test pullInstancesFix for pullInstances occurence 0 +[Compiler.test] Post condition test pullInstancesFix for pullInstances occurence 0 successful diff --git a/tests/lean/CompilerSimp.lean b/tests/lean/CompilerSimp.lean index 23f47201af..6288c2bb73 100644 --- a/tests/lean/CompilerSimp.lean +++ b/tests/lean/CompilerSimp.lean @@ -9,11 +9,11 @@ open Lean.Compiler.LCNF #eval Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo] @[cpass] -def simpFixTest : PassInstaller := Testing.assertIsAtFixPoint `simp +def simpFixTest : PassInstaller := Testing.assertIsAtFixPoint |>.install `simp `simpFix @[cpass] def simpReaderTest : PassInstaller := - Testing.assertDoesNotContainConstAfter `simp `simpInlinesBinds `ReaderT.bind "simp did not inline ReaderT.bind" + Testing.assertDoesNotContainConstAfter `ReaderT.bind "simp did not inline ReaderT.bind" |>.install `simp `simpInlinesBinds set_option trace.Compiler.test true in #eval Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo] diff --git a/tests/lean/CompilerSimp.lean.expected.out b/tests/lean/CompilerSimp.lean.expected.out index 7f4eb82474..bb09e89762 100644 --- a/tests/lean/CompilerSimp.lean.expected.out +++ b/tests/lean/CompilerSimp.lean.expected.out @@ -1,5 +1,9 @@ -[Compiler.test] Starting post condition test simpInlinesBinds for simp -[Compiler.test] Post condition test simpInlinesBinds for simp successful -[Compiler.test] Running fixpoint test for simp -[Compiler.test] Fixpoint test for simp successful +[Compiler.test] Starting post condition test simpInlinesBinds for simp occurence 0 +[Compiler.test] Post condition test simpInlinesBinds for simp occurence 0 successful +[Compiler.test] Starting post condition test simpFix for simp occurence 0 +[Compiler.test] Post condition test simpFix for simp occurence 0 successful +[Compiler.test] Starting post condition test simpInlinesBinds for simp occurence 1 +[Compiler.test] Post condition test simpInlinesBinds for simp occurence 1 successful +[Compiler.test] Starting post condition test simpFix for simp occurence 1 +[Compiler.test] Post condition test simpFix for simp occurence 1 successful