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/InterpreterExpansion.ml | 147 ++++++++++++++++++++-------------------
 1 file changed, 74 insertions(+), 73 deletions(-)

(limited to 'compiler/InterpreterExpansion.ml')

diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index e489ddc3..0a5a289e 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -13,6 +13,7 @@ open ValuesUtils
 open InterpreterUtils
 open InterpreterProjectors
 open Print.EvalCtx
+open Errors
 module S = SynthesizeSymbolic
 
 (** The local logger *)
@@ -47,7 +48,7 @@ type proj_kind = LoanProj | BorrowProj
     Note that 2. and 3. may have a little bit of duplicated code, but hopefully
     it would make things clearer.
 *)
-let apply_symbolic_expansion_to_target_avalues (config : config)
+let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : config)
     (allow_reborrows : bool) (proj_kind : proj_kind)
     (original_sv : symbolic_value) (expansion : symbolic_expansion)
     (ctx : eval_ctx) : eval_ctx =
@@ -65,7 +66,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
       (** When visiting an abstraction, we remember the regions it owns to be
           able to properly reduce projectors when expanding symbolic values *)
       method! visit_abs current_abs abs =
-        assert (Option.is_none current_abs);
+        cassert (Option.is_none current_abs) meta "T";
         let current_abs = Some abs in
         super#visit_abs current_abs abs
 
@@ -77,7 +78,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
       method! visit_aproj current_abs aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
-            assert (not (same_symbolic_id sv original_sv))
+            cassert (not (same_symbolic_id sv original_sv)) meta "T"
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj current_abs aproj
 
@@ -97,7 +98,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
             (* Check if this is the symbolic value we are looking for *)
             if same_symbolic_id sv original_sv then (
               (* There mustn't be any given back values *)
-              assert (given_back = []);
+              cassert (given_back = []) meta "T";
               (* Apply the projector *)
               let projected_value =
                 apply_proj_loans_on_symbolic_expansion proj_regions
@@ -145,11 +146,11 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
 (** Auxiliary function.
     Apply a symbolic expansion to avalues in a context.
 *)
-let apply_symbolic_expansion_to_avalues (config : config)
+let apply_symbolic_expansion_to_avalues (meta : Meta.meta) (config : config)
     (allow_reborrows : bool) (original_sv : symbolic_value)
     (expansion : symbolic_expansion) (ctx : eval_ctx) : eval_ctx =
   let apply_expansion proj_kind ctx =
-    apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind
+    apply_symbolic_expansion_to_target_avalues meta config allow_reborrows proj_kind
       original_sv expansion ctx
   in
   (* First target the loan projectors, then the borrow projectors *)
@@ -162,12 +163,12 @@ let apply_symbolic_expansion_to_avalues (config : config)
     Simply replace the symbolic values (*not avalues*) in the context with
     a given value. Will break invariants if not used properly.
 *)
-let replace_symbolic_values (at_most_once : bool) (original_sv : symbolic_value)
+let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) (original_sv : symbolic_value)
     (nv : value) (ctx : eval_ctx) : eval_ctx =
   (* Count *)
   let replaced = ref false in
   let replace () =
-    if at_most_once then assert (not !replaced);
+    if at_most_once then cassert (not !replaced) meta "T";
     replaced := true;
     nv
   in
@@ -186,16 +187,16 @@ let replace_symbolic_values (at_most_once : bool) (original_sv : symbolic_value)
   (* Return *)
   ctx
 
-let apply_symbolic_expansion_non_borrow (config : config)
+let apply_symbolic_expansion_non_borrow (meta : Meta.meta) (config : config)
     (original_sv : symbolic_value) (expansion : symbolic_expansion)
     (ctx : eval_ctx) : eval_ctx =
   (* Apply the expansion to non-abstraction values *)
   let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
   let at_most_once = false in
-  let ctx = replace_symbolic_values at_most_once original_sv nv.value ctx in
+  let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in
   (* Apply the expansion to abstraction values *)
   let allow_reborrows = false in
-  apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
+  apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv
     expansion ctx
 
 (** Compute the expansion of a non-assumed (i.e.: not [Box], etc.)
@@ -208,13 +209,13 @@ let apply_symbolic_expansion_non_borrow (config : config)
     [expand_enumerations] controls the expansion of enumerations: if false, it
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
-let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
+let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (expand_enumerations : bool)
     (def_id : TypeDeclId.id) (generics : generic_args) (ctx : eval_ctx) :
     symbolic_expansion list =
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
   let def = ctx_lookup_type_decl ctx def_id in
-  assert (List.length generics.regions = List.length def.generics.regions);
+  cassert (List.length generics.regions = List.length def.generics.regions) meta "T";
   (* Retrieve, for every variant, the list of its instantiated field types *)
   let variants_fields_types =
     AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes ctx def
@@ -222,7 +223,7 @@ let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
   in
   (* Check if there is strictly more than one variant *)
   if List.length variants_fields_types > 1 && not expand_enumerations then
-    raise (Failure "Not allowed to expand enumerations with several variants");
+    craise meta "Not allowed to expand enumerations with several variants";
   (* Initialize the expanded value for a given variant *)
   let initialize ((variant_id, field_types) : VariantId.id option * rty list) :
       symbolic_expansion =
@@ -260,21 +261,21 @@ let compute_expanded_symbolic_box_value (boxed_ty : rty) : symbolic_expansion =
     [expand_enumerations] controls the expansion of enumerations: if [false], it
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
-let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
+let compute_expanded_symbolic_adt_value (meta : Meta.meta) (expand_enumerations : bool)
     (adt_id : type_id) (generics : generic_args) (ctx : eval_ctx) :
     symbolic_expansion list =
   match (adt_id, generics.regions, generics.types) with
   | TAdtId def_id, _, _ ->
-      compute_expanded_symbolic_non_assumed_adt_value expand_enumerations def_id
+      compute_expanded_symbolic_non_assumed_adt_value meta expand_enumerations def_id
         generics ctx
   | TTuple, [], _ -> [ compute_expanded_symbolic_tuple_value generics.types ]
   | TAssumed TBox, [], [ boxed_ty ] ->
       [ compute_expanded_symbolic_box_value boxed_ty ]
   | _ ->
-      raise
-        (Failure "compute_expanded_symbolic_adt_value: unexpected combination")
+      craise
+        meta "compute_expanded_symbolic_adt_value: unexpected combination"
 
-let expand_symbolic_value_shared_borrow (config : config)
+let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
     (ref_ty : rty) : cm_fun =
  fun cf ctx ->
@@ -307,7 +308,7 @@ let expand_symbolic_value_shared_borrow (config : config)
             Some [ AsbBorrow bid; shared_asb ]
           else (* Not in the set: ignore *)
             Some [ shared_asb ]
-      | _ -> raise (Failure "Unexpected")
+      | _ -> craise meta "Unexpected"
     else None
   in
   (* The fresh symbolic value for the shared value *)
@@ -324,7 +325,7 @@ let expand_symbolic_value_shared_borrow (config : config)
         else super#visit_VSymbolic env sv
 
       method! visit_EAbs proj_regions abs =
-        assert (Option.is_none proj_regions);
+        cassert (Option.is_none proj_regions) meta "T";
         let proj_regions = Some abs.regions in
         super#visit_EAbs proj_regions abs
 
@@ -349,7 +350,7 @@ let expand_symbolic_value_shared_borrow (config : config)
       method! visit_aproj proj_regions aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
-            assert (not (same_symbolic_id sv original_sv))
+            cassert (not (same_symbolic_id sv original_sv)) meta "T"
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj proj_regions aproj
 
@@ -375,27 +376,27 @@ let expand_symbolic_value_shared_borrow (config : config)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Finally, replace the projectors on loans *)
   let bids = !borrows in
-  assert (not (BorrowId.Set.is_empty bids));
+  cassert (not (BorrowId.Set.is_empty bids)) meta "T";
   let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
-    apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see
+    apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv see
       ctx
   in
   (* Call the continuation *)
   let expr = cf ctx in
   (* Update the synthesized program *)
-  S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place see
+  S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place see
     expr
 
 (** TODO: simplify and merge with the other expansion function *)
-let expand_symbolic_value_borrow (config : config)
+let expand_symbolic_value_borrow (meta : Meta.meta) (config : config)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
     (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun =
  fun cf ctx ->
-  assert (region <> RErased);
+  cassert (region <> RErased) meta "T";
   (* Check that we are allowed to expand the reference *)
-  assert (not (region_in_set region ctx.ended_regions));
+  cassert (not (region_in_set region ctx.ended_regions)) meta "T";
   (* Match on the reference kind *)
   match rkind with
   | RMut ->
@@ -408,20 +409,20 @@ let expand_symbolic_value_borrow (config : config)
        * check that we perform exactly one substitution) *)
       let nv = symbolic_expansion_non_shared_borrow_to_value original_sv see in
       let at_most_once = true in
-      let ctx = replace_symbolic_values at_most_once original_sv nv.value ctx in
+      let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in
       (* Expand the symbolic avalues *)
       let allow_reborrows = true in
       let ctx =
-        apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
+        apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv
           see ctx
       in
       (* Apply the continuation *)
       let expr = cf ctx in
       (* Update the synthesized program *)
-      S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place
+      S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place
         see expr
   | RShared ->
-      expand_symbolic_value_shared_borrow config original_sv original_sv_place
+      expand_symbolic_value_shared_borrow meta config original_sv original_sv_place
         ref_ty cf ctx
 
 (** A small helper.
@@ -440,12 +441,12 @@ let expand_symbolic_value_borrow (config : config)
     We need this continuation separately (i.e., we can't compose it with the
     continuations in [see_cf_l]) because we perform a join *before* calling it.
 *)
-let apply_branching_symbolic_expansions_non_borrow (config : config)
+let apply_branching_symbolic_expansions_non_borrow (meta : Meta.meta) (config : config)
     (sv : symbolic_value) (sv_place : SA.mplace option)
     (see_cf_l : (symbolic_expansion option * st_cm_fun) list)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
