Skip to content

Commit

Permalink
fix bug in loop unrolling
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahxephon89
rahxephon89 committed Oct 31, 2024
1 parent 3b23a90 commit 977b3d3
Show file tree
Hide file tree
Showing 16 changed files with 124 additions and 42 deletions.
1 change: 0 additions & 1 deletion third_party/move/move-compiler-v2/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -162,7 +162,6 @@ pub fn run_move_compiler_for_analysis(
options.whole_program = true; // will set `treat_everything_as_target`
options = options.set_experiment(Experiment::SPEC_REWRITE, true);
options = options.set_experiment(Experiment::ATTACH_COMPILED_MODULE, true);
options = options.set_experiment(Experiment::CFG_SIMPLIFICATION, false);
let (env, _units) = run_move_compiler(error_writer, options)?;
// Reset for subsequent analysis
env.treat_everything_as_target(false);
Expand Down
43 changes: 40 additions & 3 deletions third_party/move/move-model/bytecode/src/fat_loop.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -450,20 +450,57 @@ impl FatLoopBuilder {
cfg: &StacklessControlFlowGraph,
sub_loops: &[NaturalLoop<BlockId>],
) -> Vec<Vec<Bytecode>> {
sub_loops
let mut id_label_map = BTreeMap::new();
let blocks: Vec<(BlockId, Vec<Bytecode>)> = sub_loops
.iter()
.flat_map(|l| l.loop_body.iter())
.map(|block_id| match cfg.content(*block_id) {
BlockContent::Dummy => {
panic!("A loop body should never contain a dummy block")
},
BlockContent::Basic { lower, upper } => {
if let Some(lbl) = code[*lower as usize].get_label_inner_opt() {
id_label_map.insert(*block_id, lbl);
}
let block: Vec<_> = (*lower..=*upper)
.map(|i| code.get(i as usize).unwrap().clone())
.collect();
block
(*block_id, block)
},
})
.collect()
.collect();
let mut results = vec![];
for (i, (block_id, block)) in blocks.iter().enumerate() {
// if this block has one successor and the last bc of this block is not a branch
// we need to check whether the next block is the successor,
// if not, insert a jump to the correct block
if cfg.successors(*block_id).len() == 1 && !block[block.len() - 1].is_branching() {
let successor_id = cfg.successors(*block_id).first().unwrap();
let successor_label_opt = id_label_map.get(successor_id);
if successor_label_opt.is_some()
&& i != blocks.len() - 1
&& !blocks.get(i + 1).unwrap().1.is_empty()
{
if let Some(lbl) = blocks.get(i + 1).unwrap().1[0].get_label_inner_opt() {
let successor_label = *successor_label_opt.unwrap();
if lbl != successor_label {
let mut new_block = block.clone();
// Inserted bc is used for jumping to its successor so
// we just use the attr_id of its previous bc
new_block.push(Bytecode::Jump(
block[block.len() - 1].get_attr_id(),
Label::new(successor_label as usize),
));
results.push(new_block);
continue;
}
}
}
results.push(block.clone());
} else {
results.push(block.clone());
}
}
results
}
}
7 changes: 7 additions & 0 deletions third_party/move/move-model/bytecode/src/stackless_bytecode.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -541,6 +541,13 @@ impl Bytecode {
self.is_possibly_branching() || self.is_always_branching()
}

pub fn get_label_inner_opt(&self) -> Option<u16> {
match self {
Bytecode::Label(_, l) => Some(l.0),
_ => None,
}
}

