From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 19:28:56 +0100 Subject: Remove the 'r type variable from the ty type definition --- compiler/InterpreterProjectors.ml | 35 +++++++++++++++++++---------------- 1 file changed, 19 insertions(+), 16 deletions(-) (limited to 'compiler/InterpreterProjectors.ml') diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 9e0c2b75..70a77be5 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -12,20 +12,21 @@ open InterpreterBorrowsCore (** The local logger *) let log = L.projectors_log +(** [ty] shouldn't contain erased regions *) let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id) (regions : T.RegionId.Set.t) (v : V.typed_value) (ty : T.rty) : V.abstract_shared_borrows = - (* Sanity check - TODO: move this elsewhere (here we perform the check at every + (* Sanity check - TODO: move those elsewhere (here we perform the check at every * recursive call which is a bit overkill...) *) let ety = Subst.erase_regions ty in - assert (ety = v.V.ty); + assert (ty_is_rty ty && ety = v.V.ty); (* Project - if there are no regions from the abstraction in the type, return [_] *) if not (ty_has_regions_in_set regions ty) then [] else match (v.V.value, ty) with - | V.Literal _, T.Literal _ -> [] - | V.Adt adt, T.Adt (id, generics) -> + | V.VLiteral _, T.TLiteral _ -> [] + | V.VAdt adt, T.TAdt (id, generics) -> (* Retrieve the types of the fields *) let field_types = Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics @@ -97,14 +98,14 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) (* Sanity check - TODO: move this elsewhere (here we perform the check at every * recursive call which is a bit overkill...) *) let ety = Substitute.erase_regions ty in - assert (ety = v.V.ty); + assert (ty_is_rty ty && ety = v.V.ty); (* Project - if there are no regions from the abstraction in the type, return [_] *) if not (ty_has_regions_in_set regions ty) then { V.value = V.AIgnored; ty } else let value : V.avalue = match (v.V.value, ty) with - | V.Literal _, T.Literal _ -> V.AIgnored - | V.Adt adt, T.Adt (id, generics) -> + | V.VLiteral _, T.TLiteral _ -> V.AIgnored + | V.VAdt adt, T.TAdt (id, generics) -> (* Retrieve the types of the fields *) let field_types = Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics @@ -208,10 +209,10 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) let rset2 = regions in log#ldebug (lazy - ("projections_intersect:" ^ "\n- ty1: " ^ rty_to_string ctx ty1 - ^ "\n- rset1: " + ("projections_intersect:" ^ "\n- ty1: " + ^ PA.ty_to_string ctx ty1 ^ "\n- rset1: " ^ T.RegionId.Set.to_string None rset1 - ^ "\n- ty2: " ^ rty_to_string ctx ty2 ^ "\n- rset2: " + ^ "\n- ty2: " ^ PA.ty_to_string ctx ty2 ^ "\n- rset2: " ^ T.RegionId.Set.to_string None rset2 ^ "\n")); assert (not (projections_intersect ty1 rset1 ty2 rset2))); @@ -221,7 +222,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) (lazy ("apply_proj_borrows: unexpected inputs:\n- input value: " ^ typed_value_to_string ctx v - ^ "\n- proj rty: " ^ rty_to_string ctx ty)); + ^ "\n- proj rty: " ^ PA.ty_to_string ctx ty)); raise (Failure "Unreachable") in { V.value; V.ty } @@ -231,12 +232,12 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value) let ty = Subst.erase_regions sv.V.sv_ty in let value = match see with - | SeLiteral cv -> V.Literal cv + | SeLiteral cv -> V.VLiteral cv | SeAdt (variant_id, field_values) -> let field_values = List.map mk_typed_value_from_symbolic_value field_values in - V.Adt { V.variant_id; V.field_values } + V.VAdt { V.variant_id; V.field_values } | SeMutRef (_, _) | SeSharedRef (_, _) -> raise (Failure "Unexpected symbolic reference expansion") in @@ -265,10 +266,10 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t) * contain regions which we will project *) assert (ty_has_regions_in_set regions original_sv_ty); (* Match *) - let (value, ty) : V.avalue * T.rty = + let (value, ty) : V.avalue * T.ty = match (see, original_sv_ty) with - | SeLiteral _, T.Literal _ -> (V.AIgnored, original_sv_ty) - | SeAdt (variant_id, field_values), T.Adt (_id, _generics) -> + | SeLiteral _, T.TLiteral _ -> (V.AIgnored, original_sv_ty) + | SeAdt (variant_id, field_values), T.TAdt (_id, _generics) -> (* Project over the field values *) let field_values = List.map @@ -493,9 +494,11 @@ let prepare_reborrows (config : C.config) (allow_reborrows : bool) : in (fresh_reborrow, apply_registered_reborrows) +(** [ty] shouldn't have erased regions *) let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx) (regions : T.RegionId.Set.t) (ancestors_regions : T.RegionId.Set.t) (v : V.typed_value) (ty : T.rty) : C.eval_ctx * V.typed_avalue = + assert (ty_is_rty ty); let check_symbolic_no_ended = true in let allow_reborrows = true in (* Prepare the reborrows *) -- cgit v1.2.3 From 6ef68fa9ffd4caec09677ee2800a778080d6da34 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 20:04:11 +0100 Subject: Prefix variants related to types with "T" --- compiler/InterpreterProjectors.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'compiler/InterpreterProjectors.ml') diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 70a77be5..e47886ec 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -43,7 +43,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) in List.concat proj_fields | V.Bottom, _ -> raise (Failure "Unreachable") - | V.Borrow bc, T.Ref (r, ref_ty, kind) -> + | V.Borrow bc, TRef (r, ref_ty, kind) -> (* Retrieve the bid of the borrow and the asb of the projected borrowed value *) let bid, asb = (* Not in the set: dive *) @@ -121,7 +121,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) in V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields } | V.Bottom, _ -> raise (Failure "Unreachable") - | V.Borrow bc, T.Ref (r, ref_ty, kind) -> + | V.Borrow bc, TRef (r, ref_ty, kind) -> if (* Check if the region is in the set of projected regions (note that * we never project over static regions) *) @@ -277,7 +277,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t) field_values in (V.AAdt { V.variant_id; field_values }, original_sv_ty) - | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) -> + | SeMutRef (bid, spc), TRef (r, ref_ty, T.Mut) -> (* Sanity check *) assert (spc.V.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) @@ -295,7 +295,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t) if region_in_set r ancestors_regions then Some bid else None in (V.ALoan (V.AIgnoredMutLoan (opt_bid, child_av)), ref_ty) - | SeSharedRef (bids, spc), T.Ref (r, ref_ty, T.Shared) -> + | SeSharedRef (bids, spc), TRef (r, ref_ty, T.Shared) -> (* Sanity check *) assert (spc.V.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) -- cgit v1.2.3 From 746239e8f29de85f848d14e44eac8690e2065a1d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 20:41:58 +0100 Subject: Add the "V" prefix to most variants related to values --- compiler/InterpreterProjectors.ml | 112 +++++++++++++++++++------------------- 1 file changed, 56 insertions(+), 56 deletions(-) (limited to 'compiler/InterpreterProjectors.ml') diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index e47886ec..8a4b0b4c 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -20,20 +20,20 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) (* Sanity check - TODO: move those elsewhere (here we perform the check at every * recursive call which is a bit overkill...) *) let ety = Subst.erase_regions ty in - assert (ty_is_rty ty && ety = v.V.ty); + assert (ty_is_rty ty && ety = v.ty); (* Project - if there are no regions from the abstraction in the type, return [_] *) if not (ty_has_regions_in_set regions ty) then [] else - match (v.V.value, ty) with - | V.VLiteral _, T.TLiteral _ -> [] - | V.VAdt adt, T.TAdt (id, generics) -> + match (v.value, ty) with + | VLiteral _, TLiteral _ -> [] + | VAdt adt, TAdt (id, generics) -> (* Retrieve the types of the fields *) let field_types = Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics in (* Project over the field values *) - let fields_types = List.combine adt.V.field_values field_types in + let fields_types = List.combine adt.field_values field_types in let proj_fields = List.map (fun (fv, fty) -> @@ -42,33 +42,33 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) fields_types in List.concat proj_fields - | V.Bottom, _ -> raise (Failure "Unreachable") - | V.Borrow bc, TRef (r, ref_ty, kind) -> + | VBottom, _ -> raise (Failure "Unreachable") + | VBorrow bc, TRef (r, ref_ty, kind) -> (* Retrieve the bid of the borrow and the asb of the projected borrowed value *) let bid, asb = (* Not in the set: dive *) match (bc, kind) with - | V.MutBorrow (bid, bv), T.Mut -> + | VMutBorrow (bid, bv), Mut -> (* Apply the projection on the borrowed value *) let asb = apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions bv ref_ty in (bid, asb) - | V.SharedBorrow bid, T.Shared -> + | VSharedBorrow bid, Shared -> (* Lookup the shared value *) let ek = ek_all in let sv = lookup_loan ek bid ctx in let asb = match sv with - | _, Concrete (V.SharedLoan (_, sv)) - | _, Abstract (V.ASharedLoan (_, sv, _)) -> + | _, Concrete (VSharedLoan (_, sv)) + | _, Abstract (ASharedLoan (_, sv, _)) -> apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions sv ref_ty | _ -> raise (Failure "Unexpected") in (bid, asb) - | V.ReservedMutBorrow _, _ -> + | VReservedMutBorrow _, _ -> raise (Failure "Can't apply a proj_borrow over a reserved mutable borrow") @@ -83,8 +83,8 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) else asb in asb - | V.Loan _, _ -> raise (Failure "Unreachable") - | V.Symbolic s, _ -> + | VLoan _, _ -> raise (Failure "Unreachable") + | VSymbolic s, _ -> (* Check that the projection doesn't contain ended regions *) assert ( not (projections_intersect s.V.sv_ty ctx.ended_regions ty regions)); @@ -103,15 +103,15 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) if not (ty_has_regions_in_set regions ty) then { V.value = V.AIgnored; ty } else let value : V.avalue = - match (v.V.value, ty) with - | V.VLiteral _, T.TLiteral _ -> V.AIgnored - | V.VAdt adt, T.TAdt (id, generics) -> + match (v.value, ty) with + | VLiteral _, T.TLiteral _ -> V.AIgnored + | VAdt adt, T.TAdt (id, generics) -> (* Retrieve the types of the fields *) let field_types = Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics in (* Project over the field values *) - let fields_types = List.combine adt.V.field_values field_types in + let fields_types = List.combine adt.field_values field_types in let proj_fields = List.map (fun (fv, fty) -> @@ -119,9 +119,9 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) regions ancestors_regions fv fty) fields_types in - V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields } - | V.Bottom, _ -> raise (Failure "Unreachable") - | V.Borrow bc, TRef (r, ref_ty, kind) -> + V.AAdt { variant_id = adt.variant_id; field_values = proj_fields } + | VBottom, _ -> raise (Failure "Unreachable") + | VBorrow bc, TRef (r, ref_ty, kind) -> if (* Check if the region is in the set of projected regions (note that * we never project over static regions) *) @@ -130,14 +130,14 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) (* In the set *) let bc = match (bc, kind) with - | V.MutBorrow (bid, bv), T.Mut -> + | VMutBorrow (bid, bv), T.Mut -> (* Apply the projection on the borrowed value *) let bv = apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions bv ref_ty in V.AMutBorrow (bid, bv) - | V.SharedBorrow bid, T.Shared -> + | VSharedBorrow bid, T.Shared -> (* Rem.: we don't need to also apply the projection on the borrowed value, because for as long as the abstraction lives then the shared borrow lives, which means that the @@ -150,7 +150,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) other branch of the [if then else]). *) V.ASharedBorrow bid - | V.ReservedMutBorrow _, _ -> + | VReservedMutBorrow _, _ -> raise (Failure "Can't apply a proj_borrow over a reserved mutable \ @@ -164,7 +164,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) the region set) *) let bc = match (bc, kind) with - | V.MutBorrow (bid, bv), T.Mut -> + | VMutBorrow (bid, bv), T.Mut -> (* Apply the projection on the borrowed value *) let bv = apply_proj_borrows check_symbolic_no_ended ctx @@ -177,20 +177,20 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) in (* Return *) V.AIgnoredMutBorrow (opt_bid, bv) - | V.SharedBorrow bid, T.Shared -> + | VSharedBorrow bid, T.Shared -> (* Lookup the shared value *) let ek = ek_all in let sv = lookup_loan ek bid ctx in let asb = match sv with - | _, Concrete (V.SharedLoan (_, sv)) - | _, Abstract (V.ASharedLoan (_, sv, _)) -> + | _, Concrete (VSharedLoan (_, sv)) + | _, Abstract (ASharedLoan (_, sv, _)) -> apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions sv ref_ty | _ -> raise (Failure "Unexpected") in V.AProjSharedBorrow asb - | V.ReservedMutBorrow _, _ -> + | VReservedMutBorrow _, _ -> raise (Failure "Can't apply a proj_borrow over a reserved mutable \ @@ -198,12 +198,12 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) | _ -> raise (Failure "Unreachable") in V.ABorrow bc - | V.Loan _, _ -> raise (Failure "Unreachable") - | V.Symbolic s, _ -> + | VLoan _, _ -> raise (Failure "Unreachable") + | VSymbolic s, _ -> (* Check that the projection doesn't contain already ended regions, * if necessary *) if check_symbolic_no_ended then ( - let ty1 = s.V.sv_ty in + let ty1 = s.sv_ty in let rset1 = ctx.ended_regions in let ty2 = ty in let rset2 = regions in @@ -216,7 +216,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) ^ T.RegionId.Set.to_string None rset2 ^ "\n")); assert (not (projections_intersect ty1 rset1 ty2 rset2))); - V.ASymbolic (V.AProjBorrows (s, ty)) + V.ASymbolic (AProjBorrows (s, ty)) | _ -> log#lerror (lazy @@ -225,7 +225,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) ^ "\n- proj rty: " ^ PA.ty_to_string ctx ty)); raise (Failure "Unreachable") in - { V.value; V.ty } + { value; ty } let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value) (see : V.symbolic_expansion) : V.typed_value = @@ -249,7 +249,7 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value) | SeMutRef (bid, bv) -> let ty = Subst.erase_regions sv.V.sv_ty in let bv = mk_typed_value_from_symbolic_value bv in - let value = V.Borrow (V.MutBorrow (bid, bv)) in + let value = V.VBorrow (VMutBorrow (bid, bv)) in { V.value; ty } | SeSharedRef (_, _) -> raise (Failure "Unexpected symbolic shared reference expansion") @@ -346,11 +346,11 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) (* Check if a value is a mutable borrow, and return its identifier if it is the case *) let get_borrow_in_mut_borrow (v : V.typed_value) : V.BorrowId.id option = - match v.V.value with - | V.Borrow lc -> ( + match v.value with + | VBorrow lc -> ( match lc with - | V.SharedBorrow _ | V.ReservedMutBorrow _ -> None - | V.MutBorrow (id, _) -> Some id) + | VSharedBorrow _ | VReservedMutBorrow _ -> None + | VMutBorrow (id, _) -> Some id) | _ -> None in @@ -397,18 +397,18 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) (** We may need to reborrow mutable borrows. Note that this doesn't happen for aborrows *) method! visit_typed_value env v = - match v.V.value with - | V.Borrow (V.MutBorrow (bid, bv)) -> + match v.value with + | VBorrow (VMutBorrow (bid, bv)) -> let insert = get_reborrows_for_bid bid in - let nbc = super#visit_MutBorrow env bid bv in - let nbc = { v with V.value = V.Borrow nbc } in + let nbc = super#visit_VMutBorrow env bid bv in + let nbc = { v with value = VBorrow nbc } in if insert = [] then (* No reborrows: do nothing special *) nbc else (* There are reborrows: insert a shared loan *) let insert = borrows_to_set insert in - let value = V.Loan (V.SharedLoan (insert, nbc)) in - let ty = v.V.ty in + let value = V.VLoan (VSharedLoan (insert, nbc)) in + let ty = v.ty in { V.value; ty } | _ -> super#visit_typed_value env v @@ -416,7 +416,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) functions) on purpose: exhaustive matches are good for maintenance *) method! visit_loan_content env lc = match lc with - | V.SharedLoan (bids, sv) -> + | VSharedLoan (bids, sv) -> (* Insert the reborrows *) let bids = insert_reborrows bids in (* Check if the contained value is a mutable borrow, in which @@ -432,14 +432,14 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) | Some bid -> insert_reborrows_for_bid bids bid in (* Update and explore *) - super#visit_SharedLoan env bids sv - | V.MutLoan bid -> + super#visit_VSharedLoan env bids sv + | VMutLoan bid -> (* Nothing special to do *) - super#visit_MutLoan env bid + super#visit_VMutLoan env bid method! visit_aloan_content env lc = match lc with - | V.ASharedLoan (bids, sv, av) -> + | ASharedLoan (bids, sv, av) -> (* Insert the reborrows *) let bids = insert_reborrows bids in (* Similarly to the non-abstraction case: check if the shared @@ -452,12 +452,12 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) in (* Update and explore *) super#visit_ASharedLoan env bids sv av - | V.AIgnoredSharedLoan _ - | V.AMutLoan (_, _) - | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AEndedSharedLoan (_, _) - | V.AIgnoredMutLoan (_, _) - | V.AEndedIgnoredMutLoan + | AIgnoredSharedLoan _ + | AMutLoan (_, _) + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedSharedLoan (_, _) + | AIgnoredMutLoan (_, _) + | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } -> (* Nothing particular to do *) super#visit_aloan_content env lc -- cgit v1.2.3 From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 15 Nov 2023 22:03:21 +0100 Subject: Start updating the name type, cleanup the names and the module abbrevs --- compiler/InterpreterProjectors.ml | 182 +++++++++++++++++++------------------- 1 file changed, 89 insertions(+), 93 deletions(-) (limited to 'compiler/InterpreterProjectors.ml') diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 8a4b0b4c..4dc53586 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -1,22 +1,19 @@ -module T = Types -module V = Values -module E = Expressions -module C = Contexts +open Types +open Values +open Contexts module Subst = Substitute module Assoc = AssociatedTypes -module L = Logging open TypesUtils open InterpreterUtils open InterpreterBorrowsCore (** The local logger *) -let log = L.projectors_log +let log = Logging.projectors_log (** [ty] shouldn't contain erased regions *) -let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) - (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id) - (regions : T.RegionId.Set.t) (v : V.typed_value) (ty : T.rty) : - V.abstract_shared_borrows = +let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx) + (fresh_reborrow : BorrowId.id -> BorrowId.id) (regions : RegionId.Set.t) + (v : typed_value) (ty : rty) : abstract_shared_borrows = (* Sanity check - TODO: move those elsewhere (here we perform the check at every * recursive call which is a bit overkill...) *) let ety = Subst.erase_regions ty in @@ -48,14 +45,14 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) let bid, asb = (* Not in the set: dive *) match (bc, kind) with - | VMutBorrow (bid, bv), Mut -> + | VMutBorrow (bid, bv), RMut -> (* Apply the projection on the borrowed value *) let asb = apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions bv ref_ty in (bid, asb) - | VSharedBorrow bid, Shared -> + | VSharedBorrow bid, RShared -> (* Lookup the shared value *) let ek = ek_all in let sv = lookup_loan ek bid ctx in @@ -79,33 +76,32 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) * we never project over static regions) *) if region_in_set r regions then let bid' = fresh_reborrow bid in - V.AsbBorrow bid' :: asb + AsbBorrow bid' :: asb else asb in asb | VLoan _, _ -> raise (Failure "Unreachable") | VSymbolic s, _ -> (* Check that the projection doesn't contain ended regions *) - assert ( - not (projections_intersect s.V.sv_ty ctx.ended_regions ty regions)); - [ V.AsbProjReborrows (s, ty) ] + assert (not (projections_intersect s.sv_ty ctx.ended_regions ty regions)); + [ AsbProjReborrows (s, ty) ] | _ -> raise (Failure "Unreachable") -let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) - (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id) - (regions : T.RegionId.Set.t) (ancestors_regions : T.RegionId.Set.t) - (v : V.typed_value) (ty : T.rty) : V.typed_avalue = +let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) + (fresh_reborrow : BorrowId.id -> BorrowId.id) (regions : RegionId.Set.t) + (ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) : + typed_avalue = (* Sanity check - TODO: move this elsewhere (here we perform the check at every * recursive call which is a bit overkill...) *) let ety = Substitute.erase_regions ty in - assert (ty_is_rty ty && ety = v.V.ty); + assert (ty_is_rty ty && ety = v.ty); (* Project - if there are no regions from the abstraction in the type, return [_] *) - if not (ty_has_regions_in_set regions ty) then { V.value = V.AIgnored; ty } + if not (ty_has_regions_in_set regions ty) then { value = AIgnored; ty } else - let value : V.avalue = + let value : avalue = match (v.value, ty) with - | VLiteral _, T.TLiteral _ -> V.AIgnored - | VAdt adt, T.TAdt (id, generics) -> + | VLiteral _, TLiteral _ -> AIgnored + | VAdt adt, TAdt (id, generics) -> (* Retrieve the types of the fields *) let field_types = Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics @@ -119,7 +115,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) regions ancestors_regions fv fty) fields_types in - V.AAdt { variant_id = adt.variant_id; field_values = proj_fields } + AAdt { variant_id = adt.variant_id; field_values = proj_fields } | VBottom, _ -> raise (Failure "Unreachable") | VBorrow bc, TRef (r, ref_ty, kind) -> if @@ -130,14 +126,14 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) (* In the set *) let bc = match (bc, kind) with - | VMutBorrow (bid, bv), T.Mut -> + | VMutBorrow (bid, bv), RMut -> (* Apply the projection on the borrowed value *) let bv = apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions bv ref_ty in - V.AMutBorrow (bid, bv) - | VSharedBorrow bid, T.Shared -> + AMutBorrow (bid, bv) + | VSharedBorrow bid, RShared -> (* Rem.: we don't need to also apply the projection on the borrowed value, because for as long as the abstraction lives then the shared borrow lives, which means that the @@ -149,7 +145,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) need to lookup the shared value and project it (see the other branch of the [if then else]). *) - V.ASharedBorrow bid + ASharedBorrow bid | VReservedMutBorrow _, _ -> raise (Failure @@ -157,14 +153,14 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) borrow") | _ -> raise (Failure "Unreachable") in - V.ABorrow bc + ABorrow bc else (* Not in the set: ignore the borrow, but project the borrowed value (maybe some borrows *inside* the borrowed value are in the region set) *) let bc = match (bc, kind) with - | VMutBorrow (bid, bv), T.Mut -> + | VMutBorrow (bid, bv), RMut -> (* Apply the projection on the borrowed value *) let bv = apply_proj_borrows check_symbolic_no_ended ctx @@ -176,8 +172,8 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) if region_in_set r ancestors_regions then Some bid else None in (* Return *) - V.AIgnoredMutBorrow (opt_bid, bv) - | VSharedBorrow bid, T.Shared -> + AIgnoredMutBorrow (opt_bid, bv) + | VSharedBorrow bid, RShared -> (* Lookup the shared value *) let ek = ek_all in let sv = lookup_loan ek bid ctx in @@ -189,7 +185,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) regions sv ref_ty | _ -> raise (Failure "Unexpected") in - V.AProjSharedBorrow asb + AProjSharedBorrow asb | VReservedMutBorrow _, _ -> raise (Failure @@ -197,7 +193,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) borrow") | _ -> raise (Failure "Unreachable") in - V.ABorrow bc + ABorrow bc | VLoan _, _ -> raise (Failure "Unreachable") | VSymbolic s, _ -> (* Check that the projection doesn't contain already ended regions, @@ -209,48 +205,48 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) let rset2 = regions in log#ldebug (lazy - ("projections_intersect:" ^ "\n- ty1: " - ^ PA.ty_to_string ctx ty1 ^ "\n- rset1: " - ^ T.RegionId.Set.to_string None rset1 - ^ "\n- ty2: " ^ PA.ty_to_string ctx ty2 ^ "\n- rset2: " - ^ T.RegionId.Set.to_string None rset2 + ("projections_intersect:" ^ "\n- ty1: " ^ ty_to_string ctx ty1 + ^ "\n- rset1: " + ^ RegionId.Set.to_string None rset1 + ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: " + ^ RegionId.Set.to_string None rset2 ^ "\n")); assert (not (projections_intersect ty1 rset1 ty2 rset2))); - V.ASymbolic (AProjBorrows (s, ty)) + ASymbolic (AProjBorrows (s, ty)) | _ -> log#lerror (lazy ("apply_proj_borrows: unexpected inputs:\n- input value: " ^ typed_value_to_string ctx v - ^ "\n- proj rty: " ^ PA.ty_to_string ctx ty)); + ^ "\n- proj rty: " ^ ty_to_string ctx ty)); raise (Failure "Unreachable") in { value; ty } -let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value) - (see : V.symbolic_expansion) : V.typed_value = - let ty = Subst.erase_regions sv.V.sv_ty in +let symbolic_expansion_non_borrow_to_value (sv : symbolic_value) + (see : symbolic_expansion) : typed_value = + let ty = Subst.erase_regions sv.sv_ty in let value = match see with - | SeLiteral cv -> V.VLiteral cv + | SeLiteral cv -> VLiteral cv | SeAdt (variant_id, field_values) -> let field_values = List.map mk_typed_value_from_symbolic_value field_values in - V.VAdt { V.variant_id; V.field_values } + VAdt { variant_id; field_values } | SeMutRef (_, _) | SeSharedRef (_, _) -> raise (Failure "Unexpected symbolic reference expansion") in - { V.value; V.ty } + { value; ty } -let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value) - (see : V.symbolic_expansion) : V.typed_value = +let symbolic_expansion_non_shared_borrow_to_value (sv : symbolic_value) + (see : symbolic_expansion) : typed_value = match see with | SeMutRef (bid, bv) -> - let ty = Subst.erase_regions sv.V.sv_ty in + let ty = Subst.erase_regions sv.sv_ty in let bv = mk_typed_value_from_symbolic_value bv in - let value = V.VBorrow (VMutBorrow (bid, bv)) in - { V.value; ty } + let value = VBorrow (VMutBorrow (bid, bv)) in + { value; ty } | SeSharedRef (_, _) -> raise (Failure "Unexpected symbolic shared reference expansion") | _ -> symbolic_expansion_non_borrow_to_value sv see @@ -259,34 +255,34 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value) TODO: detailed comments. See [apply_proj_borrows] *) -let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t) - (ancestors_regions : T.RegionId.Set.t) (see : V.symbolic_expansion) - (original_sv_ty : T.rty) : V.typed_avalue = +let apply_proj_loans_on_symbolic_expansion (regions : RegionId.Set.t) + (ancestors_regions : RegionId.Set.t) (see : symbolic_expansion) + (original_sv_ty : rty) : typed_avalue = (* Sanity check: if we have a proj_loans over a symbolic value, it should * contain regions which we will project *) assert (ty_has_regions_in_set regions original_sv_ty); (* Match *) - let (value, ty) : V.avalue * T.ty = + let (value, ty) : avalue * ty = match (see, original_sv_ty) with - | SeLiteral _, T.TLiteral _ -> (V.AIgnored, original_sv_ty) - | SeAdt (variant_id, field_values), T.TAdt (_id, _generics) -> + | SeLiteral _, TLiteral _ -> (AIgnored, original_sv_ty) + | SeAdt (variant_id, field_values), TAdt (_id, _generics) -> (* Project over the field values *) let field_values = List.map (mk_aproj_loans_value_from_symbolic_value regions) field_values in - (V.AAdt { V.variant_id; field_values }, original_sv_ty) - | SeMutRef (bid, spc), TRef (r, ref_ty, T.Mut) -> + (AAdt { variant_id; field_values }, original_sv_ty) + | SeMutRef (bid, spc), TRef (r, ref_ty, RMut) -> (* Sanity check *) - assert (spc.V.sv_ty = ref_ty); + assert (spc.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in (* Check if the region is in the set of projected regions (note that * we never project over static regions) *) if region_in_set r regions then (* In the set: keep *) - (V.ALoan (V.AMutLoan (bid, child_av)), ref_ty) + (ALoan (AMutLoan (bid, child_av)), ref_ty) else (* Not in the set: ignore *) (* If the borrow id is in the ancestor's regions, we still need @@ -294,10 +290,10 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t) let opt_bid = if region_in_set r ancestors_regions then Some bid else None in - (V.ALoan (V.AIgnoredMutLoan (opt_bid, child_av)), ref_ty) - | SeSharedRef (bids, spc), TRef (r, ref_ty, T.Shared) -> + (ALoan (AIgnoredMutLoan (opt_bid, child_av)), ref_ty) + | SeSharedRef (bids, spc), TRef (r, ref_ty, RShared) -> (* Sanity check *) - assert (spc.V.sv_ty = ref_ty); + assert (spc.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in (* Check if the region is in the set of projected regions (note that @@ -305,13 +301,13 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t) if region_in_set r regions then (* In the set: keep *) let shared_value = mk_typed_value_from_symbolic_value spc in - (V.ALoan (V.ASharedLoan (bids, shared_value, child_av)), ref_ty) + (ALoan (ASharedLoan (bids, shared_value, child_av)), ref_ty) else (* Not in the set: ignore *) - (V.ALoan (V.AIgnoredSharedLoan child_av), ref_ty) + (ALoan (AIgnoredSharedLoan child_av), ref_ty) | _ -> raise (Failure "Unreachable") in - { V.value; V.ty } + { value; ty } (** Auxiliary function. See [give_back_value]. @@ -335,8 +331,8 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t) borrows - easy - and mutable borrows - in this case, we reborrow the whole borrow: [mut_borrow ... ~~> shared_loan {...} (mut_borrow ...)]). *) -let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) - (ctx : C.eval_ctx) : C.eval_ctx = +let apply_reborrows (reborrows : (BorrowId.id * BorrowId.id) list) + (ctx : eval_ctx) : eval_ctx = (* This is a bit brutal, but whenever we insert a reborrow, we remove * it from the list. This allows us to check that all the reborrows were * applied before returning. @@ -345,7 +341,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) (* Check if a value is a mutable borrow, and return its identifier if it is the case *) - let get_borrow_in_mut_borrow (v : V.typed_value) : V.BorrowId.id option = + let get_borrow_in_mut_borrow (v : typed_value) : BorrowId.id option = match v.value with | VBorrow lc -> ( match lc with @@ -358,12 +354,12 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) let insert_reborrows bids = (* Find the reborrows to apply *) let insert, reborrows' = - List.partition (fun (bid, _) -> V.BorrowId.Set.mem bid bids) !reborrows + List.partition (fun (bid, _) -> BorrowId.Set.mem bid bids) !reborrows in reborrows := reborrows'; let insert = List.map snd insert in (* Insert the borrows *) - List.fold_left (fun bids bid -> V.BorrowId.Set.add bid bids) bids insert + List.fold_left (fun bids bid -> BorrowId.Set.add bid bids) bids insert in (* Get the list of reborrows for a given borrow id *) @@ -378,8 +374,8 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) let borrows_to_set bids = List.fold_left - (fun bids bid -> V.BorrowId.Set.add bid bids) - V.BorrowId.Set.empty bids + (fun bids bid -> BorrowId.Set.add bid bids) + BorrowId.Set.empty bids in (* Insert reborrows for a given borrow id into a given set of borrows *) @@ -387,12 +383,12 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) (* Find the reborrows to apply *) let insert = get_reborrows_for_bid bid in (* Insert the borrows *) - List.fold_left (fun bids bid -> V.BorrowId.Set.add bid bids) bids insert + List.fold_left (fun bids bid -> BorrowId.Set.add bid bids) bids insert in let obj = object - inherit [_] C.map_eval_ctx as super + inherit [_] map_eval_ctx as super (** We may need to reborrow mutable borrows. Note that this doesn't happen for aborrows *) @@ -407,9 +403,9 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) else (* There are reborrows: insert a shared loan *) let insert = borrows_to_set insert in - let value = V.VLoan (VSharedLoan (insert, nbc)) in + let value = VLoan (VSharedLoan (insert, nbc)) in let ty = v.ty in - { V.value; ty } + { value; ty } | _ -> super#visit_typed_value env v (** We reimplement {!visit_loan_content} (rather than one of the sub- @@ -471,33 +467,33 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) (* Return *) ctx -let prepare_reborrows (config : C.config) (allow_reborrows : bool) : - (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) = - let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in +let prepare_reborrows (config : config) (allow_reborrows : bool) : + (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx) = + let reborrows : (BorrowId.id * BorrowId.id) list ref = ref [] in (* The function to generate and register fresh reborrows *) - let fresh_reborrow (bid : V.BorrowId.id) : V.BorrowId.id = + let fresh_reborrow (bid : BorrowId.id) : BorrowId.id = if allow_reborrows then ( - let bid' = C.fresh_borrow_id () in + let bid' = fresh_borrow_id () in reborrows := (bid, bid') :: !reborrows; bid') else raise (Failure "Unexpected reborrow") in (* The function to apply the reborrows in a context *) - let apply_registered_reborrows (ctx : C.eval_ctx) : C.eval_ctx = - match config.C.mode with - | C.ConcreteMode -> + let apply_registered_reborrows (ctx : eval_ctx) : eval_ctx = + match config.mode with + | ConcreteMode -> assert (!reborrows = []); ctx - | C.SymbolicMode -> + | SymbolicMode -> (* Apply the reborrows *) apply_reborrows !reborrows ctx in (fresh_reborrow, apply_registered_reborrows) (** [ty] shouldn't have erased regions *) -let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx) - (regions : T.RegionId.Set.t) (ancestors_regions : T.RegionId.Set.t) - (v : V.typed_value) (ty : T.rty) : C.eval_ctx * V.typed_avalue = +let apply_proj_borrows_on_input_value (config : config) (ctx : eval_ctx) + (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t) + (v : typed_value) (ty : rty) : eval_ctx * typed_avalue = assert (ty_is_rty ty); let check_symbolic_no_ended = true in let allow_reborrows = true in -- cgit v1.2.3