diff options
| -rw-r--r-- | src/Interpreter.ml | 3 | ||||
| -rw-r--r-- | src/Print.ml | 16 | ||||
| -rw-r--r-- | src/Values.ml | 35 |
3 files changed, 30 insertions, 24 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 708b1632..2a9db410 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -673,9 +673,8 @@ let rec apply_proj_borrows (regions : T.RegionId.set_t) (v : V.typed_value) let bv = apply_proj_borrows regions bv ref_ty in V.AIgnoredMutBorrow bv | V.SharedBorrow bid, T.Shared -> - (* TODO *) + (* TODO: we need the context to lookup the value *) raise Unimplemented - (* V.AIgnoredSharedBorrow bid*) | V.InactivatedMutBorrow _, _ -> failwith "Can't apply a proj_borrow over an inactivated mutable borrow" diff --git a/src/Print.ml b/src/Print.ml index bf07e57e..6b4c3c4f 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -297,16 +297,18 @@ module Values = struct "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string fmt v ^ ")" | MutLoan bid -> "⌊mut@" ^ V.BorrowId.to_string bid ^ "⌋" - let rec abstract_shared_borrows_to_string (fmt : value_formatter) - (abs : V.abstract_shared_borrows) : string = + let rec abstract_shared_borrow_to_string (fmt : value_formatter) + (abs : V.abstract_shared_borrow) : string = match abs with - | AsbSet bs -> V.BorrowId.set_to_string bs + | AsbBorrow bid -> V.BorrowId.to_string bid | AsbProjReborrows (sv, rty) -> "{" ^ symbolic_value_proj_to_string fmt sv rty ^ "}" - | AsbUnion (asb1, asb2) -> - abstract_shared_borrows_to_string fmt asb1 - ^ " U " - ^ abstract_shared_borrows_to_string fmt asb2 + + let rec abstract_shared_borrows_to_string (fmt : value_formatter) + (abs : V.abstract_shared_borrows) : string = + "{" + ^ String.concat "," (List.map (abstract_shared_borrow_to_string fmt) abs) + ^ "}" let aproj_to_string (fmt : value_formatter) (pv : V.aproj) : string = match pv with diff --git a/src/Values.ml b/src/Values.ml index 96feb814..1a61f296 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -149,13 +149,25 @@ and typed_value = { value : value; ty : ety } }] (** "Regular" typed value (we map variables to typed values) *) -type abstract_shared_borrows = - | AsbSet of BorrowId.set_t - | AsbProjReborrows of symbolic_value * rty - | AsbUnion of abstract_shared_borrows * abstract_shared_borrows - (** TODO: explanations *) +(** When giving shared borrows to functions (i.e., inserting shared borrows inside + abstractions) we need to reborrow the shared values. When doing so, we lookup + the shared values and apply some special projections to the shared value + (until we can't go further, i.e., we find symbolic values which may get + expanded upon reading them later), which don't generate avalues but + sets of borrow ids and symbolic values. + + Note that as shared values can't get modified it is ok to forget the + structure of the values we projected, and only keep the set of borrows + (and symbolic values). +*) +type abstract_shared_borrow = + | AsbBorrow of (BorrowId.id[@opaque]) + | AsbProjReborrows of (symbolic_value[@opaque]) * (rty[@opaque]) [@@deriving show] +type abstract_shared_borrows = abstract_shared_borrow list +(** A set of abstract shared borrows *) + type aproj = | AProjLoans of symbolic_value | AProjBorrows of symbolic_value * rty @@ -172,10 +184,6 @@ class ['self] iter_typed_avalue_base = method visit_aproj : 'env -> aproj -> unit = fun _ _ -> () - method visit_abstract_shared_borrows - : 'env -> abstract_shared_borrows -> unit = - fun _ _ -> () - method visit_rty : 'env -> rty -> unit = fun _ _ -> () end @@ -188,10 +196,6 @@ class ['self] map_typed_avalue_base = method visit_aproj : 'env -> aproj -> aproj = fun _ p -> p - method visit_abstract_shared_borrows - : 'env -> abstract_shared_borrows -> abstract_shared_borrows = - fun _ asb -> asb - method visit_rty : 'env -> rty -> rty = fun _ ty -> ty end @@ -247,7 +251,8 @@ and aloan_content = | AEndedSharedLoan of typed_value * typed_avalue | AIgnoredMutLoan of (BorrowId.id[@opaque]) * typed_avalue | AEndedIgnoredMutLoan of { given_back : typed_avalue; child : typed_avalue } - | AIgnoredSharedLoan of abstract_shared_borrows + | AIgnoredSharedLoan of (abstract_shared_borrows[@opaque]) + (** TODO: remove this one? *) (** Note that when a borrow content is ended, it is replaced by Bottom (while we need to track ended loans more precisely, especially because of their @@ -265,7 +270,7 @@ and aborrow_content = | AMutBorrow of (BorrowId.id[@opaque]) * typed_avalue | ASharedBorrow of (BorrowId.id[@opaque]) | AIgnoredMutBorrow of typed_avalue - | AIgnoredSharedBorrow of abstract_shared_borrows + | AIgnoredSharedBorrow of (abstract_shared_borrows[@opaque]) (* TODO: we may want to merge this with typed_value - would prevent some issues when accessing fields... *) |