/// Returns true if the bytecode is spec-only.
pub fn is_spec_only(&self) -> bool {
use Bytecode::*;
Expand Down
11 changes: 8 additions & 3 deletions third_party/move/move-prover/tests/sources/functional/aborts_if.v2_exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ error: abort not covered by any of the `aborts_if` clauses
┌─ tests/sources/functional/aborts_if.move:139:5
│
137 │ if (x == 2 || x == 3) abort 1;
│ ------ abort happened here with code 0x1
│ ----------------------------- abort happened here with code 0x1
138 │ }
139 │ ╭ spec abort_at_2_or_3_total_incorrect {
140 │ │ // Counter check that we get an error message without the pragma.
Expand All @@ -114,6 +114,8 @@ error: abort not covered by any of the `aborts_if` clauses
= at tests/sources/functional/aborts_if.move:136: abort_at_2_or_3_total_incorrect
= x = <redacted>
= at tests/sources/functional/aborts_if.move:137: abort_at_2_or_3_total_incorrect
= at tests/sources/functional/aborts_if.move:136: abort_at_2_or_3_total_incorrect
= at tests/sources/functional/aborts_if.move:137: abort_at_2_or_3_total_incorrect
= <redacted> = <redacted>
= at tests/sources/functional/aborts_if.move:137: abort_at_2_or_3_total_incorrect
= ABORTED
Expand All @@ -127,16 +129,17 @@ error: function does not abort under this condition
= at tests/sources/functional/aborts_if.move:145: abort_at_2_or_3_spec_incorrect
= x = <redacted>
= at tests/sources/functional/aborts_if.move:146: abort_at_2_or_3_spec_incorrect
= at tests/sources/functional/aborts_if.move:145: abort_at_2_or_3_spec_incorrect
= at tests/sources/functional/aborts_if.move:146: abort_at_2_or_3_spec_incorrect
= <redacted> = <redacted>
= at tests/sources/functional/aborts_if.move:146: abort_at_2_or_3_spec_incorrect
= at tests/sources/functional/aborts_if.move:147: abort_at_2_or_3_spec_incorrect
= at tests/sources/functional/aborts_if.move:151: abort_at_2_or_3_spec_incorrect (spec)

error: abort not covered by any of the `aborts_if` clauses
┌─ tests/sources/functional/aborts_if.move:157:5
│
155 │ if (x == 2 || x == 3) abort 1;
│ ------ abort happened here with code 0x1
│ ----------------------------- abort happened here with code 0x1
156 │ }
157 │ ╭ spec abort_at_2_or_3_strict_incorrect {
158 │ │ // When the strict mode is enabled, no aborts_if clause means aborts_if false.
Expand All @@ -147,6 +150,8 @@ error: abort not covered by any of the `aborts_if` clauses
= at tests/sources/functional/aborts_if.move:154: abort_at_2_or_3_strict_incorrect
= x = <redacted>
= at tests/sources/functional/aborts_if.move:155: abort_at_2_or_3_strict_incorrect
= at tests/sources/functional/aborts_if.move:154: abort_at_2_or_3_strict_incorrect
= at tests/sources/functional/aborts_if.move:155: abort_at_2_or_3_strict_incorrect
= <redacted> = <redacted>
= at tests/sources/functional/aborts_if.move:155: abort_at_2_or_3_strict_incorrect
= ABORTED
52 changes: 52 additions & 0 deletions third_party/move/move-prover/tests/sources/functional/bug_15044.move
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
module 0x42::comparator {
use std::vector;

const EQUAL: u8 = 0;
const SMALLER: u8 = 1;
const GREATER: u8 = 2;

struct Result has drop {
inner: u8,
}

spec compare_u8_vector(left: vector<u8>, right: vector<u8>): Result {
pragma unroll = 5;

let left_length = len(left);
let right_length = len(right);

ensures (result.inner == EQUAL) ==> (
(left_length == right_length) &&
(forall i: u64 where i < left_length: left[i] == right[i])
);
}

// Performs a comparison of two vector<u8>s or byte vectors
public fun compare_u8_vector(left: vector<u8>, right: vector<u8>): Result {
let left_length = vector::length(&left);
let right_length = vector::length(&right);

let idx = 0;

while (idx < left_length && idx < right_length) {
let left_byte = *vector::borrow(&left, idx);
let right_byte = *vector::borrow(&right, idx);

if (left_byte < right_byte) {
return Result { inner: SMALLER }
} else if (left_byte > right_byte) {
return Result { inner: GREATER }
};
idx = idx + 1;
};

if (left_length < right_length) {
Result { inner: SMALLER }
} else if (left_length > right_length) {
Result { inner: GREATER }
} else {
Result { inner: EQUAL }
}
}

}
20 changes: 11 additions & 9 deletions third_party/move/move-prover/tests/sources/functional/bv_aborts.v2_exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,22 +8,24 @@ error: function does not abort under this condition
= at tests/sources/functional/bv_aborts.move:11: assert_with_spec
= x = <redacted>
= at tests/sources/functional/bv_aborts.move:12: assert_with_spec
= at tests/sources/functional/bv_aborts.move:13: assert_with_spec
= at tests/sources/functional/bv_aborts.move:16: assert_with_spec (spec)

error: abort not covered by any of the `aborts_if` clauses
┌─ tests/sources/functional/bv_aborts.move:14:5
│
12 │ assert!(x > 815);
│ ------ abort happened here
13 │ }
14 │ ╭ spec assert_with_spec {
15 │ │ // This will fail
16 │ │ aborts_if x > 815 with std::error::internal(0) | (0xCA26CBD9BE << 24);
17 │ │ }
│ ╰─────^
11 │ fun assert_with_spec(x: u64) {
│ ╭──────────────────────────────────'
12 │ │ assert!(x > 815);
13 │ │ }
│ ╰─────' abort happened here
14 │ ╭ spec assert_with_spec {
15 │ │ // This will fail
16 │ │ aborts_if x > 815 with std::error::internal(0) | (0xCA26CBD9BE << 24);
17 │ │ }
│ ╰───────^
│
= at tests/sources/functional/bv_aborts.move:11: assert_with_spec
= x = <redacted>
= at tests/sources/functional/bv_aborts.move:12: assert_with_spec
= at tests/sources/functional/bv_aborts.move:11: assert_with_spec
= ABORTED
1 change: 0 additions & 1 deletion third_party/move/move-prover/tests/sources/functional/choice.v2_exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@ error: post-condition does not hold
= return = <redacted>
= at tests/sources/functional/choice.move:17: simple_incorrect
= result = <redacted>
= at tests/sources/functional/choice.move:18: simple_incorrect
= at tests/sources/functional/choice.move:22: simple_incorrect (spec)
= `TRACE(choose x: u64 where x >= 4 && x <= 5)` = <redacted>

