diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Contexts.ml | 144 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml | 7 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 40 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 5 | ||||
| -rw-r--r-- | compiler/Print.ml | 26 | ||||
| -rw-r--r-- | compiler/SymbolicAst.ml | 2 | ||||
| -rw-r--r-- | compiler/SynthesizeSymbolic.ml | 2 |
9 files changed, 139 insertions, 93 deletions
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index 8fb7053b..0c72392b 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -4,6 +4,15 @@ open Values open LlbcAst module V = Values open ValuesUtils +open Identifiers + +(** The [Id] module for dummy variables. + + Dummy variables are used to store values that we don't want to forget + in the environment, because they contain borrows for instance, typically + because they might be overwritten during an assignment. + *) +module DummyVarId = IdGen () (** Some global counters. @@ -70,6 +79,9 @@ let abstraction_id_counter, fresh_abstraction_id = let fun_call_id_counter, fresh_fun_call_id = FunCallId.fresh_stateful_generator () +let dummy_var_id_counter, fresh_dummy_var_id = + DummyVarId.fresh_stateful_generator () + (** We shouldn't need to reset the global counters, but it might be good to do it from time to time, for instance every time we start evaluating/ synthesizing a function. @@ -86,22 +98,41 @@ let reset_global_counters () = borrow_id_counter := BorrowId.generator_zero; region_id_counter := RegionId.generator_zero; abstraction_id_counter := AbstractionId.generator_zero; - fun_call_id_counter := FunCallId.generator_zero + fun_call_id_counter := FunCallId.generator_zero; + dummy_var_id_counter := DummyVarId.generator_zero (** A binder used in an environment, to map a variable to a value *) -type binder = { +type var_binder = { index : VarId.id; (** Unique variable identifier *) name : string option; (** Possible name *) } [@@deriving show] +(** A binder, for a "real" variable or a dummy variable *) +type binder = VarBinder of var_binder | DummyBinder of DummyVarId.id +[@@deriving show] + +(** Ancestor for {!env_elem} iter visitor *) +class ['self] iter_env_elem_base = + object (_self : 'self) + inherit [_] iter_abs + method visit_binder : 'env -> binder -> unit = fun _ _ -> () + end + +(** Ancestor for {!env_elem} map visitor *) +class ['self] map_env_elem_base = + object (_self : 'self) + inherit [_] map_abs + method visit_binder : 'env -> binder -> binder = fun _ x -> x + end + (** Environment value: mapping from variable to value, abstraction (only used in symbolic mode) or stack frame delimiter. TODO: rename Var (-> Binding?) *) type env_elem = - | Var of (binder option[@opaque]) * typed_value + | Var of binder * 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). *) @@ -113,7 +144,7 @@ type env_elem = { name = "iter_env_elem"; variety = "iter"; - ancestors = [ "iter_abs" ]; + ancestors = [ "iter_env_elem_base" ]; nude = true (* Don't inherit {!VisitorsRuntime.iter} *); concrete = true; }, @@ -121,7 +152,7 @@ type env_elem = { name = "map_env_elem"; variety = "map"; - ancestors = [ "map_abs" ]; + ancestors = [ "map_env_elem_base" ]; nude = true (* Don't inherit {!VisitorsRuntime.iter} *); concrete = true; }] @@ -235,54 +266,44 @@ 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 *) +(** Lookup a variable in the current frame *) +let env_lookup_var (env : env) (vid : VarId.id) : var_binder * typed_value = + (* We take care to stop at the end of current frame: different variables + in different frames can have the same id! + *) let rec lookup env = match env with | [] -> raise (Invalid_argument ("Variable not found: " ^ VarId.to_string vid)) - | Var (var, _) :: env' -> - if opt_binder_has_vid var vid then Option.get var else lookup env' - | (Abs _ | Frame) :: env' -> lookup env' + | Var (VarBinder var, v) :: env' -> + if var.index = vid then (var, v) else lookup env' + | (Var (DummyBinder _, _) | Abs _) :: env' -> lookup env' + | Frame :: _ -> raise (Failure "End of frame") in - lookup ctx.env + lookup env + +let ctx_lookup_var_binder (ctx : eval_ctx) (vid : VarId.id) : var_binder = + fst (env_lookup_var ctx.env vid) -(** TODO: make this more efficient with maps *) let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl = TypeDeclId.Map.find tid ctx.type_context.type_decls -(** TODO: make this more efficient with maps *) let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl = FunDeclId.Map.find fid ctx.fun_context.fun_decls -(** TODO: make this more efficient with maps *) let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : global_decl = GlobalDeclId.Map.find gid ctx.global_context.global_decls -(** Retrieve a variable's value in an environment *) +(** Retrieve a variable's value in the current frame *) let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = - (* We take care to stop at the end of current frame: different variables - in different frames can have the same id! - *) - let rec lookup env = - match env with - | [] -> raise (Failure "Unexpected") - | Var (var, v) :: env' -> - if opt_binder_has_vid var vid then v else lookup env' - | Abs _ :: env' -> lookup env' - | Frame :: _ -> raise (Failure "End of frame") - in - lookup env + snd (env_lookup_var env vid) (** Retrieve a variable's value in an evaluation context *) let ctx_lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value = env_lookup_var_value ctx.env vid -(** Update a variable's value in an environment +(** Update a variable's value in the current frame. This is a helper function: it can break invariants and doesn't perform any check. @@ -294,15 +315,16 @@ let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env = let rec update env = match env with | [] -> raise (Failure "Unexpected") - | Var (var, v) :: env' -> - if opt_binder_has_vid var vid then Var (var, nv) :: env' + | Var ((VarBinder b as var), v) :: env' -> + if b.index = vid then Var (var, nv) :: env' else Var (var, v) :: update env' - | Abs abs :: env' -> Abs abs :: update env' + | ((Var (DummyBinder _, _) | Abs _) as ee) :: env' -> ee :: update env' | Frame :: _ -> raise (Failure "End of frame") in update env -let var_to_binder (var : var) : binder = { index = var.index; name = var.name } +let var_to_binder (var : var) : var_binder = + { index = var.index; name = var.name } (** Update a variable's value in an evaluation context. @@ -321,7 +343,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 (Some bv, v) :: ctx.env } + { ctx with env = Var (VarBinder bv, v) :: ctx.env } (** Push a list of variables. @@ -335,37 +357,41 @@ 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 (Some (var_to_binder var), value)) vars + List.map + (fun (var, value) -> Var (VarBinder (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 a context's environment. *) -let ctx_pop_dummy_var (ctx : eval_ctx) : eval_ctx * typed_value = - let rec pop_var (env : env) : env * typed_value = +let ctx_push_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) (v : typed_value) + : eval_ctx = + { ctx with env = Var (DummyBinder vid, v) :: ctx.env } + +(** Remove a dummy variable from a context's environment. *) +let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) : + eval_ctx * typed_value = + let rec remove_var (env : env) : env * typed_value = match env with - | [] -> raise (Failure "Could not find a dummy variable") - | Var (None, v) :: env -> (env, v) + | [] -> raise (Failure "Could not lookup a dummy variable") + | Var (DummyBinder vid', v) :: env when vid' = vid -> (env, v) | ee :: env -> - let env, v = pop_var env in + let env, v = remove_var env in (ee :: env, v) in - let env, v = pop_var ctx.env in + let env, v = remove_var ctx.env in ({ ctx with env }, v) -(** Read the first dummy variable in a context's environment. *) -let ctx_read_first_dummy_var (ctx : eval_ctx) : typed_value = - let rec read_var (env : env) : typed_value = +(** Lookup a dummy variable in a context's environment. *) +let ctx_lookup_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) : typed_value = + let rec lookup_var (env : env) : typed_value = match env with - | [] -> raise (Failure "Could not find a dummy variable") - | Var (None, v) :: _env -> v - | _ :: env -> read_var env + | [] -> raise (Failure "Could not lookup a dummy variable") + | Var (DummyBinder vid', v) :: _env when vid' = vid -> v + | _ :: env -> lookup_var env in - read_var ctx.env + lookup_var ctx.env (** Push an uninitialized variable (which thus maps to {!Values.Bottom}) *) let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx = @@ -398,8 +424,8 @@ class ['self] iter_frame = object (self : 'self) inherit [_] V.iter_abs - method visit_Var : 'acc -> binder option -> typed_value -> unit = - fun acc _vid v -> self#visit_typed_value acc v + method visit_Var : 'acc -> binder -> typed_value -> unit = + fun acc _ v -> self#visit_typed_value acc v method visit_Abs : 'acc -> abs -> unit = fun acc abs -> self#visit_abs acc abs @@ -426,10 +452,10 @@ class ['self] map_frame_concrete = object (self : 'self) inherit [_] V.map_abs - method visit_Var : 'acc -> binder option -> typed_value -> env_elem = - fun acc vid v -> + method visit_Var : 'acc -> binder -> typed_value -> env_elem = + fun acc b v -> let v = self#visit_typed_value acc v in - Var (vid, v) + Var (b, v) method visit_Abs : 'acc -> abs -> env_elem = fun acc abs -> Abs (self#visit_abs acc abs) diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 16aaf60a..c8a7ae7f 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -931,7 +931,7 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids) * By doing that we should have ended the target borrow (see the * below sanity check) *) end_abstraction config chain abs_id - | VarId _, _ -> + | (VarId _ | DummyVarId _), _ -> (* The loan is not inside the same abstraction (actually inside * a non-abstraction value): we need to end the whole abstraction *) end_abstraction config chain abs_id diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 6f9b2ffe..214f2cda 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -254,7 +254,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) assert (Option.is_none !abs_or_var); abs_or_var := Some - (VarId (match bv with Some bv -> Some bv.C.index | None -> None)); + (match bv with + | VarBinder b -> VarId b.C.index + | DummyBinder id -> DummyVarId id); super#visit_Var env bv v; abs_or_var := None diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 5fcc25eb..cc5b5864 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -635,12 +635,13 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun = let access = Write in let v = read_place_unwrap config access p ctx in let ctx = write_place_unwrap config access p (mk_bottom v.V.ty) ctx in - let ctx = C.ctx_push_dummy_var ctx v in + let dummy_id = C.fresh_dummy_var_id () in + let ctx = C.ctx_push_dummy_var ctx dummy_id v in (* Auxiliary function *) let rec drop : cm_fun = fun cf ctx -> (* Read the value *) - let v = C.ctx_read_first_dummy_var ctx in + let v = C.ctx_lookup_dummy_var ctx dummy_id in (* Check if there are loans or borrows to end *) let with_borrows = false in match get_first_outer_loan_or_borrow_in_value with_borrows v with @@ -665,7 +666,7 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun = let cc = comp cc (fun cf ctx -> (* Pop *) - let ctx, v = C.ctx_pop_dummy_var ctx in + let ctx, v = C.ctx_remove_dummy_var ctx dummy_id in (* Reinsert *) let ctx = write_place_unwrap config access p v ctx in (* Sanity check *) diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 84a6716c..4d447ffe 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -40,7 +40,8 @@ let drop_value (config : C.config) (p : E.place) : cm_fun = (* Move the value at destination (that we will overwrite) to a dummy variable * to preserve the borrows it may contain *) let mv = read_place_unwrap config access p ctx in - let ctx = C.ctx_push_dummy_var ctx mv in + let dummy_id = C.fresh_dummy_var_id () in + let ctx = C.ctx_push_dummy_var ctx dummy_id mv in (* Update the destination to ⊥ *) let nv = { v with value = V.Bottom } in let ctx = write_place_unwrap config access p nv ctx in @@ -54,15 +55,16 @@ let drop_value (config : C.config) (p : E.place) : cm_fun = comp cc replace cf ctx (** Push a dummy variable to the environment *) -let push_dummy_var (v : V.typed_value) : cm_fun = +let push_dummy_var (vid : C.DummyVarId.id) (v : V.typed_value) : cm_fun = fun cf ctx -> - let ctx = C.ctx_push_dummy_var ctx v in + let ctx = C.ctx_push_dummy_var ctx vid v in cf ctx -(** Pop a dummy variable from the environment *) -let pop_dummy_var (cf : V.typed_value -> m_fun) : m_fun = +(** Remove a dummy variable from the environment *) +let remove_dummy_var (vid : C.DummyVarId.id) (cf : V.typed_value -> m_fun) : + m_fun = fun ctx -> - let ctx, v = C.ctx_pop_dummy_var ctx in + let ctx, v = C.ctx_remove_dummy_var ctx vid in cf v ctx (** Push an uninitialized variable to the environment *) @@ -106,18 +108,20 @@ let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) : ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Initial context:\n" ^ eval_ctx_to_string ctx)); (* Push the rvalue to a dummy variable, for bookkeeping *) - let cc = push_dummy_var rv in + let rvalue_vid = C.fresh_dummy_var_id () in + let cc = push_dummy_var rvalue_vid rv in (* Prepare the destination *) let cc = comp cc (prepare_lplace config p) in (* Retrieve the rvalue from the dummy variable *) - let cc = comp cc (fun cf _lv -> pop_dummy_var cf) in + let cc = comp cc (fun cf _lv -> remove_dummy_var rvalue_vid cf) in (* Update the destination *) let move_dest cf (rv : V.typed_value) : m_fun = fun ctx -> (* Move the value at destination (that we will overwrite) to a dummy variable * to preserve the borrows *) let mv = read_place_unwrap config Write p ctx in - let ctx = C.ctx_push_dummy_var ctx mv in + let dest_vid = C.fresh_dummy_var_id () in + let ctx = C.ctx_push_dummy_var ctx dest_vid mv in (* Write to the destination *) (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) assert (not (bottom_in_value ctx.ended_regions rv)); @@ -338,8 +342,8 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun = match env with | [] -> raise (Failure "Inconsistent environment") | C.Abs _ :: env -> list_locals env - | C.Var (None, _) :: env -> list_locals env - | C.Var (Some var, _) :: env -> + | C.Var (DummyBinder _, _) :: env -> list_locals env + | C.Var (VarBinder var, _) :: env -> let locals = list_locals env in if var.index <> ret_vid then var.index :: locals else locals | C.Frame :: _ -> [] @@ -390,7 +394,9 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun = match env with | [] -> raise (Failure "Inconsistent environment") | C.Abs abs :: env -> C.Abs abs :: pop env - | C.Var (_, v) :: env -> C.Var (None, v) :: pop env + | C.Var (_, v) :: env -> + let vid = C.fresh_dummy_var_id () in + C.Var (C.DummyBinder vid, v) :: pop env | C.Frame :: env -> (* Stop here *) env in let cf_pop cf (ret_value : V.typed_value) : m_fun = @@ -424,8 +430,9 @@ let eval_box_new_concrete (config : C.config) match (region_params, type_params, ctx.env) with | ( [], [ boxed_ty ], - Var (Some input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) - -> + Var (VarBinder input_var, input_value) + :: Var (_ret_var, _) + :: C.Frame :: _ ) -> (* Required type checking *) assert (input_value.V.ty = boxed_ty); @@ -465,8 +472,9 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config) match (region_params, type_params, ctx.env) with | ( [], [ boxed_ty ], - Var (Some input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) - -> + Var (VarBinder 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/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 31f25f45..8d23e8d8 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -124,7 +124,10 @@ type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs (** Generic borrow content: concrete or abstract *) type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs -type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of E.VarId.id option +type abs_or_var_id = + | AbsId of V.AbstractionId.id + | VarId of E.VarId.id + | DummyVarId of C.DummyVarId.id (** Utility exception *) exception FoundBorrowContent of V.borrow_content diff --git a/compiler/Print.ml b/compiler/Print.ml index dc73b572..53bba8c7 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -310,18 +310,24 @@ module PV = Values (* local module *) (** Pretty-printing for contexts *) module Contexts = struct - let binder_to_string (bv : C.binder) : string = + let var_binder_to_string (bv : C.var_binder) : string = match bv.name with | None -> PV.var_id_to_string bv.index | Some name -> name + let dummy_var_id_to_string (bid : C.DummyVarId.id) : string = + "_@" ^ C.DummyVarId.to_string bid + + let binder_to_string (bv : C.binder) : string = + match bv with + | VarBinder b -> var_binder_to_string b + | DummyBinder bid -> dummy_var_id_to_string bid + let env_elem_to_string (fmt : PV.value_formatter) (indent : string) (indent_incr : string) (ev : C.env_elem) : string = match ev with | Var (var, tv) -> - let bv = - match var with Some var -> binder_to_string var | None -> "_" - in + let bv = binder_to_string var in indent ^ bv ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;" | Abs abs -> PV.abs_to_string fmt indent indent_incr abs | Frame -> raise (Failure "Can't print a Frame element") @@ -343,10 +349,10 @@ module Contexts = struct *) let filter_elem (ev : C.env_elem) : C.env_elem option = match ev with - | Var (Some _, tv) -> + | Var (VarBinder _, tv) -> (* Not a dummy binding: check if the value is ⊥ *) if VU.is_bottom tv.value then None else Some ev - | Var (None, tv) -> + | Var (DummyBinder _, tv) -> (* Dummy binding: check if the value contains borrows or loans *) if VU.borrows_in_value tv || VU.loans_in_value tv then Some ev else None @@ -419,8 +425,8 @@ module Contexts = struct PT.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls in let var_id_to_string vid = - let bv = C.ctx_lookup_binder ctx vid in - binder_to_string bv + let bv = C.ctx_lookup_var_binder ctx vid in + var_binder_to_string bv in let adt_field_names = PT.type_ctx_to_adt_field_names_fun ctx.type_context.type_decls @@ -492,8 +498,8 @@ module Contexts = struct List.iter (fun ev -> match ev with - | C.Var (None, _) -> num_dummies := !num_abs + 1 - | C.Var (Some _, _) -> num_bindings := !num_bindings + 1 + | C.Var (DummyBinder _, _) -> num_dummies := !num_abs + 1 + | C.Var (VarBinder _, _) -> num_bindings := !num_bindings + 1 | C.Abs _ -> num_abs := !num_abs + 1 | _ -> raise (Failure "Unreachable")) f; diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index 604a7948..39709a13 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -18,7 +18,7 @@ module A = LlbcAst the generated code. *) type mplace = { - bv : Contexts.binder; + bv : Contexts.var_binder; (** It is important that we store the binder, and not just the variable id, because the most important information in a place is the name of the variable! diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 383ff15e..504fcdb5 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -7,7 +7,7 @@ module A = LlbcAst open SymbolicAst let mk_mplace (p : E.place) (ctx : Contexts.eval_ctx) : mplace = - let bv = Contexts.ctx_lookup_binder ctx p.var_id in + let bv = Contexts.ctx_lookup_var_binder ctx p.var_id in { bv; projection = p.projection } let mk_opt_mplace (p : E.place option) (ctx : Contexts.eval_ctx) : mplace option |