Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

For and While Loops #88

Merged
merged 17 commits into from
Sep 24, 2024
+188 −37
Merged

For and While Loops #88

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
326883e
Allow passing args to the contract's init function (#84) (#87)
ACassimiro Sep 16, 2024
184da55
First implementation of for loops and implementing initial test
ACassimiro Sep 18, 2024
dd9e5ed
Fixing int operations not working for variables and introducing first…
ACassimiro Sep 19, 2024
3328947
Adding test functions and corner case rule
ACassimiro Sep 19, 2024
57e4d7f
Adding tests and correcting scope
ACassimiro Sep 20, 2024
5bc1f42
Merge branch 'main' into for-loops
ACassimiro Sep 20, 2024
89450c6
Fixing range pattern definition working only for integer literals
ACassimiro Sep 20, 2024
b81f9d6
Removing wrong unnecessary definition and for loops with multiple pat…
ACassimiro Sep 21, 2024
4aedc14
Removing empty spaces
ACassimiro Sep 23, 2024
1b80f3e
Removing unnecessary variable creation
ACassimiro Sep 23, 2024
3260cac
Properly handling the range expression for loops
ACassimiro Sep 23, 2024
a9b7172
changing function name and enabling different integer types on for loops
ACassimiro Sep 24, 2024
0fe1c0d
Addressing review
ACassimiro Sep 24, 2024
12844f6
Organizing the rules and addressing review
ACassimiro Sep 24, 2024
324f966
Merge branch 'main' into for-loops
ACassimiro Sep 24, 2024
077e603
Add missing token
ACassimiro Sep 24, 2024
a85fc04
Removing return from stack on tests
ACassimiro Sep 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions rust-semantics/expression.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ requires "expression/bool-operations.md"
requires "expression/constants.md"
requires "expression/casts.md"
requires "expression/conditionals.md"
requires "expression/loops.md"
requires "expression/literals.md"
requires "expression/references.md"
requires "expression/struct.md"
Expand All @@ -17,6 +18,7 @@ module RUST-EXPRESSION
imports private RUST-EXPRESSION-CONSTANTS
imports private RUST-BLOCK-EXPRESSIONS
imports private RUST-CONDITIONAL-EXPRESSIONS
imports private RUST-LOOP-EXPRESSIONS
imports private RUST-EXPRESSION-LITERALS
imports private RUST-EXPRESSION-REFERENCES
imports private RUST-EXPRESSION-STRUCT
Expand Down
2 changes: 1 addition & 1 deletion rust-semantics/expression/conditionals.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module RUST-CONDITIONAL-EXPRESSIONS

rule (if ptrValue(_, true) A:BlockExpression else _:IfElseExpression):ExpressionWithBlock => A
rule (if ptrValue(_, false) _:BlockExpression else B:IfElseExpression):ExpressionWithBlock => B

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Remove spaces?

endmodule

