From 2bd4d1ca30dd0b5a22250f86bbac3cd84f33b053 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 25 Nov 2021 15:01:15 +0100 Subject: Replace `open Contexts` by `module C = Contexts` in Interpreter.ml --- src/Interpreter.ml | 246 +++++++++++++++++++++++------------------------------ 1 file changed, 108 insertions(+), 138 deletions(-) (limited to 'src/Interpreter.ml') diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 25ba60f5..ce003e71 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -3,8 +3,9 @@ open Values open Scalars open Expressions open Errors -open Contexts +module C = Contexts module Subst = Substitute +module A = CfimAst (* TODO: Change state-passing style to : st -> ... -> (st, v) *) (* TODO: check that the value types are correct when evaluating *) @@ -90,9 +91,9 @@ let rec lookup_loan_in_value (ek : exploration_kind) (l : BorrowId.id) The loan is referred to by a borrow id. *) -let lookup_loan (ek : exploration_kind) (l : BorrowId.id) (env : env) : +let lookup_loan (ek : exploration_kind) (l : BorrowId.id) (env : C.env) : loan_content = - let lookup_loan_in_env_value (ev : env_value) : loan_content option = + let lookup_loan_in_env_value (ev : C.env_value) : loan_content option = match ev with | Var (_, v) -> lookup_loan_in_value ek l v | Abs _ -> raise Unimplemented @@ -152,8 +153,8 @@ let rec update_loan_in_value (ek : exploration_kind) (l : BorrowId.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 = + (env : C.env) : C.env = + let update_loan_in_env_value (ev : C.env_value) : C.env_value = match ev with | Var (vid, v) -> Var (vid, update_loan_in_value ek l nlc v) | Abs _ -> raise Unimplemented @@ -188,9 +189,9 @@ let rec lookup_borrow_in_value (ek : exploration_kind) (l : BorrowId.id) | MutLoan _ -> None) (** Lookup a borrow content from a borrow id. *) -let lookup_borrow (ek : exploration_kind) (l : BorrowId.id) (env : env) : +let lookup_borrow (ek : exploration_kind) (l : BorrowId.id) (env : C.env) : borrow_content = - let lookup_borrow_in_env_value (ev : env_value) = + let lookup_borrow_in_env_value (ev : C.env_value) = match ev with | Var (_, v) -> lookup_borrow_in_value ek l v | Abs _ -> raise Unimplemented @@ -251,8 +252,8 @@ let rec update_borrow_in_value (ek : exploration_kind) (l : BorrowId.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 = + (nbc : borrow_content) (env : C.env) : C.env = + let update_borrow_in_env_value (ev : C.env_value) : C.env_value = match ev with | Var (vid, v) -> Var (vid, update_borrow_in_value ek l nbc v) | Abs _ -> raise Unimplemented @@ -445,17 +446,17 @@ and end_borrow_get_borrow_in_values config io l outer_borrows vl0 : borrows, we end them, and finally we end the borrow we wanted to end in the first place. *) -let rec end_borrow_get_borrow_in_env (config : config) (io : inner_outer) l env0 - : env * borrow_lres = +let rec end_borrow_get_borrow_in_env (config : C.config) (io : inner_outer) l + env0 : C.env * borrow_lres = match env0 with | [] -> ([], NotFound) - | Var (x, v) :: env -> ( + | C.Var (x, v) :: env -> ( match end_borrow_get_borrow_in_value config io l None v with | v', NotFound -> let env', res = end_borrow_get_borrow_in_env config io l env in (Var (x, v') :: env', res) | v', res -> (Var (x, v') :: env, res)) - | Abs _ :: _ -> + | C.Abs _ :: _ -> assert (config.mode = SymbolicMode); raise Unimplemented @@ -501,13 +502,13 @@ let rec give_back_value_to_value config bid (v : typed_value) if bid' = bid then v else { destv with value = Loan (MutLoan bid') }) (** See [give_back_value]. *) -let give_back_value_to_abs (_config : config) _bid _v _abs : abs = +let give_back_value_to_abs (_config : C.config) _bid _v _abs : abs = (* TODO *) raise Unimplemented (** See [give_back_shared]. *) -let rec give_back_shared_to_value (config : config) bid (destv : typed_value) : - typed_value = +let rec give_back_shared_to_value (config : C.config) bid (destv : typed_value) + : typed_value = match destv.value with | Concrete _ | Bottom | Symbolic _ -> destv | Adt av -> @@ -571,14 +572,15 @@ let give_back_shared_to_abs _config _bid _abs : abs = When we end a mutable borrow, we need to "give back" the value it contained to its original owner by reinserting it at the proper position. *) -let give_back_value (config : config) (bid : BorrowId.id) (v : typed_value) - (env : env) : env = - let give_back_value_to_env_value ev : env_value = +let give_back_value (config : C.config) (bid : BorrowId.id) (v : typed_value) + (env : C.env) : C.env = + let give_back_value_to_env_value ev : C.env_value = match ev with - | Var (vid, destv) -> Var (vid, give_back_value_to_value config bid v destv) - | Abs abs -> + | C.Var (vid, destv) -> + C.Var (vid, give_back_value_to_value config bid v destv) + | C.Abs abs -> assert (config.mode = SymbolicMode); - Abs (give_back_value_to_abs config bid v abs) + C.Abs (give_back_value_to_abs config bid v abs) in List.map give_back_value_to_env_value env @@ -587,13 +589,14 @@ let give_back_value (config : config) (bid : BorrowId.id) (v : typed_value) When we end a shared borrow, we need to remove the borrow id from the list of borrows to the shared value. *) -let give_back_shared config (bid : BorrowId.id) (env : env) : env = - let give_back_shared_to_env_value ev : env_value = +let give_back_shared config (bid : BorrowId.id) (env : C.env) : C.env = + let give_back_shared_to_env_value ev : C.env_value = match ev with - | Var (vid, destv) -> Var (vid, give_back_shared_to_value config bid destv) - | Abs abs -> + | C.Var (vid, destv) -> + C.Var (vid, give_back_shared_to_value config bid destv) + | C.Abs abs -> assert (config.mode = SymbolicMode); - Abs (give_back_shared_to_abs config bid abs) + C.Abs (give_back_shared_to_abs config bid abs) in List.map give_back_shared_to_env_value env @@ -602,8 +605,8 @@ let give_back_shared config (bid : BorrowId.id) (env : env) : env = to an environment by inserting a new borrow id in the set of borrows tracked by a shared value, referenced by the [original_bid] argument. *) -let reborrow_shared (config : config) (original_bid : BorrowId.id) - (new_bid : BorrowId.id) (env : env) : env = +let reborrow_shared (config : C.config) (original_bid : BorrowId.id) + (new_bid : BorrowId.id) (env : C.env) : C.env = let rec reborrow_in_value (v : typed_value) : typed_value = match v.value with | Concrete _ | Bottom | Symbolic _ -> v @@ -637,12 +640,12 @@ let reborrow_shared (config : config) (original_bid : BorrowId.id) else { v with value = Loan (SharedLoan (bids, reborrow_in_value sv)) }) in - let reborrow_in_ev (ev : env_value) : env_value = + let reborrow_in_ev (ev : C.env_value) : C.env_value = match ev with - | Var (vid, v) -> Var (vid, reborrow_in_value v) - | Abs abs -> + | C.Var (vid, v) -> C.Var (vid, reborrow_in_value v) + | C.Abs abs -> assert (config.mode = SymbolicMode); - Abs abs + C.Abs abs in List.map reborrow_in_ev env @@ -652,8 +655,8 @@ let reborrow_shared (config : config) (original_bid : BorrowId.id) then update the loan. Ends outer borrows before updating the borrow if it is necessary. *) -let rec end_borrow (config : config) (io : inner_outer) (l : BorrowId.id) - (env0 : env) : env = +let rec end_borrow (config : C.config) (io : inner_outer) (l : BorrowId.id) + (env0 : C.env) : C.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 *) @@ -674,8 +677,8 @@ let rec end_borrow (config : config) (io : inner_outer) (l : BorrowId.id) (* If found shared or inactivated mut: remove the borrow id from the loan set of the shared value *) | env, (FoundShared | FoundInactivatedMut) -> give_back_shared config l env -and end_borrows (config : config) (io : inner_outer) (lset : BorrowId.Set.t) - (env0 : env) : env = +and end_borrows (config : C.config) (io : inner_outer) (lset : BorrowId.Set.t) + (env0 : C.env) : C.env = BorrowId.Set.fold (fun id env -> end_borrow config io id env) lset env0 let end_outer_borrow config = end_borrow config Outer @@ -700,8 +703,8 @@ let end_inner_borrows config = end_borrows config Inner TODO: this kind of checks should be put in an auxiliary helper, because they are redundant *) -let promote_shared_loan_to_mut_loan (l : BorrowId.id) (env : env) : - env * typed_value = +let promote_shared_loan_to_mut_loan (l : BorrowId.id) (env : C.env) : + C.env * typed_value = (* Lookup the shared loan *) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } @@ -727,7 +730,7 @@ let promote_shared_loan_to_mut_loan (l : BorrowId.id) (env : env) : This function updates a shared borrow to a mutable borrow. *) let promote_inactivated_borrow_to_mut_borrow (l : BorrowId.id) - (borrowed_value : typed_value) (env : env) : env = + (borrowed_value : typed_value) (env : C.env) : C.env = (* Lookup the inactivated borrow - note that we don't go inside borrows/loans: there can't be inactivated borrows inside other borrows/loans *) @@ -745,8 +748,8 @@ let promote_inactivated_borrow_to_mut_borrow (l : BorrowId.id) The borrow must point to a shared value which is borrowed exactly once. *) -let rec activate_inactivated_mut_borrow (config : config) (io : inner_outer) - (l : BorrowId.id) (env : env) : env = +let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) + (l : BorrowId.id) (env : C.env) : C.env = (* Lookup the value *) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } @@ -819,40 +822,6 @@ type path_fail_kind = type 'a path_access_result = ('a, path_fail_kind) result (** The result of reading from/writing to a place *) -(*(** Return the shared value referenced by a borrow id *) -let lookup_shared_value_from_borrow_id (bid : BorrowId.id) (env : env) : - typed_value = - let rec lookup_in_value (v : 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 - lookup_in_values values - | Tuple values -> - let values = FieldId.vector_to_list values in - lookup_in_values values - | Borrow bc -> ( - match bc with - | SharedBorrow _ | InactivatedMutBorrow _ -> None - | MutBorrow (_, bv) -> lookup_in_value bv) - | Loan lc -> ( - match lc with - | SharedLoan (bids, sv) -> - if BorrowId.Set.mem bid bids then Some v else lookup_in_value sv - | MutLoan _ -> None) - | Assumed (Box bv) -> lookup_in_value bv - and lookup_in_values (vl : typed_value list) : typed_value option = - List.find_map lookup_in_value vl - in - let lookup_in_env_value (ev : env_value) : typed_value option = - match ev with - | Var (_, v) -> lookup_in_value v - | Abs _ -> raise Unimplemented - in - match List.find_map lookup_in_env_value env with - | None -> failwith "Unreachable" - | Some v -> v*) - type updated_read_value = { read : typed_value; updated : typed_value } type projection_access = { @@ -866,10 +835,10 @@ type projection_access = { We return the (eventually) updated value, the value we read at the end of the place and the (eventually) updated environment. *) -let rec access_projection (access : projection_access) (env : env) +let rec access_projection (access : projection_access) (env : C.env) (* Function to (eventually) update the value we find *) (update : typed_value -> typed_value) (p : projection) (v : typed_value) : - (env * updated_read_value) path_access_result = + (C.env * updated_read_value) path_access_result = (* For looking up/updating shared loans *) let ek : exploration_kind = { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } @@ -992,16 +961,16 @@ let rec access_projection (access : projection_access) (env : env) *) let access_place (access : projection_access) (* Function to (eventually) update the value we find *) - (update : typed_value -> typed_value) (p : place) (env : env) : - (env * typed_value) path_access_result = + (update : typed_value -> typed_value) (p : place) (env : C.env) : + (C.env * typed_value) path_access_result = (* Lookup the variable's value *) - let value = env_lookup_var_value env p.var_id in + let value = C.env_lookup_var_value env p.var_id in (* Apply the projection *) match access_projection access env update p.projection value with | Error err -> Error err | Ok (env1, res) -> (* Update the value *) - let env2 = env_update_var_value env1 p.var_id res.updated in + let env2 = C.env_update_var_value env1 p.var_id res.updated in (* Return *) Ok (env2, res.read) @@ -1033,8 +1002,8 @@ let access_kind_to_projection_access (access : access_kind) : projection_access } (** Read the value at a given place *) -let read_place (config : config) (access : access_kind) (p : place) (env : env) - : typed_value path_access_result = +let read_place (config : C.config) (access : access_kind) (p : place) + (env : C.env) : typed_value path_access_result = let access = access_kind_to_projection_access access in (* The update function is the identity *) let update v = v in @@ -1047,15 +1016,15 @@ let read_place (config : config) (access : access_kind) (p : place) (env : env) if config.check_invariants then assert (env1 = env); Ok read_value -let read_place_unwrap (config : config) (access : access_kind) (p : place) - (env : env) : typed_value = +let read_place_unwrap (config : C.config) (access : access_kind) (p : place) + (env : C.env) : typed_value = match read_place config access p env with | Error _ -> failwith "Unreachable" | Ok v -> v (** Update the value at a given place *) -let write_place (_config : config) (access : access_kind) (p : place) - (nv : typed_value) (env : env) : env path_access_result = +let write_place (_config : C.config) (access : access_kind) (p : place) + (nv : typed_value) (env : C.env) : C.env path_access_result = let access = access_kind_to_projection_access access in (* The update function substitutes the value with the new value *) let update _ = nv in @@ -1065,8 +1034,8 @@ let write_place (_config : config) (access : access_kind) (p : place) (* We ignore the read value *) Ok env1 -let write_place_unwrap (config : config) (access : access_kind) (p : place) - (nv : typed_value) (env : env) : env = +let write_place_unwrap (config : C.config) (access : access_kind) (p : place) + (nv : typed_value) (env : C.env) : C.env = match write_place config access p nv env with | Error _ -> failwith "Unreachable" | Ok env -> env @@ -1092,9 +1061,9 @@ let write_place_unwrap (config : config) (access : access_kind) (p : place) about which variant we should project to, which is why we *can* set the variant index when writing one of its fields). *) -let expand_bottom_value (config : config) (access : access_kind) +let expand_bottom_value (config : C.config) (access : access_kind) (tyctx : type_def TypeDefId.vector) (p : place) (remaining_pes : int) - (pe : projection_elem) (ty : ety) (env : env) : env = + (pe : projection_elem) (ty : ety) (env : C.env) : C.env = (* Prepare the update: we need to take the proper prefix of the place during whose evaluation we got stuck *) let projection' = @@ -1168,8 +1137,8 @@ let expand_bottom_value (config : config) (access : access_kind) uses this information to update the environment (by ending borrows, expanding symbolic values) until we manage to fully read the place. *) -let rec update_env_along_read_place (config : config) (access : access_kind) - (p : place) (env : env) : env = +let rec update_env_along_read_place (config : C.config) (access : access_kind) + (p : place) (env : C.env) : C.env = (* Attempt to read the place: if it fails, update the environment and retry *) match read_place config access p env with | Ok _ -> env @@ -1194,9 +1163,9 @@ let rec update_env_along_read_place (config : config) (access : access_kind) See [update_env_alond_read_place]. *) -let rec update_env_along_write_place (config : config) (access : access_kind) +let rec update_env_along_write_place (config : C.config) (access : access_kind) (tyctx : type_def TypeDefId.vector) (p : place) (nv : typed_value) - (env : env) : env = + (env : C.env) : C.env = (* Attempt to write the place: if it fails, update the environment and retry *) match write_place config access p nv env with | Ok env' -> env' @@ -1217,7 +1186,7 @@ let rec update_env_along_write_place (config : config) (access : access_kind) in update_env_along_write_place config access tyctx p nv env' -exception UpdateEnv of env +exception UpdateEnv of C.env (** Small utility used to break control-flow *) (** Collect the borrows at a given place (by ending borrows when we find some @@ -1227,8 +1196,8 @@ exception UpdateEnv of env first call [update_env_along_read_place] or [update_env_along_write_place] to get access to the value, then call this function to "prepare" the value. *) -let rec collect_borrows_at_place (config : config) (access : access_kind) - (p : place) (env : env) : env = +let rec collect_borrows_at_place (config : C.config) (access : access_kind) + (p : place) (env : C.env) : C.env = (* First, retrieve the value *) match read_place config access p env with | Error _ -> failwith "Unreachable" @@ -1299,7 +1268,8 @@ let rec collect_borrows_at_place (config : config) (access : access_kind) drop the value there to properly propagate back values which are not/can't be borrowed anymore). *) -let rec drop_borrows_at_place (config : config) (p : place) (env : env) : env = +let rec drop_borrows_at_place (config : C.config) (p : place) (env : C.env) : + C.env = (* We do something similar to [collect_borrows_at_place]. First, retrieve the value *) match read_place config Write p env with @@ -1391,8 +1361,8 @@ let rec drop_borrows_at_place (config : config) (p : place) (env : env) : env = Note that copying values might update the context. For instance, when copying shared borrows, we need to insert new shared borrows in the context. *) -let rec copy_value (config : config) (ctx : eval_ctx) (v : typed_value) : - eval_ctx * typed_value = +let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : typed_value) : + C.eval_ctx * typed_value = match v.value with | Values.Concrete _ -> (ctx, v) | Values.Adt av -> @@ -1411,7 +1381,7 @@ let rec copy_value (config : config) (ctx : eval_ctx) (v : typed_value) : (* We can only copy shared borrows *) match bc with | SharedBorrow bid -> - let ctx', bid' = fresh_borrow_id ctx in + let ctx', bid' = C.fresh_borrow_id ctx in let env'' = reborrow_shared config bid bid' ctx'.env in let ctx'' = { ctx' with env = env'' } in (ctx'', { v with value = Values.Borrow (SharedBorrow bid') }) @@ -1428,7 +1398,7 @@ let rec copy_value (config : config) (ctx : eval_ctx) (v : typed_value) : raise Unimplemented (** Convert a constant operand value to a typed value *) -let constant_value_to_typed_value (ctx : eval_ctx) (ty : ety) +let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : ety) (cv : operand_constant_value) : typed_value = (* Check the type while converting *) match (ty, cv) with @@ -1480,8 +1450,8 @@ let constant_value_to_typed_value (ctx : eval_ctx) (ty : ety) failwith "Improperly typed constant value" (** Small utility *) -let prepare_rplace (config : config) (access : access_kind) (p : place) - (ctx : eval_ctx) : eval_ctx * typed_value = +let prepare_rplace (config : C.config) (access : access_kind) (p : place) + (ctx : C.eval_ctx) : C.eval_ctx * typed_value = let env1 = update_env_along_read_place config access p ctx.env in let env2 = collect_borrows_at_place config access p env1 in let v = read_place_unwrap config access p env2 in @@ -1501,8 +1471,8 @@ let prepare_rplace (config : config) (access : access_kind) (p : place) - [eval_operand_apply] which are then used in [eval_operand] and [eval_operands]. *) -let eval_operand_prepare (config : config) (ctx : eval_ctx) (op : operand) : - eval_ctx = +let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : operand) : + C.eval_ctx = match op with | Expressions.Constant (_, _) -> ctx (* nothing to do *) | Expressions.Copy p -> @@ -1513,8 +1483,8 @@ let eval_operand_prepare (config : config) (ctx : eval_ctx) (op : operand) : fst (prepare_rplace config access p ctx) (** See [eval_operand_prepare] (which should have been called before) *) -let eval_operand_apply (config : config) (ctx : eval_ctx) (op : operand) : - eval_ctx * typed_value = +let eval_operand_apply (config : C.config) (ctx : C.eval_ctx) (op : operand) : + C.eval_ctx * typed_value = match op with | Expressions.Constant (ty, cv) -> let v = constant_value_to_typed_value ctx ty cv in @@ -1546,16 +1516,16 @@ let eval_operand_apply (config : config) (ctx : eval_ctx) (op : operand) : Otherwise, we may break invariants (if some values refer to other values via borrows). *) -let eval_operand (config : config) (ctx : eval_ctx) (op : operand) : - eval_ctx * typed_value = +let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : operand) : + C.eval_ctx * typed_value = let ctx1 = eval_operand_prepare config ctx op in eval_operand_apply config ctx1 op (** Evaluate several operands. *) -let eval_operands (config : config) (ctx : eval_ctx) (ops : operand list) : - eval_ctx * typed_value list = +let eval_operands (config : C.config) (ctx : C.eval_ctx) (ops : operand list) : + C.eval_ctx * typed_value list = (* First prepare the values to end/activate the borrows *) let ctx1 = List.fold_left (fun ctx op -> eval_operand_prepare config ctx op) ctx ops @@ -1563,14 +1533,14 @@ let eval_operands (config : config) (ctx : eval_ctx) (ops : operand list) : (* Then actually apply the operands to move, borrow, copy... *) List.fold_left_map (fun ctx op -> eval_operand_apply config ctx op) ctx1 ops -let eval_two_operands (config : config) (ctx : eval_ctx) (op1 : operand) - (op2 : operand) : eval_ctx * typed_value * typed_value = +let eval_two_operands (config : C.config) (ctx : C.eval_ctx) (op1 : operand) + (op2 : operand) : C.eval_ctx * typed_value * typed_value = match eval_operands config ctx [ op1; op2 ] with | ctx', [ v1; v2 ] -> (ctx', v1, v2) | _ -> failwith "Unreachable" -let eval_unary_op (config : config) (ctx : eval_ctx) (unop : unop) - (op : operand) : (eval_ctx * typed_value) eval_result = +let eval_unary_op (config : C.config) (ctx : C.eval_ctx) (unop : unop) + (op : operand) : (C.eval_ctx * typed_value) eval_result = (* Evaluate the operand *) let ctx1, v = eval_operand config ctx op in (* Apply the unop *) @@ -1585,8 +1555,8 @@ let eval_unary_op (config : config) (ctx : eval_ctx) (unop : unop) | (Not | Neg), Symbolic _ -> raise Unimplemented (* TODO *) | _ -> failwith "Invalid value for unop" -let eval_binary_op (config : config) (ctx : eval_ctx) (binop : binop) - (op1 : operand) (op2 : operand) : (eval_ctx * typed_value) eval_result = +let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : binop) + (op1 : operand) (op2 : operand) : (C.eval_ctx * typed_value) eval_result = (* Evaluate the operands *) let ctx2, v1, v2 = eval_two_operands config ctx op1 op2 in if @@ -1655,8 +1625,8 @@ let eval_binary_op (config : config) (ctx : eval_ctx) (binop : binop) (** Evaluate an rvalue in a given context: return the updated context and the computed value *) -let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) : - (eval_ctx * typed_value) eval_result = +let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : rvalue) : + (C.eval_ctx * typed_value) eval_result = match rvalue with | Use op -> Ok (eval_operand config ctx op) | Ref (p, bkind) -> ( @@ -1666,7 +1636,7 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) : let access = if bkind = Expressions.Shared then Read else Write in let ctx2, v = prepare_rplace config access p ctx in (* Compute the rvalue - simply a shared borrow with a fresh id *) - let ctx3, bid = fresh_borrow_id ctx2 in + let ctx3, bid = C.fresh_borrow_id ctx2 in let rv_ty = Types.Ref (Erased, v.ty, Shared) in let bc = if bkind = Expressions.Shared then SharedBorrow bid @@ -1694,7 +1664,7 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) : let access = Write in let ctx2, v = prepare_rplace config access p ctx in (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) - let ctx3, bid = fresh_borrow_id ctx2 in + let ctx3, bid = C.fresh_borrow_id ctx2 in let rv_ty = Types.Ref (Erased, v.ty, Mut) in let rv = { value = Borrow (MutBorrow (bid, v)); ty = rv_ty } in (* Compute the value with which to replace the value at place p *) @@ -1737,7 +1707,7 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) : Ok (ctx1, { value = Tuple values; ty = Types.Tuple tys }) | AggregatedAdt (def_id, opt_variant_id, regions, types) -> (* Sanity checks *) - let type_def = ctx_lookup_type_def ctx def_id in + let type_def = C.ctx_lookup_type_def ctx def_id in assert ( RegionVarId.length type_def.region_params = List.length regions); let expected_field_types = @@ -1761,17 +1731,17 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) : (** Result of evaluating a statement *) type statement_eval_res = Unit | Break of int | Continue of int | Panic -let rec eval_statement (ctx : eval_ctx) (st : statement) : - eval_ctx * statement_eval_res = +let rec eval_statement (ctx : C.eval_ctx) (st : A.statement) : + C.eval_ctx * statement_eval_res = match st with - | Assign (p, rvalue) -> raise Unimplemented - | FakeRead p -> raise Unimplemented - | SetDiscriminant (p, variant_id) -> raise Unimplemented - | Drop p -> raise Unimplemented - | Assert assertion -> raise Unimplemented - | Call call -> raise Unimplemented - | Panic -> raise Unimplemented - | Return -> raise Unimplemented - | Break i -> raise Unimplemented - | Continue -> raise Unimplemented - | Nop -> (ctx, Unit) + | A.Assign (p, rvalue) -> raise Unimplemented + | A.FakeRead p -> raise Unimplemented + | A.SetDiscriminant (p, variant_id) -> raise Unimplemented + | A.Drop p -> raise Unimplemented + | A.Assert assertion -> raise Unimplemented + | A.Call call -> raise Unimplemented + | A.Panic -> raise Unimplemented + | A.Return -> raise Unimplemented + | A.Break i -> raise Unimplemented + | A.Continue i -> raise Unimplemented + | A.Nop -> (ctx, Unit) -- cgit v1.2.3