diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Values.ml | 56 |
1 files changed, 50 insertions, 6 deletions
diff --git a/src/Values.ml b/src/Values.ml index b6bb414b..bcb08dc8 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -195,6 +195,8 @@ class ['self] iter_typed_avalue_base = object (_self : 'self) inherit [_] iter_typed_value + method visit_id : 'env -> BorrowId.id -> unit = fun _ _ -> () + method visit_region : 'env -> region -> unit = fun _ _ -> () method visit_aproj : 'env -> aproj -> unit = fun _ _ -> () @@ -211,6 +213,8 @@ class ['self] map_typed_avalue_base = object (_self : 'self) inherit [_] map_typed_value + method visit_id : 'env -> BorrowId.id -> BorrowId.id = fun _ id -> id + method visit_region : 'env -> region -> region = fun _ r -> r method visit_aproj : 'env -> aproj -> aproj = fun _ p -> p @@ -421,11 +425,15 @@ and aborrow_content = > abs0 { a_shared_bororw l0 } ``` *) - | AIgnoredMutBorrow of typed_avalue + | AIgnoredMutBorrow of BorrowId.id option * typed_avalue (** An ignored mutable borrow. - - This is mostly useful for typing concerns: when a borrow doesn't - belong to an abstraction, it would be weird to ignore it altogether. + + We need to keep track of ignored mut borrows because when ending such + borrows, we need to project the loans of the given back value to + insert them in the proper abstractions. + + Note that we need to do so only for borrows consumed by parent + abstractions (hence the optional borrow id). Example: ======== @@ -441,9 +449,38 @@ and aborrow_content = > x -> mut_loan l0 > px -> mut_loan l1 > ppx -> ⊥ - > abs'a { a_mut_borrow l1 (a_ignored_mut_borrow (U32 0)) } // TODO: duplication - > abs'b { a_ignored_mut_borrow (a_mut_borrow l0 (U32 0)) } + > abs'a { a_mut_borrow l1 (a_ignored_mut_borrow None (U32 0)) } // TODO: duplication + > abs'b {parents={abs'a}} { a_ignored_mut_borrow (Some l1) (a_mut_borrow l0 (U32 0)) } + + ... // abs'a ends + + > x -> mut_loan l0 + > px -> @s0 + > ppx -> ⊥ + > abs'b { + > a_ended_ignored_mut_borrow (a_proj_loans (@s0 <: &'b mut u32)) // <-- loan projector + > (a_mut_borrow l0 (U32 0)) + > } + + ... // `@s0` gets expanded to `&mut l2 @s1` + + > x -> mut_loan l0 + > px -> &mut l2 @s1 + > ppx -> ⊥ + > abs'b { + > a_ended_ignored_mut_borrow (a_mut_loan l2) // <-- loan l2 is here + > (a_mut_borrow l0 (U32 0)) + > } + ``` + + Note that we could use AIgnoredMutLoan in the case the borrow id is not + None, which would allow us to simplify the rules (to not have rules + to specifically handle the case of AIgnoredMutBorrow with Some borrow + id) and also remove the AEndedIgnoredMutBorrow variant. + For now, the rules are implemented and it allows us to make the avalues + more precise and clearer, so we will keep it that way. + TODO: this is annoying, we are duplicating information. Maybe we could introduce an "Ignored" value? We have to pay attention to two things: @@ -460,6 +497,10 @@ and aborrow_content = abstraction so that we can properly call the backward functions when generating the pure translation. *) + | AEndedIgnoredMutBorrow of { + given_back_loans_proj : typed_avalue; + child : typed_avalue; + } (** See the explanations for [AIgnoredMutBorrow] *) | AProjSharedBorrow of abstract_shared_borrows (** A projected shared borrow. @@ -522,6 +563,9 @@ type abs = { abs_id : (AbstractionId.id[@opaque]); parents : (AbstractionId.set_t[@opaque]); (** The parent abstractions *) regions : (RegionId.set_t[@opaque]); (** Regions owned by this abstraction *) + ancestors_regions : (RegionId.set_t[@opaque]); + (** Union of the regions owned by this abstraction's ancestors (not + including the regions of this abstraction itself) *) avalues : typed_avalue list; (** The values in this abstraction *) } [@@deriving |