```
68 changes: 34 additions & 34 deletions rust-semantics/expression/integer-operations.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,40 +50,40 @@ module RUST-INTEGER-RELATIONAL-OPERATIONS
imports RUST-SHARED-SYNTAX
imports private RUST-REPRESENTATION

rule ptrValue(null, i32(A):Value) == ptrValue(null, i32(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(null, i32(A):Value) != ptrValue(null, i32(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(null, i32(A):Value) > ptrValue(null, i32(B):Value) => ptrValue(null, A >sMInt B)
rule ptrValue(null, i32(A):Value) < ptrValue(null, i32(B):Value) => ptrValue(null, A <sMInt B)
rule ptrValue(null, i32(A):Value) >= ptrValue(null, i32(B):Value) => ptrValue(null, A >=sMInt B)
rule ptrValue(null, i32(A):Value) <= ptrValue(null, i32(B):Value) => ptrValue(null, A <=sMInt B)

rule ptrValue(null, u32(A):Value) == ptrValue(null, u32(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(null, u32(A):Value) != ptrValue(null, u32(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(null, u32(A):Value) > ptrValue(null, u32(B):Value) => ptrValue(null, A >uMInt B)
rule ptrValue(null, u32(A):Value) < ptrValue(null, u32(B):Value) => ptrValue(null, A <uMInt B)
rule ptrValue(null, u32(A):Value) >= ptrValue(null, u32(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(null, u32(A):Value) <= ptrValue(null, u32(B):Value) => ptrValue(null, A <=uMInt B)

rule ptrValue(null, i64(A):Value) == ptrValue(null, i64(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(null, i64(A):Value) != ptrValue(null, i64(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(null, i64(A):Value) > ptrValue(null, i64(B):Value) => ptrValue(null, A >sMInt B)
rule ptrValue(null, i64(A):Value) < ptrValue(null, i64(B):Value) => ptrValue(null, A <sMInt B)
rule ptrValue(null, i64(A):Value) >= ptrValue(null, i64(B):Value) => ptrValue(null, A >=sMInt B)
rule ptrValue(null, i64(A):Value) <= ptrValue(null, i64(B):Value) => ptrValue(null, A <=sMInt B)

rule ptrValue(null, u64(A):Value) == ptrValue(null, u64(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(null, u64(A):Value) != ptrValue(null, u64(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(null, u64(A):Value) > ptrValue(null, u64(B):Value) => ptrValue(null, A >uMInt B)
rule ptrValue(null, u64(A):Value) < ptrValue(null, u64(B):Value) => ptrValue(null, A <uMInt B)
rule ptrValue(null, u64(A):Value) >= ptrValue(null, u64(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(null, u64(A):Value) <= ptrValue(null, u64(B):Value) => ptrValue(null, A <=uMInt B)

rule ptrValue(null, u128(A):Value) == ptrValue(null, u128(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(null, u128(A):Value) != ptrValue(null, u128(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(null, u128(A):Value) > ptrValue(null, u128(B):Value) => ptrValue(null, A >uMInt B)
rule ptrValue(null, u128(A):Value) < ptrValue(null, u128(B):Value) => ptrValue(null, A <uMInt B)
rule ptrValue(null, u128(A):Value) >= ptrValue(null, u128(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(null, u128(A):Value) <= ptrValue(null, u128(B):Value) => ptrValue(null, A <=uMInt B)
rule ptrValue(_, i32(A):Value) == ptrValue(_, i32(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(_, i32(A):Value) != ptrValue(_, i32(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(_, i32(A):Value) > ptrValue(_, i32(B):Value) => ptrValue(null, A >sMInt B)
rule ptrValue(_, i32(A):Value) < ptrValue(_, i32(B):Value) => ptrValue(null, A <sMInt B)
rule ptrValue(_, i32(A):Value) >= ptrValue(_, i32(B):Value) => ptrValue(null, A >=sMInt B)
rule ptrValue(_, i32(A):Value) <= ptrValue(_, i32(B):Value) => ptrValue(null, A <=sMInt B)

rule ptrValue(_, u32(A):Value) == ptrValue(_, u32(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(_, u32(A):Value) != ptrValue(_, u32(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(_, u32(A):Value) > ptrValue(_, u32(B):Value) => ptrValue(null, A >uMInt B)
rule ptrValue(_, u32(A):Value) < ptrValue(_, u32(B):Value) => ptrValue(null, A <uMInt B)
rule ptrValue(_, u32(A):Value) >= ptrValue(_, u32(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(_, u32(A):Value) <= ptrValue(_, u32(B):Value) => ptrValue(null, A <=uMInt B)

rule ptrValue(_, i64(A):Value) == ptrValue(_, i64(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(_, i64(A):Value) != ptrValue(_, i64(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(_, i64(A):Value) > ptrValue(_, i64(B):Value) => ptrValue(null, A >sMInt B)
rule ptrValue(_, i64(A):Value) < ptrValue(_, i64(B):Value) => ptrValue(null, A <sMInt B)
rule ptrValue(_, i64(A):Value) >= ptrValue(_, i64(B):Value) => ptrValue(null, A >=sMInt B)
rule ptrValue(_, i64(A):Value) <= ptrValue(_, i64(B):Value) => ptrValue(null, A <=sMInt B)

rule ptrValue(_, u64(A):Value) == ptrValue(_, u64(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(_, u64(A):Value) != ptrValue(_, u64(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(_, u64(A):Value) > ptrValue(_, u64(B):Value) => ptrValue(null, A >uMInt B)
rule ptrValue(_, u64(A):Value) < ptrValue(_, u64(B):Value) => ptrValue(null, A <uMInt B)
rule ptrValue(_, u64(A):Value) >= ptrValue(_, u64(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(_, u64(A):Value) <= ptrValue(_, u64(B):Value) => ptrValue(null, A <=uMInt B)

rule ptrValue(_, u128(A):Value) == ptrValue(_, u128(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(_, u128(A):Value) != ptrValue(_, u128(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(_, u128(A):Value) > ptrValue(_, u128(B):Value) => ptrValue(null, A >uMInt B)
rule ptrValue(_, u128(A):Value) < ptrValue(_, u128(B):Value) => ptrValue(null, A <uMInt B)
rule ptrValue(_, u128(A):Value) >= ptrValue(_, u128(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(_, u128(A):Value) <= ptrValue(_, u128(B):Value) => ptrValue(null, A <=uMInt B)

endmodule

Expand Down
31 changes: 31 additions & 0 deletions rust-semantics/expression/loops.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
```k

