From a64fdc8b1be70de43afe35ff788ba3240318daac Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Tue, 12 Mar 2024 15:02:17 +0100
Subject: WIP Beginning working on better errors: began replacing raise
 (Failure) and assert by craise and cassert. Does not compile yet, still need
 to propagate the meta variable where it's relevant

---
 compiler/InterpreterProjectors.ml | 91 ++++++++++++++++++++-------------------
 1 file changed, 46 insertions(+), 45 deletions(-)

(limited to 'compiler/InterpreterProjectors.ml')

diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 4dc53586..d4a237b2 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -6,12 +6,13 @@ module Assoc = AssociatedTypes
 open TypesUtils
 open InterpreterUtils
 open InterpreterBorrowsCore
+open Errors
 
 (** The local logger *)
 let log = Logging.projectors_log
 
 (** [ty] shouldn't contain erased regions *)
-let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx)
+let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
     (fresh_reborrow : BorrowId.id -> BorrowId.id) (regions : RegionId.Set.t)
     (v : typed_value) (ty : rty) : abstract_shared_borrows =
   (* Sanity check - TODO: move those elsewhere (here we perform the check at every
@@ -34,12 +35,12 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx)
         let proj_fields =
           List.map
             (fun (fv, fty) ->
-              apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions fv
+              apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow regions fv
                 fty)
             fields_types
         in
         List.concat proj_fields
-    | VBottom, _ -> raise (Failure "Unreachable")
+    | VBottom, _ -> craise meta "Unreachable"
     | VBorrow bc, TRef (r, ref_ty, kind) ->
         (* Retrieve the bid of the borrow and the asb of the projected borrowed value *)
         let bid, asb =
@@ -48,28 +49,28 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx)
           | VMutBorrow (bid, bv), RMut ->
               (* Apply the projection on the borrowed value *)
               let asb =
-                apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions
+                apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow regions
                   bv ref_ty
               in
               (bid, asb)
           | VSharedBorrow bid, RShared ->
               (* Lookup the shared value *)
               let ek = ek_all in
-              let sv = lookup_loan ek bid ctx in
+              let sv = lookup_loan meta ek bid ctx in
               let asb =
                 match sv with
                 | _, Concrete (VSharedLoan (_, sv))
                 | _, Abstract (ASharedLoan (_, sv, _)) ->
-                    apply_proj_borrows_on_shared_borrow ctx fresh_reborrow
+                    apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow
                       regions sv ref_ty
-                | _ -> raise (Failure "Unexpected")
+                | _ -> craise meta "Unexpected"
               in
               (bid, asb)
           | VReservedMutBorrow _, _ ->
-              raise
-                (Failure
-                   "Can't apply a proj_borrow over a reserved mutable borrow")
-          | _ -> raise (Failure "Unreachable")
+              craise
+                meta
+                   "Can't apply a proj_borrow over a reserved mutable borrow"
+          | _ -> craise meta "Unreachable"
         in
         let asb =
           (* Check if the region is in the set of projected regions (note that
@@ -80,14 +81,14 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx)
           else asb
         in
         asb
-    | VLoan _, _ -> raise (Failure "Unreachable")
+    | VLoan _, _ -> craise meta "Unreachable"
     | VSymbolic s, _ ->
         (* Check that the projection doesn't contain ended regions *)
-        assert (not (projections_intersect s.sv_ty ctx.ended_regions ty regions));
+        assert (not (projections_intersect meta s.sv_ty ctx.ended_regions ty regions));
         [ AsbProjReborrows (s, ty) ]
-    | _ -> raise (Failure "Unreachable")
+    | _ -> craise meta "Unreachable"
 
-let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
+let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (ctx : eval_ctx)
     (fresh_reborrow : BorrowId.id -> BorrowId.id) (regions : RegionId.Set.t)
     (ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) :
     typed_avalue =
@@ -111,12 +112,12 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
           let proj_fields =
             List.map
               (fun (fv, fty) ->
-                apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
+                apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow
                   regions ancestors_regions fv fty)
               fields_types
           in
           AAdt { variant_id = adt.variant_id; field_values = proj_fields }
-      | VBottom, _ -> raise (Failure "Unreachable")
+      | VBottom, _ -> craise meta "Unreachable"
       | VBorrow bc, TRef (r, ref_ty, kind) ->
           if
             (* Check if the region is in the set of projected regions (note that
@@ -129,7 +130,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
               | VMutBorrow (bid, bv), RMut ->
                   (* Apply the projection on the borrowed value *)
                   let bv =
-                    apply_proj_borrows check_symbolic_no_ended ctx
+                    apply_proj_borrows meta check_symbolic_no_ended ctx
                       fresh_reborrow regions ancestors_regions bv ref_ty
                   in
                   AMutBorrow (bid, bv)
@@ -147,11 +148,11 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
                   *)
                   ASharedBorrow bid
               | VReservedMutBorrow _, _ ->
-                  raise
-                    (Failure
+                  craise
+                    meta
                        "Can't apply a proj_borrow over a reserved mutable \
-                        borrow")
-              | _ -> raise (Failure "Unreachable")
+                        borrow"
+              | _ -> craise meta "Unreachable"
             in
             ABorrow bc
           else
@@ -163,7 +164,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
               | VMutBorrow (bid, bv), RMut ->
                   (* Apply the projection on the borrowed value *)
                   let bv =
-                    apply_proj_borrows check_symbolic_no_ended ctx
+                    apply_proj_borrows meta check_symbolic_no_ended ctx
                       fresh_reborrow regions ancestors_regions bv ref_ty
                   in
                   (* If the borrow id is in the ancestor's regions, we still need
@@ -176,25 +177,25 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
               | VSharedBorrow bid, RShared ->
                   (* Lookup the shared value *)
                   let ek = ek_all in
-                  let sv = lookup_loan ek bid ctx in
+                  let sv = lookup_loan meta ek bid ctx in
                   let asb =
                     match sv with
                     | _, Concrete (VSharedLoan (_, sv))
                     | _, Abstract (ASharedLoan (_, sv, _)) ->
-                        apply_proj_borrows_on_shared_borrow ctx fresh_reborrow
+                        apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow
                           regions sv ref_ty
-                    | _ -> raise (Failure "Unexpected")
+                    | _ -> craise meta "Unexpected"
                   in
                   AProjSharedBorrow asb
               | VReservedMutBorrow _, _ ->
-                  raise
-                    (Failure
+                  craise
+                    meta
                        "Can't apply a proj_borrow over a reserved mutable \
-                        borrow")
-              | _ -> raise (Failure "Unreachable")
+                        borrow"
+              | _ -> craise meta "Unreachable"
             in
             ABorrow bc
-      | VLoan _, _ -> raise (Failure "Unreachable")
+      | VLoan _, _ -> craise meta "Unreachable"
       | VSymbolic s, _ ->
           (* Check that the projection doesn't contain already ended regions,
            * if necessary *)
@@ -211,7 +212,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
                 ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
                 ^ RegionId.Set.to_string None rset2
                 ^ "\n"));
-            assert (not (projections_intersect ty1 rset1 ty2 rset2)));
+            assert (not (projections_intersect meta ty1 rset1 ty2 rset2)));
           ASymbolic (AProjBorrows (s, ty))
       | _ ->
           log#lerror
