summaryrefslogtreecommitdiff
path: root/compiler/InterpreterBorrows.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/InterpreterBorrows.ml')
-rw-r--r--compiler/InterpreterBorrows.ml487
1 files changed, 244 insertions, 243 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 17810705..ae251fbf 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -7,6 +7,7 @@ open TypesUtils
open InterpreterUtils
open InterpreterBorrowsCore
open InterpreterProjectors
+open Errors
(** The local logger *)
let log = Logging.borrows_log
@@ -29,7 +30,7 @@ let log = Logging.borrows_log
loans. This is used to merge borrows with abstractions, to compute loop
fixed points for instance.
*)
-let end_borrow_get_borrow (allowed_abs : AbstractionId.id option)
+let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id option)
(allow_inner_loans : bool) (l : BorrowId.id) (ctx : eval_ctx) :
( eval_ctx * (AbstractionId.id option * g_borrow_content) option,
priority_borrows_or_abs )
@@ -41,7 +42,7 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option)
in
let set_replaced_bc (abs_id : AbstractionId.id option) (bc : g_borrow_content)
=
- assert (Option.is_none !replaced_bc);
+ cassert (Option.is_none !replaced_bc) meta "TODO: error message";
replaced_bc := Some (abs_id, bc)
in
(* Raise an exception if:
@@ -180,7 +181,7 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option)
* Also note that, as we are moving the borrowed value inside the
* abstraction (and not really giving the value back to the context)
* we do not insert {!AEndedMutBorrow} but rather {!ABottom} *)
- raise (Failure "Unimplemented")
+ craise meta "Unimplemented"
(* ABottom *))
else
(* Update the outer borrows before diving into the child avalue *)
@@ -223,8 +224,8 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option)
method! visit_abs outer abs =
(* Update the outer abs *)
let outer_abs, outer_borrows = outer in
- assert (Option.is_none outer_abs);
- assert (Option.is_none outer_borrows);
+ cassert (Option.is_none outer_abs) meta "TODO: error message";
+ cassert (Option.is_none outer_borrows) meta "TODO: error message";
let outer = (Some abs.abs_id, None) in
super#visit_abs outer abs
end
@@ -244,11 +245,11 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option)
give the value back.
TODO: this was not the case before, so some sanity checks are not useful anymore.
*)
-let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
+let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv : typed_value)
(ctx : eval_ctx) : eval_ctx =
(* Sanity check *)
- assert (not (loans_in_value nv));
- assert (not (bottom_in_value ctx.ended_regions nv));
+ cassert (not (loans_in_value nv)) meta "TODO: error message";
+ cassert (not (bottom_in_value ctx.ended_regions nv)) meta "TODO: error message";
(* Debug *)
log#ldebug
(lazy
@@ -258,7 +259,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
(* We use a reference to check that we updated exactly one loan *)
let replaced : bool ref = ref false in
let set_replaced () =
- assert (not !replaced);
+ cassert (not !replaced) meta "Exactly one loan should have been updated";
replaced := true
in
(* Whenever giving back symbolic values, they shouldn't contain already ended regions *)
@@ -300,7 +301,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
("give_back_value: improper type:\n- expected: "
^ ty_to_string ctx ty ^ "\n- received: "
^ ty_to_string ctx nv.ty);
- raise (Failure "Value given back doesn't have the proper type"));
+ craise meta "Value given back doesn't have the proper type");
(* Replace *)
set_replaced ();
nv.value)
@@ -345,7 +346,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
ABorrow
(AEndedIgnoredMutBorrow
{ given_back; child; given_back_meta })
- | _ -> raise (Failure "Unreachable")
+ | _ -> craise meta "Unreachable"
else
(* Continue exploring *)
ABorrow (super#visit_AIgnoredMutBorrow opt_abs bid' child)
@@ -360,7 +361,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
(* Preparing a bit *)
let regions, ancestors_regions =
match opt_abs with
- | None -> raise (Failure "Unreachable")
+ | None -> craise meta "Unreachable"
| Some abs -> (abs.regions, abs.ancestors_regions)
in
(* Rk.: there is a small issue with the types of the aloan values.
@@ -426,7 +427,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
(* We remember in which abstraction we are before diving -
* this is necessary for projecting values: we need to know
* over which regions to project *)
- assert (Option.is_none opt_abs);
+ cassert (Option.is_none opt_abs) meta "TODO: error message";
super#visit_EAbs (Some abs) abs
end
in
@@ -434,16 +435,16 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
(* Explore the environment *)
let ctx = obj#visit_eval_ctx None ctx in
(* Check we gave back to exactly one loan *)
- assert !replaced;
+ cassert !replaced meta "Only one loan should have been given back";
(* Apply the reborrows *)
apply_registered_reborrows ctx
(** Give back a *modified* symbolic value. *)
-let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t)
+let give_back_symbolic_value (meta : Meta.meta) (_config : config) (proj_regions : RegionId.Set.t)
(proj_ty : rty) (sv : symbolic_value) (nsv : symbolic_value)
(ctx : eval_ctx) : eval_ctx =
(* Sanity checks *)
- assert (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty);
+ cassert (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty) meta "TODO: error message";
(* Store the given-back value as a meta-value for synthesis purposes *)
let mv = nsv in
(* Substitution function, to replace the borrow projectors over symbolic values *)
@@ -465,11 +466,11 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t)
type [T]! We thus *mustn't* introduce a projector here.
*)
(* AProjBorrows (nsv, sv.sv_ty) *)
- raise (Failure "TODO")
+ craise meta "TODO: error message"
in
AProjLoans (sv, (mv, child_proj) :: local_given_back)
in
- update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx
+ update_intersecting_aproj_loans meta proj_regions proj_ty sv subst ctx
(** Auxiliary function to end borrows. See {!give_back}.
@@ -484,12 +485,12 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t)
end abstraction when ending this abstraction. When doing this, we need
to convert the {!avalue} to a {!type:value} by introducing the proper symbolic values.
*)
-let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id)
+let give_back_avalue_to_same_abstraction (meta : Meta.meta) (_config : config) (bid : BorrowId.id)
(nv : typed_avalue) (nsv : typed_value) (ctx : eval_ctx) : eval_ctx =
(* We use a reference to check that we updated exactly one loan *)
let replaced : bool ref = ref false in
let set_replaced () =
- assert (not !replaced);
+ cassert (not !replaced) meta "Only one loan should have been updated";
replaced := true
in
let obj =
@@ -532,7 +533,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id)
("give_back_avalue_to_same_abstraction: improper type:\n\
- expected: " ^ ty_to_string ctx ty ^ "\n- received: "
^ ty_to_string ctx nv.ty);
- raise (Failure "Value given back doesn't have the proper type"));
+ craise meta "Value given back doesn't have the proper type");
(* This is the loan we are looking for: apply the projection to
* the value we give back and replaced this mutable loan with
* an ended loan *)
@@ -558,7 +559,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id)
* we don't register the fact that we inserted the value somewhere
* (i.e., we don't call {!set_replaced}) *)
(* Sanity check *)
- assert (nv.ty = ty);
+ cassert (nv.ty = ty) meta "TODO: error message";
ALoan
(AEndedIgnoredMutLoan
{ given_back = nv; child; given_back_meta = nsv }))
@@ -574,7 +575,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id)
(* Explore the environment *)
let ctx = obj#visit_eval_ctx None ctx in
(* Check we gave back to exactly one loan *)
- assert !replaced;
+ cassert !replaced meta "Only one loan should be given back";
(* Return *)
ctx
@@ -587,11 +588,11 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id)
we update.
TODO: this was not the case before, so some sanity checks are not useful anymore.
*)
-let give_back_shared _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
+let give_back_shared (meta : Meta.meta) _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
(* We use a reference to check that we updated exactly one loan *)
let replaced : bool ref = ref false in
let set_replaced () =
- assert (not !replaced);
+ cassert (not !replaced) meta "Only one loan should be updated";
replaced := true
in
let obj =
@@ -656,7 +657,7 @@ let give_back_shared _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
(* Explore the environment *)
let ctx = obj#visit_eval_ctx None ctx in
(* Check we gave back to exactly one loan *)
- assert !replaced;
+ cassert !replaced meta "Exactly one loan should be given back";
(* Return *)
ctx
@@ -665,12 +666,12 @@ let give_back_shared _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
to an environment by inserting a new borrow id in the set of borrows tracked
by a shared value, referenced by the [original_bid] argument.
*)
-let reborrow_shared (original_bid : BorrowId.id) (new_bid : BorrowId.id)
+let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) (new_bid : BorrowId.id)
(ctx : eval_ctx) : eval_ctx =
(* Keep track of changes *)
let r = ref false in
let set_ref () =
- assert (not !r);
+ cassert (not !r) meta "TODO: error message";
r := true
in
@@ -700,7 +701,7 @@ let reborrow_shared (original_bid : BorrowId.id) (new_bid : BorrowId.id)
let env = obj#visit_env () ctx.env in
(* Check that we reborrowed once *)
- assert !r;
+ cassert !r meta "Not reborrowed once";
{ ctx with env }
(** Convert an {!type:avalue} to a {!type:value}.
@@ -738,7 +739,7 @@ let convert_avalue_to_given_back_value (av : typed_avalue) : symbolic_value =
borrows. This kind of internal reshuffling. should be similar to ending
abstractions (it is tantamount to ending *sub*-abstractions).
*)
-let give_back (config : config) (l : BorrowId.id) (bc : g_borrow_content)
+let give_back (meta : Meta.meta) (config : config) (l : BorrowId.id) (bc : g_borrow_content)
(ctx : eval_ctx) : eval_ctx =
(* Debug *)
log#ldebug
@@ -757,24 +758,24 @@ let give_back (config : config) (l : BorrowId.id) (bc : g_borrow_content)
match bc with
| Concrete (VMutBorrow (l', tv)) ->
(* Sanity check *)
- assert (l' = l);
- assert (not (loans_in_value tv));
+ cassert (l' = l) meta "TODO: error message";
+ cassert (not (loans_in_value tv)) meta "TODO: error message";
(* Check that the corresponding loan is somewhere - purely a sanity check *)
- assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+ cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The corresponding loan should be somewhere";
(* Update the context *)
- give_back_value config l tv ctx
+ give_back_value meta config l tv ctx
| Concrete (VSharedBorrow l' | VReservedMutBorrow l') ->
(* Sanity check *)
- assert (l' = l);
+ cassert (l' = l) meta "TODO: error message";
(* Check that the borrow is somewhere - purely a sanity check *)
- assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+ cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The borrow should be somewhere";
(* Update the context *)
- give_back_shared config l ctx
+ give_back_shared meta config l ctx
| Abstract (AMutBorrow (l', av)) ->
(* Sanity check *)
- assert (l' = l);
+ cassert (l' = l) meta "TODO: error message";
(* Check that the corresponding loan is somewhere - purely a sanity check *)
- assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+ cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The corresponding loan should be somewhere";
(* Convert the avalue to a (fresh symbolic) value.
Rem.: we shouldn't do this here. We should do this in a function
@@ -782,27 +783,27 @@ let give_back (config : config) (l : BorrowId.id) (bc : g_borrow_content)
*)
let sv = convert_avalue_to_given_back_value av in
(* Update the context *)
- give_back_avalue_to_same_abstraction config l av
+ give_back_avalue_to_same_abstraction meta config l av
(mk_typed_value_from_symbolic_value sv)
ctx
| Abstract (ASharedBorrow l') ->
(* Sanity check *)
- assert (l' = l);
+ cassert (l' = l) meta "TODO: error message";
(* Check that the borrow is somewhere - purely a sanity check *)
- assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+ cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The borrow should be somewhere";
(* Update the context *)
- give_back_shared config l ctx
+ give_back_shared meta config l ctx
| Abstract (AProjSharedBorrow asb) ->
(* Sanity check *)
- assert (borrow_in_asb l asb);
+ cassert (borrow_in_asb l asb) meta "TODO: error message";
(* Update the context *)
- give_back_shared config l ctx
+ give_back_shared meta config l ctx
| Abstract
( AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _
| AEndedSharedBorrow ) ->
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
-let check_borrow_disappeared (fun_name : string) (l : BorrowId.id)
+let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowId.id)
(ctx0 : eval_ctx) : cm_fun =
let check_disappeared (ctx : eval_ctx) : unit =
let _ =
@@ -815,9 +816,9 @@ let check_borrow_disappeared (fun_name : string) (l : BorrowId.id)
^ ": borrow didn't disappear:\n- original context:\n"
^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n"
^ eval_ctx_to_string ctx));
- raise (Failure "Borrow not eliminated")
+ craise meta "Borrow not eliminated"
in
- match lookup_loan_opt ek_all l ctx with
+ match lookup_loan_opt meta ek_all l ctx with
| None -> () (* Ok *)
| Some _ ->
log#lerror
@@ -826,7 +827,7 @@ let check_borrow_disappeared (fun_name : string) (l : BorrowId.id)
^ ": loan didn't disappear:\n- original context:\n"
^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n"
^ eval_ctx_to_string ctx));
- raise (Failure "Loan not eliminated")
+ craise meta "Loan not eliminated"
in
unit_to_cm_fun check_disappeared
@@ -851,7 +852,7 @@ let check_borrow_disappeared (fun_name : string) (l : BorrowId.id)
perform anything smart and is trusted, and another function for the
book-keeping.
*)
-let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids)
+let rec end_borrow_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
(allowed_abs : AbstractionId.id option) (l : BorrowId.id) : cm_fun =
fun cf ctx ->
(* Check that we don't loop *)
@@ -867,10 +868,10 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids)
(* Utility function for the sanity checks: check that the borrow disappeared
* from the context *)
let ctx0 = ctx in
- let cf_check : cm_fun = check_borrow_disappeared "end borrow" l ctx0 in
+ let cf_check : cm_fun = check_borrow_disappeared meta "end borrow" l ctx0 in
(* Start by ending the borrow itself (we lookup it up and replace it with [Bottom] *)
let allow_inner_loans = false in
- match end_borrow_get_borrow allowed_abs allow_inner_loans l ctx with
+ match end_borrow_get_borrow meta allowed_abs allow_inner_loans l ctx with
(* Two cases:
- error: we found outer borrows (the borrow is inside a borrowed value) or
inner loans (the borrow contains loans)
@@ -899,29 +900,29 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids)
* inside another borrow *)
let allowed_abs' = None in
(* End the outer borrows *)
- let cc = end_borrows_aux config chain allowed_abs' bids in
+ let cc = end_borrows_aux meta config chain allowed_abs' bids in
(* Retry to end the borrow *)
- let cc = comp cc (end_borrow_aux config chain0 allowed_abs l) in
+ let cc = comp cc (end_borrow_aux meta config chain0 allowed_abs l) in
(* Check and apply *)
comp cc cf_check cf ctx
| OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) ->
let allowed_abs' = None in
(* End the outer borrow *)
- let cc = end_borrow_aux config chain allowed_abs' bid in
+ let cc = end_borrow_aux meta config chain allowed_abs' bid in
(* Retry to end the borrow *)
- let cc = comp cc (end_borrow_aux config chain0 allowed_abs l) in
+ let cc = comp cc (end_borrow_aux meta config chain0 allowed_abs l) in
(* Check and apply *)
comp cc cf_check cf ctx
| OuterAbs abs_id ->
(* The borrow is inside an abstraction: end the whole abstraction *)
- let cf_end_abs = end_abstraction_aux config chain abs_id in
+ let cf_end_abs = end_abstraction_aux meta config chain abs_id in
(* Compose with a sanity check *)
comp cf_end_abs cf_check cf ctx)
| Ok (ctx, None) ->
log#ldebug (lazy "End borrow: borrow not found");
(* It is possible that we can't find a borrow in symbolic mode (ending
* an abstraction may end several borrows at once *)
- assert (config.mode = SymbolicMode);
+ cassert (config.mode = SymbolicMode) meta "Borrow should be in symbolic mode";
(* Do a sanity check and continue *)
cf_check cf ctx
(* We found a borrow and replaced it with [Bottom]: give it back (i.e., update
@@ -930,10 +931,10 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids)
(* Sanity check: the borrowed value shouldn't contain loans *)
(match bc with
| Concrete (VMutBorrow (_, bv)) ->
- assert (Option.is_none (get_first_loan_in_value bv))
+ cassert (Option.is_none (get_first_loan_in_value bv)) meta "Borrowed value shouldn't contain loans"
| _ -> ());
(* Give back the value *)
- let ctx = give_back config l bc ctx in
+ let ctx = give_back meta config l bc ctx in
(* Do a sanity check and continue *)
let cc = cf_check in
(* Save a snapshot of the environment for the name generation *)
@@ -941,7 +942,7 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids)
(* Compose *)
cc cf ctx
-and end_borrows_aux (config : config) (chain : borrow_or_abs_ids)
+and end_borrows_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
(allowed_abs : AbstractionId.id option) (lset : BorrowId.Set.t) : cm_fun =
fun cf ->
(* This is not necessary, but we prefer to reorder the borrow ids,
@@ -949,10 +950,10 @@ and end_borrows_aux (config : config) (chain : borrow_or_abs_ids)
* a matter of taste, and may make debugging easier *)
let ids = BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in
List.fold_left
- (fun cf id -> end_borrow_aux config chain allowed_abs id cf)
+ (fun cf id -> end_borrow_aux meta config chain allowed_abs id cf)
cf ids
-and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
+and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
(abs_id : AbstractionId.id) : cm_fun =
fun cf ctx ->
(* Check that we don't loop *)
@@ -983,14 +984,14 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
(* Check that we can end the abstraction *)
if abs.can_end then ()
else
- raise
- (Failure
+ craise
+ meta
("Can't end abstraction "
^ AbstractionId.to_string abs.abs_id
- ^ " as it is set as non-endable"));
+ ^ " as it is set as non-endable");
(* End the parent abstractions first *)
- let cc = end_abstractions_aux config chain abs.parents in
+ let cc = end_abstractions_aux meta config chain abs.parents in
let cc =
comp_unit cc (fun ctx ->
log#ldebug
@@ -1002,7 +1003,7 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
in
(* End the loans inside the abstraction *)
- let cc = comp cc (end_abstraction_loans config chain abs_id) in
+ let cc = comp cc (end_abstraction_loans meta config chain abs_id) in
let cc =
comp_unit cc (fun ctx ->
log#ldebug
@@ -1013,7 +1014,7 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
in
(* End the abstraction itself by redistributing the borrows it contains *)
- let cc = comp cc (end_abstraction_borrows config chain abs_id) in
+ let cc = comp cc (end_abstraction_borrows meta config chain abs_id) in
(* End the regions owned by the abstraction - note that we don't need to
* relookup the abstraction: the set of regions in an abstraction never
@@ -1043,7 +1044,7 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
in
(* Sanity check: ending an abstraction must preserve the invariants *)
- let cc = comp cc Invariants.cf_check_invariants in
+ let cc = comp cc (Invariants.cf_check_invariants meta) in
(* Save a snapshot of the environment for the name generation *)
let cc = comp cc SynthesizeSymbolic.cf_save_snapshot in
@@ -1051,7 +1052,7 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
(* Apply the continuation *)
cc cf ctx
-and end_abstractions_aux (config : config) (chain : borrow_or_abs_ids)
+and end_abstractions_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
(abs_ids : AbstractionId.Set.t) : cm_fun =
fun cf ->
(* This is not necessary, but we prefer to reorder the abstraction ids,
@@ -1059,10 +1060,10 @@ and end_abstractions_aux (config : config) (chain : borrow_or_abs_ids)
* a matter of taste, and may make debugging easier *)
let abs_ids = AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in
List.fold_left
- (fun cf id -> end_abstraction_aux config chain id cf)
+ (fun cf id -> end_abstraction_aux meta config chain id cf)
cf abs_ids
-and end_abstraction_loans (config : config) (chain : borrow_or_abs_ids)
+and end_abstraction_loans (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
(abs_id : AbstractionId.id) : cm_fun =
fun cf ctx ->
(* Lookup the abstraction *)
@@ -1071,7 +1072,7 @@ and end_abstraction_loans (config : config) (chain : borrow_or_abs_ids)
*
* We ignore the "ignored mut/shared loans": as we should have already ended
* the parent abstractions, they necessarily come from children. *)
- let opt_loan = get_first_non_ignored_aloan_in_abstraction abs in
+ let opt_loan = get_first_non_ignored_aloan_in_abstraction meta abs in
match opt_loan with
| None ->
(* No loans: nothing to update *)
@@ -1080,23 +1081,23 @@ and end_abstraction_loans (config : config) (chain : borrow_or_abs_ids)
(* There are loans: end the corresponding borrows, then recheck *)
let cc : cm_fun =
match bids with
- | Borrow bid -> end_borrow_aux config chain None bid
- | Borrows bids -> end_borrows_aux config chain None bids
+ | Borrow bid -> end_borrow_aux meta config chain None bid
+ | Borrows bids -> end_borrows_aux meta config chain None bids
in
(* Reexplore, looking for loans *)
- let cc = comp cc (end_abstraction_loans config chain abs_id) in
+ let cc = comp cc (end_abstraction_loans meta config chain abs_id) in
(* Continue *)
cc cf ctx
| Some (SymbolicValue sv) ->
(* There is a proj_loans over a symbolic value: end the proj_borrows
* which intersect this proj_loans, then end the proj_loans itself *)
- let cc = end_proj_loans_symbolic config chain abs_id abs.regions sv in
+ let cc = end_proj_loans_symbolic meta config chain abs_id abs.regions sv in
(* Reexplore, looking for loans *)
- let cc = comp cc (end_abstraction_loans config chain abs_id) in
+ let cc = comp cc (end_abstraction_loans meta config chain abs_id) in
(* Continue *)
cc cf ctx
-and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
+and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
(abs_id : AbstractionId.id) : cm_fun =
fun cf ctx ->
log#ldebug
@@ -1147,7 +1148,7 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
method! visit_aproj env sproj =
(match sproj with
- | AProjLoans _ -> raise (Failure "Unexpected")
+ | AProjLoans _ -> craise meta "Unexpected"
| AProjBorrows (sv, proj_ty) -> raise (FoundAProjBorrows (sv, proj_ty))
| AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
super#visit_aproj env sproj
@@ -1156,7 +1157,7 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
method! visit_borrow_content _ bc =
match bc with
| VSharedBorrow _ | VMutBorrow (_, _) -> raise (FoundBorrowContent bc)
- | VReservedMutBorrow _ -> raise (Failure "Unreachable")
+ | VReservedMutBorrow _ -> craise meta "Unreachable"
end
in
(* Lookup the abstraction *)
@@ -1181,16 +1182,16 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
(* Replace the mut borrow to register the fact that we ended
* it and store with it the freshly generated given back value *)
let ended_borrow = ABorrow (AEndedMutBorrow (sv, av)) in
- let ctx = update_aborrow ek_all bid ended_borrow ctx in
+ let ctx = update_aborrow meta ek_all bid ended_borrow ctx in
(* Give the value back *)
let sv = mk_typed_value_from_symbolic_value sv in
- give_back_value config bid sv ctx
+ give_back_value meta config bid sv ctx
| ASharedBorrow bid ->
(* Replace the shared borrow to account for the fact it ended *)
let ended_borrow = ABorrow AEndedSharedBorrow in
- let ctx = update_aborrow ek_all bid ended_borrow ctx in
+ let ctx = update_aborrow meta ek_all bid ended_borrow ctx in
(* Give back *)
- give_back_shared config bid ctx
+ give_back_shared meta config bid ctx
| AProjSharedBorrow asb ->
(* Retrieve the borrow ids *)
let bids =
@@ -1205,21 +1206,21 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
* can use to identify the whole set *)
let repr_bid = List.hd bids in
(* Replace the shared borrow with Bottom *)
- let ctx = update_aborrow ek_all repr_bid ABottom ctx in
+ let ctx = update_aborrow meta ek_all repr_bid ABottom ctx in
(* Give back the shared borrows *)
let ctx =
List.fold_left
- (fun ctx bid -> give_back_shared config bid ctx)
+ (fun ctx bid -> give_back_shared meta config bid ctx)
ctx bids
in
(* Continue *)
ctx
| AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _
| AEndedSharedBorrow ->
- raise (Failure "Unexpected")
+ craise meta "Unexpected"
in
(* Reexplore *)
- end_abstraction_borrows config chain abs_id cf ctx
+ end_abstraction_borrows meta config chain abs_id cf ctx
(* There are symbolic borrows: end them, then reexplore *)
| FoundAProjBorrows (sv, proj_ty) ->
log#ldebug
@@ -1230,13 +1231,13 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
let nsv = mk_fresh_symbolic_value proj_ty in
(* Replace the proj_borrows - there should be exactly one *)
let ended_borrow = AEndedProjBorrows nsv in
- let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in
+ let ctx = update_aproj_borrows meta abs.abs_id sv ended_borrow ctx in
(* Give back the symbolic value *)
let ctx =
- give_back_symbolic_value config abs.regions proj_ty sv nsv ctx
+ give_back_symbolic_value meta config abs.regions proj_ty sv nsv ctx
in
(* Reexplore *)
- end_abstraction_borrows config chain abs_id cf ctx
+ end_abstraction_borrows meta config chain abs_id cf ctx
(* There are concrete (i.e., not symbolic) borrows in shared values: end them, then reexplore *)
| FoundBorrowContent bc ->
log#ldebug
@@ -1249,27 +1250,27 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
(* Replace the shared borrow with bottom *)
let allow_inner_loans = false in
match
- end_borrow_get_borrow (Some abs_id) allow_inner_loans bid ctx
+ end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx
with
- | Error _ -> raise (Failure "Unreachable")
+ | Error _ -> craise meta "Unreachable"
| Ok (ctx, _) ->
(* Give back *)
- give_back_shared config bid ctx)
+ give_back_shared meta config bid ctx)
| VMutBorrow (bid, v) -> (
(* Replace the mut borrow with bottom *)
let allow_inner_loans = false in
match
- end_borrow_get_borrow (Some abs_id) allow_inner_loans bid ctx
+ end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx
with
- | Error _ -> raise (Failure "Unreachable")
+ | Error _ -> craise meta "Unreachable"
| Ok (ctx, _) ->
(* Give the value back - note that the mut borrow was below a
* shared borrow: the value is thus unchanged *)
- give_back_value config bid v ctx)
- | VReservedMutBorrow _ -> raise (Failure "Unreachable")
+ give_back_value meta config bid v ctx)
+ | VReservedMutBorrow _ -> craise meta "Unreachable"
in
(* Reexplore *)
- end_abstraction_borrows config chain abs_id cf ctx
+ end_abstraction_borrows meta config chain abs_id cf ctx
(** Remove an abstraction from the context, as well as all its references *)
and end_abstraction_remove_from_context (_config : config)
@@ -1296,12 +1297,12 @@ and end_abstraction_remove_from_context (_config : config)
intersecting proj_borrows, either in the concrete context or in an
abstraction
*)
-and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids)
+and end_proj_loans_symbolic (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
(abs_id : AbstractionId.id) (regions : RegionId.Set.t) (sv : symbolic_value)
: cm_fun =
fun cf ctx ->
(* Small helpers for sanity checks *)
- let check ctx = no_aproj_over_symbolic_in_context sv ctx in
+ let check ctx = no_aproj_over_symbolic_in_context meta sv ctx in
let cf_check (cf : m_fun) : m_fun =
fun ctx ->
check ctx;
@@ -1309,13 +1310,13 @@ and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids)
in
(* Find the first proj_borrows which intersects the proj_loans *)
let explore_shared = true in
- match lookup_intersecting_aproj_borrows_opt explore_shared regions sv ctx with
+ match lookup_intersecting_aproj_borrows_opt meta explore_shared regions sv ctx with
| None ->
(* We couldn't find any in the context: it means that the symbolic value
* is in the concrete environment (or that we dropped it, in which case
* it is completely absent). We thus simply need to replace the loans
* projector with an ended projector. *)
- let ctx = update_aproj_loans_to_ended abs_id sv ctx in
+ let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in
(* Sanity check *)
check ctx;
(* Continue *)
@@ -1359,15 +1360,15 @@ and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids)
AbstractionId.Set.empty abs_ids
in
(* End the abstractions and continue *)
- end_abstractions_aux config chain abs_ids cf ctx
+ end_abstractions_aux meta config chain abs_ids cf ctx
in
(* End the internal borrows projectors and the loans projector *)
let cf_end_internal : cm_fun =
fun cf ctx ->
(* All the proj_borrows are owned: simply erase them *)
- let ctx = remove_intersecting_aproj_borrows_shared regions sv ctx in
+ let ctx = remove_intersecting_aproj_borrows_shared meta regions sv ctx in
(* End the loan itself *)
- let ctx = update_aproj_loans_to_ended abs_id sv ctx in
+ let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in
(* Sanity check *)
check ctx;
(* Continue *)
@@ -1399,48 +1400,48 @@ and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids)
*)
(* End the projector of borrows - TODO: not completely sure what to
* replace it with... Maybe we should introduce an ABottomProj? *)
- let ctx = update_aproj_borrows abs_id sv AIgnoredProjBorrows ctx in
+ let ctx = update_aproj_borrows meta abs_id sv AIgnoredProjBorrows ctx in
(* Sanity check: no other occurrence of an intersecting projector of borrows *)
- assert (
+ cassert (
Option.is_none
- (lookup_intersecting_aproj_borrows_opt explore_shared regions sv ctx));
+ (lookup_intersecting_aproj_borrows_opt meta explore_shared regions sv ctx)) meta "no other occurrence of an intersecting projector of borrows";
(* End the projector of loans *)
- let ctx = update_aproj_loans_to_ended abs_id sv ctx in
+ let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in
(* Sanity check *)
check ctx;
(* Continue *)
cf ctx)
else
(* The borrows proj comes from a different abstraction: end it. *)
- let cc = end_abstraction_aux config chain abs_id' in
+ let cc = end_abstraction_aux meta config chain abs_id' in
(* Retry ending the projector of loans *)
let cc =
- comp cc (end_proj_loans_symbolic config chain abs_id regions sv)
+ comp cc (end_proj_loans_symbolic meta config chain abs_id regions sv)
in
(* Sanity check *)
let cc = comp cc cf_check in
(* Continue *)
cc cf ctx
-let end_borrow config : BorrowId.id -> cm_fun = end_borrow_aux config [] None
+let end_borrow (meta : Meta.meta ) config : BorrowId.id -> cm_fun = end_borrow_aux meta config [] None
-let end_borrows config : BorrowId.Set.t -> cm_fun =
- end_borrows_aux config [] None
+let end_borrows (meta : Meta.meta ) config : BorrowId.Set.t -> cm_fun =
+ end_borrows_aux meta config [] None
-let end_abstraction config = end_abstraction_aux config []
-let end_abstractions config = end_abstractions_aux config []
+let end_abstraction meta config = end_abstraction_aux meta config []
+let end_abstractions meta config = end_abstractions_aux meta config []
-let end_borrow_no_synth config id ctx =
- get_cf_ctx_no_synth (end_borrow config id) ctx
+let end_borrow_no_synth meta config id ctx =
+ get_cf_ctx_no_synth (end_borrow meta config id) ctx
-let end_borrows_no_synth config ids ctx =
- get_cf_ctx_no_synth (end_borrows config ids) ctx
+let end_borrows_no_synth meta config ids ctx =
+ get_cf_ctx_no_synth (end_borrows meta config ids) ctx
-let end_abstraction_no_synth config id ctx =
- get_cf_ctx_no_synth (end_abstraction config id) ctx
+let end_abstraction_no_synth meta config id ctx =
+ get_cf_ctx_no_synth (end_abstraction meta config id) ctx
-let end_abstractions_no_synth config ids ctx =
- get_cf_ctx_no_synth (end_abstractions config ids) ctx
+let end_abstractions_no_synth meta config ids ctx =
+ get_cf_ctx_no_synth (end_abstractions meta config ids) ctx
(** Helper function: see {!activate_reserved_mut_borrow}.
@@ -1458,7 +1459,7 @@ let end_abstractions_no_synth config ids ctx =
The loan to update mustn't be a borrowed value.
*)
-let promote_shared_loan_to_mut_loan (l : BorrowId.id)
+let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
(cf : typed_value -> m_fun) : m_fun =
fun ctx ->
(* Debug *)
@@ -1473,38 +1474,38 @@ let promote_shared_loan_to_mut_loan (l : BorrowId.id)
let ek =
{ enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
in
- match lookup_loan ek l ctx with
+ match lookup_loan meta ek l ctx with
| _, Concrete (VMutLoan _) ->
- raise (Failure "Expected a shared loan, found a mut loan")
+ craise meta "Expected a shared loan, found a mut loan"
| _, Concrete (VSharedLoan (bids, sv)) ->
(* Check that there is only one borrow id (l) and update the loan *)
- assert (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1);
+ cassert (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1) meta "There should only be one borrow id";
(* We need to check that there aren't any loans in the value:
we should have gotten rid of those already, but it is better
to do a sanity check. *)
- assert (not (loans_in_value sv));
+ cassert (not (loans_in_value sv)) meta "There shouldn't be any loans in the value";
(* Check there isn't {!Bottom} (this is actually an invariant *)
- assert (not (bottom_in_value ctx.ended_regions sv));
+ cassert (not (bottom_in_value ctx.ended_regions sv)) meta "There shouldn't be a !Bottom";
(* Check there aren't reserved borrows *)
- assert (not (reserved_in_value sv));
+ cassert (not (reserved_in_value sv)) meta "There shouldn't have reserved borrows";
(* Update the loan content *)
- let ctx = update_loan ek l (VMutLoan l) ctx in
+ let ctx = update_loan meta ek l (VMutLoan l) ctx in
(* Continue *)
cf sv ctx
| _, Abstract _ ->
(* I don't think it is possible to have two-phase borrows involving borrows
* returned by abstractions. I'm not sure how we could handle that anyway. *)
- raise
- (Failure
+ craise
+ meta
"Can't promote a shared loan to a mutable loan if the loan is \
- inside an abstraction")
+ inside an abstraction"
(** Helper function: see {!activate_reserved_mut_borrow}.
This function updates a shared borrow to a mutable borrow (and that is
all: it doesn't touch the corresponding loan).
*)
-let replace_reserved_borrow_with_mut_borrow (l : BorrowId.id) (cf : m_fun)
+let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id) (cf : m_fun)
(borrowed_value : typed_value) : m_fun =
fun ctx ->
(* Lookup the reserved borrow - note that we don't go inside borrows/loans:
@@ -1514,32 +1515,32 @@ let replace_reserved_borrow_with_mut_borrow (l : BorrowId.id) (cf : m_fun)
{ enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false }
in
let ctx =
- match lookup_borrow ek l ctx with
+ match lookup_borrow meta ek l ctx with
| Concrete (VSharedBorrow _ | VMutBorrow (_, _)) ->
- raise (Failure "Expected a reserved mutable borrow")
+ craise meta "Expected a reserved mutable borrow"
| Concrete (VReservedMutBorrow _) ->
(* Update it *)
- update_borrow ek l (VMutBorrow (l, borrowed_value)) ctx
+ update_borrow meta ek l (VMutBorrow (l, borrowed_value)) ctx
| Abstract _ ->
(* This can't happen for sure *)
- raise
- (Failure
+ craise
+ meta
"Can't promote a shared borrow to a mutable borrow if the borrow \
- is inside an abstraction")
+ is inside an abstraction"
in
(* Continue *)
cf ctx
(** Promote a reserved mut borrow to a mut borrow. *)
-let rec promote_reserved_mut_borrow (config : config) (l : BorrowId.id) : cm_fun
+let rec promote_reserved_mut_borrow (meta : Meta.meta) (config : config) (l : BorrowId.id) : cm_fun
=
fun cf ctx ->
(* Lookup the value *)
let ek =
{ enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
in
- match lookup_loan ek l ctx with
- | _, Concrete (VMutLoan _) -> raise (Failure "Unreachable")
+ match lookup_loan meta ek l ctx with
+ | _, Concrete (VMutLoan _) -> craise meta "Unreachable"
| _, Concrete (VSharedLoan (bids, sv)) -> (
(* If there are loans inside the value, end them. Note that there can't be
reserved borrows inside the value.
@@ -1549,11 +1550,11 @@ let rec promote_reserved_mut_borrow (config : config) (l : BorrowId.id) : cm_fun
(* End the loans *)
let cc =
match lc with
- | VSharedLoan (bids, _) -> end_borrows config bids
- | VMutLoan bid -> end_borrow config bid
+ | VSharedLoan (bids, _) -> end_borrows meta config bids
+ | VMutLoan bid -> end_borrow meta config bid
in
(* Recursive call *)
- let cc = comp cc (promote_reserved_mut_borrow config l) in
+ let cc = comp cc (promote_reserved_mut_borrow meta config l) in
(* Continue *)
cc cf ctx
| None ->
@@ -1563,36 +1564,36 @@ let rec promote_reserved_mut_borrow (config : config) (l : BorrowId.id) : cm_fun
(lazy
("activate_reserved_mut_borrow: resulting value:\n"
^ typed_value_to_string ctx sv));
- assert (not (loans_in_value sv));
- assert (not (bottom_in_value ctx.ended_regions sv));
- assert (not (reserved_in_value sv));
+ cassert (not (loans_in_value sv)) meta "TODO: error message";
+ cassert (not (bottom_in_value ctx.ended_regions sv)) meta "TODO: error message";
+ cassert (not (reserved_in_value sv)) meta "TODO: error message";
(* End the borrows which borrow from the value, at the exception of
the borrow we want to promote *)
let bids = BorrowId.Set.remove l bids in
- let cc = end_borrows config bids in
+ let cc = end_borrows meta config bids in
(* Promote the loan - TODO: this will fail if the value contains
* any loans. In practice, it shouldn't, but we could also
* look for loans inside the value and end them before promoting
* the borrow. *)
- let cc = comp cc (promote_shared_loan_to_mut_loan l) in
+ let cc = comp cc (promote_shared_loan_to_mut_loan meta l) in
(* Promote the borrow - the value should have been checked by
{!promote_shared_loan_to_mut_loan}
*)
let cc =
comp cc (fun cf borrowed_value ->
- replace_reserved_borrow_with_mut_borrow l cf borrowed_value)
+ replace_reserved_borrow_with_mut_borrow meta l cf borrowed_value)
in
(* Continue *)
cc cf ctx)
| _, Abstract _ ->
(* I don't think it is possible to have two-phase borrows involving borrows
* returned by abstractions. I'm not sure how we could handle that anyway. *)
- raise
- (Failure
+ craise
+ meta
"Can't activate a reserved mutable borrow referencing a loan inside\n\
- \ an abstraction")
+ \ an abstraction"
-let destructure_abs (abs_kind : abs_kind) (can_end : bool)
+let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
(destructure_shared_values : bool) (ctx : eval_ctx) (abs0 : abs) : abs =
(* Accumulator to store the destructured values *)
let avalues = ref [] in
@@ -1605,7 +1606,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
ignore the children altogether. Instead, we explore them and make sure
we don't register values while doing so.
*)
- let push_fail _ = raise (Failure "Unreachable") in
+ let push_fail _ = craise meta "Unreachable" in
(* Function to explore an avalue and destructure it *)
let rec list_avalues (allow_borrows : bool) (push : typed_avalue -> unit)
(av : typed_avalue) : unit =
@@ -1620,7 +1621,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
match lc with
| ASharedLoan (bids, sv, child_av) ->
(* We don't support nested borrows for now *)
- assert (not (value_has_borrows ctx sv.value));
+ cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows are not supported yet";
(* Destructure the shared value *)
let avl, sv =
if destructure_shared_values then list_values sv else ([], sv)
@@ -1647,8 +1648,8 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
push { value; ty }
| AIgnoredMutLoan (opt_bid, child_av) ->
(* We don't support nested borrows for now *)
- assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
- assert (opt_bid = None);
+ cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
+ cassert (opt_bid = None) meta "TODO: error message";
(* Simply explore the child *)
list_avalues false push_fail child_av
| AEndedMutLoan
@@ -1658,12 +1659,12 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
{ child = child_av; given_back = _; given_back_meta = _ }
| AIgnoredSharedLoan child_av ->
(* We don't support nested borrows for now *)
- assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
+ cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
(* Simply explore the child *)
list_avalues false push_fail child_av)
| ABorrow bc -> (
(* Sanity check - rem.: may be redundant with [push_fail] *)
- assert allow_borrows;
+ cassert allow_borrows meta "TODO: error message";
(* Explore the borrow content *)
match bc with
| AMutBorrow (bid, child_av) ->
@@ -1678,19 +1679,19 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
push av
| AIgnoredMutBorrow (opt_bid, child_av) ->
(* We don't support nested borrows for now *)
- assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
- assert (opt_bid = None);
+ cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
+ cassert (opt_bid = None) meta "TODO: error message";
(* Just explore the child *)
list_avalues false push_fail child_av
| AEndedIgnoredMutBorrow
{ child = child_av; given_back = _; given_back_meta = _ } ->
(* We don't support nested borrows for now *)
- assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
+ cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
(* Just explore the child *)
list_avalues false push_fail child_av
| AProjSharedBorrow asb ->
(* We don't support nested borrows *)
- assert (asb = []);
+ cassert (asb = []) meta "Nested borrows are not supported yet";
(* Nothing specific to do *)
()
| AEndedMutBorrow _ | AEndedSharedBorrow ->
@@ -1698,11 +1699,11 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
be in the context anymore (if we end *one* borrow in an abstraction,
we have to end them all and remove the abstraction from the context)
*)
- raise (Failure "Unreachable"))
+ craise meta "Unreachable")
| ASymbolic _ ->
(* For now, we fore all symbolic values containing borrows to be eagerly
expanded *)
- assert (not (ty_has_borrows ctx.type_ctx.type_infos ty))
+ cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta "TODO: error message"
and list_values (v : typed_value) : typed_avalue list * typed_value =
let ty = v.ty in
match v.value with
@@ -1714,19 +1715,19 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
let avl = List.concat avll in
let adt = { adt with field_values } in
(avl, { v with value = VAdt adt })
- | VBottom -> raise (Failure "Unreachable")
+ | VBottom -> craise meta "Unreachable"
| VBorrow _ ->
(* We don't support nested borrows for now *)
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
| VLoan lc -> (
match lc with
| VSharedLoan (bids, sv) ->
let avl, sv = list_values sv in
if destructure_shared_values then (
(* Rem.: the shared value can't contain loans nor borrows *)
- assert (ty_no_regions ty);
+ cassert (ty_no_regions ty) meta "The shared value can't contain loans nor borrows";
let av : typed_avalue =
- assert (not (value_has_loans_or_borrows ctx sv.value));
+ cassert (not (value_has_loans_or_borrows ctx sv.value)) meta "The shared value can't contain loans nor borrows";
(* We introduce fresh ids for the symbolic values *)
let mk_value_with_fresh_sids (v : typed_value) : typed_value =
let visitor =
@@ -1747,11 +1748,11 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
let avl = List.append [ av ] avl in
(avl, sv))
else (avl, { v with value = VLoan (VSharedLoan (bids, sv)) })
- | VMutLoan _ -> raise (Failure "Unreachable"))
+ | VMutLoan _ -> craise meta "Unreachable")
| VSymbolic _ ->
(* For now, we fore all symbolic values containing borrows to be eagerly
expanded *)
- assert (not (ty_has_borrows ctx.type_ctx.type_infos ty));
+ cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta "TODO: error message";
([], v)
in
@@ -1761,14 +1762,14 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
(* Update *)
{ abs0 with avalues; kind = abs_kind; can_end }
-let abs_is_destructured (destructure_shared_values : bool) (ctx : eval_ctx)
+let abs_is_destructured (meta : Meta.meta) (destructure_shared_values : bool) (ctx : eval_ctx)
(abs : abs) : bool =
let abs' =
- destructure_abs abs.kind abs.can_end destructure_shared_values ctx abs
+ destructure_abs meta abs.kind abs.can_end destructure_shared_values ctx abs
in
abs = abs'
-let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool)
+let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
(destructure_shared_values : bool) (ctx : eval_ctx) (v : typed_value) :
abs list =
(* Convert the value to a list of avalues *)
@@ -1851,20 +1852,20 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool)
(avl, { v with value = VAdt adt })
| VBorrow bc -> (
let _, ref_ty, kind = ty_as_ref ty in
- assert (ty_no_regions ref_ty);
+ cassert (ty_no_regions ref_ty) meta "TODO: error message";
(* Sanity check *)
- assert allow_borrows;
+ cassert allow_borrows meta "TODO: error message";
(* Convert the borrow content *)
match bc with
| VSharedBorrow bid ->
- assert (ty_no_regions ref_ty);
+ cassert (ty_no_regions ref_ty) meta "TODO: error message";
let ty = TRef (RFVar r_id, ref_ty, kind) in
let value = ABorrow (ASharedBorrow bid) in
([ { value; ty } ], v)
| VMutBorrow (bid, bv) ->
let r_id = if group then r_id else fresh_region_id () in
(* We don't support nested borrows for now *)
- assert (not (value_has_borrows ctx bv.value));
+ cassert (not (value_has_borrows ctx bv.value)) meta "Nested borrows are not supported yet";
(* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
let ty = TRef (RFVar r_id, ref_ty, kind) in
let ignored = mk_aignored ref_ty in
@@ -1877,16 +1878,16 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool)
(av :: avl, value)
| VReservedMutBorrow _ ->
(* This borrow should have been activated *)
- raise (Failure "Unexpected"))
+ craise meta "Unexpected")
| VLoan lc -> (
match lc with
| VSharedLoan (bids, sv) ->
let r_id = if group then r_id else fresh_region_id () in
(* We don't support nested borrows for now *)
- assert (not (value_has_borrows ctx sv.value));
+ cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows are not supported yet";
(* Push the avalue - note that we use [AIgnore] for the inner avalue *)
(* For avalues, a loan has the borrow type *)
- assert (ty_no_regions ty);
+ cassert (ty_no_regions ty) meta "TODO: error message";
let ty = mk_ref_ty (RFVar r_id) ty RShared in
let ignored = mk_aignored ty in
(* Rem.: the shared value might contain loans *)
@@ -1904,7 +1905,7 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool)
| VMutLoan bid ->
(* Push the avalue - note that we use [AIgnore] for the inner avalue *)
(* For avalues, a loan has the borrow type *)
- assert (ty_no_regions ty);
+ cassert (ty_no_regions ty) meta "TODO: error message";
let ty = mk_ref_ty (RFVar r_id) ty RMut in
let ignored = mk_aignored ty in
let av = ALoan (AMutLoan (bid, ignored)) in
@@ -1913,7 +1914,7 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool)
| VSymbolic _ ->
(* For now, we force all the symbolic values containing borrows to
be eagerly expanded, and we don't support nested borrows *)
- assert (not (value_has_borrows ctx v.value));
+ cassert (not (value_has_borrows ctx v.value)) meta "TODO: error message";
(* Return nothing *)
([], v)
in
@@ -1954,7 +1955,7 @@ type merge_abstraction_info = {
- all the borrows are destructured (for instance, shared loans can't
contain shared loans).
*)
-let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) :
+let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) (abs : abs) :
merge_abstraction_info =
let loans : loan_id_set ref = ref BorrowId.Set.empty in
let borrows : borrow_id_set ref = ref BorrowId.Set.empty in
@@ -1967,26 +1968,26 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) :
in
let push_loans ids (lc : g_loan_content_with_ty) : unit =
- assert (BorrowId.Set.disjoint !loans ids);
+ cassert (BorrowId.Set.disjoint !loans ids) meta "TODO: error message";
loans := BorrowId.Set.union !loans ids;
BorrowId.Set.iter
(fun id ->
- assert (not (BorrowId.Map.mem id !loan_to_content));
+ cassert (not (BorrowId.Map.mem id !loan_to_content)) meta "TODO: error message";
loan_to_content := BorrowId.Map.add id lc !loan_to_content;
borrows_loans := LoanId id :: !borrows_loans)
ids
in
let push_loan id (lc : g_loan_content_with_ty) : unit =
- assert (not (BorrowId.Set.mem id !loans));
+ cassert (not (BorrowId.Set.mem id !loans)) meta "TODO: error message";
loans := BorrowId.Set.add id !loans;
- assert (not (BorrowId.Map.mem id !loan_to_content));
+ cassert (not (BorrowId.Map.mem id !loan_to_content)) meta "TODO: error message";
loan_to_content := BorrowId.Map.add id lc !loan_to_content;
borrows_loans := LoanId id :: !borrows_loans
in
let push_borrow id (bc : g_borrow_content_with_ty) : unit =
- assert (not (BorrowId.Set.mem id !borrows));
+ cassert (not (BorrowId.Set.mem id !borrows)) meta "TODO: error message";
borrows := BorrowId.Set.add id !borrows;
- assert (not (BorrowId.Map.mem id !borrow_to_content));
+ cassert (not (BorrowId.Map.mem id !borrow_to_content)) meta "TODO: error message";
borrow_to_content := BorrowId.Map.add id bc !borrow_to_content;
borrows_loans := BorrowId id :: !borrows_loans
in
@@ -2009,23 +2010,23 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) :
let ty =
match Option.get env with
| Concrete ty -> ty
- | Abstract _ -> raise (Failure "Unreachable")
+ | Abstract _ -> craise meta "Unreachable"
in
(match lc with
| VSharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc))
- | VMutLoan _ -> raise (Failure "Unreachable"));
+ | VMutLoan _ -> craise meta "Unreachable");
(* Continue *)
super#visit_loan_content env lc
method! visit_borrow_content _ _ =
(* Can happen if we explore shared values which contain borrows -
i.e., if we have nested borrows (we forbid this for now) *)
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
method! visit_aloan_content env lc =
let ty =
match Option.get env with
- | Concrete _ -> raise (Failure "Unreachable")
+ | Concrete _ -> craise meta "Unreachable"
| Abstract ty -> ty
in
(* Register the loans *)
@@ -2035,14 +2036,14 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) :
| AEndedMutLoan _ | AEndedSharedLoan _ | AIgnoredMutLoan _
| AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ ->
(* The abstraction has been destructured, so those shouldn't appear *)
- raise (Failure "Unreachable"));
+ craise meta "Unreachable");
(* Continue *)
super#visit_aloan_content env lc
method! visit_aborrow_content env bc =
let ty =
match Option.get env with
- | Concrete _ -> raise (Failure "Unreachable")
+ | Concrete _ -> craise meta "Unreachable"
| Abstract ty -> ty
in
(* Explore the borrow content *)
@@ -2056,18 +2057,18 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) :
| AsbProjReborrows _ ->
(* Can only happen if the symbolic value (potentially) contains
borrows - i.e., we have nested borrows *)
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
in
List.iter register asb
| AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedMutBorrow _
| AEndedSharedBorrow ->
(* The abstraction has been destructured, so those shouldn't appear *)
- raise (Failure "Unreachable"));
+ craise meta "Unreachable");
super#visit_aborrow_content env bc
method! visit_symbolic_value _ sv =
(* Sanity check: no borrows *)
- assert (not (symbolic_value_has_borrows ctx sv))
+ cassert (not (symbolic_value_has_borrows ctx sv)) meta "TODO: error message"
end
in
@@ -2134,7 +2135,7 @@ type merge_duplicates_funcs = {
Merge two abstractions into one, without updating the context.
*)
-let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
+let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
(merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx) (abs0 : abs)
(abs1 : abs) : abs =
log#ldebug
@@ -2145,8 +2146,8 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
(* Check that the abstractions are destructured *)
if !Config.sanity_checks then (
let destructure_shared_values = true in
- assert (abs_is_destructured destructure_shared_values ctx abs0);
- assert (abs_is_destructured destructure_shared_values ctx abs1));
+ cassert (abs_is_destructured meta destructure_shared_values ctx abs0) meta "Abstractions should be destructured";
+ cassert (abs_is_destructured meta destructure_shared_values ctx abs1) meta "Abstractions should be destructured");
(* Compute the relevant information *)
let {
@@ -2156,7 +2157,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
loan_to_content = loan_to_content0;
borrow_to_content = borrow_to_content0;
} =
- compute_merge_abstraction_info ctx abs0
+ compute_merge_abstraction_info meta ctx abs0
in
let {
@@ -2166,14 +2167,14 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
loan_to_content = loan_to_content1;
borrow_to_content = borrow_to_content1;
} =
- compute_merge_abstraction_info ctx abs1
+ compute_merge_abstraction_info meta ctx abs1
in
(* Sanity check: there is no loan/borrows which appears in both abstractions,
unless we allow to merge duplicates *)
if merge_funs = None then (
- assert (BorrowId.Set.disjoint borrows0 borrows1);
- assert (BorrowId.Set.disjoint loans0 loans1));
+ cassert (BorrowId.Set.disjoint borrows0 borrows1) meta "TODO: error message";
+ cassert (BorrowId.Set.disjoint loans0 loans1)) meta "TODO: error message";
(* Merge.
There are several cases:
@@ -2214,7 +2215,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
in
let filter_bids (bids : BorrowId.Set.t) : BorrowId.Set.t =
let bids = BorrowId.Set.diff bids intersect in
- assert (not (BorrowId.Set.is_empty bids));
+ cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message";
bids
in
let filter_bid (bid : BorrowId.id) : BorrowId.id option =
@@ -2242,11 +2243,11 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
(Option.get merge_funs).merge_ashared_borrows id ty0 ty1
| AProjSharedBorrow _, AProjSharedBorrow _ ->
(* Unreachable because requires nested borrows *)
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
| _ ->
(* Unreachable because those cases are ignored (ended/ignored borrows)
or inconsistent *)
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
in
let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty)
@@ -2254,12 +2255,12 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
match (bc0, bc1) with
| Concrete _, Concrete _ ->
(* This can happen only in case of nested borrows *)
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
| Abstract (ty0, bc0), Abstract (ty1, bc1) ->
merge_aborrow_contents ty0 bc0 ty1 bc1
| Concrete _, Abstract _ | Abstract _, Concrete _ ->
(* TODO: is it really unreachable? *)
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
in
let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty)
@@ -2277,7 +2278,7 @@ let merge_into_abstraction_aux (abs_kind : 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 (BorrowId.Set.equal ids0 ids1);
+ cassert (BorrowId.Set.equal ids0 ids1) meta "Ids are not the same - Case ignored for now";
let ids = ids0 in
if BorrowId.Set.is_empty ids then (
(* If the set of ids is empty, we can eliminate this shared loan.
@@ -2289,10 +2290,10 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
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.value));
- assert (not (value_has_loans_or_borrows ctx sv0.value));
- assert (is_aignored child0.value);
- assert (is_aignored child1.value);
+ cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message";
+ cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message";
+ cassert (is_aignored child0.value) meta "TODO: error message";
+ cassert (is_aignored child1.value) meta "TODO: error message";
None)
else (
(* Register the loan ids *)
@@ -2304,7 +2305,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
| _ ->
(* Unreachable because those cases are ignored (ended/ignored borrows)
or inconsistent *)
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
in
(* Note that because we may filter ids from a set of id, this function has
@@ -2315,12 +2316,12 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
match (lc0, lc1) with
| Concrete _, Concrete _ ->
(* This can not happen: the values should have been destructured *)
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
| Abstract (ty0, lc0), Abstract (ty1, lc1) ->
merge_aloan_contents ty0 lc0 ty1 lc1
| Concrete _, Abstract _ | Abstract _, Concrete _ ->
(* TODO: is it really unreachable? *)
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
in
(* Note that we first explore the borrows/loans of [abs1], because we
@@ -2361,12 +2362,12 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
a concrete borrow can only happen inside a shared
loan
*)
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
| Abstract (ty, bc) -> { value = ABorrow bc; ty })
| Some bc0, Some bc1 ->
- assert (merge_funs <> None);
+ cassert (merge_funs <> None) meta "TODO: error message";
merge_g_borrow_contents bc0 bc1
- | None, None -> raise (Failure "Unreachable")
+ | None, None -> craise meta "Unreachable"
in
push_avalue av)
| LoanId bid ->
@@ -2399,15 +2400,15 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
| Concrete _ ->
(* This shouldn't happen because the avalues should
have been destructured. *)
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
| Abstract (ty, lc) -> (
match lc with
| ASharedLoan (bids, sv, child) ->
let bids = filter_bids bids in
- assert (not (BorrowId.Set.is_empty bids));
- assert (is_aignored child.value);
- assert (
- not (value_has_loans_or_borrows ctx sv.value));
+ cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message";
+ cassert (is_aignored child.value) meta "TODO: error message";
+ cassert (
+ not (value_has_loans_or_borrows ctx sv.value)) meta "TODO: error message";
let lc = ASharedLoan (bids, sv, child) in
set_loans_as_merged bids;
Some { value = ALoan lc; ty }
@@ -2418,11 +2419,11 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
| AIgnoredMutLoan _ | AEndedIgnoredMutLoan _
| AIgnoredSharedLoan _ ->
(* The abstraction has been destructured, so those shouldn't appear *)
- raise (Failure "Unreachable")))
+ craise meta "Unreachable"))
| Some lc0, Some lc1 ->
- assert (merge_funs <> None);
+ cassert (merge_funs <> None) meta "TODO: error message";
merge_g_loan_contents lc0 lc1
- | None, None -> raise (Failure "Unreachable")
+ | None, None -> craise meta "Unreachable"
in
push_opt_avalue av))
borrows_loans;
@@ -2440,7 +2441,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
match av.value with
| ABorrow _ -> true
| ALoan _ -> false
- | _ -> raise (Failure "Unexpected")
+ | _ -> craise meta "Unexpected"
in
let aborrows, aloans = List.partition is_borrow avalues in
List.append aborrows aloans
@@ -2475,7 +2476,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
in
(* Sanity check *)
- if !Config.sanity_checks then assert (abs_is_destructured true ctx abs);
+ if !Config.sanity_checks then cassert (abs_is_destructured meta true ctx abs) meta "TODO: error message";
(* Return *)
abs
@@ -2486,7 +2487,7 @@ let ctx_merge_regions (ctx : eval_ctx) (rid : RegionId.id)
let env = Substitute.env_subst_rids rsubst ctx.env in
{ ctx with env }
-let merge_into_abstraction (abs_kind : abs_kind) (can_end : bool)
+let merge_into_abstraction (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
(merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx)
(abs_id0 : AbstractionId.id) (abs_id1 : AbstractionId.id) :
eval_ctx * AbstractionId.id =
@@ -2496,7 +2497,7 @@ let merge_into_abstraction (abs_kind : abs_kind) (can_end : bool)
(* Merge them *)
let nabs =
- merge_into_abstraction_aux abs_kind can_end merge_funs ctx abs0 abs1
+ merge_into_abstraction_aux meta abs_kind can_end merge_funs ctx abs0 abs1
in
(* Update the environment: replace the abstraction 1 with the result of the merge,
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-11 04:14:36 +0000