Repository: aptos-labs/aptos-core (language: python)

Issue:
[Bug][move-compiler-v2] COPYLOC_EXISTS_BORROW_ERROR for mutable ownership violation
# 🐛 Bug

```move
module 0xCAFE::Module0 {
    public fun f1(x: bool) {
        let y: &mut bool =  &mut x;
        if (x) {
        } else {
            *y= false;
        };
        if (copy x) { } else { };
    }
}
```

Compiling with V1 will report an ownership error:
```
error[E07002]: mutable ownership violated
  ┌─ ~/debug_package/sources/repro.move:4:13
  │
3 │         let y: &mut bool =  &mut x;
  │                             ------ It is still being mutably borrowed by this reference
4 │         if (x) {
  │             ^ Invalid copy of variable 'x'
```

However, compiling with V2 will report a bytecode verifier error `COPYLOC_EXISTS_BORROW_ERROR` instead of a compiler error:
```
bug: bytecode verification failed with unexpected status code `COPYLOC_EXISTS_BORROW_ERROR`. This is a compiler bug, consider reporting it.
  ┌─ ~/debug_package/sources/repro.move:4:9
  │  
4 │ ╭         if (x) {
5 │ │         } else {
6 │ │             *y= false;
7 │ │         };
  │ ╰─────────^
```


Discussion / hints:

Fix patch:
diff --git a/third_party/move/move-compiler-v2/src/pipeline/reference_safety_processor.rs b/third_party/move/move-compiler-v2/src/pipeline/reference_safety_processor.rs
index 1bc0f468233fc..87fa16953085c 100644
--- a/third_party/move/move-compiler-v2/src/pipeline/reference_safety_processor.rs
+++ b/third_party/move/move-compiler-v2/src/pipeline/reference_safety_processor.rs
@@ -915,6 +915,8 @@ enum ReadMode {
     Copy,
     /// The local is transferred as an argument to another function
     Argument,
+    /// The local is used as a branch condition
+    BranchCondition,
 }
 
 impl<'env> LifeTimeAnalysis<'env> {
@@ -1051,6 +1053,26 @@ impl<'env, 'state> LifetimeAnalysisStep<'env, 'state> {
                         true
                     }
                 },
