summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Contexts.ml18
-rw-r--r--compiler/Interpreter.ml2
-rw-r--r--compiler/InterpreterBorrows.ml133
-rw-r--r--compiler/InterpreterBorrows.mli13
-rw-r--r--compiler/InterpreterLoops.ml894
-rw-r--r--compiler/InterpreterUtils.ml14
-rw-r--r--compiler/Invariants.ml9
-rw-r--r--compiler/Substitute.ml30
-rw-r--r--compiler/SymbolicToPure.ml15
-rw-r--r--compiler/ValuesUtils.ml22
-rw-r--r--tests/coq/misc/Loops.v380
-rw-r--r--tests/fstar/misc/Loops.Clauses.Template.fst51
-rw-r--r--tests/fstar/misc/Loops.Clauses.fst51
-rw-r--r--tests/fstar/misc/Loops.Funs.fst356
14 files changed, 1819 insertions, 169 deletions
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index f2fa36c5..0a6b27fd 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -551,3 +551,21 @@ class ['self] map_eval_ctx =
let env = super#visit_env acc ctx.env in
{ ctx with env }
end
+
+let env_iter_abs (f : V.abs -> unit) (env : env) : unit =
+ List.iter
+ (fun (ee : env_elem) ->
+ match ee with Var _ | Frame -> () | Abs abs -> f abs)
+ env
+
+let env_map_abs (f : V.abs -> V.abs) (env : env) : env =
+ List.map
+ (fun (ee : env_elem) ->
+ match ee with Var _ | Frame -> ee | Abs abs -> Abs (f abs))
+ env
+
+let env_filter_abs (f : V.abs -> bool) (env : env) : env =
+ List.filter
+ (fun (ee : env_elem) ->
+ match ee with Var _ | Frame -> true | Abs abs -> f abs)
+ env
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index dd0051f6..f47c6226 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -142,6 +142,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return
^ T.RegionGroupId.to_string back_id
^ "\n- loop_id: "
^ Print.option_to_string V.LoopId.to_string loop_id
+ ^ "\n- is_regular_return: "
+ ^ Print.bool_to_string is_regular_return
^ "\n- inside_loop: "
^ Print.bool_to_string inside_loop
^ "\n- ctx:\n"
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index a1cb4ec3..b2a46b1e 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1633,7 +1633,7 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
(* Accumulator to store the destructured values *)
let avalues = ref [] in
(* Utility function to store a value in the accumulator *)
- let push_avalue av = avalues := av :: !avalues in
+ let push_avalue av = avalues := List.append !avalues [ av ] in
(* We use this function to make sure we never register values (i.e.,
loans or borrows) when we shouldn't - see it as a sanity check:
for now, we don't allow nested borrows, which means we should register
@@ -1665,21 +1665,22 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
let ignored = mk_aignored child_av.V.ty in
let value = V.ALoan (V.ASharedLoan (bids, sv, ignored)) in
push { V.value; ty };
+ (* Explore the child *)
+ list_avalues false push_fail child_av;
(* Push the avalues introduced because we decomposed the inner loans -
note that we pay attention to the order in which we introduce
the avalues: we want to push them *after* the outer loan. If we
didn't want that, we would have implemented [list_values] in
exactly the same way as [list_avalues] (i.e., with a similar
signature) *)
- List.iter push avl;
- (* Explore the child *)
- list_avalues false push_fail child_av
+ List.iter push avl
| V.AMutLoan (bid, child_av) ->
+ (* Explore the child *)
+ list_avalues false push_fail child_av;
+ (* Explore the whole loan *)
let ignored = mk_aignored child_av.V.ty in
let value = V.ALoan (V.AMutLoan (bid, ignored)) in
- push { V.value; ty };
- (* Explore the child *)
- list_avalues false push_fail child_av
+ push { V.value; ty }
| V.AIgnoredMutLoan (opt_bid, child_av) ->
(* We don't support nested borrows for now *)
assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
@@ -1702,11 +1703,12 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
(* Explore the borrow content *)
match bc with
| V.AMutBorrow (bid, child_av) ->
+ (* Explore the child *)
+ list_avalues false push_fail child_av;
+ (* Explore the borrow *)
let ignored = mk_aignored child_av.V.ty in
let value = V.ABorrow (V.AMutBorrow (bid, ignored)) in
- push { V.value; ty };
- (* Explore the child *)
- list_avalues false push_fail child_av
+ push { V.value; ty }
| V.ASharedBorrow _ ->
(* Nothing specific to do: keep the value as it is *)
push av
@@ -1761,12 +1763,27 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
let rty = ety_no_regions_to_rty ty in
let av : V.typed_avalue =
assert (not (value_has_loans_or_borrows ctx sv.V.value));
+ (* We introduce fresh ids for the symbolic values *)
+ let mk_value_with_fresh_sids (v : V.typed_value) : V.typed_value
+ =
+ let visitor =
+ object
+ inherit [_] V.map_typed_avalue
+
+ method! visit_symbolic_value_id _ _ =
+ C.fresh_symbolic_value_id ()
+ end
+ in
+ visitor#visit_typed_value () v
+ in
+ let sv = mk_value_with_fresh_sids sv in
+ (* Create the new avalue *)
let value =
V.ALoan (V.ASharedLoan (bids, sv, mk_aignored rty))
in
{ V.value; ty = rty }
in
- let avl = List.append avl [ av ] in
+ let avl = List.append [ av ] avl in
(avl, sv)
else (avl, { v with V.value = V.Loan (V.SharedLoan (bids, sv)) })
| MutLoan _ -> raise (Failure "Unreachable"))
@@ -1779,7 +1796,7 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
(* Destructure the avalues *)
List.iter (list_avalues true push_avalue) abs0.V.avalues;
- let avalues = List.rev !avalues in
+ let avalues = !avalues in
(* Update *)
{ abs0 with V.avalues; kind = abs_kind; can_end }
@@ -1969,14 +1986,15 @@ type merge_abstraction_info = {
We compute the list of loan/borrow contents, maps from borrow/loan ids
to borrow/loan contents, etc.
- Note that this function is very specific to [merge_abstractions]: we
+ Note that this function is very specific to [merge_into_abstraction]: we
have strong assumptions about the shape of the abstraction, and in
particular that:
- its values don't contain nested borrows
- all the borrows are destructured (for instance, shared loans can't
contain shared loans).
*)
-let compute_merge_abstractions_info (abs : V.abs) : merge_abstraction_info =
+let compute_merge_abstraction_info (ctx : C.eval_ctx) (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
@@ -2086,9 +2104,9 @@ let compute_merge_abstractions_info (abs : V.abs) : merge_abstraction_info =
raise (Failure "Unreachable"));
super#visit_aborrow_content env bc
- method! visit_symbolic_value _ _ =
- (* Sanity check *)
- raise (Failure "Unreachable")
+ method! visit_symbolic_value _ sv =
+ (* Sanity check: no borrows *)
+ assert (not (symbolic_value_has_borrows ctx sv))
end
in
@@ -2165,12 +2183,12 @@ type merge_duplicates_funcs = {
Merge two abstractions into one, without updating the context.
*)
-let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
+let merge_into_abstraction_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
+ ("merge_into_abstraction_aux:\n- abs0:\n" ^ abs_to_string ctx abs0
^ "\n\n- abs1:\n" ^ abs_to_string ctx abs1));
(* Check that the abstractions are destructured *)
@@ -2187,7 +2205,7 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
loan_to_content = loan_to_content0;
borrow_to_content = borrow_to_content0;
} =
- compute_merge_abstractions_info abs0
+ compute_merge_abstraction_info ctx abs0
in
let {
@@ -2197,7 +2215,7 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
loan_to_content = loan_to_content1;
borrow_to_content = borrow_to_content1;
} =
- compute_merge_abstractions_info abs1
+ compute_merge_abstraction_info ctx abs1
in
(* Sanity check: there is no loan/borrows which appears in both abstractions,
@@ -2227,7 +2245,16 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
let merged_borrows = ref V.BorrowId.Set.empty in
let merged_loans = ref V.BorrowId.Set.empty in
let avalues = ref [] in
- let push_avalue av = avalues := av :: !avalues in
+ let push_avalue av =
+ log#ldebug
+ (lazy
+ ("merge_into_abstraction_aux: push_avalue: "
+ ^ typed_avalue_to_string ctx av));
+ avalues := av :: !avalues
+ in
+ let push_opt_avalue av =
+ match av with None -> () | Some av -> push_avalue av
+ in
let intersect =
V.BorrowId.Set.union
@@ -2251,6 +2278,7 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
let set_loan_as_merged id =
merged_loans := V.BorrowId.Set.add id !merged_loans
in
+ let set_loans_as_merged ids = V.BorrowId.Set.iter set_loan_as_merged ids in
(* Some utility functions *)
(* Merge two aborrow contents - note that those contents must have the same id *)
@@ -2284,13 +2312,13 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
in
let merge_aloan_contents (ty0 : T.rty) (lc0 : V.aloan_content) (ty1 : T.rty)
- (lc1 : V.aloan_content) : V.typed_avalue =
+ (lc1 : V.aloan_content) : V.typed_avalue option =
match (lc0, lc1) with
| V.AMutLoan (id, child0), V.AMutLoan (_, child1) ->
(* Register the loan id *)
set_loan_as_merged id;
(* Merge *)
- (Option.get merge_funs).merge_amut_loans id ty0 child0 ty1 child1
+ Some ((Option.get merge_funs).merge_amut_loans id ty0 child0 ty1 child1)
| ASharedLoan (ids0, sv0, child0), ASharedLoan (ids1, sv1, child1) ->
(* Filter the ids *)
let ids0 = filter_bids ids0 in
@@ -2298,14 +2326,30 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
(* Check that the sets of ids are the same - if it is not the case, it
means we actually need to merge more than 2 avalues: we ignore this
case for now *)
- assert (ids0 = ids1);
+ assert (V.BorrowId.Set.equal ids0 ids1);
let ids = ids0 in
- assert (not (V.BorrowId.Set.is_empty ids));
- (* Register the loan ids *)
- V.BorrowId.Set.iter set_loan_as_merged ids;
- (* Merge *)
- (Option.get merge_funs).merge_ashared_loans ids ty0 sv0 child0 ty1 sv1
- child1
+ if V.BorrowId.Set.is_empty ids then (
+ (* If the set of ids is empty, we can eliminate this shared loan.
+ For now, we check that we can eliminate the whole shared value
+ altogether.
+ A more complete approach would be to explore the value and introduce
+ as many shared loans/borrows/etc. as necessary for the sub-values.
+ For now, we check that there are no such values that we would need
+ to preserve (in practice it works because we destructure the
+ shared values in the abstractions, and forbid nested borrows).
+ *)
+ assert (not (value_has_loans_or_borrows ctx sv0.V.value));
+ assert (not (value_has_loans_or_borrows ctx sv0.V.value));
+ assert (is_aignored child0.V.value);
+ assert (is_aignored child1.V.value);
+ None)
+ else (
+ (* Register the loan ids *)
+ set_loans_as_merged ids;
+ (* Merge *)
+ Some
+ ((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 *)
@@ -2316,7 +2360,7 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
to register the merged loan ids: the caller doesn't do it (contrary to
the borrow case) *)
let merge_g_loan_contents (lc0 : g_loan_content_with_ty)
- (lc1 : g_loan_content_with_ty) : V.typed_avalue =
+ (lc1 : g_loan_content_with_ty) : V.typed_avalue option =
match (lc0, lc1) with
| Concrete _, Concrete _ ->
(* This can not happen: the values should have been destructured *)
@@ -2339,7 +2383,7 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
| BorrowId bid ->
log#ldebug
(lazy
- ("merge_abstractions_aux: merging borrow "
+ ("merge_into_abstraction_aux: merging borrow "
^ V.BorrowId.to_string bid));
(* Check if the borrow has already been merged - this can happen
@@ -2386,7 +2430,7 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
else (
log#ldebug
(lazy
- ("merge_abstractions_aux: merging loan "
+ ("merge_into_abstraction_aux: merging loan "
^ V.BorrowId.to_string bid));
(* Check if we need to filter it *)
@@ -2397,7 +2441,7 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
let lc0 = V.BorrowId.Map.find_opt bid loan_to_content0 in
let lc1 = V.BorrowId.Map.find_opt bid loan_to_content1 in
(* Merge *)
- let av : V.typed_avalue =
+ let av : V.typed_avalue option =
match (lc0, lc1) with
| None, Some lc | Some lc, None -> (
match lc with
@@ -2414,8 +2458,11 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
assert (
not (value_has_loans_or_borrows ctx sv.V.value));
let lc = V.ASharedLoan (bids, sv, child) in
- { V.value = V.ALoan lc; ty }
- | V.AMutLoan _ -> { V.value = V.ALoan lc; ty }
+ set_loans_as_merged bids;
+ Some { V.value = V.ALoan lc; ty }
+ | V.AMutLoan _ ->
+ set_loan_as_merged bid;
+ Some { V.value = V.ALoan lc; ty }
| V.AEndedMutLoan _ | V.AEndedSharedLoan _
| V.AIgnoredMutLoan _ | V.AEndedIgnoredMutLoan _
| V.AIgnoredSharedLoan _ ->
@@ -2426,7 +2473,7 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
merge_g_loan_contents lc0 lc1
| None, None -> raise (Failure "Unreachable")
in
- push_avalue av))
+ push_opt_avalue av))
borrows_loans;
(* Reverse the avalues (we visited the loans/borrows in order, but pushed
@@ -2488,7 +2535,7 @@ let ctx_merge_regions (ctx : C.eval_ctx) (rid : T.RegionId.id)
let env = Substitute.env_subst_rids rsubst ctx.env in
{ ctx with C.env }
-let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
+let merge_into_abstraction (abs_kind : V.abs_kind) (can_end : bool)
(merge_funs : merge_duplicates_funcs option) (ctx : C.eval_ctx)
(abs_id0 : V.AbstractionId.id) (abs_id1 : V.AbstractionId.id) :
C.eval_ctx * V.AbstractionId.id =
@@ -2497,10 +2544,12 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
let abs1 = C.ctx_lookup_abs ctx abs_id1 in
(* Merge them *)
- let nabs = merge_abstractions_aux abs_kind can_end merge_funs ctx abs0 abs1 in
+ let nabs =
+ merge_into_abstraction_aux abs_kind can_end merge_funs ctx abs0 abs1
+ in
- (* Update the environment: replace the first abstraction with the result of the merge,
- remove the second abstraction *)
+ (* Update the environment: replace the abstraction 1 with the result of the merge,
+ remove the abstraction 0 *)
let ctx = fst (C.ctx_subst_abs ctx abs_id1 nabs) in
let ctx = fst (C.ctx_remove_abs ctx abs_id0) in
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 9e407399..31b67bd7 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -132,7 +132,7 @@ val abs_is_destructured : bool -> C.eval_ctx -> V.abs -> bool
val convert_value_to_abstractions :
V.abs_kind -> bool -> bool -> C.eval_ctx -> V.typed_value -> V.abs list
-(** See {!merge_abstractions}.
+(** See {!merge_into_abstraction}.
Rem.: it may be more idiomatic to have a functor, but this seems a bit
heavyweight, though.
@@ -199,9 +199,10 @@ type merge_duplicates_funcs = {
(** Merge an abstraction into another abstraction.
- We insert the result of the merge in place of the first abstraction (this
- helps preserving the structure of the environment, when computing loop
- fixed points for instance).
+ We insert the result of the merge in place of the second abstraction (and in
+ particular, we don't simply push the merged abstraction at the end of the
+ environment: this helps preserving the structure of the environment, when
+ computing loop fixed points for instance).
When we merge two abstractions together, we remove the loans/borrows
which appear in one and whose associated loans/borrows appear in the
@@ -236,7 +237,7 @@ type merge_duplicates_funcs = {
abs'0 { mut_borrow l0, mut_loan l1 } // mut_borrow l0 !
abs'1 { mut_borrow l0, mut_loan l2 } // mut_borrow l0 !
]}
- If you want to forbid this, provide [None]. In that case, [merge_abstractions]
+ If you want to forbid this, provide [None]. In that case, [merge_into_abstraction]
actually simply performs some sort of a union.
- [ctx]
@@ -246,7 +247,7 @@ type merge_duplicates_funcs = {
We return the updated context as well as the id of the new abstraction which
results from the merge.
*)
-val merge_abstractions :
+val merge_into_abstraction :
V.abs_kind ->
bool ->
merge_duplicates_funcs option ->
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 43863722..1c1ae0bc 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -215,21 +215,17 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool)
end
in
- List.iter
- (fun (ee : C.env_elem) ->
- match ee with
- | Var _ | Frame -> ()
- | Abs abs ->
- let abs_id = abs.abs_id in
- if explore abs then (
- abs_to_borrows :=
- V.AbstractionId.Map.add abs_id V.BorrowId.Set.empty
- !abs_to_borrows;
- abs_to_loans :=
- V.AbstractionId.Map.add abs_id V.BorrowId.Set.empty !abs_to_loans;
- abs_ids := abs.abs_id :: !abs_ids;
- List.iter (explore_abs#visit_typed_avalue abs.abs_id) abs.avalues)
- else ())
+ C.env_iter_abs
+ (fun abs ->
+ let abs_id = abs.abs_id in
+ if explore abs then (
+ abs_to_borrows :=
+ V.AbstractionId.Map.add abs_id V.BorrowId.Set.empty !abs_to_borrows;
+ abs_to_loans :=
+ V.AbstractionId.Map.add abs_id V.BorrowId.Set.empty !abs_to_loans;
+ abs_ids := abs.abs_id :: !abs_ids;
+ List.iter (explore_abs#visit_typed_avalue abs.abs_id) abs.avalues)
+ else ())
env;
(* Rem.: there is no need to reverse the abs ids, because we explored the environment
@@ -244,6 +240,96 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool)
borrow_loan_to_abs = !borrow_loan_to_abs;
}
+(** Refresh the ids of the fresh abstractions.
+
+ We do this because {!prepare_ashared_loans} introduces some non-fixed
+ abstractions in contexts which are later joined: we have to make sure
+ two contexts we join don't have non-fixed abstractions with the same ids.
+ *)
+let refresh_abs (old_abs : V.AbstractionId.Set.t) (ctx : C.eval_ctx) :
+ C.eval_ctx =
+ let ids, _ = compute_context_ids ctx in
+ let abs_to_refresh = V.AbstractionId.Set.diff ids.aids old_abs in
+ let aids_subst =
+ List.map
+ (fun id -> (id, C.fresh_abstraction_id ()))
+ (V.AbstractionId.Set.elements abs_to_refresh)
+ in
+ let aids_subst = V.AbstractionId.Map.of_list aids_subst in
+ let subst id =
+ match V.AbstractionId.Map.find_opt id aids_subst with
+ | None -> id
+ | Some id -> id
+ in
+ let env =
+ Subst.env_subst_ids
+ (fun x -> x)
+ (fun x -> x)
+ (fun x -> x)
+ (fun x -> x)
+ (fun x -> x)
+ subst ctx.env
+ in
+ { ctx with C.env }
+
+(** Reorder the loans and borrows in the fresh abstractions.
+
+ We do this in order to enforce some structure in the environments: this
+ allows us to find fixed-points. Note that this function needs to be
+ called typically after we merge abstractions together (see {!collapse_ctx}
+ for instance).
+ *)
+let reorder_loans_borrows_in_fresh_abs (old_abs_ids : V.AbstractionId.Set.t)
+ (ctx : C.eval_ctx) : C.eval_ctx =
+ let reorder_in_fresh_abs (abs : V.abs) : V.abs =
+ (* Split between the loans and borrows *)
+ let is_borrow (av : V.typed_avalue) : bool =
+ match av.V.value with
+ | ABorrow _ -> true
+ | ALoan _ -> false
+ | _ -> raise (Failure "Unexpected")
+ in
+ let aborrows, aloans = List.partition is_borrow abs.V.avalues in
+
+ (* Reoder the borrows, and the loans.
+
+ After experimenting, it seems that a good way of reordering the loans
+ and the borrows to find fixed points is simply to sort them by increasing
+ order of id (taking the smallest id of a set of ids, in case of sets).
+ *)
+ let get_borrow_id (av : V.typed_avalue) : V.BorrowId.id =
+ match av.V.value with
+ | V.ABorrow (V.AMutBorrow (bid, _) | V.ASharedBorrow bid) -> bid
+ | _ -> raise (Failure "Unexpected")
+ in
+ let get_loan_id (av : V.typed_avalue) : V.BorrowId.id =
+ match av.V.value with
+ | V.ALoan (V.AMutLoan (lid, _)) -> lid
+ | V.ALoan (V.ASharedLoan (lids, _, _)) -> V.BorrowId.Set.min_elt lids
+ | _ -> raise (Failure "Unexpected")
+ in
+ (* We use ordered maps to reorder the borrows and loans *)
+ let reorder (get_bid : V.typed_avalue -> V.BorrowId.id)
+ (values : V.typed_avalue list) : V.typed_avalue list =
+ List.map snd
+ (V.BorrowId.Map.bindings
+ (V.BorrowId.Map.of_list (List.map (fun v -> (get_bid v, v)) values)))
+ in
+ let aborrows = reorder get_borrow_id aborrows in
+ let aloans = reorder get_loan_id aloans in
+ let avalues = List.append aborrows aloans in
+ { abs with V.avalues }
+ in
+
+ let reorder_in_abs (abs : V.abs) =
+ if V.AbstractionId.Set.mem abs.abs_id old_abs_ids then abs
+ else reorder_in_fresh_abs abs
+ in
+
+ let env = C.env_map_abs reorder_in_abs ctx.env in
+
+ { ctx with C.env }
+
(** 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 =
@@ -254,22 +340,122 @@ let destructure_new_abs (loop_id : V.LoopId.id)
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)
+ C.env_map_abs
+ (fun abs ->
+ if is_fresh_abs_id abs.abs_id then
+ let abs =
+ destructure_abs abs_kind can_end destructure_shared_values ctx abs
+ in
+ abs
+ else abs)
ctx.env
in
{ ctx with env }
+(** Decompose the shared avalues, so as not to have nested shared loans
+ inside of abstractions.
+
+ For instance:
+ {[
+ abs'0 { shared_aloan ls0 (true, shared_loan ls1 s0) _ }
+
+ ~~>
+
+ abs'0 {
+ shared_aloan ls0 (true, s0) _
+ shared_aloan ls1 s1 _
+ }
+ ]}
+
+ Note that we decompose only in the "fresh" abstractions (this is controled
+ by the [old_aids] parameter).
+
+ TODO: how to factorize with {!destructure_abs}?
+ *)
+let decompose_shared_avalues (loop_id : V.LoopId.id)
+ (old_aids : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx =
+ (* Decompose the shared avalues in a fresh abstraction. We only decompose
+ in fresh (i.e., non-fixed) abstractions: {!decompose_in_abs} below
+ ignores the fixed abstractions and delegates to this function *)
+ let decompose_in_fresh_abs (abs : V.abs) : V.abs =
+ let new_loans = ref [] in
+ (* When decomposing, we need to duplicate the symbolic values (we
+ simply introduce fresh ids) *)
+ let mk_value_with_fresh_sids (v : V.typed_value) : V.typed_value =
+ let visitor =
+ object
+ inherit [_] V.map_typed_avalue
+ method! visit_symbolic_value_id _ _ = C.fresh_symbolic_value_id ()
+ end
+ in
+ visitor#visit_typed_value () v
+ in
+ (* Visit the values: whenever we enter a shared loan (which is necessarily
+ a strict subvalue of a shared aloan, because we only explore abstractions)
+ we move it outside (we remove the shared loan, register a shared value
+ to insert in the abstraction, and use fresh symbolic values in this new
+ shared value).
+ *)
+ let loan_visitor =
+ object (self : 'self)
+ inherit [_] V.map_typed_avalue as super
+
+ method! visit_typed_value env v =
+ match v.V.value with
+ | V.Loan (V.SharedLoan (lids, sv)) ->
+ let sv = self#visit_typed_value env sv in
+
+ (* Introduce fresh symbolic values for the new loan *)
+ let nsv = mk_value_with_fresh_sids sv in
+ new_loans := List.append !new_loans [ (lids, nsv) ];
+
+ (* Return *)
+ sv
+ | _ -> super#visit_typed_value env v
+ end
+ in
+ let rid = T.RegionId.Set.min_elt abs.regions in
+
+ (* We registered new loans to add in the abstraction: actually create those
+ loans, and insert them in the abstraction *)
+ let mk_ashared_loan (lids : V.BorrowId.Set.t) (sv : V.typed_value) :
+ V.typed_avalue =
+ (* There shouldn't be nested borrows *)
+ let sv_ty = ety_no_regions_to_rty sv.V.ty in
+ let ty = T.Ref (T.Var rid, sv_ty, T.Shared) in
+ let child_av = mk_aignored sv_ty in
+ let value = V.ALoan (V.ASharedLoan (lids, sv, child_av)) in
+ { V.value; ty }
+ in
+ let avalues =
+ List.map
+ (fun av ->
+ new_loans := [];
+ let av = loan_visitor#visit_typed_avalue () av in
+ let new_loans =
+ List.map (fun (lids, sv) -> mk_ashared_loan lids sv) !new_loans
+ in
+ av :: List.rev new_loans)
+ abs.V.avalues
+ in
+ let avalues = List.concat avalues in
+ let abs_id = C.fresh_abstraction_id () in
+ let kind = V.Loop (loop_id, None, V.LoopSynthInput) in
+ let can_end = true in
+ let abs = { abs with V.abs_id; kind; can_end; avalues } in
+ abs
+ in
+
+ (* Decompose only in the fresh abstractions *)
+ let decompose_in_abs abs =
+ if V.AbstractionId.Set.mem abs.V.abs_id old_aids then abs
+ else decompose_in_fresh_abs abs
+ in
+
+ (* Apply in the environment *)
+ let env = C.env_map_abs decompose_in_abs ctx.env in
+ { ctx with C.env }
+
(** Collapse an environment.
We do this to simplify an environment, for the purpose of finding a loop
@@ -277,7 +463,7 @@ let destructure_new_abs (loop_id : V.LoopId.id)
We do the following:
- we look for all the *new* dummy values (we use sets of old ids to decide
- wether a value is new or not)
+ wether a value is new or not) and convert them into abstractions
- 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.
@@ -303,9 +489,9 @@ let destructure_new_abs (loop_id : V.LoopId.id)
]}
In this new environment, the dummy variables [_@1], [_@2] and [_@3] are
- considered as new. We collapse them.
+ considered as new.
- We first convert the dummy values to abstractions. It gives:
+ We first convert the new dummy values to abstractions. It gives:
{[
abs@0 { ML l0 }
ls -> MB l4 (s@6 : loops::List<T>)
@@ -315,7 +501,7 @@ let destructure_new_abs (loop_id : V.LoopId.id)
abs@3 { MB l1 }
]}
- We then merge those abstractions together. It gives:
+ We finally merge the new abstractions together. It gives:
{[
abs@0 { ML l0 }
ls -> MB l4 (s@6 : loops::List<T>)
@@ -367,12 +553,18 @@ let collapse_ctx (loop_id : V.LoopId.id)
else [ ee ])
ctx0.env)
in
+ let ctx = { ctx0 with C.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"));
+ ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n"
+ ));
+
+ log#ldebug
+ (lazy
+ ("collapse_ctx: after decomposing the shared values in the abstractions:\n"
+ ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n"
+ ));
(* Explore all the *new* abstractions, and compute various maps *)
let explore (abs : V.abs) = is_fresh_abs_id abs.abs_id in
@@ -402,7 +594,7 @@ let collapse_ctx (loop_id : V.LoopId.id)
V.AbstractionId.Map.of_list (List.map (fun id -> (id, UF.make id)) abs_ids)
in
- let ctx = ref { ctx0 with C.env } in
+ let ctx = ref ctx in
(* Merge all the mergeable abs.
@@ -436,19 +628,21 @@ let collapse_ctx (loop_id : V.LoopId.id)
(* If the two ids are the same, it means the abstractions were already merged *)
if abs_id0 = abs_id1 then ()
else (
+ (* We actually need to merge the abstractions *)
+
+ (* Debug *)
log#ldebug
(lazy
- ("collapse_ctx: merging abstractions: "
+ ("collapse_ctx: merging abstraction "
+ ^ V.AbstractionId.to_string abs_id1
+ ^ " into "
^ V.AbstractionId.to_string abs_id0
- ^ " and "
- ^ V.AbstractionId.to_string abs_id1));
-
- (* We actually need to merge the abstractions *)
+ ^ ":\n\n" ^ eval_ctx_to_string !ctx));
(* Update the environment - pay attention to the order: we
we merge [abs_id1] *into* [abs_id0] *)
let nctx, abs_id =
- merge_abstractions abs_kind can_end merge_funs !ctx
+ merge_into_abstraction abs_kind can_end merge_funs !ctx
abs_id1 abs_id0
in
ctx := nctx;
@@ -460,8 +654,22 @@ let collapse_ctx (loop_id : V.LoopId.id)
bids)
abs_ids;
+ log#ldebug
+ (lazy
+ ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
+ ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string !ctx ^ "\n\n"));
+
+ (* Reorder the loans and borrows in the fresh abstractions *)
+ let ctx = reorder_loans_borrows_in_fresh_abs old_ids.aids !ctx in
+
+ log#ldebug
+ (lazy
+ ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
+ ^ "\n\n- after collapse and reorder borrows/loans:\n"
+ ^ eval_ctx_to_string ctx ^ "\n\n"));
+
(* Return the new context *)
- !ctx
+ ctx
(** Match two types during a join. *)
let rec match_types (match_distinct_types : 'r T.ty -> 'r T.ty -> 'r T.ty)
@@ -513,8 +721,22 @@ module type Matcher = sig
(** The input ADTs don't have the same variant *)
val match_distinct_adts : T.ety -> V.adt_value -> V.adt_value -> V.typed_value
- (** The meta-value is the result of a match *)
- val match_shared_borrows : T.ety -> V.borrow_id -> V.borrow_id -> V.borrow_id
+ (** 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.
+ We do this for shared borrows (and not, e.g., mutable borrows) because
+ shared borrows introduce indirections, while mutable borrows carry the
+ borrowed values with them: we might want to explore and match those
+ borrowed values, in which case we have to manually look them up before
+ calling the match function.
+ *)
+ val match_shared_borrows :
+ (V.typed_value -> V.typed_value -> V.typed_value) ->
+ T.ety ->
+ V.borrow_id ->
+ V.borrow_id ->
+ V.borrow_id
(** The input parameters are:
- [ty]
@@ -707,7 +929,7 @@ module Match (M : Matcher) = struct
let bc =
match (bc0, bc1) with
| SharedBorrow bid0, SharedBorrow bid1 ->
- let bid = M.match_shared_borrows ty bid0 bid1 in
+ let bid = M.match_shared_borrows match_rec ty bid0 bid1 in
V.SharedBorrow bid
| MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) ->
let bv = match_rec bv0 bv1 in
@@ -948,7 +1170,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
(* No borrows, no loans: we can introduce a symbolic value *)
mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty
- let match_shared_borrows (ty : T.ety) (bid0 : V.borrow_id)
+ let match_shared_borrows _ (ty : T.ety) (bid0 : V.borrow_id)
(bid1 : V.borrow_id) : V.borrow_id =
if bid0 = bid1 then bid0
else
@@ -1199,7 +1421,7 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : V.LoopId.id)
(* We need to pick a type for the avalue. The types on the left and on the
right may use different regions: it doesn't really matter (here, we pick
the one from the left), because we will merge those regions together
- anyway (see the comments for {!merge_abstractions}).
+ anyway (see the comments for {!merge_into_abstraction}).
*)
let ty = ty0 in
let child = child0 in
@@ -1209,8 +1431,12 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : V.LoopId.id)
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));
+ let _ =
+ let _, ty0, _ = ty_as_ref ty0 in
+ let _, ty1, _ = ty_as_ref ty1 in
+ assert (not (ty_has_borrows ctx.type_context.type_infos ty0));
+ assert (not (ty_has_borrows ctx.type_context.type_infos ty1))
+ in
(* Same remarks as for [merge_amut_borrows] *)
let ty = ty0 in
@@ -1253,11 +1479,11 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : V.LoopId.id)
merge_ashared_loans;
}
-let merge_abstractions (loop_id : V.LoopId.id) (abs_kind : V.abs_kind)
+let merge_into_abstraction (loop_id : V.LoopId.id) (abs_kind : V.abs_kind)
(can_end : bool) (ctx : C.eval_ctx) (aid0 : V.AbstractionId.id)
(aid1 : V.AbstractionId.id) : C.eval_ctx * V.AbstractionId.id =
let merge_funs = mk_collapse_ctx_merge_duplicate_funs loop_id ctx in
- merge_abstractions abs_kind can_end (Some merge_funs) ctx aid0 aid1
+ merge_into_abstraction abs_kind can_end (Some merge_funs) ctx aid0 aid1
(** Collapse an environment, merging the duplicated borrows/loans.
@@ -1288,9 +1514,9 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets)
Note that when joining the values mapped to by the non-dummy variables, we
may introduce duplicated borrows. Also, we don't match the abstractions
- which are not in the prefix, which can also lead to borrow duplications. For
- this reason, the environment needs to be collapsed afterwards to get rid of
- those duplicated loans/borrows.
+ which are not in the prefix, and this can also lead to borrow
+ duplications. For this reason, the environment needs to be collapsed
+ afterwards to get rid of those duplicated loans/borrows.
For instance, if we have:
{[
@@ -1538,6 +1764,8 @@ module type MatchCheckEquivState = sig
val sid_map : V.SymbolicValueId.InjSubst.t ref
val sid_to_value_map : V.typed_value V.SymbolicValueId.Map.t ref
val aid_map : V.AbstractionId.InjSubst.t ref
+ val lookup_shared_value_in_ctx0 : V.BorrowId.id -> V.typed_value
+ val lookup_shared_value_in_ctx1 : V.BorrowId.id -> V.typed_value
end
(** An auxiliary matcher that we use for two purposes:
@@ -1648,9 +1876,21 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
(_adt1 : V.adt_value) : V.typed_value =
raise Distinct
- let match_shared_borrows (_ty : T.ety) (bid0 : V.borrow_id)
- (bid1 : V.borrow_id) : V.borrow_id =
+ let match_shared_borrows
+ (match_typed_values : V.typed_value -> V.typed_value -> V.typed_value)
+ (_ty : T.ety) (bid0 : V.borrow_id) (bid1 : V.borrow_id) : V.borrow_id =
let bid = match_borrow_id bid0 bid1 in
+ (* If we don't check for equivalence (i.e., we apply a fixed-point),
+ we lookup the shared values and match them.
+ *)
+ let _ =
+ if S.check_equiv then ()
+ else
+ let v0 = S.lookup_shared_value_in_ctx0 bid0 in
+ let v1 = S.lookup_shared_value_in_ctx1 bid1 in
+ let _ = match_typed_values v0 v1 in
+ ()
+ in
bid
let match_mut_borrows (_ty : T.ety) (bid0 : V.borrow_id)
@@ -1790,10 +2030,17 @@ type ids_maps = {
If [false], compute a mapping from the first context to the second context,
in the sense of [match_ctx_with_target].
+ The lookup functions are used to match the shared values when [check_equiv]
+ is [false] (we sometimes use [match_ctxs] on partial environments, meaning
+ we have to lookup the shared values in the complete environment, otherwise
+ we miss some mappings).
+
We return an optional ids map: [Some] if the match succeeded, [None] otherwise.
*)
-let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
- (ctx1 : C.eval_ctx) : ids_maps option =
+let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets)
+ (lookup_shared_value_in_ctx0 : V.BorrowId.id -> V.typed_value)
+ (lookup_shared_value_in_ctx1 : V.BorrowId.id -> V.typed_value)
+ (ctx0 : C.eval_ctx) (ctx1 : C.eval_ctx) : ids_maps option =
log#ldebug
(lazy
("match_ctxs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids
@@ -1851,6 +2098,8 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
let sid_map = sid_map
let sid_to_value_map = sid_to_value_map
let aid_map = aid_map
+ let lookup_shared_value_in_ctx0 = lookup_shared_value_in_ctx0
+ let lookup_shared_value_in_ctx1 = lookup_shared_value_in_ctx1
end in
let module CEM = MakeCheckEquivMatcher (S) in
let module M = Match (CEM) in
@@ -1878,10 +2127,6 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
(* Rem.: this function raises exceptions of type [Distinct] *)
let match_abstractions (abs0 : V.abs) (abs1 : V.abs) : unit =
- log#ldebug
- (lazy
- ("match_ctxs: match_abstractions: " ^ "\n\n- abs0: " ^ V.show_abs abs0
- ^ "\n\n- abs1: " ^ V.show_abs abs1));
let {
V.abs_id = abs_id0;
kind = kind0;
@@ -2058,7 +2303,10 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
(ctx1 : C.eval_ctx) : bool =
let check_equivalent = true in
- Option.is_some (match_ctxs check_equivalent fixed_ids ctx0 ctx1)
+ let lookup_shared_value _ = raise (Failure "Unreachable") in
+ Option.is_some
+ (match_ctxs check_equivalent fixed_ids lookup_shared_value
+ lookup_shared_value ctx0 ctx1)
(** 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
@@ -2102,6 +2350,17 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
("loop_join_origin_with_continue_ctxs:join_one: initial ctx:\n"
^ eval_ctx_to_string ctx));
+ (* (* Push the abstractions introduced by {!prepare_shared_loans} as
+ far as we can to preserve the structure of the context. *)
+ let ctx =
+ push_fresh_shared_loans_abs fresh_shared_loans_abs_ids original_ctx_length
+ ctx
+ in
+ log#ldebug
+ (lazy
+ ("loop_join_origin_with_continue_ctxs:join_one: after push fresh \
+ shared loan abs:\n" ^ eval_ctx_to_string ctx)); *)
+
(* Destructure the abstractions introduced in the new context *)
let ctx = destructure_new_abs loop_id fixed_ids.aids ctx in
log#ldebug
@@ -2116,6 +2375,9 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n"
^ eval_ctx_to_string ctx));
+ (* Refresh the fresh abstractions *)
+ let ctx = refresh_abs fixed_ids.aids ctx in
+
(* Join the two contexts *)
let ctx1 = join_one_aux ctx in
log#ldebug
@@ -2143,6 +2405,245 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
(* # Return *)
((old_ctx, ctxl), !joined_ctx)
+(** Prepare the shared loans in the abstractions by moving them to fresh
+ abstractions.
+
+ We use this to prepare an evaluation context before computing a fixed point.
+
+ Because a loop iteration might lead to symbolic value expansions and create
+ shared loans in shared values inside the *fixed* abstractions, which we want
+ to leave unchanged, we introduce some reborrows in the following way:
+
+ {[
+ abs'0 { SL {l0, l1} s0 }
+ l0 -> SB l0
+ l1 -> SB l1
+
+ ~~>
+
+ abs'0 { SL {l0, l1} s0 }
+ l0 -> SB l2
+ l1 -> SB l3
+ abs'2 { SB l0, SL {l2} s2 }
+ abs'3 { SB l1, SL {l3} s3 }
+ ]}
+
+ This is sound but leads to information loss. This way, the fixed abstraction
+ [abs'0] is never modified because [s0] is never accessed (and thus never
+ expanded).
+
+ We do this because it makes it easier to compute joins and fixed points.
+
+ We return the new context and the set of fresh abs ids.
+ *)
+let prepare_ashared_loans (loop_id : V.LoopId.id) (ctx : C.eval_ctx) :
+ C.eval_ctx * V.AbstractionId.Set.t =
+ (* Return the same value but where:
+ - the shared loans have been removed
+ - the symbolic values have been replaced with fresh symbolic values
+ - the region ids found in the value and belonging to the set [rids] have
+ been substituted with [nrid]
+ *)
+ let mk_value_with_fresh_sids_no_shared_loans (rids : T.RegionId.Set.t)
+ (nrid : T.RegionId.id) (v : V.typed_value) : V.typed_value =
+ (* Remove the shared loans *)
+ let v = value_remove_shared_loans v in
+ (* Substitute the symbolic values and the region *)
+ Subst.typed_value_subst_ids
+ (fun r -> if T.RegionId.Set.mem r rids then nrid else r)
+ (fun x -> x)
+ (fun x -> x)
+ (fun _ -> C.fresh_symbolic_value_id ())
+ (fun x -> x)
+ v
+ in
+
+ let borrow_substs = ref [] in
+ let fresh_absl = ref [] in
+
+ (* Auxiliary function to create a new abstraction for a shared value found in
+ an abstraction.
+
+ Example:
+ ========
+ When exploring:
+ {[
+ abs'0 { SL {l0, l1} s0 }
+ ]}
+
+ we find the shared value:
+
+ {[
+ SL {l0, l1} s0
+ ]}
+
+ and introduce the corresponding abstraction:
+ {[
+ abs'2 { SB l0, SL {l2} s2 }
+ ]}
+ *)
+ let push_abs_for_shared_value (abs : V.abs) (sv : V.typed_value)
+ (lid : V.BorrowId.id) : unit =
+ (* Create a fresh borrow (for the reborrow) *)
+ let nlid = C.fresh_borrow_id () in
+
+ (* We need a fresh region for the new abstraction *)
+ let nrid = C.fresh_region_id () in
+
+ (* Prepare the shared value *)
+ let nsv = mk_value_with_fresh_sids_no_shared_loans abs.regions nrid sv in
+
+ (* Save the borrow substitution, to apply it to the context later *)
+ borrow_substs := (lid, nlid) :: !borrow_substs;
+
+ (* Rem.: the below sanity checks are not really necessary *)
+ assert (V.AbstractionId.Set.is_empty abs.parents);
+ assert (abs.original_parents = []);
+ assert (T.RegionId.Set.is_empty abs.ancestors_regions);
+
+ (* Introduce the new abstraction for the shared values *)
+ let rty = ety_no_regions_to_rty sv.V.ty in
+
+ (* Create the shared loan child *)
+ let child_rty = rty in
+ let child_av = mk_aignored child_rty in
+
+ (* Create the shared loan *)
+ let loan_rty = T.Ref (T.Var nrid, rty, T.Shared) in
+ let loan_value =
+ V.ALoan (V.ASharedLoan (V.BorrowId.Set.singleton nlid, nsv, child_av))
+ in
+ let loan_value = mk_typed_avalue loan_rty loan_value in
+
+ (* Create the shared borrow *)
+ let borrow_rty = loan_rty in
+ let borrow_value = V.ABorrow (V.ASharedBorrow lid) in
+ let borrow_value = mk_typed_avalue borrow_rty borrow_value in
+
+ (* Create the abstraction *)
+ let avalues = [ borrow_value; loan_value ] in
+ let kind = V.Loop (loop_id, None, V.LoopSynthInput) in
+ let can_end = true in
+ let fresh_abs =
+ {
+ V.abs_id = C.fresh_abstraction_id ();
+ kind;
+ can_end;
+ parents = V.AbstractionId.Set.empty;
+ original_parents = [];
+ regions = T.RegionId.Set.singleton nrid;
+ ancestors_regions = T.RegionId.Set.empty;
+ avalues;
+ }
+ in
+ fresh_absl := fresh_abs :: !fresh_absl
+ in
+
+ (* Explore the shared values in the context abstractions, and introduce
+ fresh abstractions with reborrows for those shared values.
+
+ We simply explore the context and call {!push_abs_for_shared_value}
+ when necessary.
+ *)
+ let collect_shared_values_in_abs (abs : V.abs) : unit =
+ let visit_avalue =
+ object
+ inherit [_] V.iter_typed_avalue as super
+
+ method! visit_SharedLoan env lids sv =
+ (* Sanity check: we don't support nested borrows for now *)
+ assert (not (value_has_borrows ctx sv.V.value));
+
+ (* Generate fresh borrows and values *)
+ V.BorrowId.Set.iter (push_abs_for_shared_value abs sv) lids;
+
+ (* Continue the exploration *)
+ super#visit_SharedLoan env lids sv
+
+ method! visit_ASharedLoan env lids sv _ =
+ (* Sanity check: we don't support nested borrows for now *)
+ assert (not (value_has_borrows ctx sv.V.value));
+
+ (* Generate fresh borrows and values *)
+ V.BorrowId.Set.iter (push_abs_for_shared_value abs sv) lids;
+
+ (* Continue the exploration *)
+ super#visit_SharedLoan env lids sv
+
+ (** Check that there are no symbolic values with *borrows* inside the
+ abstraction - shouldn't happen if the symbolic values are greedily
+ expanded.
+ We do this because those values could contain shared borrows:
+ if it is the case, we need to duplicate them too.
+ TODO: implement this more general behavior.
+ *)
+ method! visit_symbolic_value env sv =
+ assert (not (symbolic_value_has_borrows ctx sv));
+ super#visit_symbolic_value env sv
+ end
+ in
+ List.iter (visit_avalue#visit_typed_avalue None) abs.avalues
+ in
+ C.env_iter_abs collect_shared_values_in_abs ctx.env;
+
+ (* Update the borrow ids in the environment.
+
+ Example:
+ ========
+ If we start with environment:
+ {[
+ abs'0 { SL {l0, l1} s0 }
+ l0 -> SB l0
+ l1 -> SB l1
+ ]}
+
+ We introduce the following abstractions:
+ {[
+ abs'2 { SB l0, SL {l2} s2 }
+ abs'3 { SB l1, SL {l3} s3 }
+ ]}
+
+ While doing so, we registered the fact that we introduced [l2] for [l0]
+ and [l3] for [l1]: we now need to perform the proper substitutions in
+ the values [l0] and [l1]. This gives:
+
+ {[
+ l0 -> SB l0
+ l1 -> SB l1
+
+ ~~>
+
+ l0 -> SB l2
+ l1 -> SB l3
+ ]}
+ *)
+ let env =
+ let bmap = V.BorrowId.Map.of_list !borrow_substs in
+ let bsusbt bid =
+ match V.BorrowId.Map.find_opt bid bmap with
+ | None -> bid
+ | Some bid -> bid
+ in
+
+ let visitor =
+ object
+ inherit [_] C.map_env
+ method! visit_borrow_id _ bid = bsusbt bid
+ end
+ in
+ visitor#visit_env () ctx.env
+ in
+
+ (* Add the abstractions *)
+ let fresh_abs_ids =
+ V.AbstractionId.Set.of_list (List.map (fun abs -> abs.V.abs_id) !fresh_absl)
+ in
+ let fresh_absl = List.map (fun abs -> C.Abs abs) !fresh_absl in
+ let env = List.append fresh_absl env in
+
+ (* Return *)
+ ({ ctx with C.env }, fresh_abs_ids)
+
(** Compute a fixed-point for the context at the entry of the loop.
We also return the sets of fixed ids, and the list of symbolic values
that appear in the fixed point context.
@@ -2161,6 +2662,26 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
let ctx_upon_entry = ref None in
let ctxs = ref [] in
let register_ctx ctx = ctxs := ctx :: !ctxs in
+
+ (* Introduce "reborrows" for the shared values in the abstractions, so that
+ the shared values in the fixed abstractions never get modified (technically,
+ they are immutable, but in practice we can introduce more shared loans, or
+ expand symbolic values).
+
+ For more details, see the comments for {!prepare_ashared_loans}
+ *)
+ let ctx, _ = prepare_ashared_loans loop_id ctx0 in
+
+ (* Debug *)
+ log#ldebug
+ (lazy
+ ("compute_loop_entry_fixed_point: after prepare_ashared_loans:"
+ ^ "\n\n- ctx0:\n"
+ ^ eval_ctx_to_string_no_filter ctx0
+ ^ "\n\n- ctx1:\n"
+ ^ eval_ctx_to_string_no_filter ctx
+ ^ "\n\n"));
+
let cf_exit_loop_body (res : statement_eval_res) : m_fun =
fun ctx ->
match res with
@@ -2184,17 +2705,20 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
*)
let fixed_ids : ids_sets option ref = ref None in
- (* Join the contexts at the loop entry *)
- let join_ctxs (ctx0 : C.eval_ctx) : C.eval_ctx =
+ (* Join the contexts at the loop entry - ctx1 is the current joined
+ context (the context at the loop entry, after we called
+ {!prepare_ashared_loans}, if this is the first iteration) *)
+ (* TODO: ctx_upon_entry is useless, it should be ctx0? *)
+ let join_ctxs (ctx1 : 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
+ appear in ctx1 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 =
+ let ctx1 =
match !fixed_ids with
- | Some _ -> ctx0
+ | Some _ -> ctx1
| None ->
- let old_ids, _ = compute_context_ids ctx0 in
+ let old_ids, _ = compute_context_ids ctx1 in
let new_ids, _ = compute_contexts_ids !ctxs in
let blids = V.BorrowId.Set.diff old_ids.blids new_ids.blids in
let aids = V.AbstractionId.Set.diff old_ids.aids new_ids.aids in
@@ -2208,25 +2732,27 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
in
ctx
in
- (* End the borrows/abs in [ctx0] *)
- let ctx0 = end_borrows_abs blids aids ctx0 in
+ (* End the borrows/abs in [ctx1] *)
+ let ctx1 = end_borrows_abs blids aids ctx1 in
(* We can also do the same in the contexts [ctxs]: if there are
several contexts, maybe one of them ended some borrows and some
others didn't. As we need to end those borrows anyway (the join
will detect them and ask to end them) we do it preemptively.
*)
ctxs := List.map (end_borrows_abs blids aids) !ctxs;
+ (* Note that the fixed ids are given by the original context, from *before*
+ we introduce fresh abstractions/reborrows for the shared values *)
fixed_ids := Some (fst (compute_context_ids ctx0));
- ctx0
+ ctx1
in
let fixed_ids = Option.get !fixed_ids in
- let (ctx0', _), ctx1 =
- loop_join_origin_with_continue_ctxs config loop_id fixed_ids ctx0 !ctxs
+ let (ctx1', _), ctx2 =
+ loop_join_origin_with_continue_ctxs config loop_id fixed_ids ctx1 !ctxs
in
ctxs := [];
- if !ctx_upon_entry = None then ctx_upon_entry := Some ctx0';
- ctx1
+ if !ctx_upon_entry = None then ctx_upon_entry := Some ctx1';
+ ctx2
in
(* Check if two contexts are equivalent - modulo alpha conversion on the
existentially quantified borrows/abstractions/symbolic values.
@@ -2235,7 +2761,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
(* 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 fixed_ids, _ = compute_context_ids ctx0 in
let { aids; blids; borrow_ids; loan_ids; dids; rids; sids } = fixed_ids in
let fixed_ids1, _ = compute_context_ids ctx1 in
let fixed_ids2, _ = compute_context_ids ctx2 in
@@ -2249,7 +2775,10 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
let equiv_ctxs (ctx1 : C.eval_ctx) (ctx2 : C.eval_ctx) : bool =
let fixed_ids = compute_fixed_ids ctx1 ctx2 in
let check_equivalent = true in
- Option.is_some (match_ctxs check_equivalent fixed_ids ctx1 ctx2)
+ let lookup_shared_value _ = raise (Failure "Unreachable") in
+ Option.is_some
+ (match_ctxs check_equivalent fixed_ids lookup_shared_value
+ lookup_shared_value ctx1 ctx2)
in
let max_num_iter = Config.loop_fixed_point_max_num_iters in
let rec compute_fixed_point (ctx : C.eval_ctx) (i0 : int) (i : int) :
@@ -2278,7 +2807,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
(* Check if we reached a fixed point: if not, iterate *)
if equiv_ctxs ctx ctx1 then ctx1 else compute_fixed_point ctx1 i0 (i - 1)
in
- let fp = compute_fixed_point ctx0 max_num_iter max_num_iter in
+ let fp = compute_fixed_point ctx max_num_iter max_num_iter in
(* Debug *)
log#ldebug
@@ -2426,13 +2955,13 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
log#ldebug
(lazy
("compute_loop_entry_fixed_point: merge FP \
- abstractions: "
- ^ V.AbstractionId.to_string !id0
- ^ " and "
- ^ V.AbstractionId.to_string id));
+ abstraction: "
+ ^ V.AbstractionId.to_string id
+ ^ " into "
+ ^ V.AbstractionId.to_string !id0));
(* Note that we merge *into* [id0] *)
let fp', id0' =
- merge_abstractions loop_id abs_kind false !fp id !id0
+ merge_into_abstraction loop_id abs_kind false !fp id !id0
in
fp := fp';
id0 := id0';
@@ -2442,6 +2971,11 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
!fp_ended_aids
in
+ (* Reorder the loans and borrows in the fresh abstractions in the fixed-point *)
+ let fp =
+ reorder_loans_borrows_in_fresh_abs (Option.get !fixed_ids).aids !fp
+ in
+
(* Update the abstraction's [can_end] field and their kinds.
Note that if [remove_rg_id] is [true], we set the region id to [None]
@@ -2474,7 +3008,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
let update_kinds_can_end (remove_rg_id : bool) ctx =
(update_loop_abstractions remove_rg_id)#visit_eval_ctx () ctx
in
- let fp = update_kinds_can_end false !fp in
+ let fp = update_kinds_can_end false fp in
(* Sanity check: we still have a fixed point - we simply call [compute_fixed_point]
while allowing exactly one iteration to see if it fails *)
@@ -2559,6 +3093,13 @@ let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets =
in
ids
+(** Utility *)
+type loans_borrows_pair = {
+ loans : V.BorrowId.Set.t;
+ borrows : V.BorrowId.Set.t;
+}
+[@@deriving show, ord]
+
(** For the abstractions in the fixed point, compute the correspondance between
the borrows ids and the loans ids, if we want to introduce equivalent
identity abstractions (i.e., abstractions which do nothing - the input
@@ -2658,10 +3199,21 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets)
^ "\n\n"));
(* Match the source context and the filtered target context *)
- let check_equiv = false in
let maps =
+ let check_equiv = false in
let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in
- Option.get (match_ctxs check_equiv fixed_ids filt_tgt_ctx filt_src_ctx)
+ let open InterpreterBorrowsCore in
+ let lookup_shared_loan lid ctx : V.typed_value =
+ match snd (lookup_loan ek_all lid ctx) with
+ | Concrete (V.SharedLoan (_, v)) -> v
+ | Abstract (V.ASharedLoan (_, v, _)) -> v
+ | _ -> raise (Failure "Unreachable")
+ in
+ let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in
+ let lookup_in_src id = lookup_shared_loan id src_ctx in
+ Option.get
+ (match_ctxs check_equiv fixed_ids lookup_in_tgt lookup_in_src filt_tgt_ctx
+ filt_src_ctx)
in
log#ldebug
@@ -2677,7 +3229,34 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets)
in
(* Sanity check: for every abstraction, the target loans and borrows are mapped
- to the same set of source loans and borrows *)
+ to the same set of source loans and borrows.
+
+ For instance, if we map the [env_fp] to [env0] (only looking at the bindings,
+ ignoring the abstractions) below:
+ {[
+ env0 = {
+ abs@0 { ML l0 }
+ ls -> MB l0 (s2 : loops::List<T>)
+ i -> s1 : u32
+ }
+
+ env_fp = {
+ abs@0 { ML l0 }
+ ls -> MB l1 (s3 : loops::List<T>)
+ i -> s4 : u32
+ abs@fp {
+ MB l0
+ ML l1
+ }
+ }
+ ]}
+
+ We get that l1 is mapped to l0. From there, we see that abs@fp consumes
+ the same borrows that it gives: it is indeed an identity function.
+
+ TODO: we should also check the mappings for the shared values (to
+ make sure the abstractions are indeed the identity)...
+ *)
List.iter
(fun abs ->
let ids, _ = compute_abs_ids abs in
@@ -2697,6 +3276,10 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets)
- for every tgt borrow, find the corresponding src borrow ([l0], because
we have: [borrows_map: { l1 -> l0 }])
- from there, find the corresponding tgt loan ([l0])
+
+ Note that this borrow does not necessarily appear in the src_to_tgt_borrow_map,
+ if it actually corresponds to a borrows introduced when decomposing the
+ abstractions to move the shared values out of the source context abstractions.
*)
let tgt_borrow_to_loan = ref V.BorrowId.InjSubst.empty in
let visit_tgt =
@@ -2878,7 +3461,46 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
context, which results from joins during which we ended the loans which
were introduced during the loop iterations)
*)
- let rec cf_reorganize_tgt : cm_fun =
+ (* End the borrows in the dummy values - TODO: is this useful? *)
+ let rec cf_reorganize_dummy_tgt : cm_fun =
+ fun cf tgt_ctx ->
+ (* Collect the dummy values in the target context *)
+ let _, _, tgt_dummies = ctx_split_fixed_new fixed_ids tgt_ctx in
+
+ (* Whenever we find a borrow which can be ended (doesn't contain loans)
+ we end it *)
+ let bid = ref None in
+ try
+ let visitor =
+ object
+ inherit [_] V.iter_typed_value
+
+ method! visit_SharedBorrow _ l =
+ bid := Some l;
+ raise Utils.Found
+
+ method! visit_MutBorrow _ l v =
+ if not (value_has_loans v.value) then (
+ bid := Some l;
+ raise Utils.Found)
+ else ()
+ end
+ in
+ List.iter (visitor#visit_typed_value ()) tgt_dummies;
+
+ log#ldebug
+ (lazy
+ ("match_ctx_with_target: after reorganizing dummies:\n"
+ ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- tgt_ctx: "
+ ^ eval_ctx_to_string tgt_ctx));
+
+ cf tgt_ctx
+ with Utils.Found ->
+ let cc = InterpreterBorrows.end_borrow config (Option.get !bid) in
+ comp cc cf_reorganize_dummy_tgt cf tgt_ctx
+ in
+ (* End the loans which lead to mismatches when joining *)
+ let rec cf_reorganize_join_tgt : cm_fun =
fun cf tgt_ctx ->
(* Collect fixed values in the source and target contexts: end the loans in the
source context which don't appear in the target context *)
@@ -2946,7 +3568,7 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
| AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ ->
raise (Failure "Unexpected")
in
- comp cc cf_reorganize_tgt cf tgt_ctx
+ comp cc cf_reorganize_join_tgt cf tgt_ctx
in
(* Introduce the "identity" abstractions for the loop reentry.
@@ -2976,7 +3598,18 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
let check_equiv = false in
let src_to_tgt_maps =
let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in
- Option.get (match_ctxs check_equiv fixed_ids filt_src_ctx filt_tgt_ctx)
+ let open InterpreterBorrowsCore in
+ let lookup_shared_loan lid ctx : V.typed_value =
+ match snd (lookup_loan ek_all lid ctx) with
+ | Concrete (V.SharedLoan (_, v)) -> v
+ | Abstract (V.ASharedLoan (_, v, _)) -> v
+ | _ -> raise (Failure "Unreachable")
+ in
+ let lookup_in_src id = lookup_shared_loan id src_ctx in
+ let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in
+ Option.get
+ (match_ctxs check_equiv fixed_ids lookup_in_src lookup_in_tgt
+ filt_src_ctx filt_tgt_ctx)
in
let tgt_to_src_borrow_map =
V.BorrowId.Map.of_list
@@ -2988,8 +3621,9 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
(* Debug *)
log#ldebug
(lazy
- ("match_ctx_with_target:cf_introduce_loop_fp_abs:"
- ^ "\n\n- filt_tgt_ctx: "
+ ("match_ctx_with_target:cf_introduce_loop_fp_abs:" ^ "\n\n- tgt_ctx: "
+ ^ eval_ctx_to_string tgt_ctx ^ "\n\n- src_ctx: "
+ ^ eval_ctx_to_string src_ctx ^ "\n\n- filt_tgt_ctx: "
^ eval_ctx_to_string filt_tgt_ctx
^ "\n\n- filt_src_ctx: "
^ eval_ctx_to_string filt_src_ctx
@@ -2998,7 +3632,7 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
(* Update the borrows and symbolic ids in the source context.
- Going back to the [list_nth_mut_example], the source environment upon
+ Going back to the [list_nth_mut_example], the original environment upon
re-entering the loop is:
{[
@@ -3038,6 +3672,11 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
_@3 -> MB l1 (s@3 : T) // hd
abs@1 { MB l4, ML l5 }
]}
+
+ Later, we will introduce the identity abstraction:
+ {[
+ abs@2 { MB l5, ML l6 }
+ ]}
*)
let src_fresh_borrows_map = ref V.BorrowId.Map.empty in
let visit_tgt =
@@ -3130,16 +3769,15 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
end
in
let new_absl = List.map (visit_src#visit_abs ()) new_absl in
+ let new_absl = List.map (fun abs -> C.Abs abs) new_absl in
(* Add the abstractions from the target context to the source context *)
- let nenv =
- List.append (List.map (fun abs -> C.Abs abs) new_absl) tgt_ctx.env
- in
+ let nenv = List.append new_absl tgt_ctx.env in
let tgt_ctx = { tgt_ctx with env = nenv } in
log#ldebug
(lazy
- ("match_ctx_with_target:cf_introduce_loop_fp_abs:\n- result ctx:"
+ ("match_ctx_with_target:cf_introduce_loop_fp_abs:\n- result ctx:\n"
^ eval_ctx_to_string tgt_ctx));
(* Sanity check *)
@@ -3165,7 +3803,8 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
in
(* Compose and continue *)
- cf_reorganize_tgt cf_introduce_loop_fp_abs tgt_ctx
+ comp cf_reorganize_dummy_tgt cf_reorganize_join_tgt cf_introduce_loop_fp_abs
+ tgt_ctx
(** Evaluate a loop in concrete mode *)
let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun =
@@ -3224,6 +3863,12 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
(* Compute a fresh loop id *)
let loop_id = C.fresh_loop_id () in
+
+ log#ldebug
+ (lazy
+ ("eval_loop_symbolic:\nContext after shared borrows preparation:\n"
+ ^ eval_ctx_to_string ctx ^ "\n\n"));
+
(* Compute the fixed point at the loop entrance *)
let fp_ctx, fixed_ids =
compute_loop_entry_fixed_point config loop_id eval_loop_body ctx
@@ -3282,9 +3927,58 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
let old_ids, _ = compute_context_ids ctx in
let fp_ids, fp_ids_maps = compute_context_ids fp_ctx in
let fresh_sids = V.SymbolicValueId.Set.diff fp_ids.sids old_ids.sids in
+
+ (* Compute the set of symbolic values which appear in shared values inside
+ *fixed* abstractions: because we introduce fresh abstractions and reborrows
+ with {!prepare_ashared_loans}, those values are never accessed directly
+ inside the loop iterations: we can ignore them (and should, because
+ otherwise it leads to a very ugly translation with duplicated, unused
+ values) *)
+ let shared_sids_in_fixed_abs =
+ let fixed_absl =
+ List.filter
+ (fun (ee : C.env_elem) ->
+ match ee with
+ | C.Var _ | C.Frame -> false
+ | Abs abs -> V.AbstractionId.Set.mem abs.abs_id old_ids.aids)
+ ctx.env
+ in
+
+ (* Rem.: as we greedily expand the symbolic values containing borrows, and
+ in particular the (mutable/shared) borrows, we could simply list the
+ symbolic values appearing in the abstractions: those are necessarily
+ shared values. We prefer to be more general, in prevision of later
+ changes.
+ *)
+ let sids = ref V.SymbolicValueId.Set.empty in
+ let visitor =
+ object (self : 'self)
+ inherit [_] C.iter_env
+
+ method! visit_ASharedLoan inside_shared _ sv child_av =
+ self#visit_typed_value true sv;
+ self#visit_typed_avalue inside_shared child_av
+
+ method! visit_symbolic_value_id inside_shared sid =
+ if inside_shared then sids := V.SymbolicValueId.Set.add sid !sids
+ end
+ in
+ visitor#visit_env false fixed_absl;
+ !sids
+ in
+
+ (* Remove the shared symbolic values present in the fixed abstractions -
+ see comments for [shared_sids_in_fixed_abs]. *)
+ let sids_to_values = fp_ids_maps.sids_to_values in
+ let sids_to_values =
+ V.SymbolicValueId.Map.filter
+ (fun sid _ ->
+ not (V.SymbolicValueId.Set.mem sid shared_sids_in_fixed_abs))
+ sids_to_values
+ in
(* The value ids should be listed in increasing order *)
let input_svalues =
- List.map snd (V.SymbolicValueId.Map.bindings fp_ids_maps.sids_to_values)
+ List.map snd (V.SymbolicValueId.Map.bindings sids_to_values)
in
(fresh_sids, input_svalues)
in
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 408184e0..670435a5 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -259,6 +259,11 @@ let rvalue_get_place (rv : E.rvalue) : E.place option =
| Ref (p, _) -> Some p
| UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None
+(** See {!ValuesUtils.symbolic_value_has_borrows} *)
+let symbolic_value_has_borrows (ctx : C.eval_ctx) (sv : V.symbolic_value) : bool
+ =
+ ValuesUtils.symbolic_value_has_borrows ctx.type_context.type_infos sv
+
(** See {!ValuesUtils.value_has_borrows}. *)
let value_has_borrows (ctx : C.eval_ctx) (v : V.value) : bool =
ValuesUtils.value_has_borrows ctx.type_context.type_infos v
@@ -267,6 +272,9 @@ let value_has_borrows (ctx : C.eval_ctx) (v : V.value) : bool =
let value_has_loans_or_borrows (ctx : C.eval_ctx) (v : V.value) : bool =
ValuesUtils.value_has_loans_or_borrows ctx.type_context.type_infos v
+(** See {!ValuesUtils.value_has_loans}. *)
+let value_has_loans (v : V.value) : bool = ValuesUtils.value_has_loans v
+
(** See {!compute_typed_value_ids}, {!compute_context_ids}, etc. *)
type ids_sets = {
aids : V.AbstractionId.Set.t;
@@ -360,6 +368,12 @@ let compute_absl_ids (xl : V.abs list) : ids_sets * ids_to_values =
let compute_abs_ids (x : V.abs) : ids_sets * ids_to_values =
compute_absl_ids [ x ]
+(** Compute the sets of ids found in an environment element. *)
+let compute_env_elem_ids (x : C.env_elem) : ids_sets * ids_to_values =
+ let compute, get_ids, get_ids_to_values = compute_ids () in
+ compute#visit_env_elem () x;
+ (get_ids (), get_ids_to_values ())
+
(** Compute the sets of ids found in a list of contexts. *)
let compute_contexts_ids (ctxl : C.eval_ctx list) : ids_sets * ids_to_values =
let compute, get_ids, get_ids_to_values = compute_ids () in
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 27dcb330..c69e6441 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -627,7 +627,14 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
given_back_ls
| V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> ())
| V.AIgnored, _ -> ()
- | _ -> raise (Failure "Erroneous typing"));
+ | _ ->
+ log#lerror
+ (lazy
+ ("Erroneous typing:" ^ "\n- raw value: "
+ ^ V.show_typed_avalue atv ^ "\n- value: "
+ ^ typed_avalue_to_string ctx atv
+ ^ "\n- type: " ^ rty_to_string ctx atv.V.ty));
+ raise (Failure "Erroneous typing"));
(* Continue exploring to inspect the subterms *)
super#visit_typed_avalue info atv
end
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index fdb07535..5040fd9f 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -27,6 +27,17 @@ let ty_substitute (rsubst : 'r1 -> 'r2) (tsubst : T.TypeVarId.id -> 'r2 T.ty)
visitor#visit_ty () ty
+let rty_substitute (rsubst : T.RegionId.id -> T.RegionId.id)
+ (tsubst : T.TypeVarId.id -> T.rty) (ty : T.rty) : T.rty =
+ let rsubst r =
+ match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid)
+ in
+ ty_substitute rsubst tsubst ty
+
+let ety_substitute (tsubst : T.TypeVarId.id -> T.ety) (ty : T.ety) : T.ety =
+ let rsubst r = r in
+ ty_substitute rsubst tsubst ty
+
(** Convert an {!T.rty} to an {!T.ety} by erasing the region variables *)
let erase_regions (ty : T.rty) : T.ety =
ty_substitute (fun _ -> T.Erased) (fun vid -> T.TypeVar vid) ty
@@ -354,7 +365,7 @@ let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
let regions_hierarchy = List.map subst_region_group sg.A.regions_hierarchy in
{ A.regions_hierarchy; inputs; output }
-(** Substitute identifiers in a type *)
+(** Substitute type variable identifiers in a type *)
let ty_substitute_ids (tsubst : T.TypeVarId.id -> T.TypeVarId.id) (ty : 'r T.ty)
: 'r T.ty =
let open T in
@@ -440,6 +451,15 @@ let typed_value_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
(subst_ids_visitor rsubst rvsubst tsubst ssubst bsubst asubst)
#visit_typed_value v
+let typed_value_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
+ (v : V.typed_value) : V.typed_value =
+ typed_value_subst_ids rsubst
+ (fun x -> x)
+ (fun x -> x)
+ (fun x -> x)
+ (fun x -> x)
+ v
+
let typed_avalue_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
(rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
(tsubst : T.TypeVarId.id -> T.TypeVarId.id)
@@ -458,6 +478,14 @@ let abs_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
(asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : V.abs) : V.abs =
(subst_ids_visitor rsubst rvsubst tsubst ssubst bsubst asubst)#visit_abs x
+let env_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
+ (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
+ (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
+ (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
+ (bsubst : V.BorrowId.id -> V.BorrowId.id)
+ (asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : C.env) : C.env =
+ (subst_ids_visitor rsubst rvsubst tsubst ssubst bsubst asubst)#visit_env x
+
let typed_avalue_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
(x : V.typed_avalue) : V.typed_avalue =
let asubst _ = raise (Failure "Unreachable") in
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index ad603bd5..174fc4d1 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -245,6 +245,10 @@ let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
let fmt = Print.PC.ctx_to_rtype_formatter fmt in
Print.PV.symbolic_value_to_string fmt sv
+let typed_value_to_string (ctx : bs_ctx) (v : V.typed_value) : string =
+ let fmt = bs_ctx_to_ctx_formatter ctx in
+ Print.PV.typed_value_to_string fmt v
+
let ty_to_string (ctx : bs_ctx) (ty : ty) : string =
let fmt = bs_ctx_to_pp_ast_formatter ctx in
let fmt = PrintPure.ast_to_type_formatter fmt in
@@ -2116,6 +2120,17 @@ and translate_forward_end (ectx : C.eval_ctx)
(* Lookup the loop information *)
let loop_info = LoopId.Map.find loop_id ctx.loops in
+ log#ldebug
+ (lazy
+ ("translate_forward_end:\n- loop_input_values:\n"
+ ^ V.SymbolicValueId.Map.show
+ (typed_value_to_string ctx)
+ loop_input_values
+ ^ "\n- loop_info.input_svl:\n"
+ ^ Print.list_to_string
+ (symbolic_value_to_string ctx)
+ loop_info.input_svl));
+
(* Translate the input values *)
let loop_input_values =
List.map
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index adeb105f..4612b019 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -11,6 +11,7 @@ let mk_unit_value : typed_value =
{ value = Adt { variant_id = None; field_values = [] }; ty = mk_unit_ty }
let mk_typed_value (ty : ety) (value : value) : typed_value = { value; ty }
+let mk_typed_avalue (ty : rty) (value : avalue) : typed_avalue = { value; ty }
let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty }
let mk_abottom (ty : rty) : typed_avalue = { value = ABottom; ty }
let mk_aignored (ty : rty) : typed_avalue = { value = AIgnored; ty }
@@ -155,6 +156,11 @@ let rec value_strip_shared_loans (v : typed_value) : typed_value =
| Loan (SharedLoan (_, v')) -> value_strip_shared_loans v'
| _ -> v
+(** Check if a symbolic value has borrows *)
+let symbolic_value_has_borrows (infos : TA.type_infos) (sv : symbolic_value) :
+ bool =
+ ty_has_borrow_under_mut infos sv.sv_ty
+
(** Check if a value has borrows in **a general sense**.
It checks if:
@@ -168,7 +174,7 @@ let value_has_borrows (infos : TA.type_infos) (v : value) : bool =
method! visit_borrow_content _env _ = raise Found
method! visit_symbolic_value _ sv =
- if ty_has_borrow_under_mut infos sv.sv_ty then raise Found else ()
+ if symbolic_value_has_borrows infos sv then raise Found else ()
end
in
(* We use exceptions *)
@@ -218,3 +224,17 @@ let value_has_loans_or_borrows (infos : TA.type_infos) (v : value) : bool =
obj#visit_value () v;
false
with Found -> true
+
+(** Remove the shared loans in a value *)
+let value_remove_shared_loans (v : typed_value) : typed_value =
+ let visitor =
+ object (self : 'self)
+ inherit [_] map_typed_value as super
+
+ method! visit_typed_value env v =
+ match v.value with
+ | Loan (SharedLoan (_, sv)) -> self#visit_typed_value env sv
+ | _ -> super#visit_typed_value env v
+ end
+ in
+ visitor#visit_typed_value () v
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 67ee0880..4fc68e1c 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -22,8 +22,8 @@ Definition sum_fwd (n : nat) (max : u32) : result u32 :=
sum_loop_fwd n max (0%u32) (0%u32)
.
-(** [loops::sum_with_borrows] *)
-Fixpoint sum_with_borrows_loop_fwd
+(** [loops::sum_with_mut_borrows] *)
+Fixpoint sum_with_mut_borrows_loop_fwd
(n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 :=
match n with
| O => Fail_ OutOfFuel
@@ -32,14 +32,34 @@ Fixpoint sum_with_borrows_loop_fwd
then (
ms0 <- u32_add ms mi;
mi0 <- u32_add mi 1%u32;
- sum_with_borrows_loop_fwd n0 max mi0 ms0)
+ sum_with_mut_borrows_loop_fwd n0 max mi0 ms0)
else u32_mul ms 2%u32
end
.
-(** [loops::sum_with_borrows] *)
-Definition sum_with_borrows_fwd (n : nat) (max : u32) : result u32 :=
- sum_with_borrows_loop_fwd n max (0%u32) (0%u32)
+(** [loops::sum_with_mut_borrows] *)
+Definition sum_with_mut_borrows_fwd (n : nat) (max : u32) : result u32 :=
+ sum_with_mut_borrows_loop_fwd n max (0%u32) (0%u32)
+.
+
+(** [loops::sum_with_shared_borrows] *)
+Fixpoint sum_with_shared_borrows_loop_fwd
+ (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ if i s< max
+ then (
+ i0 <- u32_add i 1%u32;
+ s0 <- u32_add s i0;
+ sum_with_shared_borrows_loop_fwd n0 max i0 s0)
+ else u32_mul s 2%u32
+ end
+.
+
+(** [loops::sum_with_shared_borrows] *)
+Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 :=
+ sum_with_shared_borrows_loop_fwd n max (0%u32) (0%u32)
.
(** [loops::List] *)
@@ -102,6 +122,28 @@ Definition list_nth_mut_loop_back
list_nth_mut_loop_loop_back T n ls i ret
.
+(** [loops::list_nth_shared_loop] *)
+Fixpoint list_nth_shared_loop_loop_fwd
+ (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match ls with
+ | ListCons x tl =>
+ if i s= 0%u32
+ then Return x
+ else (i0 <- u32_sub i 1%u32; list_nth_shared_loop_loop_fwd T n0 tl i0)
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_shared_loop] *)
+Definition list_nth_shared_loop_fwd
+ (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
+ list_nth_shared_loop_loop_fwd T n ls i
+.
+
(** [loops::list_nth_mut_loop_pair] *)
Fixpoint list_nth_mut_loop_pair_loop_fwd
(T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
@@ -200,6 +242,38 @@ Definition list_nth_mut_loop_pair_back'b
list_nth_mut_loop_pair_loop_back'b T n ls0 ls1 i ret
.
+(** [loops::list_nth_shared_loop_pair] *)
+Fixpoint list_nth_shared_loop_pair_loop_fwd
+ (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match l with
+ | ListCons x0 tl0 =>
+ match l0 with
+ | ListCons x1 tl1 =>
+ if i s= 0%u32
+ then Return (x0, x1)
+ else (
+ i0 <- u32_sub i 1%u32;
+ list_nth_shared_loop_pair_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_shared_loop_pair] *)
+Definition list_nth_shared_loop_pair_fwd
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ list_nth_shared_loop_pair_loop_fwd T n ls0 ls1 i
+.
+
(** [loops::list_nth_mut_loop_pair_merge] *)
Fixpoint list_nth_mut_loop_pair_merge_loop_fwd
(T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
@@ -268,4 +342,298 @@ Definition list_nth_mut_loop_pair_merge_back
list_nth_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret
.
+(** [loops::list_nth_shared_loop_pair_merge] *)
+Fixpoint list_nth_shared_loop_pair_merge_loop_fwd
+ (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match l with
+ | ListCons x0 tl0 =>
+ match l0 with
+ | ListCons x1 tl1 =>
+ if i s= 0%u32
+ then Return (x0, x1)
+ else (
+ i0 <- u32_sub i 1%u32;
+ list_nth_shared_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_shared_loop_pair_merge] *)
+Definition list_nth_shared_loop_pair_merge_fwd
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ list_nth_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i
+.
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+Fixpoint list_nth_mut_shared_loop_pair_loop_fwd
+ (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match l with
+ | ListCons x0 tl0 =>
+ match l0 with
+ | ListCons x1 tl1 =>
+ if i s= 0%u32
+ then Return (x0, x1)
+ else (
+ i0 <- u32_sub i 1%u32;
+ list_nth_mut_shared_loop_pair_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+Definition list_nth_mut_shared_loop_pair_fwd
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ list_nth_mut_shared_loop_pair_loop_fwd T n ls0 ls1 i
+.
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+Fixpoint list_nth_mut_shared_loop_pair_loop_back
+ (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match l with
+ | ListCons x0 tl0 =>
+ match l0 with
+ | ListCons x1 tl1 =>
+ if i s= 0%u32
+ then Return (ListCons ret tl0)
+ else (
+ i0 <- u32_sub i 1%u32;
+ l1 <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+ Return (ListCons x0 l1))
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+Definition list_nth_mut_shared_loop_pair_back
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ list_nth_mut_shared_loop_pair_loop_back T n ls0 ls1 i ret
+.
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd
+ (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match l with
+ | ListCons x0 tl0 =>
+ match l0 with
+ | ListCons x1 tl1 =>
+ if i s= 0%u32
+ then Return (x0, x1)
+ else (
+ i0 <- u32_sub i 1%u32;
+ list_nth_mut_shared_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+Definition list_nth_mut_shared_loop_pair_merge_fwd
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ list_nth_mut_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i
+.
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back
+ (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match l with
+ | ListCons x0 tl0 =>
+ match l0 with
+ | ListCons x1 tl1 =>
+ if i s= 0%u32
+ then Return (ListCons ret tl0)
+ else (
+ i0 <- u32_sub i 1%u32;
+ l1 <-
+ list_nth_mut_shared_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
+ Return (ListCons x0 l1))
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+Definition list_nth_mut_shared_loop_pair_merge_back
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ list_nth_mut_shared_loop_pair_merge_loop_back T n ls0 ls1 i ret
+.
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+Fixpoint list_nth_shared_mut_loop_pair_loop_fwd
+ (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match l with
+ | ListCons x0 tl0 =>
+ match l0 with
+ | ListCons x1 tl1 =>
+ if i s= 0%u32
+ then Return (x0, x1)
+ else (
+ i0 <- u32_sub i 1%u32;
+ list_nth_shared_mut_loop_pair_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+Definition list_nth_shared_mut_loop_pair_fwd
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ list_nth_shared_mut_loop_pair_loop_fwd T n ls0 ls1 i
+.
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+Fixpoint list_nth_shared_mut_loop_pair_loop_back
+ (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match l with
+ | ListCons x0 tl0 =>
+ match l0 with
+ | ListCons x1 tl1 =>
+ if i s= 0%u32
+ then Return (ListCons ret tl1)
+ else (
+ i0 <- u32_sub i 1%u32;
+ l1 <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+ Return (ListCons x1 l1))
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+Definition list_nth_shared_mut_loop_pair_back
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ list_nth_shared_mut_loop_pair_loop_back T n ls0 ls1 i ret
+.
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd
+ (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match l with
+ | ListCons x0 tl0 =>
+ match l0 with
+ | ListCons x1 tl1 =>
+ if i s= 0%u32
+ then Return (x0, x1)
+ else (
+ i0 <- u32_sub i 1%u32;
+ list_nth_shared_mut_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+Definition list_nth_shared_mut_loop_pair_merge_fwd
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ list_nth_shared_mut_loop_pair_merge_loop_fwd T n ls0 ls1 i
+.
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back
+ (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match l with
+ | ListCons x0 tl0 =>
+ match l0 with
+ | ListCons x1 tl1 =>
+ if i s= 0%u32
+ then Return (ListCons ret tl1)
+ else (
+ i0 <- u32_sub i 1%u32;
+ l1 <-
+ list_nth_shared_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
+ Return (ListCons x1 l1))
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+Definition list_nth_shared_mut_loop_pair_merge_back
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ list_nth_shared_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret
+.
+
End Loops .
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index 3e44ef4f..cd29ca13 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -9,9 +9,14 @@ open Loops.Types
(** [loops::sum]: decreases clause *)
unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat = admit ()
-(** [loops::sum_with_borrows]: decreases clause *)
+(** [loops::sum_with_mut_borrows]: decreases clause *)
unfold
-let sum_with_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+let sum_with_mut_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+ admit ()
+
+(** [loops::sum_with_shared_borrows]: decreases clause *)
+unfold
+let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat =
admit ()
(** [loops::list_nth_mut_loop]: decreases clause *)
@@ -19,15 +24,57 @@ unfold
let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
admit ()
+(** [loops::list_nth_shared_loop]: decreases clause *)
+unfold
+let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat
+ =
+ admit ()
+
(** [loops::list_nth_mut_loop_pair]: decreases clause *)
unfold
let list_nth_mut_loop_pair_decreases (t : Type0) (l : list_t t) (l0 : list_t t)
(i : u32) : nat =
admit ()
+(** [loops::list_nth_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : nat =
+ admit ()
+
(** [loops::list_nth_mut_loop_pair_merge]: decreases clause *)
unfold
let list_nth_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
(l0 : list_t t) (i : u32) : nat =
admit ()
+(** [loops::list_nth_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : nat =
+ admit ()
+
+(** [loops::list_nth_mut_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : nat =
+ admit ()
+
+(** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : nat =
+ admit ()
+
+(** [loops::list_nth_shared_mut_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : nat =
+ admit ()
+
+(** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : nat =
+ admit ()
+
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index d315a4f0..9cf5db1f 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -9,25 +9,70 @@ open Loops.Types
unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat =
if i <= max then max - i else 0
+(** [loops::sum_with_mut_borrows]: decreases clause *)
+unfold
+let sum_with_mut_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+ if max >= mi then max - mi else 0
-(** [loops::sum_with_borrows]: decreases clause *)
+(** [loops::sum_with_shared_borrows]: decreases clause *)
unfold
-let sum_with_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
- if mi <= max then max - mi else 0
+let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat =
+ if max >= i then max - i else 0
(** [loops::list_nth_mut_loop]: decreases clause *)
unfold
let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
i
+(** [loops::list_nth_shared_loop]: decreases clause *)
+unfold
+let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : list_t t =
+ ls
+
(** [loops::list_nth_mut_loop_pair]: decreases clause *)
unfold
let list_nth_mut_loop_pair_decreases (t : Type0) (l : list_t t) (l0 : list_t t)
(i : u32) : nat =
i
+(** [loops::list_nth_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
(** [loops::list_nth_mut_loop_pair_merge]: decreases clause *)
unfold
let list_nth_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
(l0 : list_t t) (i : u32) : nat =
i
+
+(** [loops::list_nth_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
+(** [loops::list_nth_mut_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
+(** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
+(** [loops::list_nth_shared_mut_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
+(** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 05d1f70f..ee8e95d2 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -27,10 +27,10 @@ let rec sum_loop_fwd
(** [loops::sum] *)
let sum_fwd (max : u32) : result u32 = sum_loop_fwd max 0 0
-(** [loops::sum_with_borrows] *)
-let rec sum_with_borrows_loop_fwd
+(** [loops::sum_with_mut_borrows] *)
+let rec sum_with_mut_borrows_loop_fwd
(max : u32) (mi : u32) (ms : u32) :
- Tot (result u32) (decreases (sum_with_borrows_decreases max mi ms))
+ Tot (result u32) (decreases (sum_with_mut_borrows_decreases max mi ms))
=
if mi < max
then
@@ -39,14 +39,35 @@ let rec sum_with_borrows_loop_fwd
| Return ms0 ->
begin match u32_add mi 1 with
| Fail e -> Fail e
- | Return mi0 -> sum_with_borrows_loop_fwd max mi0 ms0
+ | Return mi0 -> sum_with_mut_borrows_loop_fwd max mi0 ms0
end
end
else u32_mul ms 2
-(** [loops::sum_with_borrows] *)
-let sum_with_borrows_fwd (max : u32) : result u32 =
- sum_with_borrows_loop_fwd max 0 0
+(** [loops::sum_with_mut_borrows] *)
+let sum_with_mut_borrows_fwd (max : u32) : result u32 =
+ sum_with_mut_borrows_loop_fwd max 0 0
+
+(** [loops::sum_with_shared_borrows] *)
+let rec sum_with_shared_borrows_loop_fwd
+ (max : u32) (i : u32) (s : u32) :
+ Tot (result u32) (decreases (sum_with_shared_borrows_decreases max i s))
+ =
+ if i < max
+ then
+ begin match u32_add i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ begin match u32_add s i0 with
+ | Fail e -> Fail e
+ | Return s0 -> sum_with_shared_borrows_loop_fwd max i0 s0
+ end
+ end
+ else u32_mul s 2
+
+(** [loops::sum_with_shared_borrows] *)
+let sum_with_shared_borrows_fwd (max : u32) : result u32 =
+ sum_with_shared_borrows_loop_fwd max 0 0
(** [loops::list_nth_mut_loop] *)
let rec list_nth_mut_loop_loop_fwd
@@ -95,6 +116,27 @@ let list_nth_mut_loop_back
(t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
list_nth_mut_loop_loop_back t ls i ret
+(** [loops::list_nth_shared_loop] *)
+let rec list_nth_shared_loop_loop_fwd
+ (t : Type0) (ls : list_t t) (i : u32) :
+ Tot (result t) (decreases (list_nth_shared_loop_decreases t ls i))
+ =
+ begin match ls with
+ | ListCons x tl ->
+ if i = 0
+ then Return x
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 -> list_nth_shared_loop_loop_fwd t tl i0
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_loop] *)
+let list_nth_shared_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t =
+ list_nth_shared_loop_loop_fwd t ls i
+
(** [loops::list_nth_mut_loop_pair] *)
let rec list_nth_mut_loop_pair_loop_fwd
(t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
@@ -187,6 +229,33 @@ let list_nth_mut_loop_pair_back'b
=
list_nth_mut_loop_pair_loop_back'b t ls0 ls1 i ret
+(** [loops::list_nth_shared_loop_pair] *)
+let rec list_nth_shared_loop_pair_loop_fwd
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+ Tot (result (t & t))
+ (decreases (list_nth_shared_loop_pair_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (x0, x1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 -> list_nth_shared_loop_pair_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_loop_pair] *)
+let list_nth_shared_loop_pair_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_shared_loop_pair_loop_fwd t ls0 ls1 i
+
(** [loops::list_nth_mut_loop_pair_merge] *)
let rec list_nth_mut_loop_pair_merge_loop_fwd
(t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
@@ -248,3 +317,276 @@ let list_nth_mut_loop_pair_merge_back
=
list_nth_mut_loop_pair_merge_loop_back t ls0 ls1 i ret
+(** [loops::list_nth_shared_loop_pair_merge] *)
+let rec list_nth_shared_loop_pair_merge_loop_fwd
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+ Tot (result (t & t))
+ (decreases (list_nth_shared_loop_pair_merge_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (x0, x1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 -> list_nth_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_loop_pair_merge] *)
+let list_nth_shared_loop_pair_merge_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_shared_loop_pair_merge_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+let rec list_nth_mut_shared_loop_pair_loop_fwd
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+ Tot (result (t & t))
+ (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (x0, x1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 -> list_nth_mut_shared_loop_pair_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+let list_nth_mut_shared_loop_pair_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_mut_shared_loop_pair_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+let rec list_nth_mut_shared_loop_pair_loop_back
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+ Tot (result (list_t t))
+ (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (ListCons ret tl0)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ begin match list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret
+ with
+ | Fail e -> Fail e
+ | Return l1 -> Return (ListCons x0 l1)
+ end
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+let list_nth_mut_shared_loop_pair_back
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+ result (list_t t)
+ =
+ list_nth_mut_shared_loop_pair_loop_back t ls0 ls1 i ret
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+let rec list_nth_mut_shared_loop_pair_merge_loop_fwd
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+ Tot (result (t & t))
+ (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (x0, x1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ list_nth_mut_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+let list_nth_mut_shared_loop_pair_merge_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_mut_shared_loop_pair_merge_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+let rec list_nth_mut_shared_loop_pair_merge_loop_back
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+ Tot (result (list_t t))
+ (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (ListCons ret tl0)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ begin match
+ list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
+ | Fail e -> Fail e
+ | Return l1 -> Return (ListCons x0 l1)
+ end
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+let list_nth_mut_shared_loop_pair_merge_back
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+ result (list_t t)
+ =
+ list_nth_mut_shared_loop_pair_merge_loop_back t ls0 ls1 i ret
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+let rec list_nth_shared_mut_loop_pair_loop_fwd
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+ Tot (result (t & t))
+ (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (x0, x1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 -> list_nth_shared_mut_loop_pair_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+let list_nth_shared_mut_loop_pair_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_shared_mut_loop_pair_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+let rec list_nth_shared_mut_loop_pair_loop_back
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+ Tot (result (list_t t))
+ (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (ListCons ret tl1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ begin match list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret
+ with
+ | Fail e -> Fail e
+ | Return l1 -> Return (ListCons x1 l1)
+ end
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+let list_nth_shared_mut_loop_pair_back
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+ result (list_t t)
+ =
+ list_nth_shared_mut_loop_pair_loop_back t ls0 ls1 i ret
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+let rec list_nth_shared_mut_loop_pair_merge_loop_fwd
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+ Tot (result (t & t))
+ (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (x0, x1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ list_nth_shared_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+let list_nth_shared_mut_loop_pair_merge_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_shared_mut_loop_pair_merge_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+let rec list_nth_shared_mut_loop_pair_merge_loop_back
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+ Tot (result (list_t t))
+ (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (ListCons ret tl1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ begin match
+ list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
+ | Fail e -> Fail e
+ | Return l1 -> Return (ListCons x1 l1)
+ end
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+let list_nth_shared_mut_loop_pair_merge_back
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+ result (list_t t)
+ =
+ list_nth_shared_mut_loop_pair_merge_loop_back t ls0 ls1 i ret
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 07:49:19 +0000