Update the env definition to make the frames easier to manipulate

6 files changed, 61 insertions, 51 deletions

diff --git a/src/Contexts.ml b/src/Contexts.ml
index d576083d..25865064 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -4,7 +4,12 @@ open Expressions
 open CfimAst
 open Errors
 
-type env_value = Var of var * typed_value | Abs of abs
+(** Environment value: mapping from variable to value, abstraction (only
+    used in symbolic mode) or stack frame delimiter.
+    
+    TODO: rename? Environment element or something?
+ *)
+type env_value = Var of var * typed_value | Abs of abs | Frame
 
 type env = env_value list
 
@@ -12,19 +17,10 @@ type interpreter_mode = ConcreteMode | SymbolicMode
 
 type config = { mode : interpreter_mode; check_invariants : bool }
 
-type stack_frame = { num_vars : int }
-(** A function frame
-
-    When using the interpreter in concrete mode (i.e, non symbolic) we
-    push a function frame whenever we enter a function body (and pop it
-    upon leaving it).
- *)
-
 type eval_ctx = {
   type_context : type_def TypeDefId.vector;
   fun_context : fun_def FunDefId.vector;
   type_vars : type_var TypeVarId.vector;
-  frames : stack_frame list;
   env : env;
   symbolic_counter : SymbolicValueId.generator;
   borrow_counter : BorrowId.generator;
@@ -48,7 +44,7 @@ let ctx_lookup_var (ctx : eval_ctx) (vid : VarId.id) : var =
     | [] ->
         raise (Invalid_argument ("Variable not found: " ^ VarId.to_string vid))
     | Var (var, _) :: env' -> if var.index = vid then var else lookup env'
-    | Abs _ :: env' -> lookup env'
+    | (Abs _ | Frame) :: env' -> lookup env'
   in
   lookup ctx.env
 
@@ -63,7 +59,7 @@ let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
   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 _ -> None
+    | Abs _ | Frame -> None
   in
   match List.find_map check_ev env with
   | None -> failwith "Unreachable"
@@ -83,6 +79,7 @@ let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env =
     match ev with
     | Var (var, v) -> if var.index = vid then Var (var, nv) else Var (var, v)
     | Abs abs -> Abs abs
+    | Frame -> Frame
   in
   List.map update_ev env
 
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 60441ce7..9e109709 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -97,8 +97,8 @@ let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
   let lookup_loan_in_env_value (ev : C.env_value) : V.loan_content option =
     match ev with
     | C.Var (_, v) -> lookup_loan_in_value ek l v
-    | C.Abs _ -> raise Unimplemented
-    (* TODO *)
+    | C.Abs _ -> raise Unimplemented (* TODO *)
+    | C.Frame -> None
   in
   match List.find_map lookup_loan_in_env_value env with
   | None -> failwith "Unreachable"
@@ -158,8 +158,8 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
   let update_loan_in_env_value (ev : C.env_value) : C.env_value =
     match ev with
     | C.Var (vid, v) -> Var (vid, update_loan_in_value ek l nlc v)
-    | C.Abs _ -> raise Unimplemented
-    (* TODO *)
+    | C.Abs _ -> raise Unimplemented (* TODO *)
+    | C.Frame -> C.Frame
   in
   List.map update_loan_in_env_value env
 
@@ -195,8 +195,8 @@ let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
   let lookup_borrow_in_env_value (ev : C.env_value) =
     match ev with
     | C.Var (_, v) -> lookup_borrow_in_value ek l v
-    | C.Abs _ -> raise Unimplemented
-    (* TODO *)
+    | C.Abs _ -> raise Unimplemented (* TODO *)
+    | C.Frame -> None
   in
   match List.find_map lookup_borrow_in_env_value env with
   | None -> failwith "Unreachable"
@@ -257,8 +257,8 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
   let update_borrow_in_env_value (ev : C.env_value) : C.env_value =
     match ev with
     | C.Var (vid, v) -> Var (vid, update_borrow_in_value ek l nbc v)
-    | C.Abs _ -> raise Unimplemented
-    (* TODO *)
+    | C.Abs _ -> raise Unimplemented (* TODO *)
+    | C.Frame -> C.Frame
   in
   List.map update_borrow_in_env_value env
 
@@ -362,8 +362,9 @@ let rec bottom_in_value (v : V.typed_value) : bool =
       raise Unimplemented
 
 (** See [end_borrow_get_borrow_in_env] *)
-let rec end_borrow_get_borrow_in_value config io l outer_borrows v0 :
-    V.typed_value * borrow_lres =
+let rec end_borrow_get_borrow_in_value (config : C.config) (io : inner_outer)
+    (l : V.BorrowId.id) (outer_borrows : borrow_ids option) (v0 : V.typed_value)
+    : V.typed_value * borrow_lres =
   match v0.V.value with
   | V.Concrete _ | V.Bottom | V.Symbolic _ -> (v0, NotFound)
   | V.Assumed (Box bv) ->
@@ -422,8 +423,9 @@ let rec end_borrow_get_borrow_in_value config io l outer_borrows v0 :
         in
         ({ v0 with value = V.Borrow (V.MutBorrow (l', bv')) }, res)
 
-and end_borrow_get_borrow_in_values config io l outer_borrows vl0 :
-    V.typed_value list * borrow_lres =
+and end_borrow_get_borrow_in_values (config : C.config) (io : inner_outer)
+    (l : V.BorrowId.id) (outer_borrows : borrow_ids option)
+    (vl0 : V.typed_value list) : V.typed_value list * borrow_lres =
   match vl0 with
   | [] -> (vl0, NotFound)
   | v :: vl -> (
@@ -447,8 +449,8 @@ and end_borrow_get_borrow_in_values config io l outer_borrows vl0 :
     borrows, we end them, and finally we end the borrow we wanted to end in the
     first place.
 *)
-let rec end_borrow_get_borrow_in_env (config : C.config) (io : inner_outer) l
-    env0 : C.env * borrow_lres =
+let rec end_borrow_get_borrow_in_env (config : C.config) (io : inner_outer)
+    (l : V.BorrowId.id) (env0 : C.env) : C.env * borrow_lres =
   match env0 with
   | [] -> ([], NotFound)
   | C.Var (x, v) :: env -> (
@@ -460,6 +462,7 @@ let rec end_borrow_get_borrow_in_env (config : C.config) (io : inner_outer) l
   | C.Abs _ :: _ ->
       assert (config.mode = SymbolicMode);
       raise Unimplemented
+  | C.Frame :: env -> end_borrow_get_borrow_in_env config io l env
 
 (** See [give_back_value]. *)
 let rec give_back_value_to_value config bid (v : V.typed_value)
@@ -574,6 +577,9 @@ let give_back_shared_to_abs _config _bid _abs : V.abs =
     
     When we end a mutable borrow, we need to "give back" the value it contained
     to its original owner by reinserting it at the proper position.
+
+    TODO: we must share that the borrow is somewhere in the environment, before
+    giving it back.
  *)
 let give_back_value (config : C.config) (bid : V.BorrowId.id)
     (v : V.typed_value) (env : C.env) : C.env =
@@ -584,6 +590,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
     | C.Abs abs ->
         assert (config.mode = SymbolicMode);
         C.Abs (give_back_value_to_abs config bid v abs)
+    | C.Frame -> C.Frame
   in
   List.map give_back_value_to_env_value env
 
@@ -600,6 +607,7 @@ let give_back_shared config (bid : V.BorrowId.id) (env : C.env) : C.env =
     | C.Abs abs ->
         assert (config.mode = SymbolicMode);
         C.Abs (give_back_shared_to_abs config bid abs)
+    | C.Frame -> C.Frame
   in
   List.map give_back_shared_to_env_value env
 
@@ -655,6 +663,7 @@ let reborrow_shared (config : C.config) (original_bid : V.BorrowId.id)
     | C.Abs abs ->
         assert (config.mode = SymbolicMode);
         C.Abs abs
+    | C.Frame -> C.Frame
   in
   List.map reborrow_in_ev env
 
@@ -1500,6 +1509,8 @@ let prepare_rplace (config : C.config) (access : access_kind) (p : E.place)
     - [eval_operand_prepare]
     - [eval_operand_apply]
     which are then used in [eval_operand] and [eval_operands].
+
+    TODO: this is not the proper way of doing
  *)
 let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand)
     : C.eval_ctx =
