diff options
author | Son Ho | 2022-01-12 18:10:16 +0100 |
---|---|---|
committer | Son Ho | 2022-01-12 18:10:16 +0100 |
commit | 8cc257310c643e800b6bfcbc499fb253c817d3b7 (patch) | |
tree | 31588fa0be9f0fcbf557e0ff19ca21dd1af30a73 /src/InterpreterStatements.ml | |
parent | a84adca5d499a02c50b5510dd49dbbdf9c387018 (diff) |
Introduce dummy variables and update assign_to_place
Diffstat (limited to '')
-rw-r--r-- | src/InterpreterStatements.ml | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 38813894..0100a9c6 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -35,9 +35,14 @@ let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx (** Assign a value to a given place *) let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) (p : E.place) : C.eval_ctx = + (* Push the rvalue to a dummy variable, for bookkeeping *) + let ctx = C.ctx_push_dummy_var ctx v in (* Prepare the destination *) - (* TODO: there might be a problem because the value to assign is hanging in the air ! *) let ctx, _ = prepare_lplace config p ctx in + (* Retrieve the dummy variable *) + let ctx, v = C.ctx_pop_dummy_var ctx in + (* Checks *) + assert (not (bottom_in_value ctx.ended_regions v)); (* Update the destination *) let ctx = write_place_unwrap config Write p v ctx in ctx @@ -180,6 +185,8 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) : | [] -> failwith "Inconsistent environment" | C.Abs _ :: env -> list_locals env | C.Var (var, _) :: env -> + (* There shouldn't be dummy variables *) + let var = Option.get var in let locals = list_locals env in if var.index <> ret_vid then var.index :: locals else locals | C.Frame :: _ -> [] @@ -226,7 +233,8 @@ let eval_box_new_concrete (config : C.config) match (region_params, type_params, ctx.env) with | ( [], [ boxed_ty ], - Var (input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) -> + Var (Some input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) + -> (* Required type checking *) assert (input_value.V.ty = boxed_ty); @@ -260,7 +268,8 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config) match (region_params, type_params, ctx.env) with | ( [], [ boxed_ty ], - Var (input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) -> ( + Var (Some input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) + -> ( (* Required type checking. We must have: - input_value.ty == & (mut) Box<ty> - boxed_ty == ty |