diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Config.ml | 2 | ||||
| -rw-r--r-- | compiler/Contexts.ml | 36 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 51 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.mli | 41 | ||||
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 29 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 622 |
6 files changed, 381 insertions, 400 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml index 3e882365..b37d4a84 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -82,7 +82,7 @@ let return_unit_end_abs_with_no_loans = true thus use this bound to detect a loop, fail and report the case to the user. *) -let loop_fixed_point_max_num_iters = 100 +let loop_fixed_point_max_num_iters = 2 (** {1 Translation} *) diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index be758ffe..cb6a092f 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -439,22 +439,9 @@ let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool = (** Visitor to iterate over the values in the *current* frame *) class ['self] iter_frame = object (self : 'self) - inherit [_] V.iter_abs + inherit [_] iter_env - method visit_Var : 'acc -> binder -> typed_value -> unit = - fun acc _ v -> self#visit_typed_value acc v - - method visit_Abs : 'acc -> abs -> unit = - fun acc abs -> self#visit_abs acc abs - - method visit_env_elem : 'acc -> env_elem -> unit = - fun acc em -> - match em with - | Var (vid, v) -> self#visit_Var acc vid v - | Abs abs -> self#visit_Abs acc abs - | Frame -> raise (Failure "Unreachable") - - method visit_env : 'acc -> env -> unit = + method! visit_env : 'acc -> env -> unit = fun acc env -> match env with | [] -> () @@ -467,24 +454,9 @@ class ['self] iter_frame = (** Visitor to map over the values in the *current* frame *) class ['self] map_frame_concrete = object (self : 'self) - inherit [_] V.map_abs - - method visit_Var : 'acc -> binder -> typed_value -> env_elem = - fun acc b v -> - let v = self#visit_typed_value acc v in - Var (b, v) - - method visit_Abs : 'acc -> abs -> env_elem = - fun acc abs -> Abs (self#visit_abs acc abs) - - method visit_env_elem : 'acc -> env_elem -> env_elem = - fun acc em -> - match em with - | Var (vid, v) -> self#visit_Var acc vid v - | Abs abs -> self#visit_Abs acc abs - | Frame -> raise (Failure "Unreachable") + inherit [_] map_env - method visit_env : 'acc -> env -> env = + method! visit_env : 'acc -> env -> env = fun acc env -> match env with | [] -> [] diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 1b05911b..a8d50720 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -1423,6 +1423,9 @@ let end_borrows_no_synth config ids ctx = let end_abstraction_no_synth config id ctx = get_cf_ctx_no_synth (end_abstraction config id) ctx +let end_abstractions_no_synth config ids ctx = + get_cf_ctx_no_synth (end_abstractions config ids) ctx + (** Helper function: see {!activate_reserved_mut_borrow}. This function updates the shared loan to a mutable loan (we then update @@ -1923,8 +1926,7 @@ type merge_abstraction_info = { - all the borrows are destructured (for instance, shared loans can't contain shared loans). *) -let compute_merge_abstractions_info (ctx : C.eval_ctx) (abs : V.abs) : - merge_abstraction_info = +let compute_merge_abstractions_info (abs : V.abs) : merge_abstraction_info = let loans : V.loan_id_set ref = ref V.BorrowId.Set.empty in let borrows : V.borrow_id_set ref = ref V.BorrowId.Set.empty in let borrows_loans : borrow_or_loan_id list ref = ref [] in @@ -2060,7 +2062,23 @@ type merge_duplicates_funcs = { V.mvalue -> V.typed_avalue -> V.typed_avalue; + (** Parameters: + - [id] + - [ty0] + - [mv0] + - [child0] + - [ty1] + - [mv1] + - [child1] + + The children should be [AIgnored]. + *) merge_ashared_borrows : V.borrow_id -> T.rty -> T.rty -> V.typed_avalue; + (** Parameters: + - [id] + - [ty0] + - [ty1] + *) merge_amut_loans : V.loan_id -> T.rty -> @@ -2068,13 +2086,33 @@ type merge_duplicates_funcs = { T.rty -> V.typed_avalue -> V.typed_avalue; + (** Parameters: + - [id] + - [ty0] + - [child0] + - [ty1] + - [child1] + + The children should be [AIgnored]. + *) merge_ashared_loans : V.loan_id_set -> T.rty -> V.typed_value -> + V.typed_avalue -> T.rty -> V.typed_value -> + V.typed_avalue -> V.typed_avalue; + (** Parameters: + - [ids] + - [ty0] + - [sv0] + - [child0] + - [ty1] + - [sv1] + - [child1] + *) } let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool) @@ -2094,7 +2132,7 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool) loan_to_content = loan_to_content0; borrow_to_content = borrow_to_content0; } = - compute_merge_abstractions_info ctx abs0 + compute_merge_abstractions_info abs0 in let { @@ -2104,7 +2142,7 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool) loan_to_content = loan_to_content1; borrow_to_content = borrow_to_content1; } = - compute_merge_abstractions_info ctx abs1 + compute_merge_abstractions_info abs1 in (* Sanity check: there is no loan/borrows which appears in both abstractions, @@ -2181,7 +2219,7 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool) let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty) (bc1 : g_borrow_content_with_ty) : V.typed_avalue = match (bc0, bc1) with - | Concrete (ty0, bc0), Concrete (ty1, bc1) -> + | Concrete _, Concrete _ -> (* This can happen only in case of nested borrows *) raise (Failure "Unreachable") | Abstract (ty0, bc0), Abstract (ty1, bc1) -> @@ -2212,7 +2250,8 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool) (* Register the loan ids *) V.BorrowId.Set.iter set_loan_as_merged ids; (* Merge *) - (Option.get merge_funs).merge_ashared_loans ids ty0 sv0 ty1 sv1 + (Option.get merge_funs).merge_ashared_loans ids ty0 sv0 child0 ty1 sv1 + child1 | _ -> (* Unreachable because those cases are ignored (ended/ignored borrows) or inconsistent *) diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli index 8b8b76d9..01ce206a 100644 --- a/compiler/InterpreterBorrows.mli +++ b/compiler/InterpreterBorrows.mli @@ -41,6 +41,10 @@ val end_borrows_no_synth : val end_abstraction_no_synth : C.config -> V.AbstractionId.id -> C.eval_ctx -> C.eval_ctx +(** End a set of abstractions and return the resulting environment, ignoring synthesis *) +val end_abstractions_no_synth : + C.config -> V.AbstractionId.Set.t -> C.eval_ctx -> C.eval_ctx + (** Promote a reserved mut borrow to a mut borrow, while preserving the invariants. Reserved borrows are special mutable borrows which are created as shared borrows @@ -133,6 +137,7 @@ val convert_value_to_abstractions : Rem.: it may be more idiomatic to have a functor, but this seems a bit heavyweight, though. *) + type merge_duplicates_funcs = { merge_amut_borrows : V.borrow_id -> @@ -143,7 +148,23 @@ type merge_duplicates_funcs = { V.mvalue -> V.typed_avalue -> V.typed_avalue; + (** Parameters: + - [id] + - [ty0] + - [mv0] + - [child0] + - [ty1] + - [mv1] + - [child1] + + The children should be [AIgnored]. + *) merge_ashared_borrows : V.borrow_id -> T.rty -> T.rty -> V.typed_avalue; + (** Parameters: + - [id] + - [ty0] + - [ty1] + *) merge_amut_loans : V.loan_id -> T.rty -> @@ -151,13 +172,33 @@ type merge_duplicates_funcs = { T.rty -> V.typed_avalue -> V.typed_avalue; + (** Parameters: + - [id] + - [ty0] + - [child0] + - [ty1] + - [child1] + + The children should be [AIgnored]. + *) merge_ashared_loans : V.loan_id_set -> T.rty -> V.typed_value -> + V.typed_avalue -> T.rty -> V.typed_value -> + V.typed_avalue -> V.typed_avalue; + (** Parameters: + - [ids] + - [ty0] + - [sv0] + - [child0] + - [ty1] + - [sv1] + - [child1] + *) } (** Merge two abstractions together. diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 54949d3f..6db23cc4 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -182,14 +182,29 @@ let projection_contains (ty1 : T.rty) (rset1 : T.RegionId.Set.t) (ty2 : T.rty) in compare_rtys default combine compare_regions ty1 ty2 -(** Compute the set of borrow ids, loan ids and abstraction ids in a context. *) -let compute_borrow_abs_ids_in_context (ctx : C.eval_ctx) : - V.BorrowId.Set.t * V.AbstractionId.Set.t = +(* TODO: there misses fields *) +type ctx_ids = { + aids : V.AbstractionId.Set.t; + bids : V.BorrowId.Set.t; + dids : C.DummyVarId.Set.t; +} + +(* TODO: move *) + +(** Compute the sets of ids found in a list of contexts. *) +let compute_contexts_ids (ctxl : C.eval_ctx list) : ctx_ids = let bids = ref V.BorrowId.Set.empty in let aids = ref V.AbstractionId.Set.empty in + let dids = ref C.DummyVarId.Set.empty in let obj = object inherit [_] C.iter_eval_ctx + + method! visit_binder _ bv = + match bv with + | VarBinder _ -> () + | DummyBinder bid -> dids := C.DummyVarId.Set.add bid !dids + method! visit_borrow_id _ id = bids := V.BorrowId.Set.add id !bids method! visit_loan_id _ id = @@ -201,8 +216,12 @@ let compute_borrow_abs_ids_in_context (ctx : C.eval_ctx) : aids := V.AbstractionId.Set.add id !aids end in - obj#visit_eval_ctx () ctx; - (!bids, !aids) + List.iter (obj#visit_eval_ctx ()) ctxl; + { aids = !aids; bids = !bids; dids = !dids } + +(** Compute the sets of ids found in a context. *) +let compute_context_ids (ctx : C.eval_ctx) : ctx_ids = + compute_contexts_ids [ ctx ] (** Lookup a loan content. diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 00e6eb01..85174aaf 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -15,14 +15,12 @@ open Utils open Cps open InterpreterUtils open InterpreterBorrows -open InterpreterProjectors -open InterpreterExpansion -open InterpreterPaths 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; @@ -31,34 +29,18 @@ type cnt_thresholds = { 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 = | AbsInLeft of V.AbstractionId.id | LoanInLeft of V.BorrowId.id | LoansInLeft of V.BorrowId.Set.t + | AbsInRight of V.AbstractionId.id | LoanInRight of V.BorrowId.id | LoansInRight of V.BorrowId.Set.t (** Utility exception *) exception ValueMatchFailure of updt_env_kind -type joined_ctx_or_update = (match_ctx, updt_env_kind) result +type ctx_or_update = (C.eval_ctx, updt_env_kind) result (** Union Find *) module UnionFind = UF.Make (UF.StoreMap) @@ -209,16 +191,40 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool) borrow_loan_to_abs = !borrow_loan_to_abs; } +(** Destructure all the new abstractions *) +let destructure_new_abs (loop_id : V.LoopId.id) + (old_abs_ids : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx = + let abs_kind = V.Loop loop_id in + let can_end = false in + let destructure_shared_values = true in + let is_fresh_abs_id (id : V.AbstractionId.id) : bool = + not (V.AbstractionId.Set.mem id old_abs_ids) + in + let env = + List.map + (fun ee -> + match ee with + | C.Var _ | C.Frame -> ee + | C.Abs abs -> + if is_fresh_abs_id abs.abs_id then + let abs = + destructure_abs abs_kind can_end destructure_shared_values ctx + abs + in + C.Abs abs + else ee) + ctx.env + in + { ctx with env } + (** Collapse an environment. We do this to simplify an environment, for the purpose of finding a loop fixed point. We do the following: - - we look for all the *new* dummy values (we use id thresholds to decide - wether a value is new or not - the ids generated by our counters are - monotonic), and we convert to abstractions (if they contain loans or - borrows) + - we look for all the *new* dummy values (we use sets of old ids to decide + wether a value is new or not) - whenever there is a new abstraction in the context, and some of its its borrows are associated to loans in another new abstraction, we merge them. @@ -232,18 +238,21 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool) they become well formed again after collapsing). *) let collapse_ctx (loop_id : V.LoopId.id) - (merge_funs : merge_duplicates_funcs option) (thresh : cnt_thresholds) - (ctx0 : C.eval_ctx) : C.eval_ctx = + (merge_funs : merge_duplicates_funcs option) + (old_ids : InterpreterBorrowsCore.ctx_ids) (ctx0 : C.eval_ctx) : C.eval_ctx + = let abs_kind = V.Loop loop_id in let can_end = false in let destructure_shared_values = true in let is_fresh_abs_id (id : V.AbstractionId.id) : bool = - V.AbstractionId.Ord.compare thresh.aid id >= 0 + not (V.AbstractionId.Set.mem id old_ids.aids) in let is_fresh_did (id : C.DummyVarId.id) : bool = - C.DummyVarId.Ord.compare thresh.did id >= 0 + not (C.DummyVarId.Set.mem id old_ids.dids) in - (* Convert the dummy values to abstractions *) + (* Convert the dummy values to abstractions, and destructure all the new + abstractions at the same time (note that when we convert values to + abstractions, the resulting abstraction should be destructured) *) (* Note that we preserve the order of the dummy values: we replace them with abstractions in place - this makes matching easier *) let env = @@ -538,7 +547,10 @@ end We use it for joins, to check if two environments are convertible, etc. *) module Match (M : Matcher) = struct - (** Match two values *) + (** Match two values. + + Rem.: this function raises exceptions of type {!ValueMatchFailure}. + *) let rec match_typed_values (ctx : C.eval_ctx) (v0 : V.typed_value) (v1 : V.typed_value) : V.typed_value = let match_rec = match_typed_values ctx in @@ -636,6 +648,10 @@ module Match (M : Matcher) = struct | _, Symbolic sv -> M.match_symbolic_with_other false sv v0 | _ -> raise (Failure "Unreachable") + (** Match two avalues. + + Rem.: this function raises exceptions of type {!ValueMatchFailure}. + *) and match_typed_avalues (ctx : C.eval_ctx) (v0 : V.typed_avalue) (v1 : V.typed_avalue) : V.typed_avalue = let match_rec = match_typed_values ctx in @@ -952,267 +968,93 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct let match_avalues _ _ = raise (Failure "Unreachable") end -(* -(** This function raises exceptions of kind {!ValueMatchFailue}. +(** Collapse an environment, merging the duplicated borrows/loans. - [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 - ]} + This function simply calls {!collapse_ctx} with the proper merging functions. *) -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 +let collapse_ctx_with_merge (loop_id : V.LoopId.id) + (old_ids : InterpreterBorrowsCore.ctx_ids) (ctx : C.eval_ctx) : C.eval_ctx = + (* When we join environments, we may introduce duplicated *loans*: we thus + don't implement merge functions for the borrows, only for the loans. + + For instance: + {[ + // If we have: + env0 = { + abs0 { ML l0 } + l -> MB l0 s0 + } + + env1 = { + abs0 { ML l0 } + abs1 { MB l0, ML l1 } + l -> MB l1 s1 + } + + // Then: + join env0 env1 = { + abs0 { ML l0 } + abs1 { MB l0, ML l1 } + abs2 { MB l0, MB l1, ML l2 } // Introduced when merging the "l" binding + l -> MB l2 s2 + } + ]} + + 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 + let module JM = MakeJoinMatcher (S) in + let module M = Match (JM) in + let merge_amut_borrows _ _ _ _ _ _ _ = raise (Failure "Unexpected") in + let merge_ashared_borrows _ _ _ = raise (Failure "Unexpected") in + let merge_amut_loans id ty0 child0 _ty1 child1 = + (* Sanity checks *) + assert (is_aignored child0.V.value); + assert (is_aignored child1.V.value); + (* We simply need to introduce an [AMutLoan]. Some remarks: + - the child is [AIgnored] + - we need to pick some types. The types on the left and on the right + may use different regions: it doesn't really matter (here, we pick + the ones from the left). + *) + let ty = ty0 in + let child = child0 in + let value = V.ALoan (V.AMutLoan (id, child)) in + { V.value; ty } 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 + let merge_ashared_loans ids ty0 (sv0 : V.typed_value) child0 _ty1 + (sv1 : V.typed_value) child1 = + (* Sanity checks *) + assert (is_aignored child0.V.value); + assert (is_aignored child1.V.value); + (* Same remarks as for [merge_amut_loans]. + + This time, however, we need to merge the shared values. + *) + assert (not (value_has_loans_or_borrows ctx sv0.V.value)); + assert (not (value_has_loans_or_borrows ctx sv1.V.value)); + let ty = ty0 in + let child = child0 in + let sv = M.match_typed_values ctx sv0 sv1 in + let value = V.ALoan (V.ASharedLoan (ids, sv, child)) in + { V.value; ty } 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 + let merge_funcs = + { + merge_amut_borrows; + merge_ashared_borrows; + merge_amut_loans; + merge_ashared_loans; + } 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 (LoansInLeft ids)) - | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id))) - | _, Loan lc -> ( - match lc with - | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids)) - | MutLoan id -> raise (ValueMatchFailure (LoanInRight id))) - | Symbolic _, _ -> raise (Failure "Unimplemented") - | _, Symbolic _ -> raise (Failure "Unimplemented") - | _ -> raise (Failure "Unreachable") - *) + try collapse_ctx loop_id (Some merge_funcs) old_ids ctx + with ValueMatchFailure _ -> raise (Failure "Unexpected") -(*(** 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 (LoansInLeft ids)) - | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id))) - | _, Loan lc -> ( - match lc with - | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids)) - | MutLoan id -> raise (ValueMatchFailure (LoanInRight id))) - | _ -> raise (Failure "Unreachable")*) - -(** Apply substitutions in the first abstraction, then join the abstractions together. +(*(** Apply substitutions in the first abstraction, then join the abstractions together. TODO: remove? *) @@ -1243,8 +1085,9 @@ let subst_join_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds) (* 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_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). @@ -1279,25 +1122,23 @@ let rec merge_borrows_with_parent_loop_abs (config : C.config) V.BorrowId.Set.fold (fun id ctx -> merge_borrow_with_parent_loop_abs config id ctx) bids ctx + *) +(* (* 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_mctx : match_ctx) : +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_mctx] *) + (* 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_mctx]: we need to end them *) - let src_bids, src_aids = - InterpreterBorrowsCore.compute_borrow_abs_ids_in_context src_ctx - in - let tgt_bids, tgt_aids = - InterpreterBorrowsCore.compute_borrow_abs_ids_in_context tgt_mctx.ctx - in - let bids = V.BorrowId.Set.diff src_bids tgt_bids in - let aids = V.AbstractionId.Set.diff src_aids tgt_aids in + 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 @@ -1306,8 +1147,8 @@ let match_ctx_with_target_old (config : C.config) (tgt_mctx : match_ctx) : *) let tgt_ctx = merge_borrows_with_parent_loop_abs config - (V.BorrowId.Set.diff tgt_bids src_bids) - tgt_mctx.ctx + (V.BorrowId.Set.diff tgt_ids.bids src_ids.bids) + tgt_ctx in (* Replace the source context with the target context - TODO: explain why this works *) @@ -1317,29 +1158,104 @@ let match_ctx_with_target_old (config : C.config) (tgt_mctx : match_ctx) : 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") + +(** 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 + point for the loop entry). + *) +let loop_join_origin_with_continue_ctxs (config : C.config) + (loop_id : V.LoopId.id) (old_ctx : C.eval_ctx) (ctxl : C.eval_ctx list) : + C.eval_ctx = + (* # Look for borrows and abstractions that exist in [old_ctx] and not in [ctxl]: + * we need to end those *) + (* Compute the sets of borrows and abstractions *) + let old_ids = InterpreterBorrowsCore.compute_context_ids old_ctx in + let new_ids = InterpreterBorrowsCore.compute_contexts_ids ctxl in + let bids = V.BorrowId.Set.diff old_ids.bids new_ids.bids in + let aids = V.AbstractionId.Set.diff old_ids.aids new_ids.aids in + (* End those borrows and abstractions *) + let old_ctx = InterpreterBorrows.end_borrows_no_synth config bids old_ctx in + let old_ctx = + InterpreterBorrows.end_abstractions_no_synth config aids old_ctx + in + + (* # Join with the new contexts, one by one + + For every context, we repeteadly attempt to join it with the current + result of the join: if we fail (because we need to end loans for instance), + we update the context and retry. + Rem.: we should never have to end loans in the aggregated context, only + in the one we are trying to add to the join. + *) + 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 + | Ok nctx -> joined_ctx := nctx + | Error err -> + let ctx = + match err with + | LoanInRight bid -> + InterpreterBorrows.end_borrow_no_synth config bid ctx + | LoansInRight bids -> + InterpreterBorrows.end_borrows_no_synth config bids ctx + | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ -> + raise (Failure "Unexpected") + in + join_one_aux ctx + in + let join_one (ctx : C.eval_ctx) : unit = + (* Destructure the abstractions introduced in the new context *) + let ctx = destructure_new_abs loop_id old_ids.aids ctx in + (* Collapse the context we want to add to the join *) + let ctx = collapse_ctx loop_id None old_ids ctx in + (* Join the two contexts *) + join_one_aux ctx; + (* Collapse again - the join might have introduce abstractions we want + to merge with the others (note that those abstractions may actually + lead to borrows/loans duplications) *) + joined_ctx := collapse_ctx_with_merge loop_id old_ids !joined_ctx; + (* Sanity check *) + if !Config.check_invariants then Invariants.check_invariants !joined_ctx + in + + List.iter join_one ctxl; + + (* # 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 : match_ctx) (ctx1 : C.eval_ctx) - : joined_ctx_or_update = +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 : match_ctx) - (ctxs : C.eval_ctx list) : joined_ctx_or_update = +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 _ -> res + | 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) - (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : match_ctx = - (* The continuation for when we exit the loop - we use it to register the - environments upon loop *reentry* +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 + environments upon loop *reentry*, and synthesize nothing by + returning [None] *) let ctxs = ref [] in let register_ctx ctx = ctxs := ctx :: !ctxs in @@ -1367,64 +1283,51 @@ let compute_loop_entry_fixed_point (config : C.config) * TODO: the returned env is an eval_ctx or smth else? * Maybe simply keep track of existentially quantified variables? *) - let join_ctxs (ctx0 : match_ctx) : joined_ctx_or_update = - let ctx1 = loop_join_entry_ctx_with_continue_ctxs ctx0 !ctxs in + 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 := []; ctx1 in (* Check if two contexts are equivalent - modulo alpha conversion on the existentially quantified borrows/abstractions/symbolic values *) - let equiv_ctxs (_ctx1 : match_ctx) (_ctx2 : match_ctx) : bool = + let equiv_ctxs (_ctx1 : C.eval_ctx) (_ctx2 : C.eval_ctx) : bool = failwith "Unimplemented" in let max_num_iter = Config.loop_fixed_point_max_num_iters in - let rec compute_fixed_point (mctx : match_ctx) (i : int) : match_ctx = + let rec compute_fixed_point (ctx : C.eval_ctx) (i : int) : C.eval_ctx = if i = 0 then raise (Failure ("Could not compute a loop fixed point in " ^ string_of_int max_num_iter ^ " iterations")) else - (* The join on the environments may fail if we need to end some borrows/abstractions - in the original context first: reorganize the original environment for as - long as we need to *) - let rec eval_iteration_then_join (mctx : match_ctx) = - (* Evaluate the loop body *) - let _ = eval_loop_body cf_exit_loop_body mctx.ctx in - (* Check if the join succeeded, or if we need to end abstractions/borrows - in the original environment first *) - match join_ctxs mctx with - | Error (AbsInLeft id) -> - let ctx1 = - InterpreterBorrows.end_abstraction_no_synth config id mctx.ctx - in - eval_iteration_then_join { mctx with ctx = ctx1 } - | Error (LoanInLeft id) -> - let ctx1 = - InterpreterBorrows.end_borrow_no_synth config id mctx.ctx - in - eval_iteration_then_join { mctx with ctx = ctx1 } - | Error (LoansInLeft ids) -> - let ctx1 = - InterpreterBorrows.end_borrows_no_synth config ids mctx.ctx - in - eval_iteration_then_join { mctx with ctx = ctx1 } - | Error (LoanInRight _ | LoansInRight _) -> - (* 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 - else compute_fixed_point mctx1 (i - 1) - in - eval_iteration_then_join mctx + (* Evaluate the loop body to register the different contexts upon reentry *) + let _ = eval_loop_body cf_exit_loop_body ctx in + (* Compute the join between the original contexts and the contexts computed + upon reentry *) + let ctx1 = join_ctxs ctx0 in + (* Check if we reached a fixed point: if not, iterate *) + if equiv_ctxs ctx0 ctx1 then ctx1 else compute_fixed_point ctx1 (i - 1) in - compute_fixed_point (mk_match_ctx ctx0) max_num_iter + compute_fixed_point ctx0 max_num_iter + +let match_ctx_with_target (config : C.config) (tgt_ctx : C.eval_ctx) : cm_fun = + fun cf src_ctx -> + (* We first reorganize [src_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 + (* TODO *) + raise (Failure "Unimplemented") (** Evaluate a loop in concrete mode *) -let eval_loop_concrete (config : C.config) (eval_loop_body : st_cm_fun) : - st_cm_fun = +let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun = fun cf ctx -> (* Continuation for after we evaluate the loop body: depending the result of doing one loop iteration: @@ -1470,10 +1373,17 @@ let eval_loop_concrete (config : C.config) (eval_loop_body : st_cm_fun) : let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun = fun cf ctx -> + (* Compute a fresh loop id *) + let loop_id = C.fresh_loop_id () in (* 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_old config mctx (cf EndEnterLoop) ctx in + let fp_ctx = + compute_loop_entry_fixed_point config loop_id eval_loop_body ctx + in + (* Synthesize the end of the function - we simply match the context at the + loop entry with the fixed point: in the synthesized code, the function + will end with a call to the loop translation + *) + let end_expr = match_ctx_with_target config fp_ctx (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 *) @@ -1488,14 +1398,14 @@ 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_old config mctx (cf EndContinue) ctx + match_ctx_with_target config fp_ctx (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. *) raise (Failure "Unreachable") in - let loop_expr = eval_loop_body cf_loop mctx.ctx in + let loop_expr = eval_loop_body cf_loop fp_ctx in (* Put together *) S.synthesize_loop end_expr loop_expr @@ -1503,5 +1413,5 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : let eval_loop (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun = fun cf ctx -> match config.C.mode with - | ConcreteMode -> eval_loop_concrete config eval_loop_body cf ctx + | ConcreteMode -> eval_loop_concrete eval_loop_body cf ctx | SymbolicMode -> eval_loop_symbolic config eval_loop_body cf ctx |