@@ -219,11 +220,11 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
               ("apply_proj_borrows: unexpected inputs:\n- input value: "
               ^ typed_value_to_string ctx v
               ^ "\n- proj rty: " ^ ty_to_string ctx ty));
-          raise (Failure "Unreachable")
+          craise meta "Unreachable"
     in
     { value; ty }
 
-let symbolic_expansion_non_borrow_to_value (sv : symbolic_value)
+let symbolic_expansion_non_borrow_to_value (meta : Meta.meta) (sv : symbolic_value)
     (see : symbolic_expansion) : typed_value =
   let ty = Subst.erase_regions sv.sv_ty in
   let value =
@@ -235,11 +236,11 @@ let symbolic_expansion_non_borrow_to_value (sv : symbolic_value)
         in
         VAdt { variant_id; field_values }
     | SeMutRef (_, _) | SeSharedRef (_, _) ->
-        raise (Failure "Unexpected symbolic reference expansion")
+        craise meta "Unexpected symbolic reference expansion"
   in
   { value; ty }
 
-let symbolic_expansion_non_shared_borrow_to_value (sv : symbolic_value)
+let symbolic_expansion_non_shared_borrow_to_value (meta : Meta.meta) (sv : symbolic_value)
     (see : symbolic_expansion) : typed_value =
   match see with
   | SeMutRef (bid, bv) ->
@@ -248,14 +249,14 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : symbolic_value)
       let value = VBorrow (VMutBorrow (bid, bv)) in
       { value; ty }
   | SeSharedRef (_, _) ->
-      raise (Failure "Unexpected symbolic shared reference expansion")
-  | _ -> symbolic_expansion_non_borrow_to_value sv see
+      craise meta "Unexpected symbolic shared reference expansion"
+  | _ -> symbolic_expansion_non_borrow_to_value meta sv see
 
 (** Apply (and reduce) a projector over loans to a value.
 
     TODO: detailed comments. See [apply_proj_borrows]
 *)
-let apply_proj_loans_on_symbolic_expansion (regions : RegionId.Set.t)
+let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionId.Set.t)
     (ancestors_regions : RegionId.Set.t) (see : symbolic_expansion)
     (original_sv_ty : rty) : typed_avalue =
   (* Sanity check: if we have a proj_loans over a symbolic value, it should
@@ -305,7 +306,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : RegionId.Set.t)
         else
           (* Not in the set: ignore *)
           (ALoan (AIgnoredSharedLoan child_av), ref_ty)
-    | _ -> raise (Failure "Unreachable")
+    | _ -> craise meta "Unreachable"
   in
   { value; ty }
 
@@ -467,7 +468,7 @@ let apply_reborrows (reborrows : (BorrowId.id * BorrowId.id) list)
   (* Return *)
   ctx
 
-let prepare_reborrows (config : config) (allow_reborrows : bool) :
+let prepare_reborrows (meta : Meta.meta) (config : config) (allow_reborrows : bool) :
     (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx) =
   let reborrows : (BorrowId.id * BorrowId.id) list ref = ref [] in
   (* The function to generate and register fresh reborrows *)
