From c1473942f0aa0dba524eb7fe08f149488ecc2a6d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 6 Jan 2023 18:10:38 +0100
Subject: Implement a pass to filter shallow borrows

---
 compiler/InterpreterExpressions.ml |  9 ++---
 compiler/PrePasses.ml              | 81 +++++++++++++++++++++++++++++++++++++-
 compiler/Print.ml                  |  2 +-
 3 files changed, 85 insertions(+), 7 deletions(-)

(limited to 'compiler')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 82d8586a..d75f5a26 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -549,12 +549,11 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
  fun ctx ->
   match bkind with
   | E.Shared | E.TwoPhaseMut | E.Shallow ->
-      (* **REMARK**: we treat shallow borrows like shared borrows. In theory,
-         this is incomplete. But in practice, this should allow to handle
-         many cases: in effect, we are simply forbidding match guards from
-         performing too many modifications in the environment, which is
-         probably not a too bad thing to do.
+      (* **REMARK**: we initially treated shallow borrows like shared borrows.
+         In practice this restricted the behaviour too much, so for now we
+         forbid them.
       *)
+      assert (bkind <> E.Shallow);
 
       (* Access the value *)
       let access =
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index be154539..a0c01384 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -259,8 +259,87 @@ let remove_loop_breaks (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
       ^ "\n"));
   f
 
+(** Remove the use of shallow borrows from a function.
+
+    In theory, this allows the code to do more things than what Rust allows,
+    and in particular it would allow to modify the variant of an enumeration
+    in a guard, while matching over this enumeration.
+
+    In practice, this is not a soundness issue.
+
+    The pass is implemented as follows:
+    - we look for all the variables which appear in pattern of the form and
+      remove them:
+      {[
+        let x = &shallow ...;
+        ...
+      ]}
+    - whenever we find such a variable [x], we remove all the subsequent
+      occurrences of [fake_read(x)].
+
+    We then check that [x] completely disappeared from the function body (for
+    sanity).
+ *)
+let remove_shallow_borrows (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
+  let f0 = f in
+  let filter_in_body (body : A.statement) : A.statement =
+    let filtered = ref E.VarId.Set.empty in
+
+    let filter_visitor =
+      object
+        inherit [_] A.map_statement as super
+
+        method! visit_Assign env p rv =
+          match (p.projection, rv) with
+          | [], E.Ref (_, E.Shallow) ->
+              (* Filter *)
+              filtered := E.VarId.Set.add p.var_id !filtered;
+              Nop
+          | _ ->
+              (* Don't filter *)
+              super#visit_Assign env p rv
+
+        method! visit_FakeRead env p =
+          if p.projection = [] && E.VarId.Set.mem p.var_id !filtered then
+            (* Filter *)
+            Nop
+          else super#visit_FakeRead env p
+      end
+    in
+
+    (* Filter the variables *)
+    let body = filter_visitor#visit_statement () body in
+
+    (* Check that the filtered variables completely disappeared from the body *)
+    let check_visitor =
+      object
+        inherit [_] A.iter_statement
+        method! visit_var_id _ id = assert (not (E.VarId.Set.mem id !filtered))
+      end
+    in
+    check_visitor#visit_statement () body;
+
+    (* Return the updated body *)
+    body
+  in
+
+  let body =
+    match f.body with
+    | None -> None
+    | Some body -> Some { body with body = filter_in_body body.body }
+  in
+  let f = { f with body } in
+  log#ldebug
+    (lazy
+      ("Before/after [remove_shallow_borrows]:\n"
+      ^ Print.Crate.crate_fun_decl_to_string crate f0
+      ^ "\n\n"
+      ^ Print.Crate.crate_fun_decl_to_string crate f
+      ^ "\n"));
+  f
+
 let apply_passes (crate : A.crate) : A.crate =
-  let passes = [ remove_loop_breaks crate ] in
+  let passes = [ remove_loop_breaks crate; remove_shallow_borrows crate ] in
   let functions =
     List.fold_left (fun fl pass -> List.map pass fl) crate.functions passes
   in
diff --git a/compiler/Print.ml b/compiler/Print.ml
index cf227172..f544c0db 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -343,7 +343,7 @@ module Contexts = struct
   let var_binder_to_string (bv : C.var_binder) : string =
     match bv.name with
     | None -> PV.var_id_to_string bv.index
-    | Some name -> name
+    | Some name -> name ^ "^" ^ E.VarId.to_string bv.index
 
   let dummy_var_id_to_string (bid : C.DummyVarId.id) : string =
     "_@" ^ C.DummyVarId.to_string bid
-- 
cgit v1.2.3