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

Int relational operators #76

Merged
merged 12 commits into from
Sep 9, 2024
Merged

Int relational operators #76

Show file tree
Hide file tree
Changes from 11 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
c4bb571
Extending Value to encompass booleans as well
ACassimiro Sep 4, 2024
0c902b5
Implementing relational operations for integers
ACassimiro Sep 5, 2024
df723ab
Adjusting tests and fixing ambiguity in execution
ACassimiro Sep 5, 2024
60b83ff
Add failing test
ACassimiro Sep 5, 2024
39ccfe6
Merge branch 'main' into int-relational-operators
ACassimiro Sep 5, 2024
d3fb1dd
Fixing missing implicitCast rule
ACassimiro Sep 5, 2024
a85e903
Adding tests
ACassimiro Sep 5, 2024
6d8c04e
Addressing review
ACassimiro Sep 5, 2024
dd66d41
Adding the Bool-Syntax to the shared syntax and injecting Bool into L…
ACassimiro Sep 6, 2024
def647f
removing meaningless space
ACassimiro Sep 6, 2024
1e9fc51
Merging with main and adjustments to the integer relational operations
ACassimiro Sep 7, 2024
a1fedf9
Converting bools to prtValue directly
ACassimiro Sep 9, 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
@@ -1,5 +1,6 @@
```k
requires "expression/calls.md"
requires "expression/integer-operations.md"
requires "expression/constants.md"
requires "expression/casts.md"
requires "expression/literals.md"
Expand All @@ -15,5 +16,6 @@ module RUST-EXPRESSION
imports private RUST-EXPRESSION-REFERENCES
imports private RUST-EXPRESSION-TOOLS
imports private RUST-EXPRESSION-VARIABLES
imports private RUST-INTEGER-OPERATIONS
endmodule
```
2 changes: 2 additions & 0 deletions rust-semantics/expression/casts.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,8 @@ module RUST-CASTS
rule implicitCast(u128(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(u128(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))

rule implicitCast(V:Bool, bool) => V

rule implicitCast(struct(T, _) #as V, T) => V

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

module RUST-INTEGER-OPERATIONS
imports private RUST-INTEGER-ARITHMETIC-OPERATIONS
imports private RUST-INTEGER-RELATIONAL-OPERATIONS
endmodule

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

// Operations are implemented only for the same types,
// as implicit type casting (coercion) is not available
// in Rust.

rule ptrValue(_, i32(A):Value) * ptrValue(_, i32(B):Value) => ptrValue(null, i32(A *MInt B))
rule ptrValue(_, i32(A):Value) + ptrValue(_, i32(B):Value) => ptrValue(null, i32(A +MInt B))
rule ptrValue(_, i32(A):Value) - ptrValue(_, i32(B):Value) => ptrValue(null, i32(A -MInt B))
rule ptrValue(_, i32(A):Value) / ptrValue(_, i32(B):Value) => ptrValue(null, i32(A /sMInt B))
rule ptrValue(_, i32(A):Value) % ptrValue(_, i32(B):Value) => ptrValue(null, i32(A %sMInt B))

rule ptrValue(_, u32(A):Value) * ptrValue(_, u32(B):Value) => ptrValue(null, u32(A *MInt B))
rule ptrValue(_, u32(A):Value) + ptrValue(_, u32(B):Value) => ptrValue(null, u32(A +MInt B))
rule ptrValue(_, u32(A):Value) - ptrValue(_, u32(B):Value) => ptrValue(null, u32(A -MInt B))
rule ptrValue(_, u32(A):Value) / ptrValue(_, u32(B):Value) => ptrValue(null, u32(A /uMInt B))
rule ptrValue(_, u32(A):Value) % ptrValue(_, u32(B):Value) => ptrValue(null, u32(A %uMInt B))

rule ptrValue(_, i64(A):Value) * ptrValue(_, i64(B):Value) => ptrValue(null, i64(A *MInt B))
rule ptrValue(_, i64(A):Value) + ptrValue(_, i64(B):Value) => ptrValue(null, i64(A +MInt B))
rule ptrValue(_, i64(A):Value) - ptrValue(_, i64(B):Value) => ptrValue(null, i64(A -MInt B))
rule ptrValue(_, i64(A):Value) / ptrValue(_, i64(B):Value) => ptrValue(null, i64(A /sMInt B))
rule ptrValue(_, i64(A):Value) % ptrValue(_, i64(B):Value) => ptrValue(null, i64(A %sMInt B))

rule ptrValue(_, u64(A):Value) * ptrValue(_, u64(B):Value) => ptrValue(null, u64(A *MInt B))
rule ptrValue(_, u64(A):Value) + ptrValue(_, u64(B):Value) => ptrValue(null, u64(A +MInt B))
rule ptrValue(_, u64(A):Value) - ptrValue(_, u64(B):Value) => ptrValue(null, u64(A -MInt B))
rule ptrValue(_, u64(A):Value) / ptrValue(_, u64(B):Value) => ptrValue(null, u64(A /uMInt B))
rule ptrValue(_, u64(A):Value) % ptrValue(_, u64(B):Value) => ptrValue(null, u64(A %uMInt B))

rule ptrValue(_, u128(A):Value) * ptrValue(_, u128(B):Value) => ptrValue(null, u128(A *MInt B))
rule ptrValue(_, u128(A):Value) + ptrValue(_, u128(B):Value) => ptrValue(null, u128(A +MInt B))
rule ptrValue(_, u128(A):Value) - ptrValue(_, u128(B):Value) => ptrValue(null, u128(A -MInt B))
rule ptrValue(_, u128(A):Value) / ptrValue(_, u128(B):Value) => ptrValue(null, u128(A /uMInt B))
rule ptrValue(_, u128(A):Value) % ptrValue(_, u128(B):Value) => ptrValue(null, u128(A %uMInt B))

endmodule


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)

endmodule

```
1 change: 1 addition & 0 deletions rust-semantics/expression/literals.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ module RUST-EXPRESSION-INTEGER-LITERALS
syntax String ::= IntegerLiteralToString(IntegerLiteral) [function, total, hook(STRING.token2string)]

rule I:IntegerLiteral => wrapPtrValueOrError(null, parseInteger(I))
rule B:Bool:LiteralExpression => wrapPtrValueOrError(null, B:Bool:Value)
Copy link
Member

Choose a reason for hiding this comment

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

This works, but you could also write ptrValue(null, B:Bool:Value) directly.


syntax ValueOrError ::= parseInteger(IntegerLiteral) [function, total]
| parseInteger(String) [function, total]
Expand Down
2 changes: 0 additions & 2 deletions rust-semantics/preprocessing.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
```k

requires "preprocessing/arithmetic-operations.md"
requires "preprocessing/constants.md"
requires "preprocessing/crate.md"
requires "preprocessing/configuration.md"
Expand All @@ -16,7 +15,6 @@ module RUST-PREPROCESSING
imports private INITIALIZATION
imports private TRAIT
imports private TRAIT-METHODS
imports private RUST-INTEGER-ARITHMETIC-OPERATIONS
endmodule

```
42 changes: 0 additions & 42 deletions rust-semantics/preprocessing/arithmetic-operations.md
View file
Open in desktop

This file was deleted.

3 changes: 3 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,6 +23,7 @@ module RUST-VALUE-SYNTAX
| u128(MInt{128})
| tuple(ValueList)
| struct(TypePath, Map) // Map from field name (Identifier) to value ID (Int)
| Bool

syntax ValueList ::= List{Value, ","}
syntax ValueOrError ::= Value | SemanticsError
Expand Down Expand Up @@ -74,6 +75,8 @@ module RUST-REPRESENTATION
| "u32" [token]
| "i64" [token]
| "u64" [token]
| "bool" [token]

syntax MaybeIdentifier ::= ".Identifier" | Identifier

syntax ExpressionOrCallParams ::= Expression | CallParams
Expand Down
15 changes: 8 additions & 7 deletions rust-semantics/rust-common-syntax.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ endmodule

module RUST-SHARED-SYNTAX
imports STRING-SYNTAX
imports BOOL-SYNTAX
```

https://doc.rust-lang.org/reference/crates-and-source-files.html
Expand Down Expand Up @@ -257,7 +258,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
| ByteLiteral | ByteStringLiteral | RawByteStringLiteral
| CStringLiteral | RawCStringLiteral
| IntegerLiteral | FloatLiteral
| "true" | "false"
Copy link
Member

Choose a reason for hiding this comment

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

Are you sure these aren't needed here? Would this grammar still parse a .rs file containing true/false? Even if the file is still parsable (e.g. it may identify true/false as identifiers), why is it a good idea to remove these?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

My motivation for removing them was to primarily eliminate parsing ambiguity in the execution module. Having a syntax element named true of type Expression was causing issues on, for instance, the check_eq true in the testing files, as it didn't recognize if this true was an Expression or a Bool.

Keeping Bool as a part of Values is also advantageous for us as we do not need to write new rules for assignments of constants and variables, and also makes it easier for us to reuse the return of the relational operations of MInts.

Finally, please, correct me if I'm wrong, but my understanding is that an Expression can also be constituted by a single Value. So having Booleans as a part of Values allows us to have effectively the same syntax of adding true and false to the Expression definition, with the advantage of having the boolean operations implemented in the BOOL module being supported here.

| Bool

syntax CharLiteral ::= "TODO: not needed yet, not implementing"
// TODO: Not implemented properly
Expand Down Expand Up @@ -373,12 +374,12 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
| Expression "^" Expression
| Expression "|" Expression

> Expression "==" Expression
| Expression "!=" Expression
| Expression ">" Expression
| Expression "<" Expression
| Expression ">=" Expression
| Expression "<=" Expression
> Expression "==" Expression [seqstrict]
| Expression "!=" Expression [seqstrict]
| Expression ">" Expression [seqstrict]
| Expression "<" Expression [seqstrict]
| Expression ">=" Expression [seqstrict]
| Expression "<=" Expression [seqstrict]

> left:
Expression "&&" Expression
Expand Down
2 changes: 2 additions & 0 deletions rust-semantics/targets/preprocessing/rust.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,15 @@ requires "../../expression/casts.md"
requires "../../expression/constants.md"
requires "../../expression/literals.md"
requires "../../rust-common-syntax.md"
requires "../../expression/integer-operations.md"

module RUST-SYNTAX
imports RUST-COMMON-SYNTAX
endmodule

module RUST
imports private RUST-EXPRESSION-LITERALS
imports private RUST-INTEGER-OPERATIONS
imports private RUST-EXPRESSION-CONSTANTS
imports private RUST-PREPROCESSING
imports private RUST-RUNNING-CONFIGURATION
Expand Down
4 changes: 0 additions & 4 deletions tests/execution/arithmetic-expression.1.run
View file
Open in desktop

This file was deleted.

4 changes: 0 additions & 4 deletions tests/execution/arithmetic-expression.2.run
View file
Open in desktop

This file was deleted.

4 changes: 0 additions & 4 deletions tests/execution/arithmetic-expression.3.run
View file
Open in desktop

This file was deleted.

4 changes: 0 additions & 4 deletions tests/execution/arithmetic-expression.4.run
View file
Open in desktop

This file was deleted.

4 changes: 0 additions & 4 deletions tests/execution/arithmetic-expression.5.run
View file
Open in desktop

This file was deleted.

4 changes: 4 additions & 0 deletions tests/execution/integer-operations.1.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
new IntegerOperations;
call IntegerOperations.arithmetic_expression_mult_constant;
return_value;
check_eq 86400_u64
4 changes: 4 additions & 0 deletions tests/execution/integer-operations.10.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
new IntegerOperations;
call IntegerOperations.relational_expression_smaller;
return_value;
check_eq true
4 changes: 4 additions & 0 deletions tests/execution/integer-operations.11.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
new IntegerOperations;
call IntegerOperations.relational_expression_greater;
return_value;
check_eq false
4 changes: 4 additions & 0 deletions tests/execution/integer-operations.2.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
new IntegerOperations;
call IntegerOperations.arithmetic_expression_div_constant;
return_value;
check_eq 2_u64
4 changes: 4 additions & 0 deletions tests/execution/integer-operations.3.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
new IntegerOperations;
call IntegerOperations.arithmetic_expression_sum_constant;
return_value;
check_eq 101_u64
4 changes: 4 additions & 0 deletions tests/execution/integer-operations.4.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
new IntegerOperations;
call IntegerOperations.arithmetic_expression_sub_constant;
return_value;
check_eq 99_u64
4 changes: 4 additions & 0 deletions tests/execution/integer-operations.5.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
new IntegerOperations;
call IntegerOperations.arithmetic_expression_mod_constant;
return_value;
check_eq 2_u64
4 changes: 4 additions & 0 deletions tests/execution/integer-operations.6.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
new IntegerOperations;
call IntegerOperations.relational_expression_equals;
return_value;
check_eq true
4 changes: 4 additions & 0 deletions tests/execution/integer-operations.7.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
new IntegerOperations;
call IntegerOperations.relational_expression_diff;
return_value;
check_eq false
4 changes: 4 additions & 0 deletions tests/execution/integer-operations.8.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
new IntegerOperations;
call IntegerOperations.relational_expression_smaller_or_equal;
return_value;
check_eq true
4 changes: 4 additions & 0 deletions tests/execution/integer-operations.9.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
new IntegerOperations;
call IntegerOperations.relational_expression_greater_or_equal;
return_value;
check_eq true
14 changes: 13 additions & 1 deletion tests/execution/arithmetic-expression.rs → tests/execution/integer-operations.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
use multiversx_sc::imports::*;

#[multiversx_sc::contract]
pub trait ArithmeticExpression {
pub trait IntegerOperations {
#[init]
fn init(&self) {
}
Expand All @@ -22,4 +22,16 @@ pub trait ArithmeticExpression {

fn arithmetic_expression_mod_constant(&self) -> u64 { 5_u64 % 3_u64 }

fn relational_expression_equals(&self) -> bool { 5_u64 == 5_u64 }

fn relational_expression_diff(&self) -> bool { 5_i64 != 5_i64 }

fn relational_expression_smaller_or_equal(&self) -> bool { 5 >= 5 }

fn relational_expression_greater_or_equal(&self) -> bool { 70 >= 7 }

fn relational_expression_smaller(&self) -> bool { 5_u32 < 7_u32 }

fn relational_expression_greater(&self) -> bool { 5_i32 > 7_i32 }

}
Loading