@@ -1895,6 +1906,7 @@ 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
   | A.Assign (p, rvalue) -> (
+      (* TODO: this is WRONG *)
       (* Prepare the rvalue, prepare the destination *)
       let ctx1 = eval_rvalue_prepare config ctx rvalue in
       let ctx2, _ = prepare_lplace config p ctx1 in
diff --git a/src/Print.ml b/src/Print.ml
index 156c9fe1..8d3e8745 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -394,9 +394,9 @@ module Contexts = struct
 
   let env_value_to_string (fmt : value_formatter) (ev : env_value) : string =
     match ev with
-    | Var (vid, tv) ->
-        var_id_to_string vid ^ " -> " ^ typed_value_to_string fmt tv
+    | Var (var, tv) -> var_to_string var ^ " -> " ^ typed_value_to_string fmt tv
     | Abs abs -> abs_to_string fmt abs
+    | Frame -> failwith "Can't print a Frame element"
 
   let env_to_string (fmt : value_formatter) (env : env) : string =
     "{\n"
@@ -426,8 +426,8 @@ module Contexts = struct
           Types.name_to_string def.name ^ "::" ^ variant.variant_name
     in
     let var_id_to_string vid =
-      let v = VarId.Map.find vid ctx.vars in
-      var_to_string v
+      let var = ctx_lookup_var ctx vid in
+      var_to_string var
     in
     {
       r_to_string;
@@ -437,32 +437,31 @@ module Contexts = struct
       var_id_to_string;
     }
 
-  let frame_to_string (fmt : ctx_formatter) (ctx : eval_ctx)
-      (frame : stack_frame) : string =
-    let var_binding_to_string (vid : VarId.id) : string =
-      let var = ctx_lookup_var ctx vid in
-      let v = ctx_lookup_var_value ctx vid in
-      let var_name =
-        match var.name with Some name -> "(" ^ name ^ ")" | None -> ""
-      in
-      "  @" ^ VarId.to_string var.index ^ var_name ^ " --> "
-      ^ typed_value_to_string fmt v
-    in
-    let vars =
-      String.concat ",\n" (List.map var_binding_to_string frame.vars)
+  (** 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)
+          * values: from the first pushed (oldest) to the last pushed
+       *)
+  let split_env_according_to_frames (env : env) : env list =
+    let rec split_aux (frames : env list) (curr_frame : env) (env : env) =
+      match env with
+      | [] -> frames
+      | Frame :: env' -> split_aux (curr_frame :: frames) [] env'
+      | ev :: env' -> split_aux frames (ev :: curr_frame) env'
     in
