summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Contexts.ml45
-rw-r--r--src/InterpreterBorrowsCore.ml4
-rw-r--r--src/InterpreterStatements.ml15
-rw-r--r--src/InterpreterUtils.ml2
-rw-r--r--src/Print.ml4
5 files changed, 56 insertions, 14 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 0fe3a09a..d8ea9a3f 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -55,7 +55,13 @@ type binder = {
TODO: rename Var (-> Binding?)
*)
-type env_elem = Var of (binder[@opaque]) * typed_value | Abs of abs | Frame
+type env_elem =
+ | Var of (binder option[@opaque]) * typed_value
+ (** Variable binding - the binder is None if the variable is a dummy variable
+ (we use dummy variables to store temporaries while doing bookkeeping such
+ as ending borrows for instance). *)
+ | Abs of abs
+ | Frame
[@@deriving
show,
visitors
@@ -115,13 +121,17 @@ type eval_ctx = {
let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
TypeVarId.nth ctx.type_vars vid
+let opt_binder_has_vid (bv : binder option) (vid : VarId.id) : bool =
+ match bv with Some bv -> bv.index = vid | None -> false
+
let ctx_lookup_binder (ctx : eval_ctx) (vid : VarId.id) : binder =
(* TOOD: we might want to stop at the end of the frame *)
let rec lookup env =
match env with
| [] ->
raise (Invalid_argument ("Variable not found: " ^ VarId.to_string vid))
- | Var (var, _) :: env' -> if var.index = vid then var else lookup env'
+ | Var (var, _) :: env' ->
+ if opt_binder_has_vid var vid then Option.get var else lookup env'
| (Abs _ | Frame) :: env' -> lookup env'
in
lookup ctx.env
@@ -140,7 +150,8 @@ let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
let rec lookup env =
match env with
| [] -> failwith "Unexpected"
- | Var (var, v) :: env' -> if var.index = vid then v else lookup env'
+ | Var (var, v) :: env' ->
+ if opt_binder_has_vid var vid then v else lookup env'
| Abs _ :: env' -> lookup env'
| Frame :: _ -> failwith "End of frame"
in
@@ -163,7 +174,7 @@ let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env =
match env with
| [] -> failwith "Unexpected"
| Var (var, v) :: env' ->
- if var.index = vid then Var (var, nv) :: env'
+ if opt_binder_has_vid var vid then Var (var, nv) :: env'
else Var (var, v) :: update env'
| Abs abs :: env' -> Abs abs :: update env'
| Frame :: _ -> failwith "End of frame"
@@ -189,7 +200,7 @@ let ctx_update_var_value (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
assert (var.var_ty = v.ty);
let bv = var_to_binder var in
- { ctx with env = Var (bv, v) :: ctx.env }
+ { ctx with env = Var (Some bv, v) :: ctx.env }
(** Push a list of variables.
@@ -203,11 +214,29 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
(fun (var, (value : typed_value)) -> var.var_ty = value.ty)
vars);
let vars =
- List.map (fun (var, value) -> Var (var_to_binder var, value)) vars
+ List.map (fun (var, value) -> Var (Some (var_to_binder var), value)) vars
in
let vars = List.rev vars in
{ ctx with env = List.append vars ctx.env }
+(** Push a dummy variable in the context's environment. *)
+let ctx_push_dummy_var (ctx : eval_ctx) (v : typed_value) : eval_ctx =
+ { ctx with env = Var (None, v) :: ctx.env }
+
+(** Pop the first dummy variable from the context's environment. *)
+let ctx_pop_dummy_var (ctx : eval_ctx) : eval_ctx * typed_value =
+ let rec pop_var (env : env) : env * typed_value =
+ match env with
+ | [] -> failwith "Could not find a dummy variable"
+ | Var (None, v) :: env -> (env, v)
+ | ee :: env ->
+ let env, v = pop_var env in
+ (ee :: env, v)
+ in
+ let env, v = pop_var ctx.env in
+ ({ ctx with env }, v)
+
+(* TODO: move *)
let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty }
(** Push an uninitialized variable (which thus maps to [Bottom]) *)
@@ -237,7 +266,7 @@ class ['self] iter_frame =
object (self : 'self)
inherit [_] V.iter_abs
- method visit_Var : 'acc -> binder -> typed_value -> unit =
+ method visit_Var : 'acc -> binder option -> typed_value -> unit =
fun acc _vid v -> self#visit_typed_value acc v
method visit_Abs : 'acc -> abs -> unit =
@@ -265,7 +294,7 @@ class ['self] map_frame_concrete =
object (self : 'self)
inherit [_] V.map_abs
- method visit_Var : 'acc -> binder -> typed_value -> env_elem =
+ method visit_Var : 'acc -> binder option -> typed_value -> env_elem =
fun acc vid v ->
let v = self#visit_typed_value acc v in
Var (vid, v)
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index b590eff6..13ad8ee6 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -122,7 +122,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
method! visit_Var env bv v =
assert (Option.is_none !abs_or_var);
- abs_or_var := Some (VarId bv.C.index);
+ abs_or_var :=
+ Some
+ (VarId (match bv with Some bv -> Some bv.C.index | None -> None));
super#visit_Var env bv v;
abs_or_var := None
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
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index fd596fd3..a808e14c 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -105,7 +105,7 @@ type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs
type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs
(** Generic borrow content: concrete or abstract *)
-type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of V.VarId.id
+type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of V.VarId.id option
exception FoundBorrowContent of V.borrow_content
(** Utility exception *)
diff --git a/src/Print.ml b/src/Print.ml
index 5ae722b9..4dbe30f7 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -455,7 +455,9 @@ module Contexts = struct
(indent_incr : string) (ev : C.env_elem) : string =
match ev with
| Var (var, tv) ->
- indent ^ binder_to_string var ^ " -> "
+ indent
+ ^ option_to_string binder_to_string var
+ ^ " -> "
^ PV.typed_value_to_string fmt tv
^ " ;"
| Abs abs -> PV.abs_to_string fmt indent indent_incr abs
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 04:20:01 +0000