Debug some issues in the interpreter

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