diff options
Diffstat (limited to 'compiler/InterpreterProjectors.ml')
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 91 |
1 files changed, 46 insertions, 45 deletions
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 4dc53586..d4a237b2 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -6,12 +6,13 @@ module Assoc = AssociatedTypes open TypesUtils open InterpreterUtils open InterpreterBorrowsCore +open Errors (** The local logger *) let log = Logging.projectors_log (** [ty] shouldn't contain erased regions *) -let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx) +let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (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 @@ -34,12 +35,12 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx) let proj_fields = List.map (fun (fv, fty) -> - apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions fv + apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow regions fv fty) fields_types in List.concat proj_fields - | VBottom, _ -> raise (Failure "Unreachable") + | VBottom, _ -> craise meta "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 = @@ -48,28 +49,28 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx) | VMutBorrow (bid, bv), RMut -> (* Apply the projection on the borrowed value *) let asb = - apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions + apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow regions bv ref_ty in (bid, asb) | VSharedBorrow bid, RShared -> (* Lookup the shared value *) let ek = ek_all in - let sv = lookup_loan ek bid ctx in + let sv = lookup_loan meta ek bid ctx in let asb = match sv with | _, Concrete (VSharedLoan (_, sv)) | _, Abstract (ASharedLoan (_, sv, _)) -> - apply_proj_borrows_on_shared_borrow ctx fresh_reborrow + apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow regions sv ref_ty - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" in (bid, asb) | VReservedMutBorrow _, _ -> - raise - (Failure - "Can't apply a proj_borrow over a reserved mutable borrow") - | _ -> raise (Failure "Unreachable") + craise + meta + "Can't apply a proj_borrow over a reserved mutable borrow" + | _ -> craise meta "Unreachable" in let asb = (* Check if the region is in the set of projected regions (note that @@ -80,14 +81,14 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx) else asb in asb - | VLoan _, _ -> raise (Failure "Unreachable") + | VLoan _, _ -> craise meta "Unreachable" | VSymbolic s, _ -> (* Check that the projection doesn't contain ended regions *) - assert (not (projections_intersect s.sv_ty ctx.ended_regions ty regions)); + assert (not (projections_intersect meta s.sv_ty ctx.ended_regions ty regions)); [ AsbProjReborrows (s, ty) ] - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" -let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) +let rec apply_proj_borrows (meta : Meta.meta) (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 = @@ -111,12 +112,12 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) let proj_fields = List.map (fun (fv, fty) -> - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow + apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions fv fty) fields_types in AAdt { variant_id = adt.variant_id; field_values = proj_fields } - | VBottom, _ -> raise (Failure "Unreachable") + | VBottom, _ -> craise meta "Unreachable" | VBorrow bc, TRef (r, ref_ty, kind) -> if (* Check if the region is in the set of projected regions (note that @@ -129,7 +130,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) | VMutBorrow (bid, bv), RMut -> (* Apply the projection on the borrowed value *) let bv = - apply_proj_borrows check_symbolic_no_ended ctx + apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions bv ref_ty in AMutBorrow (bid, bv) @@ -147,11 +148,11 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) *) ASharedBorrow bid | VReservedMutBorrow _, _ -> - raise - (Failure + craise + meta "Can't apply a proj_borrow over a reserved mutable \ - borrow") - | _ -> raise (Failure "Unreachable") + borrow" + | _ -> craise meta "Unreachable" in ABorrow bc else @@ -163,7 +164,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) | VMutBorrow (bid, bv), RMut -> (* Apply the projection on the borrowed value *) let bv = - apply_proj_borrows check_symbolic_no_ended ctx + apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions bv ref_ty in (* If the borrow id is in the ancestor's regions, we still need @@ -176,25 +177,25 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) | VSharedBorrow bid, RShared -> (* Lookup the shared value *) let ek = ek_all in - let sv = lookup_loan ek bid ctx in + let sv = lookup_loan meta ek bid ctx in let asb = match sv with | _, Concrete (VSharedLoan (_, sv)) | _, Abstract (ASharedLoan (_, sv, _)) -> - apply_proj_borrows_on_shared_borrow ctx fresh_reborrow + apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow regions sv ref_ty - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" in AProjSharedBorrow asb | VReservedMutBorrow _, _ -> - raise - (Failure + craise + meta "Can't apply a proj_borrow over a reserved mutable \ - borrow") - | _ -> raise (Failure "Unreachable") + borrow" + | _ -> craise meta "Unreachable" in ABorrow bc - | VLoan _, _ -> raise (Failure "Unreachable") + | VLoan _, _ -> craise meta "Unreachable" | VSymbolic s, _ -> (* Check that the projection doesn't contain already ended regions, * if necessary *) @@ -211,7 +212,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: " ^ RegionId.Set.to_string None rset2 ^ "\n")); - assert (not (projections_intersect ty1 rset1 ty2 rset2))); + assert (not (projections_intersect meta ty1 rset1 ty2 rset2))); ASymbolic (AProjBorrows (s, ty)) | _ -> log#lerror @@ -219,11 +220,11 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) ("apply_proj_borrows: unexpected inputs:\n- input value: " ^ typed_value_to_string ctx v ^ "\n- proj rty: " ^ ty_to_string ctx ty)); - raise (Failure "Unreachable") + craise meta "Unreachable" in { value; ty } -let symbolic_expansion_non_borrow_to_value (sv : symbolic_value) +let symbolic_expansion_non_borrow_to_value (meta : Meta.meta) (sv : symbolic_value) (see : symbolic_expansion) : typed_value = let ty = Subst.erase_regions sv.sv_ty in let value = @@ -235,11 +236,11 @@ let symbolic_expansion_non_borrow_to_value (sv : symbolic_value) in VAdt { variant_id; field_values } | SeMutRef (_, _) | SeSharedRef (_, _) -> - raise (Failure "Unexpected symbolic reference expansion") + craise meta "Unexpected symbolic reference expansion" in { value; ty } -let symbolic_expansion_non_shared_borrow_to_value (sv : symbolic_value) +let symbolic_expansion_non_shared_borrow_to_value (meta : Meta.meta) (sv : symbolic_value) (see : symbolic_expansion) : typed_value = match see with | SeMutRef (bid, bv) -> @@ -248,14 +249,14 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : symbolic_value) 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 + craise meta "Unexpected symbolic shared reference expansion" + | _ -> symbolic_expansion_non_borrow_to_value meta sv see (** Apply (and reduce) a projector over loans to a value. TODO: detailed comments. See [apply_proj_borrows] *) -let apply_proj_loans_on_symbolic_expansion (regions : RegionId.Set.t) +let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (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 @@ -305,7 +306,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : RegionId.Set.t) else (* Not in the set: ignore *) (ALoan (AIgnoredSharedLoan child_av), ref_ty) - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in { value; ty } @@ -467,7 +468,7 @@ let apply_reborrows (reborrows : (BorrowId.id * BorrowId.id) list) (* Return *) ctx -let prepare_reborrows (config : config) (allow_reborrows : bool) : +let prepare_reborrows (meta : Meta.meta) (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 *) @@ -476,7 +477,7 @@ let prepare_reborrows (config : config) (allow_reborrows : bool) : let bid' = fresh_borrow_id () in reborrows := (bid, bid') :: !reborrows; bid') - else raise (Failure "Unexpected reborrow") + else craise meta "Unexpected reborrow" in (* The function to apply the reborrows in a context *) let apply_registered_reborrows (ctx : eval_ctx) : eval_ctx = @@ -491,7 +492,7 @@ let prepare_reborrows (config : config) (allow_reborrows : bool) : (fresh_reborrow, apply_registered_reborrows) (** [ty] shouldn't have erased regions *) -let apply_proj_borrows_on_input_value (config : config) (ctx : eval_ctx) +let apply_proj_borrows_on_input_value (meta : Meta.meta) (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); @@ -499,11 +500,11 @@ let apply_proj_borrows_on_input_value (config : config) (ctx : eval_ctx) let allow_reborrows = true in (* Prepare the reborrows *) let fresh_reborrow, apply_registered_reborrows = - prepare_reborrows config allow_reborrows + prepare_reborrows meta config allow_reborrows in (* Apply the projector *) let av = - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions + apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions v ty in (* Apply the reborrows *) |