summaryrefslogtreecommitdiff
path: root/compiler/InterpreterLoopsMatchCtxs.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/InterpreterLoopsMatchCtxs.ml')
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml326
1 files changed, 163 insertions, 163 deletions
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index b95148bd..e25adb2c 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -20,7 +20,7 @@ module S = SynthesizeSymbolic
(** The local logger *)
let log = Logging.loops_match_ctxs_log
-let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool)
+let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
(explore : abs -> bool) (env : env) : abs_borrows_loans_maps =
let abs_ids = ref [] in
let abs_to_borrows = ref AbstractionId.Map.empty in
@@ -45,7 +45,7 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool)
| Some set ->
sanity_check __FILE__ __LINE__
((not check_not_already_registered) || not (Id1.Set.mem id1 set))
- meta);
+ span);
(* Update the mapping *)
map :=
Id0.Map.update id0
@@ -54,11 +54,11 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool)
| None -> Some (Id1.Set.singleton id1)
| Some ids ->
(* Sanity check *)
- sanity_check __FILE__ __LINE__ (not check_singleton_sets) meta;
+ sanity_check __FILE__ __LINE__ (not check_singleton_sets) span;
sanity_check __FILE__ __LINE__
((not check_not_already_registered)
|| not (Id1.Set.mem id1 ids))
- meta;
+ span;
(* Update *)
Some (Id1.Set.add id1 ids))
!map
@@ -92,12 +92,12 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool)
(* Process those normally *)
super#visit_aloan_content abs_id lc
| AIgnoredMutLoan (_, child)
- | AEndedIgnoredMutLoan { child; given_back = _; given_back_meta = _ }
+ | AEndedIgnoredMutLoan { child; given_back = _; given_back_span = _ }
| AIgnoredSharedLoan child ->
(* Ignore the id of the loan, if there is *)
self#visit_typed_avalue abs_id child
| AEndedMutLoan _ | AEndedSharedLoan _ ->
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
(** Make sure we don't register the ignored ids *)
method! visit_aborrow_content abs_id bc =
@@ -106,12 +106,12 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool)
(* Process those normally *)
super#visit_aborrow_content abs_id bc
| AIgnoredMutBorrow (_, child)
- | AEndedIgnoredMutBorrow { child; given_back = _; given_back_meta = _ }
+ | AEndedIgnoredMutBorrow { child; given_back = _; given_back_span = _ }
->
(* Ignore the id of the borrow, if there is *)
self#visit_typed_avalue abs_id child
| AEndedMutBorrow _ | AEndedSharedBorrow ->
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
method! visit_borrow_id abs_id bid = register_borrow_id abs_id bid
method! visit_loan_id abs_id lid = register_loan_id abs_id lid
@@ -147,18 +147,18 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool)
TODO: probably don't need to take [match_regions] as input anymore.
*)
-let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty)
+let rec match_types (span : Meta.span) (match_distinct_types : ty -> ty -> ty)
(match_regions : region -> region -> region) (ty0 : ty) (ty1 : ty) : ty =
- let match_rec = match_types meta match_distinct_types match_regions in
+ let match_rec = match_types span match_distinct_types match_regions in
match (ty0, ty1) with
| TAdt (id0, generics0), TAdt (id1, generics1) ->
- sanity_check __FILE__ __LINE__ (id0 = id1) meta;
+ sanity_check __FILE__ __LINE__ (id0 = id1) span;
sanity_check __FILE__ __LINE__
(generics0.const_generics = generics1.const_generics)
- meta;
+ span;
sanity_check __FILE__ __LINE__
(generics0.trait_refs = generics1.trait_refs)
- meta;
+ span;
let id = id0 in
let const_generics = generics1.const_generics in
let trait_refs = generics1.trait_refs in
@@ -175,23 +175,23 @@ let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty)
let generics = { regions; types; const_generics; trait_refs } in
TAdt (id, generics)
| TVar vid0, TVar vid1 ->
- sanity_check __FILE__ __LINE__ (vid0 = vid1) meta;
+ sanity_check __FILE__ __LINE__ (vid0 = vid1) span;
let vid = vid0 in
TVar vid
| TLiteral lty0, TLiteral lty1 ->
- sanity_check __FILE__ __LINE__ (lty0 = lty1) meta;
+ sanity_check __FILE__ __LINE__ (lty0 = lty1) span;
ty0
| TNever, TNever -> ty0
| TRef (r0, ty0, k0), TRef (r1, ty1, k1) ->
let r = match_regions r0 r1 in
let ty = match_rec ty0 ty1 in
- sanity_check __FILE__ __LINE__ (k0 = k1) meta;
+ sanity_check __FILE__ __LINE__ (k0 = k1) span;
let k = k0 in
TRef (r, ty, k)
| _ -> match_distinct_types ty0 ty1
module MakeMatcher (M : PrimMatcher) : Matcher = struct
- let meta = M.meta
+ let span = M.span
let rec match_typed_values (ctx0 : eval_ctx) (ctx1 : eval_ctx)
(v0 : typed_value) (v1 : typed_value) : typed_value =
@@ -221,10 +221,10 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
(* For now, we don't merge ADTs which contain borrows *)
sanity_check __FILE__ __LINE__
(not (value_has_borrows v0.value))
- M.meta;
+ M.span;
sanity_check __FILE__ __LINE__
(not (value_has_borrows v1.value))
- M.meta;
+ M.span;
(* Merge *)
M.match_distinct_adts ctx0 ctx1 ty av0 av1)
| VBottom, VBottom -> v0
@@ -243,7 +243,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
(not
(ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos
bv.value))
- M.meta "The join of nested borrows is not supported yet";
+ M.span "The join of nested borrows is not supported yet";
let bid, bv =
M.match_mut_borrows ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv
in
@@ -256,7 +256,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
trying to match a reserved borrow, which shouldn't happen because
reserved borrow should be eliminated very quickly - they are introduced
just before function calls which activate them *)
- craise __FILE__ __LINE__ M.meta "Unexpected"
+ craise __FILE__ __LINE__ M.span "Unexpected"
in
{ value = VBorrow bc; ty }
| VLoan lc0, VLoan lc1 ->
@@ -268,14 +268,14 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
let sv = match_rec sv0 sv1 in
cassert __FILE__ __LINE__
(not (value_has_borrows sv.value))
- M.meta "The join of nested borrows is not supported yet";
+ M.span "The join of nested borrows is not supported yet";
let ids, sv = M.match_shared_loans ctx0 ctx1 ty ids0 ids1 sv in
VSharedLoan (ids, sv)
| VMutLoan id0, VMutLoan id1 ->
let id = M.match_mut_loans ctx0 ctx1 ty id0 id1 in
VMutLoan id
| VSharedLoan _, VMutLoan _ | VMutLoan _, VSharedLoan _ ->
- craise __FILE__ __LINE__ M.meta "Unreachable"
+ craise __FILE__ __LINE__ M.span "Unreachable"
in
{ value = VLoan lc; ty = v1.ty }
| VSymbolic sv0, VSymbolic sv1 ->
@@ -283,12 +283,12 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
be eagerly expanded, and we don't support nested borrows *)
cassert __FILE__ __LINE__
(not (value_has_borrows v0.value))
- M.meta
+ M.span
"Nested borrows are not supported yet and all the symbolic values \
containing borrows are currently forced to be eagerly expanded";
cassert __FILE__ __LINE__
(not (value_has_borrows v1.value))
- M.meta
+ M.span
"Nested borrows are not supported yet and all the symbolic values \
containing borrows are currently forced to be eagerly expanded";
(* Match *)
@@ -310,19 +310,19 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
log#ldebug
(lazy
("Unexpected match case:\n- value0: "
- ^ typed_value_to_string ~meta:(Some M.meta) ctx0 v0
+ ^ typed_value_to_string ~span:(Some M.span) ctx0 v0
^ "\n- value1: "
- ^ typed_value_to_string ~meta:(Some M.meta) ctx1 v1));
- craise __FILE__ __LINE__ M.meta "Unexpected match case"
+ ^ typed_value_to_string ~span:(Some M.span) ctx1 v1));
+ craise __FILE__ __LINE__ M.span "Unexpected match case"
and match_typed_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx)
(v0 : typed_avalue) (v1 : typed_avalue) : typed_avalue =
log#ldebug
(lazy
("match_typed_avalues:\n- value0: "
- ^ typed_avalue_to_string ~meta:(Some M.meta) ctx0 v0
+ ^ typed_avalue_to_string ~span:(Some M.span) ctx0 v0
^ "\n- value1: "
- ^ typed_avalue_to_string ~meta:(Some M.meta) ctx1 v1));
+ ^ typed_avalue_to_string ~span:(Some M.span) ctx1 v1));
(* Using ValuesUtils.value_has_borrows on purpose here: we want
to make explicit the fact that, though we have to pick
@@ -348,8 +348,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
{ value; ty }
else (* Merge *)
M.match_distinct_aadts ctx0 ctx1 v0.ty av0 v1.ty av1 ty
- | ABottom, ABottom -> mk_abottom M.meta ty
- | AIgnored, AIgnored -> mk_aignored M.meta ty
+ | ABottom, ABottom -> mk_abottom M.span ty
+ | AIgnored, AIgnored -> mk_aignored M.span ty
| ABorrow bc0, ABorrow bc1 -> (
log#ldebug (lazy "match_typed_avalues: borrows");
match (bc0, bc1) with
@@ -367,7 +367,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
M.match_amut_borrows ctx0 ctx1 v0.ty bid0 av0 v1.ty bid1 av1 ty av
| AIgnoredMutBorrow _, AIgnoredMutBorrow _ ->
(* The abstractions are destructured: we shouldn't get there *)
- craise __FILE__ __LINE__ M.meta "Unexpected"
+ craise __FILE__ __LINE__ M.span "Unexpected"
| AProjSharedBorrow asb0, AProjSharedBorrow asb1 -> (
match (asb0, asb1) with
| [], [] ->
@@ -376,7 +376,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
v0
| _ ->
(* We should get there only if there are nested borrows *)
- craise __FILE__ __LINE__ M.meta "Unexpected")
+ craise __FILE__ __LINE__ M.span "Unexpected")
| _ ->
(* TODO: getting there is not necessarily inconsistent (it may
just be because the environments don't match) so we may want
@@ -387,7 +387,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
we are *currently* ending it, in which case we need
to completely end it before continuing.
*)
- craise __FILE__ __LINE__ M.meta "Unexpected")
+ craise __FILE__ __LINE__ M.span "Unexpected")
| ALoan lc0, ALoan lc1 -> (
log#ldebug (lazy "match_typed_avalues: loans");
(* TODO: maybe we should enforce that the ids are always exactly the same -
@@ -399,7 +399,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
let av = match_arec av0 av1 in
sanity_check __FILE__ __LINE__
(not (value_has_borrows sv.value))
- M.meta;
+ M.span;
M.match_ashared_loans ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1
av1 ty sv av
| AMutLoan (id0, av0), AMutLoan (id1, av1) ->
@@ -414,35 +414,35 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
| AIgnoredSharedLoan _, AIgnoredSharedLoan _ ->
(* Those should have been filtered when destructuring the abstractions -
they are necessary only when there are nested borrows *)
- craise __FILE__ __LINE__ M.meta "Unreachable"
- | _ -> craise __FILE__ __LINE__ M.meta "Unreachable")
+ craise __FILE__ __LINE__ M.span "Unreachable"
+ | _ -> craise __FILE__ __LINE__ M.span "Unreachable")
| ASymbolic _, ASymbolic _ ->
(* For now, we force all the symbolic values containing borrows to
be eagerly expanded, and we don't support nested borrows *)
- craise __FILE__ __LINE__ M.meta "Unreachable"
+ craise __FILE__ __LINE__ M.span "Unreachable"
| _ -> M.match_avalues ctx0 ctx1 v0 v1
end
module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(** Small utility *)
- let meta = S.meta
+ let span = S.span
let push_abs (abs : abs) : unit = S.nabs := abs :: !S.nabs
let push_absl (absl : abs list) : unit = List.iter push_abs absl
let match_etys _ _ ty0 ty1 =
- sanity_check __FILE__ __LINE__ (ty0 = ty1) meta;
+ sanity_check __FILE__ __LINE__ (ty0 = ty1) span;
ty0
let match_rtys _ _ ty0 ty1 =
(* The types must be equal - in effect, this forbids to match symbolic
values containing borrows *)
- sanity_check __FILE__ __LINE__ (ty0 = ty1) meta;
+ sanity_check __FILE__ __LINE__ (ty0 = ty1) span;
ty0
let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
(_ : literal) (_ : literal) : typed_value =
- mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty
+ mk_fresh_symbolic_typed_value_from_no_regions_ty span ty
let match_distinct_adts (ctx0 : eval_ctx) (ctx1 : eval_ctx) (ty : ety)
(adt0 : adt_value) (adt1 : adt_value) : typed_value =
@@ -451,7 +451,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
updates
*)
let check_no_borrows ctx (v : typed_value) =
- sanity_check __FILE__ __LINE__ (not (value_has_borrows ctx v.value)) meta
+ sanity_check __FILE__ __LINE__ (not (value_has_borrows ctx v.value)) span
in
List.iter (check_no_borrows ctx0) adt0.field_values;
List.iter (check_no_borrows ctx1) adt1.field_values;
@@ -474,18 +474,18 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
if
bottom_in_adt_value ctx0.ended_regions adt0
|| bottom_in_adt_value ctx1.ended_regions adt1
- then mk_bottom meta ty
+ then mk_bottom span ty
else
(* No borrows, no loans, no bottoms: we can introduce a symbolic value *)
- mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty
+ mk_fresh_symbolic_typed_value_from_no_regions_ty span ty
let match_shared_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) match_rec
(ty : ety) (bid0 : borrow_id) (bid1 : borrow_id) : borrow_id =
(* Lookup the shared values and match them - we do this mostly
to make sure we end loans which might appear on one side
and not on the other. *)
- let sv0 = lookup_shared_value meta ctx0 bid0 in
- let sv1 = lookup_shared_value meta ctx1 bid1 in
+ let sv0 = lookup_shared_value span ctx0 bid0 in
+ let sv1 = lookup_shared_value span ctx1 bid1 in
let sv = match_rec sv0 sv1 in
if bid0 = bid1 then bid0
else
@@ -510,7 +510,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
let borrows = [ mk_aborrow bid0; mk_aborrow bid1 ] in
let loan =
- ASharedLoan (BorrowId.Set.singleton bid2, sv, mk_aignored meta bv_ty)
+ ASharedLoan (BorrowId.Set.singleton bid2, sv, mk_aignored span bv_ty)
in
(* Note that an aloan has a borrow type *)
let loan : typed_avalue = { value = ALoan loan; ty = borrow_ty } in
@@ -588,10 +588,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
*)
cassert __FILE__ __LINE__
(not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value))
- meta "Nested borrows are not supported yet";
+ span "Nested borrows are not supported yet";
if bv0 = bv1 then (
- sanity_check __FILE__ __LINE__ (bv0 = bv) meta;
+ sanity_check __FILE__ __LINE__ (bv0 = bv) span;
(bid0, bv))
else
let rid = fresh_region_id () in
@@ -599,19 +599,19 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
let kind = RMut in
let bv_ty = bv.ty in
- sanity_check __FILE__ __LINE__ (ty_no_regions bv_ty) meta;
+ sanity_check __FILE__ __LINE__ (ty_no_regions bv_ty) span;
let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
let borrow_av =
let ty = borrow_ty in
- let value = ABorrow (AMutBorrow (bid0, mk_aignored meta bv_ty)) in
- mk_typed_avalue meta ty value
+ let value = ABorrow (AMutBorrow (bid0, mk_aignored span bv_ty)) in
+ mk_typed_avalue span ty value
in
let loan_av =
let ty = borrow_ty in
- let value = ALoan (AMutLoan (nbid, mk_aignored meta bv_ty)) in
- mk_typed_avalue meta ty value
+ let value = ALoan (AMutLoan (nbid, mk_aignored span bv_ty)) in
+ mk_typed_avalue span ty value
in
let avalues = [ borrow_av; loan_av ] in
@@ -645,21 +645,21 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(* Generate a fresh symbolic value for the borrowed value *)
let _, bv_ty, kind = ty_as_ref ty in
- let sv = mk_fresh_symbolic_typed_value_from_no_regions_ty meta bv_ty in
+ let sv = mk_fresh_symbolic_typed_value_from_no_regions_ty span bv_ty in
let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
(* Generate the avalues for the abstraction *)
let mk_aborrow (bid : borrow_id) (bv : typed_value) : typed_avalue =
let bv_ty = bv.ty in
- cassert __FILE__ __LINE__ (ty_no_regions bv_ty) meta
+ cassert __FILE__ __LINE__ (ty_no_regions bv_ty) span
"Nested borrows are not supported yet";
- let value = ABorrow (AMutBorrow (bid, mk_aignored meta bv_ty)) in
+ let value = ABorrow (AMutBorrow (bid, mk_aignored span bv_ty)) in
{ value; ty = borrow_ty }
in
let borrows = [ mk_aborrow bid0 bv0; mk_aborrow bid1 bv1 ] in
- let loan = AMutLoan (bid2, mk_aignored meta bv_ty) in
+ let loan = AMutLoan (bid2, mk_aignored span bv_ty) in
(* Note that an aloan has a borrow type *)
let loan : typed_avalue = { value = ALoan loan; ty = borrow_ty } in
@@ -700,7 +700,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
raise (ValueMatchFailure (LoansInRight extra_ids_right));
(* This should always be true if we get here *)
- sanity_check __FILE__ __LINE__ (ids0 = ids1) meta;
+ sanity_check __FILE__ __LINE__ (ids0 = ids1) span;
let ids = ids0 in
(* Return *)
@@ -720,7 +720,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
let id1 = sv1.sv_id in
if id0 = id1 then (
(* Sanity check *)
- sanity_check __FILE__ __LINE__ (sv0 = sv1) meta;
+ sanity_check __FILE__ __LINE__ (sv0 = sv1) span;
(* Return *)
sv0)
else (
@@ -728,7 +728,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
borrows *)
sanity_check __FILE__ __LINE__
(not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty))
- meta;
+ span;
(* TODO: the symbolic values may contain bottoms: we're being conservatice,
and fail (for now) if part of a symbolic value contains a bottom.
A more general approach would be to introduce a symbolic value
@@ -736,8 +736,8 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
sanity_check __FILE__ __LINE__
((not (symbolic_value_has_ended_regions ctx0.ended_regions sv0))
&& not (symbolic_value_has_ended_regions ctx1.ended_regions sv1))
- meta;
- mk_fresh_symbolic_value meta sv0.sv_ty)
+ span;
+ mk_fresh_symbolic_value span sv0.sv_ty)
let match_symbolic_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx)
(left : bool) (sv : symbolic_value) (v : typed_value) : typed_value =
@@ -749,14 +749,14 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
let type_infos = ctx0.type_ctx.type_infos in
cassert __FILE__ __LINE__
(not (ty_has_borrows type_infos sv.sv_ty))
- meta
+ span
"Check that:\n\
\ - there are no borrows in the symbolic value\n\
\ - there are no borrows in the \"regular\" value\n\
\ If there are loans in the regular value, raise an exception.";
cassert __FILE__ __LINE__
(not (ValuesUtils.value_has_borrows type_infos v.value))
- meta
+ span
"Check that:\n\
\ - there are no borrows in the symbolic value\n\
\ - there are no borrows in the \"regular\" value\n\
@@ -778,8 +778,8 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
if
symbolic_value_has_ended_regions ctx0.ended_regions sv
|| bottom_in_value ctx1.ended_regions v
- then mk_bottom meta sv.sv_ty
- else mk_fresh_symbolic_typed_value meta sv.sv_ty
+ then mk_bottom span sv.sv_ty
+ else mk_fresh_symbolic_typed_value span sv.sv_ty
let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool)
(v : typed_value) : typed_value =
@@ -794,7 +794,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
with
| Some (BorrowContent _) ->
(* Can't get there: we only ask for outer *loans* *)
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
| Some (LoanContent lc) -> (
match lc with
| VSharedLoan (ids, _) ->
@@ -812,37 +812,37 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
let destructure_shared_values = true in
let ctx = if value_is_left then ctx0 else ctx1 in
let absl =
- convert_value_to_abstractions meta abs_kind can_end
+ convert_value_to_abstractions span abs_kind can_end
destructure_shared_values ctx v
in
push_absl absl;
(* Return [Bottom] *)
- mk_bottom meta v.ty
+ mk_bottom span v.ty
(* As explained in comments: we don't use the join matcher to join avalues,
only concrete values *)
let match_distinct_aadts _ _ _ _ _ _ _ =
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
let match_ashared_borrows _ _ _ _ _ _ =
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
let match_amut_borrows _ _ _ _ _ _ _ _ _ _ =
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ =
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
let match_amut_loans _ _ _ _ _ _ _ _ _ _ =
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
- let match_avalues _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable"
+ let match_avalues _ _ _ _ = craise __FILE__ __LINE__ span "Unreachable"
end
(* Very annoying: functors only take modules as inputs... *)
module type MatchMoveState = sig
- val meta : Meta.meta
+ val span : Meta.span
(** The current loop *)
val loop_id : LoopId.id
@@ -868,19 +868,19 @@ end
indeed matches the resulting target environment: it will be re-checked later.
*)
module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct
- let meta = S.meta
+ let span = S.span
(** Small utility *)
let push_moved_value (v : typed_value) : unit = S.nvalues := v :: !S.nvalues
let match_etys _ _ ty0 ty1 =
- sanity_check __FILE__ __LINE__ (ty0 = ty1) meta;
+ sanity_check __FILE__ __LINE__ (ty0 = ty1) span;
ty0
let match_rtys _ _ ty0 ty1 =
(* The types must be equal - in effect, this forbids to match symbolic
values containing borrows *)
- sanity_check __FILE__ __LINE__ (ty0 = ty1) meta;
+ sanity_check __FILE__ __LINE__ (ty0 = ty1) span;
ty0
let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
@@ -925,7 +925,7 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct
if
symbolic_value_has_ended_regions ctx0.ended_regions sv
|| bottom_in_value ctx1.ended_regions v
- then mk_bottom meta sv.sv_ty
+ then mk_bottom span sv.sv_ty
else if left then v
else mk_typed_value_from_symbolic_value sv
@@ -941,47 +941,47 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct
with
| Some (BorrowContent _) ->
(* Can't get there: we only ask for outer *loans* *)
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
| Some (LoanContent _) ->
(* We should have ended all the outer loans *)
- craise __FILE__ __LINE__ meta "Unexpected outer loan"
+ craise __FILE__ __LINE__ span "Unexpected outer loan"
| None ->
(* Move the value - note that we shouldn't get there if we
were not allowed to move the value in the first place. *)
push_moved_value v;
(* Return [Bottom] *)
- mk_bottom meta v.ty)
+ mk_bottom span v.ty)
else
(* If we get there it means the source environment (e.g., the
fixed-point) has a non-bottom value, while the target environment
(e.g., the environment we have when we reach the continue)
has bottom: we shouldn't get there. *)
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
(* As explained in comments: we don't use the join matcher to join avalues,
only concrete values *)
let match_distinct_aadts _ _ _ _ _ _ _ =
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
let match_ashared_borrows _ _ _ _ _ _ =
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
let match_amut_borrows _ _ _ _ _ _ _ _ _ =
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ =
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
let match_amut_loans _ _ _ _ _ _ _ _ _ _ =
- craise __FILE__ __LINE__ meta "Unreachable"
+ craise __FILE__ __LINE__ span "Unreachable"
- let match_avalues _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable"
+ let match_avalues _ _ _ _ = craise __FILE__ __LINE__ span "Unreachable"
end
module MakeCheckEquivMatcher (S : MatchCheckEquivState) : CheckEquivMatcher =
struct
- let meta = S.meta
+ let span = S.span
module MkGetSetM (Id : Identifiers.Id) = struct
module Inj = Id.InjSubst
@@ -1081,11 +1081,11 @@ struct
RFVar rid
| _ -> raise (Distinct "match_rtys")
in
- match_types meta match_distinct_types match_regions ty0 ty1
+ match_types span match_distinct_types match_regions ty0 ty1
let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
(_ : literal) (_ : literal) : typed_value =
- mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty
+ mk_fresh_symbolic_typed_value_from_no_regions_ty span ty
let match_distinct_adts (_ : eval_ctx) (_ : eval_ctx) (_ty : ety)
(_adt0 : adt_value) (_adt1 : adt_value) : typed_value =
@@ -1112,9 +1112,9 @@ struct
(lazy
("MakeCheckEquivMatcher: match_shared_borrows: looked up values:"
^ "sv0: "
- ^ typed_value_to_string ~meta:(Some meta) ctx0 v0
+ ^ typed_value_to_string ~span:(Some span) ctx0 v0
^ ", sv1: "
- ^ typed_value_to_string ~meta:(Some meta) ctx1 v1));
+ ^ typed_value_to_string ~span:(Some span) ctx1 v1));
let _ = match_typed_values v0 v1 in
()
@@ -1163,7 +1163,7 @@ struct
(* Check: fixed values are fixed *)
sanity_check __FILE__ __LINE__
(id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map))
- meta;
+ span;
(* Update the symbolic value mapping *)
let sv1 = mk_typed_value_from_symbolic_value sv1 in
@@ -1180,12 +1180,12 @@ struct
(sv : symbolic_value) (v : typed_value) : typed_value =
if S.check_equiv then raise (Distinct "match_symbolic_with_other")
else (
- sanity_check __FILE__ __LINE__ left meta;
+ sanity_check __FILE__ __LINE__ left span;
let id = sv.sv_id in
(* Check: fixed values are fixed *)
sanity_check __FILE__ __LINE__
(not (SymbolicValueId.InjSubst.mem id !S.sid_map))
- meta;
+ span;
(* Update the binding for the target symbolic value *)
S.sid_to_value_map :=
SymbolicValueId.Map.add_strict id v !S.sid_to_value_map;
@@ -1202,7 +1202,7 @@ struct
let value_is_left = not left in
let ctx = if value_is_left then ctx0 else ctx1 in
if left && not (value_has_loans_or_borrows ctx v.value) then
- mk_bottom meta v.ty
+ mk_bottom span v.ty
else
raise
(Distinct
@@ -1238,7 +1238,7 @@ struct
("MakeCheckEquivMatcher:match_amut_loans:" ^ "\n- id0: "
^ BorrowId.to_string id0 ^ "\n- id1: " ^ BorrowId.to_string id1
^ "\n- ty: " ^ ty_to_string ctx0 ty ^ "\n- av: "
- ^ typed_avalue_to_string ~meta:(Some meta) ctx1 av));
+ ^ typed_avalue_to_string ~span:(Some span) ctx1 av));
let id = match_loan_id id0 id1 in
let value = ALoan (AMutLoan (id, av)) in
@@ -1248,13 +1248,13 @@ struct
log#ldebug
(lazy
("avalues don't match:\n- v0: "
- ^ typed_avalue_to_string ~meta:(Some meta) ctx0 v0
+ ^ typed_avalue_to_string ~span:(Some span) ctx0 v0
^ "\n- v1: "
- ^ typed_avalue_to_string ~meta:(Some meta) ctx1 v1));
+ ^ typed_avalue_to_string ~span:(Some span) ctx1 v1));
raise (Distinct "match_avalues")
end
-let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
+let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets)
(lookup_shared_value_in_ctx0 : BorrowId.id -> typed_value)
(lookup_shared_value_in_ctx1 : BorrowId.id -> typed_value) (ctx0 : eval_ctx)
(ctx1 : eval_ctx) : ids_maps option =
@@ -1262,9 +1262,9 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
(lazy
("match_ctxs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids
^ "\n\n- ctx0:\n"
- ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx0
+ ^ eval_ctx_to_string_no_filter ~span:(Some span) ctx0
^ "\n\n- ctx1:\n"
- ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx1
+ ^ eval_ctx_to_string_no_filter ~span:(Some span) ctx1
^ "\n\n"));
(* Initialize the maps and instantiate the matcher *)
@@ -1306,7 +1306,7 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
in
let module S : MatchCheckEquivState = struct
- let meta = meta
+ let span = span
let check_equiv = check_equiv
let rid_map = rid_map
let blid_map = blid_map
@@ -1394,10 +1394,10 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
^ "\n- aid_map: "
^ AbstractionId.InjSubst.show_t !aid_map
^ "\n\n- ctx0:\n"
- ^ eval_ctx_to_string_no_filter ~meta:(Some meta)
+ ^ eval_ctx_to_string_no_filter ~span:(Some span)
{ ctx0 with env = List.rev env0 }
^ "\n\n- ctx1:\n"
- ^ eval_ctx_to_string_no_filter ~meta:(Some meta)
+ ^ eval_ctx_to_string_no_filter ~span:(Some span)
{ ctx1 with env = List.rev env1 }
^ "\n\n"));
@@ -1407,19 +1407,19 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
be the same and their values equal (and the borrows/loans/symbolic *)
if DummyVarId.Set.mem b0 fixed_ids.dids then (
(* Fixed values: the values must be equal *)
- sanity_check __FILE__ __LINE__ (b0 = b1) meta;
- sanity_check __FILE__ __LINE__ (v0 = v1) meta;
+ sanity_check __FILE__ __LINE__ (b0 = b1) span;
+ sanity_check __FILE__ __LINE__ (v0 = v1) span;
(* The ids present in the left value must be fixed *)
let ids, _ = compute_typed_value_ids v0 in
sanity_check __FILE__ __LINE__
((not S.check_equiv) || ids_are_fixed ids)
- meta);
+ span);
(* We still match the values - allows to compute mappings (which
are the identity actually) *)
let _ = M.match_typed_values ctx0 ctx1 v0 v1 in
match_envs env0' env1'
| EBinding (BVar b0, v0) :: env0', EBinding (BVar b1, v1) :: env1' ->
- sanity_check __FILE__ __LINE__ (b0 = b1) meta;
+ sanity_check __FILE__ __LINE__ (b0 = b1) span;
(* Match the values *)
let _ = M.match_typed_values ctx0 ctx1 v0 v1 in
(* Continue *)
@@ -1430,12 +1430,12 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then (
log#ldebug (lazy "match_ctxs: match_envs: matching abs: fixed abs");
(* Still in the prefix: the abstractions must be the same *)
- sanity_check __FILE__ __LINE__ (abs0 = abs1) meta;
+ sanity_check __FILE__ __LINE__ (abs0 = abs1) span;
(* Their ids must be fixed *)
let ids, _ = compute_abs_ids abs0 in
sanity_check __FILE__ __LINE__
((not S.check_equiv) || ids_are_fixed ids)
- meta;
+ span;
(* Continue *)
match_envs env0' env1')
else (
@@ -1463,7 +1463,7 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
let env0, env1 =
match (env0, env1) with
| EFrame :: env0, EFrame :: env1 -> (env0, env1)
- | _ -> craise __FILE__ __LINE__ meta "Unreachable"
+ | _ -> craise __FILE__ __LINE__ span "Unreachable"
in
match_envs env0 env1;
@@ -1490,15 +1490,15 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
^ "\n"));
None
-let ctxs_are_equivalent (meta : Meta.meta) (fixed_ids : ids_sets)
+let ctxs_are_equivalent (span : Meta.span) (fixed_ids : ids_sets)
(ctx0 : eval_ctx) (ctx1 : eval_ctx) : bool =
let check_equivalent = true in
- let lookup_shared_value _ = craise __FILE__ __LINE__ meta "Unreachable" in
+ let lookup_shared_value _ = craise __FILE__ __LINE__ span "Unreachable" in
Option.is_some
- (match_ctxs meta check_equivalent fixed_ids lookup_shared_value
+ (match_ctxs span check_equivalent fixed_ids lookup_shared_value
lookup_shared_value ctx0 ctx1)
-let prepare_match_ctx_with_target (config : config) (meta : Meta.meta)
+let prepare_match_ctx_with_target (config : config) (span : Meta.span)
(loop_id : LoopId.id) (fixed_ids : ids_sets) (src_ctx : eval_ctx) : cm_fun =
fun tgt_ctx ->
(* Debug *)
@@ -1506,25 +1506,25 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta)
(lazy
("prepare_match_ctx_with_target:\n" ^ "\n- fixed_ids: "
^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: "
- ^ eval_ctx_to_string ~meta:(Some meta) src_ctx
+ ^ eval_ctx_to_string ~span:(Some span) src_ctx
^ "\n- tgt_ctx: "
- ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx));
+ ^ eval_ctx_to_string ~span:(Some span) tgt_ctx));
(* End the loans which lead to mismatches when joining *)
let rec reorganize_join_tgt : cm_fun =
fun tgt_ctx ->
(* Collect fixed values in the source and target contexts: end the loans in the
source context which don't appear in the target context *)
- let filt_src_env, _, _ = ctx_split_fixed_new meta fixed_ids src_ctx in
- let filt_tgt_env, _, _ = ctx_split_fixed_new meta fixed_ids tgt_ctx in
+ let filt_src_env, _, _ = ctx_split_fixed_new span fixed_ids src_ctx in
+ let filt_tgt_env, _, _ = ctx_split_fixed_new span fixed_ids tgt_ctx in
log#ldebug
(lazy
("prepare_match_ctx_with_target: reorganize_join_tgt:\n"
^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids ^ "\n"
^ "\n- filt_src_ctx: "
- ^ env_to_string meta src_ctx filt_src_env
+ ^ env_to_string span src_ctx filt_src_env
^ "\n- filt_tgt_ctx: "
- ^ env_to_string meta tgt_ctx filt_tgt_env));
+ ^ env_to_string span tgt_ctx filt_tgt_env));
(* Remove the abstractions *)
let filter (ee : env_elem) : bool =
@@ -1537,7 +1537,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta)
let nabs = ref [] in
let module S : MatchJoinState = struct
- let meta = meta
+ let span = span
let loop_id = loop_id
let nabs = nabs
end in
@@ -1549,14 +1549,14 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta)
(fun (var0, var1) ->
match (var0, var1) with
| EBinding (BDummy b0, v0), EBinding (BDummy b1, v1) ->
- sanity_check __FILE__ __LINE__ (b0 = b1) meta;
+ sanity_check __FILE__ __LINE__ (b0 = b1) span;
let _ = M.match_typed_values src_ctx tgt_ctx v0 v1 in
()
| EBinding (BVar b0, v0), EBinding (BVar b1, v1) ->
- sanity_check __FILE__ __LINE__ (b0 = b1) meta;
+ sanity_check __FILE__ __LINE__ (b0 = b1) span;
let _ = M.match_typed_values src_ctx tgt_ctx v0 v1 in
()
- | _ -> craise __FILE__ __LINE__ meta "Unexpected")
+ | _ -> craise __FILE__ __LINE__ span "Unexpected")
(List.combine filt_src_env filt_tgt_env)
in
(* No exception was thrown: continue *)
@@ -1565,9 +1565,9 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta)
("prepare_match_ctx_with_target: reorganize_join_tgt: done with \
borrows/loans:\n" ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids
^ "\n" ^ "\n- filt_src_ctx: "
- ^ env_to_string meta src_ctx filt_src_env
+ ^ env_to_string span src_ctx filt_src_env
^ "\n- filt_tgt_ctx: "
- ^ env_to_string meta tgt_ctx filt_tgt_env));
+ ^ env_to_string span tgt_ctx filt_tgt_env));
(* We are done with the borrows/loans: now make sure we move all
the values which are bottom in the src environment (i.e., the
@@ -1576,7 +1576,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta)
environment *)
let nvalues = ref [] in
let module S : MatchMoveState = struct
- let meta = meta
+ let span = span
let loop_id = loop_id
let nvalues = nvalues
end in
@@ -1587,14 +1587,14 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta)
(fun (var0, var1) ->
match (var0, var1) with
| EBinding (BDummy b0, v0), EBinding ((BDummy b1 as var1), v1) ->
- sanity_check __FILE__ __LINE__ (b0 = b1) meta;
+ sanity_check __FILE__ __LINE__ (b0 = b1) span;
let v = M.match_typed_values src_ctx tgt_ctx v0 v1 in
(var1, v)
| EBinding (BVar b0, v0), EBinding ((BVar b1 as var1), v1) ->
- sanity_check __FILE__ __LINE__ (b0 = b1) meta;
+ sanity_check __FILE__ __LINE__ (b0 = b1) span;
let v = M.match_typed_values src_ctx tgt_ctx v0 v1 in
(var1, v)
- | _ -> craise __FILE__ __LINE__ meta "Unexpected")
+ | _ -> craise __FILE__ __LINE__ span "Unexpected")
(List.combine filt_src_env filt_tgt_env)
in
let var_to_new_val = BinderMap.of_list var_to_new_val in
@@ -1623,9 +1623,9 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta)
("prepare_match_ctx_with_target: reorganize_join_tgt: done with \
borrows/loans and moves:\n" ^ "\n- fixed_ids: "
^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: "
- ^ eval_ctx_to_string ~meta:(Some meta) src_ctx
+ ^ eval_ctx_to_string ~span:(Some span) src_ctx
^ "\n- tgt_ctx: "
- ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx));
+ ^ eval_ctx_to_string ~span:(Some span) tgt_ctx));
(tgt_ctx, fun e -> e)
with ValueMatchFailure e ->
@@ -1633,18 +1633,18 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta)
let ctx, cc =
match e with
| LoanInRight bid ->
- InterpreterBorrows.end_borrow config meta bid tgt_ctx
+ InterpreterBorrows.end_borrow config span bid tgt_ctx
| LoansInRight bids ->
- InterpreterBorrows.end_borrows config meta bids tgt_ctx
+ InterpreterBorrows.end_borrows config span bids tgt_ctx
| AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ ->
- craise __FILE__ __LINE__ meta "Unexpected"
+ craise __FILE__ __LINE__ span "Unexpected"
in
comp cc (reorganize_join_tgt ctx)
in
(* Apply the reorganization *)
reorganize_join_tgt tgt_ctx
-let match_ctx_with_target (config : config) (meta : Meta.meta)
+let match_ctx_with_target (config : config) (span : Meta.span)
(loop_id : LoopId.id) (is_loop_entry : bool)
(fp_bl_maps : borrow_loan_corresp)
(fp_input_svalues : SymbolicValueId.id list) (fixed_ids : ids_sets)
@@ -1663,7 +1663,7 @@ let match_ctx_with_target (config : config) (meta : Meta.meta)
were introduced during the loop iterations)
*)
let tgt_ctx, cc =
- prepare_match_ctx_with_target config meta loop_id fixed_ids src_ctx tgt_ctx
+ prepare_match_ctx_with_target config span loop_id fixed_ids src_ctx tgt_ctx
in
(* Introduce the "identity" abstractions for the loop re-entry.
@@ -1691,11 +1691,11 @@ let match_ctx_with_target (config : config) (meta : Meta.meta)
^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string tgt_ctx
));
- let filt_tgt_env, _, _ = ctx_split_fixed_new meta fixed_ids tgt_ctx in
+ let filt_tgt_env, _, _ = ctx_split_fixed_new span fixed_ids tgt_ctx in
let filt_src_env, new_absl, new_dummyl =
- ctx_split_fixed_new meta fixed_ids src_ctx
+ ctx_split_fixed_new span fixed_ids src_ctx
in
- sanity_check __FILE__ __LINE__ (new_dummyl = []) meta;
+ sanity_check __FILE__ __LINE__ (new_dummyl = []) span;
let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in
let filt_src_ctx = { src_ctx with env = filt_src_env } in
@@ -1704,16 +1704,16 @@ let match_ctx_with_target (config : config) (meta : Meta.meta)
let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in
let open InterpreterBorrowsCore in
let lookup_shared_loan lid ctx : typed_value =
- match snd (lookup_loan meta ek_all lid ctx) with
+ match snd (lookup_loan span ek_all lid ctx) with
| Concrete (VSharedLoan (_, v)) -> v
| Abstract (ASharedLoan (_, v, _)) -> v
- | _ -> craise __FILE__ __LINE__ meta "Unreachable"
+ | _ -> craise __FILE__ __LINE__ span "Unreachable"
in
let lookup_in_src id = lookup_shared_loan id src_ctx in
let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in
(* Match *)
Option.get
- (match_ctxs meta check_equiv fixed_ids lookup_in_src lookup_in_tgt
+ (match_ctxs span check_equiv fixed_ids lookup_in_src lookup_in_tgt
filt_src_ctx filt_tgt_ctx)
in
let tgt_to_src_borrow_map =
@@ -1727,15 +1727,15 @@ let match_ctx_with_target (config : config) (meta : Meta.meta)
log#ldebug
(lazy
("match_ctx_with_target: cf_introduce_loop_fp_abs:" ^ "\n\n- src_ctx: "
- ^ eval_ctx_to_string ~meta:(Some meta) src_ctx
+ ^ eval_ctx_to_string ~span:(Some span) src_ctx
^ "\n\n- tgt_ctx: "
- ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx
+ ^ eval_ctx_to_string ~span:(Some span) tgt_ctx
^ "\n\n- filt_tgt_ctx: "
- ^ eval_ctx_to_string_no_filter ~meta:(Some meta) filt_tgt_ctx
+ ^ eval_ctx_to_string_no_filter ~span:(Some span) filt_tgt_ctx
^ "\n\n- filt_src_ctx: "
- ^ eval_ctx_to_string_no_filter ~meta:(Some meta) filt_src_ctx
+ ^ eval_ctx_to_string_no_filter ~span:(Some span) filt_src_ctx
^ "\n\n- new_absl:\n"
- ^ eval_ctx_to_string ~meta:(Some meta)
+ ^ eval_ctx_to_string ~span:(Some span)
{ src_ctx with env = List.map (fun abs -> EAbs abs) new_absl }
^ "\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- fp_bl_maps:\n"
^ show_borrow_loan_corresp fp_bl_maps
@@ -1834,7 +1834,7 @@ let match_ctx_with_target (config : config) (meta : Meta.meta)
values containing borrows to not be eagerly expanded.
*)
sanity_check __FILE__ __LINE__ Config.greedy_expand_symbolics_with_borrows
- meta;
+ span;
(* Update the borrows and loans in the abstractions of the target context.
@@ -1905,7 +1905,7 @@ let match_ctx_with_target (config : config) (meta : Meta.meta)
and because of this, it should actually be mapped to itself *)
sanity_check __FILE__ __LINE__
(BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id)
- meta;
+ span;
id
| Some id -> id
@@ -1917,8 +1917,8 @@ let match_ctx_with_target (config : config) (meta : Meta.meta)
method! visit_abs env abs =
match abs.kind with
| Loop (loop_id', rg_id, kind) ->
- sanity_check __FILE__ __LINE__ (loop_id' = loop_id) meta;
- sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) meta;
+ sanity_check __FILE__ __LINE__ (loop_id' = loop_id) span;
+ sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) span;
let can_end = false in
let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in
let abs = { abs with kind; can_end } in
@@ -1936,18 +1936,18 @@ let match_ctx_with_target (config : config) (meta : Meta.meta)
log#ldebug
(lazy
("match_ctx_with_target: cf_introduce_loop_fp_abs: done:\n- result ctx:\n"
- ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx));
+ ^ eval_ctx_to_string ~span:(Some span) tgt_ctx));
(* Sanity check *)
if !Config.sanity_checks then
- Invariants.check_borrowed_values_invariant meta tgt_ctx;
+ Invariants.check_borrowed_values_invariant span tgt_ctx;
(* End all the borrows which appear in the *new* abstractions *)
let new_borrows =
BorrowId.Set.of_list
(List.map snd (BorrowId.Map.bindings !src_fresh_borrows_map))
in
let tgt_ctx, cc =
- comp cc (InterpreterBorrows.end_borrows config meta new_borrows tgt_ctx)
+ comp cc (InterpreterBorrows.end_borrows config span new_borrows tgt_ctx)
in
(* Compute the loop input values *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-21 03:57:42 +0000