From dbbb01630190d999d3932fabd8a181b4f826f64f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 7 Jan 2022 11:00:05 +0100
Subject: Improve logging and introduce eval_operands_prepare

---
 src/InterpreterExpansion.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'src/InterpreterExpansion.ml')

diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 345c3df3..aebcda3c 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -16,6 +16,9 @@ open InterpreterUtils
 open InterpreterProjectors
 open InterpreterBorrows
 
+(** The local logger *)
+let log = L.expansion_log
+
 (** Projector kind *)
 type proj_kind = LoanProj | BorrowProj
 
@@ -366,6 +369,8 @@ let expand_symbolic_value_borrow (config : C.config)
 let expand_symbolic_value_no_branching (config : C.config)
     (pe : E.projection_elem) (sp : V.symbolic_value) (ctx : C.eval_ctx) :
     C.eval_ctx =
+  (* Remember the initial context for printing purposes *)
+  let ctx0 = ctx in
   (* Compute the expanded value - note that when doing so, we may introduce
    * fresh symbolic values in the context (which thus gets updated) *)
   let original_sv = sp in
@@ -424,6 +429,14 @@ let expand_symbolic_value_no_branching (config : C.config)
         failwith
           ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)
   in
+  (* Debugging *)
+  (* Debug *)
+  log#ldebug
+    (lazy
+      ("expand_symbolic_value: "
+      ^ symbolic_value_to_string ctx0 sp
+      ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
+      ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
   (* Sanity check: the symbolic value has disappeared *)
   assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx));
   (* Return *)
-- 
cgit v1.2.3


From 8917bf6aca4465873e7e7642719c70789d97590c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 7 Jan 2022 12:39:58 +0100
Subject: Add an optional borrow identifier to AIgnoredMutBorrow, introduce the
 AEndedIgnoredMutBorrow variant and fix a couple of bugs

---
 src/InterpreterExpansion.ml | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

(limited to 'src/InterpreterExpansion.ml')

diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index aebcda3c..e19f8bb4 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -63,15 +63,17 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
     object
       inherit [_] C.map_eval_ctx as super
 
-      method! visit_abs proj_regions abs =
-        assert (Option.is_none proj_regions);
-        let proj_regions = Some abs.V.regions in
-        super#visit_abs proj_regions abs
+      method! visit_abs current_abs abs =
+        assert (Option.is_none current_abs);
+        let current_abs = Some abs in
+        super#visit_abs current_abs abs
       (** When visiting an abstraction, we remember the regions it owns to be
           able to properly reduce projectors when expanding symbolic values *)
 
-      method! visit_ASymbolic proj_regions aproj =
-        let proj_regions = Option.get proj_regions in
+      method! visit_ASymbolic current_abs aproj =
+        let current_abs = Option.get current_abs in
+        let proj_regions = current_abs.regions in
+        let ancestors_regions = current_abs.ancestors_regions in
         match (aproj, proj_kind) with
         | V.AProjLoans sv, LoanProj ->
             (* Check if this is the symbolic value we are looking for *)
@@ -85,7 +87,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
               projected_value.V.value
             else
               (* Not the searched symbolic value: nothing to do *)
-              super#visit_ASymbolic (Some proj_regions) aproj
+              super#visit_ASymbolic (Some current_abs) aproj
         | V.AProjBorrows (sv, proj_ty), BorrowProj ->
             (* Check if this is the symbolic value we are looking for *)
             if same_symbolic_id sv original_sv then
@@ -101,16 +103,16 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
               (* Apply the projector *)
               let projected_value =
                 apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                  proj_regions expansion proj_ty
+                  proj_regions ancestors_regions expansion proj_ty
               in
               (* Replace *)
               projected_value.V.value
             else
               (* Not the searched symbolic value: nothing to do *)
-              super#visit_ASymbolic (Some proj_regions) aproj
+              super#visit_ASymbolic (Some current_abs) aproj
         | V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj ->
             (* Nothing to do *)
-            super#visit_ASymbolic (Some proj_regions) aproj
+            super#visit_ASymbolic (Some current_abs) aproj
     end
   in
   (* Apply the expansion *)
-- 
cgit v1.2.3