Skip to content

Commit

Permalink
[compiler] More tests for "for" loops (#11584)
Browse files Browse the repository at this point in the history
* add some tests for for loops
* fix missing output case
* get rid of tabs, commented tests, remove infinite_lop_with_dead_exits from -v2/tests since output is incorrect
* add tests illustrating issue #11427
  • Loading branch information
brmataptos authored Jan 18, 2024
1 parent b630041 commit 8f0c41a
Show file tree
Hide file tree
Showing 65 changed files with 703 additions and 34 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@

Diagnostics:
error: undeclared `<SELF>_0::_`
┌─ tests/checking/control_flow/for_loop_empty_novar.move:4:9
4 │ for (_ in 0..10) {};
│ ^^^^^^^^^^^^^^^^^^^
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//# run
script {
fun main(): () {
for (_ in 0..10) {};
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@

Diagnostics:
error: invalid call of `+`: expected `integer` but found `bool` for argument 1
┌─ tests/checking/control_flow/for_type_mismatch.move:5:9
5 │ ╭ for (i in true..false) {
6 │ │ x = x + 1;
7 │ │ };
│ ╰─────────^

error: invalid call of `<`: expected `integer` but found `bool` for argument 1
┌─ tests/checking/control_flow/for_type_mismatch.move:5:9
5 │ ╭ for (i in true..false) {
6 │ │ x = x + 1;
7 │ │ };
│ ╰─────────^
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// ---- Model Dump
module <SELF>_0 {
private fun main() {
loop {
break
};
loop {
Tuple()
}
}
spec fun $main();
} // end <SELF>_0
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
script {
fun main() {
loop { break };
loop ()
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
processed 1 task

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
//# run
script {
fun main() {
let x = 0;
for (i in 0..10) { // 0, 1, 2, 3, 4, 5, 6, 7, 8, 9
x = x + 1; // 1, 4, 13, 16,
if (x >= 15) break;
x = x + 2; // 3, 6, 15, -
if (i % 2 == 0) continue;
x = x * 2; // -, 12, -, -
};
assert!(x == 16, x);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
processed 1 task

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
//# run
script {
fun main() {
let k = 0;
let y = 0;
for (j in 0..10) { //j: 0, 1, 2, 3, 4, 5, 6, 7, 8, 9
y = y + 1; //y: 1, 4, 13, 16,
if (y >= 15) break;
y = y + 2; //y: 3, 6, 15, -
let x = 0;
for (i in 0..10) { //i: 0, 1, 2, 3, 4, 5, 6, 7, 8, 9
x = x + 1; //x: 1, 4, 13, 16,
if (x >= 15) break;
x = x + 2; //x: 3, 6, 15, -
if (i % 2 == 0) continue;
x = x * 2; //x: -, 12, -, -
};
assert!(x == 16, x);
k = k + x; //k: 16, 32, 48, -
if (j % 2 == 0) continue;
y = y * 2; //y: -, 12, -, -
};
// k: 48, y: 16
let z = 3 * k + y;
// z: 208
assert!(z == 160, z);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
processed 1 task

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
//# run
script {
fun main() {
let x = 0;
for (i in 10..4) {
x = x + 1;
};
assert!(x == 0, 42);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
processed 1 task

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
//# run
script {
fun main(): () {
let y = 0;
for (i in 0..1 spec {invariant y > 0;}) {
y = y + 1;
};
assert!(y == 1, 20);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
processed 1 task

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//# run
script {
fun main(): () {
for (i in 0..10) {};
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
processed 1 task

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
//# run
script {
fun main(): () {
for (i in 10..9) {
assert!(false, 42);
};
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
processed 1 task

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
//# run
script {
fun main(): () {
let y = 0;
for (i in 0..10) {
y = y + 1;
i = i + 1;
};
assert!(y == 5, 42);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
processed 1 task

task 0 'run'. lines 1-14:
Error: Script execution failed with VMError: {
major_status: OUT_OF_GAS,
sub_status: None,
location: script,
indices: redacted,
offsets: redacted,
}

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
//# run --gas-budget 700
script {
fun main() {
// nonterminating loop
for (i in 0..10) {
i = 0;
for (j in 0..10) {
break;
};
};
if (true) () else ();
assert!(false, 42);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
processed 1 task

task 0 'run'. lines 1-11:
Error: Script execution failed with VMError: {
major_status: OUT_OF_GAS,
sub_status: None,
location: script,
indices: redacted,
offsets: redacted,
}

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
//# run --gas-budget 700
script {
fun main(): () {
let y = 0;
// out of gas
for (i in 0..10) {
i = 0;
};
assert!(false, 42);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
processed 2 tasks

task 1 'run'. lines 16-16:
return values: 1

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
//# publish
module 0x42::m {

fun foo(x: &mut u64): u64 {
*x = *x + 1;
10
}

fun main(): u64 {
let x = 0;
for (i in 0..foo(&mut x)) {};
x
}
}

//# run 0x42::m::main
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
processed 2 tasks

task 1 'run'. lines 16-16:
return values: 1

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
//# publish
module 0x42::m {

fun foo(x: &mut u64): u64 {
*x = *x + 1;
10
}

fun main(): u64 {
let x = 0;
for (i in 0..foo(&mut x)) {};
x
}
}

//# run 0x42::m::main
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
comparison between v1 and v2 failed:
= processed 1 task
=
= task 0 'run'. lines 1-10:
- Error: error[E04007]: incompatible types
+ Error: compilation errors:
+ error: invalid call of `+`: expected `integer` but found `bool` for argument 1
= ┌─ TEMPFILE:5:9
- │
- 5 │ ╭ ╭ for (i in true..false) {
- │ ---- Found: 'bool'. It is not compatible with the other type.
- 6 │ │ │ x = x + 1;
- 7 │ │ │ };
- │ ╰─│─────────^ Incompatible arguments to '+'
- │ ╰─────────' Found: integer. It is not compatible with the other type.
-
- error[E04003]: built-in operation not supported
- ┌─ TEMPFILE:5:9
= │
= 5 │ ╭ for (i in true..false) {
- │ ---- Found: 'bool'. But expected: 'u8', 'u16', 'u32', 'u64', 'u128', 'u256'
= 6 │ │ x = x + 1;
= 7 │ │ };
- │ ╰─────────^ Invalid argument to '+'
+ │ ╰─────────^
=
- error[E04003]: built-in operation not supported
+ error: invalid call of `<`: expected `integer` but found `bool` for argument 1
= ┌─ TEMPFILE:5:9
= │
= 5 │ ╭ for (i in true..false) {
- │ ---- Found: 'bool'. But expected: 'u8', 'u16', 'u32', 'u64', 'u128', 'u256'
= 6 │ │ x = x + 1;
= 7 │ │ };
- │ ╰─────────^ Invalid argument to '<'
+ │ ╰─────────^
=
=
=
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
processed 2 tasks

task 1 'run'. lines 13-13:
return values: 12

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -1,10 +1,13 @@
//# publish
module 0x42::test {
fun for(i : u32, j: u32, k:u32) : u32 {
fun for(i: u32, j: u32, k: u32) : u32 {
i + j + k
}
fun for_user() : u32 {
public fun for_user() : u32 {
let (i, j, k) = (3, 4, 5);
let x = for(i, j, k);
x
}
}

//# run 0x42::test::for_user
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
processed 1 task

task 0 'run'. lines 1-10:
Error: Script execution failed with VMError: {
major_status: OUT_OF_GAS,
sub_status: None,
location: script,
indices: redacted,
offsets: redacted,
}

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
//# run --gas-budget 700
script {
fun main() {
loop {
loop break;
};
if (true) () else ();
assert!(false, 42);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
processed 1 task

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
//# run
script {
fun main(): () {
let y = 0;
for (i in 0..10) {
y = y + 1;
for (j in i..10) {
y = y + 1;
};
};
assert!(y == 65, 42);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
processed 1 task

==> Compiler v2 delivered same results!
Loading

0 comments on commit 8f0c41a

Please sign in to comment.