diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Driver.ml | 34 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 165 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.mli | 4 | ||||
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 12 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 32 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 4 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 10 | ||||
| -rw-r--r-- | compiler/Print.ml | 2 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 4 | ||||
| -rw-r--r-- | compiler/Values.ml | 13 |
10 files changed, 144 insertions, 136 deletions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 42fd0122..f870659a 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -143,22 +143,24 @@ let () = * command-line arguments *) (* By setting a level for the main_logger_handler, we filter everything *) Easy_logging.Handlers.set_level main_logger_handler EL.Debug; - main_log#set_level EL.Info; - llbc_of_json_logger#set_level EL.Info; - pre_passes_log#set_level EL.Info; - interpreter_log#set_level EL.Info; - statements_log#set_level EL.Info; - paths_log#set_level EL.Info; - expressions_log#set_level EL.Info; - expansion_log#set_level EL.Info; - projectors_log#set_level EL.Info; - borrows_log#set_level EL.Info; - invariants_log#set_level EL.Info; - pure_utils_log#set_level EL.Info; - symbolic_to_pure_log#set_level EL.Info; - pure_micro_passes_log#set_level EL.Info; - pure_to_extract_log#set_level EL.Info; - translate_log#set_level EL.Info; + let level = EL.Info in + main_log#set_level level; + llbc_of_json_logger#set_level level; + pre_passes_log#set_level level; + interpreter_log#set_level level; + statements_log#set_level level; + loops_log#set_level level; + paths_log#set_level level; + expressions_log#set_level level; + expansion_log#set_level level; + projectors_log#set_level level; + borrows_log#set_level level; + invariants_log#set_level level; + pure_utils_log#set_level level; + symbolic_to_pure_log#set_level level; + pure_micro_passes_log#set_level level; + pure_to_extract_log#set_level level; + translate_log#set_level level; let log = main_log in (* Load the module *) diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index c71abe25..ab3fb7ea 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -34,13 +34,18 @@ let log = L.borrows_log *) let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) (allow_inner_loans : bool) (l : V.BorrowId.id) (ctx : C.eval_ctx) : - (C.eval_ctx * g_borrow_content option, priority_borrows_or_abs) result = + ( C.eval_ctx * (V.AbstractionId.id option * g_borrow_content) option, + priority_borrows_or_abs ) + result = (* We use a reference to communicate the kind of borrow we found, if we * find one *) - let replaced_bc : g_borrow_content option ref = ref None in - let set_replaced_bc (bc : g_borrow_content) = + let replaced_bc : (V.AbstractionId.id option * g_borrow_content) option ref = + ref None + in + let set_replaced_bc (abs_id : V.AbstractionId.id option) + (bc : g_borrow_content) = assert (Option.is_none !replaced_bc); - replaced_bc := Some bc + replaced_bc := Some (abs_id, bc) in (* Raise an exception if: * - there are outer borrows @@ -104,7 +109,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) (* Check if there are outer borrows or if we are inside an abstraction *) raise_if_priority outer None; (* Register the update *) - set_replaced_bc (Concrete bc); + set_replaced_bc (fst outer) (Concrete bc); (* Update the value *) V.Bottom) else super#visit_Borrow outer bc @@ -114,7 +119,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) (* Check if there are outer borrows or if we are inside an abstraction *) raise_if_priority outer (Some bv); (* Register the update *) - set_replaced_bc (Concrete bc); + set_replaced_bc (fst outer) (Concrete bc); (* Update the value *) V.Bottom) else @@ -155,7 +160,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) method! visit_ABorrow outer bc = match bc with - | V.AMutBorrow (_, bid, _) -> + | V.AMutBorrow (bid, _) -> (* Check if this is the borrow we are looking for *) if bid = l then ( (* When ending a mut borrow, there are two cases: @@ -170,7 +175,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) * abstraction *) raise_if_priority outer None; (* Register the update *) - set_replaced_bc (Abstract bc); + set_replaced_bc (fst outer) (Abstract bc); (* Update the value - note that we are necessarily in the second * of the two cases described above. * Also note that, as we are moving the borrowed value inside the @@ -188,7 +193,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) * abstraction *) raise_if_priority outer None; (* Register the update *) - set_replaced_bc (Abstract bc); + set_replaced_bc (fst outer) (Abstract bc); (* Update the value - note that we are necessarily in the second * of the two cases described above *) V.ABottom) @@ -207,7 +212,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) * abstraction *) raise_if_priority outer None; (* Register the update *) - set_replaced_bc (Abstract bc); + set_replaced_bc (fst outer) (Abstract bc); (* Update the value - note that we are necessarily in the second * of the two cases described above *) let asb = remove_borrow_from_asb l asb in @@ -498,7 +503,7 @@ let give_back_symbolic_value (_config : C.config) to convert the {!V.avalue} to a {!type:V.value} by introducing the proper symbolic values. *) let give_back_avalue_to_same_abstraction (_config : C.config) - (bid : V.BorrowId.id) (mv : V.mvalue) (nv : V.typed_avalue) + (bid : V.BorrowId.id) (nv : V.typed_avalue) (nsv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx = (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in @@ -513,7 +518,11 @@ let give_back_avalue_to_same_abstraction (_config : C.config) (** This is a bit annoying, but as we need the type of the avalue we are exploring, in order to be able to project the value we give back, we need to reimplement {!visit_typed_avalue} instead of - {!visit_ALoan} *) + {!visit_ALoan}. + + TODO: it is possible to do this by remembering the type of the last + typed avalue we entered. + *) method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue = match av.V.value with @@ -523,7 +532,11 @@ let give_back_avalue_to_same_abstraction (_config : C.config) | _ -> super#visit_typed_avalue opt_abs av (** We are not specializing an already existing method, but adding a - new method (for projections, we need type information) *) + new method (for projections, we need type information). + + TODO: it is possible to do this by remembering the type of the last + typed avalue we entered. + *) method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty) (lc : V.aloan_content) : V.avalue = match lc with @@ -548,7 +561,7 @@ let give_back_avalue_to_same_abstraction (_config : C.config) (* Return the new value *) V.ALoan (V.AEndedMutLoan - { given_back = nv; child; given_back_meta = mv })) + { given_back = nv; child; given_back_meta = nsv })) else (* Continue exploring *) super#visit_ALoan opt_abs lc | V.ASharedLoan (_, _, _) @@ -569,7 +582,7 @@ let give_back_avalue_to_same_abstraction (_config : C.config) assert (nv.V.ty = ty); V.ALoan (V.AEndedIgnoredMutLoan - { given_back = nv; child; given_back_meta = mv })) + { given_back = nv; child; given_back_meta = nsv })) else super#visit_ALoan opt_abs lc | V.AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } @@ -713,9 +726,52 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id) assert !r; { ctx with env } -(** Auxiliary function: see {!end_borrow_aux} *) -let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) - (ctx : C.eval_ctx) : C.eval_ctx = +(** Convert an {!type:V.avalue} to a {!type:V.value}. + + This function is used when ending abstractions: whenever we end a borrow + in an abstraction, we converted the borrowed {!V.avalue} to a fresh symbolic + {!type:V.value}, then give back this {!type:V.value} to the context. + + Note that some regions may have ended in the symbolic value we generate. + For instance, consider the following function signature: + {[ + fn f<'a>(x : &'a mut &'a mut u32); + ]} + When ending the abstraction, the value given back for the outer borrow + should be ⊥. In practice, we will give back a symbolic value which can't + be expanded (because expanding this symbolic value would require expanding + a reference whose region has already ended). + *) +let convert_avalue_to_given_back_value (abs_kind : V.abs_kind) + (av : V.typed_avalue) : V.symbolic_value = + let sv_kind = + match abs_kind with + | V.FunCall _ -> V.FunCallGivenBack + | V.SynthRet _ -> V.SynthRetGivenBack + | V.SynthInput _ -> V.SynthInputGivenBack + | V.Loop _ -> V.LoopGivenBack + in + mk_fresh_symbolic_value sv_kind av.V.ty + +(** Auxiliary function: see {!end_borrow_aux}. + + When we end a mutable borrow, we need to "give back" the value it contained + to its original owner by reinserting it at the proper position. + + Rem.: this function is used when we end *one single* borrow (we don't + end this borrow as member of the group of borrows belonging to an + abstraction). + If the borrow is an "abstract" borrow, it means we are ending a borrow + inside an abstraction (we end a borrow whose corresponding loan is in + the same abstraction - we are allowed to do so without ending the whole + abstraction). + TODO: we should not treat this case here, and should only consider internal + borrows. This kind of internal reshuffling. should be similar to ending + abstractions (it is tantamount to ending *sub*-abstractions). + *) +let give_back (config : C.config) (abs_id_opt : V.AbstractionId.id option) + (l : V.BorrowId.id) (bc : g_borrow_content) (ctx : C.eval_ctx) : C.eval_ctx + = (* Debug *) log#ldebug (lazy @@ -746,13 +802,23 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); (* Update the context *) give_back_shared config l ctx - | Abstract (V.AMutBorrow (mv, l', av)) -> + | Abstract (V.AMutBorrow (l', av)) -> (* Sanity check *) assert (l' = l); (* Check that the corresponding loan is somewhere - purely a sanity check *) assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + (* Convert the avalue to a (fresh symbolic) value. + + Rem.: we shouldn't do this here. We should do this in a function + which takes care of ending *sub*-abstractions. + *) + let abs_id = Option.get abs_id_opt in + let abs = C.ctx_lookup_abs ctx abs_id in + let sv = convert_avalue_to_given_back_value abs.kind av in (* Update the context *) - give_back_avalue_to_same_abstraction config l mv av ctx + give_back_avalue_to_same_abstraction config l av + (mk_typed_value_from_symbolic_value sv) + ctx | Abstract (V.ASharedBorrow l') -> (* Sanity check *) assert (l' = l); @@ -770,33 +836,6 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) | V.AEndedSharedBorrow ) -> raise (Failure "Unreachable") -(** Convert an {!type:V.avalue} to a {!type:V.value}. - - This function is used when ending abstractions: whenever we end a borrow - in an abstraction, we converted the borrowed {!V.avalue} to a fresh symbolic - {!type:V.value}, then give back this {!type:V.value} to the context. - - Note that some regions may have ended in the symbolic value we generate. - For instance, consider the following function signature: - {[ - fn f<'a>(x : &'a mut &'a mut u32); - ]} - When ending the abstraction, the value given back for the outer borrow - should be ⊥. In practice, we will give back a symbolic value which can't - be expanded (because expanding this symbolic value would require expanding - a reference whose region has already ended). - *) -let convert_avalue_to_given_back_value (abs_kind : V.abs_kind) - (av : V.typed_avalue) : V.symbolic_value = - let sv_kind = - match abs_kind with - | V.FunCall _ -> V.FunCallGivenBack - | V.SynthRet _ -> V.SynthRetGivenBack - | V.SynthInput _ -> V.SynthInputGivenBack - | V.Loop _ -> V.LoopGivenBack - in - mk_fresh_symbolic_value sv_kind av.V.ty - let check_borrow_disappeared (fun_name : string) (l : V.BorrowId.id) (ctx0 : C.eval_ctx) : cm_fun = let check_disappeared (ctx : C.eval_ctx) : unit = @@ -921,14 +960,14 @@ let rec end_borrow_aux (config : C.config) (chain : borrow_or_abs_ids) cf_check cf ctx (* We found a borrow and replaced it with [Bottom]: give it back (i.e., update the corresponding loan) *) - | Ok (ctx, Some bc) -> + | Ok (ctx, Some (abs_id_opt, bc)) -> (* Sanity check: the borrowed value shouldn't contain loans *) (match bc with | Concrete (V.MutBorrow (_, bv)) -> assert (Option.is_none (get_first_loan_in_value bv)) | _ -> ()); (* Give back the value *) - let ctx = give_back config l bc ctx in + let ctx = give_back config abs_id_opt l bc ctx in (* Do a sanity check and continue *) cf_check cf ctx @@ -1087,7 +1126,11 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) (* We explore in-depth and use exceptions. When exploring a borrow, if * the exploration didn't trigger an exception, it means there are no * inner borrows to end: we can thus trigger an exception for the current - * borrow. *) + * borrow. + * + * TODO: there should be a function in InterpreterBorrowsCore which does just + * that. + *) let obj = object inherit [_] V.iter_abs as super @@ -1098,7 +1141,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) (* No exception was raise: we can raise an exception for the * current borrow *) match bc with - | V.AMutBorrow (_, _, _) | V.ASharedBorrow _ -> + | V.AMutBorrow _ | V.ASharedBorrow _ -> (* Raise an exception *) raise (FoundABorrowContent bc) | V.AProjSharedBorrow asb -> @@ -1146,7 +1189,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) ^ aborrow_content_to_string ctx bc)); let ctx = match bc with - | V.AMutBorrow (_mv, bid, av) -> + | V.AMutBorrow (bid, av) -> (* First, convert the avalue to a (fresh symbolic) value *) let sv = convert_avalue_to_given_back_value abs.kind av in (* Replace the mut borrow to register the fact that we ended @@ -1649,9 +1692,9 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) assert allow_borrows; (* Explore the borrow content *) match bc with - | V.AMutBorrow (mv, bid, child_av) -> + | V.AMutBorrow (bid, child_av) -> let ignored = mk_aignored child_av.V.ty in - let value = V.ABorrow (V.AMutBorrow (mv, bid, ignored)) in + let value = V.ABorrow (V.AMutBorrow (bid, ignored)) in push { V.value; ty }; (* Explore the child *) list_avalues false push_fail child_av @@ -1833,11 +1876,10 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool) (* We don't support nested borrows for now *) assert (not (value_has_borrows ctx bv.V.value)); (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *) - let mv = bv in let ref_ty = ety_no_regions_to_rty ref_ty in let ty = T.Ref (T.Var r_id, ref_ty, kind) in let ignored = mk_aignored ref_ty in - let av = V.ABorrow (V.AMutBorrow (mv, bid, ignored)) in + let av = V.ABorrow (V.AMutBorrow (bid, ignored)) in let av = { V.value = av; ty } in (* Continue exploring, looking for loans (and forbidding borrows, because we don't support nested borrows for now) *) @@ -2015,7 +2057,7 @@ let compute_merge_abstractions_info (abs : V.abs) : merge_abstraction_info = in (* Explore the borrow content *) (match bc with - | V.AMutBorrow (_, bid, _) -> push_borrow bid (Abstract (ty, bc)) + | V.AMutBorrow (bid, _) -> push_borrow bid (Abstract (ty, bc)) | V.ASharedBorrow bid -> push_borrow bid (Abstract (ty, bc)) | V.AProjSharedBorrow asb -> let register asb = @@ -2053,19 +2095,15 @@ type merge_duplicates_funcs = { merge_amut_borrows : V.borrow_id -> T.rty -> - V.mvalue -> V.typed_avalue -> T.rty -> - V.mvalue -> V.typed_avalue -> V.typed_avalue; (** Parameters: - [id] - [ty0] - - [mv0] - [child0] - [ty1] - - [mv1] - [child1] The children should be [AIgnored]. @@ -2208,9 +2246,8 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool) let merge_aborrow_contents (ty0 : T.rty) (bc0 : V.aborrow_content) (ty1 : T.rty) (bc1 : V.aborrow_content) : V.typed_avalue = match (bc0, bc1) with - | V.AMutBorrow (mv0, id, child0), V.AMutBorrow (mv1, _, child1) -> - (Option.get merge_funs).merge_amut_borrows id ty0 mv0 child0 ty1 mv1 - child1 + | V.AMutBorrow (id, child0), V.AMutBorrow (_, child1) -> + (Option.get merge_funs).merge_amut_borrows id ty0 child0 ty1 child1 | ASharedBorrow id, ASharedBorrow _ -> (Option.get merge_funs).merge_ashared_borrows id ty0 ty1 | AProjSharedBorrow _, AProjSharedBorrow _ -> diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli index 51c6c592..6a8fb87c 100644 --- a/compiler/InterpreterBorrows.mli +++ b/compiler/InterpreterBorrows.mli @@ -142,19 +142,15 @@ type merge_duplicates_funcs = { merge_amut_borrows : V.borrow_id -> T.rty -> - V.mvalue -> V.typed_avalue -> T.rty -> - V.mvalue -> V.typed_avalue -> V.typed_avalue; (** Parameters: - [id] - [ty0] - - [mv0] - [child0] - [ty1] - - [mv1] - [child1] The children should be [AIgnored]. diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 6eece4fe..f4116b75 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -186,7 +186,9 @@ let projection_contains (ty1 : T.rty) (rset1 : T.RegionId.Set.t) (ty2 : T.rty) The loan is referred to by a borrow id. - TODO: group abs_or_var_id and g_loan_content. + Rem.: if the {!g_loan_content} is {!Concrete}, the {!abs_or_var_id} is not + necessarily {!VarId} or {!DummyVarId}: there can be concrete loans in + abstractions (in the shared values). *) let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (ctx : C.eval_ctx) : (abs_or_var_id * g_loan_content) option = @@ -434,9 +436,9 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) method! visit_aborrow_content env bc = match bc with - | V.AMutBorrow (mv, bid, av) -> + | V.AMutBorrow (bid, av) -> if bid = l then raise (FoundGBorrowContent (Abstract bc)) - else super#visit_AMutBorrow env mv bid av + else super#visit_AMutBorrow env bid av | V.ASharedBorrow bid -> if bid = l then raise (FoundGBorrowContent (Abstract bc)) else super#visit_ASharedBorrow env bid @@ -551,9 +553,9 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue) method! visit_ABorrow env bc = match bc with - | V.AMutBorrow (mv, bid, av) -> + | V.AMutBorrow (bid, av) -> if bid = l then update () - else V.ABorrow (super#visit_AMutBorrow env mv bid av) + else V.ABorrow (super#visit_AMutBorrow env bid av) | V.ASharedBorrow bid -> if bid = l then update () else V.ABorrow (super#visit_ASharedBorrow env bid) diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index f0a7fdbd..1228ae99 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -476,28 +476,22 @@ module type Matcher = sig (** Parameters: [ty0] - [mv0] [bid0] [av0] [ty1] - [mv1] [bid1] [av1] [ty]: result of matching ty0 and ty1 - [mv]: result of matching mv0 and mv1 [av]: result of matching av0 and av1 *) val match_amut_borrows : T.rty -> - V.mvalue -> V.borrow_id -> V.typed_avalue -> T.rty -> - V.mvalue -> V.borrow_id -> V.typed_avalue -> T.rty -> - V.mvalue -> V.typed_avalue -> V.typed_avalue @@ -692,16 +686,9 @@ module Match (M : Matcher) = struct match (bc0, bc1) with | ASharedBorrow bid0, ASharedBorrow bid1 -> M.match_ashared_borrows v0.V.ty bid0 v1.V.ty bid1 ty - | AMutBorrow (mv0, bid0, av0), AMutBorrow (mv1, bid1, av1) -> - (* The meta-value should be the value consumed by the abstracion. - This only makes sense if the abstraction was introduced because - of a function call (we use it for the translation). - TODO: make it optional? - *) - let mv = mk_bottom mv0.V.ty in + | AMutBorrow (bid0, av0), AMutBorrow (bid1, av1) -> let av = match_arec av0 av1 in - M.match_amut_borrows v0.V.ty mv0 bid0 av0 v1.V.ty mv1 bid1 av1 ty mv - av + M.match_amut_borrows v0.V.ty bid0 av0 v1.V.ty bid1 av1 ty av | AIgnoredMutBorrow _, AIgnoredMutBorrow _ -> (* The abstractions are destructured: we shouldn't get there *) raise (Failure "Unexpected") @@ -894,7 +881,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct (* Generate the avalues for the abstraction *) let mk_aborrow (bid : V.borrow_id) (bv : V.typed_value) : V.typed_avalue = let bv_ty = ety_no_regions_to_rty bv.V.ty in - let value = V.ABorrow (V.AMutBorrow (bv, bid, mk_aignored bv_ty)) in + let value = V.ABorrow (V.AMutBorrow (bid, mk_aignored bv_ty)) in { V.value; ty = borrow_ty } in let borrows = [ mk_aborrow bid0 bv0; mk_aborrow bid1 bv1 ] in @@ -1026,7 +1013,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct let match_distinct_aadts _ _ _ _ _ = raise (Failure "Unreachable") let match_ashared_borrows _ _ _ _ = raise (Failure "Unreachable") - let match_amut_borrows _ _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") + let match_amut_borrows _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") let match_amut_loans _ _ _ _ _ _ _ _ = raise (Failure "Unreachable") let match_avalues _ _ = raise (Failure "Unreachable") @@ -1053,18 +1040,15 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets) let module M = Match (JM) in (* TODO: why not simply call: M.match_type_avalues? (or move this code to MakeJoinMatcher?) *) - let merge_amut_borrows id ty0 (mv0 : V.typed_value) child0 _ty1 - (mv1 : V.typed_value) child1 = + let merge_amut_borrows id ty0 child0 _ty1 child1 = (* Sanity checks *) assert (is_aignored child0.V.value); assert (is_aignored child1.V.value); - assert (mv0.V.ty = mv1.V.ty); (* Same remarks as for [merge_amut_loans] *) let ty = ty0 in let child = child0 in - let mv = mk_bottom mv0.ty in - let value = V.ABorrow (V.AMutBorrow (mv, id, child)) in + let value = V.ABorrow (V.AMutBorrow (id, child)) in { V.value; ty } in @@ -1486,9 +1470,9 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct let value = V.ABorrow (V.ASharedBorrow bid) in { V.value; ty } - let match_amut_borrows _ty0 _mv0 bid0 _av0 _ty1 _mv1 bid1 _av1 ty mv av = + let match_amut_borrows _ty0 bid0 _av0 _ty1 bid1 _av1 ty av = let bid = match_bid bid0 bid1 in - let value = V.ABorrow (V.AMutBorrow (mv, bid, av)) in + let value = V.ABorrow (V.AMutBorrow (bid, av)) in { V.value; ty } let match_ashared_loans _ty0 ids0 _v0 _av0 _ty1 ids1 _v1 _av1 ty v av = diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index a69052cb..9487df84 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -130,14 +130,12 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) let bc = match (bc, kind) with | V.MutBorrow (bid, bv), T.Mut -> - (* Remember the borrowed value we are about to project as a meta-value *) - let mv = bv in (* Apply the projection on the borrowed value *) let bv = apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions bv ref_ty in - V.AMutBorrow (mv, bid, bv) + V.AMutBorrow (bid, bv) | V.SharedBorrow bid, T.Shared -> (* Rem.: we don't need to also apply the projection on the borrowed value, because for as long as the abstraction diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 3fdb963a..5b81cc02 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -253,7 +253,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = method! visit_aborrow_content env bc = let _ = match bc with - | V.AMutBorrow (_, bid, _) -> register_borrow Mut bid + | V.AMutBorrow (bid, _) -> register_borrow Mut bid | V.ASharedBorrow bid -> register_borrow Shared bid | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid | V.AIgnoredMutBorrow (None, _) @@ -361,7 +361,7 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = (* Update the info *) let info = match bc with - | V.AMutBorrow (_, _, _) -> set_outer_mut info + | V.AMutBorrow (_, _) -> set_outer_mut info | V.ASharedBorrow _ | V.AEndedSharedBorrow -> set_outer_shared info | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow _ -> @@ -480,7 +480,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = let glc = lookup_borrow ek_all bid ctx in match glc with | Concrete (V.MutBorrow (_, bv)) -> assert (bv.V.ty = ty) - | Abstract (V.AMutBorrow (_, _, sv)) -> + | Abstract (V.AMutBorrow (_, sv)) -> assert (Subst.erase_regions sv.V.ty = ty) | _ -> raise (Failure "Inconsistent context"))) | V.Symbolic sv, ty -> @@ -547,7 +547,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | V.ABottom, _ -> (* Nothing to check *) () | V.ABorrow bc, T.Ref (_, ref_ty, rkind) -> ( match (bc, rkind) with - | V.AMutBorrow (_, _, av), T.Mut -> + | V.AMutBorrow (_, av), T.Mut -> (* Check that the child value has the proper type *) assert (av.V.ty = ref_ty) | V.ASharedBorrow bid, T.Shared -> ( @@ -578,7 +578,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = match glc with | Concrete (V.MutBorrow (_, bv)) -> assert (bv.V.ty = Subst.erase_regions borrowed_aty) - | Abstract (V.AMutBorrow (_, _, sv)) -> + | Abstract (V.AMutBorrow (_, sv)) -> assert ( Subst.erase_regions sv.V.ty = Subst.erase_regions borrowed_aty) diff --git a/compiler/Print.ml b/compiler/Print.ml index 88d33bce..393f80c2 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -264,7 +264,7 @@ module Values = struct and aborrow_content_to_string (fmt : value_formatter) (bc : V.aborrow_content) : string = match bc with - | AMutBorrow (_, bid, av) -> + | AMutBorrow (bid, av) -> "&mut@" ^ V.BorrowId.to_string bid ^ " (" ^ typed_avalue_to_string fmt av ^ ")" diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 81cc22e1..6c956fe8 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -949,7 +949,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) : texpression option = match bc with - | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> + | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> raise (Failure "Unreachable") | AEndedMutBorrow (_, _) -> (* We collect consumed values: ignore *) @@ -1089,7 +1089,7 @@ and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content) and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content) (ctx : bs_ctx) : bs_ctx * typed_pattern option = match bc with - | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> + | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> raise (Failure "Unreachable") | AEndedMutBorrow (msv, _) -> (* Return the meta-symbolic-value *) diff --git a/compiler/Values.ml b/compiler/Values.ml index 54575edd..a57c589b 100644 --- a/compiler/Values.ml +++ b/compiler/Values.ml @@ -638,7 +638,7 @@ and aloan_content = ids)? *) and aborrow_content = - | AMutBorrow of mvalue * borrow_id * typed_avalue + | AMutBorrow of borrow_id * typed_avalue (** A mutable borrow owned by an abstraction. Is used when an abstraction "consumes" borrows, when giving borrows @@ -658,17 +658,6 @@ and aborrow_content = > px -> ⊥ > abs0 { a_mut_borrow l0 (U32 0) } ]} - - The meta-value stores the initial value on which the projector was - applied, which reduced to this mut borrow. This meta-information - is only used for the synthesis. - Rem.: we don't use the meta-value for now, but might need it when - using nested borrows: if we end an *internal* borrow, this meta - value is propagated to the corresponding loan (we need to know - what the loan consumed, for the synthesis). We could also generate - a fresh symbolic value upon ending the internal borrow (as is - done in the regular case), which would allow us to remove the - meta-value altogether. *) | ASharedBorrow of borrow_id (** A shared borrow owned by an abstraction. |