diff --git a/Makefile b/Makefile index b2c857a..f73ddef 100644 --- a/Makefile +++ b/Makefile @@ -63,9 +63,10 @@ $(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: $(EXECUTION_INPUT_DIR)/%.run $(RUST krun \ "$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \ --definition $(RUST_EXECUTION_KOMPILED) \ + --parser $(CURDIR)/parse-rust.sh \ --output kore \ --output-file $@.tmp \ -cTEST="$(shell cat $<)" \ - -pTEST=$(CURDIR)/run-test.sh + -pTEST=$(CURDIR)/parse-test.sh cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())" mv -f $@.tmp $@ diff --git a/README.md b/README.md index a672291..15c1d7a 100644 --- a/README.md +++ b/README.md @@ -240,6 +240,19 @@ We will ignore: use declaratios, some attributes and macros. We will not handle: extern crates, functions, type aliases, enumerations, unions, static items, external blocks. +Int literals and casts +---------------------- + +Int literal [type determination](https://doc.rust-lang.org/stable/reference/expressions/literal-expr.html#integer-literal-expressions) + +We will not implement explicit casts. However, int literals with a default type +are special in that they have some implicit casts determined by the context. + +To implement that, we will follow the algorithm in the link above, converting +everything to `u128`, then we will do a conversion on the spot if something +else is required. This should mostly work, since we are relying on the Rust +compiler to check that int types are properly used. + Other things not discussed elsewhere ------------------------------------ diff --git a/deps/k_release b/deps/k_release index 0299866..25b8aaf 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.1.92 +7.1.121 diff --git a/parse-rust.sh b/parse-rust.sh new file mode 100755 index 0000000..1833265 --- /dev/null +++ b/parse-rust.sh @@ -0,0 +1,8 @@ +#! /bin/bash + +kast \ + --output kore \ + --definition .build/rust-execution-kompiled \ + --module RUST-COMMON-SYNTAX \ + --sort Crate \ + $1 diff --git a/run-test.sh b/parse-test.sh similarity index 100% rename from run-test.sh rename to parse-test.sh diff --git a/rust-semantics/execution/block.md b/rust-semantics/execution/block.md index 5ef8832..c478852 100644 --- a/rust-semantics/execution/block.md +++ b/rust-semantics/execution/block.md @@ -1,6 +1,7 @@ ```k module RUST-BLOCK + imports RUST-REPRESENTATION imports RUST-SHARED-SYNTAX imports RUST-STACK @@ -12,6 +13,10 @@ module RUST-BLOCK // variable shadowing rule {.InnerAttributes S:Statements}:BlockExpression => pushLocalState ~> S ~> popLocalState + + // Blocks are always value expressions and evaluate the last operand in + // value expression context. + rule V:Value ~> popLocalState => popLocalState ~> V endmodule ``` diff --git a/rust-semantics/execution/calls.md b/rust-semantics/execution/calls.md index 7ea8177..e005cbf 100644 --- a/rust-semantics/execution/calls.md +++ b/rust-semantics/execution/calls.md @@ -24,12 +24,14 @@ module RUST-CALLS ~> clearLocalState ~> setArgs(Args, Params) ~> FunctionBody + ~> implicitCastTo(ReturnType) ~> popLocalState ... TraitName MethodName Params:NormalizedFunctionParameterList + ReturnType:Type block(FunctionBody) rule diff --git a/rust-semantics/expression/casts.md b/rust-semantics/expression/casts.md index 5c09b8e..ebbd293 100644 --- a/rust-semantics/expression/casts.md +++ b/rust-semantics/expression/casts.md @@ -3,38 +3,44 @@ module RUST-CASTS imports private RUST-REPRESENTATION - syntax ValueOrError ::= cast(Value, Type) [function, total] + syntax ValueOrError ::= implicitCast(Value, Type) [function, total] - rule cast(V:Value, T:Type) => error("Unknown cast.", ListItem(V) ListItem(T)) + rule implicitCast(V:Value, T:Type) => error("Unknown implicitCast.", ListItem(V) ListItem(T)) [owise] - // https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-cast + // https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-implicitCast - rule cast(i32(Value), i32) => i32(Value) - rule cast(i32(Value), u32) => u32(Value) - rule cast(i32(Value), i64) => i64(Int2MInt(MInt2Signed(Value))) - rule cast(i32(Value), u64) => u64(Int2MInt(MInt2Signed(Value))) + rule implicitCast(i32(Value), i32) => i32(Value) + rule implicitCast(i32(Value), u32) => u32(Value) + rule implicitCast(i32(Value), i64) => i64(Int2MInt(MInt2Signed(Value))) + rule implicitCast(i32(Value), u64) => u64(Int2MInt(MInt2Signed(Value))) - rule cast(u32(Value), i32) => i32(Value) - rule cast(u32(Value), u32) => u32(Value) - rule cast(u32(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value))) - rule cast(u32(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value))) + rule implicitCast(u32(Value), i32) => i32(Value) + rule implicitCast(u32(Value), u32) => u32(Value) + rule implicitCast(u32(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value))) + rule implicitCast(u32(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value))) - rule cast(i64(Value), i32) => i32(Int2MInt(MInt2Signed(Value))) - rule cast(i64(Value), u32) => u32(Int2MInt(MInt2Signed(Value))) - rule cast(i64(Value), i64) => i64(Value) - rule cast(i64(Value), u64) => u64(Value) + rule implicitCast(i64(Value), i32) => i32(Int2MInt(MInt2Signed(Value))) + rule implicitCast(i64(Value), u32) => u32(Int2MInt(MInt2Signed(Value))) + rule implicitCast(i64(Value), i64) => i64(Value) + rule implicitCast(i64(Value), u64) => u64(Value) - rule cast(u64(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value))) - rule cast(u64(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value))) - rule cast(u64(Value), i64) => i64(Value) - rule cast(u64(Value), u64) => u64(Value) + rule implicitCast(u64(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value))) + rule implicitCast(u64(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value))) + rule implicitCast(u64(Value), i64) => i64(Value) + rule implicitCast(u64(Value), u64) => u64(Value) - rule cast(u128(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value))) - rule cast(u128(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value))) - rule cast(u128(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value))) - rule cast(u128(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value))) + rule implicitCast(u128(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value))) + rule implicitCast(u128(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value))) + rule implicitCast(u128(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value))) + rule implicitCast(u128(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value))) + + // Rewrites + + rule V:Value ~> implicitCastTo(T:Type) => implicitCast(V, T) + // We don't need a value for the unit type + rule implicitCastTo(( )) => .K endmodule diff --git a/rust-semantics/preprocessing/constants.md b/rust-semantics/preprocessing/constants.md index db7a118..76caa73 100644 --- a/rust-semantics/preprocessing/constants.md +++ b/rust-semantics/preprocessing/constants.md @@ -10,7 +10,7 @@ module RUST-CONSTANTS rule (const Name:Identifier : T:Type = V:Value;):ConstantItem:KItem - => setConstant(Name, cast(V, T)) + => setConstant(Name, implicitCast(V, T)) rule diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md index 05cf311..bc89a65 100644 --- a/rust-semantics/representation.md +++ b/rust-semantics/representation.md @@ -1,11 +1,11 @@ ```k -module RUST-REPRESENTATION - imports INT +module RUST-VALUE-SYNTAX imports LIST // for filling the second argument of `error`. imports MAP imports MINT imports RUST-SHARED-SYNTAX + imports STRING syntax MInt{8} syntax MInt{16} @@ -15,18 +15,6 @@ module RUST-REPRESENTATION syntax SemanticsError ::= error(String, KItem) - syntax FunctionBodyRepresentation ::= block(BlockExpression) - | "empty" - | storageAccessor(StringLiteral) - syntax NormalizedFunctionParameter ::= Identifier ":" Type - syntax NormalizedFunctionParameterList ::= List{NormalizedFunctionParameter, ","} - - syntax NormalizedCallParams ::=List{Int, ","} - - syntax Instruction ::= normalizedMethodCall(TypePath, Identifier, NormalizedCallParams) - - syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError - syntax Value ::= i32(MInt{32}) | u32(MInt{32}) | i64(MInt{64}) @@ -34,11 +22,31 @@ module RUST-REPRESENTATION | u128(MInt{128}) | tuple(ValueList) | struct(TypePath, Map) // Map from field name (Identifier) to value ID (Int) + syntax ValueList ::= List{Value, ","} syntax Expression ::= Value syntax KResult ::= Value syntax ValueOrError ::= Value | SemanticsError +endmodule + +module RUST-REPRESENTATION + imports INT + imports RUST-SHARED-SYNTAX + imports RUST-VALUE-SYNTAX + + syntax FunctionBodyRepresentation ::= block(BlockExpression) + | "empty" + | storageAccessor(StringLiteral) + syntax NormalizedFunctionParameter ::= Identifier ":" Type + syntax NormalizedFunctionParameterList ::= List{NormalizedFunctionParameter, ","} + + syntax NormalizedCallParams ::=List{Int, ","} + + syntax Instruction ::= normalizedMethodCall(TypePath, Identifier, NormalizedCallParams) + | implicitCastTo(Type) + + syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError syntax Type ::= "$selftype" diff --git a/rust-semantics/rust-common-syntax.md b/rust-semantics/rust-common-syntax.md index 0746f21..2932643 100644 --- a/rust-semantics/rust-common-syntax.md +++ b/rust-semantics/rust-common-syntax.md @@ -454,7 +454,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html ``` - https://doc.rust-lang.org/reference/expressions/operator-expr.html#type-cast-expressions + https://doc.rust-lang.org/reference/expressions/operator-expr.html#type-implicitCast-expressions ```k @@ -952,7 +952,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html // // As an example, this means that you can't simply write // - // rule cast(u64(Value), u64) => u64(Value) + // rule implicitCast(u64(Value), u64) => u64(Value) // // because that rule will compile just fine, but it will never apply at // runtime because it uses an injection (why??? there is no injection @@ -960,7 +960,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html // (the K rule will also produce lists from `u64` sometimes, I'm not yet sure // when). Instead, you need to write // - // rule cast(u64(Value), u64 :: .TypePathSegments) => u64(Value) + // rule implicitCast(u64(Value), u64 :: .TypePathSegments) => u64(Value) // // which will work, but you have to figure out all cases where this may happen // without any help from the compiler. diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md index 7d92941..7f98469 100644 --- a/rust-semantics/test/execution.md +++ b/rust-semantics/test/execution.md @@ -2,11 +2,14 @@ module RUST-EXECUTION-TEST-PARSING-SYNTAX imports RUST-SHARED-SYNTAX + imports RUST-VALUE-SYNTAX syntax ExecutionTest ::= NeList{ExecutionItem, ";"} // syntax ExecutionTest ::= ExecutionItem ";" ExecutionItem syntax ExecutionItem ::= "new" TypePath | "call" TypePath "." Identifier + | "return_value" + | "check_eq" Expression [strict] endmodule module RUST-EXECUTION-TEST @@ -61,6 +64,15 @@ module RUST-EXECUTION-TEST Args:NormalizedCallParams, 0 ) => normalizedMethodCall(TraitName, MethodName, Args) + + rule + (V:Value ~> return_value ; Es:ExecutionTest) => Es ... + .List => ListItem(V) ... + + rule + check_eq V:Value => .K ... + ListItem(V) => .List ... + endmodule ``` \ No newline at end of file diff --git a/tests/execution/final-expression.1.run b/tests/execution/final-expression.1.run new file mode 100644 index 0000000..0a99a58 --- /dev/null +++ b/tests/execution/final-expression.1.run @@ -0,0 +1,4 @@ +new FinalExpression; +call FinalExpression.constant; +return_value; +check_eq 100_u64 diff --git a/tests/execution/final-expression.2.run b/tests/execution/final-expression.2.run new file mode 100644 index 0000000..c391cb0 --- /dev/null +++ b/tests/execution/final-expression.2.run @@ -0,0 +1,4 @@ +new FinalExpression; +call FinalExpression.constant_cast; +return_value; +check_eq 100_u64 diff --git a/tests/execution/final-expression.rs b/tests/execution/final-expression.rs new file mode 100644 index 0000000..8e09fa7 --- /dev/null +++ b/tests/execution/final-expression.rs @@ -0,0 +1,18 @@ +#![no_std] + +#[allow(unused_imports)] +use multiversx_sc::imports::*; + +#[multiversx_sc::contract] +pub trait FinalExpression { + #[init] + fn init(&self) { + } + + #[upgrade] + fn upgrade(&self) {} + + fn constant(&self) -> u64 { 100_u64 } + + fn constant_cast(&self) -> u64 { 100 } +} diff --git a/tests/syntax/lending.rs b/tests/syntax/lending.rs index 23353c8..ccb624f 100644 --- a/tests/syntax/lending.rs +++ b/tests/syntax/lending.rs @@ -84,7 +84,7 @@ pub trait Lending { let token_amount = self.token_amount(&token).get(); let token_shares = self.token_shares(&token).get(); - let shares = + let shares = self.to_shares( &amount, &token_amount, @@ -111,7 +111,7 @@ pub trait Lending { let token_borrowed = self.token_borrowed(&token).get(); let token_borrowed_shares = self.token_borrowed_shares(&token).get(); - let shares = + let shares = self.to_shares( &amount, &token_borrowed,