From 74fb8e627a9119ef015b773547ce2e0a5801dca7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 May 2019 05:47:25 -0700
Subject: [PATCH] feat(library/init/lean/compiler/ir/checker): improve IR
 checker

---
 library/init/lean/compiler/ir/basic.lean   |  7 +++-
 library/init/lean/compiler/ir/checker.lean | 41 +++++++++++++++++++---
 src/library/compiler/ir.cpp                |  8 ++++-
 3 files changed, 50 insertions(+), 6 deletions(-)

diff --git a/library/init/lean/compiler/ir/basic.lean b/library/init/lean/compiler/ir/basic.lean
index 8c9fb71503..20e17ee009 100644
--- a/library/init/lean/compiler/ir/basic.lean
+++ b/library/init/lean/compiler/ir/basic.lean
@@ -80,6 +80,8 @@ def IRType.beq : IRType → IRType → Bool
 | IRType.tobject    IRType.tobject    := true
 | _               _                   := false
 
+instance IRType.HasBeq : HasBeq IRType := ⟨IRType.beq⟩
+
 def IRType.isScalar : IRType → Bool
 | IRType.float  := true
 | IRType.uint8  := true
@@ -89,7 +91,10 @@ def IRType.isScalar : IRType → Bool
 | IRType.usize  := true
 | _             := false
 
-instance IRType.HasBeq : HasBeq IRType := ⟨IRType.beq⟩
+def IRType.isObj : IRType → Bool
+| IRType.object  := true
+| IRType.tobject := true
+| _              := false
 
 /- Arguments to applications, constructors, etc.
    We use `irrelevant` for Lean types, propositions and proofs that have been erased.
diff --git a/library/init/lean/compiler/ir/checker.lean b/library/init/lean/compiler/ir/checker.lean
index 338de825f4..945ce481c8 100644
--- a/library/init/lean/compiler/ir/checker.lean
+++ b/library/init/lean/compiler/ir/checker.lean
@@ -30,8 +30,41 @@ match a with
 def checkArgs (as : Array Arg) : M Unit :=
 as.mfor checkArg
 
-def checkExpr : Expr → M Unit
-| e := pure ()
+@[inline] def checkType (ty : IRType) (p : IRType → Bool) : M Unit :=
+unless (p ty) $ throw ("unexpected type")
+
+def checkObjType (ty : IRType) : M Unit := checkType ty IRType.isObj
+
+def checkScalarType (ty : IRType) : M Unit := checkType ty IRType.isScalar
+
+@[inline] def checkVarType (x : VarId) (p : IRType → Bool) : M Unit :=
+do ctx ← read,
+   match ctx.getType x with
+   | some ty := checkType ty p
+   | none    := throw ("unknown variable '" ++ toString x ++ "'")
+
+def checkObjVar (x : VarId) : M Unit :=
+checkVarType x IRType.isObj
+
+def checkScalarVar (x : VarId) : M Unit :=
+checkVarType x IRType.isScalar
+
+def checkExpr (ty : IRType) : Expr → M Unit
+| (Expr.pap _ ys)           := checkObjType ty *> checkArgs ys -- partial applications should always produce a closure object
+| (Expr.ap x ys)            := checkObjVar x *> checkArgs ys
+| (Expr.fap c ys)           := checkArgs ys
+| (Expr.ctor c ys)          := when (!c.isScalar) (checkObjType ty) *> checkArgs ys
+| (Expr.reset x)            := checkObjVar x *> checkObjType ty
+| (Expr.reuse x i u ys)     := checkObjVar x *> checkArgs ys *> checkObjType ty
+| (Expr.box xty x)          := checkObjType ty *> checkScalarVar x *> checkVarType x (==xty)
+| (Expr.unbox x)            := checkScalarType ty *> checkObjVar x
+| (Expr.proj _ x)           := checkObjVar x *> checkObjType ty
+| (Expr.uproj _ x)          := checkObjVar x *> checkType ty (==IRType.usize)
+| (Expr.sproj _ _ x)        := checkObjVar x *> checkScalarType ty
+| (Expr.isShared x)         := checkObjVar x *> checkType ty (==IRType.uint8)
+| (Expr.isTaggedPtr x)      := checkObjVar x *> checkType ty (==IRType.uint8)
+| (Expr.lit (LitVal.str _)) := checkObjType ty
+| (Expr.lit _)              := pure ()
 
 @[inline] def withParams (ps : Array Param) (k : M Unit) : M Unit :=
 do ctx ← read,
@@ -44,7 +77,7 @@ local attribute [instance] monadInhabited
 
 partial def checkFnBody : FnBody → M Unit
 | (FnBody.vdecl x t v b)    := do
-  checkExpr v,
+  checkExpr t v,
   ctx ← read,
   when (ctx.contains x.idx) $ throw ("invalid variable declaration, shadowing is not allowed"),
   adaptReader (λ ctx : Context, ctx.addLocal x t v) (checkFnBody b)
@@ -73,7 +106,7 @@ end Checker
 
 def Decl.check (d : Decl) : IO Unit :=
 match Checker.checkDecl d {} with
-| Except.error msg := throw (IO.userError ("IR check failed at '" ++ toString d.id ++ "'"))
+| Except.error msg := throw (IO.userError ("IR check failed at '" ++ toString d.id ++ "', error: " ++ msg))
 | other := pure ()
 
 end IR
diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp
index 560285a27d..e8f3bd1bd4 100644
--- a/src/library/compiler/ir.cpp
+++ b/src/library/compiler/ir.cpp
@@ -118,7 +118,13 @@ std::string decl_to_string(decl const & d) {
 void test(decl const & d) {
     inc(d.raw());
     object * r = test_core(d.raw(), io_mk_world());
-    dec(r);
+    if (io_result_is_error(r)) {
+        io_result_show_error(r);
+        dec(r);
+        throw exception("IR test error");
+    } else {
+        dec(r);
+    }
 }
 }