From 4849b736e9b86b08c690152c734abf50d2021559 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 30 Nov 2022 21:37:11 +0100
Subject: Make more progress on the joins
---
compiler/InterpreterLoops.ml | 269 ++++++++++++++++++++-----------------------
1 file changed, 127 insertions(+), 142 deletions(-)
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 85174aaf..cc8cdcff 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -20,15 +20,6 @@ open InterpreterExpressions
(** The local logger *)
let log = L.loops_log
-(* TODO: some fields are actually useless *)
-type cnt_thresholds = {
- aid : V.AbstractionId.id;
- sid : V.SymbolicValueId.id;
- bid : V.BorrowId.id;
- did : C.DummyVarId.id;
- rid : T.RegionId.id;
-}
-
type updt_env_kind =
| AbsInLeft of V.AbstractionId.id
| LoanInLeft of V.BorrowId.id
@@ -1054,116 +1045,139 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id)
try collapse_ctx loop_id (Some merge_funcs) old_ids ctx
with ValueMatchFailure _ -> raise (Failure "Unexpected")
-(*(** Apply substitutions in the first abstraction, then join the abstractions together.
-
- TODO: remove?
- *)
-let subst_join_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
-
- (* Merge the two abstractions *)
- let abs_kind = V.Loop loop_id in
- let can_end = false in
-merge_abstractions abs_kind can_end None 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
- the operation).
+(** Join two contexts *)
+let join_ctxs (config : C.config) (loop_id : V.LoopId.id)
+ (old_ids : InterpreterBorrowsCore.ctx_ids) (ctx0 : C.eval_ctx)
+ (ctx1 : C.eval_ctx) : ctx_or_update =
+ 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
- For instance:
- {[
- abs'0 { mut_loan l0 }
- x -> mut_borrow l0 sx
+ let nabs = ref [] in
- ~~>
+ (* Explore the environments.
- abs'0 {}
- x -> ⊥
- ]}
- *)
-let merge_borrow_with_parent_loop_abs (config : C.config) (bid : V.BorrowId.id)
- (ctx : C.eval_ctx) : C.eval_ctx =
- (* TODO: use the function from InterpreterBorrows *)
- failwith "Unimplemented"
-(* (* Lookup the borrow *)
- let ek =
- { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false }
- in
- (* TODO: use [end_borrow_get_borrow]? *)
- match lookup_borrow ek bid ctx with
- | None -> ctx
- | Some b -> failwith "Unimplemented"*)
-
-(** See {!merge_borrow_with_parent_loop_abs} *)
-let rec merge_borrows_with_parent_loop_abs (config : C.config)
- (bids : V.BorrowId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx =
- V.BorrowId.Set.fold
- (fun id ctx -> merge_borrow_with_parent_loop_abs config id ctx)
- bids ctx
- *)
+ Note that they should have the same prefixes (they should start with
+ old dummy values, old abstractions and bindings which have the same ids).
+ Those old values and abstractions should actually be equal between the
+ two environments.
-(*
-(* 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_old (config : C.config) (tgt_ctx : C.eval_ctx) :
- cm_fun =
- fun cf src_ctx ->
- (* We first reorganize [ctx] so that we can match it with [tgt_ctx] *)
- (* First, collect all the borrows and abstractions which are in [ctx]
- and not in [tgt_ctx]: we need to end them *)
- let src_ids = InterpreterBorrowsCore.compute_context_ids src_ctx in
- let tgt_ids = InterpreterBorrowsCore.compute_context_ids tgt_ctx in
- let bids = V.BorrowId.Set.diff src_ids.bids tgt_ids.bids in
- let aids = V.AbstractionId.Set.diff src_ids.aids tgt_ids.aids in
- (* End those borrows and abstractions *)
- let cc = InterpreterBorrows.end_borrows config bids in
- let cc = comp cc (InterpreterBorrows.end_abstractions config aids) in
- (* In the target context, merge all the borrows introduced by the loop with
- their parent abstractions
+ Rem.: this is important to make the match easy (we take care of preserving
+ the structure of the environments, and ending the proper borrows/abstractions,
+ etc.). We could also implement a more general join.
*)
- let tgt_ctx =
- merge_borrows_with_parent_loop_abs config
- (V.BorrowId.Set.diff tgt_ids.bids src_ids.bids)
- tgt_ctx
+ let join_suffixes (env0 : C.env) (env1 : C.env) : C.env =
+ (* Sanity check: there are no values/abstractions which should be in the prefix *)
+ let check_valid (ee : C.env_elem) : unit =
+ match ee with
+ | C.Var (C.VarBinder _, _) ->
+ (* Variables are necessarily in the prefix *)
+ raise (Failure "Unreachable")
+ | Var (C.DummyBinder did, _) ->
+ assert (not (C.DummyVarId.Set.mem did old_ids.dids))
+ | Abs abs ->
+ assert (not (V.AbstractionId.Set.mem abs.abs_id old_ids.aids))
+ | Frame -> ()
+ in
+ List.iter check_valid env0;
+ List.iter check_valid env1;
+ (* Concatenate the suffixes and append the abstractions introduced while
+ joining the prefixes *)
+ let absl = List.map (fun abs -> C.Abs abs) !nabs in
+ List.concat [ env0; env1; absl ]
in
- (* Replace the source context with the target context - TODO: explain
- why this works *)
- let cf_apply_match : cm_fun = fun cf _ -> cf tgt_ctx in
- let cc = comp cc cf_apply_match in
- (* Sanity check on the resulting context *)
- let cc = comp_check_ctx cc Inv.check_invariants in
- (* Apply and continue *)
- cc cf src_ctx
-*)
-(** Join two contexts *)
-let join_ctxs (_config : C.config) (_old_ids : InterpreterBorrowsCore.ctx_ids)
- (_ctx0 : C.eval_ctx) (_ctx1 : C.eval_ctx) : ctx_or_update =
- raise (Failure "Unimplemented")
+ 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
+ let module JM = MakeJoinMatcher (S) in
+ let module M = Match (JM) in
+ (* Rem.: this function raises exceptions *)
+ let rec join_prefixes (env0 : C.env) (env1 : C.env) : C.env =
+ match (env0, env1) with
+ | ( (C.Var (C.DummyBinder b0, v0) as var) :: env0',
+ C.Var (C.DummyBinder b1, v1) :: env1' ) ->
+ (* Two cases: the dummy value is an old value, in which case the bindings
+ must be the same and we must join their values. Otherwise, it means we
+ are not in the prefix anymore *)
+ if C.DummyVarId.Set.mem b0 old_ids.dids then (
+ (* Still in the prefix: the values must match *)
+ assert (b0 = b1);
+ assert (v0 = v1);
+ (* Continue *)
+ var :: join_prefixes env0' env1')
+ else (* Not in the prefix anymore *)
+ join_suffixes env0 env1
+ | C.Var (C.VarBinder b0, v0) :: env0', C.Var (C.VarBinder b1, v1) :: env1'
+ ->
+ (* 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 var = C.Var (C.VarBinder b, v) in
+ (* Continue *)
+ var :: join_prefixes env0' env1'
+ | (C.Abs abs0 as abs) :: env0', C.Abs abs1 :: env1' ->
+ (* Same as for the dummy values: there are two cases *)
+ if V.AbstractionId.Set.mem abs0.abs_id old_ids.aids then (
+ (* Still in the prefix: the abstractions must be the same *)
+ assert (abs0 = abs1);
+ (* Continue *)
+ abs :: join_suffixes env0' env1')
+ else (* Not in the prefix anymore *)
+ join_suffixes env0 env1
+ | _ ->
+ (* The elements don't match: we are not in the prefix anymore *)
+ join_suffixes env0 env1
+ in
+
+ try
+ let env = List.rev (join_prefixes env0 env1) in
+
+ (* Construct the joined context - of course, the type, fun, etc. contexts
+ * should be the same in the two contexts *)
+ let {
+ C.type_context;
+ fun_context;
+ global_context;
+ type_vars;
+ env = _;
+ ended_regions = ended_regions0;
+ } =
+ ctx0
+ in
+ let {
+ C.type_context = _;
+ fun_context = _;
+ global_context = _;
+ type_vars = _;
+ env = _;
+ ended_regions = ended_regions1;
+ } =
+ ctx1
+ in
+ let ended_regions = T.RegionId.Set.union ended_regions0 ended_regions1 in
+ Ok
+ {
+ C.type_context;
+ fun_context;
+ global_context;
+ type_vars;
+ env;
+ ended_regions;
+ }
+ with ValueMatchFailure e -> Error e
(** Join the context at the entry of the loop with the contexts upon reentry
(upon reaching the [Continue] statement - the goal is to compute a fixed
@@ -1195,7 +1209,7 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
*)
let joined_ctx = ref old_ctx in
let rec join_one_aux (ctx : C.eval_ctx) : unit =
- match join_ctxs config old_ids !joined_ctx ctx with
+ match join_ctxs config loop_id old_ids !joined_ctx ctx with
| Ok nctx -> joined_ctx := nctx
| Error err ->
let ctx =
@@ -1229,28 +1243,6 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
(* # Return *)
!joined_ctx
-(*
-(** Join a context at the entry of a loop with a context upon reaching
- a continue in this loop.
- *)
-let loop_join_entry_ctx_with_continue_ctx (_ctx0 : C.eval_ctx)
- (_ctx1 : C.eval_ctx) : ctx_or_update =
- failwith "Unimplemented"
-
-(** See {!loop_join_entry_ctx_with_continue_ctx} *)
-let rec loop_join_entry_ctx_with_continue_ctxs (ctx0 : C.eval_ctx)
- (ctxs : C.eval_ctx list) : ctx_or_update =
- match ctxs with
- | [] -> Ok ctx0
- | ctx1 :: ctxs -> (
- let res = loop_join_entry_ctx_with_continue_ctx ctx0 ctx1 in
- match res with
- | Error _ ->
- (* TODO: apply the error *)
- raise (Failure "Unimplemented")
- | Ok ctx0 -> loop_join_entry_ctx_with_continue_ctxs ctx0 ctxs)
- *)
-
let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
(eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : C.eval_ctx =
(* The continuation for when we exit the loop - we register the
@@ -1276,13 +1268,6 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
raise (Failure "Nested loops are not supported for now")
in
(* Join the contexts at the loop entry *)
- (* TODO: return result:
- * - end borrows in ctx0
- * - ok: return joined env
- * TODO: keep initial env somewhere?
- * TODO: the returned env is an eval_ctx or smth else?
- * Maybe simply keep track of existentially quantified variables?
- *)
let join_ctxs (ctx0 : C.eval_ctx) : C.eval_ctx =
let ctx1 = loop_join_origin_with_continue_ctxs config loop_id ctx0 !ctxs in
ctxs := [];
--
cgit v1.2.3