From a64fdc8b1be70de43afe35ff788ba3240318daac Mon Sep 17 00:00:00 2001 From: Escherichia Date: Tue, 12 Mar 2024 15:02:17 +0100 Subject: WIP Beginning working on better errors: began replacing raise (Failure) and assert by craise and cassert. Does not compile yet, still need to propagate the meta variable where it's relevant --- compiler/InterpreterLoopsMatchCtxs.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'compiler/InterpreterLoopsMatchCtxs.ml') diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index dd7bd7a7..67c1155c 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -14,6 +14,7 @@ open InterpreterUtils open InterpreterBorrowsCore open InterpreterBorrows open InterpreterLoopsCore +open Errors module S = SynthesizeSymbolic (** The local logger *) @@ -1400,7 +1401,7 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : eval_ctx) (match_ctxs check_equivalent fixed_ids lookup_shared_value lookup_shared_value ctx0 ctx1) -let prepare_match_ctx_with_target (config : config) (loop_id : LoopId.id) +let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id : LoopId.id) (fixed_ids : ids_sets) (src_ctx : eval_ctx) : cm_fun = fun cf tgt_ctx -> (* Debug *) @@ -1599,7 +1600,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) 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 ek_all lid ctx) with + match snd (lookup_loan meta ek_all lid ctx) with | Concrete (VSharedLoan (_, v)) -> v | Abstract (ASharedLoan (_, v, _)) -> v | _ -> raise (Failure "Unreachable") -- cgit v1.2.3 From 5209cea7012cfa3b39a5a289e65e2ea5e166d730 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 21 Mar 2024 12:34:40 +0100 Subject: WIP: translate.ml and extract.ml do not compile. Some assert left to do and we need to see how translate_crate can give meta to the functions it calls --- compiler/InterpreterLoopsMatchCtxs.ml | 310 +++++++++++++++++----------------- 1 file changed, 151 insertions(+), 159 deletions(-) (limited to 'compiler/InterpreterLoopsMatchCtxs.ml') diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 67c1155c..08d18407 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 (no_duplicates : bool) +let compute_abs_borrows_loans_maps (meta : Meta.meta) (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 @@ -94,7 +94,7 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool) | AIgnoredSharedLoan child -> (* Ignore the id of the loan, if there is *) self#visit_typed_avalue abs_id child - | AEndedMutLoan _ | AEndedSharedLoan _ -> raise (Failure "Unreachable") + | AEndedMutLoan _ | AEndedSharedLoan _ -> craise meta "Unreachable" (** Make sure we don't register the ignored ids *) method! visit_aborrow_content abs_id bc = @@ -108,7 +108,7 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool) (* Ignore the id of the borrow, if there is *) self#visit_typed_avalue abs_id child | AEndedMutBorrow _ | AEndedSharedBorrow -> - raise (Failure "Unreachable") + craise meta "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 @@ -184,9 +184,9 @@ let rec match_types (match_distinct_types : ty -> ty -> ty) | _ -> match_distinct_types ty0 ty1 module MakeMatcher (M : PrimMatcher) : Matcher = struct - let rec match_typed_values (ctx0 : eval_ctx) (ctx1 : eval_ctx) + let rec match_typed_values (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (v0 : typed_value) (v1 : typed_value) : typed_value = - let match_rec = match_typed_values ctx0 ctx1 in + let match_rec = match_typed_values meta ctx0 ctx1 in let ty = M.match_etys ctx0 ctx1 v0.ty v1.ty in (* Using ValuesUtils.value_has_borrows on purpose here: we want to make explicit the fact that, though we have to pick @@ -197,7 +197,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct in match (v0.value, v1.value) with | VLiteral lv0, VLiteral lv1 -> - if lv0 = lv1 then v1 else M.match_distinct_literals ctx0 ctx1 ty lv0 lv1 + if lv0 = lv1 then v1 else M.match_distinct_literals meta ctx0 ctx1 ty lv0 lv1 | VAdt av0, VAdt av1 -> if av0.variant_id = av1.variant_id then let fields = List.combine av0.field_values av1.field_values in @@ -213,14 +213,14 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct assert (not (value_has_borrows v0.value)); assert (not (value_has_borrows v1.value)); (* Merge *) - M.match_distinct_adts ctx0 ctx1 ty av0 av1) + M.match_distinct_adts meta ctx0 ctx1 ty av0 av1) | VBottom, VBottom -> v0 | VBorrow bc0, VBorrow bc1 -> let bc = match (bc0, bc1) with | VSharedBorrow bid0, VSharedBorrow bid1 -> let bid = - M.match_shared_borrows ctx0 ctx1 match_rec ty bid0 bid1 + M.match_shared_borrows meta ctx0 ctx1 match_rec ty bid0 bid1 in VSharedBorrow bid | VMutBorrow (bid0, bv0), VMutBorrow (bid1, bv1) -> @@ -231,7 +231,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)); let bid, bv = - M.match_mut_borrows ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv + M.match_mut_borrows meta ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv in VMutBorrow (bid, bv) | VReservedMutBorrow _, _ @@ -242,7 +242,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 *) - raise (Failure "Unexpected") + craise meta "Unexpected" in { value = VBorrow bc; ty } | VLoan lc0, VLoan lc1 -> @@ -259,7 +259,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let id = M.match_mut_loans ctx0 ctx1 ty id0 id1 in VMutLoan id | VSharedLoan _, VMutLoan _ | VMutLoan _, VSharedLoan _ -> - raise (Failure "Unreachable") + craise meta "Unreachable" in { value = VLoan lc; ty = v1.ty } | VSymbolic sv0, VSymbolic sv1 -> @@ -268,7 +268,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct assert (not (value_has_borrows v0.value)); assert (not (value_has_borrows v1.value)); (* Match *) - let sv = M.match_symbolic_values ctx0 ctx1 sv0 sv1 in + let sv = M.match_symbolic_values meta ctx0 ctx1 sv0 sv1 in { v1 with value = VSymbolic sv } | VLoan lc, _ -> ( match lc with @@ -278,27 +278,27 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct match lc with | VSharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids)) | VMutLoan id -> raise (ValueMatchFailure (LoanInRight id))) - | VSymbolic sv, _ -> M.match_symbolic_with_other ctx0 ctx1 true sv v1 - | _, VSymbolic sv -> M.match_symbolic_with_other ctx0 ctx1 false sv v0 - | VBottom, _ -> M.match_bottom_with_other ctx0 ctx1 true v1 - | _, VBottom -> M.match_bottom_with_other ctx0 ctx1 false v0 + | VSymbolic sv, _ -> M.match_symbolic_with_other meta ctx0 ctx1 true sv v1 + | _, VSymbolic sv -> M.match_symbolic_with_other meta ctx0 ctx1 false sv v0 + | VBottom, _ -> M.match_bottom_with_other meta ctx0 ctx1 true v1 + | _, VBottom -> M.match_bottom_with_other meta ctx0 ctx1 false v0 | _ -> log#ldebug (lazy ("Unexpected match case:\n- value0: " - ^ typed_value_to_string ctx0 v0 + ^ typed_value_to_string meta ctx0 v0 ^ "\n- value1: " - ^ typed_value_to_string ctx1 v1)); - raise (Failure "Unexpected match case") + ^ typed_value_to_string meta ctx1 v1)); + craise meta "Unexpected match case" - and match_typed_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx) + and match_typed_avalues (meta : Meta.meta) (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 ctx0 v0 + ^ typed_avalue_to_string meta ctx0 v0 ^ "\n- value1: " - ^ typed_avalue_to_string ctx1 v1)); + ^ typed_avalue_to_string meta ctx1 v1)); (* Using ValuesUtils.value_has_borrows on purpose here: we want to make explicit the fact that, though we have to pick @@ -308,8 +308,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos in - let match_rec = match_typed_values ctx0 ctx1 in - let match_arec = match_typed_avalues ctx0 ctx1 in + let match_rec = match_typed_values meta ctx0 ctx1 in + let match_arec = match_typed_avalues meta ctx0 ctx1 in let ty = M.match_rtys ctx0 ctx1 v0.ty v1.ty in match (v0.value, v1.value) with | AAdt av0, AAdt av1 -> @@ -323,15 +323,15 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct in { value; ty } else (* Merge *) - M.match_distinct_aadts ctx0 ctx1 v0.ty av0 v1.ty av1 ty - | ABottom, ABottom -> mk_abottom ty - | AIgnored, AIgnored -> mk_aignored ty + M.match_distinct_aadts meta ctx0 ctx1 v0.ty av0 v1.ty av1 ty + | ABottom, ABottom -> mk_abottom meta ty + | AIgnored, AIgnored -> mk_aignored meta ty | ABorrow bc0, ABorrow bc1 -> ( log#ldebug (lazy "match_typed_avalues: borrows"); match (bc0, bc1) with | ASharedBorrow bid0, ASharedBorrow bid1 -> log#ldebug (lazy "match_typed_avalues: shared borrows"); - M.match_ashared_borrows ctx0 ctx1 v0.ty bid0 v1.ty bid1 ty + M.match_ashared_borrows meta ctx0 ctx1 v0.ty bid0 v1.ty bid1 ty | AMutBorrow (bid0, av0), AMutBorrow (bid1, av1) -> log#ldebug (lazy "match_typed_avalues: mut borrows"); log#ldebug @@ -340,10 +340,10 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let av = match_arec av0 av1 in log#ldebug (lazy "match_typed_avalues: mut borrows: matched children values"); - M.match_amut_borrows ctx0 ctx1 v0.ty bid0 av0 v1.ty bid1 av1 ty av + M.match_amut_borrows meta ctx0 ctx1 v0.ty bid0 av0 v1.ty bid1 av1 ty av | AIgnoredMutBorrow _, AIgnoredMutBorrow _ -> (* The abstractions are destructured: we shouldn't get there *) - raise (Failure "Unexpected") + craise meta "Unexpected" | AProjSharedBorrow asb0, AProjSharedBorrow asb1 -> ( match (asb0, asb1) with | [], [] -> @@ -352,7 +352,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct v0 | _ -> (* We should get there only if there are nested borrows *) - raise (Failure "Unexpected")) + craise meta "Unexpected") | _ -> (* TODO: getting there is not necessarily inconsistent (it may just be because the environments don't match) so we may want @@ -363,7 +363,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct we are *currently* ending it, in which case we need to completely end it before continuing. *) - raise (Failure "Unexpected")) + craise meta "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 - @@ -374,7 +374,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let sv = match_rec sv0 sv1 in let av = match_arec av0 av1 in assert (not (value_has_borrows sv.value)); - M.match_ashared_loans ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1 + M.match_ashared_loans meta ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1 av1 ty sv av | AMutLoan (id0, av0), AMutLoan (id1, av1) -> log#ldebug (lazy "match_typed_avalues: mut loans"); @@ -383,18 +383,18 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let av = match_arec av0 av1 in log#ldebug (lazy "match_typed_avalues: mut loans: matched children values"); - M.match_amut_loans ctx0 ctx1 v0.ty id0 av0 v1.ty id1 av1 ty av + M.match_amut_loans meta ctx0 ctx1 v0.ty id0 av0 v1.ty id1 av1 ty av | AIgnoredMutLoan _, AIgnoredMutLoan _ | AIgnoredSharedLoan _, AIgnoredSharedLoan _ -> (* Those should have been filtered when destructuring the abstractions - they are necessary only when there are nested borrows *) - raise (Failure "Unreachable") - | _ -> raise (Failure "Unreachable")) + craise meta "Unreachable" + | _ -> craise meta "Unreachable") | ASymbolic _, ASymbolic _ -> (* For now, we force all the symbolic values containing borrows to be eagerly expanded, and we don't support nested borrows *) - raise (Failure "Unreachable") - | _ -> M.match_avalues ctx0 ctx1 v0 v1 + craise meta "Unreachable" + | _ -> M.match_avalues meta ctx0 ctx1 v0 v1 end module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct @@ -413,11 +413,11 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct assert (ty0 = ty1); ty0 - let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_distinct_literals (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) (_ : literal) (_ : literal) : typed_value = - mk_fresh_symbolic_typed_value_from_no_regions_ty ty + mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty - let match_distinct_adts (ctx0 : eval_ctx) (ctx1 : eval_ctx) (ty : ety) + let match_distinct_adts (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (ty : ety) (adt0 : adt_value) (adt1 : adt_value) : typed_value = (* Check that the ADTs don't contain borrows - this is redundant with checks performed by the caller, but we prefer to be safe with regards to future @@ -447,12 +447,12 @@ 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 ty + then mk_bottom meta ty else (* No borrows, no loans, no bottoms: we can introduce a symbolic value *) - mk_fresh_symbolic_typed_value_from_no_regions_ty ty + mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty - let match_shared_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) match_rec + let match_shared_borrows (meta : Meta.meta) (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 @@ -483,7 +483,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 bv_ty) + ASharedLoan (BorrowId.Set.singleton bid2, sv, mk_aignored meta bv_ty) in (* Note that an aloan has a borrow type *) let loan : typed_avalue = { value = ALoan loan; ty = borrow_ty } in @@ -508,7 +508,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Return the new borrow *) bid2 - let match_mut_borrows (ctx0 : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_mut_borrows (meta : Meta.meta) (ctx0 : eval_ctx) (_ : eval_ctx) (ty : ety) (bid0 : borrow_id) (bv0 : typed_value) (bid1 : borrow_id) (bv1 : typed_value) (bv : typed_value) : borrow_id * typed_value = if bid0 = bid1 then ( @@ -576,14 +576,14 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let borrow_av = let ty = borrow_ty in - let value = ABorrow (AMutBorrow (bid0, mk_aignored bv_ty)) in - mk_typed_avalue ty value + let value = ABorrow (AMutBorrow (bid0, mk_aignored meta bv_ty)) in + mk_typed_avalue meta ty value in let loan_av = let ty = borrow_ty in - let value = ALoan (AMutLoan (nbid, mk_aignored bv_ty)) in - mk_typed_avalue ty value + let value = ALoan (AMutLoan (nbid, mk_aignored meta bv_ty)) in + mk_typed_avalue meta ty value in let avalues = [ borrow_av; loan_av ] in @@ -617,7 +617,7 @@ 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 bv_ty in + let sv = mk_fresh_symbolic_typed_value_from_no_regions_ty meta bv_ty in let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in @@ -625,12 +625,12 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let mk_aborrow (bid : borrow_id) (bv : typed_value) : typed_avalue = let bv_ty = bv.ty in assert (ty_no_regions bv_ty); - let value = ABorrow (AMutBorrow (bid, mk_aignored bv_ty)) in + let value = ABorrow (AMutBorrow (bid, mk_aignored meta 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 bv_ty) in + let loan = AMutLoan (bid2, mk_aignored meta bv_ty) in (* Note that an aloan has a borrow type *) let loan : typed_avalue = { value = ALoan loan; ty = borrow_ty } in @@ -685,7 +685,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct both borrows *) raise (ValueMatchFailure (LoanInLeft id0)) - let match_symbolic_values (ctx0 : eval_ctx) (_ : eval_ctx) + let match_symbolic_values (meta : Meta.meta) (ctx0 : eval_ctx) (_ : eval_ctx) (sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value = let id0 = sv0.sv_id in let id1 = sv1.sv_id in @@ -699,9 +699,9 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct borrows *) assert (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)); (* We simply introduce a fresh symbolic value *) - mk_fresh_symbolic_value sv0.sv_ty) + mk_fresh_symbolic_value meta sv0.sv_ty) - let match_symbolic_with_other (ctx0 : eval_ctx) (_ : eval_ctx) (left : bool) + let match_symbolic_with_other (meta : Meta.meta) (ctx0 : eval_ctx) (_ : eval_ctx) (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = (* Check that: - there are no borrows in the symbolic value @@ -721,9 +721,9 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct if value_is_left then raise (ValueMatchFailure (LoanInLeft id)) else raise (ValueMatchFailure (LoanInRight id))); (* Return a fresh symbolic value *) - mk_fresh_symbolic_typed_value sv.sv_ty + mk_fresh_symbolic_typed_value meta sv.sv_ty - let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) + let match_bottom_with_other (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) (v : typed_value) : typed_value = (* If there are outer loans in the non-bottom value, raise an exception. Otherwise, convert it to an abstraction and return [Bottom]. @@ -736,7 +736,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct with | Some (BorrowContent _) -> (* Can't get there: we only ask for outer *loans* *) - raise (Failure "Unreachable") + craise meta "Unreachable" | Some (LoanContent lc) -> ( match lc with | VSharedLoan (ids, _) -> @@ -754,25 +754,25 @@ 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 abs_kind can_end + convert_value_to_abstractions meta abs_kind can_end destructure_shared_values ctx v in push_absl absl; (* Return [Bottom] *) - mk_bottom v.ty + mk_bottom meta v.ty (* As explained in comments: we don't use the join matcher to join avalues, only concrete values *) - let match_distinct_aadts _ _ _ _ _ _ _ = raise (Failure "Unreachable") - let match_ashared_borrows _ _ _ _ _ _ = raise (Failure "Unreachable") - let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") + let match_distinct_aadts (meta : Meta.meta) _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_ashared_borrows (meta : Meta.meta) _ _ _ _ _ _ = craise meta "Unreachable" + let match_amut_borrows (meta : Meta.meta) _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = - raise (Failure "Unreachable") + let match_ashared_loans (meta: Meta.meta) _ _ _ _ _ _ _ _ _ _ _ _ _ = + craise meta "Unreachable" - let match_amut_loans _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") - let match_avalues _ _ _ _ = raise (Failure "Unreachable") + let match_amut_loans (meta: Meta.meta) _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_avalues (meta: Meta.meta) _ _ _ _ = craise meta "Unreachable" end (* Very annoying: functors only take modules as inputs... *) @@ -814,22 +814,22 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct assert (ty0 = ty1); ty0 - let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_distinct_literals (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) (_ : literal) (l : literal) : typed_value = { value = VLiteral l; ty } - let match_distinct_adts (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_distinct_adts (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) (_ : adt_value) (adt1 : adt_value) : typed_value = (* Note that if there was a bottom inside the ADT on the left, the value on the left should have been simplified to bottom. *) { ty; value = VAdt adt1 } - let match_shared_borrows (_ : eval_ctx) (_ : eval_ctx) _ (_ : ety) + let match_shared_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ (_ : ety) (_ : borrow_id) (bid1 : borrow_id) : borrow_id = (* There can't be bottoms in shared values *) bid1 - let match_mut_borrows (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (_ : borrow_id) + let match_mut_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (_ : borrow_id) (_ : typed_value) (bid1 : borrow_id) (bv1 : typed_value) (_ : typed_value) : borrow_id * typed_value = (* There can't be bottoms in borrowed values *) @@ -845,15 +845,15 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (id1 : loan_id) : loan_id = id1 - let match_symbolic_values (_ : eval_ctx) (_ : eval_ctx) (_ : symbolic_value) + let match_symbolic_values (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : symbolic_value) (sv1 : symbolic_value) : symbolic_value = sv1 - let match_symbolic_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) + let match_symbolic_with_other (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = if left then v else mk_typed_value_from_symbolic_value sv - let match_bottom_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) + let match_bottom_with_other (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (left : bool) (v : typed_value) : typed_value = let with_borrows = false in if left then ( @@ -865,35 +865,35 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct with | Some (BorrowContent _) -> (* Can't get there: we only ask for outer *loans* *) - raise (Failure "Unreachable") + craise meta "Unreachable" | Some (LoanContent _) -> (* We should have ended all the outer loans *) - raise (Failure "Unexpected outer loan") + craise meta "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 v.ty) + mk_bottom meta 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. *) - raise (Failure "Unreachable") + craise meta "Unreachable" (* As explained in comments: we don't use the join matcher to join avalues, only concrete values *) - let match_distinct_aadts _ _ _ _ _ _ _ = raise (Failure "Unreachable") - let match_ashared_borrows _ _ _ _ _ _ = raise (Failure "Unreachable") - let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") + let match_distinct_aadts (meta : Meta.meta) _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_ashared_borrows (meta : Meta.meta) _ _ _ _ _ _ = craise meta "Unreachable" + let match_amut_borrows (meta : Meta.meta) _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = - raise (Failure "Unreachable") + let match_ashared_loans (meta : Meta.meta) _ _ _ _ _ _ _ _ _ _ _ _ _ = + craise meta "Unreachable" - let match_amut_loans _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") - let match_avalues _ _ _ _ = raise (Failure "Unreachable") + let match_amut_loans (meta : Meta.meta) _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_avalues (meta : Meta.meta) _ _ _ _ = craise meta "Unreachable" end module MakeCheckEquivMatcher (S : MatchCheckEquivState) : CheckEquivMatcher = @@ -998,15 +998,15 @@ struct in match_types match_distinct_types match_regions ty0 ty1 - let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_distinct_literals (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) (_ : literal) (_ : literal) : typed_value = - mk_fresh_symbolic_typed_value_from_no_regions_ty ty + mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty - let match_distinct_adts (_ : eval_ctx) (_ : eval_ctx) (_ty : ety) + let match_distinct_adts (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ty : ety) (_adt0 : adt_value) (_adt1 : adt_value) : typed_value = raise (Distinct "match_distinct_adts") - let match_shared_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) + let match_shared_borrows (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (match_typed_values : typed_value -> typed_value -> typed_value) (_ty : ety) (bid0 : borrow_id) (bid1 : borrow_id) : borrow_id = log#ldebug @@ -1027,16 +1027,16 @@ struct (lazy ("MakeCheckEquivMatcher: match_shared_borrows: looked up values:" ^ "sv0: " - ^ typed_value_to_string ctx0 v0 + ^ typed_value_to_string meta ctx0 v0 ^ ", sv1: " - ^ typed_value_to_string ctx1 v1)); + ^ typed_value_to_string meta ctx1 v1)); let _ = match_typed_values v0 v1 in () in bid - let match_mut_borrows (_ : eval_ctx) (_ : eval_ctx) (_ty : ety) + let match_mut_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ty : ety) (bid0 : borrow_id) (_bv0 : typed_value) (bid1 : borrow_id) (_bv1 : typed_value) (bv : typed_value) : borrow_id * typed_value = let bid = match_borrow_id bid0 bid1 in @@ -1052,7 +1052,7 @@ struct (bid1 : loan_id) : loan_id = match_loan_id bid0 bid1 - let match_symbolic_values (ctx0 : eval_ctx) (ctx1 : eval_ctx) + let match_symbolic_values (_ : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value = let id0 = sv0.sv_id in let id1 = sv1.sv_id in @@ -1089,7 +1089,7 @@ struct we want *) sv0) - let match_symbolic_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) + let match_symbolic_with_other (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = if S.check_equiv then raise (Distinct "match_symbolic_with_other") else ( @@ -1103,7 +1103,7 @@ struct (* Return - the returned value is not used, so we can return whatever we want *) v) - let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) + let match_bottom_with_other (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) (v : typed_value) : typed_value = (* It can happen that some variables get initialized in some branches and not in some others, which causes problems when matching. *) @@ -1112,7 +1112,7 @@ struct a continue, where the fixed point contains some bottom values. *) 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 v.ty + if left && not (value_has_loans_or_borrows ctx v.value) then mk_bottom meta v.ty else raise (Distinct @@ -1120,51 +1120,51 @@ struct ^ Print.bool_to_string left ^ "\n- value to match with bottom:\n" ^ show_typed_value v)) - let match_distinct_aadts _ _ _ _ _ _ _ = + let match_distinct_aadts _ _ _ _ _ _ _ _ = raise (Distinct "match_distinct_adts") - let match_ashared_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _ty1 bid1 ty + let match_ashared_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _ty1 bid1 ty = let bid = match_borrow_id bid0 bid1 in let value = ABorrow (ASharedBorrow bid) in { value; ty } - let match_amut_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _av0 _ty1 bid1 + let match_amut_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _av0 _ty1 bid1 _av1 ty av = let bid = match_borrow_id bid0 bid1 in let value = ABorrow (AMutBorrow (bid, av)) in { value; ty } - let match_ashared_loans (_ : eval_ctx) (_ : eval_ctx) _ty0 ids0 _v0 _av0 _ty1 + let match_ashared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ty0 ids0 _v0 _av0 _ty1 ids1 _v1 _av1 ty v av = let bids = match_loan_ids ids0 ids1 in let value = ALoan (ASharedLoan (bids, v, av)) in { value; ty } - let match_amut_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 id0 _av0 _ty1 + let match_amut_loans (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 id0 _av0 _ty1 id1 _av1 ty av = log#ldebug (lazy ("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 ctx1 av)); + ^ typed_avalue_to_string meta ctx1 av)); let id = match_loan_id id0 id1 in let value = ALoan (AMutLoan (id, av)) in { value; ty } - let match_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx) v0 v1 = + let match_avalues (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) v0 v1 = log#ldebug (lazy ("avalues don't match:\n- v0: " - ^ typed_avalue_to_string ctx0 v0 + ^ typed_avalue_to_string meta ctx0 v0 ^ "\n- v1: " - ^ typed_avalue_to_string ctx1 v1)); + ^ typed_avalue_to_string meta ctx1 v1)); raise (Distinct "match_avalues") end -let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) +let match_ctxs (meta : Meta.meta) (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 = @@ -1172,9 +1172,9 @@ let match_ctxs (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 ctx0 + ^ eval_ctx_to_string_no_filter meta ctx0 ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter ctx1 + ^ eval_ctx_to_string_no_filter meta ctx1 ^ "\n\n")); (* Initialize the maps and instantiate the matcher *) @@ -1282,7 +1282,7 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) log#ldebug (lazy "match_abstractions: matching values"); let _ = List.map - (fun (v0, v1) -> M.match_typed_avalues ctx0 ctx1 v0 v1) + (fun (v0, v1) -> M.match_typed_avalues meta ctx0 ctx1 v0 v1) (List.combine avalues0 avalues1) in log#ldebug (lazy "match_abstractions: values matched OK"); @@ -1303,9 +1303,9 @@ let match_ctxs (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 { ctx0 with env = List.rev env0 } + ^ eval_ctx_to_string_no_filter meta { ctx0 with env = List.rev env0 } ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter { ctx1 with env = List.rev env1 } + ^ eval_ctx_to_string_no_filter meta { ctx1 with env = List.rev env1 } ^ "\n\n")); match (env0, env1) with @@ -1321,12 +1321,12 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) assert ((not S.check_equiv) || ids_are_fixed ids)); (* We still match the values - allows to compute mappings (which are the identity actually) *) - let _ = M.match_typed_values ctx0 ctx1 v0 v1 in + let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in match_envs env0' env1' | EBinding (BVar b0, v0) :: env0', EBinding (BVar b1, v1) :: env1' -> assert (b0 = b1); (* Match the values *) - let _ = M.match_typed_values ctx0 ctx1 v0 v1 in + let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in (* Continue *) match_envs env0' env1' | EAbs abs0 :: env0', EAbs abs1 :: env1' -> @@ -1366,7 +1366,7 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) let env0, env1 = match (env0, env1) with | EFrame :: env0, EFrame :: env1 -> (env0, env1) - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in match_envs env0 env1; @@ -1382,23 +1382,16 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) } in Some maps - with - | Distinct msg -> - log#ldebug (lazy ("match_ctxs: distinct: " ^ msg ^ "\n")); - None - | ValueMatchFailure k -> - log#ldebug - (lazy - ("match_ctxs: distinct: ValueMatchFailure" ^ show_updt_env_kind k - ^ "\n")); - None + with Distinct msg -> + log#ldebug (lazy ("match_ctxs: distinct: " ^ msg)); + None -let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : eval_ctx) +let ctxs_are_equivalent (meta : Meta.meta) (fixed_ids : ids_sets) (ctx0 : eval_ctx) (ctx1 : eval_ctx) : bool = let check_equivalent = true in - let lookup_shared_value _ = raise (Failure "Unreachable") in + let lookup_shared_value _ = craise meta "Unreachable" in Option.is_some - (match_ctxs check_equivalent fixed_ids lookup_shared_value + (match_ctxs meta check_equivalent fixed_ids lookup_shared_value lookup_shared_value ctx0 ctx1) let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id : LoopId.id) @@ -1409,23 +1402,23 @@ let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id (lazy ("prepare_match_ctx_with_target:\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 + ^ eval_ctx_to_string meta src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string meta tgt_ctx )); (* End the loans which lead to mismatches when joining *) let rec cf_reorganize_join_tgt : cm_fun = fun cf 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 fixed_ids src_ctx in - let filt_tgt_env, _, _ = ctx_split_fixed_new fixed_ids tgt_ctx in + 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 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 src_ctx filt_src_env + ^ env_to_string meta src_ctx filt_src_env ^ "\n- filt_tgt_ctx: " - ^ env_to_string tgt_ctx filt_tgt_env)); + ^ env_to_string meta tgt_ctx filt_tgt_env)); (* Remove the abstractions *) let filter (ee : env_elem) : bool = @@ -1450,13 +1443,13 @@ let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id match (var0, var1) with | EBinding (BDummy b0, v0), EBinding (BDummy b1, v1) -> assert (b0 = b1); - let _ = M.match_typed_values src_ctx tgt_ctx v0 v1 in + let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in () | EBinding (BVar b0, v0), EBinding (BVar b1, v1) -> assert (b0 = b1); - let _ = M.match_typed_values src_ctx tgt_ctx v0 v1 in + let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in () - | _ -> raise (Failure "Unexpected")) + | _ -> craise meta "Unexpected") (List.combine filt_src_env filt_tgt_env) in (* No exception was thrown: continue *) @@ -1465,9 +1458,9 @@ let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id ("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 src_ctx filt_src_env + ^ env_to_string meta src_ctx filt_src_env ^ "\n- filt_tgt_ctx: " - ^ env_to_string tgt_ctx filt_tgt_env)); + ^ env_to_string meta 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 @@ -1487,13 +1480,13 @@ let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id match (var0, var1) with | EBinding (BDummy b0, v0), EBinding ((BDummy b1 as var1), v1) -> assert (b0 = b1); - let v = M.match_typed_values src_ctx tgt_ctx v0 v1 in + let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in (var1, v) | EBinding (BVar b0, v0), EBinding ((BVar b1 as var1), v1) -> assert (b0 = b1); - let v = M.match_typed_values src_ctx tgt_ctx v0 v1 in + let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in (var1, v) - | _ -> raise (Failure "Unexpected")) + | _ -> craise meta "Unexpected") (List.combine filt_src_env filt_tgt_env) in let var_to_new_val = BinderMap.of_list var_to_new_val in @@ -1521,18 +1514,18 @@ let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id (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 src_ctx ^ "\n- tgt_ctx: " - ^ eval_ctx_to_string tgt_ctx)); + ^ eval_ctx_to_string meta src_ctx ^ "\n- tgt_ctx: " + ^ eval_ctx_to_string meta tgt_ctx)); cf tgt_ctx with ValueMatchFailure e -> (* Exception: end the corresponding borrows, and continue *) let cc = match e with - | LoanInRight bid -> InterpreterBorrows.end_borrow config bid - | LoansInRight bids -> InterpreterBorrows.end_borrows config bids + | LoanInRight bid -> InterpreterBorrows.end_borrow meta config bid + | LoansInRight bids -> InterpreterBorrows.end_borrows meta config bids | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ -> - raise (Failure "Unexpected") + craise meta "Unexpected" in comp cc cf_reorganize_join_tgt cf tgt_ctx in @@ -1587,9 +1580,9 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string tgt_ctx)); - let filt_tgt_env, _, _ = ctx_split_fixed_new fixed_ids tgt_ctx in + 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 fixed_ids src_ctx + ctx_split_fixed_new meta fixed_ids src_ctx in assert (new_dummyl = []); let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in @@ -1603,13 +1596,13 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) match snd (lookup_loan meta ek_all lid ctx) with | Concrete (VSharedLoan (_, v)) -> v | Abstract (ASharedLoan (_, v, _)) -> v - | _ -> raise (Failure "Unreachable") + | _ -> craise 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 check_equiv fixed_ids lookup_in_src lookup_in_tgt + (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 = @@ -1623,13 +1616,13 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) log#ldebug (lazy ("match_ctx_with_target: cf_introduce_loop_fp_abs:" ^ "\n\n- src_ctx: " - ^ eval_ctx_to_string src_ctx ^ "\n\n- tgt_ctx: " - ^ eval_ctx_to_string tgt_ctx ^ "\n\n- filt_tgt_ctx: " - ^ eval_ctx_to_string_no_filter filt_tgt_ctx + ^ eval_ctx_to_string meta src_ctx ^ "\n\n- tgt_ctx: " + ^ eval_ctx_to_string meta tgt_ctx ^ "\n\n- filt_tgt_ctx: " + ^ eval_ctx_to_string_no_filter meta filt_tgt_ctx ^ "\n\n- filt_src_ctx: " - ^ eval_ctx_to_string_no_filter filt_src_ctx + ^ eval_ctx_to_string_no_filter meta filt_src_ctx ^ "\n\n- new_absl:\n" - ^ eval_ctx_to_string + ^ eval_ctx_to_string 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 @@ -1828,18 +1821,17 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) log#ldebug (lazy ("match_ctx_with_target: cf_introduce_loop_fp_abs: done:\n\ - - result ctx:\n" ^ eval_ctx_to_string tgt_ctx)); + - result ctx:\n" ^ eval_ctx_to_string meta tgt_ctx)); (* Sanity check *) if !Config.sanity_checks then - Invariants.check_borrowed_values_invariant tgt_ctx; - + 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 new_borrows in + let cc = InterpreterBorrows.end_borrows meta config new_borrows in (* Compute the loop input values *) let input_values = -- cgit v1.2.3 From 76fda6b5d205a4422c2360b676227690714c9ac5 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 22 Mar 2024 15:59:22 +0100 Subject: Still need to fill the TODO: error message and check some meta but it builds --- compiler/InterpreterLoopsMatchCtxs.ml | 146 ++++++++++++++++++---------------- 1 file changed, 76 insertions(+), 70 deletions(-) (limited to 'compiler/InterpreterLoopsMatchCtxs.ml') diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 08d18407..0e0a06e3 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -43,8 +43,8 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) match Id0.Map.find_opt id0 !map with | None -> () | Some set -> - assert ( - (not check_not_already_registered) || not (Id1.Set.mem id1 set))); + cassert ( + (not check_not_already_registered) || not (Id1.Set.mem id1 set)) meta "TODO: error message"); (* Update the mapping *) map := Id0.Map.update id0 @@ -53,10 +53,10 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) | None -> Some (Id1.Set.singleton id1) | Some ids -> (* Sanity check *) - assert (not check_singleton_sets); - assert ( + cassert (not check_singleton_sets) meta "TODO: error message"; + cassert ( (not check_not_already_registered) - || not (Id1.Set.mem id1 ids)); + || not (Id1.Set.mem id1 ids)) meta "TODO: error message"; (* Update *) Some (Id1.Set.add id1 ids)) !map @@ -144,14 +144,14 @@ 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 (match_distinct_types : ty -> ty -> ty) +let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty) (match_regions : region -> region -> region) (ty0 : ty) (ty1 : ty) : ty = - let match_rec = match_types match_distinct_types match_regions in + let match_rec = match_types meta match_distinct_types match_regions in match (ty0, ty1) with | TAdt (id0, generics0), TAdt (id1, generics1) -> - assert (id0 = id1); - assert (generics0.const_generics = generics1.const_generics); - assert (generics0.trait_refs = generics1.trait_refs); + cassert (id0 = id1) meta "T"; + cassert (generics0.const_generics = generics1.const_generics) meta "T"; + cassert (generics0.trait_refs = generics1.trait_refs) meta "T"; let id = id0 in let const_generics = generics1.const_generics in let trait_refs = generics1.trait_refs in @@ -168,17 +168,17 @@ let rec match_types (match_distinct_types : ty -> ty -> ty) let generics = { regions; types; const_generics; trait_refs } in TAdt (id, generics) | TVar vid0, TVar vid1 -> - assert (vid0 = vid1); + cassert (vid0 = vid1) meta "T"; let vid = vid0 in TVar vid | TLiteral lty0, TLiteral lty1 -> - assert (lty0 = lty1); + cassert (lty0 = lty1) meta "T"; 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 - assert (k0 = k1); + cassert (k0 = k1) meta "T"; let k = k0 in TRef (r, ty, k) | _ -> match_distinct_types ty0 ty1 @@ -187,7 +187,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let rec match_typed_values (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (v0 : typed_value) (v1 : typed_value) : typed_value = let match_rec = match_typed_values meta ctx0 ctx1 in - let ty = M.match_etys ctx0 ctx1 v0.ty v1.ty in + let ty = M.match_etys meta ctx0 ctx1 v0.ty v1.ty in (* Using ValuesUtils.value_has_borrows on purpose here: we want to make explicit the fact that, though we have to pick one of the two contexts (ctx0 here) to call value_has_borrows, @@ -210,8 +210,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct { value; ty = v1.ty } else ( (* For now, we don't merge ADTs which contain borrows *) - assert (not (value_has_borrows v0.value)); - assert (not (value_has_borrows v1.value)); + cassert (not (value_has_borrows v0.value)) meta "ADTs which contain borrows are not merged yet"; + cassert (not (value_has_borrows v1.value)) meta "ADTs which contain borrows are not merged yet"; (* Merge *) M.match_distinct_adts meta ctx0 ctx1 ty av0 av1) | VBottom, VBottom -> v0 @@ -226,10 +226,10 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct | VMutBorrow (bid0, bv0), VMutBorrow (bid1, bv1) -> let bv = match_rec bv0 bv1 in - assert ( + cassert ( not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos - bv.value)); + bv.value)) meta "T"; let bid, bv = M.match_mut_borrows meta ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv in @@ -252,8 +252,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct match (lc0, lc1) with | VSharedLoan (ids0, sv0), VSharedLoan (ids1, sv1) -> let sv = match_rec sv0 sv1 in - assert (not (value_has_borrows sv.value)); - let ids, sv = M.match_shared_loans ctx0 ctx1 ty ids0 ids1 sv in + cassert (not (value_has_borrows sv.value)) meta "T"; + let ids, sv = M.match_shared_loans meta 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 @@ -265,8 +265,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct | VSymbolic sv0, VSymbolic sv1 -> (* For now, we force all the symbolic values containing borrows to be eagerly expanded, and we don't support nested borrows *) - assert (not (value_has_borrows v0.value)); - assert (not (value_has_borrows v1.value)); + cassert (not (value_has_borrows v0.value)) meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded"; + cassert (not (value_has_borrows v1.value)) meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded"; (* Match *) let sv = M.match_symbolic_values meta ctx0 ctx1 sv0 sv1 in { v1 with value = VSymbolic sv } @@ -310,7 +310,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let match_rec = match_typed_values meta ctx0 ctx1 in let match_arec = match_typed_avalues meta ctx0 ctx1 in - let ty = M.match_rtys ctx0 ctx1 v0.ty v1.ty in + let ty = M.match_rtys meta ctx0 ctx1 v0.ty v1.ty in match (v0.value, v1.value) with | AAdt av0, AAdt av1 -> if av0.variant_id = av1.variant_id then @@ -373,7 +373,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct log#ldebug (lazy "match_typed_avalues: shared loans"); let sv = match_rec sv0 sv1 in let av = match_arec av0 av1 in - assert (not (value_has_borrows sv.value)); + cassert (not (value_has_borrows sv.value)) meta "T"; M.match_ashared_loans meta ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1 av1 ty sv av | AMutLoan (id0, av0), AMutLoan (id1, av1) -> @@ -403,14 +403,14 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let push_absl (absl : abs list) : unit = List.iter push_abs absl - let match_etys _ _ ty0 ty1 = - assert (ty0 = ty1); + let match_etys (meta : Meta.meta) _ _ ty0 ty1 = + cassert (ty0 = ty1) meta "T"; ty0 - let match_rtys _ _ ty0 ty1 = + let match_rtys (meta : Meta.meta) _ _ ty0 ty1 = (* The types must be equal - in effect, this forbids to match symbolic values containing borrows *) - assert (ty0 = ty1); + cassert (ty0 = ty1) meta "The types must be equal - in effect, this forbids to match symbolic values containing borrows"; ty0 let match_distinct_literals (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) @@ -424,7 +424,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct updates *) let check_no_borrows ctx (v : typed_value) = - assert (not (value_has_borrows ctx v.value)) + cassert (not (value_has_borrows ctx v.value)) meta "ADTs should not contain borrows" in List.iter (check_no_borrows ctx0) adt0.field_values; List.iter (check_no_borrows ctx1) adt1.field_values; @@ -559,11 +559,11 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct do so, we won't introduce reborrows like above: the forward loop function will update [v], while the backward loop function will return nothing. *) - assert ( - not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)); + cassert ( + not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) meta "T"; if bv0 = bv1 then ( - assert (bv0 = bv); + cassert (bv0 = bv) meta "T"; (bid0, bv)) else let rid = fresh_region_id () in @@ -571,7 +571,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let kind = RMut in let bv_ty = bv.ty in - assert (ty_no_regions bv_ty); + cassert (ty_no_regions bv_ty) meta "T"; let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in let borrow_av = @@ -624,7 +624,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Generate the avalues for the abstraction *) let mk_aborrow (bid : borrow_id) (bv : typed_value) : typed_avalue = let bv_ty = bv.ty in - assert (ty_no_regions bv_ty); + cassert (ty_no_regions bv_ty) meta "T"; let value = ABorrow (AMutBorrow (bid, mk_aignored meta bv_ty)) in { value; ty = borrow_ty } in @@ -654,7 +654,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Return the new borrow *) (bid2, sv) - let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety) + let match_shared_loans (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (ids0 : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) : loan_id_set * typed_value = (* Check if the ids are the same - Rem.: we forbid the sets of loans @@ -671,7 +671,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct raise (ValueMatchFailure (LoansInRight extra_ids_right)); (* This should always be true if we get here *) - assert (ids0 = ids1); + cassert (ids0 = ids1) meta "This should always be true if we get here "; let ids = ids0 in (* Return *) @@ -691,13 +691,13 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let id1 = sv1.sv_id in if id0 = id1 then ( (* Sanity check *) - assert (sv0 = sv1); + cassert (sv0 = sv1) meta "T"; (* Return *) sv0) else ( (* The caller should have checked that the symbolic values don't contain borrows *) - assert (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)); + cassert (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) meta "The caller should have checked that the symbolic values don't contain borrows"; (* We simply introduce a fresh symbolic value *) mk_fresh_symbolic_value meta sv0.sv_ty) @@ -709,8 +709,14 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct If there are loans in the regular value, raise an exception. *) let type_infos = ctx0.type_ctx.type_infos in - assert (not (ty_has_borrows type_infos sv.sv_ty)); - assert (not (ValuesUtils.value_has_borrows type_infos v.value)); + cassert (not (ty_has_borrows type_infos sv.sv_ty)) meta "Check that: + - there are no borrows in the symbolic value + - there are no borrows in the \"regular\" value + If there are loans in the regular value, raise an exception."; + cassert (not (ValuesUtils.value_has_borrows type_infos v.value)) meta "Check that: + - there are no borrows in the symbolic value + - there are no borrows in the \"regular\" value + If there are loans in the regular value, raise an exception."; let value_is_left = not left in (match InterpreterBorrowsCore.get_first_loan_in_value v with | None -> () @@ -804,14 +810,14 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (** Small utility *) let push_moved_value (v : typed_value) : unit = S.nvalues := v :: !S.nvalues - let match_etys _ _ ty0 ty1 = - assert (ty0 = ty1); + let match_etys (meta : Meta.meta) _ _ ty0 ty1 = + cassert (ty0 = ty1) meta "T"; ty0 - let match_rtys _ _ ty0 ty1 = + let match_rtys (meta : Meta.meta) _ _ ty0 ty1 = (* The types must be equal - in effect, this forbids to match symbolic values containing borrows *) - assert (ty0 = ty1); + cassert (ty0 = ty1) meta "The types must be equal - in effect, this forbids to match symbolic values containing borrows"; ty0 let match_distinct_literals (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) @@ -835,7 +841,7 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (* There can't be bottoms in borrowed values *) (bid1, bv1) - let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety) + let match_shared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (_ : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) : loan_id_set * typed_value = (* There can't be bottoms in shared loans *) @@ -983,10 +989,10 @@ struct let match_aids = GetSetAid.match_es "match_aids: " S.aid_map (** *) - let match_etys (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = + let match_etys (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = if ty0 <> ty1 then raise (Distinct "match_etys") else ty0 - let match_rtys (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = + let match_rtys (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = let match_distinct_types _ _ = raise (Distinct "match_rtys") in let match_regions r0 r1 = match (r0, r1) with @@ -996,7 +1002,7 @@ struct RFVar rid | _ -> raise (Distinct "match_rtys") in - match_types match_distinct_types match_regions ty0 ty1 + match_types meta match_distinct_types match_regions ty0 ty1 let match_distinct_literals (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) (_ : literal) (_ : literal) : typed_value = @@ -1042,7 +1048,7 @@ struct let bid = match_borrow_id bid0 bid1 in (bid, bv) - let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety) + let match_shared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (ids0 : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) : loan_id_set * typed_value = let ids = match_loan_ids ids0 ids1 in @@ -1052,7 +1058,7 @@ struct (bid1 : loan_id) : loan_id = match_loan_id bid0 bid1 - let match_symbolic_values (_ : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) + let match_symbolic_values (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value = let id0 = sv0.sv_id in let id1 = sv1.sv_id in @@ -1071,12 +1077,12 @@ struct let sv_id = GetSetSid.match_e "match_symbolic_values: ids: " S.sid_map id0 id1 in - let sv_ty = match_rtys ctx0 ctx1 sv0.sv_ty sv1.sv_ty in + let sv_ty = match_rtys meta ctx0 ctx1 sv0.sv_ty sv1.sv_ty in let sv = { sv_id; sv_ty } in sv else ( (* Check: fixed values are fixed *) - assert (id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map)); + cassert (id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map)) meta "Fixed values should be fixed"; (* Update the symbolic value mapping *) let sv1 = mk_typed_value_from_symbolic_value sv1 in @@ -1093,10 +1099,10 @@ struct (sv : symbolic_value) (v : typed_value) : typed_value = if S.check_equiv then raise (Distinct "match_symbolic_with_other") else ( - assert left; + cassert left meta "T"; let id = sv.sv_id in (* Check: fixed values are fixed *) - assert (not (SymbolicValueId.InjSubst.mem id !S.sid_map)); + cassert (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) meta "Fixed values should be fixed"; (* Update the binding for the target symbolic value *) S.sid_to_value_map := SymbolicValueId.Map.add_strict id v !S.sid_to_value_map; @@ -1314,17 +1320,17 @@ 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 *) - assert (b0 = b1); - assert (v0 = v1); + cassert (b0 = b1) meta "The fixed values should be equal"; + cassert (v0 = v1) meta "The fixed values should be equal"; (* The ids present in the left value must be fixed *) let ids, _ = compute_typed_value_ids v0 in - assert ((not S.check_equiv) || ids_are_fixed ids)); + cassert ((not S.check_equiv) || ids_are_fixed ids)) meta "T"; (* We still match the values - allows to compute mappings (which are the identity actually) *) let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in match_envs env0' env1' | EBinding (BVar b0, v0) :: env0', EBinding (BVar b1, v1) :: env1' -> - assert (b0 = b1); + cassert (b0 = b1) meta "T"; (* Match the values *) let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in (* Continue *) @@ -1335,10 +1341,10 @@ 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 *) - assert (abs0 = abs1); + cassert (abs0 = abs1) meta "The abstractions should be the same"; (* Their ids must be fixed *) let ids, _ = compute_abs_ids abs0 in - assert ((not S.check_equiv) || ids_are_fixed ids); + cassert ((not S.check_equiv) || ids_are_fixed ids) meta "The ids should be fixed"; (* Continue *) match_envs env0' env1') else ( @@ -1442,11 +1448,11 @@ let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id (fun (var0, var1) -> match (var0, var1) with | EBinding (BDummy b0, v0), EBinding (BDummy b1, v1) -> - assert (b0 = b1); + cassert (b0 = b1) meta "T"; let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in () | EBinding (BVar b0, v0), EBinding (BVar b1, v1) -> - assert (b0 = b1); + cassert (b0 = b1) meta "T"; let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in () | _ -> craise meta "Unexpected") @@ -1479,11 +1485,11 @@ let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id (fun (var0, var1) -> match (var0, var1) with | EBinding (BDummy b0, v0), EBinding ((BDummy b1 as var1), v1) -> - assert (b0 = b1); + cassert (b0 = b1) meta "T"; let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in (var1, v) | EBinding (BVar b0, v0), EBinding ((BVar b1 as var1), v1) -> - assert (b0 = b1); + cassert (b0 = b1) meta "T"; let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in (var1, v) | _ -> craise meta "Unexpected") @@ -1584,7 +1590,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) let filt_src_env, new_absl, new_dummyl = ctx_split_fixed_new meta fixed_ids src_ctx in - assert (new_dummyl = []); + cassert (new_dummyl = []) meta "T"; let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in let filt_src_ctx = { src_ctx with env = filt_src_env } in @@ -1720,7 +1726,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) abstractions and in the *variable bindings* once we allow symbolic values containing borrows to not be eagerly expanded. *) - assert Config.greedy_expand_symbolics_with_borrows; + cassert Config.greedy_expand_symbolics_with_borrows meta "T"; (* Update the borrows and loans in the abstractions of the target context. @@ -1789,8 +1795,8 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) (* 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 *) - assert ( - BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id); + cassert ( + BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id) meta "The borrow should mapped to itself: no mapping means that the borrow was mapped when we matched values (it doesn't come from a fresh abstraction) "; id | Some id -> id @@ -1802,8 +1808,8 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) method! visit_abs env abs = match abs.kind with | Loop (loop_id', rg_id, kind) -> - assert (loop_id' = loop_id); - assert (kind = LoopSynthInput); + cassert (loop_id' = loop_id) meta "T"; + cassert (kind = LoopSynthInput) meta "T"; let can_end = false in let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in let abs = { abs with kind; can_end } in -- cgit v1.2.3 From 9b1a0d82c19375619904efe7e18e064701fb947b Mon Sep 17 00:00:00 2001 From: Escherichia Date: Mon, 25 Mar 2024 10:16:15 +0100 Subject: Replaced some unclear TODOs error message placeholder by clearer TODOs, they were forgotten before last push --- compiler/InterpreterLoopsMatchCtxs.ml | 54 +++++++++++++++++------------------ 1 file changed, 27 insertions(+), 27 deletions(-) (limited to 'compiler/InterpreterLoopsMatchCtxs.ml') diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 0e0a06e3..033e51c1 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -149,9 +149,9 @@ let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty) let match_rec = match_types meta match_distinct_types match_regions in match (ty0, ty1) with | TAdt (id0, generics0), TAdt (id1, generics1) -> - cassert (id0 = id1) meta "T"; - cassert (generics0.const_generics = generics1.const_generics) meta "T"; - cassert (generics0.trait_refs = generics1.trait_refs) meta "T"; + cassert (id0 = id1) meta "TODO: error message"; + cassert (generics0.const_generics = generics1.const_generics) meta "TODO: error message"; + cassert (generics0.trait_refs = generics1.trait_refs) meta "TODO: error message"; let id = id0 in let const_generics = generics1.const_generics in let trait_refs = generics1.trait_refs in @@ -168,17 +168,17 @@ 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 -> - cassert (vid0 = vid1) meta "T"; + cassert (vid0 = vid1) meta "TODO: error message"; let vid = vid0 in TVar vid | TLiteral lty0, TLiteral lty1 -> - cassert (lty0 = lty1) meta "T"; + cassert (lty0 = lty1) meta "TODO: error message"; 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 - cassert (k0 = k1) meta "T"; + cassert (k0 = k1) meta "TODO: error message"; let k = k0 in TRef (r, ty, k) | _ -> match_distinct_types ty0 ty1 @@ -229,7 +229,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct cassert ( not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos - bv.value)) meta "T"; + bv.value)) meta "TODO: error message"; let bid, bv = M.match_mut_borrows meta ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv in @@ -252,7 +252,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct match (lc0, lc1) with | VSharedLoan (ids0, sv0), VSharedLoan (ids1, sv1) -> let sv = match_rec sv0 sv1 in - cassert (not (value_has_borrows sv.value)) meta "T"; + cassert (not (value_has_borrows sv.value)) meta "TODO: error message"; let ids, sv = M.match_shared_loans meta ctx0 ctx1 ty ids0 ids1 sv in VSharedLoan (ids, sv) | VMutLoan id0, VMutLoan id1 -> @@ -373,7 +373,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct log#ldebug (lazy "match_typed_avalues: shared loans"); let sv = match_rec sv0 sv1 in let av = match_arec av0 av1 in - cassert (not (value_has_borrows sv.value)) meta "T"; + cassert (not (value_has_borrows sv.value)) meta "TODO: error message"; M.match_ashared_loans meta ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1 av1 ty sv av | AMutLoan (id0, av0), AMutLoan (id1, av1) -> @@ -404,7 +404,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let push_absl (absl : abs list) : unit = List.iter push_abs absl let match_etys (meta : Meta.meta) _ _ ty0 ty1 = - cassert (ty0 = ty1) meta "T"; + cassert (ty0 = ty1) meta "TODO: error message"; ty0 let match_rtys (meta : Meta.meta) _ _ ty0 ty1 = @@ -560,10 +560,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct will update [v], while the backward loop function will return nothing. *) cassert ( - not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) meta "T"; + not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) meta "TODO: error message"; if bv0 = bv1 then ( - cassert (bv0 = bv) meta "T"; + cassert (bv0 = bv) meta "TODO: error message"; (bid0, bv)) else let rid = fresh_region_id () in @@ -571,7 +571,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let kind = RMut in let bv_ty = bv.ty in - cassert (ty_no_regions bv_ty) meta "T"; + cassert (ty_no_regions bv_ty) meta "TODO: error message"; let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in let borrow_av = @@ -624,7 +624,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Generate the avalues for the abstraction *) let mk_aborrow (bid : borrow_id) (bv : typed_value) : typed_avalue = let bv_ty = bv.ty in - cassert (ty_no_regions bv_ty) meta "T"; + cassert (ty_no_regions bv_ty) meta "TODO: error message"; let value = ABorrow (AMutBorrow (bid, mk_aignored meta bv_ty)) in { value; ty = borrow_ty } in @@ -691,7 +691,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let id1 = sv1.sv_id in if id0 = id1 then ( (* Sanity check *) - cassert (sv0 = sv1) meta "T"; + cassert (sv0 = sv1) meta "TODO: error message"; (* Return *) sv0) else ( @@ -811,7 +811,7 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct let push_moved_value (v : typed_value) : unit = S.nvalues := v :: !S.nvalues let match_etys (meta : Meta.meta) _ _ ty0 ty1 = - cassert (ty0 = ty1) meta "T"; + cassert (ty0 = ty1) meta "TODO: error message"; ty0 let match_rtys (meta : Meta.meta) _ _ ty0 ty1 = @@ -1099,7 +1099,7 @@ struct (sv : symbolic_value) (v : typed_value) : typed_value = if S.check_equiv then raise (Distinct "match_symbolic_with_other") else ( - cassert left meta "T"; + cassert left meta "TODO: error message"; let id = sv.sv_id in (* Check: fixed values are fixed *) cassert (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) meta "Fixed values should be fixed"; @@ -1324,13 +1324,13 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) cassert (v0 = v1) meta "The fixed values should be equal"; (* The ids present in the left value must be fixed *) let ids, _ = compute_typed_value_ids v0 in - cassert ((not S.check_equiv) || ids_are_fixed ids)) meta "T"; + cassert ((not S.check_equiv) || ids_are_fixed ids)) meta "TODO: error message"; (* We still match the values - allows to compute mappings (which are the identity actually) *) let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in match_envs env0' env1' | EBinding (BVar b0, v0) :: env0', EBinding (BVar b1, v1) :: env1' -> - cassert (b0 = b1) meta "T"; + cassert (b0 = b1) meta "TODO: error message"; (* Match the values *) let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in (* Continue *) @@ -1448,11 +1448,11 @@ let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id (fun (var0, var1) -> match (var0, var1) with | EBinding (BDummy b0, v0), EBinding (BDummy b1, v1) -> - cassert (b0 = b1) meta "T"; + cassert (b0 = b1) meta "TODO: error message"; let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in () | EBinding (BVar b0, v0), EBinding (BVar b1, v1) -> - cassert (b0 = b1) meta "T"; + cassert (b0 = b1) meta "TODO: error message"; let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in () | _ -> craise meta "Unexpected") @@ -1485,11 +1485,11 @@ let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id (fun (var0, var1) -> match (var0, var1) with | EBinding (BDummy b0, v0), EBinding ((BDummy b1 as var1), v1) -> - cassert (b0 = b1) meta "T"; + cassert (b0 = b1) meta "TODO: error message"; let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in (var1, v) | EBinding (BVar b0, v0), EBinding ((BVar b1 as var1), v1) -> - cassert (b0 = b1) meta "T"; + cassert (b0 = b1) meta "TODO: error message"; let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in (var1, v) | _ -> craise meta "Unexpected") @@ -1590,7 +1590,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) let filt_src_env, new_absl, new_dummyl = ctx_split_fixed_new meta fixed_ids src_ctx in - cassert (new_dummyl = []) meta "T"; + cassert (new_dummyl = []) meta "TODO: error message"; let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in let filt_src_ctx = { src_ctx with env = filt_src_env } in @@ -1726,7 +1726,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) abstractions and in the *variable bindings* once we allow symbolic values containing borrows to not be eagerly expanded. *) - cassert Config.greedy_expand_symbolics_with_borrows meta "T"; + cassert Config.greedy_expand_symbolics_with_borrows meta "TODO: error message"; (* Update the borrows and loans in the abstractions of the target context. @@ -1808,8 +1808,8 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) method! visit_abs env abs = match abs.kind with | Loop (loop_id', rg_id, kind) -> - cassert (loop_id' = loop_id) meta "T"; - cassert (kind = LoopSynthInput) meta "T"; + cassert (loop_id' = loop_id) meta "TODO: error message"; + cassert (kind = LoopSynthInput) meta "TODO: error message"; let can_end = false in let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in let abs = { abs with kind; can_end } in -- cgit v1.2.3 From d6ea35868e30bbc7542bfa09bb04d5b6cbe93b22 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Mon, 25 Mar 2024 12:06:05 +0100 Subject: Inverted meta and config argument orders (from meta -> config to config -> meta) --- compiler/InterpreterLoopsMatchCtxs.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'compiler/InterpreterLoopsMatchCtxs.ml') diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 033e51c1..2e700c50 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -1400,7 +1400,7 @@ let ctxs_are_equivalent (meta : Meta.meta) (fixed_ids : ids_sets) (ctx0 : eval_c (match_ctxs meta check_equivalent fixed_ids lookup_shared_value lookup_shared_value ctx0 ctx1) -let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id : LoopId.id) +let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (src_ctx : eval_ctx) : cm_fun = fun cf tgt_ctx -> (* Debug *) @@ -1528,8 +1528,8 @@ let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id (* Exception: end the corresponding borrows, and continue *) let cc = match e with - | LoanInRight bid -> InterpreterBorrows.end_borrow meta config bid - | LoansInRight bids -> InterpreterBorrows.end_borrows meta config bids + | LoanInRight bid -> InterpreterBorrows.end_borrow config meta bid + | LoansInRight bids -> InterpreterBorrows.end_borrows config meta bids | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ -> craise meta "Unexpected" in @@ -1837,7 +1837,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) BorrowId.Set.of_list (List.map snd (BorrowId.Map.bindings !src_fresh_borrows_map)) in - let cc = InterpreterBorrows.end_borrows meta config new_borrows in + let cc = InterpreterBorrows.end_borrows config meta new_borrows in (* Compute the loop input values *) let input_values = -- cgit v1.2.3 From 0f0082c81db8852dff23cd4691af19c434c8be78 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Wed, 27 Mar 2024 10:22:06 +0100 Subject: Added sanity_check and sanity_check_opt_meta helpers and changed sanity checks related cassert to these helpers to have a proper error message --- compiler/InterpreterLoopsMatchCtxs.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'compiler/InterpreterLoopsMatchCtxs.ml') diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 2e700c50..435174a7 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -43,8 +43,8 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) match Id0.Map.find_opt id0 !map with | None -> () | Some set -> - cassert ( - (not check_not_already_registered) || not (Id1.Set.mem id1 set)) meta "TODO: error message"); + sanity_check ( + (not check_not_already_registered) || not (Id1.Set.mem id1 set)) meta); (* Update the mapping *) map := Id0.Map.update id0 @@ -53,10 +53,10 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) | None -> Some (Id1.Set.singleton id1) | Some ids -> (* Sanity check *) - cassert (not check_singleton_sets) meta "TODO: error message"; - cassert ( + sanity_check (not check_singleton_sets) meta; + sanity_check ( (not check_not_already_registered) - || not (Id1.Set.mem id1 ids)) meta "TODO: error message"; + || not (Id1.Set.mem id1 ids)) meta; (* Update *) Some (Id1.Set.add id1 ids)) !map @@ -691,7 +691,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let id1 = sv1.sv_id in if id0 = id1 then ( (* Sanity check *) - cassert (sv0 = sv1) meta "TODO: error message"; + sanity_check (sv0 = sv1) meta; (* Return *) sv0) else ( -- cgit v1.2.3 From 5ad671a0960692af1c00609fa6864c6f44ca299c Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 13:56:31 +0100 Subject: Should answer all comments, there are still some TODO: error message left --- compiler/InterpreterLoopsMatchCtxs.ml | 322 +++++++++++++++++----------------- 1 file changed, 164 insertions(+), 158 deletions(-) (limited to 'compiler/InterpreterLoopsMatchCtxs.ml') diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 435174a7..c02d3117 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -149,9 +149,9 @@ let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty) let match_rec = match_types meta match_distinct_types match_regions in match (ty0, ty1) with | TAdt (id0, generics0), TAdt (id1, generics1) -> - cassert (id0 = id1) meta "TODO: error message"; - cassert (generics0.const_generics = generics1.const_generics) meta "TODO: error message"; - cassert (generics0.trait_refs = generics1.trait_refs) meta "TODO: error message"; + sanity_check (id0 = id1) meta; + sanity_check (generics0.const_generics = generics1.const_generics) meta; + sanity_check (generics0.trait_refs = generics1.trait_refs) meta; let id = id0 in let const_generics = generics1.const_generics in let trait_refs = generics1.trait_refs in @@ -168,27 +168,28 @@ 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 -> - cassert (vid0 = vid1) meta "TODO: error message"; + sanity_check (vid0 = vid1) meta; let vid = vid0 in TVar vid | TLiteral lty0, TLiteral lty1 -> - cassert (lty0 = lty1) meta "TODO: error message"; + sanity_check (lty0 = lty1) meta; 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 - cassert (k0 = k1) meta "TODO: error message"; + sanity_check (k0 = k1) meta; let k = k0 in TRef (r, ty, k) | _ -> match_distinct_types ty0 ty1 module MakeMatcher (M : PrimMatcher) : Matcher = struct - let rec match_typed_values (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) + let meta = M.meta + let rec match_typed_values (ctx0 : eval_ctx) (ctx1 : eval_ctx) (v0 : typed_value) (v1 : typed_value) : typed_value = - let match_rec = match_typed_values meta ctx0 ctx1 in - let ty = M.match_etys meta ctx0 ctx1 v0.ty v1.ty in - (* Using ValuesUtils.value_has_borrows on purpose here: we want + let match_rec = match_typed_values ctx0 ctx1 in + let ty = M.match_etys ctx0 ctx1 v0.ty v1.ty in + (* Using ValuesUtils.value_ has_borrows on purpose here: we want to make explicit the fact that, though we have to pick one of the two contexts (ctx0 here) to call value_has_borrows, it doesn't matter here. *) @@ -197,7 +198,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct in match (v0.value, v1.value) with | VLiteral lv0, VLiteral lv1 -> - if lv0 = lv1 then v1 else M.match_distinct_literals meta ctx0 ctx1 ty lv0 lv1 + if lv0 = lv1 then v1 else M.match_distinct_literals ctx0 ctx1 ty lv0 lv1 | VAdt av0, VAdt av1 -> if av0.variant_id = av1.variant_id then let fields = List.combine av0.field_values av1.field_values in @@ -210,17 +211,17 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct { value; ty = v1.ty } else ( (* For now, we don't merge ADTs which contain borrows *) - cassert (not (value_has_borrows v0.value)) meta "ADTs which contain borrows are not merged yet"; - cassert (not (value_has_borrows v1.value)) meta "ADTs which contain borrows are not merged yet"; + sanity_check (not (value_has_borrows v0.value)) M.meta; + sanity_check (not (value_has_borrows v1.value)) M.meta; (* Merge *) - M.match_distinct_adts meta ctx0 ctx1 ty av0 av1) + M.match_distinct_adts ctx0 ctx1 ty av0 av1) | VBottom, VBottom -> v0 | VBorrow bc0, VBorrow bc1 -> let bc = match (bc0, bc1) with | VSharedBorrow bid0, VSharedBorrow bid1 -> let bid = - M.match_shared_borrows meta ctx0 ctx1 match_rec ty bid0 bid1 + M.match_shared_borrows ctx0 ctx1 match_rec ty bid0 bid1 in VSharedBorrow bid | VMutBorrow (bid0, bv0), VMutBorrow (bid1, bv1) -> @@ -229,9 +230,9 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct cassert ( not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos - bv.value)) meta "TODO: error message"; + bv.value)) M.meta "TODO: error message"; let bid, bv = - M.match_mut_borrows meta ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv + M.match_mut_borrows ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv in VMutBorrow (bid, bv) | VReservedMutBorrow _, _ @@ -242,7 +243,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 meta "Unexpected" + craise M.meta "Unexpected" in { value = VBorrow bc; ty } | VLoan lc0, VLoan lc1 -> @@ -252,23 +253,23 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct match (lc0, lc1) with | VSharedLoan (ids0, sv0), VSharedLoan (ids1, sv1) -> let sv = match_rec sv0 sv1 in - cassert (not (value_has_borrows sv.value)) meta "TODO: error message"; - let ids, sv = M.match_shared_loans meta ctx0 ctx1 ty ids0 ids1 sv in + cassert (not (value_has_borrows sv.value)) M.meta "TODO: error message"; + 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 meta "Unreachable" + craise M.meta "Unreachable" in { value = VLoan lc; ty = v1.ty } | VSymbolic sv0, VSymbolic sv1 -> (* For now, we force all the symbolic values containing borrows to be eagerly expanded, and we don't support nested borrows *) - cassert (not (value_has_borrows v0.value)) meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded"; - cassert (not (value_has_borrows v1.value)) meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded"; + cassert (not (value_has_borrows v0.value)) M.meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded"; + cassert (not (value_has_borrows v1.value)) M.meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded"; (* Match *) - let sv = M.match_symbolic_values meta ctx0 ctx1 sv0 sv1 in + let sv = M.match_symbolic_values ctx0 ctx1 sv0 sv1 in { v1 with value = VSymbolic sv } | VLoan lc, _ -> ( match lc with @@ -278,27 +279,27 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct match lc with | VSharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids)) | VMutLoan id -> raise (ValueMatchFailure (LoanInRight id))) - | VSymbolic sv, _ -> M.match_symbolic_with_other meta ctx0 ctx1 true sv v1 - | _, VSymbolic sv -> M.match_symbolic_with_other meta ctx0 ctx1 false sv v0 - | VBottom, _ -> M.match_bottom_with_other meta ctx0 ctx1 true v1 - | _, VBottom -> M.match_bottom_with_other meta ctx0 ctx1 false v0 + | VSymbolic sv, _ -> M.match_symbolic_with_other ctx0 ctx1 true sv v1 + | _, VSymbolic sv -> M.match_symbolic_with_other ctx0 ctx1 false sv v0 + | VBottom, _ -> M.match_bottom_with_other ctx0 ctx1 true v1 + | _, VBottom -> M.match_bottom_with_other ctx0 ctx1 false v0 | _ -> log#ldebug (lazy ("Unexpected match case:\n- value0: " - ^ typed_value_to_string meta ctx0 v0 + ^ typed_value_to_string ~meta:(Some M.meta) ctx0 v0 ^ "\n- value1: " - ^ typed_value_to_string meta ctx1 v1)); - craise meta "Unexpected match case" + ^ typed_value_to_string ~meta:(Some M.meta) ctx1 v1)); + craise M.meta "Unexpected match case" - and match_typed_avalues (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) + 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 ctx0 v0 + ^ typed_avalue_to_string ~meta:(Some M.meta) ctx0 v0 ^ "\n- value1: " - ^ typed_avalue_to_string meta ctx1 v1)); + ^ typed_avalue_to_string ~meta:(Some M.meta) ctx1 v1)); (* Using ValuesUtils.value_has_borrows on purpose here: we want to make explicit the fact that, though we have to pick @@ -308,9 +309,9 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos in - let match_rec = match_typed_values meta ctx0 ctx1 in - let match_arec = match_typed_avalues meta ctx0 ctx1 in - let ty = M.match_rtys meta ctx0 ctx1 v0.ty v1.ty in + let match_rec = match_typed_values ctx0 ctx1 in + let match_arec = match_typed_avalues ctx0 ctx1 in + let ty = M.match_rtys ctx0 ctx1 v0.ty v1.ty in match (v0.value, v1.value) with | AAdt av0, AAdt av1 -> if av0.variant_id = av1.variant_id then @@ -323,15 +324,15 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct in { value; ty } else (* Merge *) - M.match_distinct_aadts meta ctx0 ctx1 v0.ty av0 v1.ty av1 ty - | ABottom, ABottom -> mk_abottom meta ty - | AIgnored, AIgnored -> mk_aignored meta ty + 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 | ABorrow bc0, ABorrow bc1 -> ( log#ldebug (lazy "match_typed_avalues: borrows"); match (bc0, bc1) with | ASharedBorrow bid0, ASharedBorrow bid1 -> log#ldebug (lazy "match_typed_avalues: shared borrows"); - M.match_ashared_borrows meta ctx0 ctx1 v0.ty bid0 v1.ty bid1 ty + M.match_ashared_borrows ctx0 ctx1 v0.ty bid0 v1.ty bid1 ty | AMutBorrow (bid0, av0), AMutBorrow (bid1, av1) -> log#ldebug (lazy "match_typed_avalues: mut borrows"); log#ldebug @@ -340,10 +341,10 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let av = match_arec av0 av1 in log#ldebug (lazy "match_typed_avalues: mut borrows: matched children values"); - M.match_amut_borrows meta ctx0 ctx1 v0.ty bid0 av0 v1.ty bid1 av1 ty av + 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 meta "Unexpected" + craise M.meta "Unexpected" | AProjSharedBorrow asb0, AProjSharedBorrow asb1 -> ( match (asb0, asb1) with | [], [] -> @@ -352,7 +353,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct v0 | _ -> (* We should get there only if there are nested borrows *) - craise meta "Unexpected") + craise M.meta "Unexpected") | _ -> (* TODO: getting there is not necessarily inconsistent (it may just be because the environments don't match) so we may want @@ -363,7 +364,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct we are *currently* ending it, in which case we need to completely end it before continuing. *) - craise meta "Unexpected") + craise M.meta "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 - @@ -373,8 +374,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct log#ldebug (lazy "match_typed_avalues: shared loans"); let sv = match_rec sv0 sv1 in let av = match_arec av0 av1 in - cassert (not (value_has_borrows sv.value)) meta "TODO: error message"; - M.match_ashared_loans meta ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1 + sanity_check (not (value_has_borrows sv.value)) M.meta; + 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) -> log#ldebug (lazy "match_typed_avalues: mut loans"); @@ -383,48 +384,49 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let av = match_arec av0 av1 in log#ldebug (lazy "match_typed_avalues: mut loans: matched children values"); - M.match_amut_loans meta ctx0 ctx1 v0.ty id0 av0 v1.ty id1 av1 ty av + M.match_amut_loans ctx0 ctx1 v0.ty id0 av0 v1.ty id1 av1 ty av | AIgnoredMutLoan _, AIgnoredMutLoan _ | AIgnoredSharedLoan _, AIgnoredSharedLoan _ -> (* Those should have been filtered when destructuring the abstractions - they are necessary only when there are nested borrows *) - craise meta "Unreachable" - | _ -> craise meta "Unreachable") + craise M.meta "Unreachable" + | _ -> craise M.meta "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 meta "Unreachable" - | _ -> M.match_avalues meta ctx0 ctx1 v0 v1 + craise M.meta "Unreachable" + | _ -> M.match_avalues ctx0 ctx1 v0 v1 end module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (** Small utility *) + let meta = S.meta 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 (meta : Meta.meta) _ _ ty0 ty1 = - cassert (ty0 = ty1) meta "TODO: error message"; + let match_etys _ _ ty0 ty1 = + sanity_check (ty0 = ty1) meta; ty0 - let match_rtys (meta : Meta.meta) _ _ ty0 ty1 = + let match_rtys _ _ ty0 ty1 = (* The types must be equal - in effect, this forbids to match symbolic values containing borrows *) - cassert (ty0 = ty1) meta "The types must be equal - in effect, this forbids to match symbolic values containing borrows"; + sanity_check (ty0 = ty1) meta; ty0 - let match_distinct_literals (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + 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 - let match_distinct_adts (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (ty : ety) + let match_distinct_adts (ctx0 : eval_ctx) (ctx1 : eval_ctx) (ty : ety) (adt0 : adt_value) (adt1 : adt_value) : typed_value = (* Check that the ADTs don't contain borrows - this is redundant with checks performed by the caller, but we prefer to be safe with regards to future updates *) let check_no_borrows ctx (v : typed_value) = - cassert (not (value_has_borrows ctx v.value)) meta "ADTs should not contain borrows" + sanity_check (not (value_has_borrows ctx v.value)) meta in List.iter (check_no_borrows ctx0) adt0.field_values; List.iter (check_no_borrows ctx1) adt1.field_values; @@ -452,7 +454,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* No borrows, no loans, no bottoms: we can introduce a symbolic value *) mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty - let match_shared_borrows (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) match_rec + 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 @@ -508,7 +510,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Return the new borrow *) bid2 - let match_mut_borrows (meta : Meta.meta) (ctx0 : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_mut_borrows (ctx0 : eval_ctx) (_ : eval_ctx) (ty : ety) (bid0 : borrow_id) (bv0 : typed_value) (bid1 : borrow_id) (bv1 : typed_value) (bv : typed_value) : borrow_id * typed_value = if bid0 = bid1 then ( @@ -560,10 +562,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct will update [v], while the backward loop function will return nothing. *) cassert ( - not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) meta "TODO: error message"; + not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) meta "Nested borrows are not supported yet"; if bv0 = bv1 then ( - cassert (bv0 = bv) meta "TODO: error message"; + sanity_check (bv0 = bv) meta; (bid0, bv)) else let rid = fresh_region_id () in @@ -571,7 +573,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let kind = RMut in let bv_ty = bv.ty in - cassert (ty_no_regions bv_ty) meta "TODO: error message"; + sanity_check (ty_no_regions bv_ty) meta; let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in let borrow_av = @@ -624,7 +626,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Generate the avalues for the abstraction *) let mk_aborrow (bid : borrow_id) (bv : typed_value) : typed_avalue = let bv_ty = bv.ty in - cassert (ty_no_regions bv_ty) meta "TODO: error message"; + cassert (ty_no_regions bv_ty) meta "Nested borrows are not supported yet"; let value = ABorrow (AMutBorrow (bid, mk_aignored meta bv_ty)) in { value; ty = borrow_ty } in @@ -654,7 +656,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Return the new borrow *) (bid2, sv) - let match_shared_loans (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety) + let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (ids0 : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) : loan_id_set * typed_value = (* Check if the ids are the same - Rem.: we forbid the sets of loans @@ -671,7 +673,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct raise (ValueMatchFailure (LoansInRight extra_ids_right)); (* This should always be true if we get here *) - cassert (ids0 = ids1) meta "This should always be true if we get here "; + sanity_check (ids0 = ids1) meta; let ids = ids0 in (* Return *) @@ -685,7 +687,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct both borrows *) raise (ValueMatchFailure (LoanInLeft id0)) - let match_symbolic_values (meta : Meta.meta) (ctx0 : eval_ctx) (_ : eval_ctx) + let match_symbolic_values (ctx0 : eval_ctx) (_ : eval_ctx) (sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value = let id0 = sv0.sv_id in let id1 = sv1.sv_id in @@ -697,11 +699,11 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct else ( (* The caller should have checked that the symbolic values don't contain borrows *) - cassert (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) meta "The caller should have checked that the symbolic values don't contain borrows"; + sanity_check (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) meta; (* We simply introduce a fresh symbolic value *) mk_fresh_symbolic_value meta sv0.sv_ty) - let match_symbolic_with_other (meta : Meta.meta) (ctx0 : eval_ctx) (_ : eval_ctx) (left : bool) + let match_symbolic_with_other (ctx0 : eval_ctx) (_ : eval_ctx) (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = (* Check that: - there are no borrows in the symbolic value @@ -729,7 +731,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Return a fresh symbolic value *) mk_fresh_symbolic_typed_value meta sv.sv_ty - let match_bottom_with_other (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) + let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) (v : typed_value) : typed_value = (* If there are outer loans in the non-bottom value, raise an exception. Otherwise, convert it to an abstraction and return [Bottom]. @@ -770,15 +772,15 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* As explained in comments: we don't use the join matcher to join avalues, only concrete values *) - let match_distinct_aadts (meta : Meta.meta) _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_borrows (meta : Meta.meta) _ _ _ _ _ _ = craise meta "Unreachable" - let match_amut_borrows (meta : Meta.meta) _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_distinct_aadts _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_ashared_borrows _ _ _ _ _ _ = craise meta "Unreachable" + let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_loans (meta: Meta.meta) _ _ _ _ _ _ _ _ _ _ _ _ _ = + let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_amut_loans (meta: Meta.meta) _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_avalues (meta: Meta.meta) _ _ _ _ = craise meta "Unreachable" + let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_avalues _ _ _ _ = craise meta "Unreachable" end (* Very annoying: functors only take modules as inputs... *) @@ -788,6 +790,7 @@ module type MatchMoveState = sig (** The moved values *) val nvalues : typed_value list ref + val meta : Meta.meta end (* We use this matcher to move values in environment. @@ -808,40 +811,41 @@ end *) module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (** Small utility *) + let meta = S.meta let push_moved_value (v : typed_value) : unit = S.nvalues := v :: !S.nvalues - let match_etys (meta : Meta.meta) _ _ ty0 ty1 = - cassert (ty0 = ty1) meta "TODO: error message"; + let match_etys _ _ ty0 ty1 = + sanity_check (ty0 = ty1) meta; ty0 - let match_rtys (meta : Meta.meta) _ _ ty0 ty1 = + let match_rtys _ _ ty0 ty1 = (* The types must be equal - in effect, this forbids to match symbolic values containing borrows *) - cassert (ty0 = ty1) meta "The types must be equal - in effect, this forbids to match symbolic values containing borrows"; + sanity_check (ty0 = ty1) meta; ty0 - let match_distinct_literals (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety) (_ : literal) (l : literal) : typed_value = { value = VLiteral l; ty } - let match_distinct_adts (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_distinct_adts (_ : eval_ctx) (_ : eval_ctx) (ty : ety) (_ : adt_value) (adt1 : adt_value) : typed_value = (* Note that if there was a bottom inside the ADT on the left, the value on the left should have been simplified to bottom. *) { ty; value = VAdt adt1 } - let match_shared_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ (_ : ety) + let match_shared_borrows (_ : eval_ctx) (_ : eval_ctx) _ (_ : ety) (_ : borrow_id) (bid1 : borrow_id) : borrow_id = (* There can't be bottoms in shared values *) bid1 - let match_mut_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (_ : borrow_id) + let match_mut_borrows (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (_ : borrow_id) (_ : typed_value) (bid1 : borrow_id) (bv1 : typed_value) (_ : typed_value) : borrow_id * typed_value = (* There can't be bottoms in borrowed values *) (bid1, bv1) - let match_shared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety) + let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (_ : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) : loan_id_set * typed_value = (* There can't be bottoms in shared loans *) @@ -851,15 +855,15 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (id1 : loan_id) : loan_id = id1 - let match_symbolic_values (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : symbolic_value) + let match_symbolic_values (_ : eval_ctx) (_ : eval_ctx) (_ : symbolic_value) (sv1 : symbolic_value) : symbolic_value = sv1 - let match_symbolic_with_other (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (left : bool) + let match_symbolic_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = if left then v else mk_typed_value_from_symbolic_value sv - let match_bottom_with_other (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (left : bool) + let match_bottom_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) (v : typed_value) : typed_value = let with_borrows = false in if left then ( @@ -891,22 +895,21 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (* As explained in comments: we don't use the join matcher to join avalues, only concrete values *) - let match_distinct_aadts (meta : Meta.meta) _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_borrows (meta : Meta.meta) _ _ _ _ _ _ = craise meta "Unreachable" - let match_amut_borrows (meta : Meta.meta) _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_distinct_aadts _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_ashared_borrows _ _ _ _ _ _ = craise meta "Unreachable" + let match_amut_borrows _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_loans (meta : Meta.meta) _ _ _ _ _ _ _ _ _ _ _ _ _ = + let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_amut_loans (meta : Meta.meta) _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_avalues (meta : Meta.meta) _ _ _ _ = craise meta "Unreachable" + let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_avalues _ _ _ _ = craise meta "Unreachable" end module MakeCheckEquivMatcher (S : MatchCheckEquivState) : CheckEquivMatcher = struct module MkGetSetM (Id : Identifiers.Id) = struct module Inj = Id.InjSubst - let add (msg : string) (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) = (* Check if k0 is already registered as a key *) match Inj.find_opt k0 !m with @@ -945,7 +948,7 @@ struct Id.Set.of_list (match_el msg m (Id.Set.elements ks0) (Id.Set.elements ks1)) end - + let meta = S.meta module GetSetRid = MkGetSetM (RegionId) let match_rid = GetSetRid.match_e "match_rid: " S.rid_map @@ -989,10 +992,10 @@ struct let match_aids = GetSetAid.match_es "match_aids: " S.aid_map (** *) - let match_etys (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = + let match_etys (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = if ty0 <> ty1 then raise (Distinct "match_etys") else ty0 - let match_rtys (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = + let match_rtys (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = let match_distinct_types _ _ = raise (Distinct "match_rtys") in let match_regions r0 r1 = match (r0, r1) with @@ -1004,15 +1007,15 @@ struct in match_types meta match_distinct_types match_regions ty0 ty1 - let match_distinct_literals (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + 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 - let match_distinct_adts (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ty : ety) + let match_distinct_adts (_ : eval_ctx) (_ : eval_ctx) (_ty : ety) (_adt0 : adt_value) (_adt1 : adt_value) : typed_value = raise (Distinct "match_distinct_adts") - let match_shared_borrows (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) + let match_shared_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) (match_typed_values : typed_value -> typed_value -> typed_value) (_ty : ety) (bid0 : borrow_id) (bid1 : borrow_id) : borrow_id = log#ldebug @@ -1033,22 +1036,22 @@ struct (lazy ("MakeCheckEquivMatcher: match_shared_borrows: looked up values:" ^ "sv0: " - ^ typed_value_to_string meta ctx0 v0 + ^ typed_value_to_string ~meta:(Some meta) ctx0 v0 ^ ", sv1: " - ^ typed_value_to_string meta ctx1 v1)); + ^ typed_value_to_string ~meta:(Some meta) ctx1 v1)); let _ = match_typed_values v0 v1 in () in bid - let match_mut_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ty : ety) + let match_mut_borrows (_ : eval_ctx) (_ : eval_ctx) (_ty : ety) (bid0 : borrow_id) (_bv0 : typed_value) (bid1 : borrow_id) (_bv1 : typed_value) (bv : typed_value) : borrow_id * typed_value = let bid = match_borrow_id bid0 bid1 in (bid, bv) - let match_shared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety) + let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (ids0 : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) : loan_id_set * typed_value = let ids = match_loan_ids ids0 ids1 in @@ -1058,7 +1061,7 @@ struct (bid1 : loan_id) : loan_id = match_loan_id bid0 bid1 - let match_symbolic_values (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) + let match_symbolic_values (ctx0 : eval_ctx) (ctx1 : eval_ctx) (sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value = let id0 = sv0.sv_id in let id1 = sv1.sv_id in @@ -1077,12 +1080,12 @@ struct let sv_id = GetSetSid.match_e "match_symbolic_values: ids: " S.sid_map id0 id1 in - let sv_ty = match_rtys meta ctx0 ctx1 sv0.sv_ty sv1.sv_ty in + let sv_ty = match_rtys ctx0 ctx1 sv0.sv_ty sv1.sv_ty in let sv = { sv_id; sv_ty } in sv else ( (* Check: fixed values are fixed *) - cassert (id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map)) meta "Fixed values should be fixed"; + sanity_check (id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map)) meta; (* Update the symbolic value mapping *) let sv1 = mk_typed_value_from_symbolic_value sv1 in @@ -1095,21 +1098,21 @@ struct we want *) sv0) - let match_symbolic_with_other (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (left : bool) + let match_symbolic_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = if S.check_equiv then raise (Distinct "match_symbolic_with_other") else ( - cassert left meta "TODO: error message"; + sanity_check left meta; let id = sv.sv_id in (* Check: fixed values are fixed *) - cassert (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) meta "Fixed values should be fixed"; + sanity_check (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) meta; (* Update the binding for the target symbolic value *) S.sid_to_value_map := SymbolicValueId.Map.add_strict id v !S.sid_to_value_map; (* Return - the returned value is not used, so we can return whatever we want *) v) - let match_bottom_with_other (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) + let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) (v : typed_value) : typed_value = (* It can happen that some variables get initialized in some branches and not in some others, which causes problems when matching. *) @@ -1126,47 +1129,47 @@ struct ^ Print.bool_to_string left ^ "\n- value to match with bottom:\n" ^ show_typed_value v)) - let match_distinct_aadts _ _ _ _ _ _ _ _ = + let match_distinct_aadts _ _ _ _ _ _ _ = raise (Distinct "match_distinct_adts") - let match_ashared_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _ty1 bid1 ty + let match_ashared_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _ty1 bid1 ty = let bid = match_borrow_id bid0 bid1 in let value = ABorrow (ASharedBorrow bid) in { value; ty } - let match_amut_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _av0 _ty1 bid1 + let match_amut_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _av0 _ty1 bid1 _av1 ty av = let bid = match_borrow_id bid0 bid1 in let value = ABorrow (AMutBorrow (bid, av)) in { value; ty } - let match_ashared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ty0 ids0 _v0 _av0 _ty1 + let match_ashared_loans (_ : eval_ctx) (_ : eval_ctx) _ty0 ids0 _v0 _av0 _ty1 ids1 _v1 _av1 ty v av = let bids = match_loan_ids ids0 ids1 in let value = ALoan (ASharedLoan (bids, v, av)) in { value; ty } - let match_amut_loans (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 id0 _av0 _ty1 + let match_amut_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 id0 _av0 _ty1 id1 _av1 ty av = log#ldebug (lazy ("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 ctx1 av)); + ^ typed_avalue_to_string ~meta:(Some meta) ctx1 av)); let id = match_loan_id id0 id1 in let value = ALoan (AMutLoan (id, av)) in { value; ty } - let match_avalues (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) v0 v1 = + let match_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx) v0 v1 = log#ldebug (lazy ("avalues don't match:\n- v0: " - ^ typed_avalue_to_string meta ctx0 v0 + ^ typed_avalue_to_string ~meta:(Some meta) ctx0 v0 ^ "\n- v1: " - ^ typed_avalue_to_string meta ctx1 v1)); + ^ typed_avalue_to_string ~meta:(Some meta) ctx1 v1)); raise (Distinct "match_avalues") end @@ -1178,9 +1181,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 ctx0 + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx0 ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter meta ctx1 + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx1 ^ "\n\n")); (* Initialize the maps and instantiate the matcher *) @@ -1222,6 +1225,7 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) in let module S : MatchCheckEquivState = struct + let meta = meta let check_equiv = check_equiv let rid_map = rid_map let blid_map = blid_map @@ -1288,7 +1292,7 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) log#ldebug (lazy "match_abstractions: matching values"); let _ = List.map - (fun (v0, v1) -> M.match_typed_avalues meta ctx0 ctx1 v0 v1) + (fun (v0, v1) -> M.match_typed_avalues ctx0 ctx1 v0 v1) (List.combine avalues0 avalues1) in log#ldebug (lazy "match_abstractions: values matched OK"); @@ -1309,9 +1313,9 @@ 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 { ctx0 with env = List.rev env0 } + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx0 with env = List.rev env0 } ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter meta { ctx1 with env = List.rev env1 } + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx1 with env = List.rev env1 } ^ "\n\n")); match (env0, env1) with @@ -1320,19 +1324,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 *) - cassert (b0 = b1) meta "The fixed values should be equal"; - cassert (v0 = v1) meta "The fixed values should be equal"; + sanity_check (b0 = b1) meta; + sanity_check (v0 = v1) meta; (* The ids present in the left value must be fixed *) let ids, _ = compute_typed_value_ids v0 in - cassert ((not S.check_equiv) || ids_are_fixed ids)) meta "TODO: error message"; + sanity_check ((not S.check_equiv) || ids_are_fixed ids)) meta; (* We still match the values - allows to compute mappings (which are the identity actually) *) - let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in + let _ = M.match_typed_values ctx0 ctx1 v0 v1 in match_envs env0' env1' | EBinding (BVar b0, v0) :: env0', EBinding (BVar b1, v1) :: env1' -> - cassert (b0 = b1) meta "TODO: error message"; + sanity_check (b0 = b1) meta; (* Match the values *) - let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in + let _ = M.match_typed_values ctx0 ctx1 v0 v1 in (* Continue *) match_envs env0' env1' | EAbs abs0 :: env0', EAbs abs1 :: env1' -> @@ -1341,10 +1345,10 @@ 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 *) - cassert (abs0 = abs1) meta "The abstractions should be the same"; + sanity_check (abs0 = abs1) meta; (* Their ids must be fixed *) let ids, _ = compute_abs_ids abs0 in - cassert ((not S.check_equiv) || ids_are_fixed ids) meta "The ids should be fixed"; + sanity_check ((not S.check_equiv) || ids_are_fixed ids) meta; (* Continue *) match_envs env0' env1') else ( @@ -1408,7 +1412,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id (lazy ("prepare_match_ctx_with_target:\n" ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: " - ^ eval_ctx_to_string meta src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string meta tgt_ctx + ^ eval_ctx_to_string ~meta:(Some meta) src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx )); (* End the loans which lead to mismatches when joining *) let rec cf_reorganize_join_tgt : cm_fun = @@ -1437,6 +1441,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id let nabs = ref [] in let module S : MatchJoinState = struct + let meta = meta let loop_id = loop_id let nabs = nabs end in @@ -1448,12 +1453,12 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id (fun (var0, var1) -> match (var0, var1) with | EBinding (BDummy b0, v0), EBinding (BDummy b1, v1) -> - cassert (b0 = b1) meta "TODO: error message"; - let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in + sanity_check (b0 = b1) meta; + let _ = M.match_typed_values src_ctx tgt_ctx v0 v1 in () | EBinding (BVar b0, v0), EBinding (BVar b1, v1) -> - cassert (b0 = b1) meta "TODO: error message"; - let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in + sanity_check (b0 = b1) meta; + let _ = M.match_typed_values src_ctx tgt_ctx v0 v1 in () | _ -> craise meta "Unexpected") (List.combine filt_src_env filt_tgt_env) @@ -1475,6 +1480,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id environment *) let nvalues = ref [] in let module S : MatchMoveState = struct + let meta = meta let loop_id = loop_id let nvalues = nvalues end in @@ -1485,12 +1491,12 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id (fun (var0, var1) -> match (var0, var1) with | EBinding (BDummy b0, v0), EBinding ((BDummy b1 as var1), v1) -> - cassert (b0 = b1) meta "TODO: error message"; - let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in + sanity_check (b0 = b1) meta; + 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) -> - cassert (b0 = b1) meta "TODO: error message"; - let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in + sanity_check (b0 = b1) meta; + let v = M.match_typed_values src_ctx tgt_ctx v0 v1 in (var1, v) | _ -> craise meta "Unexpected") (List.combine filt_src_env filt_tgt_env) @@ -1520,8 +1526,8 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id (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 src_ctx ^ "\n- tgt_ctx: " - ^ eval_ctx_to_string meta tgt_ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) src_ctx ^ "\n- tgt_ctx: " + ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx)); cf tgt_ctx with ValueMatchFailure e -> @@ -1590,7 +1596,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) let filt_src_env, new_absl, new_dummyl = ctx_split_fixed_new meta fixed_ids src_ctx in - cassert (new_dummyl = []) meta "TODO: error message"; + sanity_check (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 @@ -1622,13 +1628,13 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) log#ldebug (lazy ("match_ctx_with_target: cf_introduce_loop_fp_abs:" ^ "\n\n- src_ctx: " - ^ eval_ctx_to_string meta src_ctx ^ "\n\n- tgt_ctx: " - ^ eval_ctx_to_string meta tgt_ctx ^ "\n\n- filt_tgt_ctx: " - ^ eval_ctx_to_string_no_filter meta filt_tgt_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 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 + ^ 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 @@ -1726,7 +1732,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) abstractions and in the *variable bindings* once we allow symbolic values containing borrows to not be eagerly expanded. *) - cassert Config.greedy_expand_symbolics_with_borrows meta "TODO: error message"; + sanity_check Config.greedy_expand_symbolics_with_borrows meta; (* Update the borrows and loans in the abstractions of the target context. @@ -1795,8 +1801,8 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) (* 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 *) - cassert ( - BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id) meta "The borrow should mapped to itself: no mapping means that the borrow was mapped when we matched values (it doesn't come from a fresh abstraction) "; + sanity_check ( + BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id) meta; id | Some id -> id @@ -1808,8 +1814,8 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) method! visit_abs env abs = match abs.kind with | Loop (loop_id', rg_id, kind) -> - cassert (loop_id' = loop_id) meta "TODO: error message"; - cassert (kind = LoopSynthInput) meta "TODO: error message"; + sanity_check (loop_id' = loop_id) meta; + sanity_check (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 @@ -1827,7 +1833,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) log#ldebug (lazy ("match_ctx_with_target: cf_introduce_loop_fp_abs: done:\n\ - - result ctx:\n" ^ eval_ctx_to_string meta tgt_ctx)); + - result ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx)); (* Sanity check *) if !Config.sanity_checks then -- cgit v1.2.3 From 53347ecc40b308b0b75a620453bfa8bd520a2c70 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 16:31:24 +0100 Subject: changes after git rebase main --- compiler/InterpreterLoopsMatchCtxs.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'compiler/InterpreterLoopsMatchCtxs.ml') diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index c02d3117..24e588f2 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -459,8 +459,8 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* 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 ctx0 bid0 in - let sv1 = lookup_shared_value ctx1 bid1 in + let sv0 = lookup_shared_value meta ctx0 bid0 in + let sv1 = lookup_shared_value meta ctx1 bid1 in let sv = match_rec sv0 sv1 in if bid0 = bid1 then bid0 else @@ -1544,7 +1544,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id (* Apply the reorganization *) cf_reorganize_join_tgt cf tgt_ctx -let match_ctx_with_target (config : config) (loop_id : LoopId.id) +let match_ctx_with_target (config : config) (meta : Meta.meta) (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 = @@ -1562,7 +1562,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) were introduced during the loop iterations) *) let cf_reorganize_join_tgt = - prepare_match_ctx_with_target config loop_id fixed_ids src_ctx + prepare_match_ctx_with_target config meta loop_id fixed_ids src_ctx in (* Introduce the "identity" abstractions for the loop re-entry. -- cgit v1.2.3 From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 17:14:27 +0100 Subject: formatting --- compiler/InterpreterLoopsMatchCtxs.ml | 203 ++++++++++++++++++++-------------- 1 file changed, 119 insertions(+), 84 deletions(-) (limited to 'compiler/InterpreterLoopsMatchCtxs.ml') diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 24e588f2..1a6e6926 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -43,8 +43,9 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) match Id0.Map.find_opt id0 !map with | None -> () | Some set -> - sanity_check ( - (not check_not_already_registered) || not (Id1.Set.mem id1 set)) meta); + sanity_check + ((not check_not_already_registered) || not (Id1.Set.mem id1 set)) + meta); (* Update the mapping *) map := Id0.Map.update id0 @@ -54,9 +55,10 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) | Some ids -> (* Sanity check *) sanity_check (not check_singleton_sets) meta; - sanity_check ( - (not check_not_already_registered) - || not (Id1.Set.mem id1 ids)) meta; + sanity_check + ((not check_not_already_registered) + || not (Id1.Set.mem id1 ids)) + meta; (* Update *) Some (Id1.Set.add id1 ids)) !map @@ -107,8 +109,7 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) -> (* Ignore the id of the borrow, if there is *) self#visit_typed_avalue abs_id child - | AEndedMutBorrow _ | AEndedSharedBorrow -> - craise meta "Unreachable" + | AEndedMutBorrow _ | AEndedSharedBorrow -> craise meta "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 @@ -185,6 +186,7 @@ let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty) module MakeMatcher (M : PrimMatcher) : Matcher = struct let meta = M.meta + let rec match_typed_values (ctx0 : eval_ctx) (ctx1 : eval_ctx) (v0 : typed_value) (v1 : typed_value) : typed_value = let match_rec = match_typed_values ctx0 ctx1 in @@ -227,10 +229,11 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct | VMutBorrow (bid0, bv0), VMutBorrow (bid1, bv1) -> let bv = match_rec bv0 bv1 in - cassert ( - not - (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos - bv.value)) M.meta "TODO: error message"; + cassert + (not + (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos + bv.value)) + M.meta "TODO: error message"; let bid, bv = M.match_mut_borrows ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv in @@ -253,7 +256,9 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct match (lc0, lc1) with | VSharedLoan (ids0, sv0), VSharedLoan (ids1, sv1) -> let sv = match_rec sv0 sv1 in - cassert (not (value_has_borrows sv.value)) M.meta "TODO: error message"; + cassert + (not (value_has_borrows sv.value)) + M.meta "TODO: error message"; let ids, sv = M.match_shared_loans ctx0 ctx1 ty ids0 ids1 sv in VSharedLoan (ids, sv) | VMutLoan id0, VMutLoan id1 -> @@ -266,8 +271,16 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct | VSymbolic sv0, VSymbolic sv1 -> (* For now, we force all the symbolic values containing borrows to be eagerly expanded, and we don't support nested borrows *) - cassert (not (value_has_borrows v0.value)) M.meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded"; - cassert (not (value_has_borrows v1.value)) M.meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded"; + cassert + (not (value_has_borrows v0.value)) + M.meta + "Nested borrows are not supported yet and all the symbolic values \ + containing borrows are currently forced to be eagerly expanded"; + cassert + (not (value_has_borrows v1.value)) + M.meta + "Nested borrows are not supported yet and all the symbolic values \ + containing borrows are currently forced to be eagerly expanded"; (* Match *) let sv = M.match_symbolic_values ctx0 ctx1 sv0 sv1 in { v1 with value = VSymbolic sv } @@ -401,25 +414,25 @@ end module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (** Small utility *) let meta = S.meta - let push_abs (abs : abs) : unit = S.nabs := abs :: !S.nabs + 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 = + let match_etys _ _ ty0 ty1 = sanity_check (ty0 = ty1) meta; ty0 - let match_rtys _ _ ty0 ty1 = + let match_rtys _ _ ty0 ty1 = (* The types must be equal - in effect, this forbids to match symbolic values containing borrows *) sanity_check (ty0 = ty1) meta; ty0 - let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + 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 - let match_distinct_adts (ctx0 : eval_ctx) (ctx1 : eval_ctx) (ty : ety) + let match_distinct_adts (ctx0 : eval_ctx) (ctx1 : eval_ctx) (ty : ety) (adt0 : adt_value) (adt1 : adt_value) : typed_value = (* Check that the ADTs don't contain borrows - this is redundant with checks performed by the caller, but we prefer to be safe with regards to future @@ -454,7 +467,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* No borrows, no loans, no bottoms: we can introduce a symbolic value *) mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty - let match_shared_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) match_rec + 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 @@ -510,7 +523,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Return the new borrow *) bid2 - let match_mut_borrows (ctx0 : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_mut_borrows (ctx0 : eval_ctx) (_ : eval_ctx) (ty : ety) (bid0 : borrow_id) (bv0 : typed_value) (bid1 : borrow_id) (bv1 : typed_value) (bv : typed_value) : borrow_id * typed_value = if bid0 = bid1 then ( @@ -561,8 +574,9 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct do so, we won't introduce reborrows like above: the forward loop function will update [v], while the backward loop function will return nothing. *) - cassert ( - not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) meta "Nested borrows are not supported yet"; + cassert + (not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) + meta "Nested borrows are not supported yet"; if bv0 = bv1 then ( sanity_check (bv0 = bv) meta; @@ -626,7 +640,8 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Generate the avalues for the abstraction *) let mk_aborrow (bid : borrow_id) (bv : typed_value) : typed_avalue = let bv_ty = bv.ty in - cassert (ty_no_regions bv_ty) meta "Nested borrows are not supported yet"; + cassert (ty_no_regions bv_ty) meta + "Nested borrows are not supported yet"; let value = ABorrow (AMutBorrow (bid, mk_aignored meta bv_ty)) in { value; ty = borrow_ty } in @@ -656,7 +671,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Return the new borrow *) (bid2, sv) - let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety) + let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (ids0 : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) : loan_id_set * typed_value = (* Check if the ids are the same - Rem.: we forbid the sets of loans @@ -687,7 +702,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct both borrows *) raise (ValueMatchFailure (LoanInLeft id0)) - let match_symbolic_values (ctx0 : eval_ctx) (_ : eval_ctx) + let match_symbolic_values (ctx0 : eval_ctx) (_ : eval_ctx) (sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value = let id0 = sv0.sv_id in let id1 = sv1.sv_id in @@ -699,11 +714,13 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct else ( (* The caller should have checked that the symbolic values don't contain borrows *) - sanity_check (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) meta; + sanity_check + (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) + meta; (* We simply introduce a fresh symbolic value *) mk_fresh_symbolic_value meta sv0.sv_ty) - let match_symbolic_with_other (ctx0 : eval_ctx) (_ : eval_ctx) (left : bool) + let match_symbolic_with_other (ctx0 : eval_ctx) (_ : eval_ctx) (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = (* Check that: - there are no borrows in the symbolic value @@ -711,14 +728,20 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct If there are loans in the regular value, raise an exception. *) let type_infos = ctx0.type_ctx.type_infos in - cassert (not (ty_has_borrows type_infos sv.sv_ty)) meta "Check that: - - there are no borrows in the symbolic value - - there are no borrows in the \"regular\" value - If there are loans in the regular value, raise an exception."; - cassert (not (ValuesUtils.value_has_borrows type_infos v.value)) meta "Check that: - - there are no borrows in the symbolic value - - there are no borrows in the \"regular\" value - If there are loans in the regular value, raise an exception."; + cassert + (not (ty_has_borrows type_infos sv.sv_ty)) + meta + "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 + (not (ValuesUtils.value_has_borrows type_infos v.value)) + meta + "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."; let value_is_left = not left in (match InterpreterBorrowsCore.get_first_loan_in_value v with | None -> () @@ -731,7 +754,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Return a fresh symbolic value *) mk_fresh_symbolic_typed_value meta sv.sv_ty - let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) + let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) (v : typed_value) : typed_value = (* If there are outer loans in the non-bottom value, raise an exception. Otherwise, convert it to an abstraction and return [Bottom]. @@ -775,10 +798,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let match_distinct_aadts _ _ _ _ _ _ _ = craise meta "Unreachable" let match_ashared_borrows _ _ _ _ _ _ = craise meta "Unreachable" let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - - let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = - craise meta "Unreachable" - + let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" let match_avalues _ _ _ _ = craise meta "Unreachable" end @@ -790,6 +810,7 @@ module type MatchMoveState = sig (** The moved values *) val nvalues : typed_value list ref + val meta : Meta.meta end @@ -812,13 +833,14 @@ end module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (** Small utility *) let meta = S.meta + let push_moved_value (v : typed_value) : unit = S.nvalues := v :: !S.nvalues - let match_etys _ _ ty0 ty1 = + let match_etys _ _ ty0 ty1 = sanity_check (ty0 = ty1) meta; ty0 - let match_rtys _ _ ty0 ty1 = + let match_rtys _ _ ty0 ty1 = (* The types must be equal - in effect, this forbids to match symbolic values containing borrows *) sanity_check (ty0 = ty1) meta; @@ -863,7 +885,7 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (sv : symbolic_value) (v : typed_value) : typed_value = if left then v else mk_typed_value_from_symbolic_value sv - let match_bottom_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) + let match_bottom_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) (v : typed_value) : typed_value = let with_borrows = false in if left then ( @@ -898,18 +920,16 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct let match_distinct_aadts _ _ _ _ _ _ _ = craise meta "Unreachable" let match_ashared_borrows _ _ _ _ _ _ = craise meta "Unreachable" let match_amut_borrows _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - - let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = - craise meta "Unreachable" - - let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_avalues _ _ _ _ = craise meta "Unreachable" + let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_avalues _ _ _ _ = craise meta "Unreachable" end module MakeCheckEquivMatcher (S : MatchCheckEquivState) : CheckEquivMatcher = struct module MkGetSetM (Id : Identifiers.Id) = struct module Inj = Id.InjSubst + let add (msg : string) (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) = (* Check if k0 is already registered as a key *) match Inj.find_opt k0 !m with @@ -948,7 +968,9 @@ struct Id.Set.of_list (match_el msg m (Id.Set.elements ks0) (Id.Set.elements ks1)) end + let meta = S.meta + module GetSetRid = MkGetSetM (RegionId) let match_rid = GetSetRid.match_e "match_rid: " S.rid_map @@ -995,7 +1017,7 @@ struct let match_etys (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = if ty0 <> ty1 then raise (Distinct "match_etys") else ty0 - let match_rtys (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = + let match_rtys (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = let match_distinct_types _ _ = raise (Distinct "match_rtys") in let match_regions r0 r1 = match (r0, r1) with @@ -1007,7 +1029,7 @@ struct in match_types meta match_distinct_types match_regions ty0 ty1 - let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + 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 @@ -1015,7 +1037,7 @@ struct (_adt0 : adt_value) (_adt1 : adt_value) : typed_value = raise (Distinct "match_distinct_adts") - let match_shared_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) + let match_shared_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) (match_typed_values : typed_value -> typed_value -> typed_value) (_ty : ety) (bid0 : borrow_id) (bid1 : borrow_id) : borrow_id = log#ldebug @@ -1061,7 +1083,7 @@ struct (bid1 : loan_id) : loan_id = match_loan_id bid0 bid1 - let match_symbolic_values (ctx0 : eval_ctx) (ctx1 : eval_ctx) + let match_symbolic_values (ctx0 : eval_ctx) (ctx1 : eval_ctx) (sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value = let id0 = sv0.sv_id in let id1 = sv1.sv_id in @@ -1085,7 +1107,9 @@ struct sv else ( (* Check: fixed values are fixed *) - sanity_check (id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map)) meta; + sanity_check + (id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map)) + meta; (* Update the symbolic value mapping *) let sv1 = mk_typed_value_from_symbolic_value sv1 in @@ -1098,7 +1122,7 @@ struct we want *) sv0) - let match_symbolic_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) + let match_symbolic_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = if S.check_equiv then raise (Distinct "match_symbolic_with_other") else ( @@ -1112,7 +1136,7 @@ struct (* Return - the returned value is not used, so we can return whatever we want *) v) - let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) + let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) (v : typed_value) : typed_value = (* It can happen that some variables get initialized in some branches and not in some others, which causes problems when matching. *) @@ -1121,7 +1145,8 @@ struct a continue, where the fixed point contains some bottom values. *) 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 + if left && not (value_has_loans_or_borrows ctx v.value) then + mk_bottom meta v.ty else raise (Distinct @@ -1150,7 +1175,7 @@ struct let value = ALoan (ASharedLoan (bids, v, av)) in { value; ty } - let match_amut_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 id0 _av0 _ty1 + let match_amut_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 id0 _av0 _ty1 id1 _av1 ty av = log#ldebug (lazy @@ -1163,7 +1188,7 @@ struct let value = ALoan (AMutLoan (id, av)) in { value; ty } - let match_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx) v0 v1 = + let match_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx) v0 v1 = log#ldebug (lazy ("avalues don't match:\n- v0: " @@ -1313,22 +1338,25 @@ 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) { ctx0 with env = List.rev env0 } + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) + { ctx0 with env = List.rev env0 } ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx1 with env = List.rev env1 } + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) + { ctx1 with env = List.rev env1 } ^ "\n\n")); match (env0, env1) with | EBinding (BDummy b0, v0) :: env0', EBinding (BDummy b1, v1) :: env1' -> (* Sanity check: if the dummy value is an old value, the bindings must 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 (b0 = b1) meta; - sanity_check (v0 = v1) meta; - (* The ids present in the left value must be fixed *) - let ids, _ = compute_typed_value_ids v0 in - sanity_check ((not S.check_equiv) || ids_are_fixed ids)) meta; + if DummyVarId.Set.mem b0 fixed_ids.dids then + ((* Fixed values: the values must be equal *) + sanity_check (b0 = b1) meta; + sanity_check (v0 = v1) meta; + (* The ids present in the left value must be fixed *) + let ids, _ = compute_typed_value_ids v0 in + sanity_check ((not S.check_equiv) || ids_are_fixed ids)) + meta; (* We still match the values - allows to compute mappings (which are the identity actually) *) let _ = M.match_typed_values ctx0 ctx1 v0 v1 in @@ -1396,24 +1424,25 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) log#ldebug (lazy ("match_ctxs: distinct: " ^ msg)); None -let ctxs_are_equivalent (meta : Meta.meta) (fixed_ids : ids_sets) (ctx0 : eval_ctx) - (ctx1 : eval_ctx) : bool = +let ctxs_are_equivalent (meta : Meta.meta) (fixed_ids : ids_sets) + (ctx0 : eval_ctx) (ctx1 : eval_ctx) : bool = let check_equivalent = true in let lookup_shared_value _ = craise meta "Unreachable" in Option.is_some (match_ctxs meta check_equivalent fixed_ids lookup_shared_value lookup_shared_value ctx0 ctx1) -let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id : LoopId.id) - (fixed_ids : ids_sets) (src_ctx : eval_ctx) : cm_fun = +let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) + (loop_id : LoopId.id) (fixed_ids : ids_sets) (src_ctx : eval_ctx) : cm_fun = fun cf 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 ^ "\n- tgt_ctx: " ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx - )); + ^ eval_ctx_to_string ~meta:(Some meta) src_ctx + ^ "\n- tgt_ctx: " + ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx)); (* End the loans which lead to mismatches when joining *) let rec cf_reorganize_join_tgt : cm_fun = fun cf tgt_ctx -> @@ -1526,8 +1555,9 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id (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 ^ "\n- tgt_ctx: " - ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) src_ctx + ^ "\n- tgt_ctx: " + ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx)); cf tgt_ctx with ValueMatchFailure e -> @@ -1544,8 +1574,9 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id (* Apply the reorganization *) cf_reorganize_join_tgt cf tgt_ctx -let match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id : LoopId.id) - (is_loop_entry : bool) (fp_bl_maps : borrow_loan_corresp) +let match_ctx_with_target (config : config) (meta : Meta.meta) + (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 -> @@ -1628,8 +1659,10 @@ let match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id : LoopId 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 ~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 @@ -1801,8 +1834,9 @@ let match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id : LoopId (* 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 ( - BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id) meta; + sanity_check + (BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id) + meta; id | Some id -> id @@ -1833,7 +1867,8 @@ let match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id : LoopId 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)); + - result ctx:\n" + ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx)); (* Sanity check *) if !Config.sanity_checks then -- cgit v1.2.3 From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 29 Mar 2024 13:21:08 +0100 Subject: added file and line arg to craise and cassert --- compiler/InterpreterLoopsMatchCtxs.ml | 162 +++++++++++++++++----------------- 1 file changed, 81 insertions(+), 81 deletions(-) (limited to 'compiler/InterpreterLoopsMatchCtxs.ml') diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 1a6e6926..9c017f19 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -43,7 +43,7 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) match Id0.Map.find_opt id0 !map with | None -> () | Some set -> - sanity_check + sanity_check __FILE__ __LINE__ ((not check_not_already_registered) || not (Id1.Set.mem id1 set)) meta); (* Update the mapping *) @@ -54,8 +54,8 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) | None -> Some (Id1.Set.singleton id1) | Some ids -> (* Sanity check *) - sanity_check (not check_singleton_sets) meta; - sanity_check + sanity_check __FILE__ __LINE__ (not check_singleton_sets) meta; + sanity_check __FILE__ __LINE__ ((not check_not_already_registered) || not (Id1.Set.mem id1 ids)) meta; @@ -96,7 +96,7 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) | AIgnoredSharedLoan child -> (* Ignore the id of the loan, if there is *) self#visit_typed_avalue abs_id child - | AEndedMutLoan _ | AEndedSharedLoan _ -> craise meta "Unreachable" + | AEndedMutLoan _ | AEndedSharedLoan _ -> craise __FILE__ __LINE__ meta "Unreachable" (** Make sure we don't register the ignored ids *) method! visit_aborrow_content abs_id bc = @@ -109,7 +109,7 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) -> (* Ignore the id of the borrow, if there is *) self#visit_typed_avalue abs_id child - | AEndedMutBorrow _ | AEndedSharedBorrow -> craise meta "Unreachable" + | AEndedMutBorrow _ | AEndedSharedBorrow -> craise __FILE__ __LINE__ meta "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 @@ -150,9 +150,9 @@ let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty) let match_rec = match_types meta match_distinct_types match_regions in match (ty0, ty1) with | TAdt (id0, generics0), TAdt (id1, generics1) -> - sanity_check (id0 = id1) meta; - sanity_check (generics0.const_generics = generics1.const_generics) meta; - sanity_check (generics0.trait_refs = generics1.trait_refs) meta; + sanity_check __FILE__ __LINE__ (id0 = id1) meta; + sanity_check __FILE__ __LINE__ (generics0.const_generics = generics1.const_generics) meta; + sanity_check __FILE__ __LINE__ (generics0.trait_refs = generics1.trait_refs) meta; let id = id0 in let const_generics = generics1.const_generics in let trait_refs = generics1.trait_refs in @@ -169,17 +169,17 @@ 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 (vid0 = vid1) meta; + sanity_check __FILE__ __LINE__ (vid0 = vid1) meta; let vid = vid0 in TVar vid | TLiteral lty0, TLiteral lty1 -> - sanity_check (lty0 = lty1) meta; + sanity_check __FILE__ __LINE__ (lty0 = lty1) meta; 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 (k0 = k1) meta; + sanity_check __FILE__ __LINE__ (k0 = k1) meta; let k = k0 in TRef (r, ty, k) | _ -> match_distinct_types ty0 ty1 @@ -213,8 +213,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct { value; ty = v1.ty } else ( (* For now, we don't merge ADTs which contain borrows *) - sanity_check (not (value_has_borrows v0.value)) M.meta; - sanity_check (not (value_has_borrows v1.value)) M.meta; + sanity_check __FILE__ __LINE__ (not (value_has_borrows v0.value)) M.meta; + sanity_check __FILE__ __LINE__ (not (value_has_borrows v1.value)) M.meta; (* Merge *) M.match_distinct_adts ctx0 ctx1 ty av0 av1) | VBottom, VBottom -> v0 @@ -229,7 +229,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct | VMutBorrow (bid0, bv0), VMutBorrow (bid1, bv1) -> let bv = match_rec bv0 bv1 in - cassert + cassert __FILE__ __LINE__ (not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) @@ -246,7 +246,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 M.meta "Unexpected" + craise __FILE__ __LINE__ M.meta "Unexpected" in { value = VBorrow bc; ty } | VLoan lc0, VLoan lc1 -> @@ -256,7 +256,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct match (lc0, lc1) with | VSharedLoan (ids0, sv0), VSharedLoan (ids1, sv1) -> let sv = match_rec sv0 sv1 in - cassert + cassert __FILE__ __LINE__ (not (value_has_borrows sv.value)) M.meta "TODO: error message"; let ids, sv = M.match_shared_loans ctx0 ctx1 ty ids0 ids1 sv in @@ -265,18 +265,18 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let id = M.match_mut_loans ctx0 ctx1 ty id0 id1 in VMutLoan id | VSharedLoan _, VMutLoan _ | VMutLoan _, VSharedLoan _ -> - craise M.meta "Unreachable" + craise __FILE__ __LINE__ M.meta "Unreachable" in { value = VLoan lc; ty = v1.ty } | VSymbolic sv0, VSymbolic sv1 -> (* For now, we force all the symbolic values containing borrows to be eagerly expanded, and we don't support nested borrows *) - cassert + cassert __FILE__ __LINE__ (not (value_has_borrows v0.value)) M.meta "Nested borrows are not supported yet and all the symbolic values \ containing borrows are currently forced to be eagerly expanded"; - cassert + cassert __FILE__ __LINE__ (not (value_has_borrows v1.value)) M.meta "Nested borrows are not supported yet and all the symbolic values \ @@ -303,7 +303,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct ^ typed_value_to_string ~meta:(Some M.meta) ctx0 v0 ^ "\n- value1: " ^ typed_value_to_string ~meta:(Some M.meta) ctx1 v1)); - craise M.meta "Unexpected match case" + craise __FILE__ __LINE__ M.meta "Unexpected match case" and match_typed_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx) (v0 : typed_avalue) (v1 : typed_avalue) : typed_avalue = @@ -357,7 +357,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 M.meta "Unexpected" + craise __FILE__ __LINE__ M.meta "Unexpected" | AProjSharedBorrow asb0, AProjSharedBorrow asb1 -> ( match (asb0, asb1) with | [], [] -> @@ -366,7 +366,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct v0 | _ -> (* We should get there only if there are nested borrows *) - craise M.meta "Unexpected") + craise __FILE__ __LINE__ M.meta "Unexpected") | _ -> (* TODO: getting there is not necessarily inconsistent (it may just be because the environments don't match) so we may want @@ -377,7 +377,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct we are *currently* ending it, in which case we need to completely end it before continuing. *) - craise M.meta "Unexpected") + craise __FILE__ __LINE__ M.meta "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 - @@ -387,7 +387,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct log#ldebug (lazy "match_typed_avalues: shared loans"); let sv = match_rec sv0 sv1 in let av = match_arec av0 av1 in - sanity_check (not (value_has_borrows sv.value)) M.meta; + sanity_check __FILE__ __LINE__ (not (value_has_borrows sv.value)) M.meta; 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) -> @@ -402,12 +402,12 @@ 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 M.meta "Unreachable" - | _ -> craise M.meta "Unreachable") + craise __FILE__ __LINE__ M.meta "Unreachable" + | _ -> craise __FILE__ __LINE__ M.meta "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 M.meta "Unreachable" + craise __FILE__ __LINE__ M.meta "Unreachable" | _ -> M.match_avalues ctx0 ctx1 v0 v1 end @@ -419,13 +419,13 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let push_absl (absl : abs list) : unit = List.iter push_abs absl let match_etys _ _ ty0 ty1 = - sanity_check (ty0 = ty1) meta; + sanity_check __FILE__ __LINE__ (ty0 = ty1) meta; ty0 let match_rtys _ _ ty0 ty1 = (* The types must be equal - in effect, this forbids to match symbolic values containing borrows *) - sanity_check (ty0 = ty1) meta; + sanity_check __FILE__ __LINE__ (ty0 = ty1) meta; ty0 let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety) @@ -439,7 +439,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct updates *) let check_no_borrows ctx (v : typed_value) = - sanity_check (not (value_has_borrows ctx v.value)) meta + sanity_check __FILE__ __LINE__ (not (value_has_borrows ctx v.value)) meta in List.iter (check_no_borrows ctx0) adt0.field_values; List.iter (check_no_borrows ctx1) adt1.field_values; @@ -574,12 +574,12 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct do so, we won't introduce reborrows like above: the forward loop function will update [v], while the backward loop function will return nothing. *) - cassert + cassert __FILE__ __LINE__ (not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) meta "Nested borrows are not supported yet"; if bv0 = bv1 then ( - sanity_check (bv0 = bv) meta; + sanity_check __FILE__ __LINE__ (bv0 = bv) meta; (bid0, bv)) else let rid = fresh_region_id () in @@ -587,7 +587,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let kind = RMut in let bv_ty = bv.ty in - sanity_check (ty_no_regions bv_ty) meta; + sanity_check __FILE__ __LINE__ (ty_no_regions bv_ty) meta; let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in let borrow_av = @@ -640,7 +640,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Generate the avalues for the abstraction *) let mk_aborrow (bid : borrow_id) (bv : typed_value) : typed_avalue = let bv_ty = bv.ty in - cassert (ty_no_regions bv_ty) meta + cassert __FILE__ __LINE__ (ty_no_regions bv_ty) meta "Nested borrows are not supported yet"; let value = ABorrow (AMutBorrow (bid, mk_aignored meta bv_ty)) in { value; ty = borrow_ty } @@ -688,7 +688,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct raise (ValueMatchFailure (LoansInRight extra_ids_right)); (* This should always be true if we get here *) - sanity_check (ids0 = ids1) meta; + sanity_check __FILE__ __LINE__ (ids0 = ids1) meta; let ids = ids0 in (* Return *) @@ -708,13 +708,13 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let id1 = sv1.sv_id in if id0 = id1 then ( (* Sanity check *) - sanity_check (sv0 = sv1) meta; + sanity_check __FILE__ __LINE__ (sv0 = sv1) meta; (* Return *) sv0) else ( (* The caller should have checked that the symbolic values don't contain borrows *) - sanity_check + sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) meta; (* We simply introduce a fresh symbolic value *) @@ -728,14 +728,14 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct If there are loans in the regular value, raise an exception. *) let type_infos = ctx0.type_ctx.type_infos in - cassert + cassert __FILE__ __LINE__ (not (ty_has_borrows type_infos sv.sv_ty)) meta "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 + cassert __FILE__ __LINE__ (not (ValuesUtils.value_has_borrows type_infos v.value)) meta "Check that:\n\ @@ -767,7 +767,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct with | Some (BorrowContent _) -> (* Can't get there: we only ask for outer *loans* *) - craise meta "Unreachable" + craise __FILE__ __LINE__ meta "Unreachable" | Some (LoanContent lc) -> ( match lc with | VSharedLoan (ids, _) -> @@ -795,12 +795,12 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* As explained in comments: we don't use the join matcher to join avalues, only concrete values *) - let match_distinct_aadts _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_borrows _ _ _ _ _ _ = craise meta "Unreachable" - let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_avalues _ _ _ _ = craise meta "Unreachable" + let match_distinct_aadts _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_ashared_borrows _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_avalues _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" end (* Very annoying: functors only take modules as inputs... *) @@ -837,13 +837,13 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct let push_moved_value (v : typed_value) : unit = S.nvalues := v :: !S.nvalues let match_etys _ _ ty0 ty1 = - sanity_check (ty0 = ty1) meta; + sanity_check __FILE__ __LINE__ (ty0 = ty1) meta; ty0 let match_rtys _ _ ty0 ty1 = (* The types must be equal - in effect, this forbids to match symbolic values containing borrows *) - sanity_check (ty0 = ty1) meta; + sanity_check __FILE__ __LINE__ (ty0 = ty1) meta; ty0 let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety) @@ -897,10 +897,10 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct with | Some (BorrowContent _) -> (* Can't get there: we only ask for outer *loans* *) - craise meta "Unreachable" + craise __FILE__ __LINE__ meta "Unreachable" | Some (LoanContent _) -> (* We should have ended all the outer loans *) - craise meta "Unexpected outer loan" + craise __FILE__ __LINE__ meta "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. *) @@ -912,17 +912,17 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct 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 meta "Unreachable" + craise __FILE__ __LINE__ meta "Unreachable" (* As explained in comments: we don't use the join matcher to join avalues, only concrete values *) - let match_distinct_aadts _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_borrows _ _ _ _ _ _ = craise meta "Unreachable" - let match_amut_borrows _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_avalues _ _ _ _ = craise meta "Unreachable" + let match_distinct_aadts _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_ashared_borrows _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_amut_borrows _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_avalues _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" end module MakeCheckEquivMatcher (S : MatchCheckEquivState) : CheckEquivMatcher = @@ -1107,7 +1107,7 @@ struct sv else ( (* Check: fixed values are fixed *) - sanity_check + sanity_check __FILE__ __LINE__ (id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map)) meta; @@ -1126,10 +1126,10 @@ struct (sv : symbolic_value) (v : typed_value) : typed_value = if S.check_equiv then raise (Distinct "match_symbolic_with_other") else ( - sanity_check left meta; + sanity_check __FILE__ __LINE__ left meta; let id = sv.sv_id in (* Check: fixed values are fixed *) - sanity_check (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) meta; + sanity_check __FILE__ __LINE__ (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) meta; (* Update the binding for the target symbolic value *) S.sid_to_value_map := SymbolicValueId.Map.add_strict id v !S.sid_to_value_map; @@ -1351,18 +1351,18 @@ 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 (b0 = b1) meta; - sanity_check (v0 = v1) meta; + sanity_check __FILE__ __LINE__ (b0 = b1) meta; + sanity_check __FILE__ __LINE__ (v0 = v1) meta; (* The ids present in the left value must be fixed *) let ids, _ = compute_typed_value_ids v0 in - sanity_check ((not S.check_equiv) || ids_are_fixed ids)) + sanity_check __FILE__ __LINE__ ((not S.check_equiv) || ids_are_fixed ids)) meta; (* 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 (b0 = b1) meta; + sanity_check __FILE__ __LINE__ (b0 = b1) meta; (* Match the values *) let _ = M.match_typed_values ctx0 ctx1 v0 v1 in (* Continue *) @@ -1373,10 +1373,10 @@ 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 (abs0 = abs1) meta; + sanity_check __FILE__ __LINE__ (abs0 = abs1) meta; (* Their ids must be fixed *) let ids, _ = compute_abs_ids abs0 in - sanity_check ((not S.check_equiv) || ids_are_fixed ids) meta; + sanity_check __FILE__ __LINE__ ((not S.check_equiv) || ids_are_fixed ids) meta; (* Continue *) match_envs env0' env1') else ( @@ -1404,7 +1404,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 meta "Unreachable" + | _ -> craise __FILE__ __LINE__ meta "Unreachable" in match_envs env0 env1; @@ -1427,7 +1427,7 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) let ctxs_are_equivalent (meta : Meta.meta) (fixed_ids : ids_sets) (ctx0 : eval_ctx) (ctx1 : eval_ctx) : bool = let check_equivalent = true in - let lookup_shared_value _ = craise meta "Unreachable" in + let lookup_shared_value _ = craise __FILE__ __LINE__ meta "Unreachable" in Option.is_some (match_ctxs meta check_equivalent fixed_ids lookup_shared_value lookup_shared_value ctx0 ctx1) @@ -1482,14 +1482,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 (b0 = b1) meta; + sanity_check __FILE__ __LINE__ (b0 = b1) meta; let _ = M.match_typed_values src_ctx tgt_ctx v0 v1 in () | EBinding (BVar b0, v0), EBinding (BVar b1, v1) -> - sanity_check (b0 = b1) meta; + sanity_check __FILE__ __LINE__ (b0 = b1) meta; let _ = M.match_typed_values src_ctx tgt_ctx v0 v1 in () - | _ -> craise meta "Unexpected") + | _ -> craise __FILE__ __LINE__ meta "Unexpected") (List.combine filt_src_env filt_tgt_env) in (* No exception was thrown: continue *) @@ -1520,14 +1520,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 (b0 = b1) meta; + sanity_check __FILE__ __LINE__ (b0 = b1) meta; 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 (b0 = b1) meta; + sanity_check __FILE__ __LINE__ (b0 = b1) meta; let v = M.match_typed_values src_ctx tgt_ctx v0 v1 in (var1, v) - | _ -> craise meta "Unexpected") + | _ -> craise __FILE__ __LINE__ meta "Unexpected") (List.combine filt_src_env filt_tgt_env) in let var_to_new_val = BinderMap.of_list var_to_new_val in @@ -1567,7 +1567,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) | LoanInRight bid -> InterpreterBorrows.end_borrow config meta bid | LoansInRight bids -> InterpreterBorrows.end_borrows config meta bids | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ -> - craise meta "Unexpected" + craise __FILE__ __LINE__ meta "Unexpected" in comp cc cf_reorganize_join_tgt cf tgt_ctx in @@ -1627,7 +1627,7 @@ let match_ctx_with_target (config : config) (meta : Meta.meta) let filt_src_env, new_absl, new_dummyl = ctx_split_fixed_new meta fixed_ids src_ctx in - sanity_check (new_dummyl = []) meta; + 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 @@ -1639,7 +1639,7 @@ let match_ctx_with_target (config : config) (meta : Meta.meta) match snd (lookup_loan meta ek_all lid ctx) with | Concrete (VSharedLoan (_, v)) -> v | Abstract (ASharedLoan (_, v, _)) -> v - | _ -> craise meta "Unreachable" + | _ -> 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 @@ -1765,7 +1765,7 @@ let match_ctx_with_target (config : config) (meta : Meta.meta) abstractions and in the *variable bindings* once we allow symbolic values containing borrows to not be eagerly expanded. *) - sanity_check Config.greedy_expand_symbolics_with_borrows meta; + sanity_check __FILE__ __LINE__ Config.greedy_expand_symbolics_with_borrows meta; (* Update the borrows and loans in the abstractions of the target context. @@ -1834,7 +1834,7 @@ let match_ctx_with_target (config : config) (meta : Meta.meta) (* 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 + sanity_check __FILE__ __LINE__ (BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id) meta; id @@ -1848,8 +1848,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 (loop_id' = loop_id) meta; - sanity_check (kind = LoopSynthInput) meta; + 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 -- cgit v1.2.3 From 8f969634f3f192a9282a21a1ca2a1b6a676984ca Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 29 Mar 2024 14:07:36 +0100 Subject: formatting and changed save_error condition for failing from b to not b --- compiler/InterpreterLoopsMatchCtxs.ml | 80 ++++++++++++++++++++++++++--------- 1 file changed, 59 insertions(+), 21 deletions(-) (limited to 'compiler/InterpreterLoopsMatchCtxs.ml') diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 9c017f19..6d814c5c 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -96,7 +96,8 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) | 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" + | AEndedMutLoan _ | AEndedSharedLoan _ -> + craise __FILE__ __LINE__ meta "Unreachable" (** Make sure we don't register the ignored ids *) method! visit_aborrow_content abs_id bc = @@ -109,7 +110,8 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) -> (* Ignore the id of the borrow, if there is *) self#visit_typed_avalue abs_id child - | AEndedMutBorrow _ | AEndedSharedBorrow -> craise __FILE__ __LINE__ meta "Unreachable" + | AEndedMutBorrow _ | AEndedSharedBorrow -> + craise __FILE__ __LINE__ meta "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 @@ -151,8 +153,12 @@ let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty) match (ty0, ty1) with | TAdt (id0, generics0), TAdt (id1, generics1) -> sanity_check __FILE__ __LINE__ (id0 = id1) meta; - sanity_check __FILE__ __LINE__ (generics0.const_generics = generics1.const_generics) meta; - sanity_check __FILE__ __LINE__ (generics0.trait_refs = generics1.trait_refs) meta; + sanity_check __FILE__ __LINE__ + (generics0.const_generics = generics1.const_generics) + meta; + sanity_check __FILE__ __LINE__ + (generics0.trait_refs = generics1.trait_refs) + meta; let id = id0 in let const_generics = generics1.const_generics in let trait_refs = generics1.trait_refs in @@ -213,8 +219,12 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct { value; ty = v1.ty } else ( (* For now, we don't merge ADTs which contain borrows *) - sanity_check __FILE__ __LINE__ (not (value_has_borrows v0.value)) M.meta; - sanity_check __FILE__ __LINE__ (not (value_has_borrows v1.value)) M.meta; + sanity_check __FILE__ __LINE__ + (not (value_has_borrows v0.value)) + M.meta; + sanity_check __FILE__ __LINE__ + (not (value_has_borrows v1.value)) + M.meta; (* Merge *) M.match_distinct_adts ctx0 ctx1 ty av0 av1) | VBottom, VBottom -> v0 @@ -387,7 +397,9 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct log#ldebug (lazy "match_typed_avalues: shared loans"); let sv = match_rec sv0 sv1 in let av = match_arec av0 av1 in - sanity_check __FILE__ __LINE__ (not (value_has_borrows sv.value)) M.meta; + sanity_check __FILE__ __LINE__ + (not (value_has_borrows sv.value)) + M.meta; 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) -> @@ -795,11 +807,21 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* 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" - let match_ashared_borrows _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_distinct_aadts _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_ashared_borrows _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_amut_loans _ _ _ _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + let match_avalues _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" end @@ -917,11 +939,21 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (* 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" - let match_ashared_borrows _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_amut_borrows _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_distinct_aadts _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_ashared_borrows _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_amut_borrows _ _ _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_amut_loans _ _ _ _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + let match_avalues _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" end @@ -1129,7 +1161,9 @@ struct sanity_check __FILE__ __LINE__ left meta; let id = sv.sv_id in (* Check: fixed values are fixed *) - sanity_check __FILE__ __LINE__ (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) meta; + sanity_check __FILE__ __LINE__ + (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) + meta; (* Update the binding for the target symbolic value *) S.sid_to_value_map := SymbolicValueId.Map.add_strict id v !S.sid_to_value_map; @@ -1355,7 +1389,8 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) sanity_check __FILE__ __LINE__ (v0 = v1) meta; (* 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)) + sanity_check __FILE__ __LINE__ + ((not S.check_equiv) || ids_are_fixed ids)) meta; (* We still match the values - allows to compute mappings (which are the identity actually) *) @@ -1376,7 +1411,9 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) sanity_check __FILE__ __LINE__ (abs0 = abs1) meta; (* 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; + sanity_check __FILE__ __LINE__ + ((not S.check_equiv) || ids_are_fixed ids) + meta; (* Continue *) match_envs env0' env1') else ( @@ -1765,7 +1802,8 @@ let match_ctx_with_target (config : config) (meta : Meta.meta) 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; + sanity_check __FILE__ __LINE__ Config.greedy_expand_symbolics_with_borrows + meta; (* Update the borrows and loans in the abstractions of the target context. -- cgit v1.2.3 From 5809c45fbbfcbb78b15a97be619dcde4ab4868b8 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 29 Mar 2024 16:21:15 +0100 Subject: Add some error messages --- compiler/InterpreterLoopsMatchCtxs.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'compiler/InterpreterLoopsMatchCtxs.ml') diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 6d814c5c..bd271ff4 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -243,7 +243,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct (not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) - M.meta "TODO: error message"; + M.meta "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 @@ -268,7 +268,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let sv = match_rec sv0 sv1 in cassert __FILE__ __LINE__ (not (value_has_borrows sv.value)) - M.meta "TODO: error message"; + M.meta "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 -> -- cgit v1.2.3 From 1a86cac476c1f5c0d64d5a12db267d3ac651561b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 29 Mar 2024 17:49:46 +0100 Subject: Cleanup and fix a mistake --- compiler/InterpreterLoopsMatchCtxs.ml | 41 ++++++++++++++++++++--------------- 1 file changed, 24 insertions(+), 17 deletions(-) (limited to 'compiler/InterpreterLoopsMatchCtxs.ml') diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index bd271ff4..e710ed2b 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -827,13 +827,13 @@ end (* Very annoying: functors only take modules as inputs... *) module type MatchMoveState = sig + val meta : Meta.meta + (** The current loop *) val loop_id : LoopId.id (** The moved values *) val nvalues : typed_value list ref - - val meta : Meta.meta end (* We use this matcher to move values in environment. @@ -853,9 +853,9 @@ end indeed matches the resulting target environment: it will be re-checked later. *) module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct - (** Small utility *) let meta = S.meta + (** Small utility *) let push_moved_value (v : typed_value) : unit = S.nvalues := v :: !S.nvalues let match_etys _ _ ty0 ty1 = @@ -959,6 +959,8 @@ end module MakeCheckEquivMatcher (S : MatchCheckEquivState) : CheckEquivMatcher = struct + let meta = S.meta + module MkGetSetM (Id : Identifiers.Id) = struct module Inj = Id.InjSubst @@ -1001,8 +1003,6 @@ struct (match_el msg m (Id.Set.elements ks0) (Id.Set.elements ks1)) end - let meta = S.meta - module GetSetRid = MkGetSetM (RegionId) let match_rid = GetSetRid.match_e "match_rid: " S.rid_map @@ -1383,15 +1383,15 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) | EBinding (BDummy b0, v0) :: env0', EBinding (BDummy b1, v1) :: env1' -> (* Sanity check: if the dummy value is an old value, the bindings must 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; - (* 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; + 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; + (* 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); (* We still match the values - allows to compute mappings (which are the identity actually) *) let _ = M.match_typed_values ctx0 ctx1 v0 v1 in @@ -1457,9 +1457,16 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) } in Some maps - with Distinct msg -> - log#ldebug (lazy ("match_ctxs: distinct: " ^ msg)); - None + with + | Distinct msg -> + log#ldebug (lazy ("match_ctxs: distinct: " ^ msg ^ "\n")); + None + | ValueMatchFailure k -> + log#ldebug + (lazy + ("match_ctxs: distinct: ValueMatchFailure" ^ show_updt_env_kind k + ^ "\n")); + None let ctxs_are_equivalent (meta : Meta.meta) (fixed_ids : ids_sets) (ctx0 : eval_ctx) (ctx1 : eval_ctx) : bool = -- cgit v1.2.3