Skip to content

Commit

Permalink
fix code generation bug when inline spec is involved
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahxephon89
rahxephon89 committed Oct 8, 2024
1 parent 2deaf9f commit 4a5545f
Show file tree
Hide file tree
Showing 14 changed files with 404 additions and 1 deletion.
35 changes: 35 additions & 0 deletions third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand All @@ -906,6 +916,31 @@ impl<'a> FunctionGenerator<'a> {
self.emit(FF::Bytecode::Nop)
}

fn collect_temps_from_spec(&mut self, spec: &Spec) -> BTreeSet<TempIndex> {
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
})

Check warning on line 938 in third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs

View check run for this annotation

Codecov / codecov/patch

third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs#L932-L938 

Added lines #L932 - L938 were not covered by tests
}
}
temps
}

/// Emits a file-format bytecode.
fn emit(&mut self, bc: FF::Bytecode) {
self.code.push(bc)
Expand Down
118 changes: 118 additions & 0 deletions third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.exp
View file
Original file line number Diff line number Diff line change
@@ -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<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(43)
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(36)
B3:
28: CopyLoc[2](loc0: &vector<T>)
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<T>)
44: Pop
45: Branch(47)
B7:
46: Branch(12)
B8:
47: MoveLoc[2](loc0: &vector<T>)
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<T>)
58: MoveLoc[11](loc9: u64)
59: Call vector::remove<T>(&mut vector<T>, u64): T
60: Call option::some<T>(T): Option<T>
61: StLoc[12](loc10: Option<T>)
62: Branch(67)
B10:
63: MoveLoc[0](Arg0: &mut S)
64: Pop
65: Call option::none<T>(): Option<T>
66: StLoc[12](loc10: Option<T>)
B11:
67: MoveLoc[12](loc10: Option<T>)
68: StLoc[13](loc11: Option<T>)
69: MoveLoc[13](loc11: Option<T>)
70: Ret
}
}
============ bytecode verification succeeded ========
54 changes: 54 additions & 0 deletions third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.move
View file
Original file line number Diff line number Diff line change
@@ -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
}

}
106 changes: 106 additions & 0 deletions third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.opt.exp
View file
Original file line number Diff line number Diff line change
@@ -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<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(61)
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(54)
B3:
24: CopyLoc[2](loc0: &vector<T>)
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<T>)
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<T>)
41: MoveLoc[8](loc6: u64)
42: Call vector::remove<T>(&mut vector<T>, u64): T
43: Call option::some<T>(T): Option<T>
44: StLoc[9](loc7: Option<T>)
B6:
45: MoveLoc[9](loc7: Option<T>)
46: StLoc[10](loc8: Option<T>)
47: MoveLoc[10](loc8: Option<T>)
48: Ret
B7:
49: MoveLoc[0](Arg0: &mut S)
50: Pop
51: Call option::none<T>(): Option<T>
52: StLoc[9](loc7: Option<T>)
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<T>)
62: Pop
63: Branch(30)
}
}
============ bytecode verification succeeded ========
1 change: 1 addition & 0 deletions third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.exp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
processed 2 tasks
Loading

0 comments on commit 4a5545f

Please sign in to comment.