-  assert (see_cf_l <> []);
+  cassert (see_cf_l <> []) meta "T";
   (* Apply the symbolic expansion in the context and call the continuation *)
   let resl =
     List.map
@@ -456,7 +457,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : config)
         let ctx =
           match see_opt with
           | None -> ctx
-          | Some see -> apply_symbolic_expansion_non_borrow config sv see ctx
+          | Some see -> apply_symbolic_expansion_non_borrow meta config sv see ctx
         in
         (* Debug *)
         log#ldebug
@@ -475,15 +476,15 @@ let apply_branching_symbolic_expansions_non_borrow (config : config)
     match resl with
     | Some _ :: _ -> Some (List.map Option.get resl)
     | None :: _ ->
-        List.iter (fun res -> assert (res = None)) resl;
+        List.iter (fun res -> cassert (res = None) meta "T") resl;
         None
-    | _ -> raise (Failure "Unreachable")
+    | _ -> craise meta "Unreachable"
   in
   (* Synthesize and return *)
   let seel = List.map fst see_cf_l in
-  S.synthesize_symbolic_expansion sv sv_place seel subterms
+  S.synthesize_symbolic_expansion meta sv sv_place seel subterms
 
-let expand_symbolic_bool (config : config) (sv : symbolic_value)
+let expand_symbolic_bool (meta : Meta.meta) (config : config) (sv : symbolic_value)
     (sv_place : SA.mplace option) (cf_true : st_cm_fun) (cf_false : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
@@ -491,16 +492,16 @@ let expand_symbolic_bool (config : config) (sv : symbolic_value)
   let original_sv = sv in
   let original_sv_place = sv_place in
   let rty = original_sv.sv_ty in
-  assert (rty = TLiteral TBool);
+  cassert (rty = TLiteral TBool) meta "T";
   (* Expand the symbolic value to true or false and continue execution *)
   let see_true = SeLiteral (VBool true) in
   let see_false = SeLiteral (VBool false) in
   let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in
   (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *)
-  apply_branching_symbolic_expansions_non_borrow config original_sv
+  apply_branching_symbolic_expansions_non_borrow meta config original_sv
     original_sv_place seel cf_after_join ctx
 
-let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value)
+let expand_symbolic_value_no_branching (meta : Meta.meta) (config : config) (sv : symbolic_value)
     (sv_place : SA.mplace option) : cm_fun =
  fun cf ctx ->
   (* Debug *)
@@ -522,29 +523,29 @@ let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value)
         (* Compute the expanded value *)
         let allow_branching = false in
         let seel =
-          compute_expanded_symbolic_adt_value allow_branching adt_id generics
+          compute_expanded_symbolic_adt_value meta allow_branching adt_id generics
             ctx
         in
         (* There should be exacly one branch *)
         let see = Collections.List.to_cons_nil seel in
         (* Apply in the context *)
         let ctx =
-          apply_symbolic_expansion_non_borrow config original_sv see ctx
+          apply_symbolic_expansion_non_borrow meta config original_sv see ctx
         in
         (* Call the continuation *)
         let expr = cf ctx in
         (* Update the synthesized program *)
-        S.synthesize_symbolic_expansion_no_branching original_sv
+        S.synthesize_symbolic_expansion_no_branching meta original_sv
           original_sv_place see expr
     (* Borrows *)
     | TRef (region, ref_ty, rkind) ->
-        expand_symbolic_value_borrow config original_sv original_sv_place region
+        expand_symbolic_value_borrow meta config original_sv original_sv_place region
           ref_ty rkind cf ctx
     | _ ->
-        raise
-          (Failure
+        craise
+          meta
              ("expand_symbolic_value_no_branching: unexpected type: "
-            ^ show_rty rty))
+            ^ show_rty rty)
   in
   (* Debug *)
   let cc =
@@ -556,12 +557,12 @@ let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value)
             ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
             ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
         (* Sanity check: the symbolic value has disappeared *)
-        assert (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)))
+        cassert (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta "T")
   in
   (* Continue *)
   cc cf ctx
 
-let expand_symbolic_adt (config : config) (sv : symbolic_value)
+let expand_symbolic_adt (meta : Meta.meta) (config : config) (sv : symbolic_value)
     (sv_place : SA.mplace option) (cf_branches : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
@@ -579,21 +580,21 @@ let expand_symbolic_adt (config : config) (sv : symbolic_value)
       let allow_branching = true in
       (* Compute the expanded value *)
       let seel =
-        compute_expanded_symbolic_adt_value allow_branching adt_id generics ctx
+        compute_expanded_symbolic_adt_value meta allow_branching adt_id generics ctx
       in
       (* Apply *)
       let seel = List.map (fun see -> (Some see, cf_branches)) seel in
-      apply_branching_symbolic_expansions_non_borrow config original_sv
+      apply_branching_symbolic_expansions_non_borrow meta config original_sv
         original_sv_place seel cf_after_join ctx
   | _ ->
-      raise (Failure ("expand_symbolic_adt: unexpected type: " ^ show_rty rty))
+      craise meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty)
 
-let expand_symbolic_int (config : config) (sv : symbolic_value)
+let expand_symbolic_int (meta : Meta.meta) (config : config) (sv : symbolic_value)
     (sv_place : SA.mplace option) (int_type : integer_type)
     (tgts : (scalar_value * st_cm_fun) list) (otherwise : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
   (* Sanity check *)
-  assert (sv.sv_ty = TLiteral (TInteger int_type));
+  cassert (sv.sv_ty = TLiteral (TInteger int_type)) meta "T";
   (* For all the branches of the switch, we expand the symbolic value
    * to the value given by the branch and execute the branch statement.
    * For the otherwise branch, we leave the symbolic value as it is
@@ -608,7 +609,7 @@ let expand_symbolic_int (config : config) (sv : symbolic_value)
   in
   let seel = List.append seel [ (None, otherwise) ] in
   (* Then expand and evaluate - this generates the proper symbolic AST *)
-  apply_branching_symbolic_expansions_non_borrow config sv sv_place seel
+  apply_branching_symbolic_expansions_non_borrow meta config sv sv_place seel
     cf_after_join
 
 (** Expand all the symbolic values which contain borrows.
@@ -619,7 +620,7 @@ let expand_symbolic_int (config : config) (sv : symbolic_value)
     an enumeration with strictly more than one variant, a slice, etc.) or if
     we need to expand a recursive type (because this leads to looping).
  *)
-let greedy_expand_symbolics_with_borrows (config : config) : cm_fun =
+let greedy_expand_symbolics_with_borrows (meta : Meta.meta) (config : config) : cm_fun =
  fun cf ctx ->
   (* The visitor object, to look for symbolic values in the concrete environment *)
   let obj =
@@ -660,33 +661,33 @@ let greedy_expand_symbolics_with_borrows (config : config) : cm_fun =
             (match def.kind with
             | Struct _ | Enum ([] | [ _ ]) -> ()
             | Enum (_ :: _) ->
-                raise
-                  (Failure
+                craise
+                  meta
                      ("Attempted to greedily expand a symbolic enumeration \
                        with > 1 variants (option \
                        [greedy_expand_symbolics_with_borrows] of [config]): "
-                     ^ name_to_string ctx def.name))
+                     ^ name_to_string ctx def.name)
             | Opaque ->
-                raise (Failure "Attempted to greedily expand an opaque type"));
+                craise meta "Attempted to greedily expand an opaque type");
             (* Also, we need to check if the definition is recursive *)
             if ctx_type_decl_is_rec ctx def_id then
-              raise
-                (Failure
+              craise
+                meta
                    ("Attempted to greedily expand a recursive definition \
                      (option [greedy_expand_symbolics_with_borrows] of \
                      [config]): "
-                   ^ name_to_string ctx def.name))
-            else expand_symbolic_value_no_branching config sv None
+                   ^ name_to_string ctx def.name)
+            else expand_symbolic_value_no_branching meta config sv None
         | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) ->
             (* Ok *)
-            expand_symbolic_value_no_branching config sv None
+            expand_symbolic_value_no_branching meta config sv None
         | TAdt (TAssumed (TArray | TSlice | TStr), _) ->
             (* We can't expand those *)
-            raise
-              (Failure
-                 "Attempted to greedily expand an ADT which can't be expanded ")
+            craise
+              meta
+                 "Attempted to greedily expand an ADT which can't be expanded "
         | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ ->
-            raise (Failure "Unreachable")
+            craise meta "Unreachable"
       in
       (* Compose and continue *)
       comp cc expand cf ctx
@@ -694,9 +695,9 @@ let greedy_expand_symbolics_with_borrows (config : config) : cm_fun =
   (* Apply *)
   expand cf ctx
 
-let greedy_expand_symbolic_values (config : config) : cm_fun =
+let greedy_expand_symbolic_values (meta : Meta.meta) (config : config) : cm_fun =
  fun cf ctx ->
   if Config.greedy_expand_symbolics_with_borrows then (
     log#ldebug (lazy "greedy_expand_symbolic_values");
-    greedy_expand_symbolics_with_borrows config cf ctx)
+    greedy_expand_symbolics_with_borrows meta config cf ctx)
   else cf ctx
-- 
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/InterpreterExpansion.ml | 68 ++++++++++++++++++++--------------------
 1 file changed, 34 insertions(+), 34 deletions(-)

(limited to 'compiler/InterpreterExpansion.ml')

diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 0a5a289e..9448f3e8 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -56,7 +56,7 @@ let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : conf
   let check_symbolic_no_ended = false in
   (* Prepare reborrows registration *)
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows config allow_reborrows
+    prepare_reborrows meta config allow_reborrows
   in
   (* Visitor to apply the expansion *)
   let obj =
@@ -66,7 +66,7 @@ let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : conf
       (** When visiting an abstraction, we remember the regions it owns to be
           able to properly reduce projectors when expanding symbolic values *)
       method! visit_abs current_abs abs =
