Make progress on environments matches and joins

1 files changed, 369 insertions, 27 deletions

diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 702420cd..08607deb 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -28,8 +28,38 @@ type cnt_thresholds = {
   sid : V.SymbolicValueId.id;
   bid : V.BorrowId.id;
   did : C.DummyVarId.id;
+  rid : T.RegionId.id;
 }
 
+(* TODO: document.
+   TODO: we might not use the bounds properly, use sets instead.
+   TODO: actually, bounds are good
+*)
+type match_ctx = {
+  ctx : C.eval_ctx;
+  aids : V.AbstractionId.Set.t;
+  sids : V.SymbolicValueId.Set.t;
+  bids : V.BorrowId.Set.t;
+}
+
+let mk_match_ctx (ctx : C.eval_ctx) : match_ctx =
+  let aids = V.AbstractionId.Set.empty in
+  let sids = V.SymbolicValueId.Set.empty in
+  let bids = V.BorrowId.Set.empty in
+  { ctx; aids; sids; bids }
+
+type updt_env_kind =
+  | EndAbsInSrc of V.AbstractionId.id
+  | EndBorrowsInSrc of V.BorrowId.Set.t
+  | EndBorrowInSrc of V.BorrowId.id
+  | EndBorrowInTgt of V.BorrowId.id
+  | EndBorrowsInTgt of V.BorrowId.Set.t
+
+(** Utility exception *)
+exception ValueMatchFailure of updt_env_kind
+
+type joined_ctx_or_update = (match_ctx, updt_env_kind) result
+
 (** Union Find *)
 module UnionFind = UF.Make (UF.StoreMap)
 
@@ -248,26 +278,328 @@ let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
   (* Return the new context *)
   !ctx
 
-(* TODO: document.
-   TODO: we might not use the bounds properly, use sets instead.
-*)
-type match_ctx = {
-  ctx : C.eval_ctx;
-  aids : V.AbstractionId.Set.t;
-  sids : V.SymbolicValueId.Set.t;
-  bids : V.BorrowId.Set.t;
-}
+let rec match_types (check_regions : 'r -> 'r -> unit) (ctx : C.eval_ctx)
+    (ty0 : 'r T.ty) (ty1 : 'r T.ty) : unit =
+  let match_rec = match_types check_regions ctx in
+  match (ty0, ty1) with
+  | Adt (id0, regions0, tys0), Adt (id1, regions1, tys1) ->
+      assert (id0 = id1);
+      List.iter
+        (fun (id0, id1) -> check_regions id0 id1)
+        (List.combine regions0 regions1);
+      List.iter (fun (ty0, ty1) -> match_rec ty0 ty1) (List.combine tys0 tys1)
+  | TypeVar vid0, TypeVar vid1 -> assert (vid0 = vid1)
+  | Bool, Bool | Char, Char | Never, Never | Str, Str -> ()
+  | Integer int_ty0, Integer int_ty1 -> assert (int_ty0 = int_ty1)
+  | Array ty0, Array ty1 | Slice ty0, Slice ty1 -> match_rec ty0 ty1
+  | Ref (r0, ty0, k0), Ref (r1, ty1, k1) ->
+      check_regions r0 r1;
+      match_rec ty0 ty1;
+      assert (k0 = k1)
+  | _ -> raise (Failure "Unreachable")
+
+let match_rtypes (rid_map : T.RegionId.InjSubst.t ref) (ctx : C.eval_ctx)
+    (ty0 : T.rty) (ty1 : T.rty) : unit =
+  let lookup_rid (id : T.RegionId.id) : T.RegionId.id =
+    T.RegionId.InjSubst.find_with_default id id !rid_map
+  in
+  let check_regions r0 r1 =
+    match (r0, r1) with
+    | T.Static, T.Static -> ()
+    | T.Var id0, T.Var id1 ->
+        let id0 = lookup_rid id0 in
+        assert (id0 = id1)
+    | _ -> raise (Failure "Unexpected")
+  in
+  match_types check_regions ctx ty0 ty1
 
