From 7f0dc28713323c7546c4ac627c216133461ddd89 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 13 Feb 2024 00:28:07 +0100
Subject: Add logging information

---
 compiler/InterpreterLoopsCore.ml       |  1 +
 compiler/InterpreterLoopsFixedPoint.ml | 16 ++++++++++++++++
 compiler/InterpreterStatements.ml      |  7 +++++++
 3 files changed, 24 insertions(+)

(limited to 'compiler')

diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index e663eb42..0bd57756 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -12,6 +12,7 @@ type updt_env_kind =
   | AbsInRight of AbstractionId.id
   | LoanInRight of BorrowId.id
   | LoansInRight of BorrowId.Set.t
+[@@deriving show]
 
 (** Utility exception *)
 exception ValueMatchFailure of updt_env_kind
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 4dabe974..c9bad3ef 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -352,6 +352,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
 
   let cf_exit_loop_body (res : statement_eval_res) : m_fun =
    fun ctx ->
+    log#ldebug (lazy "compute_loop_entry_fixed_point: cf_exit_loop_body");
     match res with
     | Return | Panic | Break _ -> None
     | Unit ->
@@ -377,6 +378,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
      context (the context at the loop entry, after we called
      {!prepare_ashared_loans}, if this is the first iteration) *)
   let join_ctxs (ctx1 : eval_ctx) : eval_ctx =
+    log#ldebug (lazy "compute_loop_entry_fixed_point: join_ctxs");
     (* If this is the first iteration, end the borrows/loans/abs which
        appear in ctx1 and not in the other contexts, then compute the
        set of fixed ids. This means those borrows/loans have to end
@@ -400,6 +402,15 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
             ctx
           in
           (* End the borrows/abs in [ctx1] *)
+          log#ldebug
+            (lazy
+              ("compute_loop_entry_fixed_point: join_ctxs: ending \
+                borrows/abstractions before entering the loop:\n\
+                - ending borrow ids: "
+              ^ BorrowId.Set.to_string None blids
+              ^ "\n- ending abstraction ids: "
+              ^ AbstractionId.Set.to_string None aids
+              ^ "\n\n"));
           let ctx1 = end_borrows_abs blids aids ctx1 in
           (* We can also do the same in the contexts [ctxs]: if there are
              several contexts, maybe one of them ended some borrows and some
@@ -420,6 +431,8 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
     ctxs := [];
     ctx2
   in
+  log#ldebug (lazy "compute_loop_entry_fixed_point: after join_ctxs");
+
   (* Compute the set of fixed ids - for the symbolic ids, we compute the
      intersection of ids between the original environment and the list
      of new environments *)
@@ -440,6 +453,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
      existentially quantified borrows/abstractions/symbolic values.
   *)
   let equiv_ctxs (ctx1 : eval_ctx) (ctx2 : eval_ctx) : bool =
+    log#ldebug (lazy "compute_fixed_point: equiv_ctx:");
     let fixed_ids = compute_fixed_ids [ ctx1; ctx2 ] in
     let check_equivalent = true in
     let lookup_shared_value _ = raise (Failure "Unreachable") in
@@ -531,6 +545,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
     in
     let cf_loop : st_m_fun =
      fun res ctx ->
+      log#ldebug (lazy "compute_loop_entry_fixed_point: cf_loop");
       match res with
       | Continue _ | Panic ->
           (* We don't want to generate anything *)
@@ -544,6 +559,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
           *)
           raise (Failure "Unreachable")
       | Return ->
+          log#ldebug (lazy "compute_loop_entry_fixed_point: cf_loop: Return");
           (* Should we consume the return value and pop the frame?
            * If we check in [Interpreter] that the loop abstraction we end is
            * indeed the correct one, I think it is sound to under-approximate here
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 97c8bcd6..0cf8b88a 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -933,6 +933,11 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
   (* Evaluate *)
   let cf_eval_st cf : m_fun =
    fun ctx ->
+    log#ldebug
+      (lazy
+        ("\neval_statement: cf_eval_st: statement:\n"
+        ^ statement_to_string_with_tab ctx st
+        ^ "\n\n"));
     match st.content with
     | Assign (p, rvalue) -> (
         (* We handle global assignments separately *)
@@ -1520,8 +1525,10 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id)
 (** Evaluate a statement seen as a function body *)
 and eval_function_body (config : config) (body : statement) : st_cm_fun =
  fun cf ctx ->
+  log#ldebug (lazy "eval_function_body:");
   let cc = eval_statement config body in
   let cf_finish cf res =
+    log#ldebug (lazy "eval_function_body: cf_finish");
     (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we
      * delegate the check to the caller. *)
     (* Expand the symbolic values if necessary - we need to do that before
-- 
cgit v1.2.3