diff options
Diffstat (limited to 'compiler/Contexts.ml')
-rw-r--r-- | compiler/Contexts.ml | 472 |
1 files changed, 472 insertions, 0 deletions
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml new file mode 100644 index 00000000..510976f4 --- /dev/null +++ b/compiler/Contexts.ml @@ -0,0 +1,472 @@ +open Types +open Values +open LlbcAst +module V = Values +open ValuesUtils + +(** Some global counters. + + Note that those counters were initially stored in {!eval_ctx} values, + but it proved better to make them global and stateful: + - when branching (and thus executing on several paths with different + contexts) it is better to really have unique ids everywhere (and + not have fresh ids shared by several contexts even though introduced + after the branching) because at some point we might need to merge the + different contexts + - also, it is a lot more convenient to not store those counters in contexts + objects + + ============= + **WARNING**: + ============= + Pay attention when playing with closures, as you may not always generate + fresh identifiers without noticing it, especially when using type abbreviations. + For instance, consider the following: + {[ + type fun_type = unit -> ... + fn f x : fun_type = + let id = fresh_id () in + ... + + let g = f x in // <-- the fresh identifier gets generated here + let x1 = g () in // <-- no fresh generation here + let x2 = g () in + ... + ]} + + This is why, in such cases, we often introduce all the inputs, even + when they are not used (which happens!). + {[ + fn f x : fun_type = + fun .. -> + let id = fresh_id () in + ... + ]} + + Note that in practice, we never reuse closures, except when evaluating + a branching in the execution (which is fine, because the branches evaluate + independentely of each other). Still, it is always a good idea to be + defensive. + + However, the same problem arises with logging. + + Also, a more defensive way would be to not use global references, and + store the counters in the evaluation context. This is actually what was + originally done, before we updated the code to use global counters because + it proved more convenient (and even before updating the code of the + interpreter to use CPS). + *) + +let symbolic_value_id_counter, fresh_symbolic_value_id = + SymbolicValueId.fresh_stateful_generator () + +let borrow_id_counter, fresh_borrow_id = BorrowId.fresh_stateful_generator () +let region_id_counter, fresh_region_id = RegionId.fresh_stateful_generator () + +let abstraction_id_counter, fresh_abstraction_id = + AbstractionId.fresh_stateful_generator () + +let fun_call_id_counter, fresh_fun_call_id = + FunCallId.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. + + The reasons are manifold: + - it might prevent the counters from overflowing (although this seems + extremely unlikely - as a side node: we have overflow checks to make + sure the synthesis doesn't get impacted by potential overflows) + - most importantly, it allows to always manipulate low values, which + is always a lot more readable when debugging + *) +let reset_global_counters () = + symbolic_value_id_counter := SymbolicValueId.generator_zero; + 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 + +(** A binder used in an environment, to map a variable to a value *) +type binder = { + index : VarId.id; (** Unique variable identifier *) + name : string option; (** Possible name *) +} +[@@deriving show] + +(** 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 + (** 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 + { + name = "iter_env_elem"; + variety = "iter"; + ancestors = [ "iter_abs" ]; + nude = true (* Don't inherit {!VisitorsRuntime.iter} *); + concrete = true; + }, + visitors + { + name = "map_env_elem"; + variety = "map"; + ancestors = [ "map_abs" ]; + nude = true (* Don't inherit {!VisitorsRuntime.iter} *); + concrete = true; + }] + +type env = env_elem list +[@@deriving + show, + visitors + { + name = "iter_env"; + variety = "iter"; + ancestors = [ "iter_env_elem" ]; + nude = true (* Don't inherit {!VisitorsRuntime.iter} *); + concrete = true; + }, + visitors + { + name = "map_env"; + variety = "map"; + ancestors = [ "map_env_elem" ]; + nude = true (* Don't inherit {!VisitorsRuntime.iter} *); + concrete = true; + }] + +type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show] + +type config = { + mode : interpreter_mode; + (** Concrete mode (interpreter) or symbolic mode (for synthesis) **) + check_invariants : bool; + (** Check that invariants are maintained whenever we execute a statement *) + greedy_expand_symbolics_with_borrows : bool; + (** Expand all symbolic values containing borrows upon introduction - allows + to use restrict ourselves to a simpler model for the projectors over + symbolic values. + The interpreter fails if doing this requires to do a branching (because + we need to expand an enumeration with strictly more than one variant) + or if we need to expand a recursive type (because this leads to looping). + *) + allow_bottom_below_borrow : bool; + (** Experimental. + + We sometimes want to temporarily break the invariant that there is no + bottom value below a borrow. If this value is true, we don't check + the invariant, and the rule becomes: we can't end a borrow *if* it contains + a bottom value. The consequence is that it becomes ok to temporarily + have bottom below a borrow, if we put something else inside before ending + the borrow. + + For instance, when evaluating an assignment, we move the value which + will be overwritten then do some administrative tasks with the borrows, + then move the rvalue to its destination. We currently want to be able + to check the invariants every time we end a borrow/an abstraction, + meaning at intermediate steps of the assignment where the invariants + might actually be broken. + *) + return_unit_end_abs_with_no_loans : bool; + (** If a function doesn't return any borrows, we can immediately call + its backward functions. If this option is on, whenever we call a + function *and* this function returns unit, we immediately end all the + abstractions which are introduced and don't contain loans. This can be + useful to make the code cleaner (the backward function is introduced + where the function call happened) and make sure all forward functions + with no return value are followed by a backward function. + *) +} +[@@deriving show] + +(** See {!config} *) +type partial_config = { + check_invariants : bool; + greedy_expand_symbolics_with_borrows : bool; + allow_bottom_below_borrow : bool; + return_unit_end_abs_with_no_loans : bool; +} + +let config_of_partial (mode : interpreter_mode) (config : partial_config) : + config = + { + mode; + check_invariants = config.check_invariants; + greedy_expand_symbolics_with_borrows = + config.greedy_expand_symbolics_with_borrows; + allow_bottom_below_borrow = config.allow_bottom_below_borrow; + return_unit_end_abs_with_no_loans = config.return_unit_end_abs_with_no_loans; + } + +type type_context = { + type_decls_groups : Crates.type_declaration_group TypeDeclId.Map.t; + type_decls : type_decl TypeDeclId.Map.t; + type_infos : TypesAnalysis.type_infos; +} +[@@deriving show] + +type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show] + +type global_context = { global_decls : global_decl GlobalDeclId.Map.t } +[@@deriving show] + +(** Evaluation context *) +type eval_ctx = { + type_context : type_context; + fun_context : fun_context; + global_context : global_context; + type_vars : type_var list; + env : env; + ended_regions : RegionId.Set.t; +} +[@@deriving show] + +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 opt_binder_has_vid var vid then Option.get var else lookup env' + | (Abs _ | Frame) :: env' -> lookup env' + in + lookup ctx.env + +(** 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 *) +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 + | [] -> failwith "Unexpected" + | 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 + lookup env + +(** 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 + + This is a helper function: it can break invariants and doesn't perform + any check. +*) +let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env = + (* We take care to stop at the end of current frame: different variables + in different frames can have the same id! + *) + let rec update env = + match env with + | [] -> failwith "Unexpected" + | Var (var, v) :: 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" + in + update env + +let var_to_binder (var : var) : binder = { index = var.index; name = var.name } + +(** Update a variable's value in an evaluation context. + + This is a helper function: it can break invariants and doesn't perform + any check. +*) +let ctx_update_var_value (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) : + eval_ctx = + { ctx with env = env_update_var_value ctx.env vid nv } + +(** Push a variable in the context's environment. + + Checks that the pushed variable and its value have the same type (this + is important). +*) +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 } + +(** Push a list of variables. + + Checks that the pushed variables and their values have the same type (this + is important). +*) +let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx + = + assert ( + List.for_all + (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 + 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 = + 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) + +(** 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 = + match env with + | [] -> failwith "Could not find a dummy variable" + | Var (None, v) :: _env -> v + | _ :: env -> read_var env + in + read_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 = + ctx_push_var ctx var (mk_bottom var.var_ty) + +(** Push a list of uninitialized variables (which thus map to {!Values.Bottom}) *) +let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx = + let vars = List.map (fun v -> (v, mk_bottom v.var_ty)) vars in + ctx_push_vars ctx vars + +let env_lookup_abs (env : env) (abs_id : V.AbstractionId.id) : V.abs = + let rec lookup env = + match env with + | [] -> failwith "Unexpected" + | Var (_, _) :: env' -> lookup env' + | Abs abs :: env' -> if abs.abs_id = abs_id then abs else lookup env' + | Frame :: env' -> lookup env' + in + lookup env + +let ctx_lookup_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) : V.abs = + env_lookup_abs ctx.env abs_id + +let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool = + let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in + match decl_group with Crates.Rec _ -> true | Crates.NonRec _ -> false + +(** Visitor to iterate over the values in the *current* frame *) +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_Abs : 'acc -> abs -> unit = + fun acc abs -> self#visit_abs acc abs + + method visit_env_elem : 'acc -> env_elem -> unit = + fun acc em -> + match em with + | Var (vid, v) -> self#visit_Var acc vid v + | Abs abs -> self#visit_Abs acc abs + | Frame -> failwith "Unreachable" + + method visit_env : 'acc -> env -> unit = + fun acc env -> + match env with + | [] -> () + | Frame :: _ -> (* We stop here *) () + | em :: env -> + self#visit_env_elem acc em; + self#visit_env acc env + end + +(** Visitor to map over the values in the *current* frame *) +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 -> + let v = self#visit_typed_value acc v in + Var (vid, v) + + method visit_Abs : 'acc -> abs -> env_elem = + fun acc abs -> Abs (self#visit_abs acc abs) + + method visit_env_elem : 'acc -> env_elem -> env_elem = + fun acc em -> + match em with + | Var (vid, v) -> self#visit_Var acc vid v + | Abs abs -> self#visit_Abs acc abs + | Frame -> failwith "Unreachable" + + method visit_env : 'acc -> env -> env = + fun acc env -> + match env with + | [] -> [] + | Frame :: env -> (* We stop here *) Frame :: env + | em :: env -> + let em = self#visit_env_elem acc em in + let env = self#visit_env acc env in + em :: env + end + +(** Visitor to iterate over the values in a context *) +class ['self] iter_eval_ctx = + object (_self : 'self) + inherit [_] iter_env as super + + method visit_eval_ctx : 'acc -> eval_ctx -> unit = + fun acc ctx -> super#visit_env acc ctx.env + end + +(** Visitor to map the values in a context *) +class ['self] map_eval_ctx = + object (_self : 'self) + inherit [_] map_env as super + + method visit_eval_ctx : 'acc -> eval_ctx -> eval_ctx = + fun acc ctx -> + let env = super#visit_env acc ctx.env in + { ctx with env } + end |