diff options
Diffstat (limited to 'compiler/InterpreterLoopsMatchCtxs.ml')
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 853 |
1 files changed, 426 insertions, 427 deletions
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 3db68f5d..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,40 +1490,41 @@ 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 cf tgt_ctx -> + fun tgt_ctx -> (* Debug *) log#ldebug (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 cf_reorganize_join_tgt : cm_fun = - fun cf tgt_ctx -> + 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 - ("cf_reorganize_join_tgt: match_ctx_with_target:\n" ^ "\n- fixed_ids: " - ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- filt_src_ctx: " - ^ env_to_string meta src_ctx filt_src_env + ("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 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 = @@ -1536,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 @@ -1548,25 +1549,25 @@ 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 *) log#ldebug (lazy - ("cf_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 + ("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 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 @@ -1575,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 @@ -1586,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 @@ -1619,33 +1620,36 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) log#ldebug (lazy - ("cf_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 + ("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 ~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)); - cf tgt_ctx + (tgt_ctx, fun e -> e) with ValueMatchFailure e -> (* Exception: end the corresponding borrows, and continue *) - let cc = + let ctx, cc = match e with - | LoanInRight bid -> InterpreterBorrows.end_borrow config meta bid - | LoansInRight bids -> InterpreterBorrows.end_borrows config meta bids + | LoanInRight bid -> + InterpreterBorrows.end_borrow config span bid tgt_ctx + | LoansInRight bids -> + 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 cf_reorganize_join_tgt cf tgt_ctx + comp cc (reorganize_join_tgt ctx) in (* Apply the reorganization *) - cf_reorganize_join_tgt cf tgt_ctx + 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) (src_ctx : eval_ctx) : st_cm_fun = - fun cf tgt_ctx -> + fun tgt_ctx -> (* Debug *) log#ldebug (lazy @@ -1658,8 +1662,8 @@ let match_ctx_with_target (config : config) (meta : Meta.meta) context, which results from joins during which we ended the loans which were introduced during the loop iterations) *) - let cf_reorganize_join_tgt = - prepare_match_ctx_with_target config meta loop_id fixed_ids src_ctx + let tgt_ctx, cc = + 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. @@ -1679,290 +1683,285 @@ let match_ctx_with_target (config : config) (meta : Meta.meta) We should rely on a more primitive and safer function [add_identity_abs] to add the identity abstractions one by one. *) - let cf_introduce_loop_fp_abs : m_fun = - fun tgt_ctx -> - (* Match the source and target contexts *) - log#ldebug - (lazy - ("cf_introduce_loop_fp_abs:\n" ^ "\n- fixed_ids: " - ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: " - ^ 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_src_env, new_absl, new_dummyl = - ctx_split_fixed_new meta fixed_ids src_ctx - in - sanity_check __FILE__ __LINE__ (new_dummyl = []) meta; - let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in - let filt_src_ctx = { src_ctx with env = filt_src_env } in - - let src_to_tgt_maps = - let check_equiv = false in - 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 - | Concrete (VSharedLoan (_, v)) -> v - | Abstract (ASharedLoan (_, v, _)) -> v - | _ -> craise __FILE__ __LINE__ meta "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 - filt_src_ctx filt_tgt_ctx) - in - let tgt_to_src_borrow_map = - BorrowId.Map.of_list - (List.map - (fun (x, y) -> (y, x)) - (BorrowId.InjSubst.bindings src_to_tgt_maps.borrow_id_map)) + (* Match the source and target contexts *) + log#ldebug + (lazy + ("cf_introduce_loop_fp_abs:\n" ^ "\n- fixed_ids: " + ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: " + ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string tgt_ctx + )); + + 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 span fixed_ids src_ctx + in + 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 + + let src_to_tgt_maps = + let check_equiv = false in + 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 span ek_all lid ctx) with + | Concrete (VSharedLoan (_, v)) -> v + | Abstract (ASharedLoan (_, v, _)) -> v + | _ -> 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 span check_equiv fixed_ids lookup_in_src lookup_in_tgt + filt_src_ctx filt_tgt_ctx) + in + let tgt_to_src_borrow_map = + BorrowId.Map.of_list + (List.map + (fun (x, y) -> (y, x)) + (BorrowId.InjSubst.bindings src_to_tgt_maps.borrow_id_map)) + in - (* Debug *) - 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 - ^ "\n\n- tgt_ctx: " - ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx - ^ "\n\n- filt_tgt_ctx: " - ^ eval_ctx_to_string_no_filter ~meta:(Some meta) filt_tgt_ctx - ^ "\n\n- filt_src_ctx: " - ^ eval_ctx_to_string_no_filter ~meta:(Some meta) filt_src_ctx - ^ "\n\n- new_absl:\n" - ^ eval_ctx_to_string ~meta:(Some meta) - { 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 - ^ "\n\n- src_to_tgt_maps: " - ^ show_ids_maps src_to_tgt_maps)); - - (* Update the borrows and symbolic ids in the source context. - - Going back to the [list_nth_mut_example], the original environment upon - re-entering the loop is: - - {[ + (* Debug *) + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs:" ^ "\n\n- src_ctx: " + ^ eval_ctx_to_string ~span:(Some span) src_ctx + ^ "\n\n- tgt_ctx: " + ^ eval_ctx_to_string ~span:(Some span) tgt_ctx + ^ "\n\n- 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 ~span:(Some span) filt_src_ctx + ^ "\n\n- new_absl:\n" + ^ 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 + ^ "\n\n- src_to_tgt_maps: " + ^ show_ids_maps src_to_tgt_maps)); + + (* Update the borrows and symbolic ids in the source context. + + Going back to the [list_nth_mut_example], the original environment upon + re-entering the loop is: + + {[ + abs@0 { ML l0 } + ls -> MB l5 (s@6 : loops::List<T>) + i -> s@7 : u32 + _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) + _@2 -> MB l2 (@Box (ML l4)) // tail + _@3 -> MB l1 (s@3 : T) // hd + abs@1 { MB l4, ML l5 } + ]} + + The fixed-point environment is: + {[ + env_fp = { abs@0 { ML l0 } - ls -> MB l5 (s@6 : loops::List<T>) - i -> s@7 : u32 - _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) - _@2 -> MB l2 (@Box (ML l4)) // tail - _@3 -> MB l1 (s@3 : T) // hd - abs@1 { MB l4, ML l5 } - ]} - - The fixed-point environment is: - {[ - env_fp = { - abs@0 { ML l0 } - ls -> MB l1 (s3 : loops::List<T>) - i -> s4 : u32 - abs@fp { - MB l0 // this borrow appears in [env0] - ML l1 - } + ls -> MB l1 (s3 : loops::List<T>) + i -> s4 : u32 + abs@fp { + MB l0 // this borrow appears in [env0] + ML l1 } - ]} + } + ]} + + Through matching, we detect that in [env_fp], [l1] is matched + to [l5]. We introduce a fresh borrow [l6] for [l1], and remember + in the map [src_fresh_borrows_map] that: [{ l1 -> l6}]. + + We get: + {[ + abs@0 { ML l0 } + ls -> MB l6 (s@6 : loops::List<T>) // l6 is fresh and doesn't have a corresponding loan + i -> s@7 : u32 + _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) + _@2 -> MB l2 (@Box (ML l4)) // tail + _@3 -> MB l1 (s@3 : T) // hd + abs@1 { MB l4, ML l5 } + ]} + + Later, we will introduce the identity abstraction: + {[ + abs@2 { MB l5, ML l6 } + ]} + *) + (* First, compute the set of borrows which appear in the fresh abstractions + of the fixed-point: we want to introduce fresh ids only for those. *) + let new_absl_ids, _ = compute_absl_ids new_absl in + let src_fresh_borrows_map = ref BorrowId.Map.empty in + let visit_tgt = + object + inherit [_] map_eval_ctx + + method! visit_borrow_id _ id = + (* Map the borrow, if it needs to be mapped *) + if + (* We map the borrows for which we computed a mapping *) + BorrowId.InjSubst.Set.mem id + (BorrowId.InjSubst.elements src_to_tgt_maps.borrow_id_map) + (* And which have corresponding loans in the fresh fixed-point abstractions *) + && BorrowId.Set.mem + (BorrowId.Map.find id tgt_to_src_borrow_map) + new_absl_ids.loan_ids + then ( + let src_id = BorrowId.Map.find id tgt_to_src_borrow_map in + let nid = fresh_borrow_id () in + src_fresh_borrows_map := + BorrowId.Map.add src_id nid !src_fresh_borrows_map; + nid) + else id + end + in - Through matching, we detect that in [env_fp], [l1] is matched - to [l5]. We introduce a fresh borrow [l6] for [l1], and remember - in the map [src_fresh_borrows_map] that: [{ l1 -> l6}]. + let tgt_ctx = visit_tgt#visit_eval_ctx () tgt_ctx in - We get: - {[ - abs@0 { ML l0 } - ls -> MB l6 (s@6 : loops::List<T>) // l6 is fresh and doesn't have a corresponding loan - i -> s@7 : u32 - _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) - _@2 -> MB l2 (@Box (ML l4)) // tail - _@3 -> MB l1 (s@3 : T) // hd - abs@1 { MB l4, ML l5 } - ]} - - Later, we will introduce the identity abstraction: - {[ - abs@2 { MB l5, ML l6 } - ]} - *) - (* First, compute the set of borrows which appear in the fresh abstractions - of the fixed-point: we want to introduce fresh ids only for those. *) - let new_absl_ids, _ = compute_absl_ids new_absl in - let src_fresh_borrows_map = ref BorrowId.Map.empty in - let visit_tgt = - object - inherit [_] map_eval_ctx - - method! visit_borrow_id _ id = - (* Map the borrow, if it needs to be mapped *) - if - (* We map the borrows for which we computed a mapping *) - BorrowId.InjSubst.Set.mem id - (BorrowId.InjSubst.elements src_to_tgt_maps.borrow_id_map) - (* And which have corresponding loans in the fresh fixed-point abstractions *) - && BorrowId.Set.mem - (BorrowId.Map.find id tgt_to_src_borrow_map) - new_absl_ids.loan_ids - then ( - let src_id = BorrowId.Map.find id tgt_to_src_borrow_map in - let nid = fresh_borrow_id () in - src_fresh_borrows_map := - BorrowId.Map.add src_id nid !src_fresh_borrows_map; - nid) - else id - end - in - let tgt_ctx = visit_tgt#visit_eval_ctx () tgt_ctx in + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: src_fresh_borrows_map:\n" + ^ BorrowId.Map.show BorrowId.to_string !src_fresh_borrows_map + ^ "\n")); - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ - src_fresh_borrows_map:\n" - ^ BorrowId.Map.show BorrowId.to_string !src_fresh_borrows_map - ^ "\n")); + (* Rem.: we don't update the symbolic values. It is not necessary + because there shouldn't be any symbolic value containing borrows. - (* Rem.: we don't update the symbolic values. It is not necessary - because there shouldn't be any symbolic value containing borrows. + Rem.: we will need to do something about the symbolic values in the + abstractions and in the *variable bindings* once we allow symbolic + values containing borrows to not be eagerly expanded. + *) + sanity_check __FILE__ __LINE__ Config.greedy_expand_symbolics_with_borrows + span; + + (* Update the borrows and loans in the abstractions of the target context. + + Going back to the [list_nth_mut] example and by using [src_fresh_borrows_map], + we instantiate the fixed-point abstractions that we will insert into the + context. + The abstraction is [abs { MB l0, ML l1 }]. + Because of [src_fresh_borrows_map], we substitute [l1] with [l6]. + Because of the match between the contexts, we substitute [l0] with [l5]. + We get: + {[ + abs@2 { MB l5, ML l6 } + ]} + *) + let region_id_map = ref RegionId.Map.empty in + let get_rid rid = + match RegionId.Map.find_opt rid !region_id_map with + | Some rid -> rid + | None -> + let nid = fresh_region_id () in + region_id_map := RegionId.Map.add rid nid !region_id_map; + nid + in + let visit_src = + object + inherit [_] map_eval_ctx as super - Rem.: we will need to do something about the symbolic values in the - abstractions and in the *variable bindings* once we allow symbolic - values containing borrows to not be eagerly expanded. - *) - sanity_check __FILE__ __LINE__ Config.greedy_expand_symbolics_with_borrows - meta; - - (* Update the borrows and loans in the abstractions of the target context. - - Going back to the [list_nth_mut] example and by using [src_fresh_borrows_map], - we instantiate the fixed-point abstractions that we will insert into the - context. - The abstraction is [abs { MB l0, ML l1 }]. - Because of [src_fresh_borrows_map], we substitute [l1] with [l6]. - Because of the match between the contexts, we substitute [l0] with [l5]. - We get: - {[ - abs@2 { MB l5, ML l6 } - ]} - *) - let region_id_map = ref RegionId.Map.empty in - let get_rid rid = - match RegionId.Map.find_opt rid !region_id_map with - | Some rid -> rid - | None -> - let nid = fresh_region_id () in - region_id_map := RegionId.Map.add rid nid !region_id_map; - nid - in - let visit_src = - object - inherit [_] map_eval_ctx as super + method! visit_borrow_id _ bid = + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ + visit_borrow_id: " ^ BorrowId.to_string bid ^ "\n")); - method! visit_borrow_id _ bid = - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ - visit_borrow_id: " ^ BorrowId.to_string bid ^ "\n")); + (* Lookup the id of the loan corresponding to this borrow *) + let src_lid = + BorrowId.InjSubst.find bid fp_bl_maps.borrow_to_loan_id_map + in - (* Lookup the id of the loan corresponding to this borrow *) - let src_lid = - BorrowId.InjSubst.find bid fp_bl_maps.borrow_to_loan_id_map - in + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ + src_lid: " ^ BorrowId.to_string src_lid ^ "\n")); - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ - src_lid: " ^ BorrowId.to_string src_lid ^ "\n")); + (* Lookup the tgt borrow id to which this borrow was mapped *) + let tgt_bid = + BorrowId.InjSubst.find src_lid src_to_tgt_maps.borrow_id_map + in - (* Lookup the tgt borrow id to which this borrow was mapped *) - let tgt_bid = - BorrowId.InjSubst.find src_lid src_to_tgt_maps.borrow_id_map - in + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ + tgt_bid: " ^ BorrowId.to_string tgt_bid ^ "\n")); - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ - tgt_bid: " ^ BorrowId.to_string tgt_bid ^ "\n")); + tgt_bid - tgt_bid + method! visit_loan_id _ id = + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: visit_loan_id: " + ^ BorrowId.to_string id ^ "\n")); + (* Map the borrow - rem.: we mapped the borrows *in the values*, + meaning we know how to map the *corresponding loans in the + abstractions* *) + match BorrowId.Map.find_opt id !src_fresh_borrows_map with + | None -> + (* No mapping: this means that the borrow was mapped when + we matched values (it doesn't come from a fresh abstraction) + 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) + span; + id + | Some id -> id + + method! visit_symbolic_value_id _ _ = fresh_symbolic_value_id () + method! visit_abstraction_id _ _ = fresh_abstraction_id () + method! visit_region_id _ id = get_rid id + + (** We also need to change the abstraction kind *) + method! visit_abs env abs = + match abs.kind with + | Loop (loop_id', rg_id, kind) -> + 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 + super#visit_abs env abs + | _ -> super#visit_abs env abs + end + in + let new_absl = List.map (visit_src#visit_abs ()) new_absl in + let new_absl = List.map (fun abs -> EAbs abs) new_absl in - method! visit_loan_id _ id = - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ - visit_loan_id: " ^ BorrowId.to_string id ^ "\n")); - (* Map the borrow - rem.: we mapped the borrows *in the values*, - meaning we know how to map the *corresponding loans in the - abstractions* *) - match BorrowId.Map.find_opt id !src_fresh_borrows_map with - | None -> - (* No mapping: this means that the borrow was mapped when - we matched values (it doesn't come from a fresh abstraction) - 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; - id - | Some id -> id - - method! visit_symbolic_value_id _ _ = fresh_symbolic_value_id () - method! visit_abstraction_id _ _ = fresh_abstraction_id () - method! visit_region_id _ id = get_rid id - - (** We also need to change the abstraction kind *) - 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; - let can_end = false in - let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in - let abs = { abs with kind; can_end } in - super#visit_abs env abs - | _ -> super#visit_abs env abs - end - in - let new_absl = List.map (visit_src#visit_abs ()) new_absl in - let new_absl = List.map (fun abs -> EAbs abs) new_absl in + (* Add the abstractions from the target context to the source context *) + let nenv = List.append new_absl tgt_ctx.env in + let tgt_ctx = { tgt_ctx with env = nenv } in - (* Add the abstractions from the target context to the source context *) - let nenv = List.append new_absl tgt_ctx.env in - let tgt_ctx = { tgt_ctx with env = nenv } in + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: done:\n- result ctx:\n" + ^ eval_ctx_to_string ~span:(Some span) tgt_ctx)); + + (* Sanity check *) + if !Config.sanity_checks then + 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 span new_borrows tgt_ctx) + in - 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)); - - (* Sanity check *) - if !Config.sanity_checks then - Invariants.check_borrowed_values_invariant meta 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 cc = InterpreterBorrows.end_borrows config meta new_borrows in - - (* Compute the loop input values *) - let input_values = - SymbolicValueId.Map.of_list - (List.map - (fun sid -> - (sid, SymbolicValueId.Map.find sid src_to_tgt_maps.sid_to_value_map)) - fp_input_svalues) - in + (* Compute the loop input values *) + let input_values = + SymbolicValueId.Map.of_list + (List.map + (fun sid -> + (sid, SymbolicValueId.Map.find sid src_to_tgt_maps.sid_to_value_map)) + fp_input_svalues) + in - (* Continue *) - cc - (cf - (if is_loop_entry then EndEnterLoop (loop_id, input_values) - else EndContinue (loop_id, input_values))) - tgt_ctx + let res = + if is_loop_entry then EndEnterLoop (loop_id, input_values) + else EndContinue (loop_id, input_values) in - (* Compose and continue *) - cf_reorganize_join_tgt cf_introduce_loop_fp_abs tgt_ctx + ((tgt_ctx, res), cc) |