diff options
| -rw-r--r-- | src/Interpreter.ml | 168 |
1 files changed, 120 insertions, 48 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index e0915028..b8943a9a 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -28,6 +28,14 @@ type config = { mode : interpreter_mode; check_invariants : bool } type outer_borrows = Borrows of BorrowId.Set.t | Borrow of BorrowId.id +(** The following type identifies the relative position of expressions (in + particular borrows) in other expressions. + + For instance, it is used to control [end_borrow]: we usually only allow + to end "outer" borrows, unless we perform a drop. +*) +type inner_outer = Inner | Outer + (** Borrow lookup result *) type borrow_lres = | NotFound @@ -38,15 +46,24 @@ type borrow_lres = let update_if_none opt x = match opt with None -> Some x | _ -> opt +let update_outer_borrows (io : inner_outer) opt x = + match io with + | Inner -> + (* If we can end inner borrows, we don't keep track of the outer borrows *) + None + | Outer -> update_if_none opt x + let unwrap_res_to_outer_or opt default = match opt with Some x -> Outer x | None -> default -let rec end_borrow_get_borrow_in_value config l outer_borrows v0 : +let rec end_borrow_get_borrow_in_value config io l outer_borrows v0 : borrow_lres * typed_value = match v0.value with | Concrete _ | Bottom | Symbolic _ -> (NotFound, v0) | Assumed (Box bv) -> - let res, bv' = end_borrow_get_borrow_in_value config l outer_borrows bv in + let res, bv' = + end_borrow_get_borrow_in_value config io l outer_borrows bv + in (* Note that we allow boxes to outlive the inner borrows. * Also note that when using the symbolic mode, boxes will never * be "opened" and will be manipulated solely through functions @@ -56,21 +73,26 @@ let rec end_borrow_get_borrow_in_value config l outer_borrows v0 : | Adt adt -> let values = FieldId.vector_to_list adt.field_values in let res, values' = - end_borrow_get_borrow_in_values config l outer_borrows values + end_borrow_get_borrow_in_values config io l outer_borrows values in let values' = FieldId.vector_of_list values' in (res, { v0 with value = Adt { adt with field_values = values' } }) | Tuple values -> let values = FieldId.vector_to_list values in let res, values' = - end_borrow_get_borrow_in_values config l outer_borrows values + end_borrow_get_borrow_in_values config io l outer_borrows values in let values' = FieldId.vector_of_list values' in (res, { v0 with value = Tuple values' }) | Loan (MutLoan _) -> (NotFound, v0) | Loan (SharedLoan (borrows, v)) -> - let outer_borrows = update_if_none outer_borrows (Borrows borrows) in - let res, v' = end_borrow_get_borrow_in_value config l outer_borrows v in + (* Update the outer borrows, if necessary *) + let outer_borrows = + update_outer_borrows io outer_borrows (Borrows borrows) + in + let res, v' = + end_borrow_get_borrow_in_value config io l outer_borrows v + in (res, { value = Loan (SharedLoan (borrows, v')); ty = v0.ty }) | Borrow (SharedBorrow l') -> if l = l' then @@ -87,34 +109,37 @@ let rec end_borrow_get_borrow_in_value config l outer_borrows v0 : ( unwrap_res_to_outer_or outer_borrows (FoundMut bv), { v0 with value = Bottom } ) else - let outer_borrows = update_if_none outer_borrows (Borrow l') in + (* Update the outer borrows, if necessary *) + let outer_borrows = update_outer_borrows io outer_borrows (Borrow l') in let res, bv' = - end_borrow_get_borrow_in_value config l outer_borrows bv + end_borrow_get_borrow_in_value config io l outer_borrows bv in (res, { v0 with value = Borrow (MutBorrow (l', bv')) }) -and end_borrow_get_borrow_in_values config l outer_borrows vl0 : +and end_borrow_get_borrow_in_values config io l outer_borrows vl0 : borrow_lres * typed_value list = match vl0 with | [] -> (NotFound, vl0) | v :: vl -> ( - let res, v' = end_borrow_get_borrow_in_value config l outer_borrows v in + let res, v' = + end_borrow_get_borrow_in_value config io l outer_borrows v + in match res with | NotFound -> let res, vl' = - end_borrow_get_borrow_in_values config l outer_borrows vl + end_borrow_get_borrow_in_values config io l outer_borrows vl in (res, v' :: vl') | _ -> (res, v' :: vl)) -let rec end_borrow_get_borrow_in_env (config : config) l env0 : - borrow_lres * env = +let rec end_borrow_get_borrow_in_env (config : config) (io : inner_outer) l env0 + : borrow_lres * env = match env0 with | [] -> (NotFound, []) | Var (x, v) :: env -> ( - match end_borrow_get_borrow_in_value config l None v with + match end_borrow_get_borrow_in_value config io l None v with | NotFound, v' -> - let res, env' = end_borrow_get_borrow_in_env config l env in + let res, env' = end_borrow_get_borrow_in_env config io l env in (res, Var (x, v') :: env') | res, v' -> (res, Var (x, v') :: env)) | Abs _ :: _ -> @@ -251,8 +276,9 @@ let give_back_shared config (bid : BorrowId.id) (env : env) : env = then update the loan. Ends outer borrows before updating the borrow if it is necessary. *) -let rec end_borrow (config : config) (l : BorrowId.id) (env0 : env) : env = - match end_borrow_get_borrow_in_env config l env0 with +let rec end_borrow (config : config) (io : inner_outer) (l : BorrowId.id) + (env0 : env) : env = + match end_borrow_get_borrow_in_env config io l env0 with (* It is possible that we can't find a borrow in symbolic mode (ending * an abstraction may end several borrows at once *) | NotFound, env -> @@ -262,17 +288,27 @@ let rec end_borrow (config : config) (l : BorrowId.id) (env0 : env) : env = | Outer outer_borrows, env -> let env' = match outer_borrows with - | Borrows bids -> end_borrows config bids env - | Borrow bid -> end_borrow config bid env + | Borrows bids -> end_borrows config io bids env + | Borrow bid -> end_borrow config io bid env in - end_borrow config l env' + (* Retry to end the borrow *) + end_borrow config io l env' (* If found mut: give the value back *) | FoundMut tv, env -> give_back_value config l tv env (* If found shared or inactivated mut: remove the borrow id from the loan set of the shared value *) | (FoundShared | FoundInactivatedMut), env -> give_back_shared config l env -and end_borrows (config : config) (lset : BorrowId.Set.t) (env0 : env) : env = - BorrowId.Set.fold (fun id env -> end_borrow config id env) lset env0 +and end_borrows (config : config) (io : inner_outer) (lset : BorrowId.Set.t) + (env0 : env) : env = + BorrowId.Set.fold (fun id env -> end_borrow config io id env) lset env0 + +let end_outer_borrow config = end_borrow config Outer + +let end_outer_borrows config = end_borrows config Outer + +let end_inner_borrow config = end_borrow config Inner + +let end_inner_borrows config = end_borrows config Inner let rec lookup_loan_in_value (config : config) (l : BorrowId.id) (v : typed_value) : loan_content option = @@ -431,15 +467,15 @@ let promote_inactivated_borrow_to_mut_borrow (config : config) (l : BorrowId.id) The borrow must point to a shared value which is borrowed exactly once. *) -let activate_inactivated_mut_borrow (config : config) (l : BorrowId.id) - (env : env) : env = +let activate_inactivated_mut_borrow (config : config) (io : inner_outer) + (l : BorrowId.id) (env : env) : env = match lookup_loan_from_borrow_id config l env with | MutLoan _ -> failwith "Unreachable" | SharedLoan (bids, _) -> (* End the borrows which borrow from the value, at the exception of the borrow * we want to promote *) let bids = BorrowId.Set.remove l bids in - let env' = end_borrows config bids env in + let env' = end_borrows config io bids env in (* Promote the loan *) let borrowed_value, env'' = promote_shared_loan_to_mut_loan config l env' @@ -792,10 +828,10 @@ let rec update_env_along_read_place (config : config) (access : access_kind) | Error err -> let env' = match err with - | FailSharedLoan bids -> end_borrows config bids env - | FailMutLoan bid -> end_borrow config bid env + | FailSharedLoan bids -> end_outer_borrows config bids env + | FailMutLoan bid -> end_outer_borrow config bid env | FailInactivatedMutBorrow bid -> - activate_inactivated_mut_borrow config bid env + activate_inactivated_mut_borrow config Outer bid env | FailSymbolic (pe, sp) -> (* Expand the symbolic value *) raise Unimplemented @@ -818,10 +854,10 @@ let rec update_env_along_write_place (config : config) | Error err -> let env' = match err with - | FailSharedLoan bids -> end_borrows config bids env - | FailMutLoan bid -> end_borrow config bid env + | FailSharedLoan bids -> end_outer_borrows config bids env + | FailMutLoan bid -> end_outer_borrow config bid env | FailInactivatedMutBorrow bid -> - activate_inactivated_mut_borrow config bid env + activate_inactivated_mut_borrow config Outer bid env | FailSymbolic (pe, sp) -> (* Expand the symbolic value *) raise Unimplemented @@ -874,7 +910,9 @@ let rec collect_borrows_at_place (config : config) (access : access_kind) | MutBorrow (_, tv) -> inspect_update tv | InactivatedMutBorrow bid -> (* We need to activate inactivated borrows *) - let env' = activate_inactivated_mut_borrow config bid env in + let env' = + activate_inactivated_mut_borrow config Inner bid env + in raise (UpdateEnv env')) | Loan lc -> ( match lc with @@ -884,11 +922,11 @@ let rec collect_borrows_at_place (config : config) (access : access_kind) match access with | Read -> inspect_update ty | Write -> - let env' = end_borrows config bids env in + let env' = end_outer_borrows config bids env in raise (UpdateEnv env')) | MutLoan bid -> (* We always need to end mutable borrows *) - let env' = end_borrow config bid env in + let env' = end_outer_borrow config bid env in raise (UpdateEnv env')) in (* Inspect the value and update the environment while doing so. @@ -924,9 +962,22 @@ let rec drop_borrows_at_place (config : config) (p : place) (env : env) : env = | Ok v -> ( (* Explore the value to check if we need to update the environment. + Note that we can end the borrows which are inside the value (while the + value itself might be inside a borrow/loan: we are thus ending inner + borrows). Because a loan inside the value may be linked to a borrow + somewhere else *also inside* the value (it's possible with adts), + we first end all the borrows we find - by using [Inner] to allow + ending inner borrows - then end all the loans we find. It is really + important to do this in two steps: the borrow linked to a loan may + be inside the value at place p, in which case this borrow may be + an inner borrow that we *can* end, but it may also be outside this + value, in which case we need to end all the outer borrows first... + Also, whenever the environment is updated, we need to re-inspect + the value at place p *in two steps* again (end borrows, then end loans). + We use exceptions to make it handy. *) - let rec inspect_update v : unit = + let rec inspect_update (end_loans : bool) v : unit = match v.value with | Concrete _ -> () | Bottom -> @@ -937,25 +988,43 @@ let rec drop_borrows_at_place (config : config) (p : place) (env : env) : env = | Symbolic _ -> (* Nothing to do for symbolic values - TODO: not sure *) raise Unimplemented - | Adt adt -> FieldId.iter inspect_update adt.field_values - | Tuple values -> FieldId.iter inspect_update values - | Assumed (Box v) -> inspect_update v + | Adt adt -> FieldId.iter (inspect_update end_loans) adt.field_values + | Tuple values -> FieldId.iter (inspect_update end_loans) values + | Assumed (Box v) -> inspect_update end_loans v | Borrow bc -> ( - (* We need to end all borrows *) + assert (not end_loans); + (* Sanity check *) + (* We need to end all borrows. Note that we ignore the outer borrows + when ending the borrows we find here (we call [end_inner_borrow(s)]: + the value at place p might be below a borrow/loan. Note however + that the borrow we found here is an outer borrow, if we restrain + ourselves at the value at place p. + *) match bc with | SharedBorrow bid | MutBorrow (bid, _) -> - raise (UpdateEnv (end_borrow config bid env)) + raise (UpdateEnv (end_inner_borrow config bid env)) | InactivatedMutBorrow bid -> (* We need to activate inactivated borrows - later, we will * actually end it *) - let env' = activate_inactivated_mut_borrow config bid env in + let env' = + activate_inactivated_mut_borrow config Inner bid env + in raise (UpdateEnv env')) - | Loan lc -> ( - (* We need to end all loans *) - match lc with - | SharedLoan (bids, _) -> - raise (UpdateEnv (end_borrows config bids env)) - | MutLoan bid -> raise (UpdateEnv (end_borrow config bid env))) + | Loan lc -> + if (* If we can, end the loans, otherwise ignore *) + end_loans then + (* We need to end all loans. Note that as all the borrows inside + the value at place p should already have ended, the borrows + associated to the loans we find here should be borrows from + outside this value: we need to call [end_outer_borrow(s)] + (we can't ignore outer borrows this time). + *) + match lc with + | SharedLoan (bids, _) -> + raise (UpdateEnv (end_outer_borrows config bids env)) + | MutLoan bid -> + raise (UpdateEnv (end_outer_borrow config bid env)) + else () in (* Inspect the value and update the environment while doing so. If the environment gets updated: perform a recursive call (many things @@ -964,7 +1033,10 @@ let rec drop_borrows_at_place (config : config) (p : place) (env : env) : env = anymore *) try - inspect_update v; + (* Inspect the value: end the borrows only *) + inspect_update false v; + (* Inspect the value: end the loans *) + inspect_update true v; (* No environment update required: return the current environment *) env with UpdateEnv env' -> drop_borrows_at_place config p env') |