diff options
author | Son Ho | 2022-01-13 20:53:20 +0100 |
---|---|---|
committer | Son Ho | 2022-01-13 20:53:20 +0100 |
commit | 8dfe03ed7c23ecec2844287c341be9d745c2ebb2 (patch) | |
tree | 074cddd0a5bc2153b89706a016cd05af2e64348a /src/InterpreterStatements.ml | |
parent | d673cdc47a0b948871ac939075411be0929399c9 (diff) |
Make more updates to assignment and update ctx_pop_frame
Diffstat (limited to '')
-rw-r--r-- | src/InterpreterStatements.ml | 42 |
1 files changed, 38 insertions, 4 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index de904262..d172d1b7 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -51,8 +51,12 @@ let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) let ctx, v = C.ctx_pop_dummy_var ctx in (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) assert (not (bottom_in_value ctx.ended_regions v)); + (* Move the value at destination to a dummy variable *) + let mv = read_place_unwrap config Write p ctx in + let ctx = C.ctx_push_dummy_var ctx mv in (* Update the destination *) let ctx = write_place_unwrap config Write p v ctx in + (* Return *) ctx (** Evaluates an assertion. @@ -193,11 +197,41 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) : in (* Sanity check *) assert (not (bottom_in_value ctx.ended_regions ret_value)); - (* We musn't drop the local variables (because otherwise we might end - * some borrows in the return value!) but must reintroduce them instead - * in the context as dummy variables. *) + (* List the local variables, but the return variable *) + let rec list_locals env = + match env with + | [] -> failwith "Inconsistent environment" + | C.Abs _ :: env -> list_locals env + | C.Var (None, _) :: env -> list_locals env + | C.Var (Some var, _) :: env -> + let locals = list_locals env in + if var.index <> ret_vid then var.index :: locals else locals + | C.Frame :: _ -> [] + in + let locals = list_locals ctx.env in + (* Debug *) + log#ldebug + (lazy + ("ctx_pop_frame: locals in which to drop the outer loans: [" + ^ String.concat "," (List.map V.VarId.to_string locals) + ^ "]")); + (* Drop the outer *loans* in the local variables *) + let ctx = + let end_borrows = false in + List.fold_left + (fun ctx lid -> + drop_outer_borrows_loans_at_lplace config end_borrows + (mk_place_from_var_id lid) ctx) + ctx locals + in + (* Debug *) + log#ldebug + (lazy + ("ctx_pop_frame: after dropping outer loans in local variables:\n" + ^ eval_ctx_to_string ctx)); (* Pop the frame - we remove the `Frame` delimiter, and reintroduce all - * the local variables as dummy variables in the caller frame *) + * the local variables (which may still contain borrow permissions - but + * no outer loans - as dummy variables in the caller frame *) let rec pop env = match env with | [] -> failwith "Inconsistent environment" |