diff options
| -rw-r--r-- | src/InterpreterBorrows.ml | 85 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 4 | ||||
| -rw-r--r-- | src/Print.ml | 2 | ||||
| -rw-r--r-- | src/Values.ml | 2 |
5 files changed, 57 insertions, 38 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index c471faf7..067b867e 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -976,7 +976,7 @@ and end_abstraction_loans (config : C.config) (abs_id : V.AbstractionId.id) super#visit_AEndedIgnoredMutLoan env given_back child | V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av - method! visit_ASymbolic env sproj = + method! visit_ASymbolic _ sproj = match sproj with | V.AProjBorrows (_, _) -> () | V.AProjLoans sv -> raise (FoundSymbolicValue sv) @@ -1007,6 +1007,7 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) (* Note that the abstraction mustn't contain any loans *) (* We end the borrows, starting with the *inner* ones. This is important when considering nested borrows which have the same lifetime. + TODO: is that really important? For instance: ``` @@ -1057,6 +1058,12 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ -> (* Nothing to do for ignored borrows *) () + + method! visit_ASymbolic _ sproj = + match sproj with + | V.AProjLoans _ -> failwith "Unexpected" + | V.AProjBorrows (sv, proj_ty) -> + raise (FoundAProjBorrows (sv, proj_ty)) end in (* Lookup the abstraction *) @@ -1067,42 +1074,44 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) (* No borrows: nothing to update *) ctx with - (* There are borrows: end them, then reexplore *) + (* There are concrete borrows: end them, then reexplore *) | FoundABorrowContent bc -> - (* First, replace the borrow by ⊥ *) - let bid = - match bc with - | V.AMutBorrow (bid, _) | V.ASharedBorrow bid -> bid - | V.AProjSharedBorrow asb -> ( - (* There should be at least one borrow identifier in the set, which we - * can use to identify the whole set *) - match - List.find - (fun x -> match x with V.AsbBorrow _ -> true | _ -> false) - asb - with - | V.AsbBorrow bid -> bid - | _ -> failwith "Unexpected") - | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ -> - failwith "Unexpected" - in - let ctx = update_aborrow ek_all bid V.ABottom ctx in - (* Then give back the value *) - let ctx = - match bc with - | V.AMutBorrow (bid, av) -> - (* First, convert the avalue to a (fresh symbolic) value *) - let v = convert_avalue_to_value av in - give_back_value config bid v ctx - | V.ASharedBorrow bid -> give_back_shared config bid ctx - | V.AProjSharedBorrow _ -> - (* Nothing to do *) - ctx - | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ -> - failwith "Unexpected" - in - (* Reexplore *) - end_abstraction_borrows config abs_id ctx + (* First, replace the borrow by ⊥ *) + let bid = + match bc with + | V.AMutBorrow (bid, _) | V.ASharedBorrow bid -> bid + | V.AProjSharedBorrow asb -> ( + (* There should be at least one borrow identifier in the set, which we + * can use to identify the whole set *) + match + List.find + (fun x -> match x with V.AsbBorrow _ -> true | _ -> false) + asb + with + | V.AsbBorrow bid -> bid + | _ -> failwith "Unexpected") + | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ -> + failwith "Unexpected" + in + let ctx = update_aborrow ek_all bid V.ABottom ctx in + (* Then give back the value *) + let ctx = + match bc with + | V.AMutBorrow (bid, av) -> + (* First, convert the avalue to a (fresh symbolic) value *) + let v = convert_avalue_to_value av in + give_back_value config bid v ctx + | V.ASharedBorrow bid -> give_back_shared config bid ctx + | V.AProjSharedBorrow _ -> + (* Nothing to do *) + ctx + | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ -> + failwith "Unexpected" + in + (* Reexplore *) + end_abstraction_borrows config abs_id ctx + (* There are symbolic borrows: end them, then reexplore *) + | FoundAProjBorrows (_sv, _proj_ty) -> raise Errors.Unimplemented (** Remove an abstraction from the context, as well as all its references *) and end_abstraction_remove_from_context (_config : C.config) @@ -1133,8 +1142,8 @@ and end_abstraction_remove_from_context (_config : C.config) intersecting proj_borrows, either in the concrete context or in an abstraction *) -and end_proj_loans_symbolic (config : C.config) (abs_id : V.AbstractionId.id) - (regions : T.RegionId.set_t) (sv : V.symbolic_value) (ctx : C.eval_ctx) : +and end_proj_loans_symbolic (_config : C.config) (_abs_id : V.AbstractionId.id) + (_regions : T.RegionId.set_t) (_sv : V.symbolic_value) (_ctx : C.eval_ctx) : C.eval_ctx = raise Errors.Unimplemented diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index e19f8bb4..18ec1ecc 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -75,6 +75,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) let proj_regions = current_abs.regions in let ancestors_regions = current_abs.ancestors_regions in match (aproj, proj_kind) with + | (V.AEndedProjLoans | V.AEndedProjBorrows), _ -> V.ASymbolic aproj | V.AProjLoans sv, LoanProj -> (* Check if this is the symbolic value we are looking for *) if same_symbolic_id sv original_sv then @@ -311,6 +312,7 @@ let expand_symbolic_value_shared_borrow (config : C.config) match reborrow_ashared (Option.get proj_regions) sv proj_ty with | None -> super#visit_ASymbolic proj_regions aproj | Some asb -> V.ABorrow (V.AProjSharedBorrow asb)) + | AEndedProjLoans | AEndedProjBorrows -> V.ASymbolic aproj end in (* Call the visitor *) diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index ce6bd0ce..9b272db8 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -133,6 +133,9 @@ exception FoundGLoanContent of g_loan_content exception FoundSymbolicValue of V.symbolic_value (** Utility exception *) +exception FoundAProjBorrows of V.symbolic_value * T.rty +(** Utility exception *) + let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) : bool = let obj = @@ -146,6 +149,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) : match aproj with | AProjLoans sv | AProjBorrows (sv, _) -> if sv.V.sv_id = sv_id then raise Found else () + | AEndedProjLoans | AEndedProjBorrows -> () method! visit_abstract_shared_borrows _ asb = let visit (asb : V.abstract_shared_borrow) : unit = diff --git a/src/Print.ml b/src/Print.ml index bc527acc..3869012a 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -315,6 +315,8 @@ module Values = struct ^ ")" | AProjBorrows (sv, rty) -> "proj_borrows (" ^ symbolic_value_proj_to_string fmt sv rty ^ ")" + | AEndedProjLoans -> "ended_proj_loans" + | AEndedProjBorrows -> "ended_proj_borrows" let rec typed_avalue_to_string (fmt : value_formatter) (v : V.typed_avalue) : string = diff --git a/src/Values.ml b/src/Values.ml index e8d4560e..41d8bd85 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -186,6 +186,8 @@ type aproj = | AProjBorrows of symbolic_value * rty (** Note that an AProjBorrows only operates on a value which is not below a shared loan: under a shared loan, we use [abstract_shared_borrow]. *) + | AEndedProjLoans + | AEndedProjBorrows [@@deriving show] type region = RegionVarId.id Types.region [@@deriving show] |