+                ReadMode::BranchCondition => {
+                    // Mutable borrow not allowed
+                    if self.state.has_mut_edges(label) {
+                        self.error_with_hints(
+                            loc,
+                            format!(
+                                "cannot use {} which is still mutably \
+                                    borrowed as branch condition",
+                                self.display(local)
+                            ),
+                            "used in this context",
+                            self.borrow_info(label, |_| true)
+                                .into_iter()
+                                .chain(usage_info()),
+                        );
+                        false
+                    } else {
+                        true
+                    }
+                },
             }
         } else {
             true
@@ -1990,6 +2012,9 @@ impl<'env> TransferFunctions for LifeTimeAnalysis<'env> {
                 step.assign(*dest, *src, *kind);
             },
             Ret(_, srcs) => step.return_(srcs),
+            Branch(_, _, _, src) => {
+                step.check_read_local(*src, ReadMode::BranchCondition);
+            },
             Call(_, dests, oper, srcs, _) => {
                 use Operation::*;
                 match oper {


Test patch:
diff --git a/third_party/move/move-compiler-v2/tests/reference-safety/bug_13973_branch_cond_borrowed.exp b/third_party/move/move-compiler-v2/tests/reference-safety/bug_13973_branch_cond_borrowed.exp
new file mode 100644
index 0000000000000..51395ce1543b5
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/reference-safety/bug_13973_branch_cond_borrowed.exp
@@ -0,0 +1,24 @@
+
+Diagnostics:
+error: cannot use local `x` which is still mutably borrowed as branch condition
+  ┌─ tests/reference-safety/bug_13973_branch_cond_borrowed.move:4:9
+  │
+3 │           let y: &mut bool =  &mut x;
+  │                               ------ previous mutable local borrow
+4 │ ╭         if (x) {
+5 │ │         } else {
+6 │ │             *y= false;
+  │ │             --------- conflicting reference `y` used here
+7 │ │         };
+  │ ╰─────────^ used in this context
+
+error: cannot use local `x` which is still mutably borrowed as branch condition
+   ┌─ tests/reference-safety/bug_13973_branch_cond_borrowed.move:13:9
+   │
+12 │           let y: &mut bool =  &mut x;
+   │                               ------ previous mutable local borrow
+13 │ ╭         while (x) {
+14 │ │             *y= false;
+   │ │             --------- conflicting reference `y` used here
+15 │ │         };
+   │ ╰─────────^ used in this context
diff --git a/third_party/move/move-compiler-v2/tests/reference-safety/bug_13973_branch_cond_borrowed.move b/third_party/move/move-compiler-v2/tests/reference-safety/bug_13973_branch_cond_borrowed.move
new file mode 100644
index 0000000000000..ca1bfb39e4933
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/reference-safety/bug_13973_branch_cond_borrowed.move
@@ -0,0 +1,19 @@
+module 0xCAFE::Module0 {
+    public fun f1(x: bool) {
+        let y: &mut bool =  &mut x;
+        if (x) {
+        } else {
+            *y= false;
+        };
+        if (copy x) { } else { };
+    }
+
+    public fun f2(x: bool) {
+        let y: &mut bool =  &mut x;
+        while (x) {
+            *y= false;
+        };
+        if (copy x) { } else { };
+    }
+
+}
diff --git a/third_party/move/move-compiler-v2/tests/reference-safety/bug_13973_branch_cond_borrowed.no-opt.exp b/third_party/move/move-compiler-v2/tests/reference-safety/bug_13973_branch_cond_borrowed.no-opt.exp
new file mode 100644
index 0000000000000..51395ce1543b5
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/reference-safety/bug_13973_branch_cond_borrowed.no-opt.exp
@@ -0,0 +1,24 @@
+
+Diagnostics:
+error: cannot use local `x` which is still mutably borrowed as branch condition
+  ┌─ tests/reference-safety/bug_13973_branch_cond_borrowed.move:4:9
+  │
+3 │           let y: &mut bool =  &mut x;
+  │                               ------ previous mutable local borrow
+4 │ ╭         if (x) {
+5 │ │         } else {
+6 │ │             *y= false;
+  │ │             --------- conflicting reference `y` used here
+7 │ │         };
+  │ ╰─────────^ used in this context
+
+error: cannot use local `x` which is still mutably borrowed as branch condition
+   ┌─ tests/reference-safety/bug_13973_branch_cond_borrowed.move:13:9
+   │
+12 │           let y: &mut bool =  &mut x;
+   │                               ------ previous mutable local borrow
+13 │ ╭         while (x) {
+14 │ │             *y= false;
+   │ │             --------- conflicting reference `y` used here
+15 │ │         };
+   │ ╰─────────^ used in this context
diff --git a/third_party/move/move-compiler-v2/tests/testsuite.rs b/third_party/move/move-compiler-v2/tests/testsuite.rs
index e940d1aa6ab4e..10de13ae4b13a 100644
--- a/third_party/move/move-compiler-v2/tests/testsuite.rs
+++ b/third_party/move/move-compiler-v2/tests/testsuite.rs
@@ -281,7 +281,7 @@ const TEST_CONFIGS: Lazy<BTreeMap<&str, TestConfig>> = Lazy::new(|| {
             dump_ast: DumpLevel::None,
             dump_bytecode: DumpLevel::None,
             dump_bytecode_filter:
-            // For debugging:
+            // For debugging (dump_bytecode set DumpLevel::AllStages)
              Some(vec![
                INITIAL_BYTECODE_STAGE,
                "ReferenceSafetyProcessor",