summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/InterpreterBorrows.ml36
-rw-r--r--src/main.ml2
2 files changed, 32 insertions, 6 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 487e308a..24521335 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -1063,7 +1063,7 @@ and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids)
| V.AIgnoredSharedLoan _ ->
super#visit_aloan_content env lc
- method! visit_loan_content env lc =
+ method! visit_loan_content _ lc =
match lc with
| V.MutLoan _ ->
(* The mut loan linked to the mutable borrow present in a shared
@@ -1159,9 +1159,12 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
());
super#visit_aproj env sproj
- method! visit_borrow_content env bc =
- (* TODO: this happens because of shared values *)
- raise Errors.Unimplemented
+ method! visit_borrow_content _ bc =
+ match bc with
+ | V.SharedBorrow (_, _) | V.MutBorrow (_, _) ->
+ raise (FoundBorrowContent bc)
+ | V.InactivatedMutBorrow _ -> failwith "Unreachable"
+ (** We may need to end borrows in "regular" values, because of shared values *)
end
in
(* Lookup the abstraction *)
@@ -1172,7 +1175,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
(* No borrows: nothing to update *)
cf ctx
with
- (* There are concrete borrows: end them, then reexplore *)
+ (* There are concrete (i.e., not symbolic) borrows: end them, then reexplore *)
| FoundABorrowContent bc ->
let ctx =
match bc with
@@ -1233,6 +1236,29 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
in
(* Reexplore *)
end_abstraction_borrows config chain abs_id cf ctx
+ (* There are concrete (i.e., not symbolic) borrows in shared values: end them, then reexplore *)
+ | FoundBorrowContent bc ->
+ let ctx =
+ match bc with
+ | V.SharedBorrow (_, bid) -> (
+ (* Replace the shared borrow with bottom *)
+ match end_borrow_get_borrow (Some abs_id) bid ctx with
+ | Error _ -> failwith "Unreachable"
+ | Ok (ctx, _) ->
+ (* Give back *)
+ give_back_shared config bid ctx)
+ | V.MutBorrow (bid, v) -> (
+ (* Replace the mut borrow with bottom *)
+ match end_borrow_get_borrow (Some abs_id) bid ctx with
+ | Error _ -> failwith "Unreachable"
+ | Ok (ctx, _) ->
+ (* 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.InactivatedMutBorrow _ -> failwith "Unreachable"
+ in
+ (* Reexplore *)
+ end_abstraction_borrows config chain abs_id cf ctx
(** Remove an abstraction from the context, as well as all its references *)
and end_abstraction_remove_from_context (_config : C.config)
diff --git a/src/main.ml b/src/main.ml
index e803c49c..ea4ab23f 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -55,7 +55,7 @@ let () =
expressions_log#set_level EL.Debug;
expansion_log#set_level EL.Debug;
borrows_log#set_level EL.Debug;
- invariants_log#set_level EL.Debug;
+ invariants_log#set_level EL.Warning;
(* Load the module *)
let json = Yojson.Basic.from_file !filename in
match cfim_module_of_json json with