refactor: monadic compiler test framework style + new pass manager

This commit is contained in:
Henrik Böving 2022-09-10 14:06:38 +02:00 committed by Leonardo de Moura
parent c6db1099d0
commit a03ea65d73
10 changed files with 187 additions and 98 deletions

View file

@ -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

View file

@ -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

View file

@ -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]

View file

@ -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

View file

@ -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]

View file

@ -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

View file

@ -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]

View file

@ -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

View file

@ -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]

View file

@ -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