Implement final expressions (#64)

* Tests for final expressions

* Return correctly typed value

* Cast the returned value to the right type

* Rename cast -> implicitCast

* Update K

* Explain implicit casts for literals

---------

Co-authored-by: Virgil Serbanuta <Virgil Serbanuta>

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 $@

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
 ------------------------------------
 

deps/k_release

@@ -1 +1 @@
-7.1.92
+7.1.121

parse-rust.sh

@@ -0,0 +1,8 @@
+#! /bin/bash
+
+kast \
+    --output kore \
+    --definition .build/rust-execution-kompiled \
+    --module RUST-COMMON-SYNTAX \
+    --sort Crate \
+    $1

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
 
 ```

rust-semantics/execution/calls.md

@@ -24,12 +24,14 @@ module RUST-CALLS
                 ~> clearLocalState
                 ~> setArgs(Args, Params)
                 ~> FunctionBody
+                ~> implicitCastTo(ReturnType)
                 ~> popLocalState
             ...
         </k>
         <trait-path> TraitName </trait-path>
         <method-name> MethodName </method-name>
         <method-params> Params:NormalizedFunctionParameterList </method-params>
+        <method-return-type> ReturnType:Type </method-return-type>
         <method-implementation> block(FunctionBody) </method-implementation>
 
     rule

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
 

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
         <k>

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,30 +15,38 @@ 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})
                     | u64(MInt{64})
                     | 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"
 

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,15 +952,15 @@ 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
   // available!), while the parser will produce actual TypePathSegments lists
   // (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.

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
+        <k> (V:Value ~> return_value ; Es:ExecutionTest) => Es ... </k>
+        <test-stack> .List => ListItem(V) ... </test-stack>
+
+    rule
+        <k> check_eq V:Value => .K ... </k>
+        <test-stack> ListItem(V) => .List ... </test-stack>
+
 endmodule
 
 ```

tests/execution/final-expression.1.run

@@ -0,0 +1,4 @@
+new FinalExpression;
+call FinalExpression.constant;
+return_value;
+check_eq 100_u64

tests/execution/final-expression.2.run

@@ -0,0 +1,4 @@
+new FinalExpression;
+call FinalExpression.constant_cast;
+return_value;
+check_eq 100_u64

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 }
+}

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,