From 746239e8f29de85f848d14e44eac8690e2065a1d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 20:41:58 +0100 Subject: Add the "V" prefix to most variants related to values --- compiler/InterpreterBorrows.ml | 338 ++++++++++++++++----------------- compiler/InterpreterBorrowsCore.ml | 105 +++++----- compiler/InterpreterExpansion.ml | 29 ++- compiler/InterpreterExpressions.ml | 106 +++++------ compiler/InterpreterLoopsFixedPoint.ml | 18 +- compiler/InterpreterLoopsMatchCtxs.ml | 76 ++++---- compiler/InterpreterPaths.ml | 84 ++++---- compiler/InterpreterProjectors.ml | 112 +++++------ compiler/InterpreterStatements.ml | 38 ++-- compiler/InterpreterUtils.ml | 8 +- compiler/Invariants.ml | 277 +++++++++++++-------------- compiler/Print.ml | 25 +-- compiler/SymbolicToPure.ml | 20 +- compiler/Values.ml | 18 +- compiler/ValuesUtils.ml | 20 +- 15 files changed, 629 insertions(+), 645 deletions(-) diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index c54d55d4..566061c2 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -79,10 +79,10 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) | None -> () | Some c -> ( match c with - | V.SharedLoan (bids, _) -> + | VSharedLoan (bids, _) -> raise (FoundPriority (InnerLoans (Borrows bids))) - | V.MutLoan bid -> raise (FoundPriority (InnerLoans (Borrow bid))) - )) + | VMutLoan bid -> raise (FoundPriority (InnerLoans (Borrow bid)))) + ) in (* The environment is used to keep track of the outer loans *) @@ -92,18 +92,18 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) (** We reimplement {!visit_Loan} because we may have to update the outer borrows *) - method! visit_Loan (outer : V.AbstractionId.id option * borrow_ids option) - lc = + method! visit_VLoan + (outer : V.AbstractionId.id option * borrow_ids option) lc = match lc with - | V.MutLoan bid -> V.Loan (super#visit_MutLoan outer bid) - | V.SharedLoan (bids, v) -> + | VMutLoan bid -> VLoan (super#visit_VMutLoan outer bid) + | VSharedLoan (bids, v) -> (* Update the outer borrows before diving into the shared value *) let outer = update_outer_borrows outer (Borrows bids) in - V.Loan (super#visit_SharedLoan outer bids v) + VLoan (super#visit_VSharedLoan outer bids v) - method! visit_Borrow outer bc = + method! visit_VBorrow outer bc = match bc with - | SharedBorrow l' | ReservedMutBorrow l' -> + | VSharedBorrow l' | VReservedMutBorrow l' -> (* Check if this is the borrow we are looking for *) if l = l' then ( (* Check if there are outer borrows or if we are inside an abstraction *) @@ -111,9 +111,9 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) (* Register the update *) set_replaced_bc (fst outer) (Concrete bc); (* Update the value *) - V.Bottom) - else super#visit_Borrow outer bc - | V.MutBorrow (l', bv) -> + VBottom) + else super#visit_VBorrow outer bc + | VMutBorrow (l', bv) -> (* Check if this is the borrow we are looking for *) if l = l' then ( (* Check if there are outer borrows or if we are inside an abstraction *) @@ -121,11 +121,11 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) (* Register the update *) set_replaced_bc (fst outer) (Concrete bc); (* Update the value *) - V.Bottom) + VBottom) else (* Update the outer borrows before diving into the borrowed value *) let outer = update_outer_borrows outer (Borrow l') in - V.Borrow (super#visit_MutBorrow outer l' bv) + VBorrow (super#visit_VMutBorrow outer l' bv) (** We reimplement {!visit_ALoan} because we may have to update the outer borrows *) @@ -136,31 +136,31 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) * need it to properly instantiate the backward functions when generating * the pure translation. *) match lc with - | V.AMutLoan (_, _) -> + | AMutLoan (_, _) -> (* Nothing special to do *) super#visit_ALoan outer lc - | V.ASharedLoan (bids, v, av) -> + | ASharedLoan (bids, v, av) -> (* Explore the shared value - we need to update the outer borrows *) let souter = update_outer_borrows outer (Borrows bids) in let v = super#visit_typed_value souter v in (* Explore the child avalue - we keep the same outer borrows *) let av = super#visit_typed_avalue outer av in (* Reconstruct *) - V.ALoan (V.ASharedLoan (bids, v, av)) - | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AEndedSharedLoan _ + ALoan (ASharedLoan (bids, v, av)) + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedSharedLoan _ (* The loan has ended, so no need to update the outer borrows *) - | V.AIgnoredMutLoan _ (* Nothing special to do *) - | V.AEndedIgnoredMutLoan + | AIgnoredMutLoan _ (* Nothing special to do *) + | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } (* Nothing special to do *) - | V.AIgnoredSharedLoan _ -> + | AIgnoredSharedLoan _ -> (* Nothing special to do *) super#visit_ALoan outer lc method! visit_ABorrow outer bc = match bc with - | V.AMutBorrow (bid, _) -> + | AMutBorrow (bid, _) -> (* Check if this is the borrow we are looking for *) if bid = l then ( (* TODO: treat this case differently. We should not introduce @@ -184,12 +184,12 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) * abstraction (and not really giving the value back to the context) * we do not insert {!AEndedMutBorrow} but rather {!ABottom} *) raise (Failure "Unimplemented") - (* V.ABottom *)) + (* ABottom *)) else (* Update the outer borrows before diving into the child avalue *) let outer = update_outer_borrows outer (Borrow bid) in super#visit_ABorrow outer bc - | V.ASharedBorrow bid -> + | ASharedBorrow bid -> (* Check if this is the borrow we are looking for *) if bid = l then ( (* Check there are outer borrows, or if we need to end the whole @@ -199,16 +199,16 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) 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) + ABottom) else super#visit_ABorrow outer bc - | V.AIgnoredMutBorrow (_, _) - | V.AEndedMutBorrow _ - | V.AEndedIgnoredMutBorrow + | AIgnoredMutBorrow (_, _) + | AEndedMutBorrow _ + | AEndedIgnoredMutBorrow { given_back = _; child = _; given_back_meta = _ } - | V.AEndedSharedBorrow -> + | AEndedSharedBorrow -> (* Nothing special to do *) super#visit_ABorrow outer bc - | V.AProjSharedBorrow asb -> + | AProjSharedBorrow asb -> (* Check if the borrow we are looking for is in the asb *) if borrow_in_asb l asb then ( (* Check there are outer borrows, or if we need to end the whole @@ -219,7 +219,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) (* 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 - V.ABorrow (V.AProjSharedBorrow asb)) + ABorrow (AProjSharedBorrow asb)) else (* Nothing special to do *) super#visit_ABorrow outer bc @@ -282,32 +282,32 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) overriding {!visit_ALoan} *) method! visit_typed_value opt_abs (v : V.typed_value) : V.typed_value = match v.V.value with - | V.Loan lc -> + | VLoan lc -> let value = self#visit_typed_Loan opt_abs v.V.ty lc in ({ v with V.value } : V.typed_value) | _ -> super#visit_typed_value opt_abs v method visit_typed_Loan opt_abs ty lc = match lc with - | V.SharedLoan (bids, v) -> + | VSharedLoan (bids, v) -> (* We are giving back a value (i.e., the content of a *mutable* * borrow): nothing special to do *) - V.Loan (super#visit_SharedLoan opt_abs bids v) - | V.MutLoan bid' -> + VLoan (super#visit_VSharedLoan opt_abs bids v) + | VMutLoan bid' -> (* Check if this is the loan we are looking for *) if bid' = bid then ( (* Sanity check *) let expected_ty = ty in - if nv.V.ty <> expected_ty then ( + if nv.ty <> expected_ty then ( log#serror ("give_back_value: improper type:\n- expected: " ^ PA.ty_to_string ctx ty ^ "\n- received: " - ^ PA.ty_to_string ctx nv.V.ty); + ^ PA.ty_to_string ctx nv.ty); raise (Failure "Value given back doesn't have the proper type")); (* Replace *) set_replaced (); - nv.V.value) - else V.Loan (super#visit_MutLoan opt_abs bid') + nv.value) + else VLoan (super#visit_VMutLoan opt_abs bid') (** 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 @@ -333,7 +333,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) * it is necessarily because we ended a parent abstraction, * and the given back value is thus a symbolic value *) match nv.V.value with - | V.Symbolic sv -> + | VSymbolic sv -> let abs = Option.get opt_abs in (* Remember the given back value as a meta-value * TODO: it is a bit annoying to have to deconstruct @@ -374,7 +374,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) ty in match lc with - | V.AMutLoan (bid', child) -> + | AMutLoan (bid', child) -> if bid' = bid then ( (* This is the loan we are looking for: apply the projection to * the value we give back and replaced this mutable loan with @@ -391,17 +391,17 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) (* Continue giving back in the child value *) let child = super#visit_typed_avalue opt_abs child in (* Return the new value *) - V.ALoan (V.AEndedMutLoan { child; given_back; given_back_meta })) + ALoan (AEndedMutLoan { child; given_back; given_back_meta })) else (* Continue exploring *) super#visit_ALoan opt_abs lc - | V.ASharedLoan (_, _, _) -> + | ASharedLoan (_, _, _) -> (* We are giving back a value to a *mutable* loan: nothing special to do *) super#visit_ALoan opt_abs lc - | V.AEndedMutLoan { child = _; given_back = _; given_back_meta = _ } - | V.AEndedSharedLoan (_, _) -> + | AEndedMutLoan { child = _; given_back = _; given_back_meta = _ } + | AEndedSharedLoan (_, _) -> (* Nothing special to do *) super#visit_ALoan opt_abs lc - | V.AIgnoredMutLoan (opt_bid, child) -> + | AIgnoredMutLoan (opt_bid, child) -> (* This loan is ignored, but we may have to project on a subvalue * of the value which is given back *) if opt_bid = Some bid then @@ -417,12 +417,12 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) in (* Continue giving back in the child value *) let child = super#visit_typed_avalue opt_abs child in - V.ALoan - (V.AEndedIgnoredMutLoan { given_back; child; given_back_meta }) + ALoan + (AEndedIgnoredMutLoan { given_back; child; given_back_meta }) else super#visit_ALoan opt_abs lc - | V.AEndedIgnoredMutLoan + | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AIgnoredSharedLoan _ -> + | AIgnoredSharedLoan _ -> (* Nothing special to do *) super#visit_ALoan opt_abs lc @@ -624,9 +624,9 @@ let give_back_shared _config (bid : V.BorrowId.id) (ctx : C.eval_ctx) : object inherit [_] C.map_eval_ctx as super - method! visit_Loan opt_abs lc = + method! visit_VLoan opt_abs lc = match lc with - | V.SharedLoan (bids, shared_value) -> + | VSharedLoan (bids, shared_value) -> if V.BorrowId.Set.mem bid bids then ( (* This is the loan we are looking for *) set_replaced (); @@ -635,21 +635,21 @@ let give_back_shared _config (bid : V.BorrowId.id) (ctx : C.eval_ctx) : * loan identifier *) if V.BorrowId.Set.cardinal bids = 1 then shared_value.V.value else - V.Loan - (V.SharedLoan (V.BorrowId.Set.remove bid bids, shared_value))) + VLoan + (VSharedLoan (V.BorrowId.Set.remove bid bids, shared_value))) else (* Not the loan we are looking for: continue exploring *) - V.Loan (super#visit_SharedLoan opt_abs bids shared_value) - | V.MutLoan bid' -> + VLoan (super#visit_VSharedLoan opt_abs bids shared_value) + | VMutLoan bid' -> (* We are giving back a *shared* borrow: nothing special to do *) - V.Loan (super#visit_MutLoan opt_abs bid') + VLoan (super#visit_VMutLoan opt_abs bid') method! visit_ALoan opt_abs lc = match lc with - | V.AMutLoan (bid, av) -> + | AMutLoan (bid, av) -> (* Nothing special to do (we are giving back a *shared* borrow) *) - V.ALoan (super#visit_AMutLoan opt_abs bid av) - | V.ASharedLoan (bids, shared_value, child) -> + ALoan (super#visit_AMutLoan opt_abs bid av) + | ASharedLoan (bids, shared_value, child) -> if V.BorrowId.Set.mem bid bids then ( (* This is the loan we are looking for *) set_replaced (); @@ -657,24 +657,24 @@ let give_back_shared _config (bid : V.BorrowId.id) (ctx : C.eval_ctx) : * to end the loan. Otherwise, we just remove the current * loan identifier *) if V.BorrowId.Set.cardinal bids = 1 then - V.ALoan (V.AEndedSharedLoan (shared_value, child)) + ALoan (AEndedSharedLoan (shared_value, child)) else - V.ALoan - (V.ASharedLoan + ALoan + (ASharedLoan (V.BorrowId.Set.remove bid bids, shared_value, child))) else (* Not the loan we are looking for: continue exploring *) super#visit_ALoan opt_abs lc - | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } (* Nothing special to do (the loan has ended) *) - | V.AEndedSharedLoan (_, _) + | AEndedSharedLoan (_, _) (* Nothing special to do (the loan has ended) *) - | V.AIgnoredMutLoan (_, _) + | AIgnoredMutLoan (_, _) (* Nothing special to do (we are giving back a *shared* borrow) *) - | V.AEndedIgnoredMutLoan + | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } (* Nothing special to do *) - | V.AIgnoredSharedLoan _ -> + | AIgnoredSharedLoan _ -> (* Nothing special to do *) super#visit_ALoan opt_abs lc end @@ -705,15 +705,15 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id) object inherit [_] C.map_env as super - method! visit_SharedLoan env bids sv = + method! visit_VSharedLoan env bids sv = (* Shared loan: check if the borrow id we are looking for is in the set of borrow ids. If yes, insert the new borrow id, otherwise explore inside the shared value *) if V.BorrowId.Set.mem original_bid bids then ( set_ref (); let bids' = V.BorrowId.Set.add new_bid bids in - V.SharedLoan (bids', sv)) - else super#visit_SharedLoan env bids sv + VSharedLoan (bids', sv)) + else super#visit_VSharedLoan env bids sv method! visit_ASharedLoan env bids v av = (* This case is similar to the {!SharedLoan} case *) @@ -794,7 +794,7 @@ let give_back (config : C.config) (abs_id_opt : V.AbstractionId.id option) { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } in match bc with - | Concrete (V.MutBorrow (l', tv)) -> + | Concrete (VMutBorrow (l', tv)) -> (* Sanity check *) assert (l' = l); assert (not (loans_in_value tv)); @@ -802,14 +802,14 @@ let give_back (config : C.config) (abs_id_opt : V.AbstractionId.id option) assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); (* Update the context *) give_back_value config l tv ctx - | Concrete (V.SharedBorrow l' | V.ReservedMutBorrow l') -> + | Concrete (VSharedBorrow l' | VReservedMutBorrow l') -> (* Sanity check *) assert (l' = l); (* Check that the borrow is somewhere - purely a sanity check *) assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); (* Update the context *) give_back_shared config l ctx - | Abstract (V.AMutBorrow (l', av)) -> + | Abstract (AMutBorrow (l', av)) -> (* Sanity check *) assert (l' = l); (* Check that the corresponding loan is somewhere - purely a sanity check *) @@ -826,21 +826,21 @@ let give_back (config : C.config) (abs_id_opt : V.AbstractionId.id option) give_back_avalue_to_same_abstraction config l av (mk_typed_value_from_symbolic_value sv) ctx - | Abstract (V.ASharedBorrow l') -> + | Abstract (ASharedBorrow l') -> (* Sanity check *) assert (l' = l); (* Check that the borrow is somewhere - purely a sanity check *) assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); (* Update the context *) give_back_shared config l ctx - | Abstract (V.AProjSharedBorrow asb) -> + | Abstract (AProjSharedBorrow asb) -> (* Sanity check *) assert (borrow_in_asb l asb); (* Update the context *) give_back_shared config l ctx | Abstract - ( V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ - | V.AEndedSharedBorrow ) -> + ( AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ + | AEndedSharedBorrow ) -> raise (Failure "Unreachable") let check_borrow_disappeared (fun_name : string) (l : V.BorrowId.id) @@ -970,7 +970,7 @@ let rec end_borrow_aux (config : C.config) (chain : borrow_or_abs_ids) | Ok (ctx, Some (abs_id_opt, bc)) -> (* Sanity check: the borrowed value shouldn't contain loans *) (match bc with - | Concrete (V.MutBorrow (_, bv)) -> + | Concrete (VMutBorrow (_, bv)) -> assert (Option.is_none (get_first_loan_in_value bv)) | _ -> ()); (* Give back the value *) @@ -1182,8 +1182,8 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) (** We may need to end borrows in "regular" values, because of shared values *) method! visit_borrow_content _ bc = match bc with - | V.SharedBorrow _ | V.MutBorrow (_, _) -> raise (FoundBorrowContent bc) - | V.ReservedMutBorrow _ -> raise (Failure "Unreachable") + | VSharedBorrow _ | VMutBorrow (_, _) -> raise (FoundBorrowContent bc) + | VReservedMutBorrow _ -> raise (Failure "Unreachable") end in (* Lookup the abstraction *) @@ -1272,7 +1272,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) ^ borrow_content_to_string ctx bc)); let ctx = match bc with - | V.SharedBorrow bid -> ( + | VSharedBorrow bid -> ( (* Replace the shared borrow with bottom *) let allow_inner_loans = false in match @@ -1282,7 +1282,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) | Ok (ctx, _) -> (* Give back *) give_back_shared config bid ctx) - | V.MutBorrow (bid, v) -> ( + | VMutBorrow (bid, v) -> ( (* Replace the mut borrow with bottom *) let allow_inner_loans = false in match @@ -1293,7 +1293,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) (* Give the value back - note that the mut borrow was below a * shared borrow: the value is thus unchanged *) give_back_value config bid v ctx) - | V.ReservedMutBorrow _ -> raise (Failure "Unreachable") + | VReservedMutBorrow _ -> raise (Failure "Unreachable") in (* Reexplore *) end_abstraction_borrows config chain abs_id cf ctx @@ -1501,9 +1501,9 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in match lookup_loan ek l ctx with - | _, Concrete (V.MutLoan _) -> + | _, Concrete (VMutLoan _) -> raise (Failure "Expected a shared loan, found a mut loan") - | _, Concrete (V.SharedLoan (bids, sv)) -> + | _, Concrete (VSharedLoan (bids, sv)) -> (* Check that there is only one borrow id (l) and update the loan *) assert (V.BorrowId.Set.mem l bids && V.BorrowId.Set.cardinal bids = 1); (* We need to check that there aren't any loans in the value: @@ -1515,7 +1515,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (* Check there aren't reserved borrows *) assert (not (reserved_in_value sv)); (* Update the loan content *) - let ctx = update_loan ek l (V.MutLoan l) ctx in + let ctx = update_loan ek l (VMutLoan l) ctx in (* Continue *) cf sv ctx | _, Abstract _ -> @@ -1542,11 +1542,11 @@ let replace_reserved_borrow_with_mut_borrow (l : V.BorrowId.id) (cf : m_fun) in let ctx = match lookup_borrow ek l ctx with - | Concrete (V.SharedBorrow _ | V.MutBorrow (_, _)) -> + | Concrete (VSharedBorrow _ | VMutBorrow (_, _)) -> raise (Failure "Expected a reserved mutable borrow") - | Concrete (V.ReservedMutBorrow _) -> + | Concrete (VReservedMutBorrow _) -> (* Update it *) - update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx + update_borrow ek l (VMutBorrow (l, borrowed_value)) ctx | Abstract _ -> (* This can't happen for sure *) raise @@ -1566,8 +1566,8 @@ let rec promote_reserved_mut_borrow (config : C.config) (l : V.BorrowId.id) : { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in match lookup_loan ek l ctx with - | _, Concrete (V.MutLoan _) -> raise (Failure "Unreachable") - | _, Concrete (V.SharedLoan (bids, sv)) -> ( + | _, Concrete (VMutLoan _) -> raise (Failure "Unreachable") + | _, Concrete (VSharedLoan (bids, sv)) -> ( (* If there are loans inside the value, end them. Note that there can't be reserved borrows inside the value. If we perform an update, do a recursive call to lookup the updated value *) @@ -1576,8 +1576,8 @@ let rec promote_reserved_mut_borrow (config : C.config) (l : V.BorrowId.id) : (* End the loans *) let cc = match lc with - | V.SharedLoan (bids, _) -> end_borrows config bids - | V.MutLoan bid -> end_borrow config bid + | VSharedLoan (bids, _) -> end_borrows config bids + | VMutLoan bid -> end_borrow config bid in (* Recursive call *) let cc = comp cc (promote_reserved_mut_borrow config l) in @@ -1637,8 +1637,8 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) (* Function to explore an avalue and destructure it *) let rec list_avalues (allow_borrows : bool) (push : V.typed_avalue -> unit) (av : V.typed_avalue) : unit = - let ty = av.V.ty in - match av.V.value with + let ty = av.ty in + match av.value with | ABottom | AIgnored -> () | AAdt adt -> (* Simply explore the children *) @@ -1646,17 +1646,17 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) | ALoan lc -> ( (* Explore the loan content *) match lc with - | V.ASharedLoan (bids, sv, child_av) -> + | ASharedLoan (bids, sv, child_av) -> (* We don't support nested borrows for now *) - assert (not (value_has_borrows ctx sv.V.value)); + assert (not (value_has_borrows ctx sv.value)); (* Destructure the shared value *) let avl, sv = if destructure_shared_values then list_values sv else ([], sv) in (* Push a value *) - let ignored = mk_aignored child_av.V.ty in - let value = V.ALoan (V.ASharedLoan (bids, sv, ignored)) in - push { V.value; ty }; + let ignored = mk_aignored child_av.ty in + let value = V.ALoan (ASharedLoan (bids, sv, ignored)) in + push { value; ty }; (* Explore the child *) list_avalues false push_fail child_av; (* Push the avalues introduced because we decomposed the inner loans - @@ -1666,25 +1666,25 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) exactly the same way as [list_avalues] (i.e., with a similar signature) *) List.iter push avl - | V.AMutLoan (bid, child_av) -> + | AMutLoan (bid, child_av) -> (* Explore the child *) list_avalues false push_fail child_av; (* Explore the whole loan *) - let ignored = mk_aignored child_av.V.ty in - let value = V.ALoan (V.AMutLoan (bid, ignored)) in - push { V.value; ty } - | V.AIgnoredMutLoan (opt_bid, child_av) -> + let ignored = mk_aignored child_av.ty in + let value = V.ALoan (AMutLoan (bid, ignored)) in + push { value; ty } + | AIgnoredMutLoan (opt_bid, child_av) -> (* We don't support nested borrows for now *) assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); assert (opt_bid = None); (* Simply explore the child *) list_avalues false push_fail child_av - | V.AEndedMutLoan + | AEndedMutLoan { child = child_av; given_back = _; given_back_meta = _ } - | V.AEndedSharedLoan (_, child_av) - | V.AEndedIgnoredMutLoan + | AEndedSharedLoan (_, child_av) + | AEndedIgnoredMutLoan { child = child_av; given_back = _; given_back_meta = _ } - | V.AIgnoredSharedLoan child_av -> + | AIgnoredSharedLoan child_av -> (* We don't support nested borrows for now *) assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); (* Simply explore the child *) @@ -1694,34 +1694,34 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) assert allow_borrows; (* Explore the borrow content *) match bc with - | V.AMutBorrow (bid, child_av) -> + | AMutBorrow (bid, child_av) -> (* Explore the child *) list_avalues false push_fail child_av; (* Explore the borrow *) - let ignored = mk_aignored child_av.V.ty in - let value = V.ABorrow (V.AMutBorrow (bid, ignored)) in - push { V.value; ty } - | V.ASharedBorrow _ -> + let ignored = mk_aignored child_av.ty in + let value = V.ABorrow (AMutBorrow (bid, ignored)) in + push { value; ty } + | ASharedBorrow _ -> (* Nothing specific to do: keep the value as it is *) push av - | V.AIgnoredMutBorrow (opt_bid, child_av) -> + | AIgnoredMutBorrow (opt_bid, child_av) -> (* We don't support nested borrows for now *) assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); assert (opt_bid = None); (* Just explore the child *) list_avalues false push_fail child_av - | V.AEndedIgnoredMutBorrow + | AEndedIgnoredMutBorrow { child = child_av; given_back = _; given_back_meta = _ } -> (* We don't support nested borrows for now *) assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); (* Just explore the child *) list_avalues false push_fail child_av - | V.AProjSharedBorrow asb -> + | AProjSharedBorrow asb -> (* We don't support nested borrows *) assert (asb = []); (* Nothing specific to do *) () - | V.AEndedMutBorrow _ | V.AEndedSharedBorrow -> + | AEndedMutBorrow _ | AEndedSharedBorrow -> (* If we get there it means the abstraction ended: it should not be in the context anymore (if we end *one* borrow in an abstraction, we have to end them all and remove the abstraction from the context) @@ -1732,29 +1732,29 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) expanded *) assert (not (ty_has_borrows ctx.type_context.type_infos ty)) and list_values (v : V.typed_value) : V.typed_avalue list * V.typed_value = - let ty = v.V.ty in - match v.V.value with + let ty = v.ty in + match v.value with | VLiteral _ -> ([], v) | VAdt adt -> let avll, field_values = List.split (List.map list_values adt.field_values) in let avl = List.concat avll in - let adt = { adt with V.field_values } in - (avl, { v with V.value = VAdt adt }) - | Bottom -> raise (Failure "Unreachable") - | Borrow _ -> + let adt = { adt with field_values } in + (avl, { v with value = VAdt adt }) + | VBottom -> raise (Failure "Unreachable") + | VBorrow _ -> (* We don't support nested borrows for now *) raise (Failure "Unreachable") - | Loan lc -> ( + | VLoan lc -> ( match lc with - | SharedLoan (bids, sv) -> + | VSharedLoan (bids, sv) -> let avl, sv = list_values sv in if destructure_shared_values then ( (* Rem.: the shared value can't contain loans nor borrows *) assert (ty_no_regions ty); let av : V.typed_avalue = - assert (not (value_has_loans_or_borrows ctx sv.V.value)); + assert (not (value_has_loans_or_borrows ctx sv.value)); (* We introduce fresh ids for the symbolic values *) let mk_value_with_fresh_sids (v : V.typed_value) : V.typed_value = @@ -1770,16 +1770,14 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) in let sv = mk_value_with_fresh_sids sv in (* Create the new avalue *) - let value = - V.ALoan (V.ASharedLoan (bids, sv, mk_aignored ty)) - in - { V.value; ty } + let value = V.ALoan (ASharedLoan (bids, sv, mk_aignored ty)) in + { value; ty } in let avl = List.append [ av ] avl in (avl, sv)) - else (avl, { v with V.value = V.Loan (V.SharedLoan (bids, sv)) }) - | MutLoan _ -> raise (Failure "Unreachable")) - | Symbolic _ -> + else (avl, { v with value = VLoan (VSharedLoan (bids, sv)) }) + | VMutLoan _ -> raise (Failure "Unreachable")) + | VSymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) assert (not (ty_has_borrows ctx.type_context.type_infos ty)); @@ -1787,10 +1785,10 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) in (* Destructure the avalues *) - List.iter (list_avalues true push_avalue) abs0.V.avalues; + List.iter (list_avalues true push_avalue) abs0.avalues; let avalues = !avalues in (* Update *) - { abs0 with V.avalues; kind = abs_kind; can_end } + { abs0 with avalues; kind = abs_kind; can_end } let abs_is_destructured (destructure_shared_values : bool) (ctx : C.eval_ctx) (abs : V.abs) : bool = @@ -1840,14 +1838,14 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool) ("convert_value_to_abstractions: to_avalues:\n- value: " ^ typed_value_to_string ctx v)); - let ty = v.V.ty in - match v.V.value with - | V.VLiteral _ -> ([], v) - | V.Bottom -> + let ty = v.ty in + match v.value with + | VLiteral _ -> ([], v) + | VBottom -> (* Can happen: we *do* convert dummy values to abstractions, and dummy values can contain bottoms *) ([], v) - | V.VAdt adt -> + | VAdt adt -> (* Two cases, depending on whether we have to group all the borrows/loans inside one abstraction or not *) let avl, field_values = @@ -1879,72 +1877,72 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool) ([], field_values) in let adt = { adt with field_values } in - (avl, { v with V.value = V.VAdt adt }) - | V.Borrow bc -> ( + (avl, { v with value = VAdt adt }) + | VBorrow bc -> ( let _, ref_ty, kind = ty_as_ref ty in assert (ty_no_regions ref_ty); (* Sanity check *) assert allow_borrows; (* Convert the borrow content *) match bc with - | SharedBorrow bid -> + | VSharedBorrow bid -> assert (ty_no_regions ref_ty); - let ty = T.TRef (T.RVar r_id, ref_ty, kind) in - let value = V.ABorrow (V.ASharedBorrow bid) in + let ty = T.TRef (RVar r_id, ref_ty, kind) in + let value = V.ABorrow (ASharedBorrow bid) in ([ { V.value; ty } ], v) - | MutBorrow (bid, bv) -> + | VMutBorrow (bid, bv) -> let r_id = if group then r_id else C.fresh_region_id () in (* We don't support nested borrows for now *) - assert (not (value_has_borrows ctx bv.V.value)); + assert (not (value_has_borrows ctx bv.value)); (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *) - let ty = T.TRef (T.RVar r_id, ref_ty, kind) in + let ty = T.TRef (RVar r_id, ref_ty, kind) in let ignored = mk_aignored ref_ty in - let av = V.ABorrow (V.AMutBorrow (bid, ignored)) in + let av = V.ABorrow (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) *) let avl, bv = to_avalues false true true r_id bv in - let value = { v with V.value = V.Borrow (V.MutBorrow (bid, bv)) } in + let value = { v with value = VBorrow (VMutBorrow (bid, bv)) } in (av :: avl, value) - | ReservedMutBorrow _ -> + | VReservedMutBorrow _ -> (* This borrow should have been activated *) raise (Failure "Unexpected")) - | V.Loan lc -> ( + | VLoan lc -> ( match lc with - | V.SharedLoan (bids, sv) -> + | VSharedLoan (bids, sv) -> let r_id = if group then r_id else C.fresh_region_id () in (* We don't support nested borrows for now *) - assert (not (value_has_borrows ctx sv.V.value)); + assert (not (value_has_borrows ctx sv.value)); (* Push the avalue - note that we use [AIgnore] for the inner avalue *) (* For avalues, a loan has the borrow type *) assert (ty_no_regions ty); - let ty = mk_ref_ty (T.RVar r_id) ty T.Shared in + let ty = mk_ref_ty (RVar r_id) ty Shared in let ignored = mk_aignored ty in (* Rem.: the shared value might contain loans *) let avl, sv = to_avalues false true true r_id sv in - let av = V.ALoan (V.ASharedLoan (bids, sv, ignored)) in + let av = V.ALoan (ASharedLoan (bids, sv, 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) *) let value : V.value = - if destructure_shared_values then sv.V.value - else V.Loan (V.SharedLoan (bids, sv)) + if destructure_shared_values then sv.value + else VLoan (VSharedLoan (bids, sv)) in - let value = { v with V.value } in + let value = { v with value } in (av :: avl, value) - | V.MutLoan bid -> + | VMutLoan bid -> (* Push the avalue - note that we use [AIgnore] for the inner avalue *) (* For avalues, a loan has the borrow type *) assert (ty_no_regions ty); - let ty = mk_ref_ty (T.RVar r_id) ty T.Mut in + let ty = mk_ref_ty (RVar r_id) ty Mut in let ignored = mk_aignored ty in - let av = V.ALoan (V.AMutLoan (bid, ignored)) in + let av = V.ALoan (AMutLoan (bid, ignored)) in let av = { V.value = av; ty } in ([ av ], v)) - | V.Symbolic _ -> + | VSymbolic _ -> (* 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 ctx v.V.value)); + assert (not (value_has_borrows ctx v.value)); (* Return nothing *) ([], v) in @@ -2043,8 +2041,8 @@ let compute_merge_abstraction_info (ctx : C.eval_ctx) (abs : V.abs) : | Abstract _ -> raise (Failure "Unreachable") in (match lc with - | SharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc)) - | MutLoan _ -> raise (Failure "Unreachable")); + | VSharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc)) + | VMutLoan _ -> raise (Failure "Unreachable")); (* Continue *) super#visit_loan_content env lc diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 8807f3ef..cde39e9b 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -222,15 +222,15 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) method! visit_borrow_content env bc = match bc with - | V.SharedBorrow bid -> + | V.VSharedBorrow bid -> (* Nothing specific to do *) - super#visit_SharedBorrow env bid - | V.ReservedMutBorrow bid -> + super#visit_VSharedBorrow env bid + | V.VReservedMutBorrow bid -> (* Nothing specific to do *) - super#visit_ReservedMutBorrow env bid - | V.MutBorrow (bid, mv) -> + super#visit_VReservedMutBorrow env bid + | V.VMutBorrow (bid, mv) -> (* Control the dive *) - if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv + if ek.enter_mut_borrows then super#visit_VMutBorrow env bid mv else () (** We reimplement {!visit_Loan} (rather than the more precise functions @@ -240,17 +240,17 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) *) method! visit_loan_content env lc = match lc with - | V.SharedLoan (bids, sv) -> + | V.VSharedLoan (bids, sv) -> (* Check if this is the loan we are looking for, and control the dive *) if V.BorrowId.Set.mem l bids then raise (FoundGLoanContent (Concrete lc)) else if ek.enter_shared_loans then - super#visit_SharedLoan env bids sv + super#visit_VSharedLoan env bids sv else () - | V.MutLoan bid -> + | V.VMutLoan bid -> (* Check if this is the loan we are looking for *) if bid = l then raise (FoundGLoanContent (Concrete lc)) - else super#visit_MutLoan env bid + else super#visit_VMutLoan env bid (** Note that we don't control diving inside the abstractions: if we allow to dive inside abstractions, we allow to go anywhere @@ -335,28 +335,28 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id) method! visit_borrow_content env bc = match bc with - | V.SharedBorrow _ | V.ReservedMutBorrow _ -> + | VSharedBorrow _ | VReservedMutBorrow _ -> (* Nothing specific to do *) super#visit_borrow_content env bc - | V.MutBorrow (bid, mv) -> + | VMutBorrow (bid, mv) -> (* Control the dive into mutable borrows *) - if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv - else V.MutBorrow (bid, mv) + if ek.enter_mut_borrows then super#visit_VMutBorrow env bid mv + else VMutBorrow (bid, mv) (** We reimplement {!visit_loan_content} (rather than one of the sub- functions) on purpose: exhaustive matches are good for maintenance *) method! visit_loan_content env lc = match lc with - | V.SharedLoan (bids, sv) -> + | VSharedLoan (bids, sv) -> (* Shared loan: check if this is the loan we are looking for, and control the dive. *) if V.BorrowId.Set.mem l bids then update () else if ek.enter_shared_loans then - super#visit_SharedLoan env bids sv - else V.SharedLoan (bids, sv) - | V.MutLoan bid -> + super#visit_VSharedLoan env bids sv + else VSharedLoan (bids, sv) + | VMutLoan bid -> (* Mut loan: checks if this is the loan we are looking for *) - if bid = l then update () else super#visit_MutLoan env bid + if bid = l then update () else super#visit_VMutLoan env bid (** Note that once inside the abstractions, we don't control diving (there are no use cases requiring finer control). @@ -432,42 +432,42 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) method! visit_borrow_content env bc = match bc with - | V.MutBorrow (bid, mv) -> + | VMutBorrow (bid, mv) -> (* Check the borrow id and control the dive *) if bid = l then raise (FoundGBorrowContent (Concrete bc)) - else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv + else if ek.enter_mut_borrows then super#visit_VMutBorrow env bid mv else () - | V.SharedBorrow bid -> + | VSharedBorrow bid -> (* Check the borrow id *) if bid = l then raise (FoundGBorrowContent (Concrete bc)) else () - | V.ReservedMutBorrow bid -> + | VReservedMutBorrow bid -> (* Check the borrow id *) if bid = l then raise (FoundGBorrowContent (Concrete bc)) else () method! visit_loan_content env lc = match lc with - | V.MutLoan bid -> - (* Nothing special to do *) super#visit_MutLoan env bid - | V.SharedLoan (bids, sv) -> + | VMutLoan bid -> + (* Nothing special to do *) super#visit_VMutLoan env bid + | VSharedLoan (bids, sv) -> (* Control the dive *) - if ek.enter_shared_loans then super#visit_SharedLoan env bids sv + if ek.enter_shared_loans then super#visit_VSharedLoan env bids sv else () method! visit_aborrow_content env bc = match bc with - | V.AMutBorrow (bid, av) -> + | AMutBorrow (bid, av) -> if bid = l then raise (FoundGBorrowContent (Abstract bc)) else super#visit_AMutBorrow env bid av - | V.ASharedBorrow bid -> + | ASharedBorrow bid -> if bid = l then raise (FoundGBorrowContent (Abstract bc)) else super#visit_ASharedBorrow env bid - | V.AIgnoredMutBorrow (_, _) - | V.AEndedMutBorrow _ - | V.AEndedIgnoredMutBorrow + | AIgnoredMutBorrow (_, _) + | AEndedMutBorrow _ + | AEndedIgnoredMutBorrow { given_back = _; child = _; given_back_meta = _ } - | V.AEndedSharedBorrow -> + | AEndedSharedBorrow -> super#visit_aborrow_content env bc - | V.AProjSharedBorrow asb -> + | AProjSharedBorrow asb -> if borrow_in_asb l asb then raise (FoundGBorrowContent (Abstract bc)) else () @@ -516,27 +516,28 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) method! visit_borrow_content env bc = match bc with - | V.MutBorrow (bid, mv) -> + | VMutBorrow (bid, mv) -> (* Check the id and control dive *) if bid = l then update () - else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv - else V.MutBorrow (bid, mv) - | V.SharedBorrow bid -> + else if ek.enter_mut_borrows then super#visit_VMutBorrow env bid mv + else VMutBorrow (bid, mv) + | VSharedBorrow bid -> (* Check the id *) - if bid = l then update () else super#visit_SharedBorrow env bid - | V.ReservedMutBorrow bid -> + if bid = l then update () else super#visit_VSharedBorrow env bid + | VReservedMutBorrow bid -> (* Check the id *) - if bid = l then update () else super#visit_ReservedMutBorrow env bid + if bid = l then update () + else super#visit_VReservedMutBorrow env bid method! visit_loan_content env lc = match lc with - | V.SharedLoan (bids, sv) -> + | VSharedLoan (bids, sv) -> (* Control the dive *) - if ek.enter_shared_loans then super#visit_SharedLoan env bids sv - else V.SharedLoan (bids, sv) - | V.MutLoan bid -> + if ek.enter_shared_loans then super#visit_VSharedLoan env bids sv + else VSharedLoan (bids, sv) + | VMutLoan bid -> (* Nothing specific to do *) - super#visit_MutLoan env bid + super#visit_VMutLoan env bid method! visit_abs env abs = if ek.enter_abs then super#visit_abs env abs else abs @@ -1192,18 +1193,18 @@ let get_first_non_ignored_aloan_in_abstraction (abs : V.abs) : (** We may need to visit loan contents because of shared values *) method! visit_loan_content _ lc = match lc with - | V.MutLoan _ -> + | VMutLoan _ -> (* The mut loan linked to the mutable borrow present in a shared * value in an abstraction should be in an AProjBorrows *) raise (Failure "Unreachable") - | V.SharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids)) + | VSharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids)) method! visit_aproj env sproj = (match sproj with - | V.AProjBorrows (_, _) - | V.AEndedProjLoans _ | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> + | AProjBorrows (_, _) + | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> () - | V.AProjLoans (sv, _) -> raise (ValuesUtils.FoundSymbolicValue sv)); + | AProjLoans (sv, _) -> raise (ValuesUtils.FoundSymbolicValue sv)); super#visit_aproj env sproj end in @@ -1225,7 +1226,7 @@ let lookup_shared_value_opt (ctx : C.eval_ctx) (bid : V.BorrowId.id) : | None -> None | Some (_, lc) -> ( match lc with - | Concrete (SharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> + | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> Some sv | _ -> None) diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index b07f2629..2b7ff7d0 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -183,9 +183,9 @@ let replace_symbolic_values (at_most_once : bool) object inherit [_] C.map_eval_ctx as super - method! visit_Symbolic env spc = + method! visit_VSymbolic env spc = if same_symbolic_id spc original_sv then replace () - else super#visit_Symbolic env spc + else super#visit_VSymbolic env spc end in (* Apply the substitution *) @@ -326,11 +326,11 @@ let expand_symbolic_value_shared_borrow (config : C.config) object (self) inherit [_] C.map_eval_ctx as super - method! visit_Symbolic env sv = + method! visit_VSymbolic env sv = if same_symbolic_id sv original_sv then let bid = fresh_borrow () in - V.Borrow (V.SharedBorrow bid) - else super#visit_Symbolic env sv + VBorrow (VSharedBorrow bid) + else super#visit_VSymbolic env sv method! visit_EAbs proj_regions abs = assert (Option.is_none proj_regions); @@ -639,7 +639,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = object inherit [_] C.iter_eval_ctx - method! visit_Symbolic _ sv = + method! visit_VSymbolic _ sv = if ty_has_borrows ctx.type_context.type_infos sv.V.sv_ty then raise (FoundSymbolicValue sv) else () @@ -664,22 +664,22 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = ("greedy_expand_symbolics_with_borrows: about to expand: " ^ symbolic_value_to_string ctx sv)); let cc : cm_fun = - match sv.V.sv_ty with - | T.TAdt (TAdtId def_id, _) -> + match sv.sv_ty with + | TAdt (TAdtId def_id, _) -> (* {!expand_symbolic_value_no_branching} checks if there are branchings, * but we prefer to also check it here - this leads to cleaner messages * and debugging *) let def = C.ctx_lookup_type_decl ctx def_id in (match def.kind with - | T.Struct _ | T.Enum ([] | [ _ ]) -> () - | T.Enum (_ :: _) -> + | Struct _ | Enum ([] | [ _ ]) -> () + | Enum (_ :: _) -> raise (Failure ("Attempted to greedily expand a symbolic enumeration \ with > 1 variants (option \ [greedy_expand_symbolics_with_borrows] of [config]): " ^ Print.name_to_string def.name)) - | T.Opaque -> + | Opaque -> raise (Failure "Attempted to greedily expand an opaque type")); (* Also, we need to check if the definition is recursive *) if C.ctx_type_decl_is_rec ctx def_id then @@ -690,16 +690,15 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = [config]): " ^ Print.name_to_string def.name)) else expand_symbolic_value_no_branching config sv None - | T.TAdt ((TTuple | TAssumed TBox), _) | T.TRef (_, _, _) -> + | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) -> (* Ok *) expand_symbolic_value_no_branching config sv None - | T.TAdt (TAssumed (TArray | TSlice | TStr), _) -> + | TAdt (TAssumed (TArray | TSlice | TStr), _) -> (* We can't expand those *) raise (Failure "Attempted to greedily expand an ADT which can't be expanded ") - | T.TVar _ | T.TLiteral _ | TNever | T.TTraitType _ | T.TArrow _ - | T.TRawPtr _ -> + | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ -> raise (Failure "Unreachable") in (* Compose and continue *) diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 7865d7be..58426cad 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -137,18 +137,18 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) * we reverted the changes: the result was less clear actually. In particular, * the fact that we have exhaustive matches below makes very obvious the cases * in which we need to fail *) - match v.V.value with - | V.VLiteral _ -> (ctx, v) - | V.VAdt av -> + match v.value with + | VLiteral _ -> (ctx, v) + | VAdt av -> (* Sanity check *) - (match v.V.ty with - | T.TAdt (T.TAssumed T.TBox, _) -> + (match v.ty with + | TAdt (TAssumed TBox, _) -> raise (Failure "Can't copy an assumed value other than Option") - | T.TAdt (T.TAdtId _, _) as ty -> + | TAdt (TAdtId _, _) as ty -> assert (allow_adt_copy || ty_is_primitively_copyable ty) - | T.TAdt (T.TTuple, _) -> () (* Ok *) - | T.TAdt - ( T.TAssumed (TSlice | T.TArray), + | TAdt (TTuple, _) -> () (* Ok *) + | TAdt + ( TAssumed (TSlice | TArray), { regions = []; types = [ ty ]; @@ -162,33 +162,33 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) (copy_value allow_adt_copy config) ctx av.field_values in - (ctx, { v with V.value = V.VAdt { av with field_values = fields } }) - | V.Bottom -> raise (Failure "Can't copy ⊥") - | V.Borrow bc -> ( + (ctx, { v with value = VAdt { av with field_values = fields } }) + | VBottom -> raise (Failure "Can't copy ⊥") + | VBorrow bc -> ( (* We can only copy shared borrows *) match bc with - | SharedBorrow bid -> + | VSharedBorrow bid -> (* We need to create a new borrow id for the copied borrow, and * update the context accordingly *) let bid' = C.fresh_borrow_id () in let ctx = InterpreterBorrows.reborrow_shared bid bid' ctx in - (ctx, { v with V.value = V.Borrow (SharedBorrow bid') }) - | MutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow") - | V.ReservedMutBorrow _ -> + (ctx, { v with value = VBorrow (VSharedBorrow bid') }) + | VMutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow") + | VReservedMutBorrow _ -> raise (Failure "Can't copy a reserved mut borrow")) - | V.Loan lc -> ( + | VLoan lc -> ( (* We can only copy shared loans *) match lc with - | V.MutLoan _ -> raise (Failure "Can't copy a mutable loan") - | V.SharedLoan (_, sv) -> + | VMutLoan _ -> raise (Failure "Can't copy a mutable loan") + | VSharedLoan (_, sv) -> (* We don't copy the shared loan: only the shared value inside *) copy_value allow_adt_copy config ctx sv) - | V.Symbolic sp -> + | VSymbolic sp -> (* We can copy only if the type is "primitively" copyable. * Note that in the general case, copy is a trait: copying values * thus requires calling the proper function. Here, we copy values * for very simple types such as integers, shared borrows, etc. *) - assert (ty_is_primitively_copyable (Subst.erase_regions sp.V.sv_ty)); + assert (ty_is_primitively_copyable (Subst.erase_regions sp.sv_ty)); (* If the type is copyable, we simply return the current value. Side * remark: what is important to look at when copying symbolic values * is symbolic expansion. The important subcase is the expansion of shared @@ -239,16 +239,16 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) : let prepare : cm_fun = fun cf ctx -> match op with - | E.Constant _ -> + | Constant _ -> (* No need to reorganize the context *) cf ctx - | E.Copy p -> + | Copy p -> (* Access the value *) let access = Read in (* Expand the symbolic values, if necessary *) let expand_prim_copy = true in access_rplace_reorganize config expand_prim_copy access p cf ctx - | E.Move p -> + | Move p -> (* Access the value *) let access = Move in let expand_prim_copy = false in @@ -268,11 +268,11 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n")); (* Evaluate *) match op with - | E.Constant cv -> ( + | Constant cv -> ( match cv.value with - | E.CLiteral lit -> + | CLiteral lit -> cf (literal_to_typed_value (TypesUtils.ty_as_literal cv.ty) lit) ctx - | E.CTraitConst (trait_ref, generics, const_name) -> ( + | CTraitConst (trait_ref, generics, const_name) -> ( assert (generics = TypesUtils.mk_empty_generic_args); match trait_ref.trait_id with | T.TraitImpl _ -> @@ -307,7 +307,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) SymbolicAst.VaTraitConstValue (trait_ref, generics, const_name), e )))) - | E.CVar vid -> ( + | CVar vid -> ( let ctx0 = ctx in (* Lookup the const generic value *) let cv = C.ctx_lookup_const_generic_value ctx vid in @@ -331,8 +331,8 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) value_as_symbolic v.value, SymbolicAst.VaCGValue vid, e ))) - | E.CFnPtr _ -> raise (Failure "TODO")) - | E.Copy p -> + | CFnPtr _ -> raise (Failure "TODO")) + | Copy p -> (* Access the value *) let access = Read in let cc = read_place access p in @@ -353,7 +353,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) in (* Compose and apply *) comp cc copy cf ctx - | E.Move p -> + | Move p -> (* Access the value *) let access = Move in let cc = read_place access p in @@ -362,7 +362,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) fun ctx -> (* Check that there are no bottoms in the value we are about to move *) assert (not (bottom_in_value ctx.ended_regions v)); - let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in + let bottom : V.typed_value = { V.value = VBottom; ty = v.ty } in let ctx = write_place access p bottom ctx in cf v ctx in @@ -622,18 +622,18 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> match bkind with - | E.Shared | E.TwoPhaseMut | E.Shallow -> + | Shared | TwoPhaseMut | Shallow -> (* **REMARK**: we initially treated shallow borrows like shared borrows. In practice this restricted the behaviour too much, so for now we forbid them. *) - assert (bkind <> E.Shallow); + assert (bkind <> Shallow); (* Access the value *) let access = match bkind with - | E.Shared | E.Shallow -> Read - | E.TwoPhaseMut -> Write + | Shared | Shallow -> Read + | TwoPhaseMut -> Write | _ -> raise (Failure "Unreachable") in @@ -648,17 +648,17 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) let bid = C.fresh_borrow_id () in (* Compute the loan value, with which to replace the value at place p *) let nv = - match v.V.value with - | V.Loan (V.SharedLoan (bids, sv)) -> + match v.value with + | VLoan (VSharedLoan (bids, sv)) -> (* Shared loan: insert the new borrow id *) let bids1 = V.BorrowId.Set.add bid bids in - { v with V.value = V.Loan (V.SharedLoan (bids1, sv)) } + { v with value = VLoan (VSharedLoan (bids1, sv)) } | _ -> (* Not a shared loan: add a wrapper *) let v' = - V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v)) + V.VLoan (VSharedLoan (V.BorrowId.Set.singleton bid, v)) in - { v with V.value = v' } + { v with value = v' } in (* Update the borrowed value in the context *) let ctx = write_place access p nv ctx in @@ -666,27 +666,27 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) * Note that the reference is *mutable* if we do a two-phase borrow *) let ref_kind = match bkind with - | E.Shared | E.Shallow -> T.Shared - | E.TwoPhaseMut -> T.Mut + | Shared | Shallow -> T.Shared + | TwoPhaseMut -> T.Mut | _ -> raise (Failure "Unreachable") in let rv_ty = T.TRef (T.RErased, v.ty, ref_kind) in let bc = match bkind with - | E.Shared | E.Shallow -> + | Shared | Shallow -> (* See the remark at the beginning of the match branch: we handle shallow borrows like shared borrows *) - V.SharedBorrow bid - | E.TwoPhaseMut -> V.ReservedMutBorrow bid + V.VSharedBorrow bid + | TwoPhaseMut -> VReservedMutBorrow bid | _ -> raise (Failure "Unreachable") in - let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in + let rv : V.typed_value = { value = VBorrow bc; ty = rv_ty } in (* Continue *) cf rv ctx in (* Compose and apply *) comp prepare eval cf ctx - | E.Mut -> + | Mut -> (* Access the value *) let access = Write in let expand_prim_copy = false in @@ -698,12 +698,12 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) fun ctx -> (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) let bid = C.fresh_borrow_id () in - let rv_ty = T.TRef (T.RErased, v.ty, Mut) in + let rv_ty = T.TRef (RErased, v.ty, Mut) in let rv : V.typed_value = - { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty } + { V.value = VBorrow (VMutBorrow (bid, v)); ty = rv_ty } in (* Compute the value with which to replace the value at place p *) - let nv = { v with V.value = V.Loan (V.MutLoan bid) } in + let nv = { v with value = VLoan (VMutLoan bid) } in (* Update the value in the context *) let ctx = write_place access p nv ctx in (* Continue *) @@ -723,7 +723,7 @@ let eval_rvalue_aggregate (config : C.config) fun ctx -> (* Match on the aggregate kind *) match aggregate_kind with - | E.AggregatedAdt (type_id, opt_variant_id, generics) -> ( + | AggregatedAdt (type_id, opt_variant_id, generics) -> ( match type_id with | TTuple -> let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in @@ -755,7 +755,7 @@ let eval_rvalue_aggregate (config : C.config) (* Call the continuation *) cf aggregated ctx | TAssumed _ -> raise (Failure "Unreachable")) - | E.AggregatedArray (ety, cg) -> ( + | AggregatedArray (ety, cg) -> ( (* Sanity check: all the values have the proper type *) assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values); (* Sanity check: the number of values is consistent with the length *) diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 2f7e8f3d..a35b2716 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -227,17 +227,17 @@ let prepare_ashared_loans (loop_id : V.LoopId.id option) : cm_fun = object inherit [_] V.iter_typed_avalue as super - method! visit_SharedLoan env lids sv = + method! visit_VSharedLoan env lids sv = collect_shared_value lids sv; (* Continue the exploration *) - super#visit_SharedLoan env lids sv + super#visit_VSharedLoan env lids sv - method! visit_ASharedLoan env lids sv _ = + method! visit_ASharedLoan env lids sv av = collect_shared_value lids sv; (* Continue the exploration *) - super#visit_SharedLoan env lids sv + super#visit_ASharedLoan env lids sv av (** Check that there are no symbolic values with *borrows* inside the abstraction - shouldn't happen if the symbolic values are greedily @@ -743,8 +743,8 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets) let open InterpreterBorrowsCore in let lookup_shared_loan lid ctx : V.typed_value = match snd (lookup_loan ek_all lid ctx) with - | Concrete (V.SharedLoan (_, v)) -> v - | Abstract (V.ASharedLoan (_, v, _)) -> v + | Concrete (VSharedLoan (_, v)) -> v + | Abstract (ASharedLoan (_, v, _)) -> v | _ -> raise (Failure "Unreachable") in let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in @@ -927,12 +927,12 @@ let compute_fp_ctx_symbolic_values (ctx : C.eval_ctx) (fp_ctx : C.eval_ctx) : inherit [_] C.iter_env (** We lookup the shared values *) - method! visit_SharedBorrow env bid = + method! visit_VSharedBorrow env bid = let open InterpreterBorrowsCore in let v = match snd (lookup_loan ek_all bid fp_ctx) with - | Concrete (V.SharedLoan (_, v)) -> v - | Abstract (V.ASharedLoan (_, v, _)) -> v + | Concrete (VSharedLoan (_, v)) -> v + | Abstract (ASharedLoan (_, v, _)) -> v | _ -> raise (Failure "Unreachable") in self#visit_typed_value env v diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 27020efb..7741abbc 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -212,66 +212,66 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct assert (not (value_has_borrows ctx v1.V.value)); (* Merge *) M.match_distinct_adts ty av0 av1) - | Bottom, Bottom -> v0 - | Borrow bc0, Borrow bc1 -> + | VBottom, VBottom -> v0 + | VBorrow bc0, VBorrow bc1 -> let bc = match (bc0, bc1) with - | SharedBorrow bid0, SharedBorrow bid1 -> + | VSharedBorrow bid0, VSharedBorrow bid1 -> let bid = M.match_shared_borrows match_rec ty bid0 bid1 in - V.SharedBorrow bid - | MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) -> + V.VSharedBorrow bid + | VMutBorrow (bid0, bv0), VMutBorrow (bid1, bv1) -> let bv = match_rec bv0 bv1 in assert (not (value_has_borrows ctx bv.V.value)); let bid, bv = M.match_mut_borrows ty bid0 bv0 bid1 bv1 bv in - V.MutBorrow (bid, bv) - | ReservedMutBorrow _, _ - | _, ReservedMutBorrow _ - | SharedBorrow _, MutBorrow _ - | MutBorrow _, SharedBorrow _ -> + VMutBorrow (bid, bv) + | VReservedMutBorrow _, _ + | _, VReservedMutBorrow _ + | VSharedBorrow _, VMutBorrow _ + | VMutBorrow _, VSharedBorrow _ -> (* If we get here, either there is a typing inconsistency, or we are 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") in - { V.value = V.Borrow bc; ty } - | Loan lc0, Loan lc1 -> + { V.value = VBorrow bc; ty } + | VLoan lc0, VLoan lc1 -> (* TODO: maybe we should enforce that the ids are always exactly the same - without matching *) let lc = match (lc0, lc1) with - | SharedLoan (ids0, sv0), SharedLoan (ids1, sv1) -> + | VSharedLoan (ids0, sv0), VSharedLoan (ids1, sv1) -> let sv = match_rec sv0 sv1 in assert (not (value_has_borrows ctx sv.V.value)); let ids, sv = M.match_shared_loans ty ids0 ids1 sv in - V.SharedLoan (ids, sv) - | MutLoan id0, MutLoan id1 -> + V.VSharedLoan (ids, sv) + | VMutLoan id0, VMutLoan id1 -> let id = M.match_mut_loans ty id0 id1 in - V.MutLoan id - | SharedLoan _, MutLoan _ | MutLoan _, SharedLoan _ -> + VMutLoan id + | VSharedLoan _, VMutLoan _ | VMutLoan _, VSharedLoan _ -> raise (Failure "Unreachable") in - { V.value = Loan lc; ty = v1.V.ty } - | Symbolic sv0, Symbolic sv1 -> + { V.value = VLoan lc; ty = v1.V.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 *) assert (not (value_has_borrows ctx v0.V.value)); assert (not (value_has_borrows ctx v1.V.value)); (* Match *) let sv = M.match_symbolic_values sv0 sv1 in - { v1 with V.value = V.Symbolic sv } - | Loan lc, _ -> ( + { v1 with V.value = VSymbolic sv } + | VLoan lc, _ -> ( match lc with - | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids)) - | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id))) - | _, Loan lc -> ( + | VSharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids)) + | VMutLoan id -> raise (ValueMatchFailure (LoanInLeft id))) + | _, VLoan lc -> ( match lc with - | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids)) - | MutLoan id -> raise (ValueMatchFailure (LoanInRight id))) - | Symbolic sv, _ -> M.match_symbolic_with_other true sv v1 - | _, Symbolic sv -> M.match_symbolic_with_other false sv v0 - | Bottom, _ -> M.match_bottom_with_other true v1 - | _, Bottom -> M.match_bottom_with_other false v0 + | VSharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids)) + | VMutLoan id -> raise (ValueMatchFailure (LoanInRight id))) + | VSymbolic sv, _ -> M.match_symbolic_with_other true sv v1 + | _, VSymbolic sv -> M.match_symbolic_with_other false sv v0 + | VBottom, _ -> M.match_bottom_with_other true v1 + | _, VBottom -> M.match_bottom_with_other false v0 | _ -> log#ldebug (lazy @@ -414,10 +414,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Check if there are loans: we request to end them *) let check_loans (left : bool) (fields : V.typed_value list) : unit = match InterpreterBorrowsCore.get_first_loan_in_values fields with - | Some (V.SharedLoan (ids, _)) -> + | Some (VSharedLoan (ids, _)) -> if left then raise (ValueMatchFailure (LoansInLeft ids)) else raise (ValueMatchFailure (LoansInRight ids)) - | Some (V.MutLoan id) -> + | Some (VMutLoan id) -> if left then raise (ValueMatchFailure (LoanInLeft id)) else raise (ValueMatchFailure (LoanInRight id)) | None -> () @@ -688,10 +688,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let value_is_left = not left in (match InterpreterBorrowsCore.get_first_loan_in_value v with | None -> () - | Some (SharedLoan (ids, _)) -> + | Some (VSharedLoan (ids, _)) -> if value_is_left then raise (ValueMatchFailure (LoansInLeft ids)) else raise (ValueMatchFailure (LoansInRight ids)) - | Some (MutLoan id) -> + | Some (VMutLoan id) -> if value_is_left then raise (ValueMatchFailure (LoanInLeft id)) else raise (ValueMatchFailure (LoanInRight id))); (* Return a fresh symbolic value *) @@ -711,10 +711,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct | Some (BorrowContent _) -> raise (Failure "Unreachable") | Some (LoanContent lc) -> ( match lc with - | V.SharedLoan (ids, _) -> + | VSharedLoan (ids, _) -> if value_is_left then raise (ValueMatchFailure (LoansInLeft ids)) else raise (ValueMatchFailure (LoansInRight ids)) - | V.MutLoan id -> + | VMutLoan id -> if value_is_left then raise (ValueMatchFailure (LoanInLeft id)) else raise (ValueMatchFailure (LoanInRight id))) | None -> @@ -1366,8 +1366,8 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) let open InterpreterBorrowsCore in let lookup_shared_loan lid ctx : V.typed_value = match snd (lookup_loan ek_all lid ctx) with - | Concrete (V.SharedLoan (_, v)) -> v - | Abstract (V.ASharedLoan (_, v, _)) -> v + | Concrete (VSharedLoan (_, v)) -> v + | Abstract (ASharedLoan (_, v, _)) -> v | _ -> raise (Failure "Unreachable") in let lookup_in_src id = lookup_shared_loan id src_ctx in diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 36af1db4..9158f2c1 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -95,13 +95,13 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) Ok (ctx, { read = v; updated = nv }) | pe :: p' -> ( (* Match on the projection element and the value *) - match (pe, v.V.value, v.V.ty) with + match (pe, v.value, v.ty) with | ( Field ((ProjAdt (_, _) as proj_kind), field_id), - V.VAdt adt, - T.TAdt (type_id, _) ) -> ( + VAdt adt, + TAdt (type_id, _) ) -> ( (* Check consistency *) (match (proj_kind, type_id) with - | ProjAdt (def_id, opt_variant_id), T.TAdtId def_id' -> + | ProjAdt (def_id, opt_variant_id), TAdtId def_id' -> assert (def_id = def_id'); assert (opt_variant_id = adt.variant_id) | _ -> raise (Failure "Unreachable")); @@ -114,11 +114,11 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) let nvalues = T.FieldId.update_nth adt.field_values field_id res.updated in - let nadt = V.VAdt { adt with V.field_values = nvalues } in + let nadt = V.VAdt { adt with field_values = nvalues } in let updated = { v with value = nadt } in Ok (ctx, { res with updated })) (* Tuples *) - | Field (ProjTuple arity, field_id), V.VAdt adt, T.TAdt (T.TTuple, _) -> ( + | Field (ProjTuple arity, field_id), VAdt adt, TAdt (TTuple, _) -> ( assert (arity = List.length adt.field_values); let fv = T.FieldId.nth adt.field_values field_id in (* Project *) @@ -134,16 +134,16 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) Ok (ctx, { res with updated }) (* If we reach Bottom, it may mean we need to expand an uninitialized * enumeration value *)) - | Field ((ProjAdt (_, _) | ProjTuple _), _), V.Bottom, _ -> + | Field ((ProjAdt (_, _) | ProjTuple _), _), VBottom, _ -> Error (FailBottom (1 + List.length p', pe, v.ty)) (* Symbolic value: needs to be expanded *) - | _, Symbolic sp, _ -> + | _, VSymbolic sp, _ -> (* Expand the symbolic value *) Error (FailSymbolic (1 + List.length p', sp)) (* Box dereferencement *) | ( DerefBox, VAdt { variant_id = None; field_values = [ bv ] }, - T.TAdt (T.TAssumed T.TBox, _) ) -> ( + TAdt (TAssumed TBox, _) ) -> ( (* We allow moving outside of boxes. In practice, this kind of * manipulations should happen only inside unsafe code, so * it shouldn't happen due to user code, and we leverage it @@ -156,20 +156,20 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) { v with value = - V.VAdt { variant_id = None; field_values = [ res.updated ] }; + VAdt { variant_id = None; field_values = [ res.updated ] }; } in Ok (ctx, { res with updated = nv })) (* Borrows *) - | Deref, V.Borrow bc, _ -> ( + | Deref, VBorrow bc, _ -> ( match bc with - | V.SharedBorrow bid -> + | VSharedBorrow bid -> (* Lookup the loan content, and explore from there *) if access.lookup_shared_borrows then match lookup_loan ek bid ctx with - | _, Concrete (V.MutLoan _) -> + | _, Concrete (VMutLoan _) -> raise (Failure "Expected a shared loan") - | _, Concrete (V.SharedLoan (bids, sv)) -> ( + | _, Concrete (VSharedLoan (bids, sv)) -> ( (* Explore the shared value *) match access_projection access ctx update p' sv with | Error err -> Error err @@ -178,23 +178,23 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) by {!access_projection} *) let ctx = update_loan ek bid - (V.SharedLoan (bids, res.updated)) + (VSharedLoan (bids, res.updated)) ctx in (* Return - note that we don't need to update the borrow itself *) Ok (ctx, { res with updated = v })) | ( _, Abstract - ( V.AMutLoan (_, _) - | V.AEndedMutLoan + ( AMutLoan (_, _) + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AEndedSharedLoan (_, _) - | V.AIgnoredMutLoan (_, _) - | V.AEndedIgnoredMutLoan + | AEndedSharedLoan (_, _) + | AIgnoredMutLoan (_, _) + | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AIgnoredSharedLoan _ ) ) -> + | AIgnoredSharedLoan _ ) ) -> raise (Failure "Expected a shared (abstraction) loan") - | _, Abstract (V.ASharedLoan (bids, sv, _av)) -> ( + | _, Abstract (ASharedLoan (bids, sv, _av)) -> ( (* Explore the shared value *) match access_projection access ctx update p' sv with | Error err -> Error err @@ -202,37 +202,34 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) (* Relookup the child avalue *) let av = match lookup_loan ek bid ctx with - | _, Abstract (V.ASharedLoan (_, _, av)) -> av + | _, Abstract (ASharedLoan (_, _, av)) -> av | _ -> raise (Failure "Unexpected") in (* Update the shared loan with the new value returned by {!access_projection} *) let ctx = update_aloan ek bid - (V.ASharedLoan (bids, res.updated, av)) + (ASharedLoan (bids, res.updated, av)) ctx in (* Return - note that we don't need to update the borrow itself *) Ok (ctx, { res with updated = v })) else Error (FailBorrow bc) - | V.ReservedMutBorrow bid -> Error (FailReservedMutBorrow bid) - | V.MutBorrow (bid, bv) -> + | VReservedMutBorrow bid -> Error (FailReservedMutBorrow bid) + | VMutBorrow (bid, bv) -> if access.enter_mut_borrows then match access_projection access ctx update p' bv with | Error err -> Error err | Ok (ctx, res) -> let nv = - { - v with - value = V.Borrow (V.MutBorrow (bid, res.updated)); - } + { v with value = VBorrow (VMutBorrow (bid, res.updated)) } in Ok (ctx, { res with updated = nv }) else Error (FailBorrow bc)) - | _, V.Loan lc, _ -> ( + | _, VLoan lc, _ -> ( match lc with - | V.MutLoan bid -> Error (FailMutLoan bid) - | V.SharedLoan (bids, sv) -> + | VMutLoan bid -> Error (FailMutLoan bid) + | VSharedLoan (bids, sv) -> (* If we can enter shared loan, we ignore the loan. Pay attention to the fact that we need to reexplore the *whole* place (i.e, we mustn't ignore the current projection element *) @@ -241,14 +238,11 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) | Error err -> Error err | Ok (ctx, res) -> let nv = - { - v with - value = V.Loan (V.SharedLoan (bids, res.updated)); - } + { v with value = VLoan (VSharedLoan (bids, res.updated)) } in Ok (ctx, { res with updated = nv }) else Error (FailSharedLoan bids)) - | (_, (V.VLiteral _ | V.VAdt _ | V.Bottom | V.Borrow _), _) as r -> + | (_, (VLiteral _ | VAdt _ | VBottom | VBorrow _), _) as r -> let pe, v, ty = r in let pe = "- pe: " ^ E.show_projection_elem pe in let v = "- v:\n" ^ V.show_value v in @@ -531,24 +525,24 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) method! visit_borrow_content env bc = match bc with - | V.SharedBorrow _ | V.MutBorrow (_, _) -> + | VSharedBorrow _ | VMutBorrow (_, _) -> (* Nothing special to do *) super#visit_borrow_content env bc - | V.ReservedMutBorrow bid -> + | VReservedMutBorrow bid -> (* We need to activate reserved borrows *) let cc = promote_reserved_mut_borrow config bid in raise (UpdateCtx cc) method! visit_loan_content env lc = match lc with - | V.SharedLoan (bids, v) -> ( + | VSharedLoan (bids, v) -> ( (* End the loans if we need a modification access, otherwise dive into the shared value *) match access with - | Read -> super#visit_SharedLoan env bids v + | Read -> super#visit_VSharedLoan env bids v | Write | Move -> let cc = end_borrows config bids in raise (UpdateCtx cc)) - | V.MutLoan bid -> + | VMutLoan bid -> (* We always need to end mutable borrows *) let cc = end_borrow config bid in raise (UpdateCtx cc) @@ -596,8 +590,8 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun = (* There are: end them then retry *) let cc = match c with - | LoanContent (V.SharedLoan (bids, _)) -> end_borrows config bids - | LoanContent (V.MutLoan bid) -> end_borrow config bid + | LoanContent (VSharedLoan (bids, _)) -> end_borrows config bids + | LoanContent (VMutLoan bid) -> end_borrow config bid | BorrowContent _ -> raise (Failure "Unreachable") in (* Retry *) diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index e47886ec..8a4b0b4c 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -20,20 +20,20 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) (* Sanity check - TODO: move those elsewhere (here we perform the check at every * recursive call which is a bit overkill...) *) let ety = Subst.erase_regions ty in - assert (ty_is_rty ty && ety = v.V.ty); + assert (ty_is_rty ty && ety = v.ty); (* Project - if there are no regions from the abstraction in the type, return [_] *) if not (ty_has_regions_in_set regions ty) then [] else - match (v.V.value, ty) with - | V.VLiteral _, T.TLiteral _ -> [] - | V.VAdt adt, T.TAdt (id, generics) -> + match (v.value, ty) with + | VLiteral _, TLiteral _ -> [] + | VAdt adt, TAdt (id, generics) -> (* Retrieve the types of the fields *) let field_types = Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics in (* Project over the field values *) - let fields_types = List.combine adt.V.field_values field_types in + let fields_types = List.combine adt.field_values field_types in let proj_fields = List.map (fun (fv, fty) -> @@ -42,33 +42,33 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) fields_types in List.concat proj_fields - | V.Bottom, _ -> raise (Failure "Unreachable") - | V.Borrow bc, TRef (r, ref_ty, kind) -> + | VBottom, _ -> raise (Failure "Unreachable") + | VBorrow bc, TRef (r, ref_ty, kind) -> (* Retrieve the bid of the borrow and the asb of the projected borrowed value *) let bid, asb = (* Not in the set: dive *) match (bc, kind) with - | V.MutBorrow (bid, bv), T.Mut -> + | VMutBorrow (bid, bv), Mut -> (* Apply the projection on the borrowed value *) let asb = apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions bv ref_ty in (bid, asb) - | V.SharedBorrow bid, T.Shared -> + | VSharedBorrow bid, Shared -> (* Lookup the shared value *) let ek = ek_all in let sv = lookup_loan ek bid ctx in let asb = match sv with - | _, Concrete (V.SharedLoan (_, sv)) - | _, Abstract (V.ASharedLoan (_, sv, _)) -> + | _, Concrete (VSharedLoan (_, sv)) + | _, Abstract (ASharedLoan (_, sv, _)) -> apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions sv ref_ty | _ -> raise (Failure "Unexpected") in (bid, asb) - | V.ReservedMutBorrow _, _ -> + | VReservedMutBorrow _, _ -> raise (Failure "Can't apply a proj_borrow over a reserved mutable borrow") @@ -83,8 +83,8 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) else asb in asb - | V.Loan _, _ -> raise (Failure "Unreachable") - | V.Symbolic s, _ -> + | VLoan _, _ -> raise (Failure "Unreachable") + | VSymbolic s, _ -> (* Check that the projection doesn't contain ended regions *) assert ( not (projections_intersect s.V.sv_ty ctx.ended_regions ty regions)); @@ -103,15 +103,15 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) if not (ty_has_regions_in_set regions ty) then { V.value = V.AIgnored; ty } else let value : V.avalue = - match (v.V.value, ty) with - | V.VLiteral _, T.TLiteral _ -> V.AIgnored - | V.VAdt adt, T.TAdt (id, generics) -> + match (v.value, ty) with + | VLiteral _, T.TLiteral _ -> V.AIgnored + | VAdt adt, T.TAdt (id, generics) -> (* Retrieve the types of the fields *) let field_types = Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics in (* Project over the field values *) - let fields_types = List.combine adt.V.field_values field_types in + let fields_types = List.combine adt.field_values field_types in let proj_fields = List.map (fun (fv, fty) -> @@ -119,9 +119,9 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) regions ancestors_regions fv fty) fields_types in - V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields } - | V.Bottom, _ -> raise (Failure "Unreachable") - | V.Borrow bc, TRef (r, ref_ty, kind) -> + V.AAdt { variant_id = adt.variant_id; field_values = proj_fields } + | VBottom, _ -> raise (Failure "Unreachable") + | VBorrow bc, TRef (r, ref_ty, kind) -> if (* Check if the region is in the set of projected regions (note that * we never project over static regions) *) @@ -130,14 +130,14 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) (* In the set *) let bc = match (bc, kind) with - | V.MutBorrow (bid, bv), T.Mut -> + | VMutBorrow (bid, bv), T.Mut -> (* 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 (bid, bv) - | V.SharedBorrow bid, T.Shared -> + | VSharedBorrow bid, T.Shared -> (* Rem.: we don't need to also apply the projection on the borrowed value, because for as long as the abstraction lives then the shared borrow lives, which means that the @@ -150,7 +150,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) other branch of the [if then else]). *) V.ASharedBorrow bid - | V.ReservedMutBorrow _, _ -> + | VReservedMutBorrow _, _ -> raise (Failure "Can't apply a proj_borrow over a reserved mutable \ @@ -164,7 +164,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) the region set) *) let bc = match (bc, kind) with - | V.MutBorrow (bid, bv), T.Mut -> + | VMutBorrow (bid, bv), T.Mut -> (* Apply the projection on the borrowed value *) let bv = apply_proj_borrows check_symbolic_no_ended ctx @@ -177,20 +177,20 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) in (* Return *) V.AIgnoredMutBorrow (opt_bid, bv) - | V.SharedBorrow bid, T.Shared -> + | VSharedBorrow bid, T.Shared -> (* Lookup the shared value *) let ek = ek_all in let sv = lookup_loan ek bid ctx in let asb = match sv with - | _, Concrete (V.SharedLoan (_, sv)) - | _, Abstract (V.ASharedLoan (_, sv, _)) -> + | _, Concrete (VSharedLoan (_, sv)) + | _, Abstract (ASharedLoan (_, sv, _)) -> apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions sv ref_ty | _ -> raise (Failure "Unexpected") in V.AProjSharedBorrow asb - | V.ReservedMutBorrow _, _ -> + | VReservedMutBorrow _, _ -> raise (Failure "Can't apply a proj_borrow over a reserved mutable \ @@ -198,12 +198,12 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) | _ -> raise (Failure "Unreachable") in V.ABorrow bc - | V.Loan _, _ -> raise (Failure "Unreachable") - | V.Symbolic s, _ -> + | VLoan _, _ -> raise (Failure "Unreachable") + | VSymbolic s, _ -> (* Check that the projection doesn't contain already ended regions, * if necessary *) if check_symbolic_no_ended then ( - let ty1 = s.V.sv_ty in + let ty1 = s.sv_ty in let rset1 = ctx.ended_regions in let ty2 = ty in let rset2 = regions in @@ -216,7 +216,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) ^ T.RegionId.Set.to_string None rset2 ^ "\n")); assert (not (projections_intersect ty1 rset1 ty2 rset2))); - V.ASymbolic (V.AProjBorrows (s, ty)) + V.ASymbolic (AProjBorrows (s, ty)) | _ -> log#lerror (lazy @@ -225,7 +225,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) ^ "\n- proj rty: " ^ PA.ty_to_string ctx ty)); raise (Failure "Unreachable") in - { V.value; V.ty } + { value; ty } let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value) (see : V.symbolic_expansion) : V.typed_value = @@ -249,7 +249,7 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value) | SeMutRef (bid, bv) -> let ty = Subst.erase_regions sv.V.sv_ty in let bv = mk_typed_value_from_symbolic_value bv in - let value = V.Borrow (V.MutBorrow (bid, bv)) in + let value = V.VBorrow (VMutBorrow (bid, bv)) in { V.value; ty } | SeSharedRef (_, _) -> raise (Failure "Unexpected symbolic shared reference expansion") @@ -346,11 +346,11 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) (* Check if a value is a mutable borrow, and return its identifier if it is the case *) let get_borrow_in_mut_borrow (v : V.typed_value) : V.BorrowId.id option = - match v.V.value with - | V.Borrow lc -> ( + match v.value with + | VBorrow lc -> ( match lc with - | V.SharedBorrow _ | V.ReservedMutBorrow _ -> None - | V.MutBorrow (id, _) -> Some id) + | VSharedBorrow _ | VReservedMutBorrow _ -> None + | VMutBorrow (id, _) -> Some id) | _ -> None in @@ -397,18 +397,18 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) (** We may need to reborrow mutable borrows. Note that this doesn't happen for aborrows *) method! visit_typed_value env v = - match v.V.value with - | V.Borrow (V.MutBorrow (bid, bv)) -> + match v.value with + | VBorrow (VMutBorrow (bid, bv)) -> let insert = get_reborrows_for_bid bid in - let nbc = super#visit_MutBorrow env bid bv in - let nbc = { v with V.value = V.Borrow nbc } in + let nbc = super#visit_VMutBorrow env bid bv in + let nbc = { v with value = VBorrow nbc } in if insert = [] then (* No reborrows: do nothing special *) nbc else (* There are reborrows: insert a shared loan *) let insert = borrows_to_set insert in - let value = V.Loan (V.SharedLoan (insert, nbc)) in - let ty = v.V.ty in + let value = V.VLoan (VSharedLoan (insert, nbc)) in + let ty = v.ty in { V.value; ty } | _ -> super#visit_typed_value env v @@ -416,7 +416,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) functions) on purpose: exhaustive matches are good for maintenance *) method! visit_loan_content env lc = match lc with - | V.SharedLoan (bids, sv) -> + | VSharedLoan (bids, sv) -> (* Insert the reborrows *) let bids = insert_reborrows bids in (* Check if the contained value is a mutable borrow, in which @@ -432,14 +432,14 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) | Some bid -> insert_reborrows_for_bid bids bid in (* Update and explore *) - super#visit_SharedLoan env bids sv - | V.MutLoan bid -> + super#visit_VSharedLoan env bids sv + | VMutLoan bid -> (* Nothing special to do *) - super#visit_MutLoan env bid + super#visit_VMutLoan env bid method! visit_aloan_content env lc = match lc with - | V.ASharedLoan (bids, sv, av) -> + | ASharedLoan (bids, sv, av) -> (* Insert the reborrows *) let bids = insert_reborrows bids in (* Similarly to the non-abstraction case: check if the shared @@ -452,12 +452,12 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) in (* Update and explore *) super#visit_ASharedLoan env bids sv av - | V.AIgnoredSharedLoan _ - | V.AMutLoan (_, _) - | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AEndedSharedLoan (_, _) - | V.AIgnoredMutLoan (_, _) - | V.AEndedIgnoredMutLoan + | AIgnoredSharedLoan _ + | AMutLoan (_, _) + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedSharedLoan (_, _) + | AIgnoredMutLoan (_, _) + | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } -> (* Nothing particular to do *) super#visit_aloan_content env lc diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index cf9b840b..cbc09c29 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -43,7 +43,7 @@ let drop_value (config : C.config) (p : E.place) : cm_fun = let dummy_id = C.fresh_dummy_var_id () in let ctx = C.ctx_push_dummy_var ctx dummy_id mv in (* Update the destination to ⊥ *) - let nv = { v with value = V.Bottom } in + let nv = { v with value = VBottom } in let ctx = write_place access p nv ctx in log#ldebug (lazy @@ -172,7 +172,7 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun = (* Evaluate the assertion *) let eval_assert cf (v : V.typed_value) : m_fun = fun ctx -> - assert (v.ty = T.TLiteral PV.TBool); + assert (v.ty = TLiteral TBool); (* We make a choice here: we could completely decouple the concrete and * symbolic executions here but choose not to. In the case where we * know the concrete value of the boolean we test, we use this value @@ -182,16 +182,16 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun = | VLiteral (VBool _) -> (* Delegate to the concrete evaluation function *) eval_assertion_concrete config assertion cf ctx - | Symbolic sv -> - assert (config.mode = C.SymbolicMode); - assert (sv.V.sv_ty = T.TLiteral PV.TBool); + | VSymbolic sv -> + assert (config.mode = SymbolicMode); + assert (sv.sv_ty = TLiteral TBool); (* We continue the execution as if the test had succeeded, and thus * perform the symbolic expansion: sv ~~> true. * We will of course synthesize an assertion in the generated code * (see below). *) let ctx = - apply_symbolic_expansion_non_borrow config sv - (V.SeLiteral (PV.VBool true)) ctx + apply_symbolic_expansion_non_borrow config sv (SeLiteral (VBool true)) + ctx in (* Continue *) let expr = cf Unit ctx in @@ -231,8 +231,8 @@ let set_discriminant (config : C.config) (p : E.place) (* Update the value *) let update_value cf (v : V.typed_value) : m_fun = fun ctx -> - match (v.V.ty, v.V.value) with - | T.TAdt ((T.TAdtId _ as type_id), generics), V.VAdt av -> ( + match (v.ty, v.value) with + | TAdt ((TAdtId _ as type_id), generics), VAdt av -> ( (* There are two situations: - either the discriminant is already the proper one (in which case we don't do anything) @@ -248,22 +248,22 @@ let set_discriminant (config : C.config) (p : E.place) (* Replace the value *) let bottom_v = match type_id with - | T.TAdtId def_id -> + | TAdtId def_id -> compute_expanded_bottom_adt_value ctx def_id (Some variant_id) generics | _ -> raise (Failure "Unreachable") in assign_to_place config bottom_v p (cf Unit) ctx) - | T.TAdt ((T.TAdtId _ as type_id), generics), V.Bottom -> + | TAdt ((TAdtId _ as type_id), generics), VBottom -> let bottom_v = match type_id with - | T.TAdtId def_id -> + | TAdtId def_id -> compute_expanded_bottom_adt_value ctx def_id (Some variant_id) generics | _ -> raise (Failure "Unreachable") in assign_to_place config bottom_v p (cf Unit) ctx - | _, V.Symbolic _ -> + | _, VSymbolic _ -> assert (config.mode = SymbolicMode); (* This is a bit annoying: in theory we should expand the symbolic value * then set the discriminant, because in the case the discriminant is @@ -273,8 +273,8 @@ let set_discriminant (config : C.config) (p : E.place) * setting a discriminant should only be used to initialize a value, * or reset an already initialized value, really. *) raise (Failure "Unexpected value") - | _, (V.VAdt _ | V.Bottom) -> raise (Failure "Inconsistent state") - | _, (V.VLiteral _ | V.Borrow _ | V.Loan _) -> + | _, (VAdt _ | VBottom) -> raise (Failure "Inconsistent state") + | _, (VLiteral _ | VBorrow _ | VLoan _) -> raise (Failure "Unexpected value") in (* Compose and apply *) @@ -817,7 +817,7 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun = in (* Compose the continuations *) cf_branch cf ctx - | V.Symbolic sv -> + | VSymbolic sv -> (* Expand the symbolic boolean, and continue by evaluating * the branches *) let cf_true : st_cm_fun = eval_statement config st1 in @@ -848,7 +848,7 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun = in (* Compose *) cf_eval_branch cf ctx - | V.Symbolic sv -> + | VSymbolic sv -> (* Expand the symbolic value and continue by evaluating the * proper branches *) let stgts = @@ -891,14 +891,14 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun = let p_v = value_strip_shared_loans p_v in (* Match *) match p_v.value with - | V.VAdt adt -> ( + | VAdt adt -> ( (* Evaluate the discriminant *) let dv = Option.get adt.variant_id in (* Find the branch, evaluate and continue *) match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with | None -> eval_statement config otherwise cf ctx | Some (_, tgt) -> eval_statement config tgt cf ctx) - | V.Symbolic sv -> + | VSymbolic sv -> (* Expand the symbolic value - may lead to branching *) let cf_expand = expand_symbolic_adt config sv (Some (S.mk_mplace p ctx)) diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 6f62b577..60747b2a 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -90,7 +90,7 @@ let mk_fresh_symbolic_typed_value (sv_kind : V.sv_kind) (rty : T.ty) : let ty = Subst.erase_regions rty in (* Generate the fresh a symbolic value *) let value = mk_fresh_symbolic_value sv_kind rty in - let value = V.Symbolic value in + let value = V.VSymbolic value in { V.value; V.ty } let mk_fresh_symbolic_typed_value_from_no_regions_ty (sv_kind : V.sv_kind) @@ -101,7 +101,7 @@ let mk_fresh_symbolic_typed_value_from_no_regions_ty (sv_kind : V.sv_kind) (** Create a typed value from a symbolic value. *) let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) : V.typed_value = - let av = V.Symbolic svalue in + let av = V.VSymbolic svalue in let av : V.typed_value = { V.value = av; V.ty = Subst.erase_regions svalue.V.sv_ty } in @@ -204,7 +204,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) : object inherit [_] C.iter_eval_ctx as super - method! visit_Symbolic _ sv = + method! visit_VSymbolic _ sv = if sv.V.sv_id = sv_id then raise Found else () method! visit_aproj env aproj = @@ -251,7 +251,7 @@ let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) : let obj = object inherit [_] V.iter_typed_value - method! visit_Bottom _ = raise Found + method! visit_VBottom _ = raise Found method! visit_symbolic_value _ s = if symbolic_value_has_ended_regions ended_regions s then raise Found diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 8895bd8e..7830099f 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -150,8 +150,8 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = (* Register the loan *) let _ = match lc with - | V.SharedLoan (bids, _) -> register_shared_loan inside_abs bids - | V.MutLoan bid -> register_mut_loan inside_abs bid + | VSharedLoan (bids, _) -> register_shared_loan inside_abs bids + | VMutLoan bid -> register_mut_loan inside_abs bid in (* Continue exploring *) super#visit_loan_content inside_abs lc @@ -159,14 +159,14 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = method! visit_aloan_content inside_abs lc = let _ = match lc with - | V.AMutLoan (bid, _) -> register_mut_loan inside_abs bid - | V.ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids - | V.AIgnoredMutLoan (Some bid, _) -> register_ignored_loan T.Mut bid - | V.AIgnoredMutLoan (None, _) - | V.AIgnoredSharedLoan _ - | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AEndedSharedLoan (_, _) - | V.AEndedIgnoredMutLoan + | AMutLoan (bid, _) -> register_mut_loan inside_abs bid + | ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids + | AIgnoredMutLoan (Some bid, _) -> register_ignored_loan T.Mut bid + | AIgnoredMutLoan (None, _) + | AIgnoredSharedLoan _ + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedSharedLoan (_, _) + | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } -> (* Do nothing *) () @@ -244,9 +244,9 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = (* Register the loan *) let _ = match bc with - | V.SharedBorrow bid -> register_borrow Shared bid - | V.MutBorrow (bid, _) -> register_borrow Mut bid - | V.ReservedMutBorrow bid -> register_borrow Reserved bid + | VSharedBorrow bid -> register_borrow Shared bid + | VMutBorrow (bid, _) -> register_borrow Mut bid + | VReservedMutBorrow bid -> register_borrow Reserved bid in (* Continue exploring *) super#visit_borrow_content env bc @@ -254,12 +254,12 @@ 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.ASharedBorrow bid -> register_borrow Shared bid - | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid - | V.AIgnoredMutBorrow (None, _) - | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow _ - | V.AEndedSharedBorrow | V.AProjSharedBorrow _ -> + | AMutBorrow (bid, _) -> register_borrow Mut bid + | ASharedBorrow bid -> register_borrow Shared bid + | AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid + | AIgnoredMutBorrow (None, _) + | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow + | AProjSharedBorrow _ -> (* Do nothing *) () in @@ -305,7 +305,7 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = object inherit [_] C.iter_eval_ctx as super - method! visit_Bottom info = + method! visit_VBottom info = (* No ⊥ inside borrowed values *) assert (Config.allow_bottom_below_borrow || not info.outer_borrow) @@ -317,8 +317,8 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = (* Update the info *) let info = match lc with - | V.SharedLoan (_, _) -> set_outer_shared info - | V.MutLoan _ -> + | VSharedLoan (_, _) -> set_outer_shared info + | VMutLoan _ -> (* No mutable loan inside a shared loan *) assert (not info.outer_shared); set_outer_mut info @@ -330,11 +330,11 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = (* Update the info *) let info = match bc with - | V.SharedBorrow _ -> set_outer_shared info - | V.ReservedMutBorrow _ -> + | VSharedBorrow _ -> set_outer_shared info + | VReservedMutBorrow _ -> assert (not info.outer_borrow); set_outer_shared info - | V.MutBorrow (_, _) -> set_outer_mut info + | VMutBorrow (_, _) -> set_outer_mut info in (* Continue exploring *) super#visit_borrow_content info bc @@ -343,17 +343,16 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = (* Update the info *) let info = match lc with - | V.AMutLoan (_, _) -> set_outer_mut info - | V.ASharedLoan (_, _, _) -> set_outer_shared info - | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } - -> + | AMutLoan (_, _) -> set_outer_mut info + | ASharedLoan (_, _, _) -> set_outer_shared info + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } -> set_outer_mut info - | V.AEndedSharedLoan (_, _) -> set_outer_shared info - | V.AIgnoredMutLoan (_, _) -> set_outer_mut info - | V.AEndedIgnoredMutLoan + | AEndedSharedLoan (_, _) -> set_outer_shared info + | AIgnoredMutLoan (_, _) -> set_outer_mut info + | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } -> set_outer_mut info - | V.AIgnoredSharedLoan _ -> set_outer_shared info + | AIgnoredSharedLoan _ -> set_outer_shared info in (* Continue exploring *) super#visit_aloan_content info lc @@ -362,12 +361,12 @@ 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.ASharedBorrow _ | V.AEndedSharedBorrow -> set_outer_shared info - | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _ - | V.AEndedIgnoredMutBorrow _ -> + | AMutBorrow (_, _) -> set_outer_mut info + | ASharedBorrow _ | AEndedSharedBorrow -> set_outer_shared info + | AIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _ + -> set_outer_mut info - | V.AProjSharedBorrow _ -> set_outer_shared info + | AProjSharedBorrow _ -> set_outer_shared info in (* Continue exploring *) super#visit_aborrow_content info bc @@ -416,10 +415,10 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (* Check that the types have erased regions *) assert (ty_is_ety tv.ty); (* Check the current pair (value, type) *) - (match (tv.V.value, tv.V.ty) with - | V.VLiteral cv, T.TLiteral ty -> check_literal_type cv ty + (match (tv.value, tv.ty) with + | VLiteral cv, TLiteral ty -> check_literal_type cv ty (* ADT case *) - | V.VAdt av, T.TAdt (T.TAdtId def_id, generics) -> + | VAdt av, TAdt (TAdtId def_id, generics) -> (* Retrieve the definition to check the variant id, the number of * parameters, etc. *) let def = C.ctx_lookup_type_decl ctx def_id in @@ -428,53 +427,51 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = List.length generics.regions = List.length def.generics.regions); assert (List.length generics.types = List.length def.generics.types); (* Check that the variant id is consistent *) - (match (av.V.variant_id, def.T.kind) with - | Some variant_id, T.Enum variants -> + (match (av.variant_id, def.kind) with + | Some variant_id, Enum variants -> assert (T.VariantId.to_int variant_id < List.length variants) - | None, T.Struct _ -> () + | None, Struct _ -> () | _ -> raise (Failure "Erroneous typing")); (* Check that the field types are correct *) let field_types = - Assoc.type_decl_get_inst_norm_field_etypes ctx def av.V.variant_id + Assoc.type_decl_get_inst_norm_field_etypes ctx def av.variant_id generics in - let fields_with_types = - List.combine av.V.field_values field_types - in + let fields_with_types = List.combine av.field_values field_types in List.iter - (fun ((v, ty) : V.typed_value * T.ty) -> assert (v.V.ty = ty)) + (fun ((v, ty) : V.typed_value * T.ty) -> assert (v.ty = ty)) fields_with_types (* Tuple case *) - | V.VAdt av, T.TAdt (T.TTuple, generics) -> + | VAdt av, TAdt (TTuple, generics) -> assert (generics.regions = []); assert (generics.const_generics = []); - assert (av.V.variant_id = None); + assert (av.variant_id = None); (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) let fields_with_types = - List.combine av.V.field_values generics.types + List.combine av.field_values generics.types in List.iter - (fun ((v, ty) : V.typed_value * T.ty) -> assert (v.V.ty = ty)) + (fun ((v, ty) : V.typed_value * T.ty) -> assert (v.ty = ty)) fields_with_types (* Assumed type case *) - | V.VAdt av, T.TAdt (T.TAssumed aty_id, generics) -> ( - assert (av.V.variant_id = None); + | VAdt av, TAdt (TAssumed aty_id, generics) -> ( + assert (av.variant_id = None); match ( aty_id, - av.V.field_values, + av.field_values, generics.regions, generics.types, generics.const_generics ) with (* Box *) - | T.TBox, [ inner_value ], [], [ inner_ty ], [] -> - assert (inner_value.V.ty = inner_ty) - | T.TArray, inner_values, _, [ inner_ty ], [ cg ] -> + | TBox, [ inner_value ], [], [ inner_ty ], [] -> + assert (inner_value.ty = inner_ty) + | TArray, inner_values, _, [ inner_ty ], [ cg ] -> (* *) assert ( List.for_all - (fun (v : V.typed_value) -> v.V.ty = inner_ty) + (fun (v : V.typed_value) -> v.ty = inner_ty) inner_values); (* The length is necessarily concrete *) let len = @@ -483,37 +480,37 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = .value in assert (Z.of_int (List.length inner_values) = len) - | (T.TSlice | T.TStr), _, _, _, _ -> raise (Failure "Unexpected") + | (TSlice | TStr), _, _, _, _ -> raise (Failure "Unexpected") | _ -> raise (Failure "Erroneous type")) - | V.Bottom, _ -> (* Nothing to check *) () - | V.Borrow bc, T.TRef (_, ref_ty, rkind) -> ( + | VBottom, _ -> (* Nothing to check *) () + | VBorrow bc, TRef (_, ref_ty, rkind) -> ( match (bc, rkind) with - | V.SharedBorrow bid, T.Shared | V.ReservedMutBorrow bid, T.Mut -> ( + | VSharedBorrow bid, Shared | VReservedMutBorrow bid, Mut -> ( (* Lookup the borrowed value to check it has the proper type *) let _, glc = lookup_loan ek_all bid ctx in match glc with - | Concrete (V.SharedLoan (_, sv)) - | Abstract (V.ASharedLoan (_, sv, _)) -> - assert (sv.V.ty = ref_ty) + | Concrete (VSharedLoan (_, sv)) + | Abstract (ASharedLoan (_, sv, _)) -> + assert (sv.ty = ref_ty) | _ -> raise (Failure "Inconsistent context")) - | V.MutBorrow (_, bv), T.Mut -> + | VMutBorrow (_, bv), Mut -> assert ( (* Check that the borrowed value has the proper type *) - bv.V.ty = ref_ty) + bv.ty = ref_ty) | _ -> raise (Failure "Erroneous typing")) - | V.Loan lc, ty -> ( + | VLoan lc, ty -> ( match lc with - | V.SharedLoan (_, sv) -> assert (sv.V.ty = ty) - | V.MutLoan bid -> ( + | VSharedLoan (_, sv) -> assert (sv.ty = ty) + | VMutLoan bid -> ( (* Lookup the borrowed value to check it has the proper type *) 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)) -> - assert (Subst.erase_regions sv.V.ty = ty) + | Concrete (VMutBorrow (_, bv)) -> assert (bv.ty = ty) + | Abstract (AMutBorrow (_, sv)) -> + assert (Subst.erase_regions sv.ty = ty) | _ -> raise (Failure "Inconsistent context"))) - | V.Symbolic sv, ty -> - let ty' = Subst.erase_regions sv.V.sv_ty in + | VSymbolic sv, ty -> + let ty' = Subst.erase_regions sv.sv_ty in assert (ty' = ty) | _ -> raise (Failure "Erroneous typing")); (* Continue exploring to inspect the subterms *) @@ -531,9 +528,9 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (* Check that the types have regions *) assert (ty_is_rty atv.ty); (* Check the current pair (value, type) *) - (match (atv.V.value, atv.V.ty) with + (match (atv.value, atv.ty) with (* ADT case *) - | V.AAdt av, T.TAdt (T.TAdtId def_id, generics) -> + | AAdt av, TAdt (TAdtId def_id, generics) -> (* Retrieve the definition to check the variant id, the number of * parameters, etc. *) let def = C.ctx_lookup_type_decl ctx def_id in @@ -545,132 +542,126 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = List.length generics.const_generics = List.length def.generics.const_generics); (* Check that the variant id is consistent *) - (match (av.V.variant_id, def.T.kind) with - | Some variant_id, T.Enum variants -> + (match (av.variant_id, def.kind) with + | Some variant_id, Enum variants -> assert (T.VariantId.to_int variant_id < List.length variants) - | None, T.Struct _ -> () + | None, Struct _ -> () | _ -> raise (Failure "Erroneous typing")); (* Check that the field types are correct *) let field_types = - Assoc.type_decl_get_inst_norm_field_rtypes ctx def av.V.variant_id + Assoc.type_decl_get_inst_norm_field_rtypes ctx def av.variant_id generics in - let fields_with_types = - List.combine av.V.field_values field_types - in + let fields_with_types = List.combine av.field_values field_types in List.iter - (fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.V.ty = ty)) + (fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.ty = ty)) fields_with_types (* Tuple case *) - | V.AAdt av, T.TAdt (T.TTuple, generics) -> + | AAdt av, TAdt (TTuple, generics) -> assert (generics.regions = []); assert (generics.const_generics = []); - assert (av.V.variant_id = None); + assert (av.variant_id = None); (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) let fields_with_types = - List.combine av.V.field_values generics.types + List.combine av.field_values generics.types in List.iter - (fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.V.ty = ty)) + (fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.ty = ty)) fields_with_types (* Assumed type case *) - | V.AAdt av, T.TAdt (T.TAssumed aty_id, generics) -> ( - assert (av.V.variant_id = None); + | AAdt av, TAdt (TAssumed aty_id, generics) -> ( + assert (av.variant_id = None); match ( aty_id, - av.V.field_values, + av.field_values, generics.regions, generics.types, generics.const_generics ) with (* Box *) - | T.TBox, [ boxed_value ], [], [ boxed_ty ], [] -> - assert (boxed_value.V.ty = boxed_ty) + | TBox, [ boxed_value ], [], [ boxed_ty ], [] -> + assert (boxed_value.ty = boxed_ty) | _ -> raise (Failure "Erroneous type")) - | V.ABottom, _ -> (* Nothing to check *) () - | V.ABorrow bc, T.TRef (_, ref_ty, rkind) -> ( + | ABottom, _ -> (* Nothing to check *) () + | ABorrow bc, TRef (_, ref_ty, rkind) -> ( match (bc, rkind) with - | V.AMutBorrow (_, av), T.Mut -> + | AMutBorrow (_, av), Mut -> (* Check that the child value has the proper type *) - assert (av.V.ty = ref_ty) - | V.ASharedBorrow bid, T.Shared -> ( + assert (av.ty = ref_ty) + | ASharedBorrow bid, Shared -> ( (* Lookup the borrowed value to check it has the proper type *) let _, glc = lookup_loan ek_all bid ctx in match glc with - | Concrete (V.SharedLoan (_, sv)) - | Abstract (V.ASharedLoan (_, sv, _)) -> - assert (sv.V.ty = Subst.erase_regions ref_ty) + | Concrete (VSharedLoan (_, sv)) + | Abstract (ASharedLoan (_, sv, _)) -> + assert (sv.ty = Subst.erase_regions ref_ty) | _ -> raise (Failure "Inconsistent context")) - | V.AIgnoredMutBorrow (_opt_bid, av), T.Mut -> - assert (av.V.ty = ref_ty) - | ( V.AEndedIgnoredMutBorrow - { given_back; child; given_back_meta = _ }, - T.Mut ) -> - assert (given_back.V.ty = ref_ty); - assert (child.V.ty = ref_ty) - | V.AProjSharedBorrow _, T.Shared -> () + | AIgnoredMutBorrow (_opt_bid, av), Mut -> assert (av.ty = ref_ty) + | ( AEndedIgnoredMutBorrow { given_back; child; given_back_meta = _ }, + Mut ) -> + assert (given_back.ty = ref_ty); + assert (child.ty = ref_ty) + | AProjSharedBorrow _, Shared -> () | _ -> raise (Failure "Inconsistent context")) - | V.ALoan lc, aty -> ( + | ALoan lc, aty -> ( match lc with - | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (Some bid, child_av) + | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av) -> ( let borrowed_aty = aloan_get_expected_child_type aty in - assert (child_av.V.ty = borrowed_aty); + assert (child_av.ty = borrowed_aty); (* Lookup the borrowed value to check it has the proper type *) let glc = lookup_borrow ek_all bid ctx in match glc with - | Concrete (V.MutBorrow (_, bv)) -> - assert (bv.V.ty = Subst.erase_regions borrowed_aty) - | Abstract (V.AMutBorrow (_, sv)) -> + | Concrete (VMutBorrow (_, bv)) -> + assert (bv.ty = Subst.erase_regions borrowed_aty) + | Abstract (AMutBorrow (_, sv)) -> assert ( - Subst.erase_regions sv.V.ty + Subst.erase_regions sv.ty = Subst.erase_regions borrowed_aty) | _ -> raise (Failure "Inconsistent context")) - | V.AIgnoredMutLoan (None, child_av) -> + | AIgnoredMutLoan (None, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in - assert (child_av.V.ty = borrowed_aty) - | V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av) - -> + assert (child_av.ty = borrowed_aty) + | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in - assert (sv.V.ty = Subst.erase_regions borrowed_aty); + assert (sv.ty = Subst.erase_regions borrowed_aty); (* TODO: the type of aloans doesn't make sense, see above *) - assert (child_av.V.ty = borrowed_aty) - | V.AEndedMutLoan { given_back; child; given_back_meta = _ } - | V.AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ } - -> + assert (child_av.ty = borrowed_aty) + | AEndedMutLoan { given_back; child; given_back_meta = _ } + | AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ } -> let borrowed_aty = aloan_get_expected_child_type aty in - assert (given_back.V.ty = borrowed_aty); - assert (child.V.ty = borrowed_aty) - | V.AIgnoredSharedLoan child_av -> - assert (child_av.V.ty = aloan_get_expected_child_type aty)) - | V.ASymbolic aproj, ty -> ( + assert (given_back.ty = borrowed_aty); + assert (child.ty = borrowed_aty) + | AIgnoredSharedLoan child_av -> + assert (child_av.ty = aloan_get_expected_child_type aty)) + | ASymbolic aproj, ty -> ( let ty1 = Subst.erase_regions ty in match aproj with - | V.AProjLoans (sv, _) -> - let ty2 = Subst.erase_regions sv.V.sv_ty in + | AProjLoans (sv, _) -> + let ty2 = Subst.erase_regions sv.sv_ty in assert (ty1 = ty2); (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in - assert (ty_has_regions_in_set abs.regions sv.V.sv_ty) - | V.AProjBorrows (sv, proj_ty) -> - let ty2 = Subst.erase_regions sv.V.sv_ty in + assert (ty_has_regions_in_set abs.regions sv.sv_ty) + | AProjBorrows (sv, proj_ty) -> + let ty2 = Subst.erase_regions sv.sv_ty in assert (ty1 = ty2); (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in assert (ty_has_regions_in_set abs.regions proj_ty) - | V.AEndedProjLoans (_msv, given_back_ls) -> + | AEndedProjLoans (_msv, given_back_ls) -> List.iter (fun (_, proj) -> match proj with | V.AProjBorrows (_sv, ty') -> assert (ty' = ty) - | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> () + | AEndedProjBorrows _ | AIgnoredProjBorrows -> () | _ -> raise (Failure "Unexpected")) given_back_ls - | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> ()) - | V.AIgnored, _ -> () + | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()) + | AIgnored, _ -> () | _ -> log#lerror (lazy @@ -757,7 +748,7 @@ let check_symbolic_values (ctx : C.eval_ctx) : unit = object inherit [_] C.iter_eval_ctx as super method! visit_abs _ abs = super#visit_abs (Some abs) abs - method! visit_Symbolic _ sv = add_env_sv sv + method! visit_VSymbolic _ sv = add_env_sv sv method! visit_abstract_shared_borrow abs asb = let abs = Option.get abs in diff --git a/compiler/Print.ml b/compiler/Print.ml index 7494dc2a..28e940ba 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -73,10 +73,10 @@ module Values = struct List.map (typed_value_to_string fmt) av.field_values in match v.ty with - | T.TAdt (T.TTuple, _) -> + | TAdt (TTuple, _) -> (* Tuple *) "(" ^ String.concat ", " field_values ^ ")" - | T.TAdt (T.TAdtId def_id, _) -> + | TAdt (TAdtId def_id, _) -> (* "Regular" ADT *) let adt_ident = match av.variant_id with @@ -98,7 +98,7 @@ module Values = struct let field_values = String.concat " " field_values in adt_ident ^ " { " ^ field_values ^ " }" else adt_ident - | T.TAdt (T.TAssumed aty, _) -> ( + | TAdt (TAssumed aty, _) -> ( (* Assumed type *) match (aty, field_values) with | TBox, [ bv ] -> "@Box(" ^ bv ^ ")" @@ -108,28 +108,29 @@ module Values = struct | _ -> raise (Failure ("Inconsistent value: " ^ V.show_typed_value v))) | _ -> raise (Failure "Inconsistent typed value")) - | Bottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty - | Borrow bc -> borrow_content_to_string fmt bc - | Loan lc -> loan_content_to_string fmt lc - | Symbolic s -> symbolic_value_to_string ty_fmt s + | VBottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty + | VBorrow bc -> borrow_content_to_string fmt bc + | VLoan lc -> loan_content_to_string fmt lc + | VSymbolic s -> symbolic_value_to_string ty_fmt s and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) : string = match bc with - | SharedBorrow bid -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋" - | MutBorrow (bid, tv) -> + | VSharedBorrow bid -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋" + | VMutBorrow (bid, tv) -> "&mut@" ^ V.BorrowId.to_string bid ^ " (" ^ typed_value_to_string fmt tv ^ ")" - | ReservedMutBorrow bid -> "⌊reserved_mut@" ^ V.BorrowId.to_string bid ^ "⌋" + | VReservedMutBorrow bid -> + "⌊reserved_mut@" ^ V.BorrowId.to_string bid ^ "⌋" and loan_content_to_string (fmt : value_formatter) (lc : V.loan_content) : string = match lc with - | SharedLoan (loans, v) -> + | VSharedLoan (loans, v) -> let loans = V.BorrowId.Set.to_string None loans in "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string fmt v ^ ")" - | MutLoan bid -> "⌊mut@" ^ V.BorrowId.to_string bid ^ "⌋" + | VMutLoan bid -> "⌊mut@" ^ V.BorrowId.to_string bid ^ "⌋" let abstract_shared_borrow_to_string (fmt : value_formatter) (abs : V.abstract_shared_borrow) : string = diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 60020d9a..258b1cf2 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1149,7 +1149,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) (* Translate the value *) let value = match v.value with - | V.VLiteral cv -> { e = Const cv; ty } + | VLiteral cv -> { e = Const cv; ty } | VAdt av -> ( let variant_id = av.variant_id in let field_values = List.map translate av.field_values in @@ -1173,27 +1173,27 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) let cons = { e = cons_e; ty = cons_ty } in (* Apply the constructor *) mk_apps cons field_values) - | Bottom -> raise (Failure "Unreachable") - | Loan lc -> ( + | VBottom -> raise (Failure "Unreachable") + | VLoan lc -> ( match lc with - | SharedLoan (_, v) -> translate v - | MutLoan _ -> raise (Failure "Unreachable")) - | Borrow bc -> ( + | VSharedLoan (_, v) -> translate v + | VMutLoan _ -> raise (Failure "Unreachable")) + | VBorrow bc -> ( match bc with - | V.SharedBorrow bid -> + | VSharedBorrow bid -> (* Lookup the shared value in the context, and continue *) let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in translate sv - | V.ReservedMutBorrow bid -> + | VReservedMutBorrow bid -> (* Same as for shared borrows. However, note that we use reserved borrows * only in *meta-data*: a value *actually used* in the translation can't come * from an unpromoted reserved borrow *) let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in translate sv - | V.MutBorrow (_, v) -> + | VMutBorrow (_, v) -> (* Borrows are the identity in the extraction *) translate v) - | Symbolic sv -> symbolic_value_to_texpression ctx sv + | VSymbolic sv -> symbolic_value_to_texpression ctx sv in (* Debugging *) log#ldebug diff --git a/compiler/Values.ml b/compiler/Values.ml index 8526ea66..932530ff 100644 --- a/compiler/Values.ml +++ b/compiler/Values.ml @@ -115,10 +115,10 @@ type symbolic_value = { and value = | VLiteral of literal (** Non-symbolic primitive value *) | VAdt of adt_value (** Enumerations and structures *) - | Bottom (** No value (uninitialized or moved value) *) - | Borrow of borrow_content (** A borrowed value *) - | Loan of loan_content (** A loaned value *) - | Symbolic of symbolic_value + | VBottom (** No value (uninitialized or moved value) *) + | VBorrow of borrow_content (** A borrowed value *) + | VLoan of loan_content (** A loaned value *) + | VSymbolic of symbolic_value (** Borrow projector over a symbolic value. Note that contrary to the abstraction-values case, symbolic values @@ -132,9 +132,9 @@ and adt_value = { } and borrow_content = - | SharedBorrow of borrow_id (** A shared borrow. *) - | MutBorrow of borrow_id * typed_value (** A mutably borrowed value. *) - | ReservedMutBorrow of borrow_id + | VSharedBorrow of borrow_id (** A shared borrow. *) + | VMutBorrow of borrow_id * typed_value (** A mutably borrowed value. *) + | VReservedMutBorrow of borrow_id (** A reserved mut borrow. This is used to model {{: https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html} two-phase borrows}. @@ -172,8 +172,8 @@ and borrow_content = *) and loan_content = - | SharedLoan of loan_id_set * typed_value - | MutLoan of loan_id + | VSharedLoan of loan_id_set * typed_value + | VMutLoan of loan_id (** "Regular" typed value (we map variables to typed values) *) and typed_value = { value : value; ty : ty } diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml index 24485002..7880fc3a 100644 --- a/compiler/ValuesUtils.ml +++ b/compiler/ValuesUtils.ml @@ -21,7 +21,7 @@ let mk_typed_avalue (ty : ty) (value : avalue) : typed_avalue = let mk_bottom (ty : ty) : typed_value = assert (ty_is_ety ty); - { value = Bottom; ty } + { value = VBottom; ty } let mk_abottom (ty : ty) : typed_avalue = assert (ty_is_rty ty); @@ -32,7 +32,7 @@ let mk_aignored (ty : ty) : typed_avalue = { value = AIgnored; ty } let value_as_symbolic (v : value) : symbolic_value = - match v with Symbolic v -> v | _ -> raise (Failure "Unexpected") + match v with VSymbolic v -> v | _ -> raise (Failure "Unexpected") (** Box a value *) let mk_box_value (v : typed_value) : typed_value = @@ -40,20 +40,20 @@ let mk_box_value (v : typed_value) : typed_value = let box_v = VAdt { variant_id = None; field_values = [ v ] } in mk_typed_value box_ty box_v -let is_bottom (v : value) : bool = match v with Bottom -> true | _ -> false +let is_bottom (v : value) : bool = match v with VBottom -> true | _ -> false let is_aignored (v : avalue) : bool = match v with AIgnored -> true | _ -> false let is_symbolic (v : value) : bool = - match v with Symbolic _ -> true | _ -> false + match v with VSymbolic _ -> true | _ -> false let as_symbolic (v : value) : symbolic_value = - match v with Symbolic s -> s | _ -> raise (Failure "Unexpected") + match v with VSymbolic s -> s | _ -> raise (Failure "Unexpected") let as_mut_borrow (v : typed_value) : BorrowId.id * typed_value = match v.value with - | Borrow (MutBorrow (bid, bv)) -> (bid, bv) + | VBorrow (VMutBorrow (bid, bv)) -> (bid, bv) | _ -> raise (Failure "Unexpected") let is_unit (v : typed_value) : bool = @@ -86,7 +86,7 @@ let reserved_in_value (v : typed_value) : bool = let obj = object inherit [_] iter_typed_value - method! visit_ReservedMutBorrow _env _ = raise Found + method! visit_VReservedMutBorrow _env _ = raise Found end in (* We use exceptions *) @@ -151,7 +151,7 @@ let find_first_primitively_copyable_sv_with_borrows (type_infos : TA.type_infos) object inherit [_] iter_typed_value - method! visit_Symbolic _ sv = + method! visit_VSymbolic _ sv = let ty = sv.sv_ty in if ty_is_primitively_copyable ty && ty_has_borrows type_infos ty then raise (FoundSymbolicValue sv) @@ -171,7 +171,7 @@ let find_first_primitively_copyable_sv_with_borrows (type_infos : TA.type_infos) *) let rec value_strip_shared_loans (v : typed_value) : typed_value = match v.value with - | Loan (SharedLoan (_, v')) -> value_strip_shared_loans v' + | VLoan (VSharedLoan (_, v')) -> value_strip_shared_loans v' | _ -> v (** Check if a symbolic value has borrows *) @@ -251,7 +251,7 @@ let value_remove_shared_loans (v : typed_value) : typed_value = method! visit_typed_value env v = match v.value with - | Loan (SharedLoan (_, sv)) -> self#visit_typed_value env sv + | VLoan (VSharedLoan (_, sv)) -> self#visit_typed_value env sv | _ -> super#visit_typed_value env v end in -- cgit v1.2.3