Fix a minor issue when values are moved in the loops

compiler/Contexts.ml

@@ -153,6 +153,7 @@ and env_elem =
 and env = env_elem list
 [@@deriving
   show,
+    ord,
     visitors
       {
         name = "iter_env";
@@ -170,6 +171,17 @@ and env = env_elem list
         concrete = true;
       }]
 
+module OrderedBinder : Collections.OrderedType with type t = binder = struct
+  type t = binder
+
+  let compare x y = compare_binder x y
+  let to_string x = show_binder x
+  let pp_t fmt x = Format.pp_print_string fmt (show_binder x)
+  let show_t x = show_binder x
+end
+
+module BinderMap = Collections.MakeMap (OrderedBinder)
+
 type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show]
 
 type config = {
@@ -394,6 +406,13 @@ let ctx_push_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) (v : typed_value)
     : eval_ctx =
   { ctx with env = EBinding (BDummy vid, v) :: ctx.env }
 
+let ctx_push_fresh_dummy_var (ctx : eval_ctx) (v : typed_value) : eval_ctx =
+  ctx_push_dummy_var ctx (fresh_dummy_var_id ()) v
+
+let ctx_push_fresh_dummy_vars (ctx : eval_ctx) (vl : typed_value list) :
+    eval_ctx =
+  List.fold_left (fun ctx v -> ctx_push_fresh_dummy_var ctx v) ctx vl
+
 (** Remove a dummy variable from a context's environment. *)
 let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
     eval_ctx * typed_value =

compiler/InterpreterLoops.ml

@@ -93,10 +93,20 @@ let eval_loop_symbolic (config : config) (meta : meta)
   let fp_bl_corresp =
     compute_fixed_point_id_correspondance fixed_ids ctx fp_ctx
   in
-  let end_expr =
+  log#ldebug
+    (lazy
+      ("eval_loop_symbolic: about to match the fixed-point context with the \
+        original context:\n\
+        - src ctx (fixed-point ctx)" ^ eval_ctx_to_string fp_ctx
+     ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx));
+  let end_expr : SymbolicAst.expression option =
     match_ctx_with_target config loop_id true fp_bl_corresp fp_input_svalues
       fixed_ids fp_ctx cf ctx
   in
+  log#ldebug
+    (lazy
+      "eval_loop_symbolic: matched the fixed-point context with the original \
+       context");
 
   (* Synthesize the loop body by evaluating it, with the continuation for
      after the loop starting at the *fixed point*, but with a special
@@ -115,6 +125,12 @@ let eval_loop_symbolic (config : config) (meta : meta)
     | Continue i ->
         (* We don't support nested loops for now *)
         assert (i = 0);
+        log#ldebug
+          (lazy
+            ("eval_loop_symbolic: about to match the fixed-point context with \
+              the context at a continue:\n\
+              - src ctx (fixed-point ctx)" ^ eval_ctx_to_string fp_ctx
+           ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string ctx));
         let cc =
           match_ctx_with_target config loop_id false fp_bl_corresp
             fp_input_svalues fixed_ids fp_ctx

compiler/InterpreterLoopsCore.ml

@@ -45,16 +45,22 @@ type abs_borrows_loans_maps = {
 
     This module contains primitive match functions to instantiate the generic
     {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} functor.
-  *)
+
+    Remark: all the functions receive as input the left context and the right context.
+    This is useful for printing, lookups, and also in order to check the ended
+    regions.
+ *)
 module type PrimMatcher = sig
-  val match_etys : ety -> ety -> ety
-  val match_rtys : rty -> rty -> rty
+  val match_etys : eval_ctx -> eval_ctx -> ety -> ety -> ety
+  val match_rtys : eval_ctx -> eval_ctx -> rty -> rty -> rty
 
   (** The input primitive values are not equal *)
-  val match_distinct_literals : ety -> literal -> literal -> typed_value
+  val match_distinct_literals :
+    eval_ctx -> eval_ctx -> ety -> literal -> literal -> typed_value
 
   (** The input ADTs don't have the same variant *)
-  val match_distinct_adts : ety -> adt_value -> adt_value -> typed_value
+  val match_distinct_adts :
+    eval_ctx -> eval_ctx -> ety -> adt_value -> adt_value -> typed_value
 
   (** The meta-value is the result of a match.
 
@@ -67,6 +73,8 @@ module type PrimMatcher = sig
       calling the match function.
    *)
   val match_shared_borrows :
+    eval_ctx ->
+    eval_ctx ->
     (typed_value -> typed_value -> typed_value) ->
     ety ->
     borrow_id ->
@@ -82,6 +90,8 @@ module type PrimMatcher = sig
       - [bv]: the result of matching [bv0] with [bv1]
   *)
   val match_mut_borrows :
+    eval_ctx ->
+    eval_ctx ->
     ety ->
     borrow_id ->
     typed_value ->
@@ -97,16 +107,20 @@ module type PrimMatcher = sig
       [v]: the result of matching the shared values coming from the two loans
    *)
   val match_shared_loans :
+    eval_ctx ->
+    eval_ctx ->
     ety ->
     loan_id_set ->
     loan_id_set ->
     typed_value ->
     loan_id_set * typed_value
 
-  val match_mut_loans : ety -> loan_id -> loan_id -> loan_id
+  val match_mut_loans :
+    eval_ctx -> eval_ctx -> ety -> loan_id -> loan_id -> loan_id
 
   (** There are no constraints on the input symbolic values *)
-  val match_symbolic_values : symbolic_value -> symbolic_value -> symbolic_value
+  val match_symbolic_values :
+    eval_ctx -> eval_ctx -> symbolic_value -> symbolic_value -> symbolic_value
 
   (** Match a symbolic value with a value which is not symbolic.
 
@@ -116,7 +130,7 @@ module type PrimMatcher = sig
       end loans in one of the two environments).
    *)
   val match_symbolic_with_other :
