From bd93cad791d8191b47f4152461668ffcfbe38e27 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 24 Nov 2021 10:52:45 +0100 Subject: Start refactoring the code --- src/Contexts.ml | 33 ++- src/Identifiers.ml | 8 + src/Interpreter.ml | 638 ++++++++++++++++++++++++++++++++++++++--------------- src/Print.ml | 4 +- 4 files changed, 494 insertions(+), 189 deletions(-) diff --git a/src/Contexts.ml b/src/Contexts.ml index 77dd9c49..1f7d28a4 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -45,15 +45,42 @@ let fresh_borrow_id (ctx : eval_ctx) : eval_ctx * BorrowId.id = let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var = TypeVarId.nth ctx.type_vars vid -let lookup_var (ctx : eval_ctx) (vid : VarId.id) : var = +let ctx_lookup_var (ctx : eval_ctx) (vid : VarId.id) : var = VarId.Map.find vid ctx.vars -let lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value = +(** Retrieve a variable's value in an environment *) +let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = let check_ev (ev : env_value) : typed_value option = match ev with | Var (vid', v) -> if vid' = vid then Some v else None | Abs _ -> None in - match List.find_map check_ev ctx.env with + match List.find_map check_ev env with | None -> failwith "Unreachable" | Some v -> v + +(** Retrieve a variable's value in an evaluation context *) +let ctx_lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value = + env_lookup_var_value ctx.env vid + +(** Update a variable's value in an environment + + This is a helper function: it can break invariants and doesn't perform + any check. +*) +let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env = + let update_ev (ev : env_value) : env_value = + match ev with + | Var (vid', v) -> if vid' = vid then Var (vid, nv) else Var (vid', v) + | Abs abs -> Abs abs + in + List.map update_ev env + +(** Update a variable's value in an evaluation context. + + This is a helper function: it can break invariants and doesn't perform + any check. +*) +let ctx_update_var_value (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) : + eval_ctx = + { ctx with env = env_update_var_value ctx.env vid nv } diff --git a/src/Identifiers.ml b/src/Identifiers.ml index dc8ae320..22b52119 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -38,6 +38,10 @@ module type Id = sig val map : ('a -> 'b) -> 'a vector -> 'b vector + val for_all : ('a -> bool) -> 'a vector -> bool + + val exists : ('a -> bool) -> 'a vector -> bool + module Set : Set.S with type elt = id val set_to_string : Set.t -> string @@ -98,6 +102,10 @@ module IdGen () : Id = struct let map = List.map + let for_all = List.for_all + + let exists = List.exists + module Set = Set.Make (struct type t = id diff --git a/src/Interpreter.ml b/src/Interpreter.ml index ca7d7a09..7582735d 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -10,6 +10,252 @@ open Contexts (* TODO: Change state-passing style to : st -> ... -> (st, v) *) (* TODO: check that the value types are correct when evaluating *) +type exploration_kind = { + enter_shared_loans : bool; + enter_mut_borrows : bool; + enter_abs : bool; +} +(** This record controls how some generic helper lookup/update + functions behave, by restraining the kind of therms they can enter. +*) + +(** Apply a predicate to all the borrows in a value *) +let rec check_borrows_in_value (check : borrow_content -> bool) + (v : typed_value) : bool = + match v.value with + | Concrete _ | Bottom | Symbolic _ -> true + | Adt av -> FieldId.for_all (check_borrows_in_value check) av.field_values + | Tuple values -> FieldId.for_all (check_borrows_in_value check) values + | Assumed (Box bv) -> check_borrows_in_value check bv + | Borrow bc -> ( + check bc + && + match bc with + | SharedBorrow _ | InactivatedMutBorrow _ -> true + | MutBorrow (_, mv) -> check_borrows_in_value check mv) + | Loan lc -> ( + match lc with + | SharedLoan (_, sv) -> check_borrows_in_value check sv + | MutLoan _ -> true) + +(** Apply a predicate to all the loans in a value *) +let rec check_loans_in_value (check : loan_content -> bool) (v : typed_value) : + bool = + match v.value with + | Concrete _ | Bottom | Symbolic _ -> true + | Adt av -> FieldId.for_all (check_loans_in_value check) av.field_values + | Tuple values -> FieldId.for_all (check_loans_in_value check) values + | Assumed (Box bv) -> check_loans_in_value check bv + | Borrow bc -> ( + match bc with + | SharedBorrow _ | InactivatedMutBorrow _ -> true + | MutBorrow (_, mv) -> check_loans_in_value check mv) + | Loan lc -> ( + check lc + && + match lc with + | SharedLoan (_, sv) -> check_loans_in_value check sv + | MutLoan _ -> true) + +(** Lookup a loan content in a value *) +let rec lookup_loan_in_value (ek : exploration_kind) (l : BorrowId.id) + (v : typed_value) : loan_content option = + match v.value with + | Concrete _ | Bottom | Symbolic _ -> None + | Adt av -> + let values = FieldId.vector_to_list av.field_values in + List.find_map (lookup_loan_in_value ek l) values + | Tuple values -> + let values = FieldId.vector_to_list values in + List.find_map (lookup_loan_in_value ek l) values + | Assumed (Box bv) -> lookup_loan_in_value ek l bv + | Borrow bc -> ( + match bc with + | SharedBorrow _ | InactivatedMutBorrow _ -> None + | MutBorrow (_, mv) -> + if ek.enter_mut_borrows then lookup_loan_in_value ek l mv else None) + | Loan lc -> ( + match lc with + | SharedLoan (bids, sv) -> + if BorrowId.Set.mem l bids then Some lc + else if ek.enter_shared_loans then lookup_loan_in_value ek l sv + else None + | MutLoan bid -> if bid = l then Some (MutLoan bid) else None) + +(** Lookup a loan content. + + The loan is referred to by a borrow id. + *) +let lookup_loan (ek : exploration_kind) (l : BorrowId.id) (env : env) : + loan_content = + let lookup_loan_in_env_value (ev : env_value) : loan_content option = + match ev with + | Var (_, v) -> lookup_loan_in_value ek l v + | Abs _ -> raise Unimplemented + (* TODO *) + in + match List.find_map lookup_loan_in_env_value env with + | None -> failwith "Unreachable" + | Some lc -> lc + +(** Update a loan content in a value. + + The loan is referred to by a borrow id. + + This is a helper function: it might break invariants. + *) +let rec update_loan_in_value (ek : exploration_kind) (l : BorrowId.id) + (nlc : loan_content) (v : typed_value) : typed_value = + match v.value with + | Concrete _ | Bottom | Symbolic _ -> v + | Adt av -> + let values = + FieldId.map (update_loan_in_value ek l nlc) av.field_values + in + let av = { av with field_values = values } in + { v with value = Adt av } + | Tuple values -> + let values = FieldId.map (update_loan_in_value ek l nlc) values in + { v with value = Tuple values } + | Assumed (Box bv) -> + { v with value = Assumed (Box (update_loan_in_value ek l nlc bv)) } + | Borrow bc -> ( + match bc with + | SharedBorrow _ | InactivatedMutBorrow _ -> v + | MutBorrow (bid, mv) -> + if ek.enter_mut_borrows then + let v' = + Borrow (MutBorrow (bid, update_loan_in_value ek l nlc mv)) + in + { v with value = v' } + else v) + | Loan lc -> ( + match lc with + | SharedLoan (bids, sv) -> + if BorrowId.Set.mem l bids then { v with value = Loan nlc } + else if ek.enter_shared_loans then + let v' = + Loan (SharedLoan (bids, update_loan_in_value ek l nlc sv)) + in + { v with value = v' } + else v + | MutLoan bid -> if bid = l then { v with value = Loan nlc } else v) + +(** Update a loan content. + + The loan is referred to by a borrow id. + + This is a helper function: it might break invariants. + *) +let update_loan (ek : exploration_kind) (l : BorrowId.id) (nlc : loan_content) + (env : env) : env = + let update_loan_in_env_value (ev : env_value) : env_value = + match ev with + | Var (vid, v) -> Var (vid, update_loan_in_value ek l nlc v) + | Abs abs -> raise Unimplemented + (* TODO *) + in + List.map update_loan_in_env_value env + +(** Lookup a borrow content in a value *) +let rec lookup_borrow_in_value (ek : exploration_kind) (l : BorrowId.id) + (v : typed_value) : borrow_content option = + match v.value with + | Concrete _ | Bottom | Symbolic _ -> None + | Adt av -> + let values = FieldId.vector_to_list av.field_values in + List.find_map (lookup_borrow_in_value ek l) values + | Tuple values -> + let values = FieldId.vector_to_list values in + List.find_map (lookup_borrow_in_value ek l) values + | Assumed (Box bv) -> lookup_borrow_in_value ek l bv + | Borrow bc -> ( + match bc with + | SharedBorrow bid -> if l = bid then Some bc else None + | InactivatedMutBorrow bid -> if l = bid then Some bc else None + | MutBorrow (bid, mv) -> + if bid = l then Some bc + else if ek.enter_mut_borrows then lookup_borrow_in_value ek l mv + else None) + | Loan lc -> ( + match lc with + | SharedLoan (_, sv) -> + if ek.enter_shared_loans then lookup_borrow_in_value ek l sv else None + | MutLoan bid -> None) + +(** Lookup a borrow content from a borrow id. *) +let lookup_borrow (ek : exploration_kind) (l : BorrowId.id) (env : env) : + borrow_content = + let lookup_borrow_in_env_value (ev : env_value) = + match ev with + | Var (_, v) -> lookup_borrow_in_value ek l v + | Abs _ -> raise Unimplemented + (* TODO *) + in + match List.find_map lookup_borrow_in_env_value env with + | None -> failwith "Unreachable" + | Some lc -> lc + +(** Update a borrow content in a value. + + The borrow is referred to by a borrow id. + + This is a helper function: it might break invariants. + *) +let rec update_borrow_in_value (ek : exploration_kind) (l : BorrowId.id) + (nbc : borrow_content) (v : typed_value) : typed_value = + match v.value with + | Concrete _ | Bottom | Symbolic _ -> v + | Adt av -> + let values = + FieldId.map (update_borrow_in_value ek l nbc) av.field_values + in + let av = { av with field_values = values } in + { v with value = Adt av } + | Tuple values -> + let values = FieldId.map (update_borrow_in_value ek l nbc) values in + { v with value = Tuple values } + | Assumed (Box bv) -> + { v with value = Assumed (Box (update_borrow_in_value ek l nbc bv)) } + | Borrow bc -> ( + match bc with + | SharedBorrow bid | InactivatedMutBorrow bid -> + if bid = l then { v with value = Borrow nbc } else v + | MutBorrow (bid, mv) -> + if bid = l then { v with value = Borrow nbc } + else if ek.enter_mut_borrows then + let v' = + Borrow (MutBorrow (bid, update_borrow_in_value ek l nbc mv)) + in + { v with value = v' } + else v) + | Loan lc -> ( + match lc with + | SharedLoan (bids, sv) -> + if ek.enter_shared_loans then + let v' = + Loan (SharedLoan (bids, update_borrow_in_value ek l nbc sv)) + in + { v with value = v' } + else v + | MutLoan _ -> v) + +(** Update a borrow content. + + The borrow is referred to by a borrow id. + + This is a helper function: it might break invariants. + *) +let update_borrow (ek : exploration_kind) (l : BorrowId.id) + (nbc : borrow_content) (env : env) : env = + let update_borrow_in_env_value (ev : env_value) : env_value = + match ev with + | Var (vid, v) -> Var (vid, update_borrow_in_value ek l nbc v) + | Abs abs -> raise Unimplemented + (* TODO *) + in + List.map update_borrow_in_env_value env + (** The following type identifies the relative position of expressions (in particular borrows) in other expressions. @@ -430,172 +676,60 @@ 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 = - match v.value with - | Concrete _ | Bottom | Symbolic _ -> None - | Adt av -> - let values = FieldId.vector_to_list av.field_values in - List.find_map (lookup_loan_in_value config l) values - | Tuple values -> - let values = FieldId.vector_to_list values in - List.find_map (lookup_loan_in_value config l) values - | Assumed (Box bv) -> lookup_loan_in_value config l bv - | Borrow bc -> ( - match bc with - | SharedBorrow _ | InactivatedMutBorrow _ -> None - | MutBorrow (_, mv) -> lookup_loan_in_value config l mv) - | Loan lc -> ( - match lc with - | SharedLoan (bids, sv) -> - if BorrowId.Set.mem l bids then Some lc - else lookup_loan_in_value config l sv - | MutLoan _ -> None) - -(** Lookup a loan - note that we never lookup loans in abstractions *) -let lookup_loan_in_env_value (config : config) (l : BorrowId.id) - (ev : env_value) : loan_content option = - match ev with - | Var (_, v) -> lookup_loan_in_value config l v - | Abs _ -> - assert (config.mode = SymbolicMode); - None - -(** Lookup a loan content from a borrow id. - Note that we never lookup loans in the abstractions. - *) -let lookup_loan_from_borrow_id (config : config) (l : BorrowId.id) (env : env) : - loan_content = - match List.find_map (lookup_loan_in_env_value config l) env with - | None -> failwith "Unreachable" - | Some lc -> lc - -(** See [activate_inactivated_mut_borrow]. +(** Helper function: see [activate_inactivated_mut_borrow]. This function updates the shared loan to a mutable loan (we then update - the borrow). Of course, the shared loan must contain exactly one borrow id - (the one we give as parameter), otherwise we can't promote it. - Also, the shared value mustn't contain any loan. + the borrow with another helper). Of course, the shared loan must contain + exactly one borrow id (the one we give as parameter), otherwise we can't + promote it. Also, the shared value mustn't contain any loan. + + The returned value (previously shared) is checked: + - it mustn't contain loans + - it mustn't contain [Bottom] + - it mustn't contain inactivated borrows + TODO: this kind of checks should be put in an auxiliary helper, because + they are redundant *) -let promote_shared_loan_to_mut_loan (config : config) (l : BorrowId.id) - (env0 : env) : typed_value * env = - (* Promote inside a value: return the borrowed value and the updated value. - * The return value is an option: we return None if we didn't update anything. *) - let rec promote_in_value (v : typed_value) : - (typed_value * typed_value) option = - match v.value with - | Concrete _ | Bottom | Symbolic _ -> None - | Adt av -> ( - let values = FieldId.vector_to_list av.field_values in - match promote_in_values values with - | None -> None - | Some (borrowed, values') -> - let av = - { av with field_values = FieldId.vector_of_list values' } - in - Some (borrowed, { v with value = Adt av })) - | Tuple values -> ( - let values = FieldId.vector_to_list values in - match promote_in_values values with - | None -> None - | Some (borrowed, values') -> - let values' = FieldId.vector_of_list values' in - Some (borrowed, { v with value = Tuple values' })) - | Borrow _ -> - (* We can't promote inside a borrow *) - None - | Loan lc -> ( - match lc with - | SharedLoan (bids, tv) -> - (* Note that we can't promote *inside* shared values: if we - don't find the borrow we were looking for, we don't dive - inside the shared value *) - if BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1 then ( - (* We need to check that there aren't any loans in the value: - we should have gotten rid of those already, but it is better - to do a sanity check. *) - assert (not (loans_in_value tv)); - assert (not (bottom_in_value tv)); - Some (tv, { v with value = Loan (MutLoan l) })) - else None - | MutLoan _ -> None) - | Assumed (Box bv) -> ( - match promote_in_value bv with - | None -> None - | Some (borrowed, bv') -> - Some (borrowed, { v with value = Assumed (Box bv') })) - (* Promote inside a list of values: return the borrowed value (if we promoted one) - * and the list of updated values *) - and promote_in_values (vl : typed_value list) : - (typed_value * typed_value list) option = - match vl with - | [] -> None - | v :: vl' -> ( - match promote_in_value v with - | None -> ( - match promote_in_values vl' with - | None -> None - | Some (borrowed, vl'') -> Some (borrowed, v :: vl'')) - | Some (borrowed, nv) -> Some (borrowed, nv :: vl')) - in - (* Promote in the environment *) - let rec promote_in_env (env0 : env) : typed_value * env = - match env0 with - | [] -> failwith "Unreachable" - | Var (vid, v) :: env -> ( - match promote_in_value v with - | None -> - let borrowed, env' = promote_in_env env in - (borrowed, Var (vid, v) :: env') - | Some (borrowed, new_v) -> (borrowed, Var (vid, new_v) :: env)) - | Abs abs :: env -> - (* We don't promote inside abstractions *) - assert (config.mode = SymbolicMode); - let borrowed, env' = promote_in_env env in - (borrowed, Abs abs :: env') +let promote_shared_loan_to_mut_loan (l : BorrowId.id) (env : env) : + env * typed_value = + (* Lookup the shared loan *) + let ek = + { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in - (* Apply *) - promote_in_env env0 - -(** See [activate_inactivated_mut_borrow]. - - This function updates the shared borrow to a mutable borrow. + match lookup_loan ek l env with + | MutLoan _ -> failwith "Expected a shared loan, found a mut loan" + | SharedLoan (bids, sv) -> + (* Check that there is only one borrow id (l) and update the loan *) + assert (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1); + (* We need to check that there aren't any loans in the value: + we should have gotten rid of those already, but it is better + to do a sanity check. *) + assert (not (loans_in_value sv)); + (* Also need to check there isn't [Bottom] (this is actually an invariant *) + assert (not (bottom_in_value sv)); + (* Update the loan content *) + let env1 = update_loan ek l (MutLoan l) env in + (* Return *) + (env1, sv) + +(** Helper function: see [activate_inactivated_mut_borrow]. + + This function updates a shared borrow to a mutable borrow. *) -let promote_inactivated_borrow_to_mut_borrow (config : config) (l : BorrowId.id) - (borrowed_value : typed_value) (env0 : env) : env = - let rec promote_in_value (v : typed_value) : typed_value = - match v.value with - | Concrete _ | Bottom | Symbolic _ -> v - | Adt av -> - let values = FieldId.vector_to_list av.field_values in - let values = List.map promote_in_value values in - let values = FieldId.vector_of_list values in - { v with value = Adt { av with field_values = values } } - | Tuple values -> - let values = FieldId.vector_to_list values in - let values = List.map promote_in_value values in - let values = FieldId.vector_of_list values in - { v with value = Tuple values } - | Assumed (Box av) -> { v with value = Assumed (Box (promote_in_value av)) } - | Borrow bc -> ( - (* We shouldn't need to promote inside borrowed values: here we just need - * to check if the borrow is the inactivated mutable borrow we are looking - * for *) - match bc with - | SharedBorrow _ | MutBorrow (_, _) -> v - | InactivatedMutBorrow bid -> if bid == l then borrowed_value else v) - | Loan _ -> - (* We shouldn't need to promote inside loans *) - v - in - let promote_in_env_value (ev : env_value) : env_value = - match ev with - | Var (name, v) -> Var (name, promote_in_value v) - | Abs abs -> - assert (config.mode = SymbolicMode); - Abs abs +let promote_inactivated_borrow_to_mut_borrow (l : BorrowId.id) + (borrowed_value : typed_value) (env : env) : env = + (* Lookup the inactivated borrow - note that we don't go inside borrows/loans: + there can't be inactivated borrows inside other borrows/loans + *) + let ek = + { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false } in - List.map promote_in_env_value env0 + match lookup_borrow ek l env with + | SharedBorrow _ | MutBorrow (_, _) -> + failwith "Expected an inactivated mutable borrow" + | InactivatedMutBorrow _ -> + (* Update it *) + update_borrow ek l (MutBorrow (l, borrowed_value)) env (** Promote an inactivated mut borrow to a mut borrow. @@ -604,11 +738,15 @@ let promote_inactivated_borrow_to_mut_borrow (config : config) (l : BorrowId.id) let rec activate_inactivated_mut_borrow (config : config) (io : inner_outer) (l : BorrowId.id) (env : env) : env = (* Lookup the value *) - match lookup_loan_from_borrow_id config l env with + let ek = + { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } + in + match lookup_loan ek l env with | MutLoan _ -> failwith "Unreachable" | SharedLoan (bids, sv) -> ( - (* If there is a borrow inside the value, end it. Also activate inactivated - loans. If we perform an update, do a recursive call to lookup the value *) + (* If there are loans inside the value, end them. Note that there can't be + inactivated borrows inside the value. + If we perform an update, do a recursive call to lookup the updated value *) match get_first_loan_in_value sv with | Some lc -> (* End the loans *) @@ -620,28 +758,32 @@ let rec activate_inactivated_mut_borrow (config : config) (io : inner_outer) (* Recursive call *) activate_inactivated_mut_borrow config io l env' | None -> + (* No loan to end inside the value *) (* Some sanity checks *) assert (not (loans_in_value sv)); assert (not (bottom_in_value sv)); - (* End the borrows which borrow from the value, at the exception of the borrow - * we want to promote *) + let check_not_inactivated bc = + match bc with InactivatedMutBorrow _ -> false | _ -> true + in + assert (not (check_borrows_in_value check_not_inactivated sv)); + (* 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 io bids env in + let env1 = end_borrows config io bids env in (* Promote the loan *) - let borrowed_value, env'' = - promote_shared_loan_to_mut_loan config l env' - in - (* Promote the borrow *) - promote_inactivated_borrow_to_mut_borrow config l borrowed_value env'' - ) + let env2, borrowed_value = promote_shared_loan_to_mut_loan l env1 in + (* Promote the borrow - the value should have been checked by + [promote_shared_loan_to_mut_loan] + *) + promote_inactivated_borrow_to_mut_borrow l borrowed_value env2) +(* (** Paths *) type access_kind = - | Read (** Read a value *) - | Write - (** Update a value (but don't replace it with [Bottom] or values containing [Bottom] *) - | Move (** Replace a value with [Bottom] *) + | Read (** We can go inside borrows and loans *) + | Write (** Don't enter shared borrows or shared loans *) + | Move (** Don't enter borrows or loans *) (** When we fail reading from or writing to a path, it might be because we ** need to update the environment by ending borrows, expanding symbolic @@ -705,9 +847,120 @@ let lookup_shared_value_from_borrow_id (bid : BorrowId.id) (env : env) : | None -> failwith "Unreachable" | Some v -> v -(** Read the value at the end of a projection *) +type updated_read_value = { read : typed_value; updated : typed_value } + +(* +(** Generic function to access (read/write) the value at the end of a projection. + + We return the eventually updated value, and the value we read at the end of + the place. + *) +let rec access_projection (config : config) (access : access_kind) (env : env) + (* Function to (eventually) update the value we find *) + (update : typed_value -> typed_value) (p : projection) (v : typed_value) : + updated_read_value path_access_result = + match p with + | [] -> Ok { read = v; updated = update v } + | pe :: p' -> ( + (* The projection is non-empty: we need to enter all the loans we find, + * if we are allowed to do so *) + let rec enter_loans (v : typed_value) : typed_value path_access_result = + match v.value with + | Loan lc -> ( + match (access, lc) with + (* We can enter shared loans only if we are in "read" mode *) + | Read, SharedLoan (_, sv) -> enter_loans sv + | (Write | Move), SharedLoan (bids, _) -> + Error (FailSharedLoan bids) + (* We always have to end mutable loans *) + | _, MutLoan bid -> Error (FailMutLoan bid)) + | _ -> Ok v + in + (* Enter inside the loans and match on the resulting value *) + match enter_loans v with + | Ok v -> ( + (* Match on the projection element and the value *) + match (pe, v.value) with + (* Field projection *) + | Field (ProjAdt (_def_id, opt_variant_id), field_id), Adt adt -> ( + (* Check that the projection is consistent with the current value *) + (match (opt_variant_id, adt.variant_id) with + | None, None -> () + | Some vid, Some vid' -> + if vid <> vid' then failwith "Unreachable" + | _ -> failwith "Unreachable"); + (* Actually project *) + let fv = FieldId.nth adt.field_values field_id in + match access_projection config access env p fv with + | Error err -> Error err + | Ok res -> + (* Update the field value *) + let nvalues = + FieldId.update_nth adt.field_values field_id res.updated + in + let nadt = Adt { adt with field_values = nvalues } in + let updated = { v with value = nadt } in + Ok { res with updated }) + (* Tuples *) + | Field (ProjTuple _, field_id), Tuple values -> ( + let fv = FieldId.nth values field_id in + (* Project *) + match access_projection config access env p fv with + | Error err -> Error err + | Ok res -> + (* Update the field value *) + let nvalues = + FieldId.update_nth values field_id res.updated + in + let ntuple = Tuple nvalues in + let updated = { v with value = ntuple } in + Ok { res with updated }) + (* We can expand [Bottom] values only while *writing* to places *) + | _, Bottom -> failwith "Unreachable" + (* Symbolic value: needs to be expanded *) + | _, Symbolic sp -> + assert (config.mode = SymbolicMode); + (* Expand the symbolic value *) + Error (FailSymbolic (pe, sp)) + (* Box dereferencement *) + | DerefBox, Assumed (Box bv) -> ( + (* We allow moving inside of boxes *) + match access_projection config access env p' bv with + | Error err -> err + | Ok res -> + let nv = { v with value = Assumed (Box res.updated) } in + { res with updated = nv }) + (* Borrow dereferencement *) + | Deref, Borrow bc -> ( + match (access, bc) with + | Read, SharedBorrow bid -> + let sv = lookup_shared_value_from_borrow_id bid env in + (match access_projection config access env p' sv with + | Error err -> Error err + | Ok res -> + let nv = { v with value = Borrow (SharedBorrow + ) + | Write, SharedBorrow _ -> + failwith "Can't write to a shared borrow" + | (Read | Write), MutBorrow (_, bv) -> + access_projection config access env p' bv + | Move, _ -> failwith "Can't move out of a borrow" + (* We need to activate inactivated mutable borrows *) + | _, InactivatedMutBorrow bid -> + Error (FailInactivatedMutBorrow bid)) + (* Remaining cases: error. We enumerate all the value variants + * on purpose, to make sure we statically catch errors if we + * modify the [value] definition. *) + | _, (Concrete _ | Adt _ | Tuple _ | Assumed _ | Borrow _) -> + failwith "Unreachable") + (* Entering loans failed *) + | res -> res) + *) + +(** Read the value at the end of a projection. *) let rec read_projection (config : config) (access : access_kind) (env : env) - (p : projection) (v : typed_value) : typed_value path_access_result = + (p : projection) (v : typed_value) : + (typed_value * typed_value) path_access_result = match p with | [] -> Ok v | pe :: p' -> ( @@ -791,11 +1044,26 @@ let read_place (config : config) (access : access_kind) (p : place) (env0 : env) read_in_env env0 (** Update the value at the end of a projection. *) -let rec write_projection (config : config) (new_value : typed_value) - (p : projection) (v : typed_value) : typed_value path_access_result = +let rec write_projection (config : config) (access : access_kind) + (new_value : typed_value) (p : projection) (v : typed_value) : + typed_value path_access_result = match p with | [] -> Ok v | pe :: p' -> ( + (* The projection is non-empty: we need to enter all the loans we find, + * if we are allowed to do so *) + let rec enter_loans (v : typed_value) : typed_value path_access_result = + match v.value with + | Loan lc -> ( + match (access, lc) with + (* We can enter shared loans only if we are in "read" mode *) + | Read, SharedLoan (_, sv) -> enter_loans sv + | (Write | Move), SharedLoan (bids, _) -> + Error (FailSharedLoan bids) + (* We always have to end mutable loans *) + | _, MutLoan bid -> Error (FailMutLoan bid)) + | _ -> Ok v + in (* Match on the projection element and the value *) match (pe, v.value) with (* Field projection *) @@ -866,11 +1134,12 @@ let rec write_projection (config : config) (new_value : typed_value) (** Update the value at the end of a place. - We don't specify the access kind, because it should have been specified in - a prior access check with [read_place]. + Note that the usage of this function is very general: it can be used to + update a place when evaluating an assignment, or to update the set of + borrows pointing to the same shared value, etc. *) -let write_place (config : config) (nv : typed_value) (p : place) (env0 : env) : - env path_access_result = +let write_place (config : config) (access : access_kind) (nv : typed_value) + (p : place) (env0 : env) : env path_access_result = let rec write_in_env env : env path_access_result = match env with | [] -> failwith "Unreachable" @@ -1358,3 +1627,4 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) : (* TODO: update write_value *) + *) diff --git a/src/Print.ml b/src/Print.ml index ea368bd3..4b46914f 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -452,8 +452,8 @@ module Contexts = struct let frame_to_string (fmt : ctx_formatter) (ctx : eval_ctx) (frame : stack_frame) : string = let var_binding_to_string (vid : VarId.id) : string = - let var = lookup_var ctx vid in - let v = lookup_var_value ctx vid in + let var = ctx_lookup_var ctx vid in + let v = ctx_lookup_var_value ctx vid in let var_name = match var.name with Some name -> "(" ^ name ^ ")" | None -> "" in -- cgit v1.2.3