Fix some bugs

7 files changed, 42 insertions, 15 deletions

diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index ccc259f5..6e09c90c 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -128,7 +128,8 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
         assert (Option.is_none !abs_or_var);
         if ek.enter_abs then (
           abs_or_var := Some (AbsId abs.V.abs_id);
-          super#visit_Abs env abs)
+          super#visit_Abs env abs;
+          abs_or_var := None)
         else ()
     end
   in
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 105adb5a..dfc821de 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -275,6 +275,8 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t)
         in
         (V.AAdt { V.variant_id; field_values }, original_sv_ty)
     | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) ->
+        (* Sanity check *)
+        assert (spc.V.svalue.V.sv_ty = ref_ty);
         (* Apply the projector to the borrowed value *)
         let child_av = mk_aproj_loans_from_proj_comp spc in
         (* Check if the region is in the set of projected regions (note that
@@ -286,6 +288,8 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t)
           (* Not in the set: ignore *)
           (V.ALoan (V.AIgnoredMutLoan (bid, child_av)), ref_ty)
     | SeSharedRef (bids, spc), T.Ref (r, ref_ty, T.Shared) ->
+        (* Sanity check *)
+        assert (spc.V.svalue.V.sv_ty = ref_ty);
         (* Apply the projector to the borrowed value *)
         let child_av = mk_aproj_loans_from_proj_comp spc in
         (* Check if the region is in the set of projected regions (note that
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index f0e3d420..458c11b4 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -21,6 +21,8 @@ let rty_to_string = Print.EvalCtxCfimAst.rty_to_string
 
 let typed_value_to_string = Print.EvalCtxCfimAst.typed_value_to_string
 
+let typed_avalue_to_string = Print.EvalCtxCfimAst.typed_avalue_to_string
+
 let place_to_string = Print.EvalCtxCfimAst.place_to_string
 
 let operand_to_string = Print.EvalCtxCfimAst.operand_to_string
diff --git a/src/Invariants.ml b/src/Invariants.ml
index be3260be..b723d861 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -8,6 +8,7 @@ module C = Contexts
 module Subst = Substitute
 module A = CfimAst
 module L = Logging
+open TypesUtils
 open InterpreterUtils
 open InterpreterBorrowsCore
 
@@ -341,6 +342,18 @@ let check_constant_value_type (cv : V.constant_value) (ty : T.ety) : unit =
   | _ -> failwith "Erroneous typing"
 
 let check_typing_invariant (ctx : C.eval_ctx) : unit =
+  (* TODO: the type of aloans doens't make sense: they have a type
+   * of the shape `& (mut) T` where they should have type `T`...
+   * This messes a bit the type invariant checks when checking the
+   * children. In order to isolate the problem (for future modifications)
+   * we introduce function, so that we can easily spot all the involved
+   * places.
+   * *)
+  let aloan_get_expected_child_type (ty : 'r T.ty) : 'r T.ty =
+    let _, ty, _ = ty_get_ref ty in
+    ty
+  in
+
   let visitor =
     object
       inherit [_] C.iter_eval_ctx as super
@@ -496,31 +509,30 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
             match lc with
             | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (bid, child_av)
               -> (
-                L.log#ldebug
-                  (lazy
-                    ("- child_av.ty: "
-                    ^ rty_to_string ctx child_av.V.ty
-                    ^ "\n- aty: " ^ rty_to_string ctx aty));
-                assert (child_av.V.ty = aty);
+                let borrowed_aty = aloan_get_expected_child_type aty in
+                assert (child_av.V.ty = borrowed_aty);
                 (* 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 = Subst.erase_regions aty)
+                    assert (bv.V.ty = Subst.erase_regions borrowed_aty)
                 | Abstract (V.AMutBorrow (_, sv)) ->
                     assert (
-                      Subst.erase_regions sv.V.ty = Subst.erase_regions aty)
+                      Subst.erase_regions sv.V.ty
+                      = Subst.erase_regions borrowed_aty)
                 | _ -> failwith "Inconsistent context")
             | V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av)
               ->
                 let ty = Subst.erase_regions aty in
                 assert (sv.V.ty = ty);
-                assert (child_av.V.ty = aty)
+                (* TODO: the type of aloans doesn't make sense, see above *)
+                assert (child_av.V.ty = aloan_get_expected_child_type aty)
             | V.AEndedMutLoan { given_back; child }
             | V.AEndedIgnoredMutLoan { given_back; child } ->
-                assert (given_back.V.ty = aty);
-                assert (child.V.ty = aty)
-            | V.AIgnoredSharedLoan child_av -> assert (child_av.V.ty = aty))
+                assert (given_back.V.ty = aloan_get_expected_child_type aty);
+                assert (child.V.ty = aloan_get_expected_child_type aty)
+            | V.AIgnoredSharedLoan child_av ->
+                assert (child_av.V.ty = aloan_get_expected_child_type aty))
         | V.ASymbolic aproj, ty ->
             let ty1 = Subst.erase_regions ty in
             let ty2 =
diff --git a/src/Print.ml b/src/Print.ml
index e751d0a3..0b436f1a 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -981,6 +981,10 @@ module EvalCtxCfimAst = struct
     let fmt = PC.eval_ctx_to_ctx_formatter ctx in
     PV.typed_value_to_string fmt v
 
+  let typed_avalue_to_string (ctx : C.eval_ctx) (v : V.typed_avalue) : string =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    PV.typed_avalue_to_string fmt v
+
   let place_to_string (ctx : C.eval_ctx) (op : E.place) : string =
     let fmt = PA.eval_ctx_to_ast_formatter ctx in
     PA.place_to_string fmt op
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index a658adce..04a579bf 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -32,7 +32,7 @@ let ty_get_box (box_ty : ety) : ety =
 (** Deconstruct a type of the form `&T` or `&mut T` to retrieve the `T` (and
     the borrow kind, etc.)
  *)
-let ty_get_ref (ty : ety) : erased_region * ety * ref_kind =
+let ty_get_ref (ty : 'r ty) : 'r * 'r ty * ref_kind =
   match ty with
   | Ref (r, ty, ref_kind) -> (r, ty, ref_kind)
   | _ -> failwith "Not a ref type"
diff --git a/src/Values.ml b/src/Values.ml
index ac4145eb..47bdda23 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -518,7 +518,11 @@ and aborrow_content =
        *)
 
 (* TODO: we may want to merge this with typed_value - would prevent some issues
-   when accessing fields... *)
+   when accessing fields....
+
+   TODO: the type of avalues doesn't make sense for loan avalues: they currently
+   are typed as `& (mut) T` instead of `T`...
+*)
 and typed_avalue = { value : avalue; ty : rty }
 [@@deriving
   show,