From 9a94302823e07c4e8a50ea4e67c8f61e8827c23c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 7 Jan 2023 11:25:51 +0100
Subject: Add a comment for PrePasses.remove_shallow_borrows
---
compiler/PrePasses.ml | 89 +++++++++++++++++++++++++++++++++++++++++++++++++--
1 file changed, 87 insertions(+), 2 deletions(-)
(limited to 'compiler')
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index a0c01384..8b193ee2 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -267,9 +267,94 @@ let remove_loop_breaks (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
In practice, this is not a soundness issue.
+ **Soundness**:
+ ==============
+ For instance, let's consider the following Rust code:
+ {[
+ match ls : &mut List<u32> {
+ Nil => return None,
+ Cons(hd, tl) if *hd > 0 => return Some(hd),
+ Cons(hd, tl) => ...,
+ }
+ ]}
+
+ The Rust compiler enforces the fact that the guard doesn't modify the
+ variant of [ls]. It does so by compiling to (approximately) the following
+ MIR code:
+ {[
+ let d = discriminant( *ls);
+ switch d {
+ 0 => ... // Nil case
+ 1 => { // Cons case
+ // Introduce hd and tl
+ hd := &mut ( *ls as Cons).0;
+ tl := &mut ( *ls as Cons).1;
+
+ // Evaluate the guard
+ tmp := &shallow *ls; // Create a shallow borrow of ls
+ b := *hd > 0;
+ fake_read(tmp); // Make sure the shallow borrow lives until the end of the guard
+
+ // We evaluated the guard: go to the proper branch
+ if b then {
+ ... // First Cons branch
+ }
+ else {
+ ... // Second Cons branch
+ }
+ }
+ }
+ ]}
+
+ Shallow borrows are a bit like shared borrows but with the following
+ difference:
+ - they do forbid modifying the value directly below the loan
+ - but they allow modifying a strict subvalue
+ For instance, above, for as long as [tmp] lives:
+ - we can't change the variant of [*ls]
+ - but we can update [hd] and [tl]
+
+ On our side, we have to pay attention to two things:
+ - Removing shallow borrows don't modify the behavior of the program.
+ In practice, adding shallow borrows can lead to a MIR program being
+ rejected, but it doesn't change this program's behavior.
+
+ Regarding this, there is something important. At the top-level AST,
+ if the guard modifies the variant (say, to [Nil]) and evaluates to [false],
+ then we go to the second [Cons] branch, which doesn't really make sense
+ (though it is not a soundness issue - for soundness, see next point).
+
+ At the level of MIR, as the match has been desugared, there is no issue
+ in modifying the variant of the scrutinee.
+
+ - We have to make sure the evaluation in sound. In particular, modifying
+ the variant of [*ls] should invalidate [hd] and [tl]. This is important
+ for the Rust compiler to enforce this on its side. In the case of LLBC,
+ we don't need additional constraints because modifying [*ls] will
+ indeed invalidate [hd] and [tl].
+
+ More specifically, at the beginning of the [Cons] branch and just after
+ we introduced [hd] and [tl] we have the following environment:
+ {[
+ ... // l0 comes from somewhere - we omit the corresponding loan
+ ls -> MB l0 (Cons (ML l1) (ML l2))
+ hd -> MB l1 s1
+ tl -> MB l2 s2
+ ]}
+
+ If we evaluate: [*ls := Nil], we get:
+ {[
+ ... // l0 comes from somewhere - we omit the corresponding loan
+ ls -> MB l0 Nil
+ hd -> ⊥ // invalidated
+ tl -> ⊥ // invalidated
+ ]}
+
+ **Implementation**:
+ ===================
The pass is implemented as follows:
- - we look for all the variables which appear in pattern of the form and
- remove them:
+ - we look for all the variables which appear in pattern of the following
+ shape and remove them:
{[
let x = &shallow ...;
...
--
cgit v1.2.3