diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml | 59 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 13 |
3 files changed, 24 insertions, 52 deletions
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 89c22f18..6f9b2ffe 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -610,8 +610,8 @@ let get_first_borrow_in_value (v : V.typed_value) : V.borrow_content option = the outer ones). [with_borrows]: - - if true: return the first loan or borrow we find - - if false: return the first loan we find, do not dive into borrowed values + - if [true]: return the first loan or borrow we find + - if [false]: return the first loan we find, do not dive into borrowed values *) let get_first_outer_loan_or_borrow_in_value (with_borrows : bool) (v : V.typed_value) : loan_or_borrow_content option = diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 4dea4c91..5fcc25eb 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -615,30 +615,20 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) * a recursive call to reinspect the value *) comp cc (end_loans_at_place config access p) cf ctx) -(** Drop (end) outer loans and borrows at a given place, which should be - seen as an l-value (we will write to it later, but need to drop - the borrows before writing). +(** Drop (end) outer loans at a given place, which should be seen as an l-value + (we will write to it later, but need to drop the loans before writing). This is used to drop values when evaluating the drop statement or before writing to a place. - [end_borrows]: - - if true: end all the loans and borrows we find, starting with the outer - ones. This is used when evaluating the {!LlbcAst.Drop} statement (see {!InterpreterStatements.drop_value}) - - if false: only end the outer loans. This is used by {!InterpreterStatements.assign_to_place} - or to drop the loans in the local variables when popping a frame. - TODO: remove this option, it is actually not used anymore (should always be - false). - Note that we don't do what is defined in the formalization: we move the - value to a temporary dummy value, then explore this value and end the - loans/borrows inside as long as we find some, starting with the outer - ones, then move the resulting value back to where it was. This shouldn't - make any difference, really (note that the place is *inside* a borrow, - if we end the borrow, we won't be able to reinsert the value back). + value to a temporary dummy value, then explore this value and end the outer + loans which are inside as long as we find some, then move the resulting + value back to where it was. This shouldn't make any difference, really (note + that the place is *inside* a borrow, if we end the borrow, we won't be able + to reinsert the value back). *) -let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool) - (p : E.place) : cm_fun = +let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun = fun cf ctx -> (* Move the current value in the place outside of this place and into * a dummy variable *) @@ -652,7 +642,8 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool) (* Read the value *) let v = C.ctx_read_first_dummy_var ctx in (* Check if there are loans or borrows to end *) - match get_first_outer_loan_or_borrow_in_value end_borrows v with + let with_borrows = false in + match get_first_outer_loan_or_borrow_in_value with_borrows v with | None -> (* We are done: simply call the continuation *) cf ctx @@ -662,12 +653,8 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool) match c with | LoanContent (V.SharedLoan (bids, _)) -> end_outer_borrows config bids - | LoanContent (V.MutLoan bid) - | BorrowContent (V.MutBorrow (bid, _) | SharedBorrow (_, bid)) -> - end_outer_borrow config bid - | BorrowContent (V.InactivatedMutBorrow (_, bid)) -> - (* First activate the borrow *) - activate_inactivated_mut_borrow config bid + | LoanContent (V.MutLoan bid) -> end_outer_borrow config bid + | BorrowContent _ -> raise (Failure "Unreachable") in (* Retry *) comp cc drop cf ctx @@ -682,10 +669,7 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool) (* Reinsert *) let ctx = write_place_unwrap config access p v ctx in (* Sanity check *) - if end_borrows then ( - assert (not (loans_in_value v)); - assert (not (borrows_in_value v))) - else assert (not (outer_loans_in_value v)); + assert (not (outer_loans_in_value v)); (* Continue *) cf ctx) in @@ -768,18 +752,14 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) (** Small utility. Prepare a place which is to be used as the destination of an assignment: - update the environment along the paths, end the loans at this place, etc. + update the environment along the paths, end the outer loans at this place, etc. Return the updated context and the (updated) value at the end of the - place. This value should not contain any loan or borrow (and we check + place. This value should not contain any outer loan (and we check it is the case). Note that this value is very likely to contain {!V.Bottom} subvalues. - - [end_borrows]: if false, we only end the outer loans we find. If true, we - end all the loans and the borrows we find. - TODO: end_borrows is not necessary anymore. *) -let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place) +let prepare_lplace (config : C.config) (p : E.place) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> log#ldebug @@ -790,16 +770,13 @@ let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place) let access = Write in let cc = update_ctx_along_write_place config access p in (* End the borrows and loans, starting with the borrows *) - let cc = comp cc (drop_outer_borrows_loans_at_lplace config end_borrows p) in + let cc = comp cc (drop_outer_loans_at_lplace config p) in (* Read the value and check it *) let read_check cf : m_fun = fun ctx -> let v = read_place_unwrap config access p ctx in (* Sanity checks *) - if end_borrows then ( - assert (not (loans_in_value v)); - assert (not (borrows_in_value v))) - else assert (not (outer_loans_in_value v)); + assert (not (outer_loans_in_value v)); (* Continue *) cf v ctx in diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index ebba0e56..84a6716c 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -34,8 +34,7 @@ let drop_value (config : C.config) (p : E.place) : cm_fun = * symbolic values along the path, for instance *) let cc = update_ctx_along_read_place config access p in (* Prepare the place (by ending the outer loans *at* the place). *) - let end_borrows = false in - let cc = comp cc (prepare_lplace config end_borrows p) in + let cc = comp cc (prepare_lplace config p) in (* Replace the value with {!Bottom} *) let replace cf (v : V.typed_value) ctx = (* Move the value at destination (that we will overwrite) to a dummy variable @@ -109,8 +108,7 @@ let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) : (* Push the rvalue to a dummy variable, for bookkeeping *) let cc = push_dummy_var rv in (* Prepare the destination *) - let end_borrows = false in - let cc = comp cc (prepare_lplace config end_borrows p) in + let cc = comp cc (prepare_lplace config p) in (* Retrieve the rvalue from the dummy variable *) let cc = comp cc (fun cf _lv -> pop_dummy_var cf) in (* Update the destination *) @@ -223,8 +221,7 @@ let set_discriminant (config : C.config) (p : E.place) (* Access the value *) let access = Write in let cc = update_ctx_along_read_place config access p in - let end_borrows = false in - let cc = comp cc (prepare_lplace config end_borrows p) in + let cc = comp cc (prepare_lplace config p) in (* Update the value *) let update_value cf (v : V.typed_value) : m_fun = fun ctx -> @@ -366,13 +363,11 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun = (* Drop the outer *loans* we find in the local variables *) let cf_drop_loans_in_locals cf (ret_value : V.typed_value) : m_fun = (* Drop the loans *) - let end_borrows = false in let locals = List.rev locals in let cf_drop = List.fold_left (fun cf lid -> - drop_outer_borrows_loans_at_lplace config end_borrows - (mk_place_from_var_id lid) cf) + drop_outer_loans_at_lplace config (mk_place_from_var_id lid) cf) (cf ret_value) locals in (* Apply *) |