-        cassert (Option.is_none current_abs) meta "T";
+        cassert (Option.is_none current_abs) meta "TODO: error message";
         let current_abs = Some abs in
         super#visit_abs current_abs abs
 
@@ -78,7 +78,7 @@ let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : conf
       method! visit_aproj current_abs aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
-            cassert (not (same_symbolic_id sv original_sv)) meta "T"
+            cassert (not (same_symbolic_id sv original_sv)) meta "TODO: error message"
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj current_abs aproj
 
@@ -98,10 +98,10 @@ let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : conf
             (* Check if this is the symbolic value we are looking for *)
             if same_symbolic_id sv original_sv then (
               (* There mustn't be any given back values *)
-              cassert (given_back = []) meta "T";
+              cassert (given_back = []) meta "TODO: error message";
               (* Apply the projector *)
               let projected_value =
-                apply_proj_loans_on_symbolic_expansion proj_regions
+                apply_proj_loans_on_symbolic_expansion meta proj_regions
                   ancestors_regions expansion original_sv.sv_ty
               in
               (* Replace *)
@@ -118,12 +118,12 @@ let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : conf
               (* WARNING: we mustn't get there if the expansion is for a shared
                * reference. *)
               let expansion =
-                symbolic_expansion_non_shared_borrow_to_value original_sv
+                symbolic_expansion_non_shared_borrow_to_value meta original_sv
                   expansion
               in
               (* Apply the projector *)
               let projected_value =
-                apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
+                apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow
                   proj_regions ancestors_regions expansion proj_ty
               in
               (* Replace *)
@@ -168,7 +168,7 @@ let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) (original_s
   (* Count *)
   let replaced = ref false in
   let replace () =
-    if at_most_once then cassert (not !replaced) meta "T";
+    if at_most_once then cassert (not !replaced) meta "TODO: error message";
     replaced := true;
     nv
   in
@@ -191,7 +191,7 @@ let apply_symbolic_expansion_non_borrow (meta : Meta.meta) (config : config)
     (original_sv : symbolic_value) (expansion : symbolic_expansion)
     (ctx : eval_ctx) : eval_ctx =
   (* Apply the expansion to non-abstraction values *)
-  let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
+  let nv = symbolic_expansion_non_borrow_to_value meta original_sv expansion in
   let at_most_once = false in
   let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in
   (* Apply the expansion to abstraction values *)
@@ -215,7 +215,7 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (expand_e
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
   let def = ctx_lookup_type_decl ctx def_id in
-  cassert (List.length generics.regions = List.length def.generics.regions) meta "T";
+  cassert (List.length generics.regions = List.length def.generics.regions) meta "TODO: error message";
   (* Retrieve, for every variant, the list of its instantiated field types *)
   let variants_fields_types =
     AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes ctx def
@@ -228,7 +228,7 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (expand_e
   let initialize ((variant_id, field_types) : VariantId.id option * rty list) :
       symbolic_expansion =
     let field_values =
-      List.map (fun (ty : rty) -> mk_fresh_symbolic_value ty) field_types
+      List.map (fun (ty : rty) -> mk_fresh_symbolic_value meta ty) field_types
     in
     let see = SeAdt (variant_id, field_values) in
     see
@@ -236,19 +236,19 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (expand_e
   (* Initialize all the expanded values of all the variants *)
   List.map initialize variants_fields_types
 
-let compute_expanded_symbolic_tuple_value (field_types : rty list) :
+let compute_expanded_symbolic_tuple_value (meta : Meta.meta) (field_types : rty list) :
     symbolic_expansion =
   (* Generate the field values *)
   let field_values =
-    List.map (fun sv_ty -> mk_fresh_symbolic_value sv_ty) field_types
+    List.map (fun sv_ty -> mk_fresh_symbolic_value meta sv_ty) field_types
   in
   let variant_id = None in
   let see = SeAdt (variant_id, field_values) in
   see
 
-let compute_expanded_symbolic_box_value (boxed_ty : rty) : symbolic_expansion =
+let compute_expanded_symbolic_box_value (meta : Meta.meta) (boxed_ty : rty) : symbolic_expansion =
   (* Introduce a fresh symbolic value *)
-  let boxed_value = mk_fresh_symbolic_value boxed_ty in
+  let boxed_value = mk_fresh_symbolic_value meta boxed_ty in
   let see = SeAdt (None, [ boxed_value ]) in
   see
 
@@ -268,9 +268,9 @@ let compute_expanded_symbolic_adt_value (meta : Meta.meta) (expand_enumerations
   | TAdtId def_id, _, _ ->
       compute_expanded_symbolic_non_assumed_adt_value meta expand_enumerations def_id
         generics ctx
-  | TTuple, [], _ -> [ compute_expanded_symbolic_tuple_value generics.types ]
+  | TTuple, [], _ -> [ compute_expanded_symbolic_tuple_value meta generics.types ]
   | TAssumed TBox, [], [ boxed_ty ] ->
-      [ compute_expanded_symbolic_box_value boxed_ty ]
+      [ compute_expanded_symbolic_box_value meta boxed_ty ]
   | _ ->
       craise
         meta "compute_expanded_symbolic_adt_value: unexpected combination"
@@ -312,7 +312,7 @@ let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config)
     else None
   in
   (* The fresh symbolic value for the shared value *)
-  let shared_sv = mk_fresh_symbolic_value ref_ty in
+  let shared_sv = mk_fresh_symbolic_value meta ref_ty in
   (* Visitor to replace the projectors on borrows *)
   let obj =
     object (self)
@@ -325,7 +325,7 @@ let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config)
         else super#visit_VSymbolic env sv
 
       method! visit_EAbs proj_regions abs =
-        cassert (Option.is_none proj_regions) meta "T";
+        cassert (Option.is_none proj_regions) meta "TODO: error message";
         let proj_regions = Some abs.regions in
         super#visit_EAbs proj_regions abs
 
@@ -350,7 +350,7 @@ let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config)
       method! visit_aproj proj_regions aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
-            cassert (not (same_symbolic_id sv original_sv)) meta "T"
+            cassert (not (same_symbolic_id sv original_sv)) meta "TODO: error message"
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj proj_regions aproj
 
@@ -376,7 +376,7 @@ let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Finally, replace the projectors on loans *)
   let bids = !borrows in
-  cassert (not (BorrowId.Set.is_empty bids)) meta "T";
+  cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message";
   let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
@@ -394,20 +394,20 @@ let expand_symbolic_value_borrow (meta : Meta.meta) (config : config)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
     (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun =
  fun cf ctx ->
-  cassert (region <> RErased) meta "T";
+  cassert (region <> RErased) meta "TODO: error message";
   (* Check that we are allowed to expand the reference *)
-  cassert (not (region_in_set region ctx.ended_regions)) meta "T";
+  cassert (not (region_in_set region ctx.ended_regions)) meta "TODO: error message";
   (* Match on the reference kind *)
   match rkind with
   | RMut ->
       (* Simple case: simply create a fresh symbolic value and a fresh
        * borrow id *)
-      let sv = mk_fresh_symbolic_value ref_ty in
+      let sv = mk_fresh_symbolic_value meta ref_ty in
       let bid = fresh_borrow_id () in
       let see = SeMutRef (bid, sv) in
       (* Expand the symbolic values - we simply perform a substitution (and
        * check that we perform exactly one substitution) *)
-      let nv = symbolic_expansion_non_shared_borrow_to_value original_sv see in
+      let nv = symbolic_expansion_non_shared_borrow_to_value meta original_sv see in
       let at_most_once = true in
       let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in
       (* Expand the symbolic avalues *)
@@ -446,7 +446,7 @@ let apply_branching_symbolic_expansions_non_borrow (meta : Meta.meta) (config :
     (see_cf_l : (symbolic_expansion option * st_cm_fun) list)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
-  cassert (see_cf_l <> []) meta "T";
+  cassert (see_cf_l <> []) meta "TODO: error message";
   (* Apply the symbolic expansion in the context and call the continuation *)
   let resl =
     List.map
@@ -464,8 +464,8 @@ let apply_branching_symbolic_expansions_non_borrow (meta : Meta.meta) (config :
           (lazy
             ("apply_branching_symbolic_expansions_non_borrow: "
             ^ symbolic_value_to_string ctx0 sv
-            ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
-            ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
+            ^ "\n\n- original context:\n" ^ eval_ctx_to_string meta ctx0
+            ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
         (* Continuation *)
         cf_br cf_after_join ctx)
       see_cf_l
@@ -476,7 +476,7 @@ let apply_branching_symbolic_expansions_non_borrow (meta : Meta.meta) (config :
     match resl with
     | Some _ :: _ -> Some (List.map Option.get resl)
     | None :: _ ->
-        List.iter (fun res -> cassert (res = None) meta "T") resl;
+        List.iter (fun res -> cassert (res = None) meta "TODO: error message") resl;
         None
     | _ -> craise meta "Unreachable"
   in
@@ -492,7 +492,7 @@ let expand_symbolic_bool (meta : Meta.meta) (config : config) (sv : symbolic_val
   let original_sv = sv in
   let original_sv_place = sv_place in
   let rty = original_sv.sv_ty in
-  cassert (rty = TLiteral TBool) meta "T";
+  cassert (rty = TLiteral TBool) meta "TODO: error message";
   (* Expand the symbolic value to true or false and continue execution *)
   let see_true = SeLiteral (VBool true) in
   let see_false = SeLiteral (VBool false) in
@@ -554,10 +554,10 @@ let expand_symbolic_value_no_branching (meta : Meta.meta) (config : config) (sv
           (lazy
             ("expand_symbolic_value_no_branching: "
             ^ symbolic_value_to_string ctx0 sv
-            ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
-            ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
+            ^ "\n\n- original context:\n" ^ eval_ctx_to_string meta ctx0
+            ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
         (* Sanity check: the symbolic value has disappeared *)
-        cassert (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta "T")
+        cassert (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta "TODO: error message")
   in
   (* Continue *)
   cc cf ctx
@@ -594,7 +594,7 @@ let expand_symbolic_int (meta : Meta.meta) (config : config) (sv : symbolic_valu
     (tgts : (scalar_value * st_cm_fun) list) (otherwise : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
   (* Sanity check *)
-  cassert (sv.sv_ty = TLiteral (TInteger int_type)) meta "T";
+  cassert (sv.sv_ty = TLiteral (TInteger int_type)) meta "TODO: error message";
   (* For all the branches of the switch, we expand the symbolic value
    * to the value given by the branch and execute the branch statement.
    * For the otherwise branch, we leave the symbolic value as it is
-- 
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/InterpreterExpansion.ml | 54 ++++++++++++++++++++--------------------
 1 file changed, 27 insertions(+), 27 deletions(-)

(limited to 'compiler/InterpreterExpansion.ml')

diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 9448f3e8..2f886714 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -48,7 +48,7 @@ type proj_kind = LoanProj | BorrowProj
     Note that 2. and 3. may have a little bit of duplicated code, but hopefully
     it would make things clearer.
 *)
-let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : config)
+let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.meta)
     (allow_reborrows : bool) (proj_kind : proj_kind)
     (original_sv : symbolic_value) (expansion : symbolic_expansion)
     (ctx : eval_ctx) : eval_ctx =
@@ -56,7 +56,7 @@ let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : conf
   let check_symbolic_no_ended = false in
   (* Prepare reborrows registration *)
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows meta config allow_reborrows
+    prepare_reborrows config meta allow_reborrows
   in
   (* Visitor to apply the expansion *)
   let obj =
@@ -146,11 +146,11 @@ let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : conf
 (** Auxiliary function.
     Apply a symbolic expansion to avalues in a context.
 *)
-let apply_symbolic_expansion_to_avalues (meta : Meta.meta) (config : config)
+let apply_symbolic_expansion_to_avalues (config : config) (meta : Meta.meta)
     (allow_reborrows : bool) (original_sv : symbolic_value)
     (expansion : symbolic_expansion) (ctx : eval_ctx) : eval_ctx =
   let apply_expansion proj_kind ctx =
-    apply_symbolic_expansion_to_target_avalues meta config allow_reborrows proj_kind
+    apply_symbolic_expansion_to_target_avalues config meta allow_reborrows proj_kind
       original_sv expansion ctx
   in
   (* First target the loan projectors, then the borrow projectors *)
@@ -187,7 +187,7 @@ let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) (original_s
   (* Return *)
   ctx
 
-let apply_symbolic_expansion_non_borrow (meta : Meta.meta) (config : config)
+let apply_symbolic_expansion_non_borrow (config : config) (meta : Meta.meta)
     (original_sv : symbolic_value) (expansion : symbolic_expansion)
     (ctx : eval_ctx) : eval_ctx =
   (* Apply the expansion to non-abstraction values *)
@@ -196,7 +196,7 @@ let apply_symbolic_expansion_non_borrow (meta : Meta.meta) (config : config)
   let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in
   (* Apply the expansion to abstraction values *)
   let allow_reborrows = false in
-  apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv
+  apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv
     expansion ctx
 
 (** Compute the expansion of a non-assumed (i.e.: not [Box], etc.)
@@ -275,7 +275,7 @@ let compute_expanded_symbolic_adt_value (meta : Meta.meta) (expand_enumerations
       craise
         meta "compute_expanded_symbolic_adt_value: unexpected combination"
 
-let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config)
+let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
     (ref_ty : rty) : cm_fun =
  fun cf ctx ->
@@ -380,7 +380,7 @@ let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config)
   let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
-    apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv see
+    apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv see
       ctx
   in
   (* Call the continuation *)
@@ -390,7 +390,7 @@ let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config)
     expr
 
 (** TODO: simplify and merge with the other expansion function *)
-let expand_symbolic_value_borrow (meta : Meta.meta) (config : config)
+let expand_symbolic_value_borrow (config : config) (meta : Meta.meta)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
     (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun =
  fun cf ctx ->
@@ -413,7 +413,7 @@ let expand_symbolic_value_borrow (meta : Meta.meta) (config : config)
       (* Expand the symbolic avalues *)
       let allow_reborrows = true in
       let ctx =
-        apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv
+        apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv
           see ctx
       in
       (* Apply the continuation *)
@@ -422,7 +422,7 @@ let expand_symbolic_value_borrow (meta : Meta.meta) (config : config)
       S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place
         see expr
   | RShared ->
-      expand_symbolic_value_shared_borrow meta config original_sv original_sv_place
+      expand_symbolic_value_shared_borrow config meta original_sv original_sv_place
         ref_ty cf ctx
 
 (** A small helper.
@@ -441,7 +441,7 @@ let expand_symbolic_value_borrow (meta : Meta.meta) (config : config)
     We need this continuation separately (i.e., we can't compose it with the
     continuations in [see_cf_l]) because we perform a join *before* calling it.
 *)
-let apply_branching_symbolic_expansions_non_borrow (meta : Meta.meta) (config : config)
+let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Meta.meta)
     (sv : symbolic_value) (sv_place : SA.mplace option)
     (see_cf_l : (symbolic_expansion option * st_cm_fun) list)
     (cf_after_join : st_m_fun) : m_fun =
@@ -457,7 +457,7 @@ let apply_branching_symbolic_expansions_non_borrow (meta : Meta.meta) (config :
         let ctx =
           match see_opt with
           | None -> ctx
-          | Some see -> apply_symbolic_expansion_non_borrow meta config sv see ctx
+          | Some see -> apply_symbolic_expansion_non_borrow config meta sv see ctx
         in
         (* Debug *)
         log#ldebug
@@ -484,7 +484,7 @@ let apply_branching_symbolic_expansions_non_borrow (meta : Meta.meta) (config :
   let seel = List.map fst see_cf_l in
   S.synthesize_symbolic_expansion meta sv sv_place seel subterms
 
-let expand_symbolic_bool (meta : Meta.meta) (config : config) (sv : symbolic_value)
+let expand_symbolic_bool (config : config) (meta : Meta.meta) (sv : symbolic_value)
     (sv_place : SA.mplace option) (cf_true : st_cm_fun) (cf_false : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
@@ -498,10 +498,10 @@ let expand_symbolic_bool (meta : Meta.meta) (config : config) (sv : symbolic_val
   let see_false = SeLiteral (VBool false) in
   let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in
   (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *)
-  apply_branching_symbolic_expansions_non_borrow meta config original_sv
+  apply_branching_symbolic_expansions_non_borrow config meta original_sv
     original_sv_place seel cf_after_join ctx
 
-let expand_symbolic_value_no_branching (meta : Meta.meta) (config : config) (sv : symbolic_value)
+let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv : symbolic_value)
     (sv_place : SA.mplace option) : cm_fun =
  fun cf ctx ->
   (* Debug *)
@@ -530,7 +530,7 @@ let expand_symbolic_value_no_branching (meta : Meta.meta) (config : config) (sv
         let see = Collections.List.to_cons_nil seel in
         (* Apply in the context *)
         let ctx =
-          apply_symbolic_expansion_non_borrow meta config original_sv see ctx
+          apply_symbolic_expansion_non_borrow config meta original_sv see ctx
         in
         (* Call the continuation *)
         let expr = cf ctx in
@@ -539,7 +539,7 @@ let expand_symbolic_value_no_branching (meta : Meta.meta) (config : config) (sv
           original_sv_place see expr
     (* Borrows *)
     | TRef (region, ref_ty, rkind) ->
-        expand_symbolic_value_borrow meta config original_sv original_sv_place region
+        expand_symbolic_value_borrow config meta original_sv original_sv_place region
           ref_ty rkind cf ctx
     | _ ->
         craise
@@ -562,7 +562,7 @@ let expand_symbolic_value_no_branching (meta : Meta.meta) (config : config) (sv
   (* Continue *)
   cc cf ctx
 
-let expand_symbolic_adt (meta : Meta.meta) (config : config) (sv : symbolic_value)
+let expand_symbolic_adt (config : config) (meta : Meta.meta) (sv : symbolic_value)
     (sv_place : SA.mplace option) (cf_branches : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
@@ -584,12 +584,12 @@ let expand_symbolic_adt (meta : Meta.meta) (config : config) (sv : symbolic_valu
       in
       (* Apply *)
       let seel = List.map (fun see -> (Some see, cf_branches)) seel in
-      apply_branching_symbolic_expansions_non_borrow meta config original_sv
+      apply_branching_symbolic_expansions_non_borrow config meta original_sv
         original_sv_place seel cf_after_join ctx
   | _ ->
       craise meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty)
 
-let expand_symbolic_int (meta : Meta.meta) (config : config) (sv : symbolic_value)
+let expand_symbolic_int (config : config) (meta : Meta.meta) (sv : symbolic_value)
     (sv_place : SA.mplace option) (int_type : integer_type)
     (tgts : (scalar_value * st_cm_fun) list) (otherwise : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
@@ -609,7 +609,7 @@ let expand_symbolic_int (meta : Meta.meta) (config : config) (sv : symbolic_valu
   in
   let seel = List.append seel [ (None, otherwise) ] in
   (* Then expand and evaluate - this generates the proper symbolic AST *)
-  apply_branching_symbolic_expansions_non_borrow meta config sv sv_place seel
+  apply_branching_symbolic_expansions_non_borrow config meta sv sv_place seel
     cf_after_join
 
 (** Expand all the symbolic values which contain borrows.
@@ -620,7 +620,7 @@ let expand_symbolic_int (meta : Meta.meta) (config : config) (sv : symbolic_valu
     an enumeration with strictly more than one variant, a slice, etc.) or if
     we need to expand a recursive type (because this leads to looping).
  *)
-let greedy_expand_symbolics_with_borrows (meta : Meta.meta) (config : config) : cm_fun =
+let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : cm_fun =
  fun cf ctx ->
   (* The visitor object, to look for symbolic values in the concrete environment *)
   let obj =
@@ -677,10 +677,10 @@ let greedy_expand_symbolics_with_borrows (meta : Meta.meta) (config : config) :
                      (option [greedy_expand_symbolics_with_borrows] of \
                      [config]): "
                    ^ name_to_string ctx def.name)
-            else expand_symbolic_value_no_branching meta config sv None
+            else expand_symbolic_value_no_branching config meta sv None
         | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) ->
             (* Ok *)
-            expand_symbolic_value_no_branching meta config sv None
+            expand_symbolic_value_no_branching config meta sv None
         | TAdt (TAssumed (TArray | TSlice | TStr), _) ->
             (* We can't expand those *)
             craise
@@ -695,9 +695,9 @@ let greedy_expand_symbolics_with_borrows (meta : Meta.meta) (config : config) :
   (* Apply *)
   expand cf ctx
 
-let greedy_expand_symbolic_values (meta : Meta.meta) (config : config) : cm_fun =
+let greedy_expand_symbolic_values (config : config) (meta : Meta.meta) : cm_fun =
  fun cf ctx ->
   if Config.greedy_expand_symbolics_with_borrows then (
     log#ldebug (lazy "greedy_expand_symbolic_values");
-    greedy_expand_symbolics_with_borrows meta config cf ctx)
+    greedy_expand_symbolics_with_borrows config meta cf ctx)
   else cf ctx
-- 
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/InterpreterExpansion.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/InterpreterExpansion.ml')

diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 2f886714..086c0786 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -557,7 +557,7 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv
             ^ "\n\n- original context:\n" ^ eval_ctx_to_string meta ctx0
             ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
         (* Sanity check: the symbolic value has disappeared *)
-        cassert (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta "TODO: error message")
+        sanity_check (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta)
   in
   (* Continue *)
   cc cf ctx
@@ -594,7 +594,7 @@ let expand_symbolic_int (config : config) (meta : Meta.meta) (sv : symbolic_valu
     (tgts : (scalar_value * st_cm_fun) list) (otherwise : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
   (* Sanity check *)
-  cassert (sv.sv_ty = TLiteral (TInteger int_type)) meta "TODO: error message";
+  sanity_check (sv.sv_ty = TLiteral (TInteger int_type)) meta;
   (* For all the branches of the switch, we expand the symbolic value
    * to the value given by the branch and execute the branch statement.
    * For the otherwise branch, we leave the symbolic value as it is
-- 
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/InterpreterExpansion.ml | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

(limited to 'compiler/InterpreterExpansion.ml')

diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 086c0786..a2550e88 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -66,7 +66,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.me
       (** When visiting an abstraction, we remember the regions it owns to be
           able to properly reduce projectors when expanding symbolic values *)
       method! visit_abs current_abs abs =
-        cassert (Option.is_none current_abs) meta "TODO: error message";
+        sanity_check (Option.is_none current_abs) meta;
         let current_abs = Some abs in
         super#visit_abs current_abs abs
 
@@ -78,7 +78,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.me
       method! visit_aproj current_abs aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
-            cassert (not (same_symbolic_id sv original_sv)) meta "TODO: error message"
+            sanity_check (not (same_symbolic_id sv original_sv)) meta
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj current_abs aproj
 
@@ -98,7 +98,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.me
             (* Check if this is the symbolic value we are looking for *)
             if same_symbolic_id sv original_sv then (
               (* There mustn't be any given back values *)
-              cassert (given_back = []) meta "TODO: error message";
+              sanity_check (given_back = []) meta;
               (* Apply the projector *)
               let projected_value =
                 apply_proj_loans_on_symbolic_expansion meta proj_regions
@@ -168,7 +168,7 @@ let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) (original_s
   (* Count *)
   let replaced = ref false in
   let replace () =
-    if at_most_once then cassert (not !replaced) meta "TODO: error message";
+    if at_most_once then sanity_check (not !replaced) meta;
     replaced := true;
     nv
   in
@@ -215,10 +215,10 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (expand_e
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
   let def = ctx_lookup_type_decl ctx def_id in
-  cassert (List.length generics.regions = List.length def.generics.regions) meta "TODO: error message";
+  sanity_check (List.length generics.regions = List.length def.generics.regions) meta;
   (* Retrieve, for every variant, the list of its instantiated field types *)
   let variants_fields_types =
-    AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes ctx def
+    AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes meta ctx def
       generics
   in
   (* Check if there is strictly more than one variant *)
@@ -325,7 +325,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
         else super#visit_VSymbolic env sv
 
       method! visit_EAbs proj_regions abs =
-        cassert (Option.is_none proj_regions) meta "TODO: error message";
+        sanity_check (Option.is_none proj_regions) meta;
         let proj_regions = Some abs.regions in
         super#visit_EAbs proj_regions abs
 
@@ -350,7 +350,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
       method! visit_aproj proj_regions aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
-            cassert (not (same_symbolic_id sv original_sv)) meta "TODO: error message"
+            sanity_check (not (same_symbolic_id sv original_sv)) meta
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj proj_regions aproj
 
@@ -376,7 +376,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Finally, replace the projectors on loans *)
   let bids = !borrows in
-  cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message";
+  sanity_check (not (BorrowId.Set.is_empty bids)) meta;
   let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
@@ -394,9 +394,9 @@ let expand_symbolic_value_borrow (config : config) (meta : Meta.meta)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
     (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun =
  fun cf ctx ->
-  cassert (region <> RErased) meta "TODO: error message";
+  sanity_check (region <> RErased) meta;
   (* Check that we are allowed to expand the reference *)
-  cassert (not (region_in_set region ctx.ended_regions)) meta "TODO: error message";
+  sanity_check (not (region_in_set region ctx.ended_regions)) meta;
   (* Match on the reference kind *)
   match rkind with
   | RMut ->
@@ -446,7 +446,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Met
     (see_cf_l : (symbolic_expansion option * st_cm_fun) list)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
-  cassert (see_cf_l <> []) meta "TODO: error message";
+  sanity_check (see_cf_l <> []) meta;
   (* Apply the symbolic expansion in the context and call the continuation *)
   let resl =
     List.map
@@ -464,8 +464,8 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Met
           (lazy
             ("apply_branching_symbolic_expansions_non_borrow: "
             ^ symbolic_value_to_string ctx0 sv
-            ^ "\n\n- original context:\n" ^ eval_ctx_to_string meta ctx0
-            ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
+            ^ "\n\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0
+            ^ "\n\n- new context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
         (* Continuation *)
         cf_br cf_after_join ctx)
       see_cf_l
@@ -476,7 +476,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Met
     match resl with
     | Some _ :: _ -> Some (List.map Option.get resl)
     | None :: _ ->
-        List.iter (fun res -> cassert (res = None) meta "TODO: error message") resl;
+        List.iter (fun res -> sanity_check (res = None) meta) resl;
         None
     | _ -> craise meta "Unreachable"
   in
@@ -492,7 +492,7 @@ let expand_symbolic_bool (config : config) (meta : Meta.meta) (sv : symbolic_val
   let original_sv = sv in
   let original_sv_place = sv_place in
   let rty = original_sv.sv_ty in
-  cassert (rty = TLiteral TBool) meta "TODO: error message";
+  sanity_check (rty = TLiteral TBool) meta;
   (* Expand the symbolic value to true or false and continue execution *)
   let see_true = SeLiteral (VBool true) in
   let see_false = SeLiteral (VBool false) in
@@ -554,8 +554,8 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv
           (lazy
             ("expand_symbolic_value_no_branching: "
             ^ symbolic_value_to_string ctx0 sv
-            ^ "\n\n- original context:\n" ^ eval_ctx_to_string meta ctx0
-            ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
+            ^ "\n\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0
+            ^ "\n\n- new context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
         (* Sanity check: the symbolic value has disappeared *)
         sanity_check (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta)
   in
-- 
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/InterpreterExpansion.ml | 180 +++++++++++++++++++++------------------
 1 file changed, 97 insertions(+), 83 deletions(-)

(limited to 'compiler/InterpreterExpansion.ml')

diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index a2550e88..3e1aeef2 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -48,8 +48,8 @@ type proj_kind = LoanProj | BorrowProj
     Note that 2. and 3. may have a little bit of duplicated code, but hopefully
     it would make things clearer.
 *)
-let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.meta)
-    (allow_reborrows : bool) (proj_kind : proj_kind)
+let apply_symbolic_expansion_to_target_avalues (config : config)
+    (meta : Meta.meta) (allow_reborrows : bool) (proj_kind : proj_kind)
     (original_sv : symbolic_value) (expansion : symbolic_expansion)
     (ctx : eval_ctx) : eval_ctx =
   (* Symbolic values contained in the expansion might contain already ended regions *)
@@ -123,8 +123,9 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.me
               in
               (* Apply the projector *)
               let projected_value =
-                apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow
-                  proj_regions ancestors_regions expansion proj_ty
+                apply_proj_borrows meta check_symbolic_no_ended ctx
+                  fresh_reborrow proj_regions ancestors_regions expansion
+                  proj_ty
               in
               (* Replace *)
               projected_value.value
@@ -150,8 +151,8 @@ let apply_symbolic_expansion_to_avalues (config : config) (meta : Meta.meta)
     (allow_reborrows : bool) (original_sv : symbolic_value)
     (expansion : symbolic_expansion) (ctx : eval_ctx) : eval_ctx =
   let apply_expansion proj_kind ctx =
-    apply_symbolic_expansion_to_target_avalues config meta allow_reborrows proj_kind
-      original_sv expansion ctx
+    apply_symbolic_expansion_to_target_avalues config meta allow_reborrows
+      proj_kind original_sv expansion ctx
   in
   (* First target the loan projectors, then the borrow projectors *)
   let ctx = apply_expansion LoanProj ctx in
@@ -163,8 +164,8 @@ let apply_symbolic_expansion_to_avalues (config : config) (meta : Meta.meta)
     Simply replace the symbolic values (*not avalues*) in the context with
     a given value. Will break invariants if not used properly.
 *)
-let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) (original_sv : symbolic_value)
-    (nv : value) (ctx : eval_ctx) : eval_ctx =
+let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool)
+    (original_sv : symbolic_value) (nv : value) (ctx : eval_ctx) : eval_ctx =
   (* Count *)
   let replaced = ref false in
   let replace () =
@@ -193,7 +194,9 @@ let apply_symbolic_expansion_non_borrow (config : config) (meta : Meta.meta)
   (* Apply the expansion to non-abstraction values *)
   let nv = symbolic_expansion_non_borrow_to_value meta original_sv expansion in
   let at_most_once = false in
-  let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in
+  let ctx =
+    replace_symbolic_values meta at_most_once original_sv nv.value ctx
+  in
   (* Apply the expansion to abstraction values *)
   let allow_reborrows = false in
   apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv
@@ -209,13 +212,15 @@ let apply_symbolic_expansion_non_borrow (config : config) (meta : Meta.meta)
     [expand_enumerations] controls the expansion of enumerations: if false, it
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
-let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (expand_enumerations : bool)
-    (def_id : TypeDeclId.id) (generics : generic_args) (ctx : eval_ctx) :
-    symbolic_expansion list =
+let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta)
+    (expand_enumerations : bool) (def_id : TypeDeclId.id)
+    (generics : generic_args) (ctx : eval_ctx) : symbolic_expansion list =
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
   let def = ctx_lookup_type_decl ctx def_id in
-  sanity_check (List.length generics.regions = List.length def.generics.regions) meta;
+  sanity_check
+    (List.length generics.regions = List.length def.generics.regions)
+    meta;
   (* Retrieve, for every variant, the list of its instantiated field types *)
   let variants_fields_types =
     AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes meta ctx def
@@ -236,8 +241,8 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (expand_e
   (* Initialize all the expanded values of all the variants *)
   List.map initialize variants_fields_types
 
-let compute_expanded_symbolic_tuple_value (meta : Meta.meta) (field_types : rty list) :
-    symbolic_expansion =
+let compute_expanded_symbolic_tuple_value (meta : Meta.meta)
+    (field_types : rty list) : symbolic_expansion =
   (* Generate the field values *)
   let field_values =
     List.map (fun sv_ty -> mk_fresh_symbolic_value meta sv_ty) field_types
@@ -246,7 +251,8 @@ let compute_expanded_symbolic_tuple_value (meta : Meta.meta) (field_types : rty
   let see = SeAdt (variant_id, field_values) in
   see
 
-let compute_expanded_symbolic_box_value (meta : Meta.meta) (boxed_ty : rty) : symbolic_expansion =
+let compute_expanded_symbolic_box_value (meta : Meta.meta) (boxed_ty : rty) :
+    symbolic_expansion =
   (* Introduce a fresh symbolic value *)
   let boxed_value = mk_fresh_symbolic_value meta boxed_ty in
   let see = SeAdt (None, [ boxed_value ]) in
@@ -261,19 +267,19 @@ let compute_expanded_symbolic_box_value (meta : Meta.meta) (boxed_ty : rty) : sy
     [expand_enumerations] controls the expansion of enumerations: if [false], it
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
-let compute_expanded_symbolic_adt_value (meta : Meta.meta) (expand_enumerations : bool)
-    (adt_id : type_id) (generics : generic_args) (ctx : eval_ctx) :
-    symbolic_expansion list =
+let compute_expanded_symbolic_adt_value (meta : Meta.meta)
+    (expand_enumerations : bool) (adt_id : type_id) (generics : generic_args)
+    (ctx : eval_ctx) : symbolic_expansion list =
   match (adt_id, generics.regions, generics.types) with
   | TAdtId def_id, _, _ ->
-      compute_expanded_symbolic_non_assumed_adt_value meta expand_enumerations def_id
-        generics ctx
-  | TTuple, [], _ -> [ compute_expanded_symbolic_tuple_value meta generics.types ]
+      compute_expanded_symbolic_non_assumed_adt_value meta expand_enumerations
+        def_id generics ctx
+  | TTuple, [], _ ->
+      [ compute_expanded_symbolic_tuple_value meta generics.types ]
   | TAssumed TBox, [], [ boxed_ty ] ->
       [ compute_expanded_symbolic_box_value meta boxed_ty ]
   | _ ->
-      craise
-        meta "compute_expanded_symbolic_adt_value: unexpected combination"
+      craise meta "compute_expanded_symbolic_adt_value: unexpected combination"
 
 let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
@@ -380,14 +386,14 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
   let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
-    apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv see
-      ctx
+    apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv
+      see ctx
   in
   (* Call the continuation *)
   let expr = cf ctx in
   (* Update the synthesized program *)
-  S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place see
-    expr
+  S.synthesize_symbolic_expansion_no_branching meta original_sv
+    original_sv_place see expr
 
 (** TODO: simplify and merge with the other expansion function *)
 let expand_symbolic_value_borrow (config : config) (meta : Meta.meta)
@@ -407,23 +413,27 @@ let expand_symbolic_value_borrow (config : config) (meta : Meta.meta)
       let see = SeMutRef (bid, sv) in
       (* Expand the symbolic values - we simply perform a substitution (and
        * check that we perform exactly one substitution) *)
-      let nv = symbolic_expansion_non_shared_borrow_to_value meta original_sv see in
+      let nv =
+        symbolic_expansion_non_shared_borrow_to_value meta original_sv see
+      in
       let at_most_once = true in
-      let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in
+      let ctx =
+        replace_symbolic_values meta at_most_once original_sv nv.value ctx
+      in
       (* Expand the symbolic avalues *)
       let allow_reborrows = true in
       let ctx =
-        apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv
-          see ctx
+        apply_symbolic_expansion_to_avalues config meta allow_reborrows
+          original_sv see ctx
       in
       (* Apply the continuation *)
       let expr = cf ctx in
       (* Update the synthesized program *)
-      S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place
-        see expr
+      S.synthesize_symbolic_expansion_no_branching meta original_sv
+        original_sv_place see expr
   | RShared ->
-      expand_symbolic_value_shared_borrow config meta original_sv original_sv_place
-        ref_ty cf ctx
+      expand_symbolic_value_shared_borrow config meta original_sv
+        original_sv_place ref_ty cf ctx
 
 (** A small helper.
 
@@ -441,8 +451,8 @@ let expand_symbolic_value_borrow (config : config) (meta : Meta.meta)
     We need this continuation separately (i.e., we can't compose it with the
     continuations in [see_cf_l]) because we perform a join *before* calling it.
 *)
-let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Meta.meta)
-    (sv : symbolic_value) (sv_place : SA.mplace option)
+let apply_branching_symbolic_expansions_non_borrow (config : config)
+    (meta : Meta.meta) (sv : symbolic_value) (sv_place : SA.mplace option)
     (see_cf_l : (symbolic_expansion option * st_cm_fun) list)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
@@ -457,15 +467,19 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Met
         let ctx =
           match see_opt with
           | None -> ctx
-          | Some see -> apply_symbolic_expansion_non_borrow config meta sv see ctx
+          | Some see ->
+              apply_symbolic_expansion_non_borrow config meta sv see ctx
         in
         (* Debug *)
         log#ldebug
           (lazy
             ("apply_branching_symbolic_expansions_non_borrow: "
             ^ symbolic_value_to_string ctx0 sv
-            ^ "\n\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0
-            ^ "\n\n- new context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
+            ^ "\n\n- original context:\n"
+            ^ eval_ctx_to_string ~meta:(Some meta) ctx0
+            ^ "\n\n- new context:\n"
+            ^ eval_ctx_to_string ~meta:(Some meta) ctx
+            ^ "\n"));
         (* Continuation *)
         cf_br cf_after_join ctx)
       see_cf_l
@@ -484,9 +498,9 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Met
   let seel = List.map fst see_cf_l in
   S.synthesize_symbolic_expansion meta sv sv_place seel subterms
 
-let expand_symbolic_bool (config : config) (meta : Meta.meta) (sv : symbolic_value)
-    (sv_place : SA.mplace option) (cf_true : st_cm_fun) (cf_false : st_cm_fun)
-    (cf_after_join : st_m_fun) : m_fun =
+let expand_symbolic_bool (config : config) (meta : Meta.meta)
+    (sv : symbolic_value) (sv_place : SA.mplace option) (cf_true : st_cm_fun)
+    (cf_false : st_cm_fun) (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
   (* Compute the expanded value *)
   let original_sv = sv in
@@ -501,8 +515,8 @@ let expand_symbolic_bool (config : config) (meta : Meta.meta) (sv : symbolic_val
   apply_branching_symbolic_expansions_non_borrow config meta original_sv
     original_sv_place seel cf_after_join ctx
 
-let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv : symbolic_value)
-    (sv_place : SA.mplace option) : cm_fun =
+let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta)
+    (sv : symbolic_value) (sv_place : SA.mplace option) : cm_fun =
  fun cf ctx ->
   (* Debug *)
   log#ldebug
@@ -523,8 +537,8 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv
         (* Compute the expanded value *)
         let allow_branching = false in
         let seel =
-          compute_expanded_symbolic_adt_value meta allow_branching adt_id generics
-            ctx
+          compute_expanded_symbolic_adt_value meta allow_branching adt_id
+            generics ctx
         in
         (* There should be exacly one branch *)
         let see = Collections.List.to_cons_nil seel in
@@ -539,13 +553,12 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv
           original_sv_place see expr
     (* Borrows *)
     | TRef (region, ref_ty, rkind) ->
-        expand_symbolic_value_borrow config meta original_sv original_sv_place region
-          ref_ty rkind cf ctx
+        expand_symbolic_value_borrow config meta original_sv original_sv_place
+          region ref_ty rkind cf ctx
     | _ ->
-        craise
-          meta
-             ("expand_symbolic_value_no_branching: unexpected type: "
-            ^ show_rty rty)
+        craise meta
+          ("expand_symbolic_value_no_branching: unexpected type: "
+         ^ show_rty rty)
   in
   (* Debug *)
   let cc =
@@ -554,17 +567,20 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv
           (lazy
             ("expand_symbolic_value_no_branching: "
             ^ symbolic_value_to_string ctx0 sv
-            ^ "\n\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0
-            ^ "\n\n- new context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
+            ^ "\n\n- original context:\n"
+            ^ eval_ctx_to_string ~meta:(Some meta) ctx0
+            ^ "\n\n- new context:\n"
+            ^ eval_ctx_to_string ~meta:(Some meta) ctx
+            ^ "\n"));
         (* Sanity check: the symbolic value has disappeared *)
         sanity_check (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta)
   in
   (* Continue *)
   cc cf ctx
 
-let expand_symbolic_adt (config : config) (meta : Meta.meta) (sv : symbolic_value)
-    (sv_place : SA.mplace option) (cf_branches : st_cm_fun)
-    (cf_after_join : st_m_fun) : m_fun =
+let expand_symbolic_adt (config : config) (meta : Meta.meta)
+    (sv : symbolic_value) (sv_place : SA.mplace option)
+    (cf_branches : st_cm_fun) (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
   (* Debug *)
   log#ldebug (lazy ("expand_symbolic_adt:" ^ symbolic_value_to_string ctx sv));
@@ -580,19 +596,19 @@ let expand_symbolic_adt (config : config) (meta : Meta.meta) (sv : symbolic_valu
       let allow_branching = true in
       (* Compute the expanded value *)
       let seel =
-        compute_expanded_symbolic_adt_value meta allow_branching adt_id generics ctx
+        compute_expanded_symbolic_adt_value meta allow_branching adt_id generics
+          ctx
       in
       (* Apply *)
       let seel = List.map (fun see -> (Some see, cf_branches)) seel in
       apply_branching_symbolic_expansions_non_borrow config meta original_sv
         original_sv_place seel cf_after_join ctx
-  | _ ->
-      craise meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty)
+  | _ -> craise meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty)
 
-let expand_symbolic_int (config : config) (meta : Meta.meta) (sv : symbolic_value)
-    (sv_place : SA.mplace option) (int_type : integer_type)
-    (tgts : (scalar_value * st_cm_fun) list) (otherwise : st_cm_fun)
-    (cf_after_join : st_m_fun) : m_fun =
+let expand_symbolic_int (config : config) (meta : Meta.meta)
+    (sv : symbolic_value) (sv_place : SA.mplace option)
+    (int_type : integer_type) (tgts : (scalar_value * st_cm_fun) list)
+    (otherwise : st_cm_fun) (cf_after_join : st_m_fun) : m_fun =
   (* Sanity check *)
   sanity_check (sv.sv_ty = TLiteral (TInteger int_type)) meta;
   (* For all the branches of the switch, we expand the symbolic value
@@ -620,7 +636,8 @@ let expand_symbolic_int (config : config) (meta : Meta.meta) (sv : symbolic_valu
     an enumeration with strictly more than one variant, a slice, etc.) or if
     we need to expand a recursive type (because this leads to looping).
  *)
-let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : cm_fun =
+let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) :
+    cm_fun =
  fun cf ctx ->
   (* The visitor object, to look for symbolic values in the concrete environment *)
   let obj =
@@ -661,31 +678,27 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) :
             (match def.kind with
             | Struct _ | Enum ([] | [ _ ]) -> ()
             | Enum (_ :: _) ->
-                craise
-                  meta
-                     ("Attempted to greedily expand a symbolic enumeration \
-                       with > 1 variants (option \
-                       [greedy_expand_symbolics_with_borrows] of [config]): "
-                     ^ name_to_string ctx def.name)
+                craise meta
+                  ("Attempted to greedily expand a symbolic enumeration with > \
+                    1 variants (option [greedy_expand_symbolics_with_borrows] \
+                    of [config]): "
+                  ^ name_to_string ctx def.name)
             | Opaque ->
                 craise meta "Attempted to greedily expand an opaque type");
             (* Also, we need to check if the definition is recursive *)
             if ctx_type_decl_is_rec ctx def_id then
-              craise
-                meta
-                   ("Attempted to greedily expand a recursive definition \
-                     (option [greedy_expand_symbolics_with_borrows] of \
-                     [config]): "
-                   ^ name_to_string ctx def.name)
+              craise meta
+                ("Attempted to greedily expand a recursive definition (option \
+                  [greedy_expand_symbolics_with_borrows] of [config]): "
+                ^ name_to_string ctx def.name)
             else expand_symbolic_value_no_branching config meta sv None
         | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) ->
             (* Ok *)
             expand_symbolic_value_no_branching config meta sv None
         | TAdt (TAssumed (TArray | TSlice | TStr), _) ->
             (* We can't expand those *)
-            craise
-              meta
-                 "Attempted to greedily expand an ADT which can't be expanded "
+            craise meta
+              "Attempted to greedily expand an ADT which can't be expanded "
         | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ ->
             craise meta "Unreachable"
       in
@@ -695,7 +708,8 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) :
   (* Apply *)
   expand cf ctx
 
-let greedy_expand_symbolic_values (config : config) (meta : Meta.meta) : cm_fun =
+let greedy_expand_symbolic_values (config : config) (meta : Meta.meta) : cm_fun
+    =
  fun cf ctx ->
   if Config.greedy_expand_symbolics_with_borrows then (
     log#ldebug (lazy "greedy_expand_symbolic_values");
-- 
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/InterpreterExpansion.ml | 52 ++++++++++++++++++++--------------------
 1 file changed, 26 insertions(+), 26 deletions(-)

(limited to 'compiler/InterpreterExpansion.ml')

diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 3e1aeef2..0b7c071e 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -66,7 +66,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
       (** When visiting an abstraction, we remember the regions it owns to be
           able to properly reduce projectors when expanding symbolic values *)
       method! visit_abs current_abs abs =
-        sanity_check (Option.is_none current_abs) meta;
+        sanity_check __FILE__ __LINE__ (Option.is_none current_abs) meta;
         let current_abs = Some abs in
         super#visit_abs current_abs abs
 
@@ -78,7 +78,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
       method! visit_aproj current_abs aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
-            sanity_check (not (same_symbolic_id sv original_sv)) meta
+            sanity_check __FILE__ __LINE__ (not (same_symbolic_id sv original_sv)) meta
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj current_abs aproj
 
@@ -98,7 +98,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
             (* Check if this is the symbolic value we are looking for *)
             if same_symbolic_id sv original_sv then (
               (* There mustn't be any given back values *)
-              sanity_check (given_back = []) meta;
+              sanity_check __FILE__ __LINE__ (given_back = []) meta;
               (* Apply the projector *)
               let projected_value =
                 apply_proj_loans_on_symbolic_expansion meta proj_regions
@@ -169,7 +169,7 @@ let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool)
   (* Count *)
   let replaced = ref false in
   let replace () =
-    if at_most_once then sanity_check (not !replaced) meta;
+    if at_most_once then sanity_check __FILE__ __LINE__ (not !replaced) meta;
     replaced := true;
     nv
   in
@@ -218,7 +218,7 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta)
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
   let def = ctx_lookup_type_decl ctx def_id in
-  sanity_check
+  sanity_check __FILE__ __LINE__
     (List.length generics.regions = List.length def.generics.regions)
     meta;
   (* Retrieve, for every variant, the list of its instantiated field types *)
@@ -228,7 +228,7 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta)
   in
   (* Check if there is strictly more than one variant *)
   if List.length variants_fields_types > 1 && not expand_enumerations then
-    craise meta "Not allowed to expand enumerations with several variants";
+    craise __FILE__ __LINE__ meta "Not allowed to expand enumerations with several variants";
   (* Initialize the expanded value for a given variant *)
   let initialize ((variant_id, field_types) : VariantId.id option * rty list) :
       symbolic_expansion =
@@ -279,7 +279,7 @@ let compute_expanded_symbolic_adt_value (meta : Meta.meta)
   | TAssumed TBox, [], [ boxed_ty ] ->
       [ compute_expanded_symbolic_box_value meta boxed_ty ]
   | _ ->
-      craise meta "compute_expanded_symbolic_adt_value: unexpected combination"
+      craise __FILE__ __LINE__ meta "compute_expanded_symbolic_adt_value: unexpected combination"
 
 let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
@@ -314,7 +314,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
             Some [ AsbBorrow bid; shared_asb ]
           else (* Not in the set: ignore *)
             Some [ shared_asb ]
-      | _ -> craise meta "Unexpected"
+      | _ -> craise __FILE__ __LINE__ meta "Unexpected"
     else None
   in
   (* The fresh symbolic value for the shared value *)
@@ -331,7 +331,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
         else super#visit_VSymbolic env sv
 
       method! visit_EAbs proj_regions abs =
-        sanity_check (Option.is_none proj_regions) meta;
+        sanity_check __FILE__ __LINE__ (Option.is_none proj_regions) meta;
         let proj_regions = Some abs.regions in
         super#visit_EAbs proj_regions abs
 
@@ -356,7 +356,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
       method! visit_aproj proj_regions aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
-            sanity_check (not (same_symbolic_id sv original_sv)) meta
+            sanity_check __FILE__ __LINE__ (not (same_symbolic_id sv original_sv)) meta
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj proj_regions aproj
 
@@ -382,7 +382,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Finally, replace the projectors on loans *)
   let bids = !borrows in
-  sanity_check (not (BorrowId.Set.is_empty bids)) meta;
+  sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) meta;
   let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
@@ -400,9 +400,9 @@ let expand_symbolic_value_borrow (config : config) (meta : Meta.meta)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
     (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun =
  fun cf ctx ->
-  sanity_check (region <> RErased) meta;
+  sanity_check __FILE__ __LINE__ (region <> RErased) meta;
   (* Check that we are allowed to expand the reference *)
-  sanity_check (not (region_in_set region ctx.ended_regions)) meta;
+  sanity_check __FILE__ __LINE__ (not (region_in_set region ctx.ended_regions)) meta;
   (* Match on the reference kind *)
   match rkind with
   | RMut ->
@@ -456,7 +456,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : config)
     (see_cf_l : (symbolic_expansion option * st_cm_fun) list)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
-  sanity_check (see_cf_l <> []) meta;
+  sanity_check __FILE__ __LINE__ (see_cf_l <> []) meta;
   (* Apply the symbolic expansion in the context and call the continuation *)
   let resl =
     List.map
@@ -490,9 +490,9 @@ let apply_branching_symbolic_expansions_non_borrow (config : config)
     match resl with
     | Some _ :: _ -> Some (List.map Option.get resl)
     | None :: _ ->
-        List.iter (fun res -> sanity_check (res = None) meta) resl;
+        List.iter (fun res -> sanity_check __FILE__ __LINE__ (res = None) meta) resl;
         None
-    | _ -> craise meta "Unreachable"
+    | _ -> craise __FILE__ __LINE__ meta "Unreachable"
   in
   (* Synthesize and return *)
   let seel = List.map fst see_cf_l in
@@ -506,7 +506,7 @@ let expand_symbolic_bool (config : config) (meta : Meta.meta)
   let original_sv = sv in
   let original_sv_place = sv_place in
   let rty = original_sv.sv_ty in
-  sanity_check (rty = TLiteral TBool) meta;
+  sanity_check __FILE__ __LINE__ (rty = TLiteral TBool) meta;
   (* Expand the symbolic value to true or false and continue execution *)
   let see_true = SeLiteral (VBool true) in
   let see_false = SeLiteral (VBool false) in
@@ -556,7 +556,7 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta)
         expand_symbolic_value_borrow config meta original_sv original_sv_place
           region ref_ty rkind cf ctx
     | _ ->
-        craise meta
+        craise __FILE__ __LINE__ meta
           ("expand_symbolic_value_no_branching: unexpected type: "
          ^ show_rty rty)
   in
@@ -573,7 +573,7 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta)
             ^ eval_ctx_to_string ~meta:(Some meta) ctx
             ^ "\n"));
         (* Sanity check: the symbolic value has disappeared *)
-        sanity_check (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta)
+        sanity_check __FILE__ __LINE__ (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta)
   in
   (* Continue *)
   cc cf ctx
@@ -603,14 +603,14 @@ let expand_symbolic_adt (config : config) (meta : Meta.meta)
       let seel = List.map (fun see -> (Some see, cf_branches)) seel in
       apply_branching_symbolic_expansions_non_borrow config meta original_sv
         original_sv_place seel cf_after_join ctx
-  | _ -> craise meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty)
+  | _ -> craise __FILE__ __LINE__ meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty)
 
 let expand_symbolic_int (config : config) (meta : Meta.meta)
     (sv : symbolic_value) (sv_place : SA.mplace option)
     (int_type : integer_type) (tgts : (scalar_value * st_cm_fun) list)
     (otherwise : st_cm_fun) (cf_after_join : st_m_fun) : m_fun =
   (* Sanity check *)
-  sanity_check (sv.sv_ty = TLiteral (TInteger int_type)) meta;
+  sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral (TInteger int_type)) meta;
   (* For all the branches of the switch, we expand the symbolic value
    * to the value given by the branch and execute the branch statement.
    * For the otherwise branch, we leave the symbolic value as it is
@@ -678,16 +678,16 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) :
             (match def.kind with
             | Struct _ | Enum ([] | [ _ ]) -> ()
             | Enum (_ :: _) ->
-                craise meta
+                craise __FILE__ __LINE__ meta
                   ("Attempted to greedily expand a symbolic enumeration with > \
                     1 variants (option [greedy_expand_symbolics_with_borrows] \
                     of [config]): "
                   ^ name_to_string ctx def.name)
             | Opaque ->
-                craise meta "Attempted to greedily expand an opaque type");
+                craise __FILE__ __LINE__ meta "Attempted to greedily expand an opaque type");
             (* Also, we need to check if the definition is recursive *)
             if ctx_type_decl_is_rec ctx def_id then
-              craise meta
+              craise __FILE__ __LINE__ meta
                 ("Attempted to greedily expand a recursive definition (option \
                   [greedy_expand_symbolics_with_borrows] of [config]): "
                 ^ name_to_string ctx def.name)
@@ -697,10 +697,10 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) :
             expand_symbolic_value_no_branching config meta sv None
         | TAdt (TAssumed (TArray | TSlice | TStr), _) ->
             (* We can't expand those *)
-            craise meta
+            craise __FILE__ __LINE__ meta
               "Attempted to greedily expand an ADT which can't be expanded "
         | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ ->
-            craise meta "Unreachable"
+            craise __FILE__ __LINE__ meta "Unreachable"
       in
       (* Compose and continue *)
       comp cc expand cf ctx
-- 
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/InterpreterExpansion.ml | 33 ++++++++++++++++++++++++---------
 1 file changed, 24 insertions(+), 9 deletions(-)

(limited to 'compiler/InterpreterExpansion.ml')

diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 0b7c071e..e47fbfbe 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -78,7 +78,9 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
       method! visit_aproj current_abs aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
-            sanity_check __FILE__ __LINE__ (not (same_symbolic_id sv original_sv)) meta
+            sanity_check __FILE__ __LINE__
+              (not (same_symbolic_id sv original_sv))
+              meta
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj current_abs aproj
 
@@ -228,7 +230,8 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta)
   in
   (* Check if there is strictly more than one variant *)
   if List.length variants_fields_types > 1 && not expand_enumerations then
-    craise __FILE__ __LINE__ meta "Not allowed to expand enumerations with several variants";
+    craise __FILE__ __LINE__ meta
+      "Not allowed to expand enumerations with several variants";
   (* Initialize the expanded value for a given variant *)
   let initialize ((variant_id, field_types) : VariantId.id option * rty list) :
       symbolic_expansion =
@@ -279,7 +282,8 @@ let compute_expanded_symbolic_adt_value (meta : Meta.meta)
   | TAssumed TBox, [], [ boxed_ty ] ->
       [ compute_expanded_symbolic_box_value meta boxed_ty ]
   | _ ->
-      craise __FILE__ __LINE__ meta "compute_expanded_symbolic_adt_value: unexpected combination"
+      craise __FILE__ __LINE__ meta
+        "compute_expanded_symbolic_adt_value: unexpected combination"
 
 let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
@@ -356,7 +360,9 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
       method! visit_aproj proj_regions aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
-            sanity_check __FILE__ __LINE__ (not (same_symbolic_id sv original_sv)) meta
+            sanity_check __FILE__ __LINE__
+              (not (same_symbolic_id sv original_sv))
+              meta
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj proj_regions aproj
 
@@ -402,7 +408,9 @@ let expand_symbolic_value_borrow (config : config) (meta : Meta.meta)
  fun cf ctx ->
   sanity_check __FILE__ __LINE__ (region <> RErased) meta;
   (* Check that we are allowed to expand the reference *)
-  sanity_check __FILE__ __LINE__ (not (region_in_set region ctx.ended_regions)) meta;
+  sanity_check __FILE__ __LINE__
+    (not (region_in_set region ctx.ended_regions))
+    meta;
   (* Match on the reference kind *)
   match rkind with
   | RMut ->
@@ -490,7 +498,9 @@ let apply_branching_symbolic_expansions_non_borrow (config : config)
     match resl with
     | Some _ :: _ -> Some (List.map Option.get resl)
     | None :: _ ->
-        List.iter (fun res -> sanity_check __FILE__ __LINE__ (res = None) meta) resl;
+        List.iter
+          (fun res -> sanity_check __FILE__ __LINE__ (res = None) meta)
+          resl;
         None
     | _ -> craise __FILE__ __LINE__ meta "Unreachable"
   in
@@ -573,7 +583,9 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta)
             ^ eval_ctx_to_string ~meta:(Some meta) ctx
             ^ "\n"));
         (* Sanity check: the symbolic value has disappeared *)
-        sanity_check __FILE__ __LINE__ (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta)
+        sanity_check __FILE__ __LINE__
+          (not (symbolic_value_id_in_ctx original_sv.sv_id ctx))
+          meta)
   in
   (* Continue *)
   cc cf ctx
@@ -603,7 +615,9 @@ let expand_symbolic_adt (config : config) (meta : Meta.meta)
       let seel = List.map (fun see -> (Some see, cf_branches)) seel in
       apply_branching_symbolic_expansions_non_borrow config meta original_sv
         original_sv_place seel cf_after_join ctx
-  | _ -> craise __FILE__ __LINE__ meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty)
+  | _ ->
+      craise __FILE__ __LINE__ meta
+        ("expand_symbolic_adt: unexpected type: " ^ show_rty rty)
 
 let expand_symbolic_int (config : config) (meta : Meta.meta)
     (sv : symbolic_value) (sv_place : SA.mplace option)
@@ -684,7 +698,8 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) :
                     of [config]): "
                   ^ name_to_string ctx def.name)
             | Opaque ->
-                craise __FILE__ __LINE__ meta "Attempted to greedily expand an opaque type");
+                craise __FILE__ __LINE__ meta
+                  "Attempted to greedily expand an opaque type");
             (* Also, we need to check if the definition is recursive *)
             if ctx_type_decl_is_rec ctx def_id then
               craise __FILE__ __LINE__ meta
-- 
cgit v1.2.3