From 506e9dc3f8f2759769c3293e9cbeba5d6fe79a31 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Mon, 27 May 2024 16:03:36 +0200 Subject: Add markers everywhere, do not use them yet --- compiler/InterpreterLoopsCore.ml | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'compiler/InterpreterLoopsCore.ml') diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index 991f259f..675dc544 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -65,7 +65,7 @@ module type PrimMatcher = sig val match_distinct_adts : eval_ctx -> eval_ctx -> ety -> adt_value -> adt_value -> typed_value - (** The span-value is the result of a match. + (** The meta-value is the result of a match. We take an additional function as input, which acts as a matcher over typed values, to be able to lookup the shared values and match them. @@ -158,8 +158,10 @@ module type PrimMatcher = sig (** Parameters: [ty0] + [pm0] [bid0] [ty1] + [pm1] [bid1] [ty]: result of matching ty0 and ty1 *) @@ -167,17 +169,21 @@ module type PrimMatcher = sig eval_ctx -> eval_ctx -> rty -> + proj_marker -> borrow_id -> rty -> + proj_marker -> borrow_id -> rty -> typed_avalue (** Parameters: [ty0] + [pm0] [bid0] [av0] [ty1] + [pm1] [bid1] [av1] [ty]: result of matching ty0 and ty1 @@ -187,9 +193,11 @@ module type PrimMatcher = sig eval_ctx -> eval_ctx -> rty -> + proj_marker -> borrow_id -> typed_avalue -> rty -> + proj_marker -> borrow_id -> typed_avalue -> rty -> @@ -198,10 +206,12 @@ module type PrimMatcher = sig (** Parameters: [ty0] + [pm0] [ids0] [v0] [av0] [ty1] + [pm1] [ids1] [v1] [av1] @@ -213,10 +223,12 @@ module type PrimMatcher = sig eval_ctx -> eval_ctx -> rty -> + proj_marker -> loan_id_set -> typed_value -> typed_avalue -> rty -> + proj_marker -> loan_id_set -> typed_value -> typed_avalue -> @@ -227,9 +239,11 @@ module type PrimMatcher = sig (** Parameters: [ty0] + [pm0] [id0] [av0] [ty1] + [pm1] [id1] [av1] [ty]: result of matching ty0 and ty1 @@ -239,9 +253,11 @@ module type PrimMatcher = sig eval_ctx -> eval_ctx -> rty -> + proj_marker -> borrow_id -> typed_avalue -> rty -> + proj_marker -> borrow_id -> typed_avalue -> rty -> -- cgit v1.2.3 From 445c566f11dcc9ba8c69a154902a12a18ba3a2aa Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 28 May 2024 14:28:40 +0200 Subject: Add type and set/map for marker and borrow id --- compiler/InterpreterLoopsCore.ml | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'compiler/InterpreterLoopsCore.ml') diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index 675dc544..9aee361d 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -26,6 +26,20 @@ type ctx_or_update = (eval_ctx, updt_env_kind) result (** Union Find *) module UF = UnionFind.Make (UnionFind.StoreMap) +type marker_borrow_id = proj_marker * BorrowId.id [@@deriving show, ord] + +module MarkerBorrowIdOrd = struct + type t = marker_borrow_id + + let compare = compare_marker_borrow_id + let to_string = show_marker_borrow_id + let pp_t = pp_marker_borrow_id + let show_t = show_marker_borrow_id +end + +module MarkerBorrowIdSet = Collections.MakeSet (MarkerBorrowIdOrd) +module MarkerBorrowIdMap = Collections.MakeMap (MarkerBorrowIdOrd) + (** A small utility - Rem.: some environments may be ill-formed (they may contain several times -- cgit v1.2.3 From 96d803a7aefe27d4401a336c426161d387987b63 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 28 May 2024 14:51:25 +0200 Subject: Compute marker information for borrow/loan maps --- compiler/InterpreterLoopsCore.ml | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) (limited to 'compiler/InterpreterLoopsCore.ml') diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index 9aee361d..23e05e06 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -40,6 +40,19 @@ end module MarkerBorrowIdSet = Collections.MakeSet (MarkerBorrowIdOrd) module MarkerBorrowIdMap = Collections.MakeMap (MarkerBorrowIdOrd) +module MarkerBorrowId : sig + type t + + module Set : Collections.Set with type elt = t + module Map : Collections.Map with type key = t +end +with type t = marker_borrow_id = struct + type t = marker_borrow_id + + module Set = MarkerBorrowIdSet + module Map = MarkerBorrowIdMap +end + (** A small utility - Rem.: some environments may be ill-formed (they may contain several times @@ -49,12 +62,12 @@ module MarkerBorrowIdMap = Collections.MakeMap (MarkerBorrowIdOrd) *) type abs_borrows_loans_maps = { abs_ids : AbstractionId.id list; - abs_to_borrows : BorrowId.Set.t AbstractionId.Map.t; - abs_to_loans : BorrowId.Set.t AbstractionId.Map.t; - abs_to_borrows_loans : BorrowId.Set.t AbstractionId.Map.t; - borrow_to_abs : AbstractionId.Set.t BorrowId.Map.t; - loan_to_abs : AbstractionId.Set.t BorrowId.Map.t; - borrow_loan_to_abs : AbstractionId.Set.t BorrowId.Map.t; + abs_to_borrows : MarkerBorrowId.Set.t AbstractionId.Map.t; + abs_to_loans : MarkerBorrowId.Set.t AbstractionId.Map.t; + abs_to_borrows_loans : MarkerBorrowId.Set.t AbstractionId.Map.t; + borrow_to_abs : AbstractionId.Set.t MarkerBorrowId.Map.t; + loan_to_abs : AbstractionId.Set.t MarkerBorrowId.Map.t; + borrow_loan_to_abs : AbstractionId.Set.t MarkerBorrowId.Map.t; } (** See {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} and [Matcher]. -- cgit v1.2.3 From ce8614be6bd96c51756bf5922b5dfd4c59650dd4 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Thu, 30 May 2024 12:33:05 +0200 Subject: Implement two phases of loops join + collapse --- compiler/InterpreterLoopsCore.ml | 27 --------------------------- 1 file changed, 27 deletions(-) (limited to 'compiler/InterpreterLoopsCore.ml') diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index 23e05e06..cd609ab0 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -26,33 +26,6 @@ type ctx_or_update = (eval_ctx, updt_env_kind) result (** Union Find *) module UF = UnionFind.Make (UnionFind.StoreMap) -type marker_borrow_id = proj_marker * BorrowId.id [@@deriving show, ord] - -module MarkerBorrowIdOrd = struct - type t = marker_borrow_id - - let compare = compare_marker_borrow_id - let to_string = show_marker_borrow_id - let pp_t = pp_marker_borrow_id - let show_t = show_marker_borrow_id -end - -module MarkerBorrowIdSet = Collections.MakeSet (MarkerBorrowIdOrd) -module MarkerBorrowIdMap = Collections.MakeMap (MarkerBorrowIdOrd) - -module MarkerBorrowId : sig - type t - - module Set : Collections.Set with type elt = t - module Map : Collections.Map with type key = t -end -with type t = marker_borrow_id = struct - type t = marker_borrow_id - - module Set = MarkerBorrowIdSet - module Map = MarkerBorrowIdMap -end - (** A small utility - Rem.: some environments may be ill-formed (they may contain several times -- cgit v1.2.3 From 52bcaf0cdd1c08ece0f9f09bdc0d32b753a2a00f Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 31 May 2024 11:55:51 +0200 Subject: Add markers when creating new abstractions because of a join with bottom --- compiler/InterpreterLoopsCore.ml | 44 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) (limited to 'compiler/InterpreterLoopsCore.ml') diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index cd609ab0..8d6caac4 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -429,3 +429,47 @@ let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets = } in ids + +(* Small utility: Add a projection marker to a typed avalue. + This can be used in combination with List.map to add markers to an entire abstraction +*) +let add_marker_avalue (span : Meta.span) (ctx : eval_ctx) (pm : proj_marker) + (av : typed_avalue) : typed_avalue = + let obj = + object + inherit [_] map_typed_avalue as super + + method! visit_borrow_content _ _ = + craise __FILE__ __LINE__ span "Unexpected borrow" + + method! visit_loan_content _ _ = + craise __FILE__ __LINE__ span "Unexpected loan" + + method! visit_symbolic_value _ sv = + sanity_check __FILE__ __LINE__ + (not (symbolic_value_has_borrows ctx sv)) + span; + sv + + method! visit_aloan_content env lc = + match lc with + | AMutLoan (pm0, bid, av) -> + sanity_check __FILE__ __LINE__ (pm0 = PNone) span; + super#visit_aloan_content env (AMutLoan (pm, bid, av)) + | ASharedLoan (pm0, bids, av, child) -> + sanity_check __FILE__ __LINE__ (pm0 = PNone) span; + super#visit_aloan_content env (ASharedLoan (pm, bids, av, child)) + | _ -> craise __FILE__ __LINE__ span "Unsupported yet" + + method! visit_aborrow_content env bc = + match bc with + | AMutBorrow (pm0, bid, av) -> + sanity_check __FILE__ __LINE__ (pm0 = PNone) span; + super#visit_aborrow_content env (AMutBorrow (pm, bid, av)) + | ASharedBorrow (pm0, bid) -> + sanity_check __FILE__ __LINE__ (pm0 = PNone) span; + super#visit_aborrow_content env (ASharedBorrow (pm, bid)) + | _ -> craise __FILE__ __LINE__ span "Unsupported yet" + end + in + obj#visit_typed_avalue () av -- cgit v1.2.3 From 9aa328a70011d2784a943830bffabc600caba4ab Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 3 Jun 2024 12:52:04 +0200 Subject: Cleanup a bit --- compiler/InterpreterLoopsCore.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'compiler/InterpreterLoopsCore.ml') diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index 8d6caac4..4149b19e 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -26,21 +26,21 @@ type ctx_or_update = (eval_ctx, updt_env_kind) result (** Union Find *) module UF = UnionFind.Make (UnionFind.StoreMap) -(** A small utility - - - Rem.: some environments may be ill-formed (they may contain several times - the same loan or borrow - this happens for instance when merging - environments). This is the reason why we use sets in some places (for - instance, [borrow_to_abs] maps to a *set* of ids). +(** A small utility. + + Remark: we use projection markers, meaning we compute maps from/to + pairs of (projection marker, borrow/loan id). This allows us to use + this utility during a reduce phase (when we simplify the environment + and all markers should be [PNone]) as well as during a collapse (where + we actually have markers because we performed a join and are progressively + transforming the environment to get rid of those markers). *) type abs_borrows_loans_maps = { abs_ids : AbstractionId.id list; abs_to_borrows : MarkerBorrowId.Set.t AbstractionId.Map.t; abs_to_loans : MarkerBorrowId.Set.t AbstractionId.Map.t; - abs_to_borrows_loans : MarkerBorrowId.Set.t AbstractionId.Map.t; borrow_to_abs : AbstractionId.Set.t MarkerBorrowId.Map.t; loan_to_abs : AbstractionId.Set.t MarkerBorrowId.Map.t; - borrow_loan_to_abs : AbstractionId.Set.t MarkerBorrowId.Map.t; } (** See {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} and [Matcher]. -- cgit v1.2.3 From 67ef9b5316b6550c3386ae095197ea513ed7dfbb Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 3 Jun 2024 14:56:42 +0200 Subject: Cleanup a bit --- compiler/InterpreterLoopsCore.ml | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) (limited to 'compiler/InterpreterLoopsCore.ml') diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index 4149b19e..df808385 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -430,11 +430,11 @@ let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets = in ids -(* Small utility: Add a projection marker to a typed avalue. - This can be used in combination with List.map to add markers to an entire abstraction -*) -let add_marker_avalue (span : Meta.span) (ctx : eval_ctx) (pm : proj_marker) - (av : typed_avalue) : typed_avalue = +(** Small utility: add a projection marker to a typed avalue. + This can be used in combination with List.map to add markers to an entire abstraction + *) +let typed_avalue_add_marker (span : Meta.span) (ctx : eval_ctx) + (pm : proj_marker) (av : typed_avalue) : typed_avalue = let obj = object inherit [_] map_typed_avalue as super @@ -473,3 +473,13 @@ let add_marker_avalue (span : Meta.span) (ctx : eval_ctx) (pm : proj_marker) end in obj#visit_typed_avalue () av + +(** Small utility: add a projection marker to an abstraction. + This can be used in combination with List.map to add markers to an entire abstraction + *) +let abs_add_marker (span : Meta.span) (ctx : eval_ctx) (pm : proj_marker) + (abs : abs) : abs = + { + abs with + avalues = List.map (typed_avalue_add_marker span ctx pm) abs.avalues; + } -- cgit v1.2.3