diff options
author | Son Ho | 2022-01-26 17:40:56 +0100 |
---|---|---|
committer | Son Ho | 2022-01-26 17:40:56 +0100 |
commit | 781829ec8d4d825e550f36f853eed2c97ddb7a04 (patch) | |
tree | 422063b62a556b3c7676fca32b6642664f90d79d /src/Interpreter.ml | |
parent | 47b94c9938bccf1ea2b2ec1ff2cc188b6a4765ef (diff) |
Make progress on translation
Diffstat (limited to 'src/Interpreter.ml')
-rw-r--r-- | src/Interpreter.ml | 162 |
1 files changed, 78 insertions, 84 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index cd7952e0..74e4e815 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -10,100 +10,94 @@ open InterpreterStatements (** The local logger *) let log = L.interpreter_log -module Test = struct - let initialize_context (m : M.cfim_module) (type_vars : T.type_var list) : - C.eval_ctx = - let type_decls, _ = M.split_declarations m.declarations in - let type_defs, fun_defs = M.compute_defs_maps m in - let type_defs_groups, _funs_defs_groups = - M.split_declarations_to_group_maps m.declarations - in - let type_infos = - TypesAnalysis.analyze_type_declarations type_defs type_decls - in - let type_context = { C.type_defs_groups; type_defs; type_infos } in - C.reset_global_counters (); - { - C.type_context; - C.fun_context = fun_defs; - C.type_vars; - C.env = []; - C.ended_regions = T.RegionId.Set.empty; - } - - (** Initialize an evaluation context to execute a function. +let initialize_context (m : M.cfim_module) (type_vars : T.type_var list) : + C.eval_ctx = + let type_decls, _ = M.split_declarations m.declarations in + let type_defs, fun_defs = M.compute_defs_maps m in + let type_defs_groups, _funs_defs_groups = + M.split_declarations_to_group_maps m.declarations + in + let type_infos = + TypesAnalysis.analyze_type_declarations type_defs type_decls + in + let type_context = { C.type_defs_groups; type_defs; type_infos } in + C.reset_global_counters (); + { + C.type_context; + C.fun_context = fun_defs; + C.type_vars; + C.env = []; + C.ended_regions = T.RegionId.Set.empty; + } + +(** Initialize an evaluation context to execute a function. Introduces local variables initialized in the following manner: - input arguments are initialized as symbolic values - the remaining locals are initialized as ⊥ Abstractions are introduced for the regions present in the function signature. - *) - let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) - : C.eval_ctx = - (* The abstractions are not initialized the same way as for function - * calls: they contain *loan* projectors, because they "provide" us - * with the input values (which behave as if they had been returned - * by some function calls...). - * Also, note that we properly set the set of parents of every abstraction: - * this should not be necessary, as those abstractions should never be - * *automatically* ended (because ending some borrows requires to end - * one of them), but rather selectively ended when generating code - * for each of the backward functions. We do it only because we can - * do it, and because it gives a bit of sanity. - * *) - let sg = fdef.signature in - (* Create the context *) - let ctx = initialize_context m sg.type_params in - (* Instantiate the signature *) - let type_params = - List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params - in - let inst_sg = instantiate_fun_sig type_params sg in - (* Create fresh symbolic values for the inputs *) - let input_svs = - List.map - (fun ty -> mk_fresh_symbolic_value V.SynthInput ty) - inst_sg.inputs + *) +let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) : + C.eval_ctx = + (* The abstractions are not initialized the same way as for function + * calls: they contain *loan* projectors, because they "provide" us + * with the input values (which behave as if they had been returned + * by some function calls...). + * Also, note that we properly set the set of parents of every abstraction: + * this should not be necessary, as those abstractions should never be + * *automatically* ended (because ending some borrows requires to end + * one of them), but rather selectively ended when generating code + * for each of the backward functions. We do it only because we can + * do it, and because it gives a bit of sanity. + * *) + let sg = fdef.signature in + (* Create the context *) + let ctx = initialize_context m sg.type_params in + (* Instantiate the signature *) + let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in + let inst_sg = instantiate_fun_sig type_params sg in + (* Create fresh symbolic values for the inputs *) + let input_svs = + List.map (fun ty -> mk_fresh_symbolic_value V.SynthInput ty) inst_sg.inputs + in + (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) + let call_id = C.fresh_fun_call_id () in + assert (call_id = V.FunCallId.zero); + let empty_absl = + create_empty_abstractions_from_abs_region_groups call_id V.SynthInput + inst_sg.A.regions_hierarchy + in + (* Add the avalues to the abstractions and insert them in the context *) + let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = + (* Project over the values - we use *loan* projectors, as explained above *) + let avalues = + List.map (mk_aproj_loans_value_from_symbolic_value abs.regions) input_svs in - (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) - let call_id = C.fresh_fun_call_id () in - assert (call_id = V.FunCallId.zero); - let empty_absl = - create_empty_abstractions_from_abs_region_groups call_id V.SynthInput - inst_sg.A.regions_hierarchy - in - (* Add the avalues to the abstractions and insert them in the context *) - let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = - (* Project over the values - we use *loan* projectors, as explained above *) - let avalues = - List.map - (mk_aproj_loans_value_from_symbolic_value abs.regions) - input_svs - in - (* Insert the avalues in the abstraction *) - let abs = { abs with avalues } in - (* Insert the abstraction in the context *) - let ctx = { ctx with env = Abs abs :: ctx.env } in - (* Return *) - ctx - in - let ctx = List.fold_left insert_abs ctx empty_absl in - (* Split the variables between return var, inputs and remaining locals *) - let ret_var = List.hd fdef.locals in - let input_vars, local_vars = - Collections.List.split_at (List.tl fdef.locals) fdef.arg_count - in - (* Push the return variable (initialized with ⊥) *) - let ctx = C.ctx_push_uninitialized_var ctx ret_var in - (* Push the input variables (initialized with symbolic values) *) - let input_values = List.map mk_typed_value_from_symbolic_value input_svs in - let ctx = C.ctx_push_vars ctx (List.combine input_vars input_values) in - (* Push the remaining local variables (initialized with ⊥) *) - let ctx = C.ctx_push_uninitialized_vars ctx local_vars in + (* Insert the avalues in the abstraction *) + let abs = { abs with avalues } in + (* Insert the abstraction in the context *) + let ctx = { ctx with env = Abs abs :: ctx.env } in (* Return *) ctx + in + let ctx = List.fold_left insert_abs ctx empty_absl in + (* Split the variables between return var, inputs and remaining locals *) + let ret_var = List.hd fdef.locals in + let input_vars, local_vars = + Collections.List.split_at (List.tl fdef.locals) fdef.arg_count + in + (* Push the return variable (initialized with ⊥) *) + let ctx = C.ctx_push_uninitialized_var ctx ret_var in + (* Push the input variables (initialized with symbolic values) *) + let input_values = List.map mk_typed_value_from_symbolic_value input_svs in + let ctx = C.ctx_push_vars ctx (List.combine input_vars input_values) in + (* Push the remaining local variables (initialized with ⊥) *) + let ctx = C.ctx_push_uninitialized_vars ctx local_vars in + (* Return *) + ctx +module Test = struct (** Test a unit function (taking no arguments) by evaluating it in an empty environment. *) |