diff options
| -rw-r--r-- | src/Contexts.ml | 31 | ||||
| -rw-r--r-- | src/Interpreter.ml | 142 | ||||
| -rw-r--r-- | src/Utilities.ml | 7 |
3 files changed, 149 insertions, 31 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 25865064..258415a9 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -39,6 +39,7 @@ let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var = TypeVarId.nth ctx.type_vars vid let ctx_lookup_var (ctx : eval_ctx) (vid : VarId.id) : var = + (* TOOD: we might want to stop at the end of the frame *) let rec lookup env = match env with | [] -> @@ -56,6 +57,7 @@ let ctx_lookup_fun_def (ctx : eval_ctx) (fid : FunDefId.id) : fun_def = (** Retrieve a variable's value in an environment *) let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = + (* TOOD: we might want to stop at the end of the frame *) let check_ev (ev : env_value) : typed_value option = match ev with | Var (var, v) -> if var.index = vid then Some v else None @@ -75,6 +77,7 @@ let ctx_lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value = any check. *) let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env = + (* TOOD: we might want to stop at the end of the frame *) let update_ev (ev : env_value) : env_value = match ev with | Var (var, v) -> if var.index = vid then Var (var, nv) else Var (var, v) @@ -91,3 +94,31 @@ let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env = 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); + { ctx with env = Var (var, 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) -> var.var_ty = value.ty) vars); + let vars = List.map (fun (var, value) -> Var (var, value)) vars in + let vars = List.rev vars in + { ctx with env = List.append vars ctx.env } + +let mk_bottom (ty : ety) : typed_value = { value = Bottom; 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 + ctx_push_vars ctx vars diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 0eae046f..496347ff 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1342,7 +1342,7 @@ let rec collect_borrows_at_place (config : C.config) (access : access_kind) Repeat: - read the value at a given place - - as long as we find a loans or a borrow, end it + - as long as we find a loan or a borrow, end it This is used to drop values (when we need to write to a place, we first drop the value there to properly propagate back values which are not/can't @@ -1779,7 +1779,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : let aty = T.Adt (def_id, regions, types) in Ok (ctx1, { V.value = Adt av; ty = aty })) -(** Result of evaluating a statement *) +(** Result of evaluating a statement - TODO: add prefix *) type statement_eval_res = Unit | Break of int | Continue of int | Return (** Small utility. @@ -1864,6 +1864,75 @@ let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place) | _, (V.Concrete _ | V.Tuple _ | V.Borrow _ | V.Loan _ | V.Assumed _) -> failwith "Unexpected value" +(** Push a frame delimiter in the context's environment *) +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 + = + let ctx1, v = prepare_lplace config p ctx in + let nv = { v with value = V.Bottom } in + let env2 = write_place_unwrap config Write p nv ctx1.env in + let ctx2 = { ctx with env = env2 } in + ctx2 + +(** Pop the current frame. + + Drop all the local variables but the return variable, move the return + value out of the return variable, remove all the local variables (but not the + abstractions!) from the context, remove the [Frame] indicator delimiting the + current frame and return the return value and the updated context. + *) +let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) : + C.eval_ctx * V.typed_value = + let ret_vid = V.VarId.zero in + (* List the local variables, but the return variable *) + let rec list_locals env = + match env with + | [] -> failwith "Inconsistent environment" + | C.Abs _ :: env' -> list_locals env' + | C.Var (var, _) :: env' -> + let locals = list_locals env' in + if var.index = ret_vid then var.index :: locals else locals + | C.Frame :: _ -> [] + in + let locals = list_locals ctx.env in + (* Drop the local variables *) + let ctx1 = + List.fold_left + (fun ctx lid -> drop_value config ctx (mk_place_from_var_id lid)) + ctx locals + in + (* Move the return value out of the return variable *) + let ctx2, ret_value = + eval_operand config ctx1 (E.Move (mk_place_from_var_id ret_vid)) + in + (* Pop the frame *) + let rec pop env = + match env with + | [] -> failwith "Inconsistent environment" + | C.Abs abs :: env' -> C.Abs abs :: pop env' + | C.Var (_, _) :: env' -> pop env' + | C.Frame :: env' -> env' + in + let env3 = pop ctx2.env in + let ctx3 = { ctx2 with env = env3 } in + (ctx3, ret_value) + +let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) + (p : E.place) : C.eval_ctx = + (* Prepare the destination *) + let ctx2, _ = prepare_lplace config p ctx in + (* Update the destination *) + let env3 = write_place_unwrap config Write p v ctx2.env in + let ctx3 = { ctx2 with env = env3 } in + ctx3 + let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) : (C.eval_ctx * statement_eval_res) eval_result = match st with @@ -1872,23 +1941,15 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) match eval_rvalue config ctx rvalue with | Error err -> Error err | Ok (ctx1, rvalue) -> - (* Prepare the destination *) - let ctx2, _ = prepare_lplace config p ctx1 in - (* Update the destination *) - let env3 = write_place_unwrap config Write p rvalue ctx2.env in - let ctx3 = { ctx2 with env = env3 } in - Ok (ctx3, Unit)) + (* Assign *) + let ctx2 = assign_to_place config ctx1 rvalue p in + Ok (ctx2, Unit)) | A.FakeRead p -> let ctx1, _ = prepare_rplace config Read p ctx in Ok (ctx1, Unit) | A.SetDiscriminant (p, variant_id) -> set_discriminant config ctx p variant_id - | A.Drop p -> - let ctx1, v = prepare_lplace config p ctx in - let nv = { v with value = V.Bottom } in - let env2 = write_place_unwrap config Write p nv ctx1.env in - let ctx2 = { ctx with env = env2 } in - Ok (ctx2, Unit) + | A.Drop p -> Ok (drop_value config ctx p, Unit) | A.Assert assertion -> ( let ctx1, v = eval_operand config ctx assertion.cond in assert (v.ty = T.Bool); @@ -1924,7 +1985,7 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx) (* Retrieve the (correctly instantiated) body *) let def = C.ctx_lookup_fun_def ctx fid in match config.mode with - | ConcreteMode -> + | ConcreteMode -> ( let tsubst = Subst.make_type_subst (List.map @@ -1933,35 +1994,60 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx) type_params in let locals, body = Subst.fun_def_substitute_in_body tsubst def in + let locals = V.VarId.vector_to_list locals in (* Evaluate the input operands *) let ctx1, args = eval_operands config ctx args in + assert (List.length args = def.A.arg_count); + + (* Push a frame delimiter *) + let ctx2 = ctx_push_frame ctx1 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) + (* 1. Push the return value *) + let ret_var, locals = + match locals with + | ret_ty :: locals -> (ret_ty, locals) + | _ -> failwith "Unreachable" in + let ctx3 = C.ctx_push_var ctx2 ret_var (C.mk_bottom ret_var.var_ty) 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" + (* 2. Push the input values *) + let input_locals, locals = + Utilities.list_split_at locals def.A.arg_count in + let inputs = List.combine input_locals args in + (* Note that this function checks that the variables and their values + have the same type (this is important) *) + let ctx4 = C.ctx_push_vars ctx3 inputs in - (* let ctx2 = ctx_push_var *) + (* 3. Push the remaining local variables (initialized as [Bottom]) *) + let ctx5 = C.ctx_push_uninitialized_vars ctx4 locals in - (* Third, push the inputs *) + (* Execute the function body *) + match eval_function_body config ctx5 body with + | Error Panic -> Error Panic + | Ok ctx6 -> + (* Pop the stack frame and retrieve the return value *) + let ctx7, ret_value = ctx_pop_frame config ctx6 in - (* Finally, put the remaining local variables (initialized as [Bottom]) *) + (* Move the return value to its destination *) + let ctx8 = assign_to_place config ctx7 ret_value dest in - (* TODO ... *) - raise Unimplemented + (* Return *) + Ok (ctx8, Unit)) | SymbolicMode -> raise Unimplemented +and eval_function_body (config : C.config) (ctx : C.eval_ctx) + (body : A.expression) : (C.eval_ctx, eval_error) result = + raise Unimplemented + 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 + +and eval_expression (config : C.config) (ctx : C.eval_ctx) (expr : A.expression) + : (C.eval_ctx * statement_eval_res) eval_result = + raise Unimplemented diff --git a/src/Utilities.ml b/src/Utilities.ml index 84cbd6e9..6452d56f 100644 --- a/src/Utilities.ml +++ b/src/Utilities.ml @@ -1,6 +1,7 @@ -(* Split a list at a given index i (the first list contains all the elements - up to element of index i, not included, the second one contains the remaining - elements *) +(* Split a list at a given index [i] (the first list contains all the elements + up to element of index [i], not included, the second one contains the remaining + elements. Note that the first returned list has length [i]. + *) let rec list_split_at (ls : 'a list) (i : int) = if i < 0 then raise (Invalid_argument "list_split_at take positive integers") else if i = 0 then ([], ls) |