summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-30 09:33:29 +0100
committerSon Ho2021-11-30 09:33:29 +0100
commit4aeb5a70952280bc90fea1014d8097e3639896e5 (patch)
treea166306cdb53973613257c887be193ac473c8bd2
parent603fe74932fa669ed51a3c84e91710267519b133 (diff)
Debug some issues in the interpreter
-rw-r--r--src/Contexts.ml37
-rw-r--r--src/Interpreter.ml26
-rw-r--r--src/Print.ml38
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