diff --git a/Makefile b/Makefile index 6a40648..b2c857a 100644 --- a/Makefile +++ b/Makefile @@ -1,34 +1,47 @@ SEMANTICS_FILES ::= $(shell find rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')') RUST_PREPROCESSING_KOMPILED ::= .build/rust-preprocessing-kompiled RUST_PREPROCESSING_TIMESTAMP ::= $(RUST_PREPROCESSING_KOMPILED)/timestamp +RUST_EXECUTION_KOMPILED ::= .build/rust-execution-kompiled +RUST_EXECUTION_TIMESTAMP ::= $(RUST_EXECUTION_KOMPILED)/timestamp SYNTAX_INPUT_DIR ::= tests/syntax SYNTAX_OUTPUT_DIR ::= .build/syntax-output PREPROCESSING_INPUT_DIR ::= tests/preprocessing PREPROCESSING_OUTPUT_DIR ::= .build/preprocessing-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_OUTPUT_DIR)/%.rs-parsed,$(SYNTAX_INPUTS)) PREPROCESSING_INPUTS ::= $(wildcard $(PREPROCESSING_INPUT_DIR)/*.rs) -PREPROCESSING_OUTPUTS ::= $(patsubst $(PREPROCESSING_INPUT_DIR)/%.rs,$(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore,$(PREPROCESSING_INPUTS)) -PREPROCESSING_STATUSES ::= $(patsubst %.rs.preprocessed.kore,%.rs.status,$(PREPROCESSING_OUTPUTS)) +PREPROCESSING_OUTPUTS ::= $(patsubst $(PREPROCESSING_INPUT_DIR)/%,$(PREPROCESSING_OUTPUT_DIR)/%.preprocessed.kore,$(PREPROCESSING_INPUTS)) +PREPROCESSING_STATUSES ::= $(patsubst %.preprocessed.kore,%.status,$(PREPROCESSING_OUTPUTS)) -.PHONY: clean build test syntax-test preprocessing-test +EXECUTION_INPUTS ::= $(wildcard $(EXECUTION_INPUT_DIR)/*.*.run) +EXECUTION_OUTPUTS ::= $(patsubst $(EXECUTION_INPUT_DIR)/%,$(EXECUTION_OUTPUT_DIR)/%.executed.kore,$(EXECUTION_INPUTS)) +EXECUTION_STATUSES ::= $(patsubst %.executed.kore,%.status,$(EXECUTION_OUTPUTS)) + +.PHONY: clean build test syntax-test preprocessing-test execution-test clean: rm -r .build -build: $(RUST_PREPROCESSING_TIMESTAMP) +build: $(RUST_PREPROCESSING_TIMESTAMP) $(RUST_EXECUTION_TIMESTAMP) -test: syntax-test preprocessing-test +test: syntax-test preprocessing-test execution-test syntax-test: $(SYNTAX_OUTPUTS) preprocessing-test: $(PREPROCESSING_OUTPUTS) +execution-test: $(EXECUTION_OUTPUTS) + $(RUST_PREPROCESSING_TIMESTAMP): $(SEMANTICS_FILES) $$(which kompile) rust-semantics/targets/preprocessing/rust.md -o $(RUST_PREPROCESSING_KOMPILED) +$(RUST_EXECUTION_TIMESTAMP): $(SEMANTICS_FILES) + $$(which kompile) rust-semantics/targets/execution/rust.md -o $(RUST_EXECUTION_KOMPILED) + $(SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(SYNTAX_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP) mkdir -p $(SYNTAX_OUTPUT_DIR) kast --definition $(RUST_PREPROCESSING_KOMPILED) $< --sort Crate > $@.tmp && mv -f $@.tmp $@ @@ -43,3 +56,16 @@ $(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: $(PREPROCESSING_INPUT_DIR)/% cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())" mv -f $@.tmp $@ +# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs +# as a dependency +$(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: $(EXECUTION_INPUT_DIR)/%.run $(RUST_EXECUTION_TIMESTAMP) + mkdir -p $(EXECUTION_OUTPUT_DIR) + krun \ + "$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \ + --definition $(RUST_EXECUTION_KOMPILED) \ + --output kore \ + --output-file $@.tmp \ + -cTEST="$(shell cat $<)" \ + -pTEST=$(CURDIR)/run-test.sh + cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())" + mv -f $@.tmp $@ diff --git a/run-test.sh b/run-test.sh new file mode 100755 index 0000000..e0a3b2d --- /dev/null +++ b/run-test.sh @@ -0,0 +1,8 @@ +#! /bin/bash + +kast \ + --output kore \ + --definition .build/rust-execution-kompiled \ + --module RUST-SYNTAX \ + --sort ExecutionTest \ + $1 diff --git a/rust-semantics/config.md b/rust-semantics/config.md index da8ed71..155771d 100644 --- a/rust-semantics/config.md +++ b/rust-semantics/config.md @@ -1,11 +1,13 @@ ```k module RUST-CONFIGURATION + imports RUST-EXECUTION-CONFIGURATION imports RUST-PREPROCESSING-CONFIGURATION configuration + endmodule diff --git a/rust-semantics/execution.md b/rust-semantics/execution.md new file mode 100644 index 0000000..917daba --- /dev/null +++ b/rust-semantics/execution.md @@ -0,0 +1,14 @@ +```k + +requires "execution/configuration.md" +requires "execution/block.md" +requires "execution/calls.md" +requires "execution/stack.md" + +module RUST-EXECUTION + imports RUST-BLOCK + imports RUST-CALLS + imports RUST-STACK +endmodule + +``` \ No newline at end of file diff --git a/rust-semantics/execution/block.md b/rust-semantics/execution/block.md new file mode 100644 index 0000000..5ef8832 --- /dev/null +++ b/rust-semantics/execution/block.md @@ -0,0 +1,17 @@ +```k + +module RUST-BLOCK + imports RUST-SHARED-SYNTAX + imports RUST-STACK + + // https://doc.rust-lang.org/stable/reference/expressions/block-expr.html + // https://doc.rust-lang.org/stable/reference/names/scopes.html + + rule {.InnerAttributes}:BlockExpression => .K + // Pushin and popping the local state (without cleaing) should help with + // variable shadowing + rule {.InnerAttributes S:Statements}:BlockExpression + => pushLocalState ~> S ~> popLocalState +endmodule + +``` diff --git a/rust-semantics/execution/calls.md b/rust-semantics/execution/calls.md new file mode 100644 index 0000000..a106844 --- /dev/null +++ b/rust-semantics/execution/calls.md @@ -0,0 +1,56 @@ +```k + +module RUST-CALLS + imports BOOL + imports RUST-STACK + imports RUST-HELPERS + imports RUST-REPRESENTATION + imports RUST-RUNNING-CONFIGURATION + + // https://doc.rust-lang.org/stable/reference/expressions/method-call-expr.html + + syntax Instruction ::= "clearLocalState" + | setArgs(NormalizedCallParams, NormalizedFunctionParameterList) + + rule + + normalizedMethodCall( + TraitName:TypePath, + MethodName:Identifier, + Args:NormalizedCallParams + ) => pushLocalState + ~> clearLocalState + ~> setArgs(Args, Params) + ~> FunctionBody + ~> popLocalState + ... + + TraitName + MethodName + Params:NormalizedFunctionParameterList + block(FunctionBody) + + rule + + clearLocalState => .K + ... + + _ => .Map + + rule + + setArgs( + (ValueId:Int , Ids:NormalizedCallParams) => Ids, + ((Name:Identifier : T:Type) , Ps:NormalizedFunctionParameterList) => Ps + ) + ... + + Locals:Map => Locals[Name <- ValueId] + ValueId |-> Value ... + requires notBool Name in_keys(Locals) andBool isSameType(Value, T) + + rule setArgs(.NormalizedCallParams, .NormalizedFunctionParameterList) => .K + +endmodule + +``` diff --git a/rust-semantics/execution/configuration.md b/rust-semantics/execution/configuration.md new file mode 100644 index 0000000..e0242d4 --- /dev/null +++ b/rust-semantics/execution/configuration.md @@ -0,0 +1,17 @@ +```k + +module RUST-EXECUTION-CONFIGURATION + imports INT + imports LIST + imports MAP + + configuration + + .Map // Map from ValueId:Int |-> Value + .Map // Map from Identifier |-> ValueId:Int + .List // list of locals map. + 0 + +endmodule + +``` diff --git a/rust-semantics/execution/stack.md b/rust-semantics/execution/stack.md new file mode 100644 index 0000000..8652a1f --- /dev/null +++ b/rust-semantics/execution/stack.md @@ -0,0 +1,28 @@ +```k + +module RUST-STACK + imports LIST + imports RUST-RUNNING-CONFIGURATION + + syntax Instruction ::= "pushLocalState" + | "popLocalState" + + rule + + pushLocalState => .K + ... + + Locals + .List => ListItem(Locals) ... + + rule + + popLocalState => .K + ... + + _ => Locals + ListItem(Locals) => .List ... + +endmodule + +``` \ No newline at end of file diff --git a/rust-semantics/helpers.md b/rust-semantics/helpers.md new file mode 100644 index 0000000..5abff5f --- /dev/null +++ b/rust-semantics/helpers.md @@ -0,0 +1,19 @@ +```k +module RUST-HELPERS + imports BOOL + imports private RUST-REPRESENTATION + + syntax Int ::= paramsLength(NormalizedFunctionParameterList) [function, total] + rule paramsLength(.NormalizedFunctionParameterList) => 0 + rule paramsLength(_P:NormalizedFunctionParameter , Ps:NormalizedFunctionParameterList) + => 1 +Int paramsLength(Ps) + + syntax Bool ::= isSameType(Value, Type) [function, total] + rule isSameType(_, _) => false [owise] + rule isSameType(_, $selftype) => true + rule isSameType(i64(_), i64) => true + rule isSameType(u64(_), u64) => true + rule isSameType(i32(_), i32) => true + rule isSameType(u32(_), u32) => true +endmodule +``` diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md index 578d193..05cf311 100644 --- a/rust-semantics/representation.md +++ b/rust-semantics/representation.md @@ -3,6 +3,7 @@ module RUST-REPRESENTATION imports INT imports LIST // for filling the second argument of `error`. + imports MAP imports MINT imports RUST-SHARED-SYNTAX @@ -20,6 +21,10 @@ module RUST-REPRESENTATION 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}) @@ -28,6 +33,7 @@ module RUST-REPRESENTATION | 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 @@ -44,4 +50,4 @@ module RUST-REPRESENTATION endmodule -``` \ No newline at end of file +``` diff --git a/rust-semantics/rust-common.md b/rust-semantics/rust-common.md index 6a727cc..41c1abc 100644 --- a/rust-semantics/rust-common.md +++ b/rust-semantics/rust-common.md @@ -1,17 +1,19 @@ ```k requires "config.md" +requires "execution.md" requires "expression.md" +requires "helpers.md" requires "preprocessing.md" requires "representation.md" requires "rust-common-syntax.md" module RUST-COMMON - imports RUST-RUNNING-CONFIGURATION + imports RUST-EXECUTION imports RUST-EXPRESSION + imports RUST-HELPERS imports RUST-PREPROCESSING imports RUST-REPRESENTATION + imports RUST-RUNNING-CONFIGURATION imports RUST-SHARED-SYNTAX endmodule - -``` diff --git a/rust-semantics/targets/execution/configuration.md b/rust-semantics/targets/execution/configuration.md new file mode 100644 index 0000000..27781ab --- /dev/null +++ b/rust-semantics/targets/execution/configuration.md @@ -0,0 +1,17 @@ +```k + +module RUST-RUNNING-CONFIGURATION + imports private RUST-PREPROCESSING-SYNTAX + imports private RUST-EXECUTION-TEST-PARSING-SYNTAX + imports RUST-CONFIGURATION + imports RUST-EXECUTION-TEST-CONFIGURATION + + configuration + + crateParser($PGM:Crate) ~> $TEST:ExecutionTest + + + +endmodule + +``` diff --git a/rust-semantics/targets/execution/rust.md b/rust-semantics/targets/execution/rust.md new file mode 100644 index 0000000..d6a0c33 --- /dev/null +++ b/rust-semantics/targets/execution/rust.md @@ -0,0 +1,18 @@ +```k + +requires "configuration.md" +requires "../../rust-common.md" +requires "../../rust-common-syntax.md" +requires "../../test.md" + +module RUST-SYNTAX + imports RUST-COMMON-SYNTAX + imports RUST-EXECUTION-TEST-PARSING-SYNTAX +endmodule + +module RUST + imports RUST-COMMON + imports RUST-EXECUTION-TEST +endmodule + +``` \ No newline at end of file diff --git a/rust-semantics/targets/preprocessing/configuration.md b/rust-semantics/targets/preprocessing/configuration.md index 345dca8..9238cbf 100644 --- a/rust-semantics/targets/preprocessing/configuration.md +++ b/rust-semantics/targets/preprocessing/configuration.md @@ -1,11 +1,14 @@ ```k + module RUST-RUNNING-CONFIGURATION imports private RUST-PREPROCESSING-SYNTAX imports RUST-CONFIGURATION + configuration crateParser($PGM:Crate) endmodule + ``` diff --git a/rust-semantics/targets/preprocessing/rust.md b/rust-semantics/targets/preprocessing/rust.md index 89e0ad7..ca5122a 100644 --- a/rust-semantics/targets/preprocessing/rust.md +++ b/rust-semantics/targets/preprocessing/rust.md @@ -3,9 +3,11 @@ requires "configuration.md" requires "../../rust-common.md" requires "../../rust-common-syntax.md" + module RUST-SYNTAX imports RUST-COMMON-SYNTAX endmodule + module RUST imports RUST-COMMON endmodule diff --git a/rust-semantics/test.md b/rust-semantics/test.md new file mode 100644 index 0000000..bab5544 --- /dev/null +++ b/rust-semantics/test.md @@ -0,0 +1,10 @@ +```k + +requires "test/configuration.md" +requires "test/execution.md" + +module RUST-TEST + imports RUST-EXECUTION-TEST +endmodule + +``` diff --git a/rust-semantics/test/configuration.md b/rust-semantics/test/configuration.md new file mode 100644 index 0000000..4126e0e --- /dev/null +++ b/rust-semantics/test/configuration.md @@ -0,0 +1,12 @@ +```k + +module RUST-EXECUTION-TEST-CONFIGURATION + imports LIST + + configuration + + .List + +endmodule + +``` \ No newline at end of file diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md new file mode 100644 index 0000000..77e6021 --- /dev/null +++ b/rust-semantics/test/execution.md @@ -0,0 +1,63 @@ +```k + +module RUST-EXECUTION-TEST-PARSING-SYNTAX + imports RUST-SHARED-SYNTAX + + syntax ExecutionTest ::= NeList{ExecutionItem, ";"} + // syntax ExecutionTest ::= ExecutionItem ";" ExecutionItem + syntax ExecutionItem ::= "new" TypePath + | "call" TypePath "." Identifier +endmodule + +module RUST-EXECUTION-TEST + imports LIST + imports RUST-EXECUTION-TEST-PARSING-SYNTAX + imports RUST-HELPERS + imports RUST-REPRESENTATION + imports RUST-RUNNING-CONFIGURATION + + rule E:ExecutionItem ; Es:ExecutionTest => E ~> Es + rule .ExecutionTest => .K + + rule + new P:TypePath => .K ... + .List => ListItem(NVI) ... + P + VALUES:Map => VALUES[NVI <- struct(P, .Map)] + NVI:Int => NVI +Int 1 + + rule + + call P:TypePath . Name:Identifier + => buildTestMethodCall(P, Name, .NormalizedCallParams, paramsLength(Params)) + ... + + P + Name + Params + + syntax TestExecution ::= buildTestMethodCall(TypePath, Identifier, NormalizedCallParams, Int) + + rule + + buildTestMethodCall( + _TraitName:TypePath, + _MethodName:Identifier, + Args:NormalizedCallParams => (ValueId , Args), + ParamCount:Int => ParamCount -Int 1 + ) + ... + + ListItem(ValueId) => .List ... + requires ParamCount >Int 0 + + rule + buildTestMethodCall( + TraitName:TypePath, + MethodName:Identifier, + Args:NormalizedCallParams, + 0 + ) => normalizedMethodCall(TraitName, MethodName, Args) +endmodule + +``` \ No newline at end of file diff --git a/tests/execution/empty-function.1.run b/tests/execution/empty-function.1.run new file mode 100644 index 0000000..c984431 --- /dev/null +++ b/tests/execution/empty-function.1.run @@ -0,0 +1,2 @@ +new Empty; +call Empty.empty diff --git a/tests/execution/empty-function.rs b/tests/execution/empty-function.rs new file mode 100644 index 0000000..b6a2c65 --- /dev/null +++ b/tests/execution/empty-function.rs @@ -0,0 +1,16 @@ +#![no_std] + +#[allow(unused_imports)] +use multiversx_sc::imports::*; + +#[multiversx_sc::contract] +pub trait Empty { + #[init] + fn init(&self) { + } + + #[upgrade] + fn upgrade(&self) {} + + fn empty(&self) {} +}