summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Contexts.ml4
-rw-r--r--src/Identifiers.ml9
-rw-r--r--src/Interpreter.ml186
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 =