From 4a5545f983f9b97cf0073aa689cfc21317a40c2d Mon Sep 17 00:00:00 2001 From: Teng Zhang Date: Fri, 27 Sep 2024 11:30:48 -0700 Subject: [PATCH] fix code generation bug when inline spec is involved --- .../function_generator.rs | 35 ++++++ .../tests/file-format-generator/bug_14762.exp | 118 ++++++++++++++++++ .../file-format-generator/bug_14762.move | 54 ++++++++ .../file-format-generator/bug_14762.opt.exp | 106 ++++++++++++++++ .../tests/no-v1-comparison/bug_14762.exp | 1 + .../tests/no-v1-comparison/bug_14762.move | 79 ++++++++++++ .../functional/ModifiesErrorTest.v2_exp | 1 + .../tests/sources/functional/enum.v2_exp | 1 + .../sources/functional/enum_generic.v2_exp | 1 + .../sources/functional/inline-lambda.v2_exp | 3 + .../functional/inline_fun_simple.v2_exp | 1 + .../functional/loops_with_memory_ops.v2_exp | 2 +- .../sources/functional/specs_in_fun.v2_exp | 2 + .../sources/functional/strong_edges.v2_exp | 1 + 14 files changed, 404 insertions(+), 1 deletion(-) create mode 100644 third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.exp create mode 100644 third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.move create mode 100644 third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.opt.exp create mode 100644 third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.exp create mode 100644 third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.move diff --git a/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs b/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs index e35c6257716cb0..cf623fe1cb5c3a 100644 --- a/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs +++ b/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs @@ -887,6 +887,16 @@ impl<'a> FunctionGenerator<'a> { /// translation. In the actual Move bytecode, a `Nop` is inserted /// at the current code offset. fn gen_spec_block(&mut self, ctx: &BytecodeContext, spec: &Spec) { + let used_temps = self.collect_temps_from_spec(spec); + for temp in used_temps { + let live_after = ctx.is_alive_after(temp, &[], false); + let local = self.temps.get(&temp).expect("temp has mapping").local; + if !live_after && temp >= ctx.fun_ctx.fun.get_parameter_count() { + self.emit(FF::Bytecode::MoveLoc(local)); + self.emit(FF::Bytecode::Pop); + } + } + let mut replacer = |id: NodeId, target: RewriteTarget| { if let RewriteTarget::Temporary(temp) = target { Some( @@ -906,6 +916,31 @@ impl<'a> FunctionGenerator<'a> { self.emit(FF::Bytecode::Nop) } + fn collect_temps_from_spec(&mut self, spec: &Spec) -> BTreeSet { + let mut temps = BTreeSet::new(); + for cond in spec.conditions.iter() { + for exp in cond.all_exps() { + exp.visit_pre_order(&mut |inner: &ExpData| { + if let ExpData::Temporary(_, temp_index) = inner { + temps.insert(*temp_index); + } + true + }) + } + } + for (_, cond) in spec.update_map.iter() { + for exp in cond.all_exps() { + exp.visit_pre_order(&mut |inner: &ExpData| { + if let ExpData::Temporary(_, temp_index) = inner { + temps.insert(*temp_index); + } + true + }) + } + } + temps + } + /// Emits a file-format bytecode. fn emit(&mut self, bc: FF::Bytecode) { self.code.push(bc) diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.exp b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.exp new file mode 100644 index 00000000000000..41b22145633fed --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.exp @@ -0,0 +1,118 @@ + +============ disassembled file-format ================== +// Move bytecode v7 +module c0ffee.m { +use 0000000000000000000000000000000000000000000000000000000000000001::option; +use 0000000000000000000000000000000000000000000000000000000000000001::vector; + + +struct T has copy, drop, store { + issuer: vector, + version: u64 +} +struct J has copy, drop, store { + variant: u64 +} +struct S has copy, drop, store { + entries: vector +} + +test(Arg0: &mut S, Arg1: vector): Option /* def_idx: 0 */ { +L2: loc0: &vector +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 +L13: loc11: Option +B0: + 0: CopyLoc[0](Arg0: &mut S) + 1: ImmBorrowField[0](S.entries: vector) + 2: StLoc[2](loc0: &vector) + 3: LdFalse + 4: StLoc[3](loc1: bool) + 5: LdU64(0) + 6: StLoc[4](loc2: u64) + 7: LdU64(0) + 8: CopyLoc[2](loc0: &vector) + 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(43) +B2: + 16: CopyLoc[2](loc0: &vector) + 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) + 24: ReadRef + 25: CopyLoc[1](Arg1: vector) + 26: Eq + 27: BrFalse(36) +B3: + 28: CopyLoc[2](loc0: &vector) + 29: Pop + 30: LdTrue + 31: StLoc[3](loc1: bool) + 32: MoveLoc[6](loc4: u64) + 33: StLoc[4](loc2: u64) + 34: Branch(47) +B4: + 35: Branch(36) +B5: + 36: LdU64(1) + 37: StLoc[9](loc7: u64) + 38: MoveLoc[6](loc4: u64) + 39: MoveLoc[9](loc7: u64) + 40: Add + 41: StLoc[6](loc4: u64) + 42: Branch(46) +B6: + 43: CopyLoc[2](loc0: &vector) + 44: Pop + 45: Branch(47) +B7: + 46: Branch(12) +B8: + 47: MoveLoc[2](loc0: &vector) + 48: Pop + 49: Nop + 50: MoveLoc[3](loc1: bool) + 51: StLoc[10](loc8: bool) + 52: MoveLoc[4](loc2: u64) + 53: StLoc[11](loc9: u64) + 54: MoveLoc[10](loc8: bool) + 55: BrFalse(63) +B9: + 56: MoveLoc[0](Arg0: &mut S) + 57: MutBorrowField[0](S.entries: vector) + 58: MoveLoc[11](loc9: u64) + 59: Call vector::remove(&mut vector, u64): T + 60: Call option::some(T): Option + 61: StLoc[12](loc10: Option) + 62: Branch(67) +B10: + 63: MoveLoc[0](Arg0: &mut S) + 64: Pop + 65: Call option::none(): Option + 66: StLoc[12](loc10: Option) +B11: + 67: MoveLoc[12](loc10: Option) + 68: StLoc[13](loc11: Option) + 69: MoveLoc[13](loc11: Option) + 70: Ret +} +} +============ bytecode verification succeeded ======== diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.move b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.move new file mode 100644 index 00000000000000..687c39ecd04bee --- /dev/null +++ b/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, + version: u64, + } + + struct S has copy, drop, store { + entries: vector, + } + + public inline fun find(v: &vector, 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): Option { + 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 + } + +} diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.opt.exp b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.opt.exp new file mode 100644 index 00000000000000..7ba9a71944621c --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.opt.exp @@ -0,0 +1,106 @@ + +============ disassembled file-format ================== +// Move bytecode v7 +module c0ffee.m { +use 0000000000000000000000000000000000000000000000000000000000000001::option; +use 0000000000000000000000000000000000000000000000000000000000000001::vector; + + +struct T has copy, drop, store { + issuer: vector, + version: u64 +} +struct J has copy, drop, store { + variant: u64 +} +struct S has copy, drop, store { + entries: vector +} + +test(Arg0: &mut S, Arg1: vector): Option /* def_idx: 0 */ { +L2: loc0: &vector +L3: loc1: bool +L4: loc2: u64 +L5: loc3: u64 +L6: loc4: u64 +L7: loc5: bool +L8: loc6: u64 +L9: loc7: Option +L10: loc8: Option +B0: + 0: CopyLoc[0](Arg0: &mut S) + 1: ImmBorrowField[0](S.entries: vector) + 2: StLoc[2](loc0: &vector) + 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) + 10: VecLen(2) + 11: StLoc[6](loc4: u64) +B1: + 12: CopyLoc[5](loc3: u64) + 13: CopyLoc[6](loc4: u64) + 14: Lt + 15: BrFalse(61) +B2: + 16: CopyLoc[2](loc0: &vector) + 17: CopyLoc[5](loc3: u64) + 18: VecImmBorrow(2) + 19: ImmBorrowField[1](T.issuer: vector) + 20: ReadRef + 21: CopyLoc[1](Arg1: vector) + 22: Eq + 23: BrFalse(54) +B3: + 24: CopyLoc[2](loc0: &vector) + 25: Pop + 26: LdTrue + 27: StLoc[3](loc1: bool) + 28: MoveLoc[5](loc3: u64) + 29: StLoc[4](loc2: u64) +B4: + 30: MoveLoc[2](loc0: &vector) + 31: Pop + 32: Nop + 33: MoveLoc[3](loc1: bool) + 34: StLoc[7](loc5: bool) + 35: MoveLoc[4](loc2: u64) + 36: StLoc[8](loc6: u64) + 37: MoveLoc[7](loc5: bool) + 38: BrFalse(49) +B5: + 39: MoveLoc[0](Arg0: &mut S) + 40: MutBorrowField[0](S.entries: vector) + 41: MoveLoc[8](loc6: u64) + 42: Call vector::remove(&mut vector, u64): T + 43: Call option::some(T): Option + 44: StLoc[9](loc7: Option) +B6: + 45: MoveLoc[9](loc7: Option) + 46: StLoc[10](loc8: Option) + 47: MoveLoc[10](loc8: Option) + 48: Ret +B7: + 49: MoveLoc[0](Arg0: &mut S) + 50: Pop + 51: Call option::none(): Option + 52: StLoc[9](loc7: Option) + 53: Branch(45) +B8: + 54: LdU64(1) + 55: StLoc[8](loc6: u64) + 56: MoveLoc[5](loc3: u64) + 57: MoveLoc[8](loc6: u64) + 58: Add + 59: StLoc[5](loc3: u64) + 60: Branch(12) +B9: + 61: CopyLoc[2](loc0: &vector) + 62: Pop + 63: Branch(30) +} +} +============ bytecode verification succeeded ======== diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.exp b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.exp new file mode 100644 index 00000000000000..5d92c423f3fd86 --- /dev/null +++ b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.exp @@ -0,0 +1 @@ +processed 2 tasks diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.move b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.move new file mode 100644 index 00000000000000..eede6c62f227ff --- /dev/null +++ b/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, + version: u64, + } + + struct S has copy, drop, store { + entries: vector, + } + + public inline fun find(v: &vector, 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): Option { + 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 diff --git a/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp b/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp index a4c827857f7881..3552a08011baa3 100644 --- a/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp @@ -136,4 +136,5 @@ error: unknown assertion failed = at tests/sources/functional/ModifiesErrorTest.move:92: mutate_S_test2_incorrect = at tests/sources/functional/ModifiesErrorTest.move:93: mutate_S_test2_incorrect = x1 = + = at tests/sources/functional/ModifiesErrorTest.move:94: mutate_S_test2_incorrect = at tests/sources/functional/ModifiesErrorTest.move:95: mutate_S_test2_incorrect diff --git a/third_party/move/move-prover/tests/sources/functional/enum.v2_exp b/third_party/move/move-prover/tests/sources/functional/enum.v2_exp index 737366c5714f8d..5701c7c0b42598 100644 --- a/third_party/move/move-prover/tests/sources/functional/enum.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/enum.v2_exp @@ -59,4 +59,5 @@ error: unknown assertion failed = at tests/sources/functional/enum.move:65: test_enum_vector = at tests/sources/functional/enum.move:63: test_enum_vector = _common_vector_2 = + = at tests/sources/functional/enum.move:67: test_enum_vector = at tests/sources/functional/enum.move:68: test_enum_vector diff --git a/third_party/move/move-prover/tests/sources/functional/enum_generic.v2_exp b/third_party/move/move-prover/tests/sources/functional/enum_generic.v2_exp index fc4359fda9f06d..9083d6ddc4e738 100644 --- a/third_party/move/move-prover/tests/sources/functional/enum_generic.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/enum_generic.v2_exp @@ -17,4 +17,5 @@ error: unknown assertion failed = at tests/sources/functional/enum_generic.move:24: test_enum_vector = at tests/sources/functional/enum_generic.move:22: test_enum_vector = _common_vector_2 = + = at tests/sources/functional/enum_generic.move:26: test_enum_vector = at tests/sources/functional/enum_generic.move:27: test_enum_vector diff --git a/third_party/move/move-prover/tests/sources/functional/inline-lambda.v2_exp b/third_party/move/move-prover/tests/sources/functional/inline-lambda.v2_exp index a939ef7f0c9c6f..9c3d3fe786c65e 100644 --- a/third_party/move/move-prover/tests/sources/functional/inline-lambda.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/inline-lambda.v2_exp @@ -24,6 +24,7 @@ error: unknown assertion failed = at tests/sources/functional/inline-lambda.move:5: apply = at tests/sources/functional/inline-lambda.move:11: test_apply = r1 = + = at tests/sources/functional/inline-lambda.move:12: test_apply = at tests/sources/functional/inline-lambda.move:13: test_apply = at tests/sources/functional/inline-lambda.move:4: apply = at tests/sources/functional/inline-lambda.move:5: apply @@ -41,9 +42,11 @@ error: unknown assertion failed = at tests/sources/functional/inline-lambda.move:5: apply = at tests/sources/functional/inline-lambda.move:11: test_apply = r1 = + = at tests/sources/functional/inline-lambda.move:12: test_apply = at tests/sources/functional/inline-lambda.move:13: test_apply = at tests/sources/functional/inline-lambda.move:4: apply = at tests/sources/functional/inline-lambda.move:5: apply = at tests/sources/functional/inline-lambda.move:16: test_apply = r2 = + = at tests/sources/functional/inline-lambda.move:17: test_apply = at tests/sources/functional/inline-lambda.move:18: test_apply diff --git a/third_party/move/move-prover/tests/sources/functional/inline_fun_simple.v2_exp b/third_party/move/move-prover/tests/sources/functional/inline_fun_simple.v2_exp index a71d8eee327fb7..ab4196297ad940 100644 --- a/third_party/move/move-prover/tests/sources/functional/inline_fun_simple.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/inline_fun_simple.v2_exp @@ -32,5 +32,6 @@ error: unknown assertion failed = at tests/sources/functional/inline_fun_simple.move:4: apply = at tests/sources/functional/inline_fun_simple.move:22: test_apply_error = r1 = + = at tests/sources/functional/inline_fun_simple.move:23: test_apply_error = at tests/sources/functional/inline_fun_simple.move:24: test_apply_error = at tests/sources/functional/inline_fun_simple.move:4: apply diff --git a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp index 00ce62137346b0..f7a1704b6cf54a 100644 --- a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp @@ -42,7 +42,6 @@ error: induction case of the loop invariant does not hold = at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2 = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 = a = - = b = = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 = at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2 = = @@ -108,4 +107,5 @@ error: unknown assertion failed = i = = at tests/sources/functional/loops_with_memory_ops.move:86: nested_loop2 = at tests/sources/functional/loops_with_memory_ops.move:87: nested_loop2 + = at tests/sources/functional/loops_with_memory_ops.move:92: nested_loop2 = at tests/sources/functional/loops_with_memory_ops.move:93: nested_loop2 diff --git a/third_party/move/move-prover/tests/sources/functional/specs_in_fun.v2_exp b/third_party/move/move-prover/tests/sources/functional/specs_in_fun.v2_exp index a41ce4e6598425..18312f5f4403dd 100644 --- a/third_party/move/move-prover/tests/sources/functional/specs_in_fun.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/specs_in_fun.v2_exp @@ -46,6 +46,7 @@ error: unknown assertion failed = at tests/sources/functional/specs_in_fun.move:51: simple2_incorrect = = = y = + = at tests/sources/functional/specs_in_fun.move:52: simple2_incorrect = at tests/sources/functional/specs_in_fun.move:53: simple2_incorrect error: unknown assertion failed @@ -71,5 +72,6 @@ error: unknown assertion failed = y = = at tests/sources/functional/specs_in_fun.move:66: simple4_incorrect = z = + = at tests/sources/functional/specs_in_fun.move:67: simple4_incorrect = at tests/sources/functional/specs_in_fun.move:68: simple4_incorrect = at tests/sources/functional/specs_in_fun.move:69: simple4_incorrect diff --git a/third_party/move/move-prover/tests/sources/functional/strong_edges.v2_exp b/third_party/move/move-prover/tests/sources/functional/strong_edges.v2_exp index 67b7e4f38736eb..80f2bdc5019e84 100644 --- a/third_party/move/move-prover/tests/sources/functional/strong_edges.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/strong_edges.v2_exp @@ -28,4 +28,5 @@ error: unknown assertion failed = r_ref = = at tests/sources/functional/strong_edges.move:62: loc__edge_incorrect = r = + = at tests/sources/functional/strong_edges.move:63: loc__edge_incorrect = at tests/sources/functional/strong_edges.move:64: loc__edge_incorrect