diff options
Diffstat (limited to '')
| -rw-r--r-- | src/InterpreterBorrows.ml | 16 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 5 | ||||
| -rw-r--r-- | src/Invariants.ml | 4 | ||||
| -rw-r--r-- | src/Print.ml | 1 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 4 | ||||
| -rw-r--r-- | src/Values.ml | 4 |
6 files changed, 21 insertions, 13 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index ad7b5b2c..e7031d4c 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -187,7 +187,8 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) | V.AIgnoredMutBorrow (_, _) | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow - { given_back_loans_proj = _; child = _; given_back_meta = _ } -> + { given_back_loans_proj = _; child = _; given_back_meta = _ } + | V.AEndedSharedBorrow -> (* Nothing special to do *) super#visit_ABorrow outer bc | V.AProjSharedBorrow asb -> @@ -753,8 +754,8 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) (* Update the context *) give_back_shared config l ctx | Abstract - (V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _) - -> + ( V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ + | V.AEndedSharedBorrow ) -> failwith "Unreachable" (** Convert an [avalue] to a [value]. @@ -1158,7 +1159,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) then raise (FoundABorrowContent bc) else () | V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _ - | V.AEndedIgnoredMutBorrow _ -> + | V.AEndedIgnoredMutBorrow _ | V.AEndedSharedBorrow -> (* Nothing to do for ignored borrows *) () @@ -1202,8 +1203,9 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) let v = mk_typed_value_from_symbolic_value v in give_back_value config bid v ctx | V.ASharedBorrow bid -> - (* Replace the shared borrow with bottom *) - let ctx = update_aborrow ek_all bid V.ABottom ctx in + (* Replace the shared borrow to account for the fact it ended *) + let ended_borrow = V.ABorrow V.AEndedSharedBorrow in + let ctx = update_aborrow ek_all bid ended_borrow ctx in (* Give back *) give_back_shared config bid ctx | V.AProjSharedBorrow asb -> @@ -1230,7 +1232,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) (* Continue *) ctx | V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _ - | V.AEndedIgnoredMutBorrow _ -> + | V.AEndedIgnoredMutBorrow _ | V.AEndedSharedBorrow -> failwith "Unexpected" in (* Reexplore *) diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index b4ab7706..941ac140 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -434,7 +434,8 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) | V.AIgnoredMutBorrow (_, _) | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow - { given_back_loans_proj = _; child = _; given_back_meta = _ } -> + { given_back_loans_proj = _; child = _; given_back_meta = _ } + | V.AEndedSharedBorrow -> super#visit_aborrow_content env bc | V.AProjSharedBorrow asb -> if borrow_in_asb l asb then @@ -548,7 +549,7 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue) | V.ASharedBorrow bid -> if bid = l then update () else V.ABorrow (super#visit_ASharedBorrow env bid) - | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _ + | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _ | V.AEndedSharedBorrow | V.AEndedIgnoredMutBorrow _ -> super#visit_ABorrow env bc | V.AProjSharedBorrow asb -> diff --git a/src/Invariants.ml b/src/Invariants.ml index 522f2ffa..fe1b5e82 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -257,7 +257,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid | V.AIgnoredMutBorrow (None, _) | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow _ - | V.AProjSharedBorrow _ -> + | V.AEndedSharedBorrow | V.AProjSharedBorrow _ -> (* Do nothing *) () in @@ -361,7 +361,7 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = let info = match bc with | V.AMutBorrow (_, _, _) -> set_outer_mut info - | V.ASharedBorrow _ -> set_outer_shared info + | V.ASharedBorrow _ | V.AEndedSharedBorrow -> set_outer_shared info | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow _ -> set_outer_mut info diff --git a/src/Print.ml b/src/Print.ml index 69feeb6c..78a826bf 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -440,6 +440,7 @@ module Values = struct ^ "; " ^ typed_avalue_to_string fmt given_back_loans_proj ^ ")" + | AEndedSharedBorrow -> "@ended_shared_borrow" | AProjSharedBorrow sb -> "@ignored_shared_borrow(" ^ abstract_shared_borrows_to_string fmt sb diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 1985bfd3..80d08ac4 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -678,7 +678,7 @@ and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) : | AEndedIgnoredMutBorrow _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented - | AProjSharedBorrow _ -> + | AEndedSharedBorrow | AProjSharedBorrow _ -> (* Ignore *) None @@ -784,7 +784,7 @@ and aborrow_content_to_given_back (bc : V.aborrow_content) (ctx : bs_ctx) : | AEndedIgnoredMutBorrow _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented - | AProjSharedBorrow _ -> + | AEndedSharedBorrow | AProjSharedBorrow _ -> (* Ignore *) (ctx, None) diff --git a/src/Values.ml b/src/Values.ml index 57d188da..25d354fb 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -681,6 +681,10 @@ and aborrow_content = in practice the child value should only contain ended borrows, ignored values, bottom values, etc. *) + | AEndedSharedBorrow + (** We don't really need [AEndedSharedBorrow]: we simply want to be + precise, and not insert ⊥ when ending borrows. + *) | AEndedIgnoredMutBorrow of { child : typed_avalue; given_back_loans_proj : typed_avalue; |