-let mk_match_ctx (ctx : C.eval_ctx) : match_ctx =
-  let aids = V.AbstractionId.Set.empty in
-  let sids = V.SymbolicValueId.Set.empty in
-  let bids = V.BorrowId.Set.empty in
-  { ctx; aids; sids; bids }
+(** This function raises exceptions of kind {!ValueMatchFailue}.
+
+    [convertible]: the function updates it to [false] if the result of the
+    merge is not the result of an alpha-conversion. For instance, if we
+    match two primitive values which are not equal, and thus introduce a
+    symbolic value for the result:
+    {[
+      0 : u32, 1 : u32 ~~> s : u32     where s fresh
+    ]}
+ *)
+let rec match_typed_values (config : C.config) (thresh : cnt_thresholds)
+    (convertible : bool ref) (rid_map : T.RegionId.InjSubst.t ref)
+    (bid_map : V.BorrowId.InjSubst.t ref)
+    (sid_map : V.SymbolicValueId.InjSubst.t ref) (ctx : C.eval_ctx)
+    (v0 : V.typed_value) (v1 : V.typed_value) : V.typed_value =
+  let match_rec =
+    match_typed_values config thresh convertible rid_map bid_map sid_map ctx
+  in
+  let lookup_bid (id : V.BorrowId.id) : V.BorrowId.id =
+    V.BorrowId.InjSubst.find_with_default id id !bid_map
+  in
+  let lookup_bids (ids : V.BorrowId.Set.t) : V.BorrowId.Set.t =
+    V.BorrowId.Set.map lookup_bid ids
+  in
+  let map_bid (id0 : V.BorrowId.id) (id1 : V.BorrowId.id) : V.BorrowId.id =
+    assert (V.BorrowId.Ord.compare id0 thresh.bid >= 0);
+    assert (V.BorrowId.Ord.compare id1 thresh.bid >= 0);
+    assert (not (V.BorrowId.InjSubst.mem id0 !bid_map));
+    bid_map := V.BorrowId.InjSubst.add id0 id1 !bid_map;
+    id1
+  in
+  let lookup_sid (id : V.SymbolicValueId.id) : V.SymbolicValueId.id =
+    match V.SymbolicValueId.InjSubst.find_opt id !sid_map with
+    | None -> id
+    | Some id -> id
+  in
+  assert (v0.V.ty = v1.V.ty);
+  match (v0.V.value, v1.V.value) with
+  | V.Primitive pv0, V.Primitive pv1 ->
+      if pv0 = pv1 then v1 else raise (Failure "Unimplemented")
+  | V.Adt av0, V.Adt av1 ->
+      if av0.variant_id = av1.variant_id then
+        let fields = List.combine av0.field_values av1.field_values in
+        let field_values = List.map (fun (f0, f1) -> match_rec f0 f1) fields in
+        let value : V.value =
+          V.Adt { variant_id = av0.variant_id; field_values }
+        in
+        { V.value; ty = v1.V.ty }
+      else (
+        convertible := false;
+        (* For now, we don't merge values which contain borrows *)
+        (* TODO: *)
+        raise (Failure "Unimplemented"))
+  | Bottom, Bottom -> v1
+  | Borrow bc0, Borrow bc1 ->
+      let bc =
+        match (bc0, bc1) with
+        | SharedBorrow (mv0, bid0), SharedBorrow (mv1, bid1) ->
+            let bid0 = lookup_bid bid0 in
+            (* Not completely sure what to do with the meta-value. If a shared
+               symbolic value gets expanded in a branch, it may be simplified
+               (by being folded back to a symbolic value) upon doing the join,
+               which as a result would lead to code where it is considered as
+               mutable (which is sound). On the other hand, if we access a
+               symbolic value in a loop, the translated loop should take it as
+               input anyway, so maybe this actually leads to equivalent
+               code.
+            *)
+            let mv = match_rec mv0 mv1 in
+            let bid = if bid0 = bid1 then bid1 else map_bid bid0 bid1 in
+            V.SharedBorrow (mv, bid)
+        | MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) ->
+            let bid0 = lookup_bid bid0 in
+            let bv = match_rec bv0 bv1 in
+            let bid = if bid0 = bid1 then bid1 else map_bid bid0 bid1 in
+            V.MutBorrow (bid, bv)
+        | ReservedMutBorrow _, _
+        | _, ReservedMutBorrow _
+        | SharedBorrow _, MutBorrow _
+        | MutBorrow _, SharedBorrow _ ->
+            (* If we get here, either there is a typing inconsistency, or we are
+               trying to match a reserved borrow, which shouldn't happen because
+               reserved borrow should be eliminated very quickly - they are introduced
+               just before function calls which activate them *)
+            raise (Failure "Unexpected")
+      in
+      { V.value = V.Borrow bc; V.ty = v1.V.ty }
+  | Loan lc0, Loan lc1 ->
+      (* TODO: maybe we should enforce that the ids are always exactly the same -
+         without matching *)
+      let lc =
+        match (lc0, lc1) with
+        | SharedLoan (ids0, sv0), SharedLoan (ids1, sv1) ->
+            let ids0 = lookup_bids ids0 in
+            (* Not sure what to do if the ids don't match *)
+            let ids =
+              if ids0 = ids1 then ids1 else raise (Failure "Unimplemented")
+            in
+            let sv = match_rec sv0 sv1 in
+            V.SharedLoan (ids, sv)
+        | MutLoan id0, MutLoan id1 ->
+            let id0 = lookup_bid id0 in
+            let id = if id0 = id1 then id1 else map_bid id0 id1 in
+            V.MutLoan id
+        | SharedLoan _, MutLoan _ | MutLoan _, SharedLoan _ ->
+            raise (Failure "Unreachable")
+      in
+      { V.value = Loan lc; ty = v1.V.ty }
+  | Symbolic sv0, Symbolic sv1 ->
+      (* TODO: id check mapping *)
+      let id0 = lookup_sid sv0.sv_id in
+      let id1 = sv1.sv_id in
+      if id0 = id1 then (
+        assert (sv0.sv_kind = sv1.sv_kind);
+        (* Sanity check: the types should be the same *)
+        match_rtypes rid_map ctx sv0.sv_ty sv1.sv_ty;
+        (* Return *)
+        v1)
+      else (
+        (* For now, we force all the symbolic values containing borrows to
+           be eagerly expanded, and we don't support nested borrows *)
+        assert (not (value_has_borrows ctx v0.V.value));
+        assert (not (value_has_borrows ctx v1.V.value));
+        raise (Failure "Unimplemented"))
+  | Loan lc, _ -> (
+      match lc with
+      | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInSrc ids))
+      | MutLoan id -> raise (ValueMatchFailure (EndBorrowInSrc id)))
+  | _, Loan lc -> (
+      match lc with
+      | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInTgt ids))
+      | MutLoan id -> raise (ValueMatchFailure (EndBorrowInTgt id)))
+  | Symbolic _, _ -> raise (Failure "Unimplemented")
+  | _, Symbolic _ -> raise (Failure "Unimplemented")
+  | _ -> raise (Failure "Unreachable")
+
+(*(** This function raises exceptions of kind {!ValueMatchFailue} *)
+  let rec match_typed_avalues (config : C.config) (thresh : cnt_thresholds)
+      (rid_map : T.RegionId.InjSubst.t ref) (bid_map : V.BorrowId.InjSubst.t ref)
+      (sid_map : V.SymbolicValueId.InjSubst.t ref)
+      (aid_map : V.AbstractionId.InjSubst.t ref) (ctx : C.eval_ctx)
+      (v0 : V.typed_avalue) (v1 : V.typed_avalue) : V.typed_avalue =
+    let match_rec =
+      match_typed_avalues config thresh rid_map bid_map sid_map ctx
+    in
+    (* TODO: factorize those helpers with [match_typed_values] (write a functor?) *)
+    let lookup_bid (id : V.BorrowId.id) : V.BorrowId.id =
+      V.BorrowId.InjSubst.find_with_default id id !bid_map
+    in
+    let lookup_bids (ids : V.BorrowId.Set.t) : V.BorrowId.Set.t =
+      V.BorrowId.Set.map lookup_bid ids
+    in
+    let map_bid (id0 : V.BorrowId.id) (id1 : V.BorrowId.id) : V.BorrowId.id =
+      assert (V.BorrowId.Ord.compare id0 thresh.bid >= 0);
+      assert (V.BorrowId.Ord.compare id1 thresh.bid >= 0);
+      assert (not (V.BorrowId.InjSubst.mem id0 !bid_map));
+      bid_map := V.BorrowId.InjSubst.add id0 id1 !bid_map;
+      id1
+    in
+    let lookup_sid (id : V.SymbolicValueId.id) : V.SymbolicValueId.id =
+      match V.SymbolicValueId.InjSubst.find_opt id !sid_map with
+      | None -> id
+      | Some id -> id
+    in
+    assert (v0.V.ty = v1.V.ty);
+    match (v0.V.value, v1.V.value) with
+    | V.APrimitive pv0, V.APrimitive pv1 ->
+        if pv0 = pv1 then v1 else raise (Failure "Unimplemented")
+    | V.AAdt av0, V.AAdt av1 ->
+        if av0.variant_id = av1.variant_id then
+          let fields = List.combine av0.field_values av1.field_values in
+          let field_values = List.map (fun (f0, f1) -> match_rec f0 f1) fields in
+          let value : V.value =
+            V.Adt { variant_id = av0.variant_id; field_values }
+          in
+          { V.value; ty = v1.V.ty }
+        else raise (Failure "Unimplemented")
+    | Bottom, Bottom -> v1
+    | Borrow bc0, Borrow bc1 ->
+        let bc =
+          match (bc0, bc1) with
+          | SharedBorrow (mv0, bid0), SharedBorrow (mv1, bid1) ->
+              let bid0 = lookup_bid bid0 in
+              (* Not completely sure what to do with the meta-value. If a shared
+                 symbolic value gets expanded in a branch, it may be simplified
+                 (by being folded back to a symbolic value) upon doing the join,
+                 which as a result would lead to code where it is considered as
+                 mutable (which is sound). On the other hand, if we access a
+                 symbolic value in a loop, the translated loop should take it as
+                 input anyway, so maybe this actually leads to equivalent
+                 code.
+              *)
+              let mv = match_rec mv0 mv1 in
+              let bid = if bid0 = bid1 then bid1 else map_bid bid0 bid1 in
+              V.SharedBorrow (mv, bid)
+          | MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) ->
+              let bid0 = lookup_bid bid0 in
+              let bv = match_rec bv0 bv1 in
+              let bid = if bid0 = bid1 then bid1 else map_bid bid0 bid1 in
+              V.MutBorrow (bid, bv)
+          | ReservedMutBorrow _, _
+          | _, ReservedMutBorrow _
+          | SharedBorrow _, MutBorrow _
+          | MutBorrow _, SharedBorrow _ ->
+              (* If we get here, either there is a typing inconsistency, or we are
+                 trying to match a reserved borrow, which shouldn't happen because
+                 reserved borrow should be eliminated very quickly - they are introduced
+                 just before function calls which activate them *)
+              raise (Failure "Unexpected")
+        in
+        { V.value = V.Borrow bc; V.ty = v1.V.ty }
+    | Loan lc0, Loan lc1 ->
+        (* TODO: maybe we should enforce that the ids are always exactly the same -
+           without matching *)
+        let lc =
+          match (lc0, lc1) with
+          | SharedLoan (ids0, sv0), SharedLoan (ids1, sv1) ->
+              let ids0 = lookup_bids ids0 in
+              (* Not sure what to do if the ids don't match *)
+              let ids =
+                if ids0 = ids1 then ids1 else raise (Failure "Unimplemented")
+              in
+              let sv = match_rec sv0 sv1 in
+              V.SharedLoan (ids, sv)
+          | MutLoan id0, MutLoan id1 ->
+              let id0 = lookup_bid id0 in
+              let id = if id0 = id1 then id1 else map_bid id0 id1 in
+              V.MutLoan id
+          | SharedLoan _, MutLoan _ | MutLoan _, SharedLoan _ ->
+              raise (Failure "Unreachable")
+        in
+        { V.value = Loan lc; ty = v1.V.ty }
+    | Symbolic sv0, Symbolic sv1 ->
+        (* TODO: id check mapping *)
+        let id0 = lookup_sid sv0.sv_id in
+        let id1 = sv1.sv_id in
+        if id0 = id1 then (
+          assert (sv0.sv_kind = sv1.sv_kind);
+          (* Sanity check: the types should be the same *)
+          match_rtypes rid_map ctx sv0.sv_ty sv1.sv_ty;
+          (* Return *)
+          v1)
+        else (
+          (* For now, we force all the symbolic values containing borrows to
+             be eagerly expanded, and we don't support nested borrows *)
+          assert (not (value_has_borrows ctx v0.V.value));
+          assert (not (value_has_borrows ctx v1.V.value));
+          raise (Failure "Unimplemented"))
+    | Loan lc, _ -> (
+        match lc with
+        | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInSrc ids))
+        | MutLoan id -> raise (ValueMatchFailure (EndBorrowInSrc id)))
+    | _, Loan lc -> (
+        match lc with
+        | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInTgt ids))
+        | MutLoan id -> raise (ValueMatchFailure (EndBorrowInTgt id)))
+  | _ -> raise (Failure "Unreachable")*)
+
+(** Apply substitutions in the first abstraction, then merge the abstractions together. *)
+let subst_merge_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
+    (rid_map : T.RegionId.InjSubst.t) (bid_map : V.BorrowId.InjSubst.t)
+    (sid_map : V.SymbolicValueId.InjSubst.t) (ctx : C.eval_ctx) (abs0 : V.abs)
+    (abs1 : V.abs) : V.abs =
+  (* Apply the substitutions in the first abstraction *)
+  let rsubst id =
+    assert (T.RegionId.Ord.compare id thresh.rid >= 0);
+    T.RegionId.InjSubst.find_with_default id id rid_map
+  in
+  let rvsubst id = id in
+  let tsubst id = id in
+  let ssubst id =
+    assert (V.SymbolicValueId.Ord.compare id thresh.sid >= 0);
+    V.SymbolicValueId.InjSubst.find_with_default id id sid_map
+  in
+  let bsubst id =
+    assert (V.BorrowId.Ord.compare id thresh.bid >= 0);
+    V.BorrowId.InjSubst.find_with_default id id bid_map
+  in
+  let asubst id = id in
+  let abs0 =
+    Substitute.abs_subst_ids rsubst rvsubst tsubst ssubst bsubst asubst abs0
+  in
 
