diff options
| -rw-r--r-- | src/Interpreter.ml | 50 |
1 files changed, 42 insertions, 8 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 3df2fe72..308a443b 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -978,7 +978,11 @@ let rec access_projection (access : projection_access) (env : C.env) Error (FailSymbolic (pe, sp)) (* Box dereferencement *) | DerefBox, Assumed (Box bv) -> ( - (* We allow moving inside of boxes *) + (* We allow moving inside of boxes. In practice, this kind of + * manipulations should happen only inside unsage code, so + * it shouldn't happen due to user code, and we leverage it + * when implementing box dereferencement for the concrete + * interpreter *) match access_projection access env update p' bv with | Error err -> Error err | Ok (env1, res) -> @@ -1996,16 +2000,49 @@ let eval_box_new (config : C.config) (region_params : T.erased_region list) Ok ctx | _ -> failwith "Inconsistent state" +let ty_is_boxed_ty (box_ty : T.ety) (boxed_ty : T.ety) : bool = + match box_ty with + | T.Assumed (T.Box, [], [ boxed_ty' ]) -> boxed_ty' = boxed_ty + | _ -> false + +(** Auxiliary function which factorizes code to evaluate `std::Deref::deref` + and `std::DerefMut::deref_mut` - see [eval_non_local_function_call] *) +let eval_box_deref_mut_or_shared (config : C.config) + (region_params : T.erased_region list) (type_params : T.ety list) + (is_mut : bool) (ctx : C.eval_ctx) : C.eval_ctx eval_result = + (* Check the arguments *) + match (region_params, type_params, ctx.env) with + | ( [], + [ boxed_ty ], + Var (input_var, input_value) :: Var (ret_var, _) :: C.Frame :: _ ) -> ( + (* Type checking *) + assert (ty_is_boxed_ty input_value.V.ty boxed_ty); + + (* Borrow the boxed value *) + let p = { E.var_id = input_var.V.index; projection = [ E.DerefBox ] } in + let borrow_kind = if is_mut then E.Mut else E.Shared in + let rv = E.Ref (p, borrow_kind) in + match eval_rvalue config ctx rv with + | Error err -> Error err + | Ok (ctx, borrowed_value) -> + (* Move the borrowed value to its destination *) + let destp = mk_place_from_var_id V.VarId.zero in + let ctx = assign_to_place config ctx borrowed_value destp in + Ok ctx) + | _ -> failwith "Inconsistent state" + (** Auxiliary function - see [eval_non_local_function_call] *) let eval_box_deref (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) (ctx : C.eval_ctx) : C.eval_ctx eval_result = - raise Unimplemented + let is_mut = false in + eval_box_deref_mut_or_shared config region_params type_params is_mut ctx (** Auxiliary function - see [eval_non_local_function_call] *) let eval_box_deref_mut (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) (ctx : C.eval_ctx) : C.eval_ctx eval_result = - raise Unimplemented + let is_mut = true in + eval_box_deref_mut_or_shared config region_params type_params is_mut ctx (** Auxiliary function - see [eval_non_local_function_call]. @@ -2017,13 +2054,10 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) (ctx : C.eval_ctx) : C.eval_ctx eval_result = match (region_params, type_params, ctx.env) with | ( [], - [ box_ty ], + [ boxed_ty ], Var (input_var, input_value) :: Var (ret_var, _) :: C.Frame :: _ ) -> (* Check the arguments *) - assert ( - match input_value.V.ty with - | T.Assumed (T.Box, [], [ boxed_ty ]) -> boxed_ty = input_value.V.ty - | _ -> false); + assert (ty_is_boxed_ty input_value.V.ty boxed_ty); (* Update the return value *) let dest = mk_place_from_var_id V.VarId.zero in |