diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Contexts.ml | 4 | ||||
| -rw-r--r-- | src/Identifiers.ml | 9 | ||||
| -rw-r--r-- | src/Interpreter.ml | 186 |
3 files changed, 178 insertions, 21 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 258415a9..f13043d0 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -118,6 +118,10 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty } +(** Push an uninitialized variable (which thus maps to [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 [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 diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 23c887c4..824fd8ad 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -48,6 +48,9 @@ module type Id = sig val mapi : (id -> 'a -> 'b) -> 'a vector -> 'b vector + val mapi_from1 : (id -> 'a -> 'b) -> 'a vector -> 'b vector + (** Same as [mapi], but where the indices start with 1 *) + val for_all : ('a -> bool) -> 'a vector -> bool val exists : ('a -> bool) -> 'a vector -> bool @@ -120,6 +123,12 @@ module IdGen () : Id = struct let mapi = List.mapi + let mapi_from1 f ls = + let rec aux i ls = + match ls with [] -> [] | x :: ls' -> f i x :: aux (i + 1) ls' + in + aux 1 ls + let for_all = List.for_all let exists = List.exists diff --git a/src/Interpreter.ml b/src/Interpreter.ml index ce13b38c..3df2fe72 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -10,6 +10,30 @@ module A = CfimAst (* TODO: Change state-passing style to : st -> ... -> (st, v) *) (* TODO: check that the value types are correct when evaluating *) (* TODO: module Type = T, etc. *) +(* TODO: is it a good idea to give indices to variables? For instance: + let ctx1 = .. in + let ctx2 = ... ctx1 in + ... + *) + +(* TODO: move *) +let mk_unit_ty : T.ety = T.Tuple [] + +(* TODO: move *) +let mk_unit_value : V.typed_value = + { V.value = V.Tuple (T.FieldId.vector_of_list []); V.ty = mk_unit_ty } + +let mk_typed_value (ty : T.ety) (value : V.value) : V.typed_value = + { V.value; ty } + +(* TODO: move *) +let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : V.var + = + { V.index; name; var_ty } + +(** Small helper *) +let mk_place_from_var_id (var_id : V.VarId.id) : E.place = + { var_id; projection = [] } (** TODO: change the name *) type eval_error = Panic @@ -1868,10 +1892,6 @@ let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place) let ctx_push_frame (ctx : C.eval_ctx) : C.eval_ctx = { ctx with env = Frame :: ctx.env } -(** Small helper *) -let mk_place_from_var_id (var_id : V.VarId.id) : E.place = - { var_id; projection = [] } - (** Drop a value at a given place *) let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx = @@ -1881,6 +1901,18 @@ let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx let ctx2 = { ctx with env = env2 } in ctx2 +(** Small helper: compute the type of the return value for a specific + instantiation of a non-local function. + *) +let get_non_local_function_return_type (fid : A.assumed_fun_id) + (region_params : T.erased_region list) (type_params : T.ety list) : T.ety = + match (fid, region_params, type_params) with + | A.BoxNew, [], [ bty ] -> T.Assumed (T.Box, [], [ bty ]) + | A.BoxDeref, [], [ bty ] -> T.Ref (T.Erased, bty, T.Shared) + | A.BoxDerefMut, [], [ bty ] -> T.Ref (T.Erased, bty, T.Mut) + | A.BoxFree, [], [ _ ] -> mk_unit_ty + | _ -> failwith "Inconsistent state" + (** Pop the current frame. Drop all the local variables but the return variable, move the return @@ -1934,6 +1966,123 @@ let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) let ctx3 = { ctx2 with env = env3 } in ctx3 +(** Auxiliary function - see [eval_non_local_function_call] *) +let eval_box_new (config : C.config) (region_params : T.erased_region list) + (type_params : T.ety list) (ctx : C.eval_ctx) : C.eval_ctx eval_result = + (* Check and retrieve the arguments *) + match (region_params, type_params, ctx.env) with + | ( [], + [ boxed_ty ], + Var (input_var, input_value) :: Var (ret_var, _) :: C.Frame :: env' ) -> + (* Type checking *) + assert (input_value.V.ty = boxed_ty); + + (* Move the input value *) + let ctx, moved_input_value = + eval_operand config ctx + (E.Move (mk_place_from_var_id input_var.V.index)) + in + + (* Create the box value *) + let box_ty = T.Assumed (T.Box, [], [ boxed_ty ]) in + let box_v = V.Assumed (V.Box moved_input_value) in + let box_v = mk_typed_value box_ty box_v in + + (* Move this value to the return variable *) + let dest = mk_place_from_var_id V.VarId.zero in + let ctx = assign_to_place config ctx box_v dest in + + (* Return *) + Ok ctx + | _ -> failwith "Inconsistent state" + +(** Auxiliary function - see [eval_non_local_function_call] *) +let eval_box_deref (config : C.config) (region_params : T.erased_region list) + (type_params : T.ety list) (ctx : C.eval_ctx) : C.eval_ctx eval_result = + raise Unimplemented + +(** Auxiliary function - see [eval_non_local_function_call] *) +let eval_box_deref_mut (config : C.config) + (region_params : T.erased_region list) (type_params : T.ety list) + (ctx : C.eval_ctx) : C.eval_ctx eval_result = + raise Unimplemented + +(** Auxiliary function - see [eval_non_local_function_call]. + + In practice, does nothing put aside checking the input types: the box + value has been moved to a local variable in the function frame, this value + is then dropped uppon exiting. +*) +let eval_box_free (config : C.config) (region_params : T.erased_region list) + (type_params : T.ety list) (ctx : C.eval_ctx) : C.eval_ctx eval_result = + match (region_params, type_params, ctx.env) with + | ( [], + [ box_ty ], + Var (input_var, input_value) :: Var (ret_var, _) :: C.Frame :: _ ) -> + (* Check the arguments *) + assert ( + match input_value.V.ty with + | T.Assumed (T.Box, [], [ boxed_ty ]) -> boxed_ty = input_value.V.ty + | _ -> false); + + (* Update the return value *) + let dest = mk_place_from_var_id V.VarId.zero in + let ctx = assign_to_place config ctx mk_unit_value dest in + + (* Return *) + Ok ctx + | _ -> failwith "Inconsistent state" + +(** Evaluate a non-local (i.e, assumed) function call such as `Box::deref` + (auxiliary helper for [eval_statement]) *) +let eval_non_local_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 eval_result = + (* Evaluate the operands *) + let ctx, args_vl = eval_operands config ctx args in + + (* Push the stack frame: we initialize the frame with the return variable, + and one variable per input argument *) + let ctx = ctx_push_frame ctx in + + (* Create and push the return variable *) + let ret_vid = V.VarId.zero in + let ret_ty = + get_non_local_function_return_type fid region_params type_params + in + let ret_var = mk_var ret_vid (Some "@return") ret_ty in + let ctx = C.ctx_push_uninitialized_var ctx ret_var in + + (* Create and push the input variables *) + let input_vars = + V.VarId.vector_to_list + (V.VarId.mapi_from1 + (fun id v -> (mk_var id None v.V.ty, v)) + (V.VarId.vector_of_list args_vl)) + in + let ctx = C.ctx_push_vars ctx input_vars in + + (* "Execute" the function body. As the functions are assumed, here we call + custom functions to perform the proper manipulations: we don't have + access to a body. *) + let res = + match fid with + | A.BoxNew -> eval_box_new config region_params type_params ctx + | A.BoxDeref -> eval_box_deref config region_params type_params ctx + | A.BoxDerefMut -> eval_box_deref_mut config region_params type_params ctx + | A.BoxFree -> eval_box_free config region_params type_params ctx + in + + (* Pop the stack frame and retrieve the return value *) + let ctx, ret_value = ctx_pop_frame config ctx in + + (* Move the return value to its destination *) + let ctx = assign_to_place config ctx ret_value dest in + + (* Return *) + Ok ctx + (** Evaluate a statement *) let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) : (C.eval_ctx * statement_eval_res) eval_result = @@ -1973,20 +2122,23 @@ and eval_function_call (config : C.config) (ctx : C.eval_ctx) (call : A.call) : - this is a local function, in which case we execute its body - this is a non-local function, in which case there is a special treatment *) - match call.func with - | A.Local fid -> - eval_local_function_call config ctx fid call.region_params - call.type_params call.args call.dest - | A.Assumed fid -> - eval_assumed_function_call config ctx fid call.region_params - call.type_params call.args call.dest + let res = + match call.func with + | A.Local fid -> + eval_local_function_call config ctx fid call.region_params + call.type_params call.args call.dest + | A.Assumed fid -> + eval_non_local_function_call config ctx fid call.region_params + call.type_params call.args call.dest + in + match res with Error err -> Error err | Ok ctx -> Ok (ctx, Unit) (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for [eval_statement]) *) 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 = + C.eval_ctx eval_result = (* Retrieve the (correctly instantiated) body *) let def = C.ctx_lookup_fun_def ctx fid in match config.mode with @@ -2040,7 +2192,7 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx) let ctx8 = assign_to_place config ctx7 ret_value dest in (* Return *) - Ok (ctx8, Unit)) + Ok ctx8) | SymbolicMode -> raise Unimplemented (** Evaluate an expression seen as a function body (auxiliary helper for @@ -2054,14 +2206,6 @@ and eval_function_body (config : C.config) (ctx : C.eval_ctx) | Unit | Break _ | Continue _ -> failwith "Inconsistent state" | Return -> Ok ctx1) -(** Evaluate an assumed function call such as `Box::deref` (auxiliary helper for - [eval_statement]) *) -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 - (** Evaluate an expression *) and eval_expression (config : C.config) (ctx : C.eval_ctx) (e : A.expression) : (C.eval_ctx * statement_eval_res) eval_result = |