Expand Down
6 changes: 2 additions & 4 deletions third_party/move/move-prover/tests/sources/functional/emits.v2_exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,8 +76,8 @@ error: function does not emit the expected event
= x = <redacted>
= handle = <redacted>
= at tests/sources/functional/emits.move:106: conditional_wrong_condition_incorrect
= at tests/sources/functional/emits.move:107: conditional_wrong_condition_incorrect
= handle = <redacted>
= at tests/sources/functional/emits.move:109: conditional_wrong_condition_incorrect
= at tests/sources/functional/emits.move:111: conditional_wrong_condition_incorrect (spec)

error: function does not emit the expected event
Expand All @@ -90,8 +90,8 @@ error: function does not emit the expected event
= x = <redacted>
= handle = <redacted>
= at tests/sources/functional/emits.move:115: conditional_missing_condition_incorrect
= at tests/sources/functional/emits.move:116: conditional_missing_condition_incorrect
= handle = <redacted>
= at tests/sources/functional/emits.move:118: conditional_missing_condition_incorrect
= at tests/sources/functional/emits.move:120: conditional_missing_condition_incorrect (spec)

error: function does not emit the expected event
Expand All @@ -110,7 +110,6 @@ error: function does not emit the expected event
= at tests/sources/functional/emits.move:152: conditional_multiple_incorrect
= at tests/sources/functional/emits.move:149: conditional_multiple_incorrect
= handle = <redacted>
= at tests/sources/functional/emits.move:155: conditional_multiple_incorrect
= at tests/sources/functional/emits.move:157: conditional_multiple_incorrect (spec)
= at tests/sources/functional/emits.move:158: conditional_multiple_incorrect (spec)
= at tests/sources/functional/emits.move:159: conditional_multiple_incorrect (spec)
Expand All @@ -131,7 +130,6 @@ error: function does not emit the expected event
= at tests/sources/functional/emits.move:182: conditional_multiple_same_incorrect
= at tests/sources/functional/emits.move:179: conditional_multiple_same_incorrect
= handle = <redacted>
= at tests/sources/functional/emits.move:185: conditional_multiple_same_incorrect
= at tests/sources/functional/emits.move:187: conditional_multiple_same_incorrect (spec)
= at tests/sources/functional/emits.move:188: conditional_multiple_same_incorrect (spec)
= at tests/sources/functional/emits.move:189: conditional_multiple_same_incorrect (spec)
Expand Down
1 change: 1 addition & 0 deletions third_party/move/move-prover/tests/sources/functional/enum_abort.v2_exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,7 @@ error: abort not covered by any of the `aborts_if` clauses
= <redacted> = <redacted>
= at tests/sources/functional/enum_abort.move:122: test_match_abort
= _z = <redacted>
= at tests/sources/functional/enum_abort.move:123: test_match_abort
= at tests/sources/functional/enum_abort.move:122: test_match_abort
= <redacted> = <redacted>
= at tests/sources/functional/enum_abort.move:122: test_match_abort
Expand Down
2 changes: 0 additions & 2 deletions third_party/move/move-prover/tests/sources/functional/global_invariants.v2_exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,6 @@ error: global memory invariant does not hold
= at ../move-stdlib/sources/signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/signer.move:14: address_of
= at tests/sources/functional/global_invariants.move:55: remove_S_invalid
= at tests/sources/functional/global_invariants.move:56: remove_S_invalid
= at ../move-stdlib/sources/signer.move:12: address_of
= s = <redacted>
Expand All @@ -50,7 +49,6 @@ error: global memory invariant does not hold
= at ../move-stdlib/sources/signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/signer.move:14: address_of
= at tests/sources/functional/global_invariants.move:64: remove_R_invalid
= at tests/sources/functional/global_invariants.move:65: remove_R_invalid
= at ../move-stdlib/sources/signer.move:12: address_of
= s = <redacted>
Expand Down
1 change: 0 additions & 1 deletion third_party/move/move-prover/tests/sources/functional/is_txn_signer.v2_exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@ error: unknown assertion failed
= at ../move-stdlib/sources/signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/signer.move:14: address_of
= at tests/sources/functional/is_txn_signer.move:30: f4_incorrect
= at tests/sources/functional/is_txn_signer.move:31: f4_incorrect

