Make good progress on eval_local_function_call

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)