diff options
| -rw-r--r-- | src/InterpreterBorrows.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 12 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 6 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 31 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 8 | ||||
| -rw-r--r-- | src/InterpreterProjectors.ml | 8 | ||||
| -rw-r--r-- | src/Invariants.ml | 6 | ||||
| -rw-r--r-- | src/Print.ml | 2 | ||||
| -rw-r--r-- | src/Values.ml | 54 |
9 files changed, 78 insertions, 53 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index f87d053c..b231722d 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -89,7 +89,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) method! visit_Borrow outer bc = match bc with - | SharedBorrow l' | InactivatedMutBorrow l' -> + | SharedBorrow (_, l') | InactivatedMutBorrow 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 *) @@ -713,7 +713,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); (* Update the context *) give_back_value config l tv ctx - | Concrete (V.SharedBorrow l' | V.InactivatedMutBorrow l') -> + | Concrete (V.SharedBorrow (_, l') | V.InactivatedMutBorrow l') -> (* Sanity check *) assert (l' = l); (* Check that the borrow is somewhere - purely a sanity check *) diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index 81f9d0d3..b4ab7706 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -194,9 +194,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) method! visit_borrow_content env bc = match bc with - | V.SharedBorrow bid -> + | V.SharedBorrow (mv, bid) -> (* Nothing specific to do *) - super#visit_SharedBorrow env bid + super#visit_SharedBorrow env mv bid | V.InactivatedMutBorrow bid -> (* Nothing specific to do *) super#visit_InactivatedMutBorrow env bid @@ -305,7 +305,7 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id) method! visit_borrow_content env bc = match bc with - | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> + | V.SharedBorrow (_, _) | V.InactivatedMutBorrow _ -> (* Nothing specific to do *) super#visit_borrow_content env bc | V.MutBorrow (bid, mv) -> @@ -407,7 +407,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) if bid = l then raise (FoundGBorrowContent (Concrete bc)) else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv else () - | V.SharedBorrow bid -> + | V.SharedBorrow (_, bid) -> (* Check the borrow id *) if bid = l then raise (FoundGBorrowContent (Concrete bc)) else () | V.InactivatedMutBorrow bid -> @@ -490,9 +490,9 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) 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 -> + | V.SharedBorrow (mv, bid) -> (* Check the id *) - if bid = l then update () else super#visit_SharedBorrow env bid + if bid = l then update () else super#visit_SharedBorrow env mv bid | V.InactivatedMutBorrow bid -> (* Check the id *) if bid = l then update () diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 69e12545..2dd36535 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -298,6 +298,8 @@ let expand_symbolic_value_shared_borrow (config : C.config) | _ -> failwith "Unexpected" else None in + (* The fresh symbolic value for the shared value *) + let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in (* Visitor to replace the projectors on borrows *) let obj = object (self) @@ -306,7 +308,8 @@ let expand_symbolic_value_shared_borrow (config : C.config) method! visit_Symbolic env sv = if same_symbolic_id sv original_sv then let bid = fresh_borrow () in - V.Borrow (V.SharedBorrow bid) + V.Borrow + (V.SharedBorrow (mk_typed_value_from_symbolic_value shared_sv, bid)) else super#visit_Symbolic env sv method! visit_Abs proj_regions abs = @@ -362,7 +365,6 @@ let expand_symbolic_value_shared_borrow (config : C.config) (* Finally, replace the projectors on loans *) let bids = !borrows in assert (not (V.BorrowId.Set.is_empty bids)); - let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in let see = V.SeSharedRef (bids, shared_sv) in let allow_reborrows = true in let ctx = diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 3ebce9bf..84f51c94 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -508,33 +508,34 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) (* Evaluate the borrowing operation *) let eval (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun = fun ctx -> - (* Compute the rvalue - simply a shared borrow with a fresh id *) + (* Generate the fresh borrow id *) let bid = C.fresh_borrow_id () in - (* Note that the reference is *mutable* if we do a two-phase borrow *) - let rv_ty = - T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut) - in - let bc = - if bkind = E.Shared then V.SharedBorrow bid - else V.InactivatedMutBorrow bid - in - let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in - (* Compute the value with which to replace the value at place p *) - let nv = + (* Compute the loan value, with which to replace the value at place p *) + let nv, shared_mvalue = match v.V.value with | V.Loan (V.SharedLoan (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 V.value = V.Loan (V.SharedLoan (bids1, sv)) }, sv) | _ -> (* Not a shared loan: add a wrapper *) let v' = V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v)) in - { v with V.value = v' } + ({ v with V.value = v' }, v) in - (* Update the value in the context *) + (* Update the borrowed value in the context *) let ctx = write_place_unwrap config access p nv ctx in + (* Compute the rvalue - simply a shared borrow with a the fresh id. + * Note that the reference is *mutable* if we do a two-phase borrow *) + let rv_ty = + T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut) + in + let bc = + if bkind = E.Shared then V.SharedBorrow (shared_mvalue, bid) + else V.InactivatedMutBorrow bid + in + let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in (* Continue *) cf rv ctx in diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index e45dbb3a..300e50c5 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -160,7 +160,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) (* Borrows *) | Deref, V.Borrow bc, _ -> ( match bc with - | V.SharedBorrow bid -> + | V.SharedBorrow (_, bid) -> (* Lookup the loan content, and explore from there *) if access.lookup_shared_borrows then match lookup_loan ek bid ctx with @@ -643,7 +643,7 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool) | LoanContent (V.SharedLoan (bids, _)) -> end_outer_borrows config bids | LoanContent (V.MutLoan bid) - | BorrowContent (V.MutBorrow (bid, _) | SharedBorrow bid) -> + | BorrowContent (V.MutBorrow (bid, _) | SharedBorrow (_, bid)) -> end_outer_borrow config bid | BorrowContent (V.InactivatedMutBorrow bid) -> (* First activate the borrow *) @@ -715,12 +715,12 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) | V.Borrow bc -> ( (* We can only copy shared borrows *) match bc with - | SharedBorrow bid -> + | SharedBorrow (mv, 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 = reborrow_shared bid bid' ctx in - (ctx, { v with V.value = V.Borrow (SharedBorrow bid') }) + (ctx, { v with V.value = V.Borrow (SharedBorrow (mv, bid')) }) | MutBorrow (_, _) -> failwith "Can't copy a mutable borrow" | V.InactivatedMutBorrow _ -> failwith "Can't copy an inactivated mut borrow") diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index 946bacea..76b7d6ae 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -56,7 +56,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) bv ref_ty in (bid, asb) - | V.SharedBorrow bid, T.Shared -> + | V.SharedBorrow (_, bid), T.Shared -> (* Lookup the shared value *) let ek = ek_all in let sv = lookup_loan ek bid ctx in @@ -172,7 +172,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) fresh_reborrow regions ancestors_regions bv ref_ty in V.AMutBorrow (mv, bid, bv) - | V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid + | V.SharedBorrow (_, bid), T.Shared -> V.ASharedBorrow bid | V.InactivatedMutBorrow _, _ -> failwith "Can't apply a proj_borrow over an inactivated mutable \ @@ -197,7 +197,7 @@ 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 -> + | V.SharedBorrow (_, bid), T.Shared -> (* Lookup the shared value *) let ek = ek_all in let sv = lookup_loan ek bid ctx in @@ -370,7 +370,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) match v.V.value with | V.Borrow lc -> ( match lc with - | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> None + | V.SharedBorrow (_, _) | V.InactivatedMutBorrow _ -> None | V.MutBorrow (id, _) -> Some id) | _ -> None in diff --git a/src/Invariants.ml b/src/Invariants.ml index 6ebd3375..ee58a1a3 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -242,7 +242,7 @@ 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.SharedBorrow (_, bid) -> register_borrow Shared bid | V.MutBorrow (bid, _) -> register_borrow Mut bid | V.InactivatedMutBorrow bid -> register_borrow Inactivated bid in @@ -451,8 +451,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | V.Bottom, _ -> (* Nothing to check *) () | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> ( match (bc, rkind) with - | V.SharedBorrow bid, T.Shared | V.InactivatedMutBorrow bid, T.Mut - -> ( + | V.SharedBorrow (_, bid), T.Shared + | V.InactivatedMutBorrow bid, T.Mut -> ( (* Lookup the borrowed value to check it has the proper type *) let _, glc = lookup_loan ek_all bid ctx in match glc with diff --git a/src/Print.ml b/src/Print.ml index cefa3ea5..da6158b5 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -278,7 +278,7 @@ module Values = struct and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) : string = match bc with - | SharedBorrow bid -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋" + | SharedBorrow (_, bid) -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋" | MutBorrow (bid, tv) -> "&mut@" ^ V.BorrowId.to_string bid ^ " (" ^ typed_value_to_string fmt tv diff --git a/src/Values.ml b/src/Values.ml index 90250c63..57d188da 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -131,7 +131,17 @@ and adt_value = { } and borrow_content = - | SharedBorrow of (BorrowId.id[@opaque]) (** A shared value *) + | SharedBorrow of mvalue * (BorrowId.id[@opaque]) + (** A shared borrow. + + We remember the shared value which was borrowed as a meta value. + This is necessary for synthesis: upon translating to "pure" values, + we can't perform any lookup because we don't have an environment + anymore. Note that it is ok to keep the shared value and copy + the shared value this way, because shared values are immutable + for as long as they are shared (i.e., as long as we can use the + shared borrow). + *) | MutBorrow of (BorrowId.id[@opaque]) * typed_value (** A mutably borrowed value. *) | InactivatedMutBorrow of (BorrowId.id[@opaque]) @@ -168,12 +178,23 @@ and loan_content = borrows, and extremely useful when giving shared values to abstractions). *) +and mvalue = typed_value +(** "Meta"-value: information we store for the synthesis. + + Note that we never automatically visit the meta-values with the + visitors: they really are meta information, and shouldn't be considered + as part of the environment during a symbolic execution. + + TODO: we may want to create wrappers, to prevent accidently mixing meta + values and regular values. + *) + and typed_value = { value : value; ty : ety } [@@deriving show, visitors { - name = "iter_typed_value"; + name = "iter_typed_value_visit_mvalue"; variety = "iter"; ancestors = [ "iter_typed_value_base" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); @@ -181,7 +202,7 @@ and typed_value = { value : value; ty : ety } }, visitors { - name = "map_typed_value"; + name = "map_typed_value_visit_mvalue"; variety = "map"; ancestors = [ "map_typed_value_base" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); @@ -189,16 +210,21 @@ and typed_value = { value : value; ty : ety } }] (** "Regular" typed value (we map variables to typed values) *) -type mvalue = typed_value [@@deriving show] -(** "Meta"-value: information we store for the synthesis. +(** We have to override the [visit_mvalue] method, to ignore meta-values *) +class ['self] iter_typed_value = + object (_self : 'self) + inherit [_] iter_typed_value_visit_mvalue - Note that we never automatically visit the meta-values with the - visitors: they really are meta information, and shouldn't be considered - as part of the environment during a symbolic execution. - - TODO: we may want to create wrappers, to prevent mixing meta values - and regular values. - *) + method! visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> () + end + +(** We have to override the [visit_mvalue] method, to ignore meta-values *) +class ['self] map_typed_value = + object (_self : 'self) + inherit [_] map_typed_value_visit_mvalue + + method! visit_mvalue : 'env -> mvalue -> mvalue = fun _ x -> x + end type msymbolic_value = symbolic_value [@@deriving show] (** "Meta"-symbolic value. @@ -238,8 +264,6 @@ class ['self] iter_aproj_base = method visit_rty : 'env -> rty -> unit = fun _ _ -> () - method visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> () - method visit_msymbolic_value : 'env -> msymbolic_value -> unit = fun _ _ -> () end @@ -251,8 +275,6 @@ class ['self] map_aproj_base = method visit_rty : 'env -> rty -> rty = fun _ ty -> ty - method visit_mvalue : 'env -> mvalue -> mvalue = fun _ v -> v - method visit_msymbolic_value : 'env -> msymbolic_value -> msymbolic_value = fun _ m -> m end |