error: precondition does not hold at this call
Expand Down
8 changes: 0 additions & 8 deletions third_party/move/move-prover/tests/sources/functional/loop_unroll.v2_exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,6 @@ error: abort not covered by any of the `aborts_if` clauses
= at tests/sources/functional/loop_unroll.move:97: t6_failure
= <redacted> = <redacted>
= at tests/sources/functional/loop_unroll.move:97: t6_failure
= at tests/sources/functional/loop_unroll.move:95: t6_failure
= at tests/sources/functional/loop_unroll.move:90: t6_failure
= at tests/sources/functional/loop_unroll.move:92: t6_failure
= at tests/sources/functional/loop_unroll.move:94: t6_failure
= at tests/sources/functional/loop_unroll.move:90: t6_failure
Expand All @@ -34,8 +32,6 @@ error: abort not covered by any of the `aborts_if` clauses
= i = <redacted>
= at tests/sources/functional/loop_unroll.move:97: t6_failure
= <redacted> = <redacted>
= at tests/sources/functional/loop_unroll.move:95: t6_failure
= at tests/sources/functional/loop_unroll.move:90: t6_failure
= at tests/sources/functional/loop_unroll.move:91: t6_failure
= at tests/sources/functional/loop_unroll.move:92: t6_failure
= at tests/sources/functional/loop_unroll.move:94: t6_failure
Expand All @@ -45,8 +41,6 @@ error: abort not covered by any of the `aborts_if` clauses
= i = <redacted>
= at tests/sources/functional/loop_unroll.move:97: t6_failure
= <redacted> = <redacted>
= at tests/sources/functional/loop_unroll.move:95: t6_failure
= at tests/sources/functional/loop_unroll.move:90: t6_failure
= at tests/sources/functional/loop_unroll.move:91: t6_failure
= at tests/sources/functional/loop_unroll.move:92: t6_failure
= at tests/sources/functional/loop_unroll.move:94: t6_failure
Expand All @@ -56,8 +50,6 @@ error: abort not covered by any of the `aborts_if` clauses
= i = <redacted>
= at tests/sources/functional/loop_unroll.move:97: t6_failure
= <redacted> = <redacted>
= at tests/sources/functional/loop_unroll.move:95: t6_failure
= at tests/sources/functional/loop_unroll.move:90: t6_failure
= at tests/sources/functional/loop_unroll.move:91: t6_failure
= at tests/sources/functional/loop_unroll.move:92: t6_failure
= at tests/sources/functional/loop_unroll.move:94: t6_failure
Expand Down
3 changes: 0 additions & 3 deletions third_party/move/move-prover/tests/sources/functional/loops.v2_exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,6 @@ error: induction case of the loop invariant does not hold
= at tests/sources/functional/loops.move:122: nested_loop_outer_invariant_incorrect
= enter loop, variable(s) y havocked and reassigned
= y = <redacted>
= at tests/sources/functional/loops.move:123: nested_loop_outer_invariant_incorrect
= at tests/sources/functional/loops.move:128: nested_loop_outer_invariant_incorrect
= at tests/sources/functional/loops.move:131: nested_loop_outer_invariant_incorrect
= <redacted> = <redacted>
Expand Down Expand Up @@ -89,7 +88,6 @@ error: induction case of the loop invariant does not hold
= at tests/sources/functional/loops.move:150: nested_loop_inner_invariant_incorrect
= <redacted> = <redacted>
= y = <redacted>
= at tests/sources/functional/loops.move:143: nested_loop_inner_invariant_incorrect
= at tests/sources/functional/loops.move:145: nested_loop_inner_invariant_incorrect

