summaryrefslogtreecommitdiff
path: root/compiler/InterpreterProjectors.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/InterpreterProjectors.ml')
-rw-r--r--compiler/InterpreterProjectors.ml56
1 files changed, 28 insertions, 28 deletions
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index f8f99584..0421a46c 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -18,7 +18,7 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : 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
- sanity_check (ty_is_rty ty && ety = v.ty) meta;
+ sanity_check __FILE__ __LINE__ (ty_is_rty ty && ety = v.ty) meta;
(* Project - if there are no regions from the abstraction in the type, return [_] *)
if not (ty_has_regions_in_set regions ty) then []
else
@@ -41,7 +41,7 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
fields_types
in
List.concat proj_fields
- | VBottom, _ -> craise meta "Unreachable"
+ | VBottom, _ -> craise __FILE__ __LINE__ 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 =
@@ -64,13 +64,13 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
| _, Abstract (ASharedLoan (_, sv, _)) ->
apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow
regions sv ref_ty
- | _ -> craise meta "Unexpected"
+ | _ -> craise __FILE__ __LINE__ meta "Unexpected"
in
(bid, asb)
| VReservedMutBorrow _, _ ->
- craise meta
+ craise __FILE__ __LINE__ meta
"Can't apply a proj_borrow over a reserved mutable borrow"
- | _ -> craise meta "Unreachable"
+ | _ -> craise __FILE__ __LINE__ meta "Unreachable"
in
let asb =
(* Check if the region is in the set of projected regions (note that
@@ -81,15 +81,15 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
else asb
in
asb
- | VLoan _, _ -> craise meta "Unreachable"
+ | VLoan _, _ -> craise __FILE__ __LINE__ meta "Unreachable"
| VSymbolic s, _ ->
(* Check that the projection doesn't contain ended regions *)
- sanity_check
+ sanity_check __FILE__ __LINE__
(not
(projections_intersect meta s.sv_ty ctx.ended_regions ty regions))
meta;
[ AsbProjReborrows (s, ty) ]
- | _ -> craise meta "Unreachable"
+ | _ -> craise __FILE__ __LINE__ meta "Unreachable"
let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
(ctx : eval_ctx) (fresh_reborrow : BorrowId.id -> BorrowId.id)
@@ -98,7 +98,7 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
(* 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
- sanity_check (ty_is_rty ty && ety = v.ty) meta;
+ sanity_check __FILE__ __LINE__ (ty_is_rty ty && ety = v.ty) meta;
(* Project - if there are no regions from the abstraction in the type, return [_] *)
if not (ty_has_regions_in_set regions ty) then { value = AIgnored; ty }
else
@@ -121,7 +121,7 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
fields_types
in
AAdt { variant_id = adt.variant_id; field_values = proj_fields }
- | VBottom, _ -> craise meta "Unreachable"
+ | VBottom, _ -> craise __FILE__ __LINE__ meta "Unreachable"
| VBorrow bc, TRef (r, ref_ty, kind) ->
if
(* Check if the region is in the set of projected regions (note that
@@ -152,9 +152,9 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
*)
ASharedBorrow bid
| VReservedMutBorrow _, _ ->
- craise meta
+ craise __FILE__ __LINE__ meta
"Can't apply a proj_borrow over a reserved mutable borrow"
- | _ -> craise meta "Unreachable"
+ | _ -> craise __FILE__ __LINE__ meta "Unreachable"
in
ABorrow bc
else
@@ -186,16 +186,16 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
| _, Abstract (ASharedLoan (_, sv, _)) ->
apply_proj_borrows_on_shared_borrow meta ctx
fresh_reborrow regions sv ref_ty
- | _ -> craise meta "Unexpected"
+ | _ -> craise __FILE__ __LINE__ meta "Unexpected"
in
AProjSharedBorrow asb
| VReservedMutBorrow _, _ ->
- craise meta
+ craise __FILE__ __LINE__ meta
"Can't apply a proj_borrow over a reserved mutable borrow"
- | _ -> craise meta "Unreachable"
+ | _ -> craise __FILE__ __LINE__ meta "Unreachable"
in
ABorrow bc
- | VLoan _, _ -> craise meta "Unreachable"
+ | VLoan _, _ -> craise __FILE__ __LINE__ meta "Unreachable"
| VSymbolic s, _ ->
(* Check that the projection doesn't contain already ended regions,
* if necessary *)
@@ -212,7 +212,7 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
^ RegionId.Set.to_string None rset2
^ "\n"));
- sanity_check (not (projections_intersect meta ty1 rset1 ty2 rset2)))
+ sanity_check __FILE__ __LINE__ (not (projections_intersect meta ty1 rset1 ty2 rset2)))
meta;
ASymbolic (AProjBorrows (s, ty))
| _ ->
@@ -221,7 +221,7 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
("apply_proj_borrows: unexpected inputs:\n- input value: "
^ typed_value_to_string ~meta:(Some meta) ctx v
^ "\n- proj rty: " ^ ty_to_string ctx ty));
- craise meta "Unreachable"
+ craise __FILE__ __LINE__ meta "Unreachable"
in
{ value; ty }
@@ -237,7 +237,7 @@ let symbolic_expansion_non_borrow_to_value (meta : Meta.meta)
in
VAdt { variant_id; field_values }
| SeMutRef (_, _) | SeSharedRef (_, _) ->
- craise meta "Unexpected symbolic reference expansion"
+ craise __FILE__ __LINE__ meta "Unexpected symbolic reference expansion"
in
{ value; ty }
@@ -250,7 +250,7 @@ let symbolic_expansion_non_shared_borrow_to_value (meta : Meta.meta)
let value = VBorrow (VMutBorrow (bid, bv)) in
{ value; ty }
| SeSharedRef (_, _) ->
- craise meta "Unexpected symbolic shared reference expansion"
+ craise __FILE__ __LINE__ 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.
@@ -262,7 +262,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta)
(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 *)
- sanity_check (ty_has_regions_in_set regions original_sv_ty) meta;
+ sanity_check __FILE__ __LINE__ (ty_has_regions_in_set regions original_sv_ty) meta;
(* Match *)
let (value, ty) : avalue * ty =
match (see, original_sv_ty) with
@@ -277,7 +277,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta)
(AAdt { variant_id; field_values }, original_sv_ty)
| SeMutRef (bid, spc), TRef (r, ref_ty, RMut) ->
(* Sanity check *)
- sanity_check (spc.sv_ty = ref_ty) meta;
+ sanity_check __FILE__ __LINE__ (spc.sv_ty = ref_ty) meta;
(* 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
@@ -295,7 +295,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta)
(ALoan (AIgnoredMutLoan (opt_bid, child_av)), ref_ty)
| SeSharedRef (bids, spc), TRef (r, ref_ty, RShared) ->
(* Sanity check *)
- sanity_check (spc.sv_ty = ref_ty) meta;
+ sanity_check __FILE__ __LINE__ (spc.sv_ty = ref_ty) meta;
(* 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
@@ -307,7 +307,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta)
else
(* Not in the set: ignore *)
(ALoan (AIgnoredSharedLoan child_av), ref_ty)
- | _ -> craise meta "Unreachable"
+ | _ -> craise __FILE__ __LINE__ meta "Unreachable"
in
{ value; ty }
@@ -465,7 +465,7 @@ let apply_reborrows (meta : Meta.meta)
(* Visit *)
let ctx = obj#visit_eval_ctx () ctx in
(* Check that there are no reborrows remaining *)
- sanity_check (!reborrows = []) meta;
+ sanity_check __FILE__ __LINE__ (!reborrows = []) meta;
(* Return *)
ctx
@@ -479,13 +479,13 @@ let prepare_reborrows (config : config) (meta : Meta.meta)
let bid' = fresh_borrow_id () in
reborrows := (bid, bid') :: !reborrows;
bid')
- else craise meta "Unexpected reborrow"
+ else craise __FILE__ __LINE__ meta "Unexpected reborrow"
in
(* The function to apply the reborrows in a context *)
let apply_registered_reborrows (ctx : eval_ctx) : eval_ctx =
match config.mode with
| ConcreteMode ->
- sanity_check (!reborrows = []) meta;
+ sanity_check __FILE__ __LINE__ (!reborrows = []) meta;
ctx
| SymbolicMode ->
(* Apply the reborrows *)
@@ -498,7 +498,7 @@ let apply_proj_borrows_on_input_value (config : config) (meta : Meta.meta)
(ctx : eval_ctx) (regions : RegionId.Set.t)
(ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) :
eval_ctx * typed_avalue =
- cassert (ty_is_rty ty) meta "TODO: error message";
+ cassert __FILE__ __LINE__ (ty_is_rty ty) meta "TODO: error message";
let check_symbolic_no_ended = true in
let allow_reborrows = true in
(* Prepare the reborrows *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 16:41:13 +0000