summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterLoopsCore.ml16
-rw-r--r--compiler/InterpreterLoopsJoinCtxs.ml16
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml142
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.mli4
4 files changed, 87 insertions, 91 deletions
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].
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index b58d1b3e..ce874992 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -185,15 +185,13 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option)
(* Explore all the *new* abstractions, and compute various maps *)
let explore (abs : abs) = is_fresh_abs_id abs.abs_id in
- let ids_maps = compute_abs_borrows_loans_maps span true explore env in
+ let ids_maps = compute_abs_borrows_loans_maps span explore env in
let {
abs_ids;
abs_to_borrows;
abs_to_loans = _;
- abs_to_borrows_loans = _;
borrow_to_abs = _;
loan_to_abs;
- borrow_loan_to_abs = _;
} =
ids_maps
in
@@ -338,16 +336,8 @@ let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id)
(* Explore all the *new* abstractions, and compute various maps *)
let explore (abs : abs) = is_fresh_abs_id abs.abs_id in
- let ids_maps = compute_abs_borrows_loans_maps span false explore ctx0.env in
- let {
- abs_ids;
- abs_to_borrows;
- abs_to_loans;
- abs_to_borrows_loans = _;
- borrow_to_abs;
- loan_to_abs;
- borrow_loan_to_abs = _;
- } =
+ let ids_maps = compute_abs_borrows_loans_maps span explore ctx0.env in
+ let { abs_ids; abs_to_borrows; abs_to_loans; borrow_to_abs; loan_to_abs } =
ids_maps
in
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 713f462b..bc39d5ec 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -20,32 +20,28 @@ module S = SynthesizeSymbolic
(** The local logger *)
let log = Logging.loops_match_ctxs_log
-let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
- (explore : abs -> bool) (env : env) : abs_borrows_loans_maps =
+let compute_abs_borrows_loans_maps (span : Meta.span) (explore : abs -> bool)
+ (env : env) : abs_borrows_loans_maps =
let abs_ids = ref [] in
let abs_to_borrows = ref AbstractionId.Map.empty in
let abs_to_loans = ref AbstractionId.Map.empty in
- let abs_to_borrows_loans = ref AbstractionId.Map.empty in
let borrow_to_abs = ref MarkerBorrowId.Map.empty in
let loan_to_abs = ref MarkerBorrowId.Map.empty in
- let borrow_loan_to_abs = ref MarkerBorrowId.Map.empty in
let module R (M : Collections.Map) (S : Collections.Set) = struct
(*
[check_singleton_sets]: check that the mapping maps to a singleton.
- [check_not_already_registered]: check if the mapping was not already registered.
+ We need this because to tweak the behavior of the sanity checks because
+ of the following cases:
+ - when computing the map from borrow ids (with marker) to the region
+ abstractions they belong to, the marked borrow ids can map to a single
+ region abstraction, i.e., to a singleton set of region abstraction ids
+ - however, when computing the mapping from region abstractions to
+ the borrow ids they contain, this time we do map abstraction ids
+ to sets which can compute strictly more than one value
*)
- let register_mapping (check_singleton_sets : bool)
- (check_not_already_registered : bool) (map : S.t M.t ref) (id0 : M.key)
- (id1 : S.elt) : unit =
- (* Sanity check *)
- (if check_singleton_sets || check_not_already_registered then
- match M.find_opt id0 !map with
- | None -> ()
- | Some set ->
- sanity_check __FILE__ __LINE__
- ((not check_not_already_registered) || not (S.mem id1 set))
- span);
+ let register_mapping (check_singleton_sets : bool) (map : S.t M.t ref)
+ (id0 : M.key) (id1 : S.elt) : unit =
(* Update the mapping *)
map :=
M.update id0
@@ -53,11 +49,11 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
match ids with
| None -> Some (S.singleton id1)
| Some ids ->
- (* Sanity check *)
+ (* Check that we are allowed to map id0 to a set which is not
+ a singleton *)
sanity_check __FILE__ __LINE__ (not check_singleton_sets) span;
- sanity_check __FILE__ __LINE__
- ((not check_not_already_registered) || not (S.mem id1 ids))
- span;
+ (* Check that the mapping was not already registered *)
+ sanity_check __FILE__ __LINE__ (not (S.mem id1 ids)) span;
(* Update *)
Some (S.add id1 ids))
!map
@@ -65,20 +61,13 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
let module RAbsBorrow = R (AbstractionId.Map) (MarkerBorrowId.Set) in
let module RBorrowAbs = R (MarkerBorrowId.Map) (AbstractionId.Set) in
let register_borrow_id abs_id pm bid =
- RAbsBorrow.register_mapping false no_duplicates abs_to_borrows abs_id
- (pm, bid);
- RAbsBorrow.register_mapping false false abs_to_borrows_loans abs_id (pm, bid);
- RBorrowAbs.register_mapping no_duplicates no_duplicates borrow_to_abs
- (pm, bid) abs_id;
- RBorrowAbs.register_mapping false false borrow_loan_to_abs (pm, bid) abs_id
+ RAbsBorrow.register_mapping false abs_to_borrows abs_id (pm, bid);
+ RBorrowAbs.register_mapping true borrow_to_abs (pm, bid) abs_id
in
let register_loan_id abs_id pm bid =
- RAbsBorrow.register_mapping false no_duplicates abs_to_loans abs_id (pm, bid);
- RAbsBorrow.register_mapping false false abs_to_borrows_loans abs_id (pm, bid);
- RBorrowAbs.register_mapping no_duplicates no_duplicates loan_to_abs
- (pm, bid) abs_id;
- RBorrowAbs.register_mapping false false borrow_loan_to_abs (pm, bid) abs_id
+ RAbsBorrow.register_mapping false abs_to_loans abs_id (pm, bid);
+ RBorrowAbs.register_mapping true loan_to_abs (pm, bid) abs_id
in
let explore_abs =
@@ -87,10 +76,19 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
(** Make sure we don't register the ignored ids *)
method! visit_aloan_content (abs_id, pm) lc =
+ sanity_check __FILE__ __LINE__ (pm = PNone) span;
match lc with
- | AMutLoan (pm, _, _) | ASharedLoan (pm, _, _, _) ->
- (* Process those normally *)
- super#visit_aloan_content (abs_id, pm) lc
+ | AMutLoan (npm, lid, child) ->
+ (* Add the current marker when visiting the loan id *)
+ self#visit_loan_id (abs_id, npm) lid;
+ (* Recurse with the old marker *)
+ super#visit_typed_avalue (abs_id, pm) child
+ | ASharedLoan (npm, lids, sv, child) ->
+ (* Add the current marker when visiting the loan ids and the shared value *)
+ self#visit_loan_id_set (abs_id, npm) lids;
+ self#visit_typed_value (abs_id, npm) sv;
+ (* Recurse with the old marker *)
+ self#visit_typed_avalue (abs_id, pm) child
| AIgnoredMutLoan (_, child)
| AEndedIgnoredMutLoan { child; given_back = _; given_back_span = _ }
| AIgnoredSharedLoan child ->
@@ -102,10 +100,16 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
(** Make sure we don't register the ignored ids *)
method! visit_aborrow_content (abs_id, pm) bc =
+ sanity_check __FILE__ __LINE__ (pm = PNone) span;
match bc with
- | AMutBorrow (pm, _, _) | ASharedBorrow (pm, _) ->
- (* Add the current marker, and process them recursively *)
- super#visit_aborrow_content (abs_id, pm) bc
+ | AMutBorrow (npm, bid, child) ->
+ (* Add the current marker when visiting the borrow id *)
+ self#visit_borrow_id (abs_id, npm) bid;
+ (* Recurse with the old marker *)
+ self#visit_typed_avalue (abs_id, pm) child
+ | ASharedBorrow (npm, bid) ->
+ (* Add the current marker when visiting the borrow id *)
+ self#visit_borrow_id (abs_id, npm) bid
| AProjSharedBorrow _ ->
sanity_check __FILE__ __LINE__ (pm = PNone) span;
(* Process those normally *)
@@ -147,10 +151,8 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
abs_ids = !abs_ids;
abs_to_borrows = !abs_to_borrows;
abs_to_loans = !abs_to_loans;
- abs_to_borrows_loans = !abs_to_borrows_loans;
borrow_to_abs = !borrow_to_abs;
loan_to_abs = !loan_to_abs;
- borrow_loan_to_abs = !borrow_loan_to_abs;
}
(** Match two types during a join.
@@ -557,7 +559,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
an abstraction:
{[
- { MB bid0, ML nbid } // where nbid fresh
+ { MB bid0, ML bid' } // where bid' fresh
]}
and we use bid' for the borrow id that we return.
@@ -565,7 +567,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
We do this because we want to make sure that, whenever a mutably
borrowed value is modified in a loop iteration, then there is
a fresh abstraction between this borrowed value and the fixed
- abstractions.
+ abstractions (this is tantamount to introducing a reborrow).
Example:
========
@@ -596,6 +598,15 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
to say [unit]) while the backward loop function gives back a new value
for [v] (i.e., a new symbolic value which will replace [s0]).
+ By introducing the fresh region abstraction wet get:
+ {[
+ abs'0 { ML l0 } // input abstraction
+ abs'1 { MB l0, ML l1 } // fresh abstraction
+ v -> MB l1 s1
+ i -> 0
+ ]}
+
+
In the future, we will also compute joins at the *loop exits*: when we
do so, we won't introduce reborrows like above: the forward loop function
will update [v], while the backward loop function will return nothing.
@@ -613,7 +624,8 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
let kind = RMut in
let bv_ty = bv.ty in
- sanity_check __FILE__ __LINE__ (ty_no_regions bv_ty) span;
+ cassert __FILE__ __LINE__ (ty_no_regions bv_ty) span
+ "Nested borrows are not supported yet";
let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
let borrow_av =
@@ -651,9 +663,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(nbid, bv))
else
(* We replace bid0 and bid1 with a fresh borrow id, and introduce
- an abstraction which links all of them:
+ an abstraction which links all of them. This time we have to introduce
+ markers:
{[
- { MB bid0, MB bid1, ML bid2 }
+ { |MB bid0|, ︙MB bid1︙, ML bid2 }
]}
*)
let rid = fresh_region_id () in
@@ -761,24 +774,16 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(* Check that:
- there are no borrows in the symbolic value
- there are no borrows in the "regular" value
- If there are loans in the regular value, raise an exception.
*)
let type_infos = ctx0.type_ctx.type_infos in
- cassert __FILE__ __LINE__
+ sanity_check __FILE__ __LINE__
(not (ty_has_borrows type_infos sv.sv_ty))
- span
- "Check that:\n\
- \ - there are no borrows in the symbolic value\n\
- \ - there are no borrows in the \"regular\" value\n\
- \ If there are loans in the regular value, raise an exception.";
- cassert __FILE__ __LINE__
+ span;
+ sanity_check __FILE__ __LINE__
(not (ValuesUtils.value_has_borrows type_infos v.value))
- span
- "Check that:\n\
- \ - there are no borrows in the symbolic value\n\
- \ - there are no borrows in the \"regular\" value\n\
- \ If there are loans in the regular value, raise an exception.";
+ span;
let value_is_left = not left in
+ (* If there are loans in the regular value, raise an exception. *)
(match InterpreterBorrowsCore.get_first_loan_in_value v with
| None -> ()
| Some (VSharedLoan (ids, _)) ->
@@ -798,13 +803,13 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
then mk_bottom span sv.sv_ty
else mk_fresh_symbolic_typed_value span sv.sv_ty
- let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool)
- (v : typed_value) : typed_value =
+ let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx)
+ (bottom_is_left : bool) (v : typed_value) : typed_value =
+ let value_is_left = not bottom_is_left in
(* If there are outer loans in the non-bottom value, raise an exception.
Otherwise, convert it to an abstraction and return [Bottom].
*)
let with_borrows = false in
- let value_is_left = not left in
match
InterpreterBorrowsCore.get_first_outer_loan_or_borrow_in_value
with_borrows v
@@ -821,8 +826,6 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
if value_is_left then raise (ValueMatchFailure (LoanInLeft id))
else raise (ValueMatchFailure (LoanInRight id)))
| None ->
- (* *)
-
(* Convert the value to an abstraction *)
let abs_kind : abs_kind = Loop (S.loop_id, None, LoopSynthInput) in
let can_end = true in
@@ -833,16 +836,13 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
destructure_shared_values ctx v
in
(* Add a marker to the abstraction indicating the provenance of the value *)
+ let pm = if value_is_left then PLeft else PRight in
let absl =
List.map
(fun abs ->
{
abs with
- avalues =
- List.map
- (add_marker_avalue span ctx0
- (if value_is_left then PLeft else PRight))
- abs.avalues;
+ avalues = List.map (add_marker_avalue span ctx0 pm) abs.avalues;
})
absl
in
@@ -1246,6 +1246,8 @@ struct
let match_ashared_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 pm0 bid0 _ty1 pm1
bid1 ty =
+ (* We are checking whether that two environments are equivalent:
+ there shouldn't be any projection markers *)
sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
let bid = match_borrow_id bid0 bid1 in
let value = ABorrow (ASharedBorrow (PNone, bid)) in
@@ -1253,6 +1255,8 @@ struct
let match_amut_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 pm0 bid0 _av0 _ty1
pm1 bid1 _av1 ty av =
+ (* We are checking whether that two environments are equivalent:
+ there shouldn't be any projection markers *)
sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
let bid = match_borrow_id bid0 bid1 in
let value = ABorrow (AMutBorrow (PNone, bid, av)) in
@@ -1260,6 +1264,8 @@ struct
let match_ashared_loans (_ : eval_ctx) (_ : eval_ctx) _ty0 pm0 ids0 _v0 _av0
_ty1 pm1 ids1 _v1 _av1 ty v av =
+ (* We are checking whether that two environments are equivalent:
+ there shouldn't be any projection markers *)
sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
let bids = match_loan_ids ids0 ids1 in
let value = ALoan (ASharedLoan (PNone, bids, v, av)) in
@@ -1267,6 +1273,8 @@ struct
let match_amut_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 pm0 id0 _av0
_ty1 pm1 id1 _av1 ty av =
+ (* We are checking whether that two environments are equivalent:
+ there shouldn't be any projection markers *)
sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
log#ldebug
(lazy
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index 7d214cb6..cd807358 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -13,13 +13,11 @@ open InterpreterLoopsCore
(** Compute various maps linking the abstractions and the borrows/loans they contain.
Parameters:
- - [no_duplicates]: checks that borrows/loans are not referenced more than once
- (see the documentation for {!type:InterpreterLoopsCore.abs_borrows_loans_maps}).
- [explore]: this function is used to filter abstractions.
- [env]
*)
val compute_abs_borrows_loans_maps :
- Meta.span -> bool -> (abs -> bool) -> env -> abs_borrows_loans_maps
+ Meta.span -> (abs -> bool) -> env -> abs_borrows_loans_maps
(** Generic functor to implement matching functions between values, environments,
etc.