check use of variable in spec by default in live analysis

third_party/move/move-compiler-v2/src/pipeline/livevar_analysis_processor.rs

@@ -198,9 +198,7 @@ impl FunctionTargetProcessor for LiveVarAnalysisProcessor {
 impl LiveVarAnalysisProcessor {
     /// Create a new instance of live variable analysis.
     /// `track_all_usages` determines whether both primary and secondary usages of a variable are
-    /// tracked (when true), or only the primary usages (when false). Also, if set, all usages
-    /// of temporaries in specifications are tracked, which are considered as secondary because
-    /// they are not part of the execution semantics.
+    /// tracked (when true), or only the primary usages (when false).
     /// Unless all usages are needed, it is recommended to set `track_all_usages` to false.
     pub fn new(track_all_usages: bool) -> Self {
         Self { track_all_usages }
@@ -373,12 +371,12 @@ impl<'a> TransferFunctions for LiveVarAnalysis<'a> {
             Branch(id, _, _, src) => {
                 state.insert_or_update(*src, self.livevar_info(id, offset), self.track_all_usages);
             },
-            Prop(id, _, exp) if self.track_all_usages => {
+            Prop(id, _, exp) => {
                 for idx in exp.used_temporaries() {
                     state.insert_or_update(idx, self.livevar_info(id, offset), true);
                 }
             },
-            SpecBlock(id, spec) if self.track_all_usages => {
+            SpecBlock(id, spec) => {
                 for idx in spec.used_temporaries() {
                     state.insert_or_update(idx, self.livevar_info(id, offset), true);
                 }

third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.exp

@@ -0,0 +1,114 @@
+
+============ disassembled file-format ==================
+// Move bytecode v7
+module c0ffee.m {
+use 0000000000000000000000000000000000000000000000000000000000000001::option;
+use 0000000000000000000000000000000000000000000000000000000000000001::vector;
+
+
+struct T has copy, drop, store {
+	issuer: vector<u8>,
+	version: u64
+}
+struct J has copy, drop, store {
+	variant: u64
+}
+struct S has copy, drop, store {
+	entries: vector<T>
+}
+
+test(Arg0: &mut S, Arg1: vector<u8>): Option<T> /* def_idx: 0 */ {
+L2:	loc0: &vector<T>
+L3:	loc1: bool
+L4:	loc2: u64
+L5:	loc3: u64
+L6:	loc4: u64
+L7:	loc5: &T
+L8:	loc6: &T
+L9:	loc7: u64
+L10:	loc8: bool
+L11:	loc9: u64
+L12:	loc10: Option<T>
+L13:	loc11: Option<T>
+B0:
+	0: CopyLoc[0](Arg0: &mut S)
+	1: ImmBorrowField[0](S.entries: vector<T>)
+	2: StLoc[2](loc0: &vector<T>)
+	3: LdFalse
+	4: StLoc[3](loc1: bool)
+	5: LdU64(0)
+	6: StLoc[4](loc2: u64)
+	7: LdU64(0)
+	8: CopyLoc[2](loc0: &vector<T>)
+	9: VecLen(2)
+	10: StLoc[5](loc3: u64)
+	11: StLoc[6](loc4: u64)
+B1:
+	12: CopyLoc[6](loc4: u64)
+	13: CopyLoc[5](loc3: u64)
+	14: Lt
+	15: BrFalse(41)
+B2:
+	16: CopyLoc[2](loc0: &vector<T>)
+	17: CopyLoc[6](loc4: u64)
+	18: VecImmBorrow(2)
+	19: StLoc[7](loc5: &T)
+	20: MoveLoc[7](loc5: &T)
+	21: StLoc[8](loc6: &T)
+	22: MoveLoc[8](loc6: &T)
+	23: ImmBorrowField[1](T.issuer: vector<u8>)
+	24: ReadRef
+	25: CopyLoc[1](Arg1: vector<u8>)
+	26: Eq
+	27: BrFalse(34)
+B3:
+	28: LdTrue
+	29: StLoc[3](loc1: bool)
+	30: MoveLoc[6](loc4: u64)
+	31: StLoc[4](loc2: u64)
+	32: Branch(43)
+B4:
+	33: Branch(34)
+B5:
+	34: LdU64(1)
+	35: StLoc[9](loc7: u64)
+	36: MoveLoc[6](loc4: u64)
+	37: MoveLoc[9](loc7: u64)
+	38: Add
+	39: StLoc[6](loc4: u64)
+	40: Branch(42)
+B6:
+	41: Branch(43)
+B7:
+	42: Branch(12)
+B8:
+	43: Nop
+	44: MoveLoc[2](loc0: &vector<T>)
+	45: Pop
+	46: MoveLoc[3](loc1: bool)
+	47: StLoc[10](loc8: bool)
+	48: MoveLoc[4](loc2: u64)
+	49: StLoc[11](loc9: u64)
+	50: MoveLoc[10](loc8: bool)
+	51: BrFalse(59)
+B9:
+	52: MoveLoc[0](Arg0: &mut S)
+	53: MutBorrowField[0](S.entries: vector<T>)
+	54: MoveLoc[11](loc9: u64)
+	55: Call vector::remove<T>(&mut vector<T>, u64): T
+	56: Call option::some<T>(T): Option<T>
+	57: StLoc[12](loc10: Option<T>)
+	58: Branch(63)
+B10:
+	59: MoveLoc[0](Arg0: &mut S)
+	60: Pop
+	61: Call option::none<T>(): Option<T>
+	62: StLoc[12](loc10: Option<T>)
+B11:
+	63: MoveLoc[12](loc10: Option<T>)
+	64: StLoc[13](loc11: Option<T>)
+	65: MoveLoc[13](loc11: Option<T>)
+	66: Ret
+}
+}
+============ bytecode verification succeeded ========

third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.move

@@ -0,0 +1,54 @@
+module 0xc0ffee::m {
+    use std::vector;
+    use std::option;
+    use std::option::Option;
+
+    struct J has copy, drop, store {
+        variant: u64,
+    }
+
+
+    struct T has copy, drop, store {
+        issuer: vector<u8>,
+        version: u64,
+    }
+
+    struct S has copy, drop, store {
+        entries: vector<T>,
+    }
+
+    public inline fun find<Element>(v: &vector<Element>, f: |&Element|bool): (bool, u64) {
+        let find = false;
+        let found_index = 0;
+        let i = 0;
+        let len = vector::length(v);
+        while (i < len) {
+            if (f(vector::borrow(v, i))) {
+                find = true;
+                found_index = i;
+                break
+            };
+            i = i + 1;
+        };
+        spec {
+            assert find ==> f(v[found_index]);
+        };
+        (find, found_index)
+    }
+
+    fun test(s: &mut S, issuer: vector<u8>): Option<T> {
+        let (found, index) = find(&s.entries, |obj| {
+            let set: &T = obj;
+            set.issuer == issuer
+        });
+
+        let ret = if (found) {
+            option::some(vector::remove(&mut s.entries, index))
+        } else {
+            option::none()
+        };
+
+        ret
+    }
+
+}

third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.opt.exp

@@ -0,0 +1,100 @@
+
+============ disassembled file-format ==================
+// Move bytecode v7
+module c0ffee.m {
+use 0000000000000000000000000000000000000000000000000000000000000001::option;
+use 0000000000000000000000000000000000000000000000000000000000000001::vector;
+
+
+struct T has copy, drop, store {
+	issuer: vector<u8>,
+	version: u64
+}
+struct J has copy, drop, store {
+	variant: u64
+}
+struct S has copy, drop, store {
+	entries: vector<T>
+}
+
+test(Arg0: &mut S, Arg1: vector<u8>): Option<T> /* def_idx: 0 */ {
+L2:	loc0: &vector<T>
+L3:	loc1: bool
+L4:	loc2: u64
+L5:	loc3: u64
+L6:	loc4: u64
+L7:	loc5: bool
+L8:	loc6: u64
+L9:	loc7: Option<T>
+L10:	loc8: Option<T>
+B0:
+	0: CopyLoc[0](Arg0: &mut S)
+	1: ImmBorrowField[0](S.entries: vector<T>)
+	2: StLoc[2](loc0: &vector<T>)
+	3: LdFalse
+	4: StLoc[3](loc1: bool)
+	5: LdU64(0)
+	6: StLoc[4](loc2: u64)
+	7: LdU64(0)
+	8: StLoc[5](loc3: u64)
+	9: CopyLoc[2](loc0: &vector<T>)
+	10: VecLen(2)
+	11: StLoc[6](loc4: u64)
+B1:
+	12: CopyLoc[5](loc3: u64)
+	13: CopyLoc[6](loc4: u64)
+	14: Lt
+	15: BrFalse(28)
+B2:
+	16: CopyLoc[2](loc0: &vector<T>)
+	17: CopyLoc[5](loc3: u64)
+	18: VecImmBorrow(2)
+	19: ImmBorrowField[1](T.issuer: vector<u8>)
+	20: ReadRef
+	21: CopyLoc[1](Arg1: vector<u8>)
+	22: Eq
+	23: BrFalse(52)
+B3:
+	24: LdTrue
+	25: StLoc[3](loc1: bool)
+	26: MoveLoc[5](loc3: u64)
+	27: StLoc[4](loc2: u64)
+B4:
+	28: Nop
+	29: MoveLoc[2](loc0: &vector<T>)
+	30: Pop
+	31: MoveLoc[3](loc1: bool)
+	32: StLoc[7](loc5: bool)
+	33: MoveLoc[4](loc2: u64)
+	34: StLoc[8](loc6: u64)
+	35: MoveLoc[7](loc5: bool)
+	36: BrFalse(47)
+B5:
+	37: MoveLoc[0](Arg0: &mut S)
+	38: MutBorrowField[0](S.entries: vector<T>)
+	39: MoveLoc[8](loc6: u64)
+	40: Call vector::remove<T>(&mut vector<T>, u64): T
+	41: Call option::some<T>(T): Option<T>
+	42: StLoc[9](loc7: Option<T>)
+B6:
+	43: MoveLoc[9](loc7: Option<T>)
+	44: StLoc[10](loc8: Option<T>)
+	45: MoveLoc[10](loc8: Option<T>)
+	46: Ret
+B7:
+	47: MoveLoc[0](Arg0: &mut S)
+	48: Pop
+	49: Call option::none<T>(): Option<T>
+	50: StLoc[9](loc7: Option<T>)
+	51: Branch(43)
+B8:
+	52: LdU64(1)
+	53: StLoc[8](loc6: u64)
+	54: MoveLoc[5](loc3: u64)
+	55: MoveLoc[8](loc6: u64)
+	56: Add
+	57: StLoc[5](loc3: u64)
+	58: Branch(12)
+}
+}
+============ bytecode verification succeeded ========

third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.exp

@@ -0,0 +1 @@
+processed 2 tasks

third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.move

@@ -0,0 +1,79 @@
+//# publish
+module 0x42::m {
+    use std::vector;
+    use std::option;
+    use std::option::Option;
+
+    struct J has copy, drop, store {
+        variant: u64,
+    }
+
+    struct T has copy, drop, store {
+        issuer: vector<u8>,
+        version: u64,
+    }
+
+    struct S has copy, drop, store {
+        entries: vector<T>,
+    }
+
+    public inline fun find<Element>(v: &vector<Element>, f: |&Element|bool): (bool, u64) {
+        let find = false;
+        let found_index = 0;
+        let i = 0;
+        let len = vector::length(v);
+        while (i < len) {
+            if (f(vector::borrow(v, i))) {
+                find = true;
+                found_index = i;
+                break
+            };
+            i = i + 1;
+        };
+        spec {
+            assert find ==> f(v[found_index]);
+        };
+        (find, found_index)
+    }
+
+    fun test(s: &mut S, issuer: vector<u8>): Option<T> {
+        let (found, index) = find(&s.entries, |obj| {
+            let set: &T = obj;
+            set.issuer == issuer
+        });
+
+        let ret = if (found) {
+            option::some(vector::remove(&mut s.entries, index))
+        } else {
+            option::none()
+        };
+
+        ret
+    }
+
+    fun test1() {
+        let t0 = T {
+            issuer: vector[1],
+            version: 1
+        };
+        let t1 = T {
+            issuer: vector[2],
+            version: 0
+        };
+        let s = S {
+            entries: vector[t0, t1]
+        };
+        let opt_t = test(&mut s, vector[0]);
+        assert!(option::is_none(&opt_t), 0);
+        let opt_t = test(&mut s, vector[1]);
+        assert!(option::is_some(&opt_t), 0);
+        assert!(option::borrow(&opt_t).issuer == vector[1], 0);
+        let opt_t = test(&mut s, vector[2]);
+        assert!(option::is_some(&opt_t), 0);
+        assert!(option::borrow(&opt_t).issuer == vector[2], 0);
+
+    }
+
+}
+
+//# run 0x42::m::test1