-    bool -> symbolic_value -> typed_value -> typed_value
+    eval_ctx -> eval_ctx -> bool -> symbolic_value -> typed_value -> typed_value
 
   (** Match a bottom value with a value which is not bottom.
 
@@ -125,11 +139,19 @@ module type PrimMatcher = sig
       is important when throwing exceptions, for instance when we need to
       end loans in one of the two environments).
    *)
-  val match_bottom_with_other : bool -> typed_value -> typed_value
+  val match_bottom_with_other :
+    eval_ctx -> eval_ctx -> bool -> typed_value -> typed_value
 
   (** The input ADTs don't have the same variant *)
   val match_distinct_aadts :
-    rty -> adt_avalue -> rty -> adt_avalue -> rty -> typed_avalue
+    eval_ctx ->
+    eval_ctx ->
+    rty ->
+    adt_avalue ->
+    rty ->
+    adt_avalue ->
+    rty ->
+    typed_avalue
 
   (** Parameters:
       [ty0]
@@ -139,7 +161,14 @@ module type PrimMatcher = sig
       [ty]: result of matching ty0 and ty1
    *)
   val match_ashared_borrows :
-    rty -> borrow_id -> rty -> borrow_id -> rty -> typed_avalue
+    eval_ctx ->
+    eval_ctx ->
+    rty ->
+    borrow_id ->
+    rty ->
+    borrow_id ->
+    rty ->
+    typed_avalue
 
   (** Parameters:
       [ty0]
@@ -152,6 +181,8 @@ module type PrimMatcher = sig
       [av]: result of matching av0 and av1
    *)
   val match_amut_borrows :
+    eval_ctx ->
+    eval_ctx ->
     rty ->
     borrow_id ->
     typed_avalue ->
@@ -176,6 +207,8 @@ module type PrimMatcher = sig
       [av]: result of matching av0 and av1
    *)
   val match_ashared_loans :
+    eval_ctx ->
+    eval_ctx ->
     rty ->
     loan_id_set ->
     typed_value ->
@@ -200,6 +233,8 @@ module type PrimMatcher = sig
       [av]: result of matching av0 and av1
    *)
   val match_amut_loans :
+    eval_ctx ->
+    eval_ctx ->
     rty ->
     borrow_id ->
     typed_avalue ->
@@ -213,22 +248,24 @@ module type PrimMatcher = sig
   (** Match two arbitrary avalues whose constructors don't match (this function
       is typically used to raise the proper exception).
    *)
-  val match_avalues : typed_avalue -> typed_avalue -> typed_avalue
+  val match_avalues :
+    eval_ctx -> eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue
 end
 
 module type Matcher = sig
   (** Match two values.
 
       Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}.
    *)
-  val match_typed_values : eval_ctx -> typed_value -> typed_value -> typed_value
+  val match_typed_values :
+    eval_ctx -> eval_ctx -> typed_value -> typed_value -> typed_value
 
   (** Match two avalues.
 
       Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}.
    *)
   val match_typed_avalues :
-    eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue
+    eval_ctx -> eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue
 end
 
 (** See {!module:InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and
@@ -241,7 +278,6 @@ module type MatchCheckEquivState = sig
       a source context with a target context. *)
   val check_equiv : bool
 
-  val ctx : eval_ctx
   val rid_map : RegionId.InjSubst.t ref
 
   (** Substitution for the loan and borrow ids - used only if [check_equiv] is true *)
@@ -302,9 +338,6 @@ type borrow_loan_corresp = {
 
 (* Very annoying: functors only take modules as inputs... *)
 module type MatchJoinState = sig
-  (** The current context *)
-  val ctx : eval_ctx
-
   (** The current loop *)
   val loop_id : LoopId.id
 

compiler/InterpreterLoopsJoinCtxs.ml

@@ -289,7 +289,6 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx)
     : merge_duplicates_funcs =
   (* Rem.: the merge functions raise exceptions (that we catch). *)
   let module S : MatchJoinState = struct
-    let ctx = ctx
     let loop_id = loop_id
     let nabs = ref []
   end in
@@ -360,7 +359,7 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx)
     assert (not (value_has_loans_or_borrows ctx sv1.value));
     let ty = ty0 in
     let child = child0 in
-    let sv = M.match_typed_values ctx sv0 sv1 in
+    let sv = M.match_typed_values ctx ctx sv0 sv1 in
     let value = ALoan (ASharedLoan (ids, sv, child)) in
     { value; ty }
   in
@@ -404,14 +403,6 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
 
   let env0 = List.rev ctx0.env in
   let env1 = List.rev ctx1.env in
-
-  (* We need to pick a context for some functions like [match_typed_values]:
-     the context is only used to lookup module data, so we can pick whichever
-     we want.
-     TODO: this is not very clean. Maybe we should just carry this data around.
-  *)
-  let ctx = ctx0 in
-
   let nabs = ref [] in
 
   (* Explore the environments. *)
@@ -449,8 +440,6 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
   in
 
   let module S : MatchJoinState = struct
-    (* The context is only used to lookup module data: we can pick whichever we want *)
-    let ctx = ctx
     let loop_id = loop_id
     let nabs = nabs
   end in
@@ -466,9 +455,9 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
           (lazy
             ("join_prefixes: BDummys:\n\n- fixed_ids:\n" ^ "\n"
            ^ show_ids_sets fixed_ids ^ "\n\n- value0:\n"
-            ^ env_elem_to_string ctx var0
+            ^ env_elem_to_string ctx0 var0
             ^ "\n\n- value1:\n"
-            ^ env_elem_to_string ctx var1
+            ^ env_elem_to_string ctx1 var1
             ^ "\n\n"));
 
         (* Two cases: the dummy value is an old value, in which case the bindings
@@ -478,7 +467,7 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
           (* Still in the prefix: match the values *)
           assert (b0 = b1);
           let b = b0 in
-          let v = M.match_typed_values ctx v0 v1 in
+          let v = M.match_typed_values ctx0 ctx1 v0 v1 in
           let var = EBinding (BDummy b, v) in
           (* Continue *)
           var :: join_prefixes env0' env1')
@@ -491,17 +480,17 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
           (lazy
             ("join_prefixes: BVars:\n\n- fixed_ids:\n" ^ "\n"
            ^ show_ids_sets fixed_ids ^ "\n\n- value0:\n"
-            ^ env_elem_to_string ctx var0
+            ^ env_elem_to_string ctx0 var0
             ^ "\n\n- value1:\n"
-            ^ env_elem_to_string ctx var1
+            ^ env_elem_to_string ctx1 var1
             ^ "\n\n"));
 
         (* Variable bindings *must* be in the prefix and consequently their
            ids must be the same *)
         assert (b0 = b1);
         (* Match the values *)
         let b = b0 in
-        let v = M.match_typed_values ctx v0 v1 in
+        let v = M.match_typed_values ctx0 ctx1 v0 v1 in
         let var = EBinding (BVar b, v) in
         (* Continue *)
         var :: join_prefixes env0' env1'
@@ -510,8 +499,8 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
         log#ldebug
           (lazy
             ("join_prefixes: Abs:\n\n- fixed_ids:\n" ^ "\n"
-           ^ show_ids_sets fixed_ids ^ "\n\n- abs0:\n" ^ abs_to_string ctx abs0
-           ^ "\n\n- abs1:\n" ^ abs_to_string ctx abs1 ^ "\n\n"));
+           ^ show_ids_sets fixed_ids ^ "\n\n- abs0:\n" ^ abs_to_string ctx0 abs0
+           ^ "\n\n- abs1:\n" ^ abs_to_string ctx1 abs1 ^ "\n\n"));
 
         (* Same as for the dummy values: there are two cases *)
         if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then (