-    "[\n" ^ vars ^ "\n]"
+    let frames = split_aux [] [] env in
+    List.rev frames
 
   let eval_ctx_to_string (ctx : eval_ctx) : string =
     let fmt = eval_ctx_to_ctx_formatter ctx in
-    let num_frames = List.length ctx.frames in
+    let frames = split_env_according_to_frames ctx.env in
+    let num_frames = List.length frames in
     let frames =
       List.mapi
         (fun i f ->
-          "\n# Frame " ^ string_of_int i ^ ":\n" ^ frame_to_string fmt ctx f
-          ^ "\n")
-        ctx.frames
+          "\n# Frame " ^ string_of_int i ^ ":\n" ^ env_to_string fmt f ^ "\n")
+        frames
     in
-    let frames = List.rev frames in
     "# " ^ string_of_int num_frames ^ " frame(s)\n" ^ String.concat "" frames
 end
diff --git a/src/Substitute.ml b/src/Substitute.ml
index fa7016b1..dc2821f0 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -31,6 +31,7 @@ let rec ty_substitute (rsubst : 'r1 -> 'r2)
   | Never -> Never
   | Integer int_ty -> Integer int_ty
   | Str -> Str
+  | TypeVar vid -> tsubst vid
 
 (** Erase the regions in a type and substitute the type variables *)
 let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety)
diff --git a/src/dune b/src/dune
index aa3e7c37..eb2966f4 100644
--- a/src/dune
+++ b/src/dune
@@ -7,11 +7,11 @@
     :standard
     -safe-string
     -g
-    -warn-error -8-9-11-33-20-21-26-27-39
+    -warn-error -9-11-33-20-21-26-27-39
   ))
   (release (flags
     :standard
     -safe-string
     -g
-    -warn-error -8-9-11-33-20-21-26-27-39
+    -warn-error -9-11-33-20-21-26-27-39
   )))
diff --git a/src/main.ml b/src/main.ml
index 46a8b678..4fb91cea 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,5 +1,6 @@
 open CfimOfJson
 open Interpreter
+open Print
 
 (* This is necessary to have a backtrace when raising exceptions - for some
  * reason, the -g option doesn't work *)