From 63da57673652f88c6934dc9daf83a3751db863fb Mon Sep 17 00:00:00 2001 From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com> Date: Thu, 22 Aug 2024 11:56:58 +0300 Subject: [PATCH] Refactor and finish implementing trait preprocessing (#4) * Rename indexing -> preprocessing * Refactor trait initialization * Refactor addMethod * Function arguments test * Return type test --------- Co-authored-by: Virgil Serbanuta --- .gitignore | 1 + Makefile | 2 +- rust-semantics/config.md | 6 +- rust-semantics/indexing.md | 19 --- rust-semantics/indexing/configuration.md | 32 ----- rust-semantics/indexing/helpers.md | 35 ------ rust-semantics/indexing/initialization.md | 119 ------------------ rust-semantics/indexing/syntax.md | 46 ------- rust-semantics/preprocessing.md | 19 +++ rust-semantics/preprocessing/configuration.md | 34 +++++ .../{indexing => preprocessing}/crate.md | 16 +-- rust-semantics/preprocessing/helpers.md | 96 ++++++++++++++ .../preprocessing/initialization.md | 68 ++++++++++ rust-semantics/preprocessing/syntax.md | 41 ++++++ .../trait-methods.md | 4 +- .../{indexing => preprocessing}/trait.md | 2 +- rust-semantics/representation.md | 4 + rust-semantics/rust.md | 4 +- tests/execution/function-arguments.rs | 24 ++++ tests/execution/function-return-type.rs | 17 +++ 20 files changed, 322 insertions(+), 267 deletions(-) delete mode 100644 rust-semantics/indexing.md delete mode 100644 rust-semantics/indexing/configuration.md delete mode 100644 rust-semantics/indexing/helpers.md delete mode 100644 rust-semantics/indexing/initialization.md delete mode 100644 rust-semantics/indexing/syntax.md create mode 100644 rust-semantics/preprocessing.md create mode 100644 rust-semantics/preprocessing/configuration.md rename rust-semantics/{indexing => preprocessing}/crate.md (86%) create mode 100644 rust-semantics/preprocessing/helpers.md create mode 100644 rust-semantics/preprocessing/initialization.md create mode 100644 rust-semantics/preprocessing/syntax.md rename rust-semantics/{indexing => preprocessing}/trait-methods.md (71%) rename rust-semantics/{indexing => preprocessing}/trait.md (76%) create mode 100644 tests/execution/function-arguments.rs create mode 100644 tests/execution/function-return-type.rs diff --git a/.gitignore b/.gitignore index 84d8b56..c733e44 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ .build +.DS_store tmp diff --git a/Makefile b/Makefile index b2af1fb..d5f00d3 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,4 @@ -SEMANTICS_FILES ::= $(shell find rust-semantics/ -type f -name '*') +SEMANTICS_FILES ::= $(shell find rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')') RUST_KOMPILED ::= .build/rust-kompiled RUST_TIMESTAMP ::= $(RUST_KOMPILED)/timestamp SYNTAX_INPUT_DIR ::= tests/syntax diff --git a/rust-semantics/config.md b/rust-semantics/config.md index 5c6edc5..f072f87 100644 --- a/rust-semantics/config.md +++ b/rust-semantics/config.md @@ -1,17 +1,17 @@ ```k module RUST-CONFIGURATION - imports RUST-INDEXING-CONFIGURATION + imports RUST-PREPROCESSING-CONFIGURATION configuration - + endmodule module RUST-RUNNING-CONFIGURATION - imports private RUST-INDEXING-SYNTAX + imports private RUST-PREPROCESSING-SYNTAX imports RUST-CONFIGURATION configuration diff --git a/rust-semantics/indexing.md b/rust-semantics/indexing.md deleted file mode 100644 index bbe5319..0000000 --- a/rust-semantics/indexing.md +++ /dev/null @@ -1,19 +0,0 @@ -```k - -requires "indexing/crate.md" -requires "indexing/configuration.md" -requires "indexing/helpers.md" -requires "indexing/initialization.md" -requires "indexing/syntax.md" -requires "indexing/trait.md" -requires "indexing/trait-methods.md" - -module RUST-INDEXING - imports private CRATE - imports private INITIALIZATION - imports private TRAIT - imports private TRAIT-METHODS -endmodule - - -``` diff --git a/rust-semantics/indexing/configuration.md b/rust-semantics/indexing/configuration.md deleted file mode 100644 index f6498b1..0000000 --- a/rust-semantics/indexing/configuration.md +++ /dev/null @@ -1,32 +0,0 @@ -```k - -module RUST-INDEXING-CONFIGURATION - imports private RUST-REPRESENTATION - imports private RUST-SHARED-SYNTAX - - syntax Identifier ::= "my_identifier" [token] - - configuration - - - - my_identifier - tuple(.ValueList) - - - - my_identifier - - - my_identifier - .NormalizedFunctionParameterList - ():Type - empty:FunctionBodyRepresentation - - - - -endmodule - - -``` \ No newline at end of file diff --git a/rust-semantics/indexing/helpers.md b/rust-semantics/indexing/helpers.md deleted file mode 100644 index 7ebd3ea..0000000 --- a/rust-semantics/indexing/helpers.md +++ /dev/null @@ -1,35 +0,0 @@ -```k - -module RUST-INDEXING-PRIVATE-HELPERS - imports private RUST-REPRESENTATION - imports RUST-SHARED-SYNTAX - - syntax Identifier ::= getFunctionName(Function) [function, total] - rule getFunctionName(_Q:FunctionQualifiers F:FunctionWithoutQualifiers) - => getFunctionName(F) - rule getFunctionName(F:FunctionWithWhere _B:BlockExpression) - => getFunctionName(F ;) - rule getFunctionName(F:FunctionWithReturnType _W:WhereClause ;) - => getFunctionName(F ;) - rule getFunctionName(F:FunctionWithParams _R:FunctionReturnType ;) - => getFunctionName(F ;) - rule getFunctionName(fn Name:Identifier _P:GenericParams ( ) ;) - => Name - rule getFunctionName(fn Name:Identifier ( ) ;) - => Name - rule getFunctionName(fn Name:Identifier _P:GenericParams ( _Params:FunctionParameters ) ;) - => Name - rule getFunctionName(fn Name:Identifier ( _Params:FunctionParameters ) ;) - => Name - - syntax NormalizedFunctionParameterList ::= reverse(NormalizedFunctionParameterList) [function, total] - // See https://github.com/runtimeverification/k/issues/4587 - // for the "Non exhaustive match detected" warning - | #reverse(NormalizedFunctionParameterList, NormalizedFunctionParameterList) [function, total] - rule reverse(L:NormalizedFunctionParameterList) => #reverse(L, .NormalizedFunctionParameterList) - rule #reverse(.NormalizedFunctionParameterList, R) => R - rule #reverse((P:NormalizedFunctionParameter , L:NormalizedFunctionParameterList), R) - => #reverse(L, (P , R)) -endmodule - -``` diff --git a/rust-semantics/indexing/initialization.md b/rust-semantics/indexing/initialization.md deleted file mode 100644 index 1ced14d..0000000 --- a/rust-semantics/indexing/initialization.md +++ /dev/null @@ -1,119 +0,0 @@ -```k - -module INITIALIZATION - imports private RUST-RUNNING-CONFIGURATION - imports private RUST-INDEXING-PRIVATE-HELPERS - imports private RUST-INDEXING-PRIVATE-SYNTAX - - // rule - // crateInitializer - // ( ... constantNames:(ListItem(Name:Identifier) => .List) _Cts:List - // , constants: _Constants (Name |-> V:Value => .Map) - // ) - // ... - // - // - // - // .Bag => - // - // Name:Identifier - // V:Value - // - // - // ... - // - - rule (.K => addMethod(F, A)) - ~> crateInitializer - ( ... constantNames: .List - , functionNames: (ListItem(Name:Identifier) => .List) _Names:List - , functions: _Functions:Map - ((Name |-> (A:OuterAttributes F:Function):AssociatedItem) => .Map) - ) - rule - crateInitializer - ( ... constantNames : .List - , functionNames : .List - , traitName : Name:Identifier - ) => .K - ... - - - ... - - ... - _Name => Name:Identifier - - - - // rule addMethod(_Q:FunctionQualifiers F:FunctionWithoutQualifiers, A:OuterAttributes) - // => addMethod(F:FunctionWithoutQualifiers, A) - rule addMethod((F:FunctionWithWhere B:BlockExpressionOrSemicolon):FunctionWithoutQualifiers, A:OuterAttributes) - => addMethod1(F, B, A) - - // rule addMethod1(F:FunctionWithReturnType _W:WhereClause, B:BlockExpressionOrSemicolon, A:OuterAttributes) - // => addMethod1(F, B, A) - // rule addMethod1(F:FunctionWithParams -> RT:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) - // => addMethod2(F, RT, B, A) - rule addMethod1(F:FunctionWithParams, B:BlockExpressionOrSemicolon, A:OuterAttributes) - => addMethod2(F, (), B, A) - - // rule addMethod2(fn Name ( ), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) - // => addMethod4(Name, .NormalizedFunctionParameterList, T, B, A) - rule addMethod2(fn Name (_:SelfParam), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) - => addMethod4(Name, (self : $selftype), T, B, A) - // rule addMethod2(fn Name (_:SelfParam , ), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) - // => addMethod4(Name, (self : $selftype), T, B, A) - // rule addMethod2(fn Name (_:SelfParam , P:FunctionParameterList), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) - // => addMethod3(Name, (self : $selftype), P, T, B, A) - // rule addMethod2(fn Name (_:SelfParam , P:FunctionParameterList ,), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) - // => addMethod3(Name, (self : $selftype) , P, T, B, A) - - // rule addMethod3( - // _MethodName:Identifier, - // ReversedNormalizedParams:NormalizedFunctionParameterList - // => (ParamName : ParamType , ReversedNormalizedParams), - // (ParamName:Identifier : ParamType:Type , Params:FunctionParameterList) - // => Params, - // _MethodReturnType:Type, _B:BlockExpressionOrSemicolon, _A:OuterAttributes - // ) - // rule addMethod3( - // MethodName:Identifier, - // ReversedNormalizedParams:NormalizedFunctionParameterList, - // .FunctionParameterList, - // MethodReturnType:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes - // ) - // => addMethod4( - // MethodName, - // reverse(ReversedNormalizedParams), - // MethodReturnType, B, A - // ) - - rule - addMethod4( - Name:Identifier, P:NormalizedFunctionParameterList, - R:Type, B:BlockExpression, - _A:OuterAttributes - ) => .K - ... - - - ... - - ... - - .Bag => - - Name:Identifier - P - R - block(B) - - ... - - - - -endmodule - -``` diff --git a/rust-semantics/indexing/syntax.md b/rust-semantics/indexing/syntax.md deleted file mode 100644 index 5313228..0000000 --- a/rust-semantics/indexing/syntax.md +++ /dev/null @@ -1,46 +0,0 @@ -```k - -module RUST-INDEXING-SYNTAX - imports RUST-SHARED-SYNTAX - - syntax Initializer ::= crateParser(crate: Crate) -endmodule - -module RUST-INDEXING-PRIVATE-SYNTAX - imports LIST - imports MAP - imports RUST-REPRESENTATION - imports RUST-SHARED-SYNTAX - - syntax Initializer ::= traitParser(Trait) - | traitMethodsParser(AssociatedItems, functions: Map, traitName:Identifier) - | crateInitializer - ( constantNames:List, constants: Map - , traitName: Identifier - , functionNames:List, functions: Map - ) - - syntax Initializer ::= addMethod(function: Function, atts:OuterAttributes) - | addMethod1( - FunctionWithWhere, BlockExpressionOrSemicolon, - OuterAttributes - ) - | addMethod2( - FunctionWithParams, Type, - BlockExpressionOrSemicolon, OuterAttributes - ) - | addMethod3( - Identifier, NormalizedFunctionParameterList, - FunctionParameterList, Type, - BlockExpressionOrSemicolon, OuterAttributes - ) - | addMethod4( - Identifier, NormalizedFunctionParameterList, Type, - BlockExpressionOrSemicolon, OuterAttributes - ) - - // TODO: Move to a more generic place - syntax Identifier ::= "self" [token] -endmodule - -``` diff --git a/rust-semantics/preprocessing.md b/rust-semantics/preprocessing.md new file mode 100644 index 0000000..030bf02 --- /dev/null +++ b/rust-semantics/preprocessing.md @@ -0,0 +1,19 @@ +```k + +requires "preprocessing/crate.md" +requires "preprocessing/configuration.md" +requires "preprocessing/helpers.md" +requires "preprocessing/initialization.md" +requires "preprocessing/syntax.md" +requires "preprocessing/trait.md" +requires "preprocessing/trait-methods.md" + +module RUST-PREPROCESSING + imports private CRATE + imports private INITIALIZATION + imports private TRAIT + imports private TRAIT-METHODS +endmodule + + +``` diff --git a/rust-semantics/preprocessing/configuration.md b/rust-semantics/preprocessing/configuration.md new file mode 100644 index 0000000..c2f5162 --- /dev/null +++ b/rust-semantics/preprocessing/configuration.md @@ -0,0 +1,34 @@ +```k + +module RUST-PREPROCESSING-CONFIGURATION + imports private RUST-REPRESENTATION + imports private RUST-SHARED-SYNTAX + + syntax Identifier ::= "my_identifier" [token] + + configuration + + + + my_identifier + tuple(.ValueList) + + + + + my_identifier:TypePath + + + my_identifier + .NormalizedFunctionParameterList + ():Type + empty:FunctionBodyRepresentation + + + + + +endmodule + + +``` \ No newline at end of file diff --git a/rust-semantics/indexing/crate.md b/rust-semantics/preprocessing/crate.md similarity index 86% rename from rust-semantics/indexing/crate.md rename to rust-semantics/preprocessing/crate.md index 2f310e7..7acd05d 100644 --- a/rust-semantics/indexing/crate.md +++ b/rust-semantics/preprocessing/crate.md @@ -3,8 +3,8 @@ module CRATE imports private LIST imports private MAP - imports private RUST-INDEXING-PRIVATE-SYNTAX - imports private RUST-INDEXING-SYNTAX + imports private RUST-PREPROCESSING-PRIVATE-SYNTAX + imports private RUST-PREPROCESSING-SYNTAX imports private RUST-REPRESENTATION imports private RUST-RUNNING-CONFIGURATION @@ -67,11 +67,13 @@ module CRATE , traitName : Name:Identifier , traitFunctions: Functions:Map ) - => crateInitializer - ( ... constantNames: keys_list(Constants), constants: Constants - , traitName: Name - , functionNames:keys_list(Functions), functions: Functions - ) + => constantInitializer + ( ... constantNames: keys_list(Constants), constants: Constants ) + ~> traitInitializer(Name) + ~> traitMethodInitializer + ( ... traitName: Name + , functionNames:keys_list(Functions), functions: Functions + ) endmodule ``` diff --git a/rust-semantics/preprocessing/helpers.md b/rust-semantics/preprocessing/helpers.md new file mode 100644 index 0000000..2da8f06 --- /dev/null +++ b/rust-semantics/preprocessing/helpers.md @@ -0,0 +1,96 @@ +```k + +module RUST-PREPROCESSING-PRIVATE-HELPERS + imports private RUST-PREPROCESSING-PRIVATE-SYNTAX + imports private RUST-REPRESENTATION + imports RUST-SHARED-SYNTAX + + syntax FunctionWithParams ::= getFunctionWithParams(Function) [function, total] + rule getFunctionWithParams(_Q:FunctionQualifiers F:FunctionWithoutQualifiers) + => getFunctionWithParams(F) + rule getFunctionWithParams(F:FunctionWithWhere _B:BlockExpression) + => getFunctionWithParams(F ;) + rule getFunctionWithParams(F:FunctionWithReturnType _W:WhereClause ;) + => getFunctionWithParams(F ;) + rule getFunctionWithParams(F:FunctionWithParams _R:FunctionReturnType ;) + => F + rule getFunctionWithParams(F:FunctionWithParams ;) + => F + + syntax Identifier ::= getFunctionWithParamsName(FunctionWithParams) [function, total] + rule getFunctionWithParamsName(fn Name:Identifier _P:GenericParams ( )) + => Name + rule getFunctionWithParamsName(fn Name:Identifier ( )) + => Name + rule getFunctionWithParamsName(fn Name:Identifier _P:GenericParams ( _Params:FunctionParameters )) + => Name + rule getFunctionWithParamsName(fn Name:Identifier ( _Params:FunctionParameters )) + => Name + + syntax Identifier ::= getFunctionName(Function) [function, total] + rule getFunctionName(F:Function) + => getFunctionWithParamsName(getFunctionWithParams(F)) + + syntax NormalizedFunctionParameterListOrError ::= extractFunctionNormalizedParams(Function) [function, total] + rule extractFunctionNormalizedParams(F) => extractFunctionWithParamsNormalizedParams(getFunctionWithParams(F)) + + syntax NormalizedFunctionParameterListOrError ::= extractFunctionWithParamsNormalizedParams(FunctionWithParams) [function, total] + rule extractFunctionWithParamsNormalizedParams(fn _Name:Identifier _P:GenericParams ( )) + => .NormalizedFunctionParameterList + rule extractFunctionWithParamsNormalizedParams(fn _Name:Identifier ( )) + => .NormalizedFunctionParameterList + rule extractFunctionWithParamsNormalizedParams(fn _Name:Identifier _P:GenericParams ( Params:FunctionParameters )) + => normalizeParams(Params) + rule extractFunctionWithParamsNormalizedParams(fn _Name:Identifier ( Params:FunctionParameters )) + => normalizeParams(Params) + + syntax NormalizedFunctionParameterListOrError ::= concat( + NormalizedFunctionParameterOrError, + NormalizedFunctionParameterListOrError + ) [function, total] + rule concat(P:NormalizedFunctionParameter, L:NormalizedFunctionParameterList) => P , L + rule concat(P:SemanticsError, _:NormalizedFunctionParameterListOrError) => P + rule concat(_:NormalizedFunctionParameter, L:SemanticsError) => L + + syntax NormalizedFunctionParameterListOrError ::= normalizeParams(FunctionParameters) [function, total] + // We should not need an explicit conactenation here, but the LLVM decision tree code crashes. + rule normalizeParams(_:SelfParam) => self : $selftype , .NormalizedFunctionParameterList + // We should not need an explicit conactenation here, but the LLVM decision tree code crashes. + rule normalizeParams(_:SelfParam , ) => self : $selftype , .NormalizedFunctionParameterList + rule normalizeParams(_:SelfParam , F:FunctionParameterList) => concat(self : $selftype, normalizeParams(F)) + rule normalizeParams(_:SelfParam , F:FunctionParameterList , ) => concat(self : $selftype, normalizeParams(F)) + rule normalizeParams(F:FunctionParameterList ,) => normalizeParams(F) + rule normalizeParams(.FunctionParameterList) => .NormalizedFunctionParameterList + rule normalizeParams(P:FunctionParam , F:FunctionParameterList) => concat(normalizeParam(P), normalizeParams(F)) + + syntax NormalizedFunctionParameterOrError ::= NormalizedFunctionParameter | SemanticsError + + syntax NormalizedFunctionParameterOrError ::= normalizeParam(FunctionParam) [function, total] + rule normalizeParam(_:OuterAttributes Name:Identifier : T:Type) => Name : T + rule normalizeParam(P:FunctionParam) + => error("unimplemented normalizedParam case", P:FunctionParam:KItem) + [owise] + + syntax BlockExpressionOrSemicolon ::= getFunctionBlockOrSemicolon(Function) [function, total] + rule getFunctionBlockOrSemicolon(_Q:FunctionQualifiers F:FunctionWithoutQualifiers) + => getFunctionBlockOrSemicolon(F) + rule getFunctionBlockOrSemicolon(_F:FunctionWithWhere B:BlockExpressionOrSemicolon) + => B + + syntax Type ::= getFunctionReturnType(Function) + rule getFunctionReturnType(_Q:FunctionQualifiers F:FunctionWithoutQualifiers) + => getFunctionReturnType(F) + rule getFunctionReturnType(F:FunctionWithWhere _B:BlockExpression) + => getFunctionReturnType(F ;) + rule getFunctionReturnType(F:FunctionWithReturnType _W:WhereClause ;) + => getFunctionReturnType(F ;) + rule getFunctionReturnType(_F:FunctionWithParams -> R:Type ;) + => R + // https://doc.rust-lang.org/stable/reference/items/functions.html + // If the output type is not explicitly stated, it is the unit type. + rule getFunctionReturnType(_F:FunctionWithParams ;) + => ( ):Type + +endmodule + +``` diff --git a/rust-semantics/preprocessing/initialization.md b/rust-semantics/preprocessing/initialization.md new file mode 100644 index 0000000..c455036 --- /dev/null +++ b/rust-semantics/preprocessing/initialization.md @@ -0,0 +1,68 @@ +```k + +module INITIALIZATION + imports private RUST-RUNNING-CONFIGURATION + imports private RUST-PREPROCESSING-PRIVATE-HELPERS + imports private RUST-PREPROCESSING-PRIVATE-SYNTAX + + rule constantInitializer(... constantNames : .List) => .K + + rule (.K => addMethod(TraitName, F, A)) + ~> traitMethodInitializer + ( ... traitName : TraitName:TypePath + , functionNames: (ListItem(Name:Identifier) => .List) _Names:List + , functions: _Functions:Map + ((Name |-> (A:OuterAttributes F:Function):AssociatedItem) => .Map) + ) + rule traitMethodInitializer(... functionNames: .List) => .K + + rule + traitInitializer(Name:TypePath) => .K + ... + + + ... + .Bag + => + Name + .Bag + + + + rule addMethod(Trait:TypePath, F:Function, A:OuterAttributes) + => #addMethod + ( Trait + , getFunctionName(F) + , extractFunctionNormalizedParams(F) + , getFunctionReturnType(F) + , getFunctionBlockOrSemicolon(F) + , A + ) + + rule + #addMethod( + Trait:TypePath, + Name:Identifier, P:NormalizedFunctionParameterList, + R:Type, B:BlockExpression, + _A:OuterAttributes + ) => .K + ... + + + ... + Trait + + .Bag => + + Name:Identifier + P + R + block(B) + + ... + + + +endmodule + +``` diff --git a/rust-semantics/preprocessing/syntax.md b/rust-semantics/preprocessing/syntax.md new file mode 100644 index 0000000..768bd1a --- /dev/null +++ b/rust-semantics/preprocessing/syntax.md @@ -0,0 +1,41 @@ +```k + +module RUST-PREPROCESSING-SYNTAX + imports RUST-SHARED-SYNTAX + + syntax Initializer ::= crateParser(crate: Crate) +endmodule + +module RUST-PREPROCESSING-PRIVATE-SYNTAX + imports LIST + imports MAP + imports RUST-REPRESENTATION + imports RUST-SHARED-SYNTAX + + syntax Initializer ::= traitParser(Trait) + | traitMethodsParser(AssociatedItems, functions: Map, traitName:Identifier) + | constantInitializer + ( constantNames: List, constants: Map ) + | traitInitializer + ( traitName: TypePath + ) + | traitMethodInitializer + ( traitName: TypePath + , functionNames:List, functions: Map + ) + + syntax Initializer ::= addMethod(traitName : TypePath, function: Function, atts:OuterAttributes) + | #addMethod( + TypePath, + Identifier, + NormalizedFunctionParameterListOrError, + Type, + BlockExpressionOrSemicolon, + OuterAttributes + ) + + // TODO: Move to a more generic place + syntax Identifier ::= "self" [token] +endmodule + +``` diff --git a/rust-semantics/indexing/trait-methods.md b/rust-semantics/preprocessing/trait-methods.md similarity index 71% rename from rust-semantics/indexing/trait-methods.md rename to rust-semantics/preprocessing/trait-methods.md index 84653c9..1b2c106 100644 --- a/rust-semantics/indexing/trait-methods.md +++ b/rust-semantics/preprocessing/trait-methods.md @@ -1,8 +1,8 @@ ```k module TRAIT-METHODS - imports private RUST-INDEXING-PRIVATE-HELPERS - imports private RUST-INDEXING-PRIVATE-SYNTAX + imports private RUST-PREPROCESSING-PRIVATE-HELPERS + imports private RUST-PREPROCESSING-PRIVATE-SYNTAX rule traitMethodsParser( (A:OuterAttributes F:Function) AIs:AssociatedItems => AIs, diff --git a/rust-semantics/indexing/trait.md b/rust-semantics/preprocessing/trait.md similarity index 76% rename from rust-semantics/indexing/trait.md rename to rust-semantics/preprocessing/trait.md index fc17017..97c0ce1 100644 --- a/rust-semantics/indexing/trait.md +++ b/rust-semantics/preprocessing/trait.md @@ -1,7 +1,7 @@ ```k module TRAIT - imports private RUST-INDEXING-PRIVATE-SYNTAX + imports private RUST-PREPROCESSING-PRIVATE-SYNTAX rule traitParser(trait Name:Identifier { .InnerAttributes Functions:AssociatedItems }) => traitMethodsParser(Functions, .Map, Name) diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md index 96301e0..6e87048 100644 --- a/rust-semantics/representation.md +++ b/rust-semantics/representation.md @@ -10,12 +10,16 @@ module RUST-REPRESENTATION syntax MInt{32} syntax MInt{64} + syntax SemanticsError ::= error(String, KItem) + syntax FunctionBodyRepresentation ::= block(BlockExpression) | "empty" | storageAccessor(StringLiteral) syntax NormalizedFunctionParameter ::= Identifier ":" Type syntax NormalizedFunctionParameterList ::= List{NormalizedFunctionParameter, ","} + syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError + syntax Value ::= i32(MInt{32}) | u32(MInt{32}) | i64(MInt{64}) diff --git a/rust-semantics/rust.md b/rust-semantics/rust.md index 965b45d..4b12db2 100644 --- a/rust-semantics/rust.md +++ b/rust-semantics/rust.md @@ -1,12 +1,12 @@ ```k requires "config.md" -requires "indexing.md" +requires "preprocessing.md" requires "representation.md" requires "syntax.md" module RUST imports RUST-CONFIGURATION - imports RUST-INDEXING + imports RUST-PREPROCESSING imports RUST-REPRESENTATION imports RUST-SHARED-SYNTAX diff --git a/tests/execution/function-arguments.rs b/tests/execution/function-arguments.rs new file mode 100644 index 0000000..46d79b6 --- /dev/null +++ b/tests/execution/function-arguments.rs @@ -0,0 +1,24 @@ +#![no_std] + +#[allow(unused_imports)] +use multiversx_sc::imports::*; + +#[multiversx_sc::contract] +pub trait Empty { + #[init] + fn init(&self) { + } + + #[upgrade] + fn upgrade(&self) {} + + fn self_with_comma(&self, ) {} + + fn self_and_arg(&self, first: BigUint) {} + + fn self_and_args(&self, first: BigUint, second: BigUint) {} + + fn self_and_args_comma(&self, first: BigUint, second: BigUint, ) {} + + fn reference_arg(&self, first: &BigUint) {} +} diff --git a/tests/execution/function-return-type.rs b/tests/execution/function-return-type.rs new file mode 100644 index 0000000..a970396 --- /dev/null +++ b/tests/execution/function-return-type.rs @@ -0,0 +1,17 @@ +#![no_std] + +#[allow(unused_imports)] +use multiversx_sc::imports::*; + +#[multiversx_sc::contract] +pub trait Empty { + #[init] + fn init(&self) { + } + + #[upgrade] + fn upgrade(&self) {} + + fn with_return_type(&self) -> BigUint {} + +}