diff options
| -rw-r--r-- | src/Contexts.ml | 13 | ||||
| -rw-r--r-- | src/Identifiers.ml | 2 | ||||
| -rw-r--r-- | src/Interpreter.ml | 97 |
3 files changed, 105 insertions, 7 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 7b9187bf..5e8ae3d0 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -186,6 +186,19 @@ let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx = let vars = List.map (fun v -> (v, mk_bottom v.var_ty)) vars in ctx_push_vars ctx vars +let env_lookup_abs (env : env) (abs_id : V.AbstractionId.id) : V.abs = + let rec lookup env = + match env with + | [] -> failwith "Unexpected" + | Var (_, _) :: env' -> lookup env' + | Abs abs :: env' -> if abs.abs_id = abs_id then abs else lookup env' + | Frame :: env' -> lookup env' + in + lookup env + +let ctx_lookup_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) : V.abs = + env_lookup_abs ctx.env abs_id + (** Visitor to iterate over the values in the *current* frame *) class ['self] iter_frame = object (self : 'self) diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 3c07b511..68a176bb 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -16,7 +16,7 @@ module type Id = sig val generator_zero : generator - (* TODO: this is stateful! - but we may want to be able to duplicated contexts... *) + (* TODO: this is stateful! - but we may want to be able to duplicate contexts... *) val fresh : generator -> id * generator val to_string : id -> string diff --git a/src/Interpreter.ml b/src/Interpreter.ml index eb2be68c..924c1b35 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -562,6 +562,8 @@ type inner_outer = Inner | Outer type borrow_ids = Borrows of V.BorrowId.Set.t | Borrow of V.BorrowId.id +exception FoundBorrowIds of borrow_ids + let update_if_none opt x = match opt with None -> Some x | _ -> opt (** Auxiliary function: see its usage in [end_borrow_get_borrow_in_value] *) @@ -1691,17 +1693,100 @@ and end_borrows (config : C.config) (io : inner_outer) (fun id ctx -> end_borrow config io allowed_abs id ctx) lset ctx -and end_abstraction (_config : C.config) (_abs : V.AbstractionId.id) - (_ctx : C.eval_ctx) : C.eval_ctx = +and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id) + (ctx : C.eval_ctx) : C.eval_ctx = + (* Lookup the abstraction *) + let abs = C.ctx_lookup_abs ctx abs_id in + (* End the parent abstractions first *) + let ctx = end_abstractions config abs.parents ctx in + (* End the loans inside the abstraction *) + let ctx = end_abstraction_loans config abs_id ctx in + (* End the abstraction itself by redistributing the borrows it contains *) + let ctx = end_abstraction_borrows config abs_id ctx in + (* End the regions owned by the abstraction *) + let ctx = end_abstraction_regions config abs_id ctx in + (* Remove all the references to the id of the current abstraction, and remove + * the abstraction itself *) + end_abstraction_remove_from_context config abs_id ctx + +and end_abstractions (config : C.config) (abs_ids : V.AbstractionId.set_t) + (ctx : C.eval_ctx) : C.eval_ctx = + V.AbstractionId.Set.fold + (fun id ctx -> end_abstraction config id ctx) + abs_ids ctx + +and end_abstraction_loans (config : C.config) (abs_id : V.AbstractionId.id) + (ctx : C.eval_ctx) : C.eval_ctx = + (* Lookup the abstraction *) + let abs = C.ctx_lookup_abs ctx abs_id in + (* End the first loan we find *) + let obj = + object + inherit [_] V.iter_abs as super + + method! visit_aloan_content env lc = + match lc with + | V.AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid)) + | V.ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids)) + | V.AEndedMutLoan { given_back; child } -> + super#visit_AEndedMutLoan env given_back child + | V.AEndedSharedLoan (v, av) -> super#visit_AEndedSharedLoan env v av + | V.AIgnoredMutLoan (bid, av) -> + (* Note that this loan might come from a child abstraction (it can't + * come from a parent abstraction, because we should have ended them + * already) *) + super#visit_AIgnoredMutLoan env bid av + | V.AEndedIgnoredMutLoan { given_back; child } -> + super#visit_AEndedIgnoredMutLoan env given_back child + | V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av + end + in + try + (* Check if there are loans *) + obj#visit_abs () abs; + (* No loans: nothing to update *) + ctx + with (* There are loans: end them, then recheck *) + | FoundBorrowIds bids -> + let ctx = + match bids with + | Borrow bid -> end_outer_borrow config bid ctx + | Borrows bids -> end_outer_borrows config bids ctx + in + (* Recheck *) + end_abstraction_loans config abs_id ctx + +and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) + (ctx : C.eval_ctx) : C.eval_ctx = + (* The abstraction mustn't contain any loans *) + raise Unimplemented + +and end_abstraction_regions (config : C.config) (abs_id : V.AbstractionId.id) + (ctx : C.eval_ctx) : C.eval_ctx = raise Unimplemented -let end_outer_borrow config = end_borrow config Outer None +(** Remove an abstraction from the context, as well as all its references *) +and end_abstraction_remove_from_context (_config : C.config) + (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx = + let map_env_elem (ev : C.env_elem) : C.env_elem option = + match ev with + | C.Var (_, _) | C.Frame -> Some ev + | C.Abs abs -> + if abs.abs_id = abs_id then None + else + let parents = V.AbstractionId.Set.remove abs_id abs.parents in + Some (C.Abs { abs with V.parents }) + in + let env = List.filter_map map_env_elem ctx.C.env in + { ctx with C.env } + +and end_outer_borrow config = end_borrow config Outer None -let end_outer_borrows config = end_borrows config Outer None +and end_outer_borrows config = end_borrows config Outer None -let end_inner_borrow config = end_borrow config Inner None +and end_inner_borrow config = end_borrow config Inner None -let end_inner_borrows config = end_borrows config Inner None +and end_inner_borrows config = end_borrows config Inner None (** Helper function: see [activate_inactivated_mut_borrow]. |