diff options
| -rw-r--r-- | src/Contexts.ml | 4 | ||||
| -rw-r--r-- | src/Interpreter.ml | 58 | ||||
| -rw-r--r-- | src/Values.ml | 3 |
3 files changed, 54 insertions, 11 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index dd7ca016..2a12dd96 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -25,6 +25,7 @@ type eval_ctx = { fun_context : fun_def FunDefId.vector; type_vars : type_var TypeVarId.vector; vars : var VarId.Map.t; + (* TODO: remove this *) frames : stack_frame list; env : env; symbolic_counter : SymbolicValueId.generator; @@ -49,6 +50,9 @@ let ctx_lookup_var (ctx : eval_ctx) (vid : VarId.id) : var = let ctx_lookup_type_def (ctx : eval_ctx) (tid : TypeDefId.id) : type_def = TypeDefId.nth ctx.type_context tid +let ctx_lookup_fun_def (ctx : eval_ctx) (fid : FunDefId.id) : fun_def = + FunDefId.nth ctx.fun_context fid + (** Retrieve a variable's value in an environment *) let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = let check_ev (ev : env_value) : typed_value option = diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 77af0b54..60441ce7 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1939,21 +1939,57 @@ and eval_function_call (config : C.config) (ctx : C.eval_ctx) (call : A.call) : *) match call.func with | A.Local fid -> - eval_local_function_call fid call.region_params call.type_params call.args - call.dest + eval_local_function_call config ctx fid call.region_params + call.type_params call.args call.dest | A.Assumed fid -> - eval_assumed_function_call fid call.region_params call.type_params - call.args call.dest + eval_assumed_function_call config ctx fid call.region_params + call.type_params call.args call.dest -and eval_local_function_call (fid : A.FunDefId.id) - (region_params : T.erased_region list) (type_params : T.ety list) - (args : E.operand list) (dest : E.place) : +and eval_local_function_call (config : C.config) (ctx : C.eval_ctx) + (fid : A.FunDefId.id) (_region_params : T.erased_region list) + (type_params : T.ety list) (args : E.operand list) (dest : E.place) : (C.eval_ctx * statement_eval_res) eval_result = (* Retrieve the (correctly instantiated) body *) - raise Unimplemented + let def = C.ctx_lookup_fun_def ctx fid in + match config.mode with + | ConcreteMode -> + let tsubst = + Subst.make_type_subst + (List.map + (fun v -> v.T.tv_index) + (T.TypeVarId.vector_to_list def.A.signature.type_params)) + type_params + in + let locals, body = Subst.fun_def_substitute_in_body tsubst def in + + (* Evaluate the input operands *) + let ctx1, args = eval_operands config ctx args in + + (* Compute the initial values for the local variables *) + (* First, compute the types of the variables *) + let local_tys = + List.map (fun l -> l.V.var_ty) (V.VarId.vector_to_list locals) + in + + (* Second, push the return value *) + let ret_var, local_tys = + match local_tys with + | ret_ty :: local_tys -> (ret_ty, local_tys) + | _ -> failwith "Unreachable" + in + + (* let ctx2 = ctx_push_var *) + + (* Third, push the inputs *) + + (* Finally, put the remaining local variables (initialized as [Bottom]) *) + + (* TODO ... *) + raise Unimplemented + | SymbolicMode -> raise Unimplemented -and eval_assumed_function_call (fid : A.assumed_fun_id) - (region_params : T.erased_region list) (type_params : T.ety list) - (args : E.operand list) (dest : E.place) : +and eval_assumed_function_call (config : C.config) (ctx : C.eval_ctx) + (fid : A.assumed_fun_id) (region_params : T.erased_region list) + (type_params : T.ety list) (args : E.operand list) (dest : E.place) : (C.eval_ctx * statement_eval_res) eval_result = raise Unimplemented diff --git a/src/Values.ml b/src/Values.ml index 2c80cfe9..1346c7f7 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -1,6 +1,9 @@ open Identifiers open Types +(** TODO: do we put the type variable/variable/region names everywhere + (to not have to perform lookups by using the ids?) *) + module VarId = IdGen () module BorrowId = IdGen () |