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/InterpreterLoopsFixedPoint.ml | 85 +++++++++++++++++-----------------
 1 file changed, 43 insertions(+), 42 deletions(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.ml')

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 66c97cde..b07ba943 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -11,6 +11,7 @@ open InterpreterBorrows
 open InterpreterLoopsCore
 open InterpreterLoopsMatchCtxs
 open InterpreterLoopsJoinCtxs
+open Errors
 
 (** The local logger *)
 let log = Logging.loops_fixed_point_log
@@ -135,7 +136,7 @@ let cleanup_fresh_values_and_abs (config : config) (fixed_ids : ids_sets) :
     called typically after we merge abstractions together (see {!collapse_ctx}
     for instance).
  *)
-let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t)
+let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta) (old_abs_ids : AbstractionId.Set.t)
     (ctx : eval_ctx) : eval_ctx =
   let reorder_in_fresh_abs (abs : abs) : abs =
     (* Split between the loans and borrows *)
@@ -143,7 +144,7 @@ let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t)
       match av.value with
       | ABorrow _ -> true
       | ALoan _ -> false
-      | _ -> raise (Failure "Unexpected")
+      | _ -> craise meta "Unexpected"
     in
     let aborrows, aloans = List.partition is_borrow abs.avalues in
 
@@ -156,13 +157,13 @@ let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t)
     let get_borrow_id (av : typed_avalue) : BorrowId.id =
       match av.value with
       | ABorrow (AMutBorrow (bid, _) | ASharedBorrow bid) -> bid
-      | _ -> raise (Failure "Unexpected")
+      | _ -> craise meta "Unexpected"
     in
     let get_loan_id (av : typed_avalue) : BorrowId.id =
       match av.value with
       | ALoan (AMutLoan (lid, _)) -> lid
       | ALoan (ASharedLoan (lids, _, _)) -> BorrowId.Set.min_elt lids
-      | _ -> raise (Failure "Unexpected")
+      | _ -> craise meta "Unexpected"
     in
     (* We use ordered maps to reorder the borrows and loans *)
     let reorder (get_bid : typed_avalue -> BorrowId.id)
@@ -186,7 +187,7 @@ let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t)
 
   { ctx with env }
 
-let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun =
+let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_fun =
  fun cf ctx0 ->
   let ctx = ctx0 in
   (* Compute the set of borrows which appear in the abstractions, so that
@@ -266,12 +267,12 @@ let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun =
     borrow_substs := (lid, nlid) :: !borrow_substs;
 
     (* Rem.: the below sanity checks are not really necessary *)
-    assert (AbstractionId.Set.is_empty abs.parents);
-    assert (abs.original_parents = []);
-    assert (RegionId.Set.is_empty abs.ancestors_regions);
+    cassert (AbstractionId.Set.is_empty abs.parents) meta "abs.parents is not empty TODO";
+    cassert (abs.original_parents = []) meta "original_parents is not empty TODO";
+    cassert (RegionId.Set.is_empty abs.ancestors_regions) meta "ancestors_regions is not empty TODO";
 
     (* Introduce the new abstraction for the shared values *)
-    assert (ty_no_regions sv.ty);
+    cassert (ty_no_regions sv.ty) meta "TODO :  error message ";
     let rty = sv.ty in
 
     (* Create the shared loan child *)
@@ -322,7 +323,7 @@ let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun =
   let collect_shared_values_in_abs (abs : abs) : unit =
     let collect_shared_value lids (sv : typed_value) =
       (* Sanity check: we don't support nested borrows for now *)
-      assert (not (value_has_borrows ctx sv.value));
+      cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows not supported yet";
 
       (* Filter the loan ids whose corresponding borrows appear in abstractions
          (see the documentation of the function) *)
@@ -356,7 +357,7 @@ let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun =
             TODO: implement this more general behavior.
          *)
         method! visit_symbolic_value env sv =
-          assert (not (symbolic_value_has_borrows ctx sv));
+          cassert (not (symbolic_value_has_borrows ctx sv)) meta "There should be no symbolic values with borrows inside the abstraction";
           super#visit_symbolic_value env sv
       end
     in
@@ -432,11 +433,11 @@ let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun =
              SymbolicAst.IntroSymbolic (ctx, None, sv, VaSingleValue v, e))
            e !sid_subst)
 
-let prepare_ashared_loans_no_synth (loop_id : LoopId.id) (ctx : eval_ctx) :
+let prepare_ashared_loans_no_synth (meta : Meta.meta) (loop_id : LoopId.id) (ctx : eval_ctx) :
     eval_ctx =
-  get_cf_ctx_no_synth (prepare_ashared_loans (Some loop_id)) ctx
+  get_cf_ctx_no_synth (prepare_ashared_loans meta (Some loop_id)) ctx
 
-let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
+let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id : LoopId.id)
     (eval_loop_body : st_cm_fun) (ctx0 : eval_ctx) :
     eval_ctx * ids_sets * abs RegionGroupId.Map.t =
   (* The continuation for when we exit the loop - we register the
@@ -453,7 +454,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
 
      For more details, see the comments for {!prepare_ashared_loans}
   *)
-  let ctx = prepare_ashared_loans_no_synth loop_id ctx0 in
+  let ctx = prepare_ashared_loans_no_synth meta loop_id ctx0 in
 
   (* Debug *)
   log#ldebug
@@ -472,15 +473,15 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
     | Return | Panic | Break _ -> None
     | Unit ->
         (* See the comment in {!eval_loop} *)
