summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-12-02 00:00:42 +0100
committerSon HO2023-02-03 11:21:46 +0100
commitaef15fb2f961df4f935c659d85ff9982fc446cc2 (patch)
tree936457fa60ac1989cb3bf978fbc7785e3df2bd0e
parenta4743c7176b7d85aa2b414748dedb089fd361484 (diff)
Make more fixes
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterBorrows.ml102
-rw-r--r--compiler/InterpreterLoops.ml206
2 files changed, 222 insertions, 86 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index bb843714..eb3b9898 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1748,9 +1748,8 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
let push_abs (r_id : T.RegionId.id) (avalues : V.typed_avalue list) : unit =
if avalues = [] then ()
else
- (* Reverse the list of avalues *)
- let avalues = List.rev avalues in
- (* Create the abs *)
+ (* Create the abs - note that we keep the order of the avalues as it is
+ (unlike the environments) *)
let abs =
{
V.abs_id = C.fresh_abstraction_id ();
@@ -2121,6 +2120,11 @@ type merge_duplicates_funcs = {
let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
(merge_funs : merge_duplicates_funcs option) (ctx : C.eval_ctx)
(abs0 : V.abs) (abs1 : V.abs) : V.abs =
+ log#ldebug
+ (lazy
+ ("merge_abstractions_aux:\n- abs0:\n" ^ abs_to_string ctx abs0
+ ^ "\n\n- abs1:\n" ^ abs_to_string ctx abs1));
+
(* Check that the abstractions are destructured *)
if !Config.check_invariants then (
let destructure_shared_values = true in
@@ -2277,48 +2281,67 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
raise (Failure "Unreachable")
in
- let borrows_loans = List.append borrows_loans0 borrows_loans1 in
- (* Iterate over all the borrows/loans ids found in teh abstractions *)
+ (* Note that we first explore the borrows/loans of [abs1], because we
+ want to merge *into* this abstraction, and as a consequence we want to
+ preserve its structure as much as we can *)
+ let borrows_loans = List.append borrows_loans1 borrows_loans0 in
+ (* Iterate over all the borrows/loans ids found in the abstractions *)
List.iter
(fun bl ->
match bl with
- | BorrowId bid -> (
- (* Check if the borrow has already been merged *)
- assert (not (borrow_is_merged bid));
- set_borrow_as_merged bid;
- (* Check if we need to filter it *)
- match filter_bid bid with
- | None -> ()
- | Some bid ->
- (* Lookup the contents *)
- let bc0 = V.BorrowId.Map.find_opt bid borrow_to_content0 in
- let bc1 = V.BorrowId.Map.find_opt bid borrow_to_content1 in
- (* Merge *)
- let av : V.typed_avalue =
- match (bc0, bc1) with
- | None, Some bc | Some bc, None -> (
- match bc with
- | Concrete (_, _) ->
- (* This can happen only in case of nested borrows -
- a concrete borrow can only happen inside a shared
- loan
- *)
- raise (Failure "Unreachable")
- | Abstract (ty, bc) -> { V.value = V.ABorrow bc; ty })
- | Some bc0, Some bc1 ->
- assert (merge_funs <> None);
- merge_g_borrow_contents bc0 bc1
- | None, None -> raise (Failure "Unreachable")
- in
- push_avalue av)
- | LoanId bid -> (
+ | BorrowId bid ->
+ log#ldebug
+ (lazy
+ ("merge_abstractions_aux: merging borrow "
+ ^ V.BorrowId.to_string bid));
+
+ (* Check if the borrow has already been merged - this can happen
+ because we go through all the borrows/loans in [abs0] *then*
+ all the borrows/loans in [abs1], and there may be duplicates
+ between the two *)
+ if borrow_is_merged bid then ()
+ else (
+ set_borrow_as_merged bid;
+ (* Check if we need to filter it *)
+ match filter_bid bid with
+ | None -> ()
+ | Some bid ->
+ (* Lookup the contents *)
+ let bc0 = V.BorrowId.Map.find_opt bid borrow_to_content0 in
+ let bc1 = V.BorrowId.Map.find_opt bid borrow_to_content1 in
+ (* Merge *)
+ let av : V.typed_avalue =
+ match (bc0, bc1) with
+ | None, Some bc | Some bc, None -> (
+ match bc with
+ | Concrete (_, _) ->
+ (* This can happen only in case of nested borrows -
+ a concrete borrow can only happen inside a shared
+ loan
+ *)
+ raise (Failure "Unreachable")
+ | Abstract (ty, bc) -> { V.value = V.ABorrow bc; ty })
+ | Some bc0, Some bc1 ->
+ assert (merge_funs <> None);
+ merge_g_borrow_contents bc0 bc1
+ | None, None -> raise (Failure "Unreachable")
+ in
+ push_avalue av)
+ | LoanId bid ->
if
(* Check if the loan has already been treated - it can happen
- because shared loans contain sets of borrows.
+ for the same reason as for borrows, and also because shared
+ loans contain sets of borrows (meaning that when taking care
+ of one loan, we can merge several other loans at once).
*)
loan_is_merged bid
then ()
- else
+ else (
+ log#ldebug
+ (lazy
+ ("merge_abstractions_aux: merging loan "
+ ^ V.BorrowId.to_string bid));
+
(* Check if we need to filter it *)
match filter_bid bid with
| None -> ()
@@ -2359,8 +2382,9 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
push_avalue av))
borrows_loans;
- (* Note that we *don't* reverse the avalues *)
- let avalues = !avalues in
+ (* Reverse the avalues (we visited the loans/borrows in order, but pushed
+ new values at the beggining of the stack of avalues) *)
+ let avalues = List.rev !avalues in
(* Filter the regions *)
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 2fc474fc..70a5f1bf 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -237,9 +237,7 @@ let collapse_ctx (loop_id : V.LoopId.id)
log#ldebug
(lazy
("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
- ^ "\n\n- ctx0:\n"
- ^ eval_ctx_to_string_no_filter ctx0
- ^ "\n\n"));
+ ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ctx0 ^ "\n\n"));
let abs_kind = V.Loop loop_id in
let can_end = false in
@@ -250,9 +248,8 @@ let collapse_ctx (loop_id : V.LoopId.id)
let is_fresh_did (id : C.DummyVarId.id) : bool =
not (C.DummyVarId.Set.mem id old_ids.dids)
in
- (* 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) *)
+ (* Convert the dummy values to abstractions (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 =
@@ -271,6 +268,12 @@ let collapse_ctx (loop_id : V.LoopId.id)
else [ ee ])
ctx0.env)
in
+ log#ldebug
+ (lazy
+ ("collapse_ctx: after converting values to abstractions:\n"
+ ^ show_ids_sets old_ids ^ "\n\n- ctx:\n"
+ ^ eval_ctx_to_string { ctx0 with env }
+ ^ "\n\n"));
(* Explore all the *new* abstractions, and compute various maps *)
let explore (abs : V.abs) = is_fresh_abs_id abs.abs_id in
@@ -591,17 +594,20 @@ module Match (M : Matcher) = struct
let bc =
match (bc0, bc1) with
| SharedBorrow (mv0, bid0), SharedBorrow (mv1, bid1) ->
- (* 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.
+ (* Not completely sure what to do with the meta-value, as we use
+ it for the translation. TODO: remove meta-values from shared borrows?
+
+ 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.
*)
+ assert (not (value_has_borrows ctx mv0.V.value));
+ assert (not (value_has_borrows ctx mv1.V.value));
let mv = match_rec mv0 mv1 in
- assert (not (value_has_borrows ctx mv.V.value));
let mv, bid = M.match_shared_borrows ty mv bid0 bid1 in
V.SharedBorrow (mv, bid)
| MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) ->
@@ -672,6 +678,13 @@ module Match (M : Matcher) = struct
*)
and match_typed_avalues (ctx : C.eval_ctx) (v0 : V.typed_avalue)
(v1 : V.typed_avalue) : V.typed_avalue =
+ log#ldebug
+ (lazy
+ ("match_typed_avalues:\n- value0: "
+ ^ typed_avalue_to_string ctx v0
+ ^ "\n- value1: "
+ ^ typed_avalue_to_string ctx v1));
+
let match_rec = match_typed_values ctx in
let match_arec = match_typed_avalues ctx in
let ty = M.match_rtys v0.V.ty v1.V.ty in
@@ -691,14 +704,19 @@ module Match (M : Matcher) = struct
{ V.value; ty }
else (* Merge *)
M.match_distinct_aadts v0.V.ty av0 v1.V.ty av1 ty
- | ABottom, ABottom -> v0
+ | ABottom, ABottom -> mk_abottom ty
+ | AIgnored, AIgnored -> mk_aignored ty
| ABorrow bc0, ABorrow bc1 -> (
match (bc0, bc1) with
| ASharedBorrow bid0, ASharedBorrow bid1 ->
M.match_ashared_borrows v0.V.ty bid0 v1.V.ty bid1 ty
| AMutBorrow (mv0, bid0, av0), AMutBorrow (mv1, bid1, av1) ->
- (* Not sure what to do with the meta-value *)
- let mv = match_rec mv0 mv1 in
+ (* The meta-value should be the value consumed by the abstracion.
+ This only makes sense if the abstraction was introduced because
+ of a function call (we use it for the translation).
+ TODO: make it optional?
+ *)
+ let mv = mk_bottom mv0.V.ty in
let av = match_arec av0 av1 in
M.match_amut_borrows v0.V.ty mv0 bid0 av0 v1.V.ty mv1 bid1 av1 ty mv
av
@@ -1051,8 +1069,34 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets)
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
+ (* TODO: why not simply call: M.match_type_avalues? (or move this code to
+ MakeJoinMatcher?) *)
+ let merge_amut_borrows id ty0 (mv0 : V.typed_value) child0 _ty1
+ (mv1 : V.typed_value) child1 =
+ (* Sanity checks *)
+ assert (is_aignored child0.V.value);
+ assert (is_aignored child1.V.value);
+ assert (mv0.V.ty = mv1.V.ty);
+
+ (* Same remarks as for [merge_amut_loans] *)
+ let ty = ty0 in
+ let child = child0 in
+ let mv = mk_bottom mv0.ty in
+ let value = V.ABorrow (V.AMutBorrow (mv, id, child)) in
+ { V.value; ty }
+ in
+
+ let merge_ashared_borrows id ty0 ty1 =
+ (* Sanity checks *)
+ assert (not (ty_has_borrows ctx.type_context.type_infos ty0));
+ assert (not (ty_has_borrows ctx.type_context.type_infos ty1));
+
+ (* Same remarks as for [merge_amut_loans] *)
+ let ty = ty0 in
+ let value = V.ABorrow (V.ASharedBorrow id) in
+ { V.value; ty }
+ in
+
let merge_amut_loans id ty0 child0 _ty1 child1 =
(* Sanity checks *)
assert (is_aignored child0.V.value);
@@ -1327,6 +1371,7 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
(* Very annoying: functors only take modules as inputs... *)
module type MatchCheckEquivState = sig
+ val ctx : C.eval_ctx
val rid_map : T.RegionId.InjSubst.t ref
val bid_map : V.BorrowId.InjSubst.t ref
val sid_map : V.SymbolicValueId.InjSubst.t ref
@@ -1474,7 +1519,14 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
let value = V.ALoan (V.AMutLoan (id, av)) in
{ V.value; ty }
- let match_avalues _ _ = raise Distinct
+ let match_avalues v0 v1 =
+ log#ldebug
+ (lazy
+ ("avalues don't match:\n- v0: "
+ ^ typed_avalue_to_string S.ctx v0
+ ^ "\n- v1: "
+ ^ typed_avalue_to_string S.ctx v1));
+ raise Distinct
end
(** Compute whether two contexts are equivalent modulo an identifier substitution.
@@ -1524,6 +1576,7 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
in
let module S : MatchCheckEquivState = struct
+ let ctx = ctx0
let rid_map = rid_map
let bid_map = bid_map
let sid_map = sid_map
@@ -1585,6 +1638,8 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
let _ = CEM.match_aidl original_parents0 original_parents1 in
let _ = CEM.match_rids regions0 regions1 in
let _ = CEM.match_rids ancestors_regions0 ancestors_regions1 in
+
+ log#ldebug (lazy "match_abstractions: matching values");
let _ =
List.map
(fun (v0, v1) -> M.match_typed_avalues ctx v0 v1)
@@ -1598,7 +1653,15 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
log#ldebug
(lazy
("ctxs_are_equivalent: match_envs:\n\n- fixed_ids:\n"
- ^ show_ids_sets fixed_ids ^ "\n\n- ctx0:\n"
+ ^ show_ids_sets fixed_ids ^ "\n\n- rid_map: "
+ ^ T.RegionId.InjSubst.show_t !rid_map
+ ^ "\n- bid_map: "
+ ^ V.BorrowId.InjSubst.show_t !bid_map
+ ^ "\n- sid_map: "
+ ^ V.SymbolicValueId.InjSubst.show_t !sid_map
+ ^ "\n- aid_map: "
+ ^ V.AbstractionId.InjSubst.show_t !aid_map
+ ^ "\n\n- ctx0:\n"
^ eval_ctx_to_string_no_filter { ctx0 with env = List.rev env0 }
^ "\n\n- ctx1:\n"
^ eval_ctx_to_string_no_filter { ctx1 with env = List.rev env1 }
@@ -1608,8 +1671,8 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
| ( C.Var (C.DummyBinder b0, v0) :: 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 *)
+ must be the same and their values equal (and the borrows/loans/symbolic
+ values they reference must be fixed) *)
if C.DummyVarId.Set.mem b0 fixed_ids.dids then (
(* Fixed values: the values must be equal *)
assert (b0 = b1);
@@ -1648,7 +1711,7 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
(* Done *)
()
| _ ->
- (* The elements don't match: we are not in the prefix anymore *)
+ (* The elements don't match *)
raise Distinct
in
@@ -1677,21 +1740,8 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
we return those updated environments, and the joined environment.
*)
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 * 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 = compute_context_ids old_ctx in
- let new_ids = 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
-
+ (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (old_ctx : C.eval_ctx)
+ (ctxl : C.eval_ctx list) : (C.eval_ctx * C.eval_ctx list) * C.eval_ctx =
(* # Join with the new contexts, one by one
For every context, we repeteadly attempt to join it with the current
@@ -1702,7 +1752,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) : C.eval_ctx =
- match join_ctxs loop_id old_ids !joined_ctx ctx with
+ match join_ctxs loop_id fixed_ids !joined_ctx ctx with
| Ok nctx ->
joined_ctx := nctx;
ctx
@@ -1719,16 +1769,41 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
join_one_aux ctx
in
let join_one (ctx : C.eval_ctx) : C.eval_ctx =
+ log#ldebug
+ (lazy
+ ("loop_join_origin_with_continue_ctxs:join_one: initial ctx:\n"
+ ^ eval_ctx_to_string ctx));
+
(* Destructure the abstractions introduced in the new context *)
- let ctx = destructure_new_abs loop_id old_ids.aids ctx in
+ let ctx = destructure_new_abs loop_id fixed_ids.aids ctx in
+ log#ldebug
+ (lazy
+ ("loop_join_origin_with_continue_ctxs:join_one: after destructure:\n"
+ ^ eval_ctx_to_string ctx));
+
(* Collapse the context we want to add to the join *)
- let ctx = collapse_ctx loop_id None old_ids ctx in
+ let ctx = collapse_ctx loop_id None fixed_ids ctx in
+ log#ldebug
+ (lazy
+ ("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n"
+ ^ eval_ctx_to_string ctx));
+
(* Join the two contexts *)
let ctx1 = join_one_aux ctx in
+ log#ldebug
+ (lazy
+ ("loop_join_origin_with_continue_ctxs:join_one: after join:\n"
+ ^ eval_ctx_to_string ctx1));
+
(* 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;
+ joined_ctx := collapse_ctx_with_merge loop_id fixed_ids !joined_ctx;
+ log#ldebug
+ (lazy
+ ("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n"
+ ^ eval_ctx_to_string !joined_ctx));
+
(* Sanity check *)
if !Config.check_invariants then Invariants.check_invariants !joined_ctx;
(* Return *)
@@ -1765,10 +1840,39 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
(* We don't support nested loops for now *)
raise (Failure "Nested loops are not supported for now")
in
+
+ (* The fixed ids. They are the ids of the original ctx, after we ended
+ the borrows/loans which end during the first loop iteration (we do
+ one loop iteration, then set it to [Some].
+ *)
+ let fixed_ids = ref None in
+
(* Join the contexts at the loop entry *)
let join_ctxs (ctx0 : C.eval_ctx) : C.eval_ctx =
+ (* If this is the first iteration, end the borrows/loans/abs which
+ appear in ctx0 and not in the other contexts, then compute the
+ set of fixed ids. This means those borrows/loans have to end
+ in the loop, and we rather end them *before* the loop. *)
+ let ctx0 =
+ match !fixed_ids with
+ | Some _ -> ctx0
+ | None ->
+ let old_ids = compute_context_ids ctx0 in
+ let new_ids = compute_contexts_ids !ctxs 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 ctx0 = InterpreterBorrows.end_borrows_no_synth config bids ctx0 in
+ let ctx0 =
+ InterpreterBorrows.end_abstractions_no_synth config aids ctx0
+ in
+ fixed_ids := Some (compute_context_ids ctx0);
+ ctx0
+ in
+
+ let fixed_ids = Option.get !fixed_ids in
let (ctx0', _), ctx1 =
- loop_join_origin_with_continue_ctxs config loop_id ctx0 !ctxs
+ loop_join_origin_with_continue_ctxs config loop_id fixed_ids ctx0 !ctxs
in
ctxs := [];
if !ctx_upon_entry = None then ctx_upon_entry := Some ctx0';
@@ -1777,9 +1881,17 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
(* Check if two contexts are equivalent - modulo alpha conversion on the
existentially quantified borrows/abstractions/symbolic values *)
let equiv_ctxs (ctx1 : C.eval_ctx) (ctx2 : C.eval_ctx) : bool =
+ (* Compute the set of fixed ids - for the symbolic ids, we compute the
+ intersection of ids between the original environment and [ctx1]
+ and [ctx2] *)
let fixed_ids = compute_context_ids (Option.get !ctx_upon_entry) in
- let { aids; bids; dids; rids; sids = _ } = fixed_ids in
- let sids = V.SymbolicValueId.Set.empty in
+ let { aids; bids; dids; rids; sids } = fixed_ids in
+ let fixed_ids1 = compute_context_ids ctx1 in
+ let fixed_ids2 = compute_context_ids ctx2 in
+ let sids =
+ V.SymbolicValueId.Set.inter sids
+ (V.SymbolicValueId.Set.inter fixed_ids1.sids fixed_ids2.sids)
+ in
let fixed_ids = { aids; bids; dids; rids; sids } in
ctxs_are_equivalent fixed_ids ctx1 ctx2
in