diff options
| -rw-r--r-- | src/InterpreterBorrows.ml | 36 | ||||
| -rw-r--r-- | src/main.ml | 2 |
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 |