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
Merged

For and While Loops #88

Show file tree
Hide file tree
Changes from 13 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
82 changes: 48 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 @@ -3,6 +3,7 @@
module RUST-INTEGER-OPERATIONS
imports private RUST-INTEGER-ARITHMETIC-OPERATIONS
imports private RUST-INTEGER-RELATIONAL-OPERATIONS
imports private RUST-INTEGER-RANGE-OPERATIONS
endmodule

module RUST-INTEGER-ARITHMETIC-OPERATIONS
Expand Down Expand Up @@ -50,40 +51,53 @@ 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


module RUST-INTEGER-RANGE-OPERATIONS
imports RUST-SHARED-SYNTAX
imports private RUST-REPRESENTATION

rule (ptrValue(_, i32(A):Value) .. ptrValue(_, i32(B):Value)):Expression => ptrValue(null, intRange(i32(A), i32(B)))
rule (ptrValue(_, u32(A):Value) .. ptrValue(_, u32(B):Value)):Expression => ptrValue(null, intRange(u32(A), u32(B)))
rule (ptrValue(_, i64(A):Value) .. ptrValue(_, i64(B):Value)):Expression => ptrValue(null, intRange(i64(A), i64(B)))
rule (ptrValue(_, u64(A):Value) .. ptrValue(_, u64(B):Value)):Expression => ptrValue(null, intRange(u64(A), u64(B)))
rule (ptrValue(_, u128(A):Value) .. ptrValue(_, u128(B):Value)):Expression => ptrValue(null, intRange(u128(A), u128(B)))

endmodule

Expand Down
50 changes: 50 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,50 @@
```k

module RUST-LOOP-EXPRESSIONS
imports RUST-REPRESENTATION

syntax IteratorLoopExpression ::= "for1" Pattern "limit" PtrValue BlockExpression
| "for2" Pattern "limit" PtrValue BlockExpression

rule for Patt:Identifier:PatternNoTopAlt | R:PatternNoTopAlts in ptrValue(_, intRange(First, Last)) B:BlockExpression =>
{
.InnerAttributes
let Patt = ptrValue(null, First);
(for1 Patt | R limit ptrValue(null, Last) B):IteratorLoopExpression;
.NonEmptyStatements
};
requires checkIntOfSameType(First, Last)

rule for1 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts limit Last B:BlockExpression =>
if (Patt :: .PathExprSegments):PathExprSegments < Last { .InnerAttributes B; (for2 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts limit Last B):IteratorLoopExpression; .NonEmptyStatements};
Copy link
Member

Choose a reason for hiding this comment

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

I would split this into multiple lines.

Also, you can probably inline the "for2" rule below if you want.


rule for2 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts limit ptrValue(_, LastValue) #as Last B:BlockExpression =>
incrementPatt(Patt, LastValue)
~> for1 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts limit Last B

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


// Necessary for handling all possible integer types provided in the range expression of for loops
syntax LetStatement ::= incrementPatt(Identifier, Value) [function]

rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i32(Int2MInt(1:Int)));
requires checkIntOfType(ComparisonValue, i32)
rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u32(Int2MInt(1:Int)));
requires checkIntOfType(ComparisonValue, u32)
rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
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)

requires checkIntOfType(ComparisonValue, u64)
rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i64(Int2MInt(1:Int)));
requires checkIntOfType(ComparisonValue, i64)
rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u128(Int2MInt(1:Int)));
requires checkIntOfType(ComparisonValue, u128)


endmodule

```
23 changes: 23 additions & 0 deletions rust-semantics/representation.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,9 +23,13 @@ module RUST-VALUE-SYNTAX
| u128(MInt{128})
| tuple(ValueList)
| struct(TypePath, Map) // Map from field name (Identifier) to value ID (Int)
| Range
| Bool
| String


syntax Range ::= intRange(Value, Value) //[seqstrict]

syntax ValueList ::= List{Value, ","}
syntax ValueOrError ::= Value | SemanticsError

Expand Down Expand Up @@ -83,6 +87,7 @@ module RUST-REPRESENTATION
| "u32" [token]
| "i64" [token]
| "u64" [token]
| "u128" [token]
| "bool" [token]

syntax MaybeIdentifier ::= ".Identifier" | Identifier
Expand All @@ -101,6 +106,24 @@ module RUST-REPRESENTATION

syntax CallParamsList ::= reverse(CallParamsList, CallParamsList) [function, total]



syntax Bool ::= checkIntOfType(Value, Type) [function, total]
| checkIntOfSameType(Value, Value) [function, total]

rule checkIntOfType(u32(_), u32) => true
rule checkIntOfType(i32(_), i32) => true
rule checkIntOfType(u64(_), u64) => true
rule checkIntOfType(i64(_), i64) => true
rule checkIntOfType(i64(_), u128) => true
rule checkIntOfType(_, _) => false [owise]

rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, u32) requires checkIntOfType(B, u32)
rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, i32) requires checkIntOfType(B, i32)
rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, u64) requires checkIntOfType(B, u64)
rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, i64) requires checkIntOfType(B, i64)
rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, u128) requires checkIntOfType(B, u128)
rule checkIntOfSameType(_, _) => false [owise]
endmodule

```
8 changes: 5 additions & 3 deletions rust-semantics/rust-common-syntax.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -391,7 +391,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
Expression "&&" Expression [seqstrict]
| Expression "||" Expression [seqstrict]

> Expression ".." Expression
> Expression ".." Expression [seqstrict]

> right:
Expression "=" Expression
Expand Down 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 [seqstrict(2)]
| "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

```

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
2 changes: 2 additions & 0 deletions tests/execution/loops.4.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_same_pattern
43 changes: 43 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,43 @@
#![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;
};
}

fn iterator_with_same_pattern(&self) {
let i = 1_u64;
for i in i..i+3_u64 {
let x = i * 2_u64;
};
}

}