diff options
Diffstat (limited to 'compiler/InterpreterLoopsMatchCtxs.ml')
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 326 |
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 *) |