-        raise (Failure "Unreachable")
+        craise meta "Unreachable"
     | Continue i ->
         (* For now we don't support continues to outer loops *)
-        assert (i = 0);
+        cassert (i = 0) meta "Continues to outer loops not supported yet";
         register_ctx ctx;
         None
     | LoopReturn _ | EndEnterLoop _ | EndContinue _ ->
         (* We don't support nested loops for now *)
-        raise (Failure "Nested loops are not supported for now")
+        craise meta "Nested loops are not supported for now"
   in
 
   (* The fixed ids. They are the ids of the original ctx, after we ended
@@ -573,7 +574,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
     log#ldebug (lazy "compute_fixed_point: equiv_ctx:");
     let fixed_ids = compute_fixed_ids [ ctx1; ctx2 ] in
     let check_equivalent = true in
-    let lookup_shared_value _ = raise (Failure "Unreachable") in
+    let lookup_shared_value _ = craise meta "Unreachable" in
     Option.is_some
       (match_ctxs check_equivalent fixed_ids lookup_shared_value
          lookup_shared_value ctx1 ctx2)
@@ -581,10 +582,10 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
   let max_num_iter = Config.loop_fixed_point_max_num_iters in
   let rec compute_fixed_point (ctx : eval_ctx) (i0 : int) (i : int) : eval_ctx =
     if i = 0 then
-      raise
-        (Failure
+      craise
+        meta
            ("Could not compute a loop fixed point in " ^ string_of_int i0
-          ^ " iterations"))
+          ^ " iterations")
     else
       (* Evaluate the loop body to register the different contexts upon reentry *)
       let _ = eval_loop_body cf_exit_loop_body ctx in
@@ -633,10 +634,10 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
         method! visit_abs _ abs =
           match abs.kind with
           | Loop (loop_id', _, kind) ->
-              assert (loop_id' = loop_id);
-              assert (kind = LoopSynthInput);
+              cassert (loop_id' = loop_id) meta "TODO :  error message ";
+              cassert (kind = LoopSynthInput) meta "TODO :  error message ";
               (* The abstractions introduced so far should be endable *)
-              assert (abs.can_end = true);
+              cassert (abs.can_end = true) meta "The abstractions introduced so far can not end";
               add_aid abs.abs_id;
               abs
           | _ -> abs
@@ -669,12 +670,12 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
           None
       | Break _ ->
           (* We enforce that we can't get there: see {!PrePasses.remove_loop_breaks} *)
-          raise (Failure "Unreachable")
+          craise meta "Unreachable"
       | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ ->
           (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}.
              For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now.
           *)
-          raise (Failure "Unreachable")
+          craise meta "Unreachable"
       | Return ->
           log#ldebug (lazy "compute_loop_entry_fixed_point: cf_loop: Return");
           (* Should we consume the return value and pop the frame?
@@ -693,9 +694,9 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
                 in
                 (* By default, the [SynthInput] abs can't end *)
                 let ctx = ctx_set_abs_can_end ctx abs_id true in
-                assert (
+                cassert (
                   let abs = ctx_lookup_abs ctx abs_id in
-                  abs.kind = SynthInput rg_id);
+                  abs.kind = SynthInput rg_id) meta "TODO :  error message ";
                 (* End this abstraction *)
                 let ctx =
                   InterpreterBorrows.end_abstraction_no_synth config abs_id ctx
@@ -717,14 +718,14 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
     let _ =
       RegionGroupId.Map.iter
         (fun _ ids ->
-          assert (AbstractionId.Set.disjoint !aids_union ids);
+          cassert (AbstractionId.Set.disjoint !aids_union ids) meta "The sets of abstractions we need to end per region group are not pairwise disjoint";
           aids_union := AbstractionId.Set.union ids !aids_union)
         !fp_ended_aids
     in
 
     (* We also check that all the regions need to end - this is not necessary per
        se, but if it doesn't happen it is bizarre and worth investigating... *)
-    assert (AbstractionId.Set.equal !aids_union !fp_aids);
+    cassert (AbstractionId.Set.equal !aids_union !fp_aids) meta "Not all regions need to end TODO";
 
     (* Merge the abstractions which need to be merged, and compute the map from
        region id to abstraction id *)
@@ -781,7 +782,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
                     fp := fp';
                     id0 := id0';
                     ()
-                  with ValueMatchFailure _ -> raise (Failure "Unexpected"))
+                  with ValueMatchFailure _ -> craise meta "Unexpected")
                 ids;
               (* Register the mapping *)
               let abs = ctx_lookup_abs !fp !id0 in
@@ -792,7 +793,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
 
     (* Reorder the loans and borrows in the fresh abstractions in the fixed-point *)
     let fp =
-      reorder_loans_borrows_in_fresh_abs (Option.get !fixed_ids).aids !fp
+      reorder_loans_borrows_in_fresh_abs (meta : Meta.meta) (Option.get !fixed_ids).aids !fp
     in
 
     (* Update the abstraction's [can_end] field and their kinds.
@@ -814,8 +815,8 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
         method! visit_abs _ abs =
           match abs.kind with
           | Loop (loop_id', _, kind) ->
-              assert (loop_id' = loop_id);
-              assert (kind = LoopSynthInput);
+              cassert (loop_id' = loop_id) meta "TODO :  error message ";
+              cassert (kind = LoopSynthInput) meta "TODO :  error message ";
               let kind : abs_kind =
                 if remove_rg_id then Loop (loop_id, None, LoopSynthInput)
                 else abs.kind
@@ -849,7 +850,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
   (* Return *)
   (fp, fixed_ids, rg_to_abs)
 
-let compute_fixed_point_id_correspondance (fixed_ids : ids_sets)
+let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_sets)
     (src_ctx : eval_ctx) (tgt_ctx : eval_ctx) : borrow_loan_corresp =
   log#ldebug
     (lazy
@@ -877,10 +878,10 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets)
     let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in
     let open InterpreterBorrowsCore in
     let lookup_shared_loan lid ctx : typed_value =
-      match snd (lookup_loan ek_all lid ctx) with
+      match snd (lookup_loan meta ek_all lid ctx) with
       | Concrete (VSharedLoan (_, v)) -> v
       | Abstract (ASharedLoan (_, v, _)) -> v
-      | _ -> raise (Failure "Unreachable")
+      | _ -> craise meta "Unreachable"
     in
     let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in
     let lookup_in_src id = lookup_shared_loan id src_ctx in
@@ -940,7 +941,7 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets)
           ids.loan_ids
       in
       (* Check that the loan and borrows are related *)
-      assert (BorrowId.Set.equal ids.borrow_ids loan_ids))
+      cassert (BorrowId.Set.equal ids.borrow_ids loan_ids) meta "The loan and borrows are not related")
     new_absl;
 
   (* For every target abstraction (going back to the [list_nth_mut] example,
@@ -983,7 +984,7 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets)
     loan_to_borrow_id_map = tgt_loan_to_borrow;
   }
 
-let compute_fp_ctx_symbolic_values (ctx : eval_ctx) (fp_ctx : eval_ctx) :
+let compute_fp_ctx_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) (fp_ctx : eval_ctx) :
     SymbolicValueId.Set.t * symbolic_value list =
   let old_ids, _ = compute_ctx_ids ctx in
   let fp_ids, fp_ids_maps = compute_ctx_ids fp_ctx in
@@ -1064,10 +1065,10 @@ let compute_fp_ctx_symbolic_values (ctx : eval_ctx) (fp_ctx : eval_ctx) :
         method! visit_VSharedBorrow env bid =
           let open InterpreterBorrowsCore in
           let v =
-            match snd (lookup_loan ek_all bid fp_ctx) with
+            match snd (lookup_loan meta ek_all bid fp_ctx) with
             | Concrete (VSharedLoan (_, v)) -> v
             | Abstract (ASharedLoan (_, v, _)) -> v
-            | _ -> raise (Failure "Unreachable")
+            | _ -> craise meta "Unreachable"
           in
           self#visit_typed_value env v
 
-- 
cgit v1.2.3


From 8f89bd8df9f382284eabb5a2020a2fa634f92fac Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Tue, 12 Mar 2024 17:19:14 +0100
Subject: WIP: does not compile yet because we need to propagate the meta
 variable.

---
 compiler/InterpreterLoopsFixedPoint.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.ml')

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index b07ba943..35582456 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -693,7 +693,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
                   AbstractionId.of_int (RegionGroupId.to_int rg_id)
                 in
                 (* By default, the [SynthInput] abs can't end *)
-                let ctx = ctx_set_abs_can_end ctx abs_id true in
+                let ctx = ctx_set_abs_can_end meta ctx abs_id true in
                 cassert (
                   let abs = ctx_lookup_abs ctx abs_id in
                   abs.kind = SynthInput rg_id) meta "TODO :  error message ";
@@ -764,7 +764,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
               in
               let abs = ctx_lookup_abs !fp !id0 in
               let abs = { abs with kind = abs_kind } in
-              let fp', _ = ctx_subst_abs !fp !id0 abs in
+              let fp', _ = ctx_subst_abs meta !fp !id0 abs in
               fp := fp';
               (* Merge all the abstractions into this one *)
               List.iter
-- 
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/InterpreterLoopsFixedPoint.ml | 62 +++++++++++++++++-----------------
 1 file changed, 31 insertions(+), 31 deletions(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.ml')

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 35582456..508d0f0c 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -215,7 +215,7 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_f
     (* Remove the shared loans *)
     let v = value_remove_shared_loans v in
     (* Substitute the symbolic values and the region *)
-    Substitute.typed_value_subst_ids
+    Substitute.typed_value_subst_ids meta
       (fun r -> if RegionId.Set.mem r rids then nrid else r)
       (fun x -> x)
       (fun x -> x)
@@ -267,9 +267,9 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_f
     borrow_substs := (lid, nlid) :: !borrow_substs;
 
     (* Rem.: the below sanity checks are not really necessary *)
-    cassert (AbstractionId.Set.is_empty abs.parents) meta "abs.parents is not empty TODO";
-    cassert (abs.original_parents = []) meta "original_parents is not empty TODO";
-    cassert (RegionId.Set.is_empty abs.ancestors_regions) meta "ancestors_regions is not empty TODO";
+    cassert (AbstractionId.Set.is_empty abs.parents) meta "abs.parents is not empty TODO: Error message";
+    cassert (abs.original_parents = []) meta "original_parents is not empty TODO: Error message";
+    cassert (RegionId.Set.is_empty abs.ancestors_regions) meta "ancestors_regions is not empty TODO: Error message";
 
     (* Introduce the new abstraction for the shared values *)
     cassert (ty_no_regions sv.ty) meta "TODO :  error message ";
@@ -277,19 +277,19 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_f
 
     (* Create the shared loan child *)
     let child_rty = rty in
-    let child_av = mk_aignored child_rty in
+    let child_av = mk_aignored meta child_rty in
 
     (* Create the shared loan *)
     let loan_rty = TRef (RFVar nrid, rty, RShared) in
     let loan_value =
       ALoan (ASharedLoan (BorrowId.Set.singleton nlid, nsv, child_av))
     in
-    let loan_value = mk_typed_avalue loan_rty loan_value in
+    let loan_value = mk_typed_avalue meta loan_rty loan_value in
 
     (* Create the shared borrow *)
     let borrow_rty = loan_rty in
     let borrow_value = ABorrow (ASharedBorrow lid) in
-    let borrow_value = mk_typed_avalue borrow_rty borrow_value in
+    let borrow_value = mk_typed_avalue meta borrow_rty borrow_value in
 
     (* Create the abstraction *)
     let avalues = [ borrow_value; loan_value ] in
@@ -435,7 +435,7 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_f
 
 let prepare_ashared_loans_no_synth (meta : Meta.meta) (loop_id : LoopId.id) (ctx : eval_ctx) :
     eval_ctx =
-  get_cf_ctx_no_synth (prepare_ashared_loans meta (Some loop_id)) ctx
+  get_cf_ctx_no_synth meta (prepare_ashared_loans meta (Some loop_id)) ctx
 
 let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id : LoopId.id)
     (eval_loop_body : st_cm_fun) (ctx0 : eval_ctx) :
@@ -461,9 +461,9 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
     (lazy
       ("compute_loop_entry_fixed_point: after prepare_ashared_loans:"
      ^ "\n\n- ctx0:\n"
-      ^ eval_ctx_to_string_no_filter ctx0
+      ^ eval_ctx_to_string_no_filter meta ctx0
       ^ "\n\n- ctx1:\n"
-      ^ eval_ctx_to_string_no_filter ctx
+      ^ eval_ctx_to_string_no_filter meta ctx
       ^ "\n\n"));
 
   let cf_exit_loop_body (res : statement_eval_res) : m_fun =
@@ -510,10 +510,10 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
           (* End those borrows and abstractions *)
           let end_borrows_abs blids aids ctx =
             let ctx =
-              InterpreterBorrows.end_borrows_no_synth config blids ctx
+              InterpreterBorrows.end_borrows_no_synth meta config blids ctx
             in
             let ctx =
-              InterpreterBorrows.end_abstractions_no_synth config aids ctx
+              InterpreterBorrows.end_abstractions_no_synth meta config aids ctx
             in
             ctx
           in
@@ -544,7 +544,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
 
     (* Join the context with the context at the loop entry *)
     let (_, _), ctx2 =
-      loop_join_origin_with_continue_ctxs config loop_id fixed_ids ctx1 !ctxs
+      loop_join_origin_with_continue_ctxs meta config loop_id fixed_ids ctx1 !ctxs
     in
     ctxs := [];
     ctx2
@@ -576,7 +576,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
     let check_equivalent = true in
     let lookup_shared_value _ = craise meta "Unreachable" in
     Option.is_some
-      (match_ctxs check_equivalent fixed_ids lookup_shared_value
+      (match_ctxs meta check_equivalent fixed_ids lookup_shared_value
          lookup_shared_value ctx1 ctx2)
   in
   let max_num_iter = Config.loop_fixed_point_max_num_iters in
@@ -597,9 +597,9 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
       log#ldebug
         (lazy
           ("compute_fixed_point:" ^ "\n\n- ctx0:\n"
-          ^ eval_ctx_to_string_no_filter ctx
+          ^ eval_ctx_to_string_no_filter meta ctx
           ^ "\n\n- ctx1:\n"
-          ^ eval_ctx_to_string_no_filter ctx1
+          ^ eval_ctx_to_string_no_filter meta ctx1
           ^ "\n\n"));
 
       (* Check if we reached a fixed point: if not, iterate *)
@@ -612,7 +612,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
     (lazy
       ("compute_fixed_point: fixed point computed before matching with input \
         region groups:" ^ "\n\n- fp:\n"
-      ^ eval_ctx_to_string_no_filter fp
+      ^ eval_ctx_to_string_no_filter meta fp
       ^ "\n\n"));
 
   (* Make sure we have exactly one loop abstraction per function region (merge
@@ -699,7 +699,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
                   abs.kind = SynthInput rg_id) meta "TODO :  error message ";
                 (* End this abstraction *)
                 let ctx =
-                  InterpreterBorrows.end_abstraction_no_synth config abs_id ctx
+                  InterpreterBorrows.end_abstraction_no_synth meta config abs_id ctx
                 in
                 (* Explore the context, and check which abstractions are not there anymore *)
                 let ids, _ = compute_ctx_ids ctx in
@@ -725,7 +725,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
 
     (* We also check that all the regions need to end - this is not necessary per
        se, but if it doesn't happen it is bizarre and worth investigating... *)
-    cassert (AbstractionId.Set.equal !aids_union !fp_aids) meta "Not all regions need to end TODO";
+    cassert (AbstractionId.Set.equal !aids_union !fp_aids) meta "Not all regions need to end TODO: Error message";
 
     (* Merge the abstractions which need to be merged, and compute the map from
        region id to abstraction id *)
@@ -777,7 +777,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
                         ^ AbstractionId.to_string !id0));
                     (* Note that we merge *into* [id0] *)
                     let fp', id0' =
-                      merge_into_abstraction loop_id abs_kind false !fp id !id0
+                      merge_into_abstraction meta loop_id abs_kind false !fp id !id0
                     in
                     fp := fp';
                     id0 := id0';
@@ -793,7 +793,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
 
     (* Reorder the loans and borrows in the fresh abstractions in the fixed-point *)
     let fp =
-      reorder_loans_borrows_in_fresh_abs (meta : Meta.meta) (Option.get !fixed_ids).aids !fp
+      reorder_loans_borrows_in_fresh_abs meta (Option.get !fixed_ids).aids !fp
     in
 
     (* Update the abstraction's [can_end] field and their kinds.
@@ -838,7 +838,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
         (lazy
           ("compute_fixed_point: fixed point after matching with the function \
             region groups:\n"
-          ^ eval_ctx_to_string_no_filter fp_test));
+          ^ eval_ctx_to_string_no_filter meta fp_test));
       compute_fixed_point fp_test 1 1
     in
 
@@ -855,21 +855,21 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_se
   log#ldebug
     (lazy
       ("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n"
-     ^ show_ids_sets fixed_ids ^ "\n\n- src_ctx:\n" ^ eval_ctx_to_string src_ctx
-     ^ "\n\n- tgt_ctx:\n" ^ eval_ctx_to_string tgt_ctx ^ "\n\n"));
+     ^ show_ids_sets fixed_ids ^ "\n\n- src_ctx:\n" ^ eval_ctx_to_string meta src_ctx
+     ^ "\n\n- tgt_ctx:\n" ^ eval_ctx_to_string meta tgt_ctx ^ "\n\n"));
 
-  let filt_src_env, _, _ = ctx_split_fixed_new fixed_ids src_ctx in
+  let filt_src_env, _, _ = ctx_split_fixed_new meta fixed_ids src_ctx in
   let filt_src_ctx = { src_ctx with env = filt_src_env } in
-  let filt_tgt_env, new_absl, _ = ctx_split_fixed_new fixed_ids tgt_ctx in
+  let filt_tgt_env, new_absl, _ = ctx_split_fixed_new meta fixed_ids tgt_ctx in
   let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in
 
   log#ldebug
     (lazy
       ("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n"
      ^ show_ids_sets fixed_ids ^ "\n\n- filt_src_ctx:\n"
-      ^ eval_ctx_to_string filt_src_ctx
+      ^ eval_ctx_to_string meta filt_src_ctx
       ^ "\n\n- filt_tgt_ctx:\n"
-      ^ eval_ctx_to_string filt_tgt_ctx
+      ^ eval_ctx_to_string meta filt_tgt_ctx
       ^ "\n\n"));
 
   (* Match the source context and the filtered target context *)
@@ -886,7 +886,7 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_se
     let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in
     let lookup_in_src id = lookup_shared_loan id src_ctx in
     Option.get
-      (match_ctxs check_equiv fixed_ids lookup_in_tgt lookup_in_src filt_tgt_ctx
+      (match_ctxs meta check_equiv fixed_ids lookup_in_tgt lookup_in_src filt_tgt_ctx
          filt_src_ctx)
   in
 
@@ -1089,9 +1089,9 @@ let compute_fp_ctx_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) (fp_ctx :
   log#ldebug
     (lazy
       ("compute_fp_ctx_symbolic_values:" ^ "\n- src context:\n"
-      ^ eval_ctx_to_string_no_filter ctx
+      ^ eval_ctx_to_string_no_filter meta ctx
       ^ "\n- fixed point:\n"
-      ^ eval_ctx_to_string_no_filter fp_ctx
+      ^ eval_ctx_to_string_no_filter meta fp_ctx
       ^ "\n- fresh_sids: "
       ^ SymbolicValueId.Set.show fresh_sids
       ^ "\n- input_svalues: "
-- 
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/InterpreterLoopsFixedPoint.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.ml')

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 508d0f0c..ef2c5698 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -437,7 +437,7 @@ let prepare_ashared_loans_no_synth (meta : Meta.meta) (loop_id : LoopId.id) (ctx
     eval_ctx =
   get_cf_ctx_no_synth meta (prepare_ashared_loans meta (Some loop_id)) ctx
 
-let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id : LoopId.id)
+let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id : LoopId.id)
     (eval_loop_body : st_cm_fun) (ctx0 : eval_ctx) :
     eval_ctx * ids_sets * abs RegionGroupId.Map.t =
   (* The continuation for when we exit the loop - we register the
@@ -510,10 +510,10 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
           (* End those borrows and abstractions *)
           let end_borrows_abs blids aids ctx =
             let ctx =
-              InterpreterBorrows.end_borrows_no_synth meta config blids ctx
+              InterpreterBorrows.end_borrows_no_synth config meta blids ctx
             in
             let ctx =
-              InterpreterBorrows.end_abstractions_no_synth meta config aids ctx
+              InterpreterBorrows.end_abstractions_no_synth config meta aids ctx
             in
             ctx
           in
@@ -544,7 +544,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
 
     (* Join the context with the context at the loop entry *)
     let (_, _), ctx2 =
-      loop_join_origin_with_continue_ctxs meta config loop_id fixed_ids ctx1 !ctxs
+      loop_join_origin_with_continue_ctxs config meta loop_id fixed_ids ctx1 !ctxs
     in
     ctxs := [];
     ctx2
@@ -699,7 +699,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
                   abs.kind = SynthInput rg_id) meta "TODO :  error message ";
                 (* End this abstraction *)
                 let ctx =
-                  InterpreterBorrows.end_abstraction_no_synth meta config abs_id ctx
+                  InterpreterBorrows.end_abstraction_no_synth config meta abs_id ctx
                 in
                 (* Explore the context, and check which abstractions are not there anymore *)
                 let ids, _ = compute_ctx_ids ctx in
-- 
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/InterpreterLoopsFixedPoint.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.ml')

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index ef2c5698..44b9a44e 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -267,9 +267,9 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_f
     borrow_substs := (lid, nlid) :: !borrow_substs;
 
     (* Rem.: the below sanity checks are not really necessary *)
-    cassert (AbstractionId.Set.is_empty abs.parents) meta "abs.parents is not empty TODO: Error message";
-    cassert (abs.original_parents = []) meta "original_parents is not empty TODO: Error message";
-    cassert (RegionId.Set.is_empty abs.ancestors_regions) meta "ancestors_regions is not empty TODO: Error message";
+    sanity_check (AbstractionId.Set.is_empty abs.parents) meta;
+    sanity_check (abs.original_parents = []) meta;
+    sanity_check (RegionId.Set.is_empty abs.ancestors_regions) meta;
 
     (* Introduce the new abstraction for the shared values *)
     cassert (ty_no_regions sv.ty) meta "TODO :  error message ";
@@ -323,7 +323,7 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_f
   let collect_shared_values_in_abs (abs : abs) : unit =
     let collect_shared_value lids (sv : typed_value) =
       (* Sanity check: we don't support nested borrows for now *)
-      cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows not supported yet";
+      sanity_check (not (value_has_borrows ctx sv.value)) meta;
 
       (* Filter the loan ids whose corresponding borrows appear in abstractions
          (see the documentation of the function) *)
-- 
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/InterpreterLoopsFixedPoint.ml | 44 +++++++++++++++++-----------------
 1 file changed, 22 insertions(+), 22 deletions(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.ml')

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 44b9a44e..f6ce9b32 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -272,7 +272,7 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_f
     sanity_check (RegionId.Set.is_empty abs.ancestors_regions) meta;
 
     (* Introduce the new abstraction for the shared values *)
-    cassert (ty_no_regions sv.ty) meta "TODO :  error message ";
+    cassert (ty_no_regions sv.ty) meta "Nested borrows are not supported yet";
     let rty = sv.ty in
 
     (* Create the shared loan child *)
@@ -461,9 +461,9 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
     (lazy
       ("compute_loop_entry_fixed_point: after prepare_ashared_loans:"
      ^ "\n\n- ctx0:\n"
-      ^ eval_ctx_to_string_no_filter meta ctx0
+      ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx0
       ^ "\n\n- ctx1:\n"
-      ^ eval_ctx_to_string_no_filter meta ctx
+      ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx
       ^ "\n\n"));
 
   let cf_exit_loop_body (res : statement_eval_res) : m_fun =
@@ -597,9 +597,9 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
       log#ldebug
         (lazy
           ("compute_fixed_point:" ^ "\n\n- ctx0:\n"
-          ^ eval_ctx_to_string_no_filter meta ctx
+          ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx
           ^ "\n\n- ctx1:\n"
-          ^ eval_ctx_to_string_no_filter meta ctx1
+          ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx1
           ^ "\n\n"));
 
       (* Check if we reached a fixed point: if not, iterate *)
@@ -612,7 +612,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
     (lazy
       ("compute_fixed_point: fixed point computed before matching with input \
         region groups:" ^ "\n\n- fp:\n"
-      ^ eval_ctx_to_string_no_filter meta fp
+      ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp
       ^ "\n\n"));
 
   (* Make sure we have exactly one loop abstraction per function region (merge
@@ -634,10 +634,10 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
         method! visit_abs _ abs =
           match abs.kind with
           | Loop (loop_id', _, kind) ->
-              cassert (loop_id' = loop_id) meta "TODO :  error message ";
-              cassert (kind = LoopSynthInput) meta "TODO :  error message ";
+              sanity_check (loop_id' = loop_id) meta;
+              sanity_check (kind = LoopSynthInput) meta;
               (* The abstractions introduced so far should be endable *)
-              cassert (abs.can_end = true) meta "The abstractions introduced so far can not end";
+              sanity_check (abs.can_end = true) meta;
               add_aid abs.abs_id;
               abs
           | _ -> abs
@@ -694,9 +694,9 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
                 in
                 (* By default, the [SynthInput] abs can't end *)
                 let ctx = ctx_set_abs_can_end meta ctx abs_id true in
-                cassert (
+                sanity_check (
                   let abs = ctx_lookup_abs ctx abs_id in
-                  abs.kind = SynthInput rg_id) meta "TODO :  error message ";
+                  abs.kind = SynthInput rg_id) meta;
                 (* End this abstraction *)
                 let ctx =
                   InterpreterBorrows.end_abstraction_no_synth config meta abs_id ctx
@@ -725,7 +725,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
 
     (* We also check that all the regions need to end - this is not necessary per
        se, but if it doesn't happen it is bizarre and worth investigating... *)
-    cassert (AbstractionId.Set.equal !aids_union !fp_aids) meta "Not all regions need to end TODO: Error message";
+    sanity_check (AbstractionId.Set.equal !aids_union !fp_aids) meta;
 
     (* Merge the abstractions which need to be merged, and compute the map from
        region id to abstraction id *)
@@ -815,8 +815,8 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
         method! visit_abs _ abs =
           match abs.kind with
           | Loop (loop_id', _, kind) ->
-              cassert (loop_id' = loop_id) meta "TODO :  error message ";
-              cassert (kind = LoopSynthInput) meta "TODO :  error message ";
+              sanity_check (loop_id' = loop_id) meta;
+              sanity_check (kind = LoopSynthInput) meta;
               let kind : abs_kind =
                 if remove_rg_id then Loop (loop_id, None, LoopSynthInput)
                 else abs.kind
@@ -838,7 +838,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
         (lazy
           ("compute_fixed_point: fixed point after matching with the function \
             region groups:\n"
-          ^ eval_ctx_to_string_no_filter meta fp_test));
+          ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_test));
       compute_fixed_point fp_test 1 1
     in
 
@@ -855,8 +855,8 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_se
   log#ldebug
     (lazy
       ("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n"
-     ^ show_ids_sets fixed_ids ^ "\n\n- src_ctx:\n" ^ eval_ctx_to_string meta src_ctx
-     ^ "\n\n- tgt_ctx:\n" ^ eval_ctx_to_string meta tgt_ctx ^ "\n\n"));
+     ^ show_ids_sets fixed_ids ^ "\n\n- src_ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) src_ctx
+     ^ "\n\n- tgt_ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx ^ "\n\n"));
 
   let filt_src_env, _, _ = ctx_split_fixed_new meta fixed_ids src_ctx in
   let filt_src_ctx = { src_ctx with env = filt_src_env } in
@@ -867,9 +867,9 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_se
     (lazy
       ("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n"
      ^ show_ids_sets fixed_ids ^ "\n\n- filt_src_ctx:\n"
-      ^ eval_ctx_to_string meta filt_src_ctx
+      ^ eval_ctx_to_string ~meta:(Some meta) filt_src_ctx
       ^ "\n\n- filt_tgt_ctx:\n"
-      ^ eval_ctx_to_string meta filt_tgt_ctx
+      ^ eval_ctx_to_string ~meta:(Some meta) filt_tgt_ctx
       ^ "\n\n"));
 
   (* Match the source context and the filtered target context *)
@@ -941,7 +941,7 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_se
           ids.loan_ids
       in
       (* Check that the loan and borrows are related *)
-      cassert (BorrowId.Set.equal ids.borrow_ids loan_ids) meta "The loan and borrows are not related")
+      sanity_check (BorrowId.Set.equal ids.borrow_ids loan_ids) meta)
     new_absl;
 
   (* For every target abstraction (going back to the [list_nth_mut] example,
@@ -1089,9 +1089,9 @@ let compute_fp_ctx_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) (fp_ctx :
   log#ldebug
     (lazy
       ("compute_fp_ctx_symbolic_values:" ^ "\n- src context:\n"
-      ^ eval_ctx_to_string_no_filter meta ctx
+      ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx
       ^ "\n- fixed point:\n"
-      ^ eval_ctx_to_string_no_filter meta fp_ctx
+      ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_ctx
       ^ "\n- fresh_sids: "
       ^ SymbolicValueId.Set.show fresh_sids
       ^ "\n- input_svalues: "
-- 
cgit v1.2.3


From 53347ecc40b308b0b75a620453bfa8bd520a2c70 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 16:31:24 +0100
Subject: changes after git rebase main

---
 compiler/InterpreterLoopsFixedPoint.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.ml')

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index f6ce9b32..f5bd4a35 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -23,7 +23,7 @@ exception FoundAbsId of AbstractionId.id
    - end the borrows which appear in fresh anonymous values and don't contain loans
    - end the fresh region abstractions which can be ended (no loans)
 *)
-let rec end_useless_fresh_borrows_and_abs (config : config)
+let rec end_useless_fresh_borrows_and_abs (config : config) (meta : Meta.meta)
     (fixed_ids : ids_sets) : cm_fun =
  fun cf ctx ->
   let rec explore_env (env : env) : unit =
@@ -56,7 +56,7 @@ let rec end_useless_fresh_borrows_and_abs (config : config)
     | EAbs abs :: env when not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)
       -> (
         (* Check if it is possible to end the abstraction: if yes, raise an exception *)
-        let opt_loan = get_first_non_ignored_aloan_in_abstraction abs in
+        let opt_loan = get_first_non_ignored_aloan_in_abstraction meta abs in
         match opt_loan with
         | None ->
             (* No remaining loans: we can end the abstraction *)
@@ -66,7 +66,7 @@ let rec end_useless_fresh_borrows_and_abs (config : config)
             explore_env env)
     | _ :: env -> explore_env env
   in
-  let rec_call = end_useless_fresh_borrows_and_abs config fixed_ids in
+  let rec_call = end_useless_fresh_borrows_and_abs config meta fixed_ids in
   try
     (* Explore the environment *)
     explore_env ctx.env;
@@ -74,10 +74,10 @@ let rec end_useless_fresh_borrows_and_abs (config : config)
     cf ctx
   with
   | FoundAbsId abs_id ->
-      let cc = end_abstraction config abs_id in
+      let cc = end_abstraction config meta abs_id in
       comp cc rec_call cf ctx
   | FoundBorrowId bid ->
-      let cc = end_borrow config bid in
+      let cc = end_borrow config meta bid in
       comp cc rec_call cf ctx
 
 (* Explore the fresh anonymous values and replace all the values which are not
@@ -121,11 +121,11 @@ let cleanup_fresh_values (fixed_ids : ids_sets) : cm_fun =
    - also end the borrows which appear in fresh anonymous values and don't contain loans
    - end the fresh region abstractions which can be ended (no loans)
 *)
-let cleanup_fresh_values_and_abs (config : config) (fixed_ids : ids_sets) :
+let cleanup_fresh_values_and_abs (config : config) (meta : Meta.meta) (fixed_ids : ids_sets) :
     cm_fun =
  fun cf ctx ->
   comp
-    (end_useless_fresh_borrows_and_abs config fixed_ids)
+    (end_useless_fresh_borrows_and_abs config meta fixed_ids)
     (cleanup_fresh_values fixed_ids)
     cf ctx
 
-- 
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/InterpreterLoopsFixedPoint.ml | 74 +++++++++++++++++++++-------------
 1 file changed, 45 insertions(+), 29 deletions(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.ml')

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index f5bd4a35..7ddf55c1 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -121,8 +121,8 @@ let cleanup_fresh_values (fixed_ids : ids_sets) : cm_fun =
    - also end the borrows which appear in fresh anonymous values and don't contain loans
    - end the fresh region abstractions which can be ended (no loans)
 *)
-let cleanup_fresh_values_and_abs (config : config) (meta : Meta.meta) (fixed_ids : ids_sets) :
-    cm_fun =
+let cleanup_fresh_values_and_abs (config : config) (meta : Meta.meta)
+    (fixed_ids : ids_sets) : cm_fun =
  fun cf ctx ->
   comp
     (end_useless_fresh_borrows_and_abs config meta fixed_ids)
@@ -136,8 +136,8 @@ let cleanup_fresh_values_and_abs (config : config) (meta : Meta.meta) (fixed_ids
     called typically after we merge abstractions together (see {!collapse_ctx}
     for instance).
  *)
-let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta) (old_abs_ids : AbstractionId.Set.t)
-    (ctx : eval_ctx) : eval_ctx =
+let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta)
+    (old_abs_ids : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx =
   let reorder_in_fresh_abs (abs : abs) : abs =
     (* Split between the loans and borrows *)
     let is_borrow (av : typed_avalue) : bool =
@@ -187,7 +187,8 @@ let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta) (old_abs_ids : Abstrac
 
   { ctx with env }
 
-let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_fun =
+let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) :
+    cm_fun =
  fun cf ctx0 ->
   let ctx = ctx0 in
   (* Compute the set of borrows which appear in the abstractions, so that
@@ -357,7 +358,11 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_f
             TODO: implement this more general behavior.
          *)
         method! visit_symbolic_value env sv =
-          cassert (not (symbolic_value_has_borrows ctx sv)) meta "There should be no symbolic values with borrows inside the abstraction";
+          cassert
+            (not (symbolic_value_has_borrows ctx sv))
+            meta
+            "There should be no symbolic values with borrows inside the \
+             abstraction";
           super#visit_symbolic_value env sv
       end
     in
@@ -433,12 +438,12 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_f
              SymbolicAst.IntroSymbolic (ctx, None, sv, VaSingleValue v, e))
            e !sid_subst)
 
-let prepare_ashared_loans_no_synth (meta : Meta.meta) (loop_id : LoopId.id) (ctx : eval_ctx) :
-    eval_ctx =
+let prepare_ashared_loans_no_synth (meta : Meta.meta) (loop_id : LoopId.id)
+    (ctx : eval_ctx) : eval_ctx =
   get_cf_ctx_no_synth meta (prepare_ashared_loans meta (Some loop_id)) ctx
 
-let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id : LoopId.id)
-    (eval_loop_body : st_cm_fun) (ctx0 : eval_ctx) :
+let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
+    (loop_id : LoopId.id) (eval_loop_body : st_cm_fun) (ctx0 : eval_ctx) :
     eval_ctx * ids_sets * abs RegionGroupId.Map.t =
   (* The continuation for when we exit the loop - we register the
      environments upon loop *reentry*, and synthesize nothing by
@@ -544,7 +549,8 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
 
     (* Join the context with the context at the loop entry *)
     let (_, _), ctx2 =
-      loop_join_origin_with_continue_ctxs config meta loop_id fixed_ids ctx1 !ctxs
+      loop_join_origin_with_continue_ctxs config meta loop_id fixed_ids ctx1
+        !ctxs
     in
     ctxs := [];
     ctx2
@@ -582,10 +588,9 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
   let max_num_iter = Config.loop_fixed_point_max_num_iters in
   let rec compute_fixed_point (ctx : eval_ctx) (i0 : int) (i : int) : eval_ctx =
     if i = 0 then
-      craise
-        meta
-           ("Could not compute a loop fixed point in " ^ string_of_int i0
-          ^ " iterations")
+      craise meta
+        ("Could not compute a loop fixed point in " ^ string_of_int i0
+       ^ " iterations")
     else
       (* Evaluate the loop body to register the different contexts upon reentry *)
       let _ = eval_loop_body cf_exit_loop_body ctx in
@@ -694,12 +699,14 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
                 in
                 (* By default, the [SynthInput] abs can't end *)
                 let ctx = ctx_set_abs_can_end meta ctx abs_id true in
-                sanity_check (
-                  let abs = ctx_lookup_abs ctx abs_id in
-                  abs.kind = SynthInput rg_id) meta;
+                sanity_check
+                  (let abs = ctx_lookup_abs ctx abs_id in
+                   abs.kind = SynthInput rg_id)
+                  meta;
                 (* End this abstraction *)
                 let ctx =
-                  InterpreterBorrows.end_abstraction_no_synth config meta abs_id ctx
+                  InterpreterBorrows.end_abstraction_no_synth config meta abs_id
+                    ctx
                 in
                 (* Explore the context, and check which abstractions are not there anymore *)
                 let ids, _ = compute_ctx_ids ctx in
@@ -718,7 +725,11 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
     let _ =
       RegionGroupId.Map.iter
         (fun _ ids ->
-          cassert (AbstractionId.Set.disjoint !aids_union ids) meta "The sets of abstractions we need to end per region group are not pairwise disjoint";
+          cassert
+            (AbstractionId.Set.disjoint !aids_union ids)
+            meta
+            "The sets of abstractions we need to end per region group are not \
+             pairwise disjoint";
           aids_union := AbstractionId.Set.union ids !aids_union)
         !fp_ended_aids
     in
@@ -777,7 +788,8 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
                         ^ AbstractionId.to_string !id0));
                     (* Note that we merge *into* [id0] *)
                     let fp', id0' =
-                      merge_into_abstraction meta loop_id abs_kind false !fp id !id0
+                      merge_into_abstraction meta loop_id abs_kind false !fp id
+                        !id0
                     in
                     fp := fp';
                     id0 := id0';
@@ -850,13 +862,17 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
   (* Return *)
   (fp, fixed_ids, rg_to_abs)
 
-let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_sets)
-    (src_ctx : eval_ctx) (tgt_ctx : eval_ctx) : borrow_loan_corresp =
+let compute_fixed_point_id_correspondance (meta : Meta.meta)
+    (fixed_ids : ids_sets) (src_ctx : eval_ctx) (tgt_ctx : eval_ctx) :
+    borrow_loan_corresp =
   log#ldebug
     (lazy
       ("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n"
-     ^ show_ids_sets fixed_ids ^ "\n\n- src_ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) src_ctx
-     ^ "\n\n- tgt_ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx ^ "\n\n"));
+     ^ show_ids_sets fixed_ids ^ "\n\n- src_ctx:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) src_ctx
+      ^ "\n\n- tgt_ctx:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx
+      ^ "\n\n"));
 
   let filt_src_env, _, _ = ctx_split_fixed_new meta fixed_ids src_ctx in
   let filt_src_ctx = { src_ctx with env = filt_src_env } in
@@ -886,8 +902,8 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_se
     let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in
     let lookup_in_src id = lookup_shared_loan id src_ctx in
     Option.get
-      (match_ctxs meta check_equiv fixed_ids lookup_in_tgt lookup_in_src filt_tgt_ctx
-         filt_src_ctx)
+      (match_ctxs meta check_equiv fixed_ids lookup_in_tgt lookup_in_src
+         filt_tgt_ctx filt_src_ctx)
   in
 
   log#ldebug
@@ -984,8 +1000,8 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_se
     loan_to_borrow_id_map = tgt_loan_to_borrow;
   }
 
-let compute_fp_ctx_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) (fp_ctx : eval_ctx) :
-    SymbolicValueId.Set.t * symbolic_value list =
+let compute_fp_ctx_symbolic_values (meta : Meta.meta) (ctx : eval_ctx)
+    (fp_ctx : eval_ctx) : SymbolicValueId.Set.t * symbolic_value list =
   let old_ids, _ = compute_ctx_ids ctx in
   let fp_ids, fp_ids_maps = compute_ctx_ids fp_ctx in
   let fresh_sids = SymbolicValueId.Set.diff fp_ids.sids old_ids.sids 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/InterpreterLoopsFixedPoint.ml | 56 +++++++++++++++++-----------------
 1 file changed, 28 insertions(+), 28 deletions(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.ml')

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 7ddf55c1..39add08e 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -144,7 +144,7 @@ let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta)
       match av.value with
       | ABorrow _ -> true
       | ALoan _ -> false
-      | _ -> craise meta "Unexpected"
+      | _ -> craise __FILE__ __LINE__ meta "Unexpected"
     in
     let aborrows, aloans = List.partition is_borrow abs.avalues in
 
@@ -157,13 +157,13 @@ let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta)
     let get_borrow_id (av : typed_avalue) : BorrowId.id =
       match av.value with
       | ABorrow (AMutBorrow (bid, _) | ASharedBorrow bid) -> bid
-      | _ -> craise meta "Unexpected"
+      | _ -> craise __FILE__ __LINE__ meta "Unexpected"
     in
     let get_loan_id (av : typed_avalue) : BorrowId.id =
       match av.value with
       | ALoan (AMutLoan (lid, _)) -> lid
       | ALoan (ASharedLoan (lids, _, _)) -> BorrowId.Set.min_elt lids
-      | _ -> craise meta "Unexpected"
+      | _ -> craise __FILE__ __LINE__ meta "Unexpected"
     in
     (* We use ordered maps to reorder the borrows and loans *)
     let reorder (get_bid : typed_avalue -> BorrowId.id)
@@ -268,12 +268,12 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) :
     borrow_substs := (lid, nlid) :: !borrow_substs;
 
     (* Rem.: the below sanity checks are not really necessary *)
-    sanity_check (AbstractionId.Set.is_empty abs.parents) meta;
-    sanity_check (abs.original_parents = []) meta;
-    sanity_check (RegionId.Set.is_empty abs.ancestors_regions) meta;
+    sanity_check __FILE__ __LINE__ (AbstractionId.Set.is_empty abs.parents) meta;
+    sanity_check __FILE__ __LINE__ (abs.original_parents = []) meta;
+    sanity_check __FILE__ __LINE__ (RegionId.Set.is_empty abs.ancestors_regions) meta;
 
     (* Introduce the new abstraction for the shared values *)
-    cassert (ty_no_regions sv.ty) meta "Nested borrows are not supported yet";
+    cassert __FILE__ __LINE__ (ty_no_regions sv.ty) meta "Nested borrows are not supported yet";
     let rty = sv.ty in
 
     (* Create the shared loan child *)
@@ -324,7 +324,7 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) :
   let collect_shared_values_in_abs (abs : abs) : unit =
     let collect_shared_value lids (sv : typed_value) =
       (* Sanity check: we don't support nested borrows for now *)
-      sanity_check (not (value_has_borrows ctx sv.value)) meta;
+      sanity_check __FILE__ __LINE__ (not (value_has_borrows ctx sv.value)) meta;
 
       (* Filter the loan ids whose corresponding borrows appear in abstractions
          (see the documentation of the function) *)
@@ -358,7 +358,7 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) :
             TODO: implement this more general behavior.
          *)
         method! visit_symbolic_value env sv =
-          cassert
+          cassert __FILE__ __LINE__
             (not (symbolic_value_has_borrows ctx sv))
             meta
             "There should be no symbolic values with borrows inside the \
@@ -478,15 +478,15 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
     | Return | Panic | Break _ -> None
     | Unit ->
         (* See the comment in {!eval_loop} *)
-        craise meta "Unreachable"
+        craise __FILE__ __LINE__ meta "Unreachable"
     | Continue i ->
         (* For now we don't support continues to outer loops *)
-        cassert (i = 0) meta "Continues to outer loops not supported yet";
+        cassert __FILE__ __LINE__ (i = 0) meta "Continues to outer loops not supported yet";
         register_ctx ctx;
         None
     | LoopReturn _ | EndEnterLoop _ | EndContinue _ ->
         (* We don't support nested loops for now *)
-        craise meta "Nested loops are not supported for now"
+        craise __FILE__ __LINE__ meta "Nested loops are not supported for now"
   in
 
   (* The fixed ids. They are the ids of the original ctx, after we ended
@@ -580,7 +580,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
     log#ldebug (lazy "compute_fixed_point: equiv_ctx:");
     let fixed_ids = compute_fixed_ids [ ctx1; ctx2 ] in
     let check_equivalent = true in
-    let lookup_shared_value _ = craise meta "Unreachable" in
+    let lookup_shared_value _ = craise __FILE__ __LINE__ meta "Unreachable" in
     Option.is_some
       (match_ctxs meta check_equivalent fixed_ids lookup_shared_value
          lookup_shared_value ctx1 ctx2)
@@ -588,7 +588,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
   let max_num_iter = Config.loop_fixed_point_max_num_iters in
   let rec compute_fixed_point (ctx : eval_ctx) (i0 : int) (i : int) : eval_ctx =
     if i = 0 then
-      craise meta
+      craise __FILE__ __LINE__ meta
         ("Could not compute a loop fixed point in " ^ string_of_int i0
        ^ " iterations")
     else
@@ -639,10 +639,10 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
         method! visit_abs _ abs =
           match abs.kind with
           | Loop (loop_id', _, kind) ->
-              sanity_check (loop_id' = loop_id) meta;
-              sanity_check (kind = LoopSynthInput) meta;
+              sanity_check __FILE__ __LINE__ (loop_id' = loop_id) meta;
+              sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) meta;
               (* The abstractions introduced so far should be endable *)
-              sanity_check (abs.can_end = true) meta;
+              sanity_check __FILE__ __LINE__ (abs.can_end = true) meta;
               add_aid abs.abs_id;
               abs
           | _ -> abs
@@ -675,12 +675,12 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
           None
       | Break _ ->
           (* We enforce that we can't get there: see {!PrePasses.remove_loop_breaks} *)
-          craise meta "Unreachable"
+          craise __FILE__ __LINE__ meta "Unreachable"
       | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ ->
           (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}.
              For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now.
           *)
-          craise meta "Unreachable"
+          craise __FILE__ __LINE__ meta "Unreachable"
       | Return ->
           log#ldebug (lazy "compute_loop_entry_fixed_point: cf_loop: Return");
           (* Should we consume the return value and pop the frame?
@@ -699,7 +699,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
                 in
                 (* By default, the [SynthInput] abs can't end *)
                 let ctx = ctx_set_abs_can_end meta ctx abs_id true in
-                sanity_check
+                sanity_check __FILE__ __LINE__
                   (let abs = ctx_lookup_abs ctx abs_id in
                    abs.kind = SynthInput rg_id)
                   meta;
@@ -725,7 +725,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
     let _ =
       RegionGroupId.Map.iter
         (fun _ ids ->
-          cassert
+          cassert __FILE__ __LINE__
             (AbstractionId.Set.disjoint !aids_union ids)
             meta
             "The sets of abstractions we need to end per region group are not \
@@ -736,7 +736,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
 
     (* We also check that all the regions need to end - this is not necessary per
        se, but if it doesn't happen it is bizarre and worth investigating... *)
-    sanity_check (AbstractionId.Set.equal !aids_union !fp_aids) meta;
+    sanity_check __FILE__ __LINE__ (AbstractionId.Set.equal !aids_union !fp_aids) meta;
 
     (* Merge the abstractions which need to be merged, and compute the map from
        region id to abstraction id *)
@@ -794,7 +794,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
                     fp := fp';
                     id0 := id0';
                     ()
-                  with ValueMatchFailure _ -> craise meta "Unexpected")
+                  with ValueMatchFailure _ -> craise __FILE__ __LINE__ meta "Unexpected")
                 ids;
               (* Register the mapping *)
               let abs = ctx_lookup_abs !fp !id0 in
@@ -827,8 +827,8 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
         method! visit_abs _ abs =
           match abs.kind with
           | Loop (loop_id', _, kind) ->
-              sanity_check (loop_id' = loop_id) meta;
-              sanity_check (kind = LoopSynthInput) meta;
+              sanity_check __FILE__ __LINE__ (loop_id' = loop_id) meta;
+              sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) meta;
               let kind : abs_kind =
                 if remove_rg_id then Loop (loop_id, None, LoopSynthInput)
                 else abs.kind
@@ -897,7 +897,7 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta)
       match snd (lookup_loan meta ek_all lid ctx) with
       | Concrete (VSharedLoan (_, v)) -> v
       | Abstract (ASharedLoan (_, v, _)) -> v
-      | _ -> craise meta "Unreachable"
+      | _ -> craise __FILE__ __LINE__ meta "Unreachable"
     in
     let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in
     let lookup_in_src id = lookup_shared_loan id src_ctx in
@@ -957,7 +957,7 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta)
           ids.loan_ids
       in
       (* Check that the loan and borrows are related *)
-      sanity_check (BorrowId.Set.equal ids.borrow_ids loan_ids) meta)
+      sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids.borrow_ids loan_ids) meta)
     new_absl;
 
   (* For every target abstraction (going back to the [list_nth_mut] example,
@@ -1084,7 +1084,7 @@ let compute_fp_ctx_symbolic_values (meta : Meta.meta) (ctx : eval_ctx)
             match snd (lookup_loan meta ek_all bid fp_ctx) with
             | Concrete (VSharedLoan (_, v)) -> v
             | Abstract (ASharedLoan (_, v, _)) -> v
-            | _ -> craise meta "Unreachable"
+            | _ -> craise __FILE__ __LINE__ meta "Unreachable"
           in
           self#visit_typed_value env v
 
-- 
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/InterpreterLoopsFixedPoint.ml | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.ml')

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 39add08e..9ff2fe38 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -270,10 +270,13 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) :
     (* Rem.: the below sanity checks are not really necessary *)
     sanity_check __FILE__ __LINE__ (AbstractionId.Set.is_empty abs.parents) meta;
     sanity_check __FILE__ __LINE__ (abs.original_parents = []) meta;
-    sanity_check __FILE__ __LINE__ (RegionId.Set.is_empty abs.ancestors_regions) meta;
+    sanity_check __FILE__ __LINE__
+      (RegionId.Set.is_empty abs.ancestors_regions)
+      meta;
 
     (* Introduce the new abstraction for the shared values *)
-    cassert __FILE__ __LINE__ (ty_no_regions sv.ty) meta "Nested borrows are not supported yet";
+    cassert __FILE__ __LINE__ (ty_no_regions sv.ty) meta
+      "Nested borrows are not supported yet";
     let rty = sv.ty in
 
     (* Create the shared loan child *)
@@ -481,7 +484,8 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
         craise __FILE__ __LINE__ meta "Unreachable"
     | Continue i ->
         (* For now we don't support continues to outer loops *)
-        cassert __FILE__ __LINE__ (i = 0) meta "Continues to outer loops not supported yet";
+        cassert __FILE__ __LINE__ (i = 0) meta
+          "Continues to outer loops not supported yet";
         register_ctx ctx;
         None
     | LoopReturn _ | EndEnterLoop _ | EndContinue _ ->
@@ -736,7 +740,9 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
 
     (* We also check that all the regions need to end - this is not necessary per
        se, but if it doesn't happen it is bizarre and worth investigating... *)
-    sanity_check __FILE__ __LINE__ (AbstractionId.Set.equal !aids_union !fp_aids) meta;
+    sanity_check __FILE__ __LINE__
+      (AbstractionId.Set.equal !aids_union !fp_aids)
+      meta;
 
     (* Merge the abstractions which need to be merged, and compute the map from
        region id to abstraction id *)
@@ -794,7 +800,8 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
                     fp := fp';
                     id0 := id0';
                     ()
-                  with ValueMatchFailure _ -> craise __FILE__ __LINE__ meta "Unexpected")
+                  with ValueMatchFailure _ ->
+                    craise __FILE__ __LINE__ meta "Unexpected")
                 ids;
               (* Register the mapping *)
               let abs = ctx_lookup_abs !fp !id0 in
@@ -957,7 +964,9 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta)
           ids.loan_ids
       in
       (* Check that the loan and borrows are related *)
-      sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids.borrow_ids loan_ids) meta)
+      sanity_check __FILE__ __LINE__
+        (BorrowId.Set.equal ids.borrow_ids loan_ids)
+        meta)
     new_absl;
 
   (* For every target abstraction (going back to the [list_nth_mut] example,
-- 
cgit v1.2.3