From 0dab1436286440ee03a1e2b0c8278f294169642e Mon Sep 17 00:00:00 2001 From: Virgil Date: Wed, 14 Aug 2024 00:59:01 +0300 Subject: [PATCH] Index a trivial program --- .gitignore | 1 + Makefile | 35 +++++-- rust-semantics/config.md | 24 +++++ rust-semantics/indexing.md | 19 ++++ rust-semantics/indexing/configuration.md | 32 ++++++ rust-semantics/indexing/crate.md | 77 ++++++++++++++ rust-semantics/indexing/helpers.md | 35 +++++++ rust-semantics/indexing/initialization.md | 119 ++++++++++++++++++++++ rust-semantics/indexing/syntax.md | 46 +++++++++ rust-semantics/indexing/trait-methods.md | 14 +++ rust-semantics/indexing/trait.md | 10 ++ rust-semantics/representation.md | 31 ++++++ rust-semantics/rust.md | 7 ++ tests/execution/empty.rs | 15 +++ 14 files changed, 458 insertions(+), 7 deletions(-) create mode 100644 rust-semantics/config.md create mode 100644 rust-semantics/indexing.md create mode 100644 rust-semantics/indexing/configuration.md create mode 100644 rust-semantics/indexing/crate.md create mode 100644 rust-semantics/indexing/helpers.md create mode 100644 rust-semantics/indexing/initialization.md create mode 100644 rust-semantics/indexing/syntax.md create mode 100644 rust-semantics/indexing/trait-methods.md create mode 100644 rust-semantics/indexing/trait.md create mode 100644 rust-semantics/representation.md create mode 100644 tests/execution/empty.rs diff --git a/.gitignore b/.gitignore index 24e5b0a..84d8b56 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ .build +tmp diff --git a/Makefile b/Makefile index 6d33e2d..b2af1fb 100644 --- a/Makefile +++ b/Makefile @@ -2,25 +2,46 @@ SEMANTICS_FILES ::= $(shell find rust-semantics/ -type f -name '*') RUST_KOMPILED ::= .build/rust-kompiled RUST_TIMESTAMP ::= $(RUST_KOMPILED)/timestamp SYNTAX_INPUT_DIR ::= tests/syntax -SYNTAX_OUTPUTS_DIR ::= .build/syntax-output +SYNTAX_OUTPUT_DIR ::= .build/syntax-output +EXECUTION_INPUT_DIR ::= tests/execution +EXECUTION_OUTPUT_DIR ::= .build/execution-output SYNTAX_INPUTS ::= $(wildcard $(SYNTAX_INPUT_DIR)/*.rs) -SYNTAX_OUTPUTS ::= $(patsubst $(SYNTAX_INPUT_DIR)/%.rs,$(SYNTAX_OUTPUTS_DIR)/%.rs-parsed,$(SYNTAX_INPUTS)) +SYNTAX_OUTPUTS ::= $(patsubst $(SYNTAX_INPUT_DIR)/%.rs,$(SYNTAX_OUTPUT_DIR)/%.rs-parsed,$(SYNTAX_INPUTS)) -.PHONY: clean build test syntax-test +EXECUTION_INPUTS ::= $(wildcard $(EXECUTION_INPUT_DIR)/*.rs) +EXECUTION_OUTPUTS ::= $(patsubst $(EXECUTION_INPUT_DIR)/%.rs,$(EXECUTION_OUTPUT_DIR)/%.rs.executed.kore,$(EXECUTION_INPUTS)) +INDEXING_OUTPUTS ::= $(patsubst %.rs.executed.kore,%.rs.indexed.kore,$(EXECUTION_OUTPUTS)) +EXECUTION_STATUSES ::= $(patsubst %.rs.executed.kore,%.rs.status,$(EXECUTION_OUTPUTS)) + +.PHONY: clean build test syntax-test indexing-test clean: rm -r .build build: $(RUST_TIMESTAMP) -test: syntax-test +test: syntax-test indexing-test syntax-test: $(SYNTAX_OUTPUTS) +indexing-test: $(INDEXING_OUTPUTS) + echo $(INDEXING_OUTPUTS) + $(RUST_TIMESTAMP): $(SEMANTICS_FILES) $$(which kompile) rust-semantics/rust.md -o $(RUST_KOMPILED) -$(SYNTAX_OUTPUTS_DIR)/%.rs-parsed: $(SYNTAX_INPUT_DIR)/%.rs $(RUST_TIMESTAMP) - mkdir -p $(SYNTAX_OUTPUTS_DIR) - kast --definition $(RUST_KOMPILED) $< --sort Crate > $@ || (rm $@ && false) +$(SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(SYNTAX_INPUT_DIR)/%.rs $(RUST_TIMESTAMP) + mkdir -p $(SYNTAX_OUTPUT_DIR) + kast --definition $(RUST_KOMPILED) $< --sort Crate > $@.tmp && mv -f $@.tmp $@ + +$(EXECUTION_OUTPUT_DIR)/%.rs.indexed.kore: $(EXECUTION_INPUT_DIR)/%.rs $(RUST_TIMESTAMP) + mkdir -p $(EXECUTION_OUTPUT_DIR) + krun \ + $< \ + --definition $(RUST_KOMPILED) \ + --output kore \ + --output-file $@.tmp + cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())" + mv -f $@.tmp $@ + diff --git a/rust-semantics/config.md b/rust-semantics/config.md new file mode 100644 index 0000000..5c6edc5 --- /dev/null +++ b/rust-semantics/config.md @@ -0,0 +1,24 @@ +```k + +module RUST-CONFIGURATION + imports RUST-INDEXING-CONFIGURATION + + configuration + + + + +endmodule + +module RUST-RUNNING-CONFIGURATION + imports private RUST-INDEXING-SYNTAX + imports RUST-CONFIGURATION + + configuration + + crateParser($PGM:Crate) + + +endmodule + +``` diff --git a/rust-semantics/indexing.md b/rust-semantics/indexing.md new file mode 100644 index 0000000..bbe5319 --- /dev/null +++ b/rust-semantics/indexing.md @@ -0,0 +1,19 @@ +```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 new file mode 100644 index 0000000..f6498b1 --- /dev/null +++ b/rust-semantics/indexing/configuration.md @@ -0,0 +1,32 @@ +```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/crate.md b/rust-semantics/indexing/crate.md new file mode 100644 index 0000000..2f310e7 --- /dev/null +++ b/rust-semantics/indexing/crate.md @@ -0,0 +1,77 @@ +```k + +module CRATE + imports private LIST + imports private MAP + imports private RUST-INDEXING-PRIVATE-SYNTAX + imports private RUST-INDEXING-SYNTAX + imports private RUST-REPRESENTATION + imports private RUST-RUNNING-CONFIGURATION + + syntax MaybeIdentifier ::= ".Identifier" | Identifier + syntax Initializer ::= crateParser(crate: Crate, constants: Map, traitName: MaybeIdentifier, traitFunctions: Map) + + rule crateParser(C:Crate) => crateParser(... crate : C, constants : .Map, traitName : .Identifier, traitFunctions : .Map) + + rule crateParser + ( ... crate: + (_Atts:InnerAttributes (_A:OuterAttributes _U:UseDeclaration):Item Is:Items):Crate + => (.InnerAttributes Is):Crate + , constants : _Constants:Map + , traitName : _Name:MaybeIdentifier + , traitFunctions: _TraitFunctions:Map + ) + rule + (.K => traitParser(T)) + ~> crateParser + ( ... crate: + (_Atts:InnerAttributes (ItemAtts:OuterAttributes _V:MaybeVisibility T:Trait):Item Is:Items):Crate + => (.InnerAttributes (ItemAtts T):Item Is):Crate + , constants : _Constants:Map + , traitName : .Identifier + , traitFunctions: .Map + ) + rule ( traitMethodsParser(.AssociatedItems, Functions:Map, Name:Identifier) + => .K + ) + ~> crateParser + ( ... crate: + (_Atts:InnerAttributes (_ItemAtts:OuterAttributes _T:Trait):Item Is:Items):Crate + => (.InnerAttributes Is):Crate + , constants : _Constants:Map + , traitName : .Identifier => Name + , traitFunctions: .Map => Functions + ) + + // rule (.K => CI:ConstantItem:KItem) + // ~> crateParser + // ( ... crate: + // (Atts:InnerAttributes (_ItemAtts:OuterAttributes CI:ConstantItem):Item Is:Items):Crate + // => (Atts Is):Crate + // , constants : _Constants:Map + // , traitName : _Name:MaybeIdentifier + // , traitFunctions: _TraitFunctions:Map + // ) + // rule ((const Name:Identifier : _T:Type = V:Value;):ConstantItem:KItem => .K) + // ~> crateParser + // ( ... crate : _C:Crate + // , constants : Constants:Map => Constants[Name:Identifier:KItem <- V:Value:KItem] + // , traitName : _Name:MaybeIdentifier + // , traitFunctions: _TraitFunctions:Map + // ) + + rule + crateParser + ( ... crate: (_Atts:InnerAttributes .Items):Crate + , constants : Constants:Map + , traitName : Name:Identifier + , traitFunctions: Functions:Map + ) + => crateInitializer + ( ... constantNames: keys_list(Constants), constants: Constants + , traitName: Name + , functionNames:keys_list(Functions), functions: Functions + ) +endmodule + +``` diff --git a/rust-semantics/indexing/helpers.md b/rust-semantics/indexing/helpers.md new file mode 100644 index 0000000..7ebd3ea --- /dev/null +++ b/rust-semantics/indexing/helpers.md @@ -0,0 +1,35 @@ +```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 new file mode 100644 index 0000000..1ced14d --- /dev/null +++ b/rust-semantics/indexing/initialization.md @@ -0,0 +1,119 @@ +```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 new file mode 100644 index 0000000..5313228 --- /dev/null +++ b/rust-semantics/indexing/syntax.md @@ -0,0 +1,46 @@ +```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/indexing/trait-methods.md b/rust-semantics/indexing/trait-methods.md new file mode 100644 index 0000000..84653c9 --- /dev/null +++ b/rust-semantics/indexing/trait-methods.md @@ -0,0 +1,14 @@ +```k + +module TRAIT-METHODS + imports private RUST-INDEXING-PRIVATE-HELPERS + imports private RUST-INDEXING-PRIVATE-SYNTAX + + rule traitMethodsParser( + (A:OuterAttributes F:Function) AIs:AssociatedItems => AIs, + Functions => Functions[getFunctionName(F):Identifier:KItem <- (A F):AssociatedItem], + _Name:Identifier + ) +endmodule + +``` diff --git a/rust-semantics/indexing/trait.md b/rust-semantics/indexing/trait.md new file mode 100644 index 0000000..fc17017 --- /dev/null +++ b/rust-semantics/indexing/trait.md @@ -0,0 +1,10 @@ +```k + +module TRAIT + imports private RUST-INDEXING-PRIVATE-SYNTAX + + rule traitParser(trait Name:Identifier { .InnerAttributes Functions:AssociatedItems }) + => traitMethodsParser(Functions, .Map, Name) +endmodule + +``` diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md new file mode 100644 index 0000000..96301e0 --- /dev/null +++ b/rust-semantics/representation.md @@ -0,0 +1,31 @@ +```k + +module RUST-REPRESENTATION + imports INT + imports MINT + imports RUST-SHARED-SYNTAX + + syntax MInt{8} + syntax MInt{16} + syntax MInt{32} + syntax MInt{64} + + syntax FunctionBodyRepresentation ::= block(BlockExpression) + | "empty" + | storageAccessor(StringLiteral) + syntax NormalizedFunctionParameter ::= Identifier ":" Type + syntax NormalizedFunctionParameterList ::= List{NormalizedFunctionParameter, ","} + + syntax Value ::= i32(MInt{32}) + | u32(MInt{32}) + | i64(MInt{64}) + | u64(MInt{64}) + | tuple(ValueList) + syntax ValueList ::= List{Value, ","} + syntax Expression ::= Value + + syntax Type ::= "$selftype" + +endmodule + +``` \ No newline at end of file diff --git a/rust-semantics/rust.md b/rust-semantics/rust.md index e571dac..965b45d 100644 --- a/rust-semantics/rust.md +++ b/rust-semantics/rust.md @@ -1,8 +1,15 @@ ```k +requires "config.md" +requires "indexing.md" +requires "representation.md" requires "syntax.md" module RUST + imports RUST-CONFIGURATION + imports RUST-INDEXING + imports RUST-REPRESENTATION imports RUST-SHARED-SYNTAX + endmodule ``` \ No newline at end of file diff --git a/tests/execution/empty.rs b/tests/execution/empty.rs new file mode 100644 index 0000000..9591f6d --- /dev/null +++ b/tests/execution/empty.rs @@ -0,0 +1,15 @@ +#![no_std] + +#[allow(unused_imports)] +use multiversx_sc::imports::*; + +#[multiversx_sc::contract] +pub trait Empty { + #[init] + fn init(&self) { + } + + #[upgrade] + fn upgrade(&self) {} + +}