error: induction case of the loop invariant does not hold
Expand Down Expand Up @@ -149,7 +147,6 @@ error: induction case of the loop invariant does not hold
= at tests/sources/functional/loops.move:227: loop_invariant_induction_invalid
= <redacted> = <redacted>
= x = <redacted>
= at tests/sources/functional/loops.move:226: loop_invariant_induction_invalid
= at tests/sources/functional/loops.move:221: loop_invariant_induction_invalid
= at tests/sources/functional/loops.move:223: loop_invariant_induction_invalid

Expand Down
7 changes: 3 additions & 4 deletions third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,10 +38,10 @@ error: induction case of the loop invariant does not hold
= enter loop, variable(s) x, y havocked and reassigned
= x = <redacted>
= y = <redacted>
= at tests/sources/functional/loops_with_memory_ops.move:75: nested_loop2
= 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 = <redacted>
= at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
= b = <redacted>
= at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
= <redacted> = <redacted>
Expand Down Expand Up @@ -96,14 +96,13 @@ error: unknown assertion failed
= enter loop, variable(s) x, y havocked and reassigned
= x = <redacted>
= y = <redacted>
= at tests/sources/functional/loops_with_memory_ops.move:75: nested_loop2
= at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
= at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
= b = <redacted>
= a = <redacted>
= at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
= b = <redacted>
= at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
= <redacted> = <redacted>
= i = <redacted>
= 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:93: nested_loop2
Loading

0 comments on commit 977b3d3

Please sign in to comment.