@@ -476,7 +477,7 @@ let prepare_reborrows (config : config) (allow_reborrows : bool) :
       let bid' = fresh_borrow_id () in
       reborrows := (bid, bid') :: !reborrows;
       bid')
-    else raise (Failure "Unexpected reborrow")
+    else craise meta "Unexpected reborrow"
   in
   (* The function to apply the reborrows in a context *)
   let apply_registered_reborrows (ctx : eval_ctx) : eval_ctx =
@@ -491,7 +492,7 @@ let prepare_reborrows (config : config) (allow_reborrows : bool) :
   (fresh_reborrow, apply_registered_reborrows)
 
 (** [ty] shouldn't have erased regions *)
-let apply_proj_borrows_on_input_value (config : config) (ctx : eval_ctx)
+let apply_proj_borrows_on_input_value (meta : Meta.meta) (config : config) (ctx : eval_ctx)
     (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t)
     (v : typed_value) (ty : rty) : eval_ctx * typed_avalue =
   assert (ty_is_rty ty);
@@ -499,11 +500,11 @@ let apply_proj_borrows_on_input_value (config : config) (ctx : eval_ctx)
   let allow_reborrows = true in
   (* Prepare the reborrows *)
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows config allow_reborrows
+    prepare_reborrows meta config allow_reborrows
   in
   (* Apply the projector *)
   let av =
-    apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions
+    apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow regions
       ancestors_regions v ty
   in
   (* Apply the reborrows *)
-- 
cgit v1.2.3


From 5209cea7012cfa3b39a5a289e65e2ea5e166d730 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 21 Mar 2024 12:34:40 +0100
Subject: WIP: translate.ml and extract.ml do not compile. Some assert left to
 do and we need to see how translate_crate can give meta to the functions it
 calls

---
 compiler/InterpreterProjectors.ml | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

(limited to 'compiler/InterpreterProjectors.ml')

diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index d4a237b2..fff23aec 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -18,7 +18,7 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
   (* Sanity check - TODO: move those elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
   let ety = Subst.erase_regions ty in
-  assert (ty_is_rty ty && ety = v.ty);
+  cassert (ty_is_rty ty && ety = v.ty) meta "TODO: error message";
   (* Project - if there are no regions from the abstraction in the type, return [_] *)
   if not (ty_has_regions_in_set regions ty) then []
   else
@@ -27,7 +27,7 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
     | VAdt adt, TAdt (id, generics) ->
         (* Retrieve the types of the fields *)
         let field_types =
-          Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics
+          Assoc.ctx_adt_value_get_inst_norm_field_rtypes meta ctx adt id generics
         in
 
         (* Project over the field values *)
@@ -84,7 +84,7 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
     | VLoan _, _ -> craise meta "Unreachable"
     | VSymbolic s, _ ->
         (* Check that the projection doesn't contain ended regions *)
-        assert (not (projections_intersect meta s.sv_ty ctx.ended_regions ty regions));
+        cassert (not (projections_intersect meta s.sv_ty ctx.ended_regions ty regions)) meta "TODO: error message";
         [ AsbProjReborrows (s, ty) ]
     | _ -> craise meta "Unreachable"
 
@@ -95,7 +95,7 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (
   (* Sanity check - TODO: move this elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
   let ety = Substitute.erase_regions ty in
-  assert (ty_is_rty ty && ety = v.ty);
+  cassert (ty_is_rty ty && ety = v.ty) meta "TODO: error message";
   (* Project - if there are no regions from the abstraction in the type, return [_] *)
   if not (ty_has_regions_in_set regions ty) then { value = AIgnored; ty }
   else
@@ -105,7 +105,7 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (
       | VAdt adt, TAdt (id, generics) ->
           (* Retrieve the types of the fields *)
           let field_types =
-            Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics
+            Assoc.ctx_adt_value_get_inst_norm_field_rtypes meta ctx adt id generics
           in
           (* Project over the field values *)
           let fields_types = List.combine adt.field_values field_types in
@@ -212,13 +212,13 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (
                 ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
                 ^ RegionId.Set.to_string None rset2
                 ^ "\n"));
-            assert (not (projections_intersect meta ty1 rset1 ty2 rset2)));
+            cassert (not (projections_intersect meta ty1 rset1 ty2 rset2))) meta "TODO: error message";
           ASymbolic (AProjBorrows (s, ty))
       | _ ->
           log#lerror
             (lazy
               ("apply_proj_borrows: unexpected inputs:\n- input value: "
-              ^ typed_value_to_string ctx v
+              ^ typed_value_to_string meta ctx v
               ^ "\n- proj rty: " ^ ty_to_string ctx ty));
           craise meta "Unreachable"
     in
@@ -261,7 +261,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionI
     (original_sv_ty : rty) : typed_avalue =
   (* Sanity check: if we have a proj_loans over a symbolic value, it should
    * contain regions which we will project *)
-  assert (ty_has_regions_in_set regions original_sv_ty);
+  cassert (ty_has_regions_in_set regions original_sv_ty) meta "TODO: error message";
   (* Match *)
   let (value, ty) : avalue * ty =
     match (see, original_sv_ty) with
@@ -276,7 +276,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionI
         (AAdt { variant_id; field_values }, original_sv_ty)
     | SeMutRef (bid, spc), TRef (r, ref_ty, RMut) ->
         (* Sanity check *)
-        assert (spc.sv_ty = ref_ty);
+        cassert (spc.sv_ty = ref_ty) meta "TODO: error message";
         (* Apply the projector to the borrowed value *)
         let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in
         (* Check if the region is in the set of projected regions (note that
@@ -294,7 +294,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionI
           (ALoan (AIgnoredMutLoan (opt_bid, child_av)), ref_ty)
     | SeSharedRef (bids, spc), TRef (r, ref_ty, RShared) ->
         (* Sanity check *)
-        assert (spc.sv_ty = ref_ty);
+        cassert (spc.sv_ty = ref_ty) meta "TODO: error message";
         (* Apply the projector to the borrowed value *)
         let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in
         (* Check if the region is in the set of projected regions (note that
@@ -332,7 +332,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionI
     borrows - easy - and mutable borrows - in this case, we reborrow the whole
     borrow: [mut_borrow ... ~~> shared_loan {...} (mut_borrow ...)]).
 *)
-let apply_reborrows (reborrows : (BorrowId.id * BorrowId.id) list)
+let apply_reborrows (meta : Meta.meta) (reborrows : (BorrowId.id * BorrowId.id) list)
     (ctx : eval_ctx) : eval_ctx =
   (* This is a bit brutal, but whenever we insert a reborrow, we remove
    * it from the list. This allows us to check that all the reborrows were
@@ -464,7 +464,7 @@ let apply_reborrows (reborrows : (BorrowId.id * BorrowId.id) list)
   (* Visit *)
   let ctx = obj#visit_eval_ctx () ctx in
   (* Check that there are no reborrows remaining *)
-  assert (!reborrows = []);
+  cassert (!reborrows = []) meta "TODO: error message";
   (* Return *)
   ctx
 
@@ -483,11 +483,11 @@ let prepare_reborrows (meta : Meta.meta) (config : config) (allow_reborrows : bo
   let apply_registered_reborrows (ctx : eval_ctx) : eval_ctx =
     match config.mode with
     | ConcreteMode ->
-        assert (!reborrows = []);
+        cassert (!reborrows = []) meta "TODO: error message";
         ctx
     | SymbolicMode ->
         (* Apply the reborrows *)
-        apply_reborrows !reborrows ctx
+        apply_reborrows meta !reborrows ctx
   in
   (fresh_reborrow, apply_registered_reborrows)
 
@@ -495,7 +495,7 @@ let prepare_reborrows (meta : Meta.meta) (config : config) (allow_reborrows : bo
 let apply_proj_borrows_on_input_value (meta : Meta.meta) (config : config) (ctx : eval_ctx)
     (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t)
     (v : typed_value) (ty : rty) : eval_ctx * typed_avalue =
-  assert (ty_is_rty ty);
+  cassert (ty_is_rty ty) meta "TODO: error message";
   let check_symbolic_no_ended = true in
   let allow_reborrows = true in
   (* Prepare the reborrows *)
-- 
cgit v1.2.3


From d6ea35868e30bbc7542bfa09bb04d5b6cbe93b22 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Mon, 25 Mar 2024 12:06:05 +0100
Subject: Inverted meta and config argument orders (from meta -> config to
 config -> meta)

---
 compiler/InterpreterProjectors.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'compiler/InterpreterProjectors.ml')

diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index fff23aec..7eaa7659 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -468,7 +468,7 @@ let apply_reborrows (meta : Meta.meta) (reborrows : (BorrowId.id * BorrowId.id)
   (* Return *)
   ctx
 
-let prepare_reborrows (meta : Meta.meta) (config : config) (allow_reborrows : bool) :
+let prepare_reborrows (config : config) (meta : Meta.meta) (allow_reborrows : bool) :
     (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx) =
   let reborrows : (BorrowId.id * BorrowId.id) list ref = ref [] in
   (* The function to generate and register fresh reborrows *)
@@ -492,7 +492,7 @@ let prepare_reborrows (meta : Meta.meta) (config : config) (allow_reborrows : bo
   (fresh_reborrow, apply_registered_reborrows)
 
 (** [ty] shouldn't have erased regions *)
-let apply_proj_borrows_on_input_value (meta : Meta.meta) (config : config) (ctx : eval_ctx)
+let apply_proj_borrows_on_input_value (config : config) (meta : Meta.meta) (ctx : eval_ctx)
     (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t)
     (v : typed_value) (ty : rty) : eval_ctx * typed_avalue =
   cassert (ty_is_rty ty) meta "TODO: error message";
@@ -500,7 +500,7 @@ let apply_proj_borrows_on_input_value (meta : Meta.meta) (config : config) (ctx
   let allow_reborrows = true in
   (* Prepare the reborrows *)
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows meta config allow_reborrows
+    prepare_reborrows config meta allow_reborrows
   in
   (* Apply the projector *)
   let av =
-- 
cgit v1.2.3


From 0f0082c81db8852dff23cd4691af19c434c8be78 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 27 Mar 2024 10:22:06 +0100
Subject: Added sanity_check and sanity_check_opt_meta helpers and changed
 sanity checks related cassert to these helpers to have a proper error message

---
 compiler/InterpreterProjectors.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'compiler/InterpreterProjectors.ml')

diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 7eaa7659..5f83b938 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -18,7 +18,7 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
   (* Sanity check - TODO: move those elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
   let ety = Subst.erase_regions ty in
-  cassert (ty_is_rty ty && ety = v.ty) meta "TODO: error message";
+  sanity_check (ty_is_rty ty && ety = v.ty) meta;
   (* Project - if there are no regions from the abstraction in the type, return [_] *)
   if not (ty_has_regions_in_set regions ty) then []
   else
@@ -95,7 +95,7 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (
   (* Sanity check - TODO: move this elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
   let ety = Substitute.erase_regions ty in
-  cassert (ty_is_rty ty && ety = v.ty) meta "TODO: error message";
+  sanity_check (ty_is_rty ty && ety = v.ty) meta;
   (* Project - if there are no regions from the abstraction in the type, return [_] *)
   if not (ty_has_regions_in_set regions ty) then { value = AIgnored; ty }
   else
@@ -261,7 +261,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionI
     (original_sv_ty : rty) : typed_avalue =
   (* Sanity check: if we have a proj_loans over a symbolic value, it should
    * contain regions which we will project *)
-  cassert (ty_has_regions_in_set regions original_sv_ty) meta "TODO: error message";
+  sanity_check (ty_has_regions_in_set regions original_sv_ty) meta;
   (* Match *)
   let (value, ty) : avalue * ty =
     match (see, original_sv_ty) with
@@ -276,7 +276,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionI
         (AAdt { variant_id; field_values }, original_sv_ty)
     | SeMutRef (bid, spc), TRef (r, ref_ty, RMut) ->
         (* Sanity check *)
-        cassert (spc.sv_ty = ref_ty) meta "TODO: error message";
+        sanity_check (spc.sv_ty = ref_ty) meta;
         (* Apply the projector to the borrowed value *)
         let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in
         (* Check if the region is in the set of projected regions (note that
@@ -294,7 +294,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionI
           (ALoan (AIgnoredMutLoan (opt_bid, child_av)), ref_ty)
     | SeSharedRef (bids, spc), TRef (r, ref_ty, RShared) ->
         (* Sanity check *)
-        cassert (spc.sv_ty = ref_ty) meta "TODO: error message";
+        sanity_check (spc.sv_ty = ref_ty) meta;
         (* Apply the projector to the borrowed value *)
         let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in
         (* Check if the region is in the set of projected regions (note that
-- 
cgit v1.2.3


From 5ad671a0960692af1c00609fa6864c6f44ca299c Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 13:56:31 +0100
Subject: Should answer all comments, there are still some TODO: error message
 left

---
 compiler/InterpreterProjectors.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'compiler/InterpreterProjectors.ml')

diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 5f83b938..809303ae 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -84,7 +84,7 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
     | VLoan _, _ -> craise meta "Unreachable"
     | VSymbolic s, _ ->
         (* Check that the projection doesn't contain ended regions *)
-        cassert (not (projections_intersect meta s.sv_ty ctx.ended_regions ty regions)) meta "TODO: error message";
+        sanity_check (not (projections_intersect meta s.sv_ty ctx.ended_regions ty regions)) meta;
         [ AsbProjReborrows (s, ty) ]
     | _ -> craise meta "Unreachable"
 
@@ -212,13 +212,13 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (
                 ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
                 ^ RegionId.Set.to_string None rset2
                 ^ "\n"));
-            cassert (not (projections_intersect meta ty1 rset1 ty2 rset2))) meta "TODO: error message";
+            sanity_check (not (projections_intersect meta ty1 rset1 ty2 rset2))) meta;
           ASymbolic (AProjBorrows (s, ty))
       | _ ->
           log#lerror
             (lazy
               ("apply_proj_borrows: unexpected inputs:\n- input value: "
-              ^ typed_value_to_string meta ctx v
+              ^ typed_value_to_string ~meta:(Some meta) ctx v
               ^ "\n- proj rty: " ^ ty_to_string ctx ty));
           craise meta "Unreachable"
     in
@@ -464,7 +464,7 @@ let apply_reborrows (meta : Meta.meta) (reborrows : (BorrowId.id * BorrowId.id)
   (* Visit *)
   let ctx = obj#visit_eval_ctx () ctx in
   (* Check that there are no reborrows remaining *)
-  cassert (!reborrows = []) meta "TODO: error message";
+  sanity_check (!reborrows = []) meta;
   (* Return *)
   ctx
 
@@ -483,7 +483,7 @@ let prepare_reborrows (config : config) (meta : Meta.meta) (allow_reborrows : bo
   let apply_registered_reborrows (ctx : eval_ctx) : eval_ctx =
     match config.mode with
     | ConcreteMode ->
-        cassert (!reborrows = []) meta "TODO: error message";
+        sanity_check (!reborrows = []) meta;
         ctx
     | SymbolicMode ->
         (* Apply the reborrows *)
-- 
cgit v1.2.3


From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 17:14:27 +0100
Subject: formatting

---
 compiler/InterpreterProjectors.ml | 109 ++++++++++++++++++++------------------
 1 file changed, 56 insertions(+), 53 deletions(-)

(limited to 'compiler/InterpreterProjectors.ml')

diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 809303ae..f8f99584 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -27,7 +27,8 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
     | VAdt adt, TAdt (id, generics) ->
         (* Retrieve the types of the fields *)
         let field_types =
-          Assoc.ctx_adt_value_get_inst_norm_field_rtypes meta ctx adt id generics
+          Assoc.ctx_adt_value_get_inst_norm_field_rtypes meta ctx adt id
+            generics
         in
 
         (* Project over the field values *)
@@ -35,8 +36,8 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
         let proj_fields =
           List.map
             (fun (fv, fty) ->
-              apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow regions fv
-                fty)
+              apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow
+                regions fv fty)
             fields_types
         in
         List.concat proj_fields
@@ -49,8 +50,8 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
           | VMutBorrow (bid, bv), RMut ->
               (* Apply the projection on the borrowed value *)
               let asb =
-                apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow regions
-                  bv ref_ty
+                apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow
+                  regions bv ref_ty
               in
               (bid, asb)
           | VSharedBorrow bid, RShared ->
@@ -67,9 +68,8 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
               in
               (bid, asb)
           | VReservedMutBorrow _, _ ->
-              craise
-                meta
-                   "Can't apply a proj_borrow over a reserved mutable borrow"
+              craise meta
+                "Can't apply a proj_borrow over a reserved mutable borrow"
           | _ -> craise meta "Unreachable"
         in
         let asb =
@@ -84,14 +84,17 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
     | VLoan _, _ -> craise meta "Unreachable"
     | VSymbolic s, _ ->
         (* Check that the projection doesn't contain ended regions *)
-        sanity_check (not (projections_intersect meta s.sv_ty ctx.ended_regions ty regions)) meta;
+        sanity_check
+          (not
+             (projections_intersect meta s.sv_ty ctx.ended_regions ty regions))
+          meta;
         [ AsbProjReborrows (s, ty) ]
     | _ -> craise meta "Unreachable"
 
-let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (ctx : eval_ctx)
-    (fresh_reborrow : BorrowId.id -> BorrowId.id) (regions : RegionId.Set.t)
-    (ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) :
-    typed_avalue =
+let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
+    (ctx : eval_ctx) (fresh_reborrow : BorrowId.id -> BorrowId.id)
+    (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t)
+    (v : typed_value) (ty : rty) : typed_avalue =
   (* Sanity check - TODO: move this elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
   let ety = Substitute.erase_regions ty in
@@ -105,15 +108,16 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (
       | VAdt adt, TAdt (id, generics) ->
           (* Retrieve the types of the fields *)
           let field_types =
-            Assoc.ctx_adt_value_get_inst_norm_field_rtypes meta ctx adt id generics
+            Assoc.ctx_adt_value_get_inst_norm_field_rtypes meta ctx adt id
+              generics
           in
           (* Project over the field values *)
           let fields_types = List.combine adt.field_values field_types in
           let proj_fields =
             List.map
               (fun (fv, fty) ->
-                apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow
-                  regions ancestors_regions fv fty)
+                apply_proj_borrows meta check_symbolic_no_ended ctx
+                  fresh_reborrow regions ancestors_regions fv fty)
               fields_types
           in
           AAdt { variant_id = adt.variant_id; field_values = proj_fields }
@@ -148,10 +152,8 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (
                   *)
                   ASharedBorrow bid
               | VReservedMutBorrow _, _ ->
-                  craise
-                    meta
-                       "Can't apply a proj_borrow over a reserved mutable \
-                        borrow"
+                  craise meta
+                    "Can't apply a proj_borrow over a reserved mutable borrow"
               | _ -> craise meta "Unreachable"
             in
             ABorrow bc
@@ -182,16 +184,14 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (
                     match sv with
                     | _, Concrete (VSharedLoan (_, sv))
                     | _, Abstract (ASharedLoan (_, sv, _)) ->
-                        apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow
-                          regions sv ref_ty
+                        apply_proj_borrows_on_shared_borrow meta ctx
+                          fresh_reborrow regions sv ref_ty
                     | _ -> craise meta "Unexpected"
                   in
                   AProjSharedBorrow asb
               | VReservedMutBorrow _, _ ->
-                  craise
-                    meta
-                       "Can't apply a proj_borrow over a reserved mutable \
-                        borrow"
+                  craise meta
+                    "Can't apply a proj_borrow over a reserved mutable borrow"
               | _ -> craise meta "Unreachable"
             in
             ABorrow bc
@@ -199,20 +199,21 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (
       | VSymbolic s, _ ->
           (* Check that the projection doesn't contain already ended regions,
            * if necessary *)
-          if check_symbolic_no_ended then (
-            let ty1 = s.sv_ty in
-            let rset1 = ctx.ended_regions in
-            let ty2 = ty in
-            let rset2 = regions in
-            log#ldebug
-              (lazy
-                ("projections_intersect:" ^ "\n- ty1: " ^ ty_to_string ctx ty1
-               ^ "\n- rset1: "
-                ^ RegionId.Set.to_string None rset1
-                ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
-                ^ RegionId.Set.to_string None rset2
-                ^ "\n"));
-            sanity_check (not (projections_intersect meta ty1 rset1 ty2 rset2))) meta;
+          if check_symbolic_no_ended then
+            (let ty1 = s.sv_ty in
+             let rset1 = ctx.ended_regions in
+             let ty2 = ty in
+             let rset2 = regions in
+             log#ldebug
+               (lazy
+                 ("projections_intersect:" ^ "\n- ty1: " ^ ty_to_string ctx ty1
+                ^ "\n- rset1: "
+                 ^ RegionId.Set.to_string None rset1
+                 ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
+                 ^ RegionId.Set.to_string None rset2
+                 ^ "\n"));
+             sanity_check (not (projections_intersect meta ty1 rset1 ty2 rset2)))
+              meta;
           ASymbolic (AProjBorrows (s, ty))
       | _ ->
           log#lerror
@@ -224,8 +225,8 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (
     in
     { value; ty }
 
-let symbolic_expansion_non_borrow_to_value (meta : Meta.meta) (sv : symbolic_value)
-    (see : symbolic_expansion) : typed_value =
+let symbolic_expansion_non_borrow_to_value (meta : Meta.meta)
+    (sv : symbolic_value) (see : symbolic_expansion) : typed_value =
   let ty = Subst.erase_regions sv.sv_ty in
   let value =
     match see with
@@ -240,8 +241,8 @@ let symbolic_expansion_non_borrow_to_value (meta : Meta.meta) (sv : symbolic_val
   in
   { value; ty }
 
-let symbolic_expansion_non_shared_borrow_to_value (meta : Meta.meta) (sv : symbolic_value)
-    (see : symbolic_expansion) : typed_value =
+let symbolic_expansion_non_shared_borrow_to_value (meta : Meta.meta)
+    (sv : symbolic_value) (see : symbolic_expansion) : typed_value =
   match see with
   | SeMutRef (bid, bv) ->
       let ty = Subst.erase_regions sv.sv_ty in
@@ -256,9 +257,9 @@ let symbolic_expansion_non_shared_borrow_to_value (meta : Meta.meta) (sv : symbo
 
     TODO: detailed comments. See [apply_proj_borrows]
 *)
-let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionId.Set.t)
-    (ancestors_regions : RegionId.Set.t) (see : symbolic_expansion)
-    (original_sv_ty : rty) : typed_avalue =
+let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta)
+    (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t)
+    (see : symbolic_expansion) (original_sv_ty : rty) : typed_avalue =
   (* Sanity check: if we have a proj_loans over a symbolic value, it should
    * contain regions which we will project *)
   sanity_check (ty_has_regions_in_set regions original_sv_ty) meta;
@@ -332,8 +333,8 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionI
     borrows - easy - and mutable borrows - in this case, we reborrow the whole
     borrow: [mut_borrow ... ~~> shared_loan {...} (mut_borrow ...)]).
 *)
-let apply_reborrows (meta : Meta.meta) (reborrows : (BorrowId.id * BorrowId.id) list)
-    (ctx : eval_ctx) : eval_ctx =
+let apply_reborrows (meta : Meta.meta)
+    (reborrows : (BorrowId.id * BorrowId.id) list) (ctx : eval_ctx) : eval_ctx =
   (* This is a bit brutal, but whenever we insert a reborrow, we remove
    * it from the list. This allows us to check that all the reborrows were
    * applied before returning.
@@ -468,7 +469,8 @@ let apply_reborrows (meta : Meta.meta) (reborrows : (BorrowId.id * BorrowId.id)
   (* Return *)
   ctx
 
-let prepare_reborrows (config : config) (meta : Meta.meta) (allow_reborrows : bool) :
+let prepare_reborrows (config : config) (meta : Meta.meta)
+    (allow_reborrows : bool) :
     (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx) =
   let reborrows : (BorrowId.id * BorrowId.id) list ref = ref [] in
   (* The function to generate and register fresh reborrows *)
@@ -492,9 +494,10 @@ let prepare_reborrows (config : config) (meta : Meta.meta) (allow_reborrows : bo
   (fresh_reborrow, apply_registered_reborrows)
 
 (** [ty] shouldn't have erased regions *)
-let apply_proj_borrows_on_input_value (config : config) (meta : Meta.meta) (ctx : eval_ctx)
-    (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t)
-    (v : typed_value) (ty : rty) : eval_ctx * typed_avalue =
+let apply_proj_borrows_on_input_value (config : config) (meta : Meta.meta)
+    (ctx : eval_ctx) (regions : RegionId.Set.t)
+    (ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) :
+    eval_ctx * typed_avalue =
   cassert (ty_is_rty ty) meta "TODO: error message";
   let check_symbolic_no_ended = true in
   let allow_reborrows = true in
-- 
cgit v1.2.3


From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 13:21:08 +0100
Subject: added file and line arg to craise and cassert

---
 compiler/InterpreterProjectors.ml | 56 +++++++++++++++++++--------------------
 1 file changed, 28 insertions(+), 28 deletions(-)

(limited to 'compiler/InterpreterProjectors.ml')

diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index f8f99584..0421a46c 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -18,7 +18,7 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
   (* Sanity check - TODO: move those elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
   let ety = Subst.erase_regions ty in
-  sanity_check (ty_is_rty ty && ety = v.ty) meta;
+  sanity_check __FILE__ __LINE__ (ty_is_rty ty && ety = v.ty) meta;
   (* Project - if there are no regions from the abstraction in the type, return [_] *)
   if not (ty_has_regions_in_set regions ty) then []
   else
@@ -41,7 +41,7 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
             fields_types
         in
         List.concat proj_fields
-    | VBottom, _ -> craise meta "Unreachable"
+    | VBottom, _ -> craise __FILE__ __LINE__ meta "Unreachable"
     | VBorrow bc, TRef (r, ref_ty, kind) ->
         (* Retrieve the bid of the borrow and the asb of the projected borrowed value *)
         let bid, asb =
@@ -64,13 +64,13 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
                 | _, Abstract (ASharedLoan (_, sv, _)) ->
                     apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow
                       regions sv ref_ty
-                | _ -> craise meta "Unexpected"
+                | _ -> craise __FILE__ __LINE__ meta "Unexpected"
               in
               (bid, asb)
           | VReservedMutBorrow _, _ ->
-              craise meta
+              craise __FILE__ __LINE__ meta
                 "Can't apply a proj_borrow over a reserved mutable borrow"
-          | _ -> craise meta "Unreachable"
+          | _ -> craise __FILE__ __LINE__ meta "Unreachable"
         in
         let asb =
           (* Check if the region is in the set of projected regions (note that
@@ -81,15 +81,15 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
           else asb
         in
         asb
-    | VLoan _, _ -> craise meta "Unreachable"
+    | VLoan _, _ -> craise __FILE__ __LINE__ meta "Unreachable"
     | VSymbolic s, _ ->
         (* Check that the projection doesn't contain ended regions *)
-        sanity_check
+        sanity_check __FILE__ __LINE__
           (not
              (projections_intersect meta s.sv_ty ctx.ended_regions ty regions))
           meta;
         [ AsbProjReborrows (s, ty) ]
-    | _ -> craise meta "Unreachable"
+    | _ -> craise __FILE__ __LINE__ meta "Unreachable"
 
 let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
     (ctx : eval_ctx) (fresh_reborrow : BorrowId.id -> BorrowId.id)
@@ -98,7 +98,7 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
   (* Sanity check - TODO: move this elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
   let ety = Substitute.erase_regions ty in
-  sanity_check (ty_is_rty ty && ety = v.ty) meta;
+  sanity_check __FILE__ __LINE__ (ty_is_rty ty && ety = v.ty) meta;
   (* Project - if there are no regions from the abstraction in the type, return [_] *)
   if not (ty_has_regions_in_set regions ty) then { value = AIgnored; ty }
   else
@@ -121,7 +121,7 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
               fields_types
           in
           AAdt { variant_id = adt.variant_id; field_values = proj_fields }
-      | VBottom, _ -> craise meta "Unreachable"
+      | VBottom, _ -> craise __FILE__ __LINE__ meta "Unreachable"
       | VBorrow bc, TRef (r, ref_ty, kind) ->
           if
             (* Check if the region is in the set of projected regions (note that
@@ -152,9 +152,9 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
                   *)
                   ASharedBorrow bid
               | VReservedMutBorrow _, _ ->
-                  craise meta
+                  craise __FILE__ __LINE__ meta
                     "Can't apply a proj_borrow over a reserved mutable borrow"
-              | _ -> craise meta "Unreachable"
+              | _ -> craise __FILE__ __LINE__ meta "Unreachable"
             in
             ABorrow bc
           else
@@ -186,16 +186,16 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
                     | _, Abstract (ASharedLoan (_, sv, _)) ->
                         apply_proj_borrows_on_shared_borrow meta ctx
                           fresh_reborrow regions sv ref_ty
-                    | _ -> craise meta "Unexpected"
+                    | _ -> craise __FILE__ __LINE__ meta "Unexpected"
                   in
                   AProjSharedBorrow asb
               | VReservedMutBorrow _, _ ->
-                  craise meta
+                  craise __FILE__ __LINE__ meta
                     "Can't apply a proj_borrow over a reserved mutable borrow"
-              | _ -> craise meta "Unreachable"
+              | _ -> craise __FILE__ __LINE__ meta "Unreachable"
             in
             ABorrow bc
-      | VLoan _, _ -> craise meta "Unreachable"
+      | VLoan _, _ -> craise __FILE__ __LINE__ meta "Unreachable"
       | VSymbolic s, _ ->
           (* Check that the projection doesn't contain already ended regions,
            * if necessary *)
@@ -212,7 +212,7 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
                  ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
                  ^ RegionId.Set.to_string None rset2
                  ^ "\n"));
-             sanity_check (not (projections_intersect meta ty1 rset1 ty2 rset2)))
+             sanity_check __FILE__ __LINE__ (not (projections_intersect meta ty1 rset1 ty2 rset2)))
               meta;
           ASymbolic (AProjBorrows (s, ty))
       | _ ->
@@ -221,7 +221,7 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
               ("apply_proj_borrows: unexpected inputs:\n- input value: "
               ^ typed_value_to_string ~meta:(Some meta) ctx v
               ^ "\n- proj rty: " ^ ty_to_string ctx ty));
-          craise meta "Unreachable"
+          craise __FILE__ __LINE__ meta "Unreachable"
     in
     { value; ty }
 
@@ -237,7 +237,7 @@ let symbolic_expansion_non_borrow_to_value (meta : Meta.meta)
         in
         VAdt { variant_id; field_values }
     | SeMutRef (_, _) | SeSharedRef (_, _) ->
-        craise meta "Unexpected symbolic reference expansion"
+        craise __FILE__ __LINE__ meta "Unexpected symbolic reference expansion"
   in
   { value; ty }
 
@@ -250,7 +250,7 @@ let symbolic_expansion_non_shared_borrow_to_value (meta : Meta.meta)
       let value = VBorrow (VMutBorrow (bid, bv)) in
       { value; ty }
   | SeSharedRef (_, _) ->
-      craise meta "Unexpected symbolic shared reference expansion"
+      craise __FILE__ __LINE__ meta "Unexpected symbolic shared reference expansion"
   | _ -> symbolic_expansion_non_borrow_to_value meta sv see
 
 (** Apply (and reduce) a projector over loans to a value.
@@ -262,7 +262,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta)
     (see : symbolic_expansion) (original_sv_ty : rty) : typed_avalue =
   (* Sanity check: if we have a proj_loans over a symbolic value, it should
    * contain regions which we will project *)
-  sanity_check (ty_has_regions_in_set regions original_sv_ty) meta;
+  sanity_check __FILE__ __LINE__ (ty_has_regions_in_set regions original_sv_ty) meta;
   (* Match *)
   let (value, ty) : avalue * ty =
     match (see, original_sv_ty) with
@@ -277,7 +277,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta)
         (AAdt { variant_id; field_values }, original_sv_ty)
     | SeMutRef (bid, spc), TRef (r, ref_ty, RMut) ->
         (* Sanity check *)
-        sanity_check (spc.sv_ty = ref_ty) meta;
+        sanity_check __FILE__ __LINE__ (spc.sv_ty = ref_ty) meta;
         (* Apply the projector to the borrowed value *)
         let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in
         (* Check if the region is in the set of projected regions (note that
@@ -295,7 +295,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta)
           (ALoan (AIgnoredMutLoan (opt_bid, child_av)), ref_ty)
     | SeSharedRef (bids, spc), TRef (r, ref_ty, RShared) ->
         (* Sanity check *)
-        sanity_check (spc.sv_ty = ref_ty) meta;
+        sanity_check __FILE__ __LINE__ (spc.sv_ty = ref_ty) meta;
         (* Apply the projector to the borrowed value *)
         let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in
         (* Check if the region is in the set of projected regions (note that
@@ -307,7 +307,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta)
         else
           (* Not in the set: ignore *)
           (ALoan (AIgnoredSharedLoan child_av), ref_ty)
-    | _ -> craise meta "Unreachable"
+    | _ -> craise __FILE__ __LINE__ meta "Unreachable"
   in
   { value; ty }
 
@@ -465,7 +465,7 @@ let apply_reborrows (meta : Meta.meta)
   (* Visit *)
   let ctx = obj#visit_eval_ctx () ctx in
   (* Check that there are no reborrows remaining *)
-  sanity_check (!reborrows = []) meta;
+  sanity_check __FILE__ __LINE__ (!reborrows = []) meta;
   (* Return *)
   ctx
 
@@ -479,13 +479,13 @@ let prepare_reborrows (config : config) (meta : Meta.meta)
       let bid' = fresh_borrow_id () in
       reborrows := (bid, bid') :: !reborrows;
       bid')
-    else craise meta "Unexpected reborrow"
+    else craise __FILE__ __LINE__ meta "Unexpected reborrow"
   in
   (* The function to apply the reborrows in a context *)
   let apply_registered_reborrows (ctx : eval_ctx) : eval_ctx =
     match config.mode with
     | ConcreteMode ->
-        sanity_check (!reborrows = []) meta;
+        sanity_check __FILE__ __LINE__ (!reborrows = []) meta;
         ctx
     | SymbolicMode ->
         (* Apply the reborrows *)
@@ -498,7 +498,7 @@ let apply_proj_borrows_on_input_value (config : config) (meta : Meta.meta)
     (ctx : eval_ctx) (regions : RegionId.Set.t)
     (ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) :
     eval_ctx * typed_avalue =
-  cassert (ty_is_rty ty) meta "TODO: error message";
+  cassert __FILE__ __LINE__ (ty_is_rty ty) meta "TODO: error message";
   let check_symbolic_no_ended = true in
   let allow_reborrows = true in
   (* Prepare the reborrows *)
-- 
cgit v1.2.3


From 8f969634f3f192a9282a21a1ca2a1b6a676984ca Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 14:07:36 +0100
Subject: formatting and changed save_error condition for failing from b to not
 b

---
 compiler/InterpreterProjectors.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'compiler/InterpreterProjectors.ml')

diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 0421a46c..d7c20ae0 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -212,7 +212,8 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
                  ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
                  ^ RegionId.Set.to_string None rset2
                  ^ "\n"));
-             sanity_check __FILE__ __LINE__ (not (projections_intersect meta ty1 rset1 ty2 rset2)))
+             sanity_check __FILE__ __LINE__
+               (not (projections_intersect meta ty1 rset1 ty2 rset2)))
               meta;
           ASymbolic (AProjBorrows (s, ty))
       | _ ->
@@ -250,7 +251,8 @@ let symbolic_expansion_non_shared_borrow_to_value (meta : Meta.meta)
       let value = VBorrow (VMutBorrow (bid, bv)) in
       { value; ty }
   | SeSharedRef (_, _) ->
-      craise __FILE__ __LINE__ meta "Unexpected symbolic shared reference expansion"
+      craise __FILE__ __LINE__ meta
+        "Unexpected symbolic shared reference expansion"
   | _ -> symbolic_expansion_non_borrow_to_value meta sv see
 
 (** Apply (and reduce) a projector over loans to a value.
@@ -262,7 +264,9 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta)
     (see : symbolic_expansion) (original_sv_ty : rty) : typed_avalue =
   (* Sanity check: if we have a proj_loans over a symbolic value, it should
    * contain regions which we will project *)
-  sanity_check __FILE__ __LINE__ (ty_has_regions_in_set regions original_sv_ty) meta;
+  sanity_check __FILE__ __LINE__
+    (ty_has_regions_in_set regions original_sv_ty)
+    meta;
   (* Match *)
   let (value, ty) : avalue * ty =
     match (see, original_sv_ty) with
-- 
cgit v1.2.3


From 5809c45fbbfcbb78b15a97be619dcde4ab4868b8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 29 Mar 2024 16:21:15 +0100
Subject: Add some error messages

---
 compiler/InterpreterProjectors.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/InterpreterProjectors.ml')

diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index d7c20ae0..8b6eeb6c 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -502,7 +502,7 @@ let apply_proj_borrows_on_input_value (config : config) (meta : Meta.meta)
     (ctx : eval_ctx) (regions : RegionId.Set.t)
     (ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) :
     eval_ctx * typed_avalue =
-  cassert __FILE__ __LINE__ (ty_is_rty ty) meta "TODO: error message";
+  sanity_check __FILE__ __LINE__ (ty_is_rty ty) meta;
   let check_symbolic_no_ended = true in
   let allow_reborrows = true in
   (* Prepare the reborrows *)
-- 
cgit v1.2.3


From 1a86cac476c1f5c0d64d5a12db267d3ac651561b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 29 Mar 2024 17:49:46 +0100
Subject: Cleanup and fix a mistake

---
 compiler/InterpreterProjectors.ml | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

(limited to 'compiler/InterpreterProjectors.ml')

diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 8b6eeb6c..6e86e6a4 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -199,22 +199,22 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
       | VSymbolic s, _ ->
           (* Check that the projection doesn't contain already ended regions,
            * if necessary *)
-          if check_symbolic_no_ended then
-            (let ty1 = s.sv_ty in
-             let rset1 = ctx.ended_regions in
-             let ty2 = ty in
-             let rset2 = regions in
-             log#ldebug
-               (lazy
-                 ("projections_intersect:" ^ "\n- ty1: " ^ ty_to_string ctx ty1
-                ^ "\n- rset1: "
-                 ^ RegionId.Set.to_string None rset1
-                 ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
-                 ^ RegionId.Set.to_string None rset2
-                 ^ "\n"));
-             sanity_check __FILE__ __LINE__
-               (not (projections_intersect meta ty1 rset1 ty2 rset2)))
-              meta;
+          if check_symbolic_no_ended then (
+            let ty1 = s.sv_ty in
+            let rset1 = ctx.ended_regions in
+            let ty2 = ty in
+            let rset2 = regions in
+            log#ldebug
+              (lazy
+                ("projections_intersect:" ^ "\n- ty1: " ^ ty_to_string ctx ty1
+               ^ "\n- rset1: "
+                ^ RegionId.Set.to_string None rset1
+                ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
+                ^ RegionId.Set.to_string None rset2
+                ^ "\n"));
+            sanity_check __FILE__ __LINE__
+              (not (projections_intersect meta ty1 rset1 ty2 rset2))
+              meta);
           ASymbolic (AProjBorrows (s, ty))
       | _ ->
           log#lerror
-- 
cgit v1.2.3