-type joined_ctx_or_update =
-  | EndAbs of V.AbstractionId.id
-  | EndBorrow of V.BorrowId.id
-  | JoinedCtx of match_ctx
+  (* Merge the two abstractions *)
+  let abs_kind = V.Loop loop_id in
+  let can_end = false in
+  merge_abstractions abs_kind can_end ctx abs0 abs1
 
 (** Merge a borrow with the abstraction containing the associated loan, where
     the abstraction must be a *loop abstraction* (we don't synthesize code during
@@ -306,8 +638,10 @@ let rec merge_borrows_with_parent_loop_abs (config : C.config)
 
 (* TODO: we probably don't need an [match_ctx], and actually we might not use
    the bounds propertly.
+   TODO: remove
 *)
-let match_ctx_with_target (config : C.config) (tgt_mctx : match_ctx) : cm_fun =
+let match_ctx_with_target_old (config : C.config) (tgt_mctx : match_ctx) :
+    cm_fun =
  fun cf src_ctx ->
   (* We first reorganize [ctx] so that we can match it with [tgt_mctx] *)
   (* First, collect all the borrows and abstractions which are in [ctx]
@@ -351,12 +685,12 @@ let loop_join_entry_ctx_with_continue_ctx (ctx0 : match_ctx) (ctx1 : C.eval_ctx)
 let rec loop_join_entry_ctx_with_continue_ctxs (ctx0 : match_ctx)
     (ctxs : C.eval_ctx list) : joined_ctx_or_update =
   match ctxs with
-  | [] -> JoinedCtx ctx0
+  | [] -> Ok ctx0
   | ctx1 :: ctxs -> (
       let res = loop_join_entry_ctx_with_continue_ctx ctx0 ctx1 in
       match res with
-      | EndAbs _ | EndBorrow _ -> res
-      | JoinedCtx ctx0 -> loop_join_entry_ctx_with_continue_ctxs ctx0 ctxs)
+      | Error _ -> res
+      | Ok ctx0 -> loop_join_entry_ctx_with_continue_ctxs ctx0 ctxs)
 
 let compute_loop_entry_fixed_point (config : C.config)
     (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : match_ctx =
@@ -416,17 +750,25 @@ let compute_loop_entry_fixed_point (config : C.config)
         (* Check if the join succeeded, or if we need to end abstractions/borrows
            in the original environment first *)
         match join_ctxs mctx with
-        | EndAbs id ->
+        | Error (EndAbsInSrc id) ->
             let ctx1 =
               InterpreterBorrows.end_abstraction_no_synth config id mctx.ctx
             in
             eval_iteration_then_join { mctx with ctx = ctx1 }
-        | EndBorrow id ->
+        | Error (EndBorrowInSrc id) ->
             let ctx1 =
               InterpreterBorrows.end_borrow_no_synth config id mctx.ctx
             in
             eval_iteration_then_join { mctx with ctx = ctx1 }
-        | JoinedCtx mctx1 ->
+        | Error (EndBorrowsInSrc ids) ->
+            let ctx1 =
+              InterpreterBorrows.end_borrows_no_synth config ids mctx.ctx
+            in
+            eval_iteration_then_join { mctx with ctx = ctx1 }
+        | Error (EndBorrowInTgt _ | EndBorrowsInTgt _) ->
+            (* Shouldn't happen here *)
+            raise (Failure "Unreachable")
+        | Ok mctx1 ->
             (* The join succeeded: check if we reached a fixed point, otherwise
                iterate *)
             if equiv_ctxs mctx mctx1 then mctx1
@@ -487,7 +829,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
   (* Compute the fixed point at the loop entrance *)
   let mctx = compute_loop_entry_fixed_point config eval_loop_body ctx in
   (* Synthesize the end of the function *)
-  let end_expr = match_ctx_with_target config mctx (cf EndEnterLoop) ctx in
+  let end_expr = match_ctx_with_target_old config mctx (cf EndEnterLoop) ctx in
   (* Synthesize the loop body by evaluating it, with the continuation for
      after the loop starting at the *fixed point*, but with a special
      treatment for the [Break] and [Continue] cases *)
@@ -502,7 +844,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
     | Continue i ->
         (* We don't support nested loops for now *)
         assert (i = 0);
-        match_ctx_with_target config mctx (cf EndContinue) ctx
+        match_ctx_with_target_old config mctx (cf EndContinue) ctx
     | Unit | EndEnterLoop | EndContinue ->
         (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}.
            For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now.