module RUST-LOOP-EXPRESSIONS
imports RUST-SHARED-SYNTAX
imports RUST-VALUE-SYNTAX
imports INT
imports MINT

syntax IteratorLoopExpression ::= "for1" Pattern "in" ExpressionExceptStructExpression BlockExpression
| "for2" Pattern "in" ExpressionExceptStructExpression BlockExpression

rule for Patt:Identifier:PatternNoTopAlt | R:PatternNoTopAlts in First..Last B:BlockExpression =>
{
.InnerAttributes
(for1 Patt:Identifier:PatternNoTopAlt | R:PatternNoTopAlts in First..Last B:BlockExpression):IteratorLoopExpression; // Covers the cases of "for x | x in range"
.NonEmptyStatements
};

rule for1 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts in First..Last B:BlockExpression =>
let Patt = First; ~>
if (Patt :: .PathExprSegments):PathExprSegments < Last { .InnerAttributes B; (for2 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts in First..Last B):IteratorLoopExpression; .NonEmptyStatements};

rule for2 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts in _..Last B:BlockExpression =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u64(Int2MInt(1:Int)));
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmmm... This is interesting...

Right now, we have defined addition only between ints of the same kind, and I think that Rust does not allow adding ints of different types, e.g. 12u64 + 1u32 does not compile. Now, this probably works for our examples, but it's not correct, so here are some suggestions:

  • Add a TODO saying that this is wrong and it should be fixed.
  • define and use a function intOfSameType(1, Last) (Last should be a value when this rule is being applied, so it should have a concrete int type)

~> for Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts in (Patt :: .PathExprSegments):PathExprSegments..Last B

rule while (E:ExpressionExceptStructExpression) S:BlockExpression => if E { .InnerAttributes S; while(E)S; .NonEmptyStatements};

endmodule

```
6 changes: 4 additions & 2 deletions rust-semantics/rust-common-syntax.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -663,7 +663,8 @@ https://doc.rust-lang.org/reference/items/extern-crates.html

```k

syntax IteratorLoopExpression ::= "for" Pattern "in" ExpressionExceptStructExpression BlockExpression
syntax IteratorLoopExpression ::= "for" Pattern "in" ExpressionExceptStructExpression BlockExpression
| "while" ExpressionExceptStructExpression BlockExpression

```

Expand All @@ -680,6 +681,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
```k

syntax IfExpression ::= "if" ExpressionExceptStructExpression BlockExpression MaybeIfElseExpression [strict(1)]

syntax MaybeIfElseExpression ::= ""
| "else" IfElseExpression
syntax IfElseExpression ::= BlockExpression
Expand Down Expand Up @@ -769,7 +771,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html

```k

syntax RangePattern ::= "TODO: not needed yet, not implementing"
syntax RangePattern ::= Expression ".." Expression // "TODO: not needed yet, not implementing"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Remove the TODO since you just added this to the syntax.


```

Expand Down
2 changes: 2 additions & 0 deletions tests/execution/loops.1.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
new LoopExpressions;
call LoopExpressions.iterator_evaluation
2 changes: 2 additions & 0 deletions tests/execution/loops.2.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
new LoopExpressions;
call LoopExpressions.while_evaluation
2 changes: 2 additions & 0 deletions tests/execution/loops.3.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
new LoopExpressions;
call LoopExpressions.iterator_with_variables
36 changes: 36 additions & 0 deletions tests/execution/loops.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
#![no_std]

#[allow(unused_imports)]
use multiversx_sc::imports::*;

#[multiversx_sc::contract]
pub trait LoopExpressions {
#[init]
fn init(&self) {
}

#[upgrade]
fn upgrade(&self) {}

fn iterator_evaluation(&self){
for i in 1_u64..10_u64 {
let x = i * 2_u64;
};
}

fn while_evaluation(&self){
while 1_u64 < 1_u64 {
let x: u64 = 2_u64;
};
}

fn iterator_with_variables(&self) {
let y = 20_u64;
let z = 10_u64;

for i in z..y {
let x = i * 2_u64;
};
}

}
Loading