From 8235330fd8150b464213c0b55acf4b0a13d42728 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 4 Jan 2022 22:52:27 +0100
Subject: Improve check_typing_invariant to lookup borrowed/shared values and
 check they have the proper type

---
 src/Invariants.ml | 25 ++++++++++++++++++++-----
 1 file changed, 20 insertions(+), 5 deletions(-)

diff --git a/src/Invariants.ml b/src/Invariants.ml
index 457c00ad..b3fc4903 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -396,15 +396,30 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
             match (bc, rkind) with
             | V.SharedBorrow bid, T.Shared | V.InactivatedMutBorrow bid, T.Mut
-              ->
-                (* TODO: lookup the borrowed value to check it has the proper type *)
-                ()
-            | V.MutBorrow (_, bv), T.Mut -> assert (bv.V.ty = ref_ty)
+              -> (
+                (* Lookup the borrowed value to check it has the proper type *)
+                let _, glc = lookup_loan ek_all bid ctx in
+                match glc with
+                | Concrete (V.SharedLoan (_, sv))
+                | Abstract (V.ASharedLoan (_, sv, _)) ->
+                    assert (sv.V.ty = ref_ty)
+                | _ -> failwith "Inconsistent context")
+            | V.MutBorrow (bid, bv), T.Mut ->
+                assert (
+                  (* Check that the borrowed value has the proper type *)
+                  bv.V.ty = ref_ty)
             | _ -> failwith "Erroneous typing")
         | V.Loan lc, ty -> (
             match lc with
             | V.SharedLoan (_, sv) -> assert (sv.V.ty = ty)
-            | V.MutLoan _ -> ())
+            | V.MutLoan bid -> (
+                (* Lookup the borrowed value to check it has the proper type *)
+                let glc = lookup_borrow ek_all bid ctx in
+                match glc with
+                | Concrete (V.MutBorrow (_, bv)) -> assert (bv.V.ty = ty)
+                | Abstract (V.AMutBorrow (_, sv)) ->
+                    assert (Subst.erase_regions sv.V.ty = ty)
+                | _ -> failwith "Inconsistent context"))
         | V.Symbolic spc, ty ->
             let ty' = Subst.erase_regions spc.V.svalue.V.sv_ty in
             assert (ty' = ty)
-- 
cgit v1.2.3