diff options
| -rw-r--r-- | src/Contexts.ml | 37 | ||||
| -rw-r--r-- | src/Interpreter.ml | 26 | ||||
| -rw-r--r-- | src/Print.ml | 38 |
3 files changed, 72 insertions, 29 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index f182add5..8a498e2e 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -58,15 +58,17 @@ 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 - | Abs _ | Frame -> None + (* We take care to stop at the end of current frame: different variables + in different frames can have the same id! + *) + let rec lookup env = + match env with + | [] -> failwith "Unexpected" + | Var (var, v) :: env' -> if var.index = vid then v else lookup env' + | Abs _ :: env' -> lookup env' + | Frame :: _ -> failwith "End of frame" in - match List.find_map check_ev env with - | None -> failwith "Unreachable" - | Some v -> v + lookup env (** Retrieve a variable's value in an evaluation context *) let ctx_lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value = @@ -78,14 +80,19 @@ 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) - | Abs abs -> Abs abs - | Frame -> Frame + (* We take care to stop at the end of current frame: different variables + in different frames can have the same id! + *) + let rec update env = + match env with + | [] -> failwith "Unexpected" + | Var (var, v) :: env' -> + if var.index = vid then Var (var, nv) :: env' + else Var (var, v) :: update env' + | Abs abs :: env' -> Abs abs :: update env' + | Frame :: _ -> failwith "End of frame" in - List.map update_ev env + update env (** Update a variable's value in an evaluation context. diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 90df16ed..c0efc0cc 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -23,6 +23,10 @@ module L = Logging let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string +let typed_value_to_string = Print.EvalCtxCfimAst.typed_value_to_string + +let operand_to_string = Print.EvalCtxCfimAst.operand_to_string + let statement_to_string = Print.EvalCtxCfimAst.statement_to_string let expression_to_string ctx = @@ -1128,7 +1132,14 @@ let read_place (config : C.config) (access : access_kind) (p : E.place) (* Note that we ignore the new environment: it should be the same as the original one. *) - if config.check_invariants then assert (env1 = env); + if config.check_invariants then + if env1 <> env then ( + let msg = + "Unexpected environment update:\nNew environment:\n" + ^ C.show_env env1 ^ "\n\nOld environment:\n" ^ C.show_env env + in + L.log#serror msg; + failwith "Unexpected environment update"); Ok read_value let read_place_unwrap (config : C.config) (access : access_kind) (p : E.place) @@ -1595,6 +1606,12 @@ let prepare_rplace (config : C.config) (access : access_kind) (p : E.place) (** Evaluate an operand. *) let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : C.eval_ctx * V.typed_value = + (* Debug *) + L.log#ldebug + (lazy + ("eval_operand:\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n- op:\n" + ^ operand_to_string ctx op ^ "\n")); + (* Evaluate *) match op with | Expressions.Constant (ty, cv) -> let v = constant_value_to_typed_value ctx ty cv in @@ -1604,6 +1621,7 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : let access = Read in let ctx1, v = prepare_rplace config access p ctx in (* Copy the value *) + L.log#ldebug (lazy ("Value to copy:\n" ^ typed_value_to_string ctx1 v)); assert (not (bottom_in_value v)); copy_value config ctx1 v | Expressions.Move p -> ( @@ -1611,6 +1629,7 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : let access = Move in let ctx1, v = prepare_rplace config access p ctx in (* Move the value *) + L.log#ldebug (lazy ("Value to move:\n" ^ typed_value_to_string ctx1 v)); assert (not (bottom_in_value v)); let bottom = { V.value = Bottom; ty = v.ty } in match write_place config access p bottom ctx1.env with @@ -1953,6 +1972,9 @@ let get_non_local_function_return_type (fid : A.assumed_fun_id) *) let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + (* Debug *) + L.log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx)); + (* Eval *) let ret_vid = V.VarId.zero in (* List the local variables, but the return variable *) let rec list_locals env = @@ -1961,7 +1983,7 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) : | 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 + if var.index <> ret_vid then var.index :: locals else locals | C.Frame :: _ -> [] in let locals = list_locals ctx.env in diff --git a/src/Print.ml b/src/Print.ml index 9cdde188..d1bf5f47 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -473,7 +473,7 @@ module Contexts = struct (** Split an [env] at every occurrence of [Frame], eliminating those elements. Also reorders the frames and the values in the frames according to the following order: - * frames: from the first pushed (oldest) to the last pushed (current frame) + * frames: from the current frame to the first pushed (oldest frame) * values: from the first pushed (oldest) to the last pushed *) let split_env_according_to_frames (env : C.env) : C.env list = @@ -485,7 +485,7 @@ module Contexts = struct | ev :: env' -> split_aux frames (ev :: curr_frame) env' in let frames = split_aux [] [] env in - List.rev frames + frames let eval_ctx_to_string (ctx : C.eval_ctx) : string = let fmt = eval_ctx_to_ctx_formatter ctx in @@ -688,7 +688,7 @@ module CfimAst = struct let cond = operand_to_string fmt a.A.cond in if a.A.expected then "assert(" ^ cond ^ ")" else "assert(¬" ^ cond ^ ")" - | A.Call call -> ( + | A.Call call -> let ty_fmt = ast_to_etype_formatter fmt in let params = if List.length call.A.type_params > 0 then @@ -698,15 +698,21 @@ module CfimAst = struct ^ ">" else "" in - match call.A.func with - | A.Local fid -> fmt.fun_def_id_to_string fid ^ params - | A.Assumed fid -> ( - match fid with - | A.BoxNew -> "alloc::boxed::Box" ^ params ^ "::new" - | A.BoxDeref -> "core::ops::deref::Deref<Box" ^ params ^ ">::deref" - | A.BoxDerefMut -> - "core::ops::deref::DerefMut<Box" ^ params ^ ">::deref_mut" - | A.BoxFree -> "alloc::alloc::box_free<" ^ params ^ ">")) + let args = List.map (operand_to_string fmt) call.A.args in + let args = "(" ^ String.concat ", " args ^ ")" in + let name_params = + match call.A.func with + | A.Local fid -> fmt.fun_def_id_to_string fid ^ params + | A.Assumed fid -> ( + match fid with + | A.BoxNew -> "alloc::boxed::Box" ^ params ^ "::new" + | A.BoxDeref -> + "core::ops::deref::Deref<Box" ^ params ^ ">::deref" + | A.BoxDerefMut -> + "core::ops::deref::DerefMut" ^ params ^ "::deref_mut" + | A.BoxFree -> "alloc::alloc::box_free" ^ params) + in + name_params ^ args | A.Panic -> "panic" | A.Return -> "return" | A.Break i -> "break " ^ string_of_int i @@ -908,6 +914,14 @@ end (** Pretty-printing for ASTs (functions based on an evaluation context) *) module EvalCtxCfimAst = struct + let typed_value_to_string (ctx : C.eval_ctx) (v : V.typed_value) : string = + let fmt = PC.eval_ctx_to_ctx_formatter ctx in + PV.typed_value_to_string fmt v + + let operand_to_string (ctx : C.eval_ctx) (op : E.operand) : string = + let fmt = PA.eval_ctx_to_ast_formatter ctx in + PA.operand_to_string fmt op + let statement_to_string (ctx : C.eval_ctx) (s : A.statement) : string = let fmt = PA.eval_ctx_to_ast_formatter ctx in PA.statement_to_string fmt s |