From b62f09a1e60256944ea14cd7b2f9873291ba2607 Mon Sep 17 00:00:00 2001 From: ACassimiro Date: Wed, 11 Sep 2024 16:26:27 -0300 Subject: [PATCH] Mx-rust framework and storage implementation (#80) (#81) * Arrange the cells for easier debugging * Create a list of traits to help with mx preprocessing * Static method calls * Integer - value conversions * Ignore generic args when casting structs * Framework for executing Mx+Rust * Framework for testing Mx+Rust * Implement storage functions * Implement storage accessors * Implement BigUint::from * Default storage values * Storage set_if_empty * Storage tests --------- Co-authored-by: Virgil <25692529+virgil-serbanuta@users.noreply.github.com> --- Makefile | 65 ++++++++- mx-rust-semantics/main/configuration.md | 17 +++ mx-rust-semantics/main/expression.md | 9 ++ mx-rust-semantics/main/expression/strings.md | 34 +++++ mx-rust-semantics/main/glue.md | 50 +++++++ mx-rust-semantics/main/modules.md | 11 ++ mx-rust-semantics/main/modules/biguint.md | 48 +++++++ mx-rust-semantics/main/modules/storage.md | 113 ++++++++++++++++ mx-rust-semantics/main/mx-rust-common.md | 17 +++ mx-rust-semantics/main/preprocessing.md | 11 ++ .../main/preprocessing/methods.md | 124 ++++++++++++++++++ .../main/preprocessing/traits.md | 27 ++++ mx-rust-semantics/main/representation.md | 28 ++++ .../targets/blockchain/configuration.md | 21 +++ .../targets/blockchain/mx-rust.md | 21 +++ .../targets/testing/configuration.md | 30 +++++ mx-rust-semantics/targets/testing/mx-rust.md | 31 +++++ mx-rust-semantics/test/configuration.md | 15 +++ mx-rust-semantics/test/execution.md | 54 ++++++++ mx-semantics/targets/testing/configuration.md | 2 +- mx-semantics/test/execution.md | 8 +- parse-mx-rust-test.sh | 8 ++ parse-mx-rust.sh | 8 ++ rust-semantics/config.md | 2 +- rust-semantics/expression/calls.md | 103 +++++++++++---- rust-semantics/expression/casts.md | 1 + rust-semantics/expression/literals.md | 9 +- rust-semantics/preprocessing/configuration.md | 1 + .../preprocessing/initialization.md | 1 + rust-semantics/representation.md | 11 ++ rust-semantics/rust-common-syntax.md | 11 +- .../targets/execution/configuration.md | 4 +- .../targets/preprocessing/configuration.md | 2 +- tests/mx-rust/storage.1.run | 12 ++ tests/mx-rust/storage.2.run | 9 ++ tests/mx-rust/storage.3.run | 20 +++ tests/mx-rust/storage.rs | 33 +++++ tests/mx/storage/get-existing-storage.mx | 2 +- tests/mx/storage/set-existing-storage.mx | 2 +- 39 files changed, 929 insertions(+), 46 deletions(-) create mode 100644 mx-rust-semantics/main/configuration.md create mode 100644 mx-rust-semantics/main/expression.md create mode 100644 mx-rust-semantics/main/expression/strings.md create mode 100644 mx-rust-semantics/main/glue.md create mode 100644 mx-rust-semantics/main/modules.md create mode 100644 mx-rust-semantics/main/modules/biguint.md create mode 100644 mx-rust-semantics/main/modules/storage.md create mode 100644 mx-rust-semantics/main/mx-rust-common.md create mode 100644 mx-rust-semantics/main/preprocessing.md create mode 100644 mx-rust-semantics/main/preprocessing/methods.md create mode 100644 mx-rust-semantics/main/preprocessing/traits.md create mode 100644 mx-rust-semantics/main/representation.md create mode 100644 mx-rust-semantics/targets/blockchain/configuration.md create mode 100644 mx-rust-semantics/targets/blockchain/mx-rust.md create mode 100644 mx-rust-semantics/targets/testing/configuration.md create mode 100644 mx-rust-semantics/targets/testing/mx-rust.md create mode 100644 mx-rust-semantics/test/configuration.md create mode 100644 mx-rust-semantics/test/execution.md create mode 100755 parse-mx-rust-test.sh create mode 100755 parse-mx-rust.sh create mode 100644 tests/mx-rust/storage.1.run create mode 100644 tests/mx-rust/storage.2.run create mode 100644 tests/mx-rust/storage.3.run create mode 100644 tests/mx-rust/storage.rs diff --git a/Makefile b/Makefile index a9cdf29..7478b43 100644 --- a/Makefile +++ b/Makefile @@ -27,14 +27,30 @@ MX_TESTING_OUTPUT_DIR ::= .build/mx/output MX_TESTING_INPUTS ::= $(wildcard $(MX_TESTING_INPUT_DIR)/**/*.mx) MX_TESTING_OUTPUTS ::= $(patsubst $(MX_TESTING_INPUT_DIR)/%,$(MX_TESTING_OUTPUT_DIR)/%.executed.kore,$(MX_TESTING_INPUTS)) -.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test +MX_RUST_SEMANTICS_FILES ::= $(shell find mx-rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')') +MX_RUST_KOMPILED ::= .build/mx-rust-kompiled +MX_RUST_TIMESTAMP ::= $(MX_RUST_KOMPILED)/timestamp + +MX_RUST_TESTING_SEMANTICS_FILES ::= $(shell find mx-rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')') +MX_RUST_TESTING_KOMPILED ::= .build/mx-rust-testing-kompiled +MX_RUST_TESTING_TIMESTAMP ::= $(MX_RUST_TESTING_KOMPILED)/timestamp +MX_RUST_TESTING_INPUT_DIR ::= tests/mx-rust +MX_RUST_TESTING_OUTPUT_DIR ::= .build/mx-rust/output +MX_RUST_TESTING_INPUTS ::= $(wildcard $(MX_RUST_TESTING_INPUT_DIR)/*.run) +MX_RUST_TESTING_OUTPUTS ::= $(patsubst $(MX_RUST_TESTING_INPUT_DIR)/%,$(MX_RUST_TESTING_OUTPUT_DIR)/%.executed.kore,$(MX_RUST_TESTING_INPUTS)) + +.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test mx-rust-test clean: rm -r .build -build: $(RUST_PREPROCESSING_TIMESTAMP) $(RUST_EXECUTION_TIMESTAMP) $(MX_TESTING_TIMESTAMP) +build: $(RUST_PREPROCESSING_TIMESTAMP) \ + $(RUST_EXECUTION_TIMESTAMP) \ + $(MX_TESTING_TIMESTAMP) \ + $(MX_RUST_TIMESTAMP) \ + $(MX_RUST_TESTING_TIMESTAMP) -test: syntax-test preprocessing-test execution-test mx-test +test: build syntax-test preprocessing-test execution-test mx-test mx-rust-test syntax-test: $(SYNTAX_OUTPUTS) @@ -44,6 +60,8 @@ execution-test: $(EXECUTION_OUTPUTS) mx-test: $(MX_TESTING_OUTPUTS) +mx-rust-test: $(MX_RUST_TESTING_OUTPUTS) + $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES) # Workaround for https://github.com/runtimeverification/k/issues/4141 -rm -r $(RUST_PREPROCESSING_KOMPILED) @@ -59,6 +77,22 @@ $(MX_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) -rm -r $(MX_TESTING_KOMPILED) $$(which kompile) mx-semantics/targets/testing/mx.md -o $(MX_TESTING_KOMPILED) --debug +$(MX_RUST_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(MX_RUST_SEMANTICS_FILES) + # Workaround for https://github.com/runtimeverification/k/issues/4141 + -rm -r $(MX_RUST_KOMPILED) + $$(which kompile) mx-rust-semantics/targets/blockchain/mx-rust.md \ + -o $(MX_RUST_KOMPILED) \ + -I . \ + --debug + +$(MX_RUST_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(MX_RUST_SEMANTICS_FILES) + # Workaround for https://github.com/runtimeverification/k/issues/4141 + -rm -r $(MX_RUST_TESTING_KOMPILED) + $$(which kompile) mx-rust-semantics/targets/testing/mx-rust.md \ + -o $(MX_RUST_TESTING_KOMPILED) \ + -I . \ + --debug + $(RUST_SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(RUST_SYNTAX_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP) mkdir -p $(RUST_SYNTAX_OUTPUT_DIR) kast --definition $(RUST_PREPROCESSING_KOMPILED) $< --sort Crate > $@.tmp && mv -f $@.tmp $@ @@ -75,7 +109,11 @@ $(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: $(PREPROCESSING_INPUT_DIR)/% # TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs # as a dependency -$(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: $(EXECUTION_INPUT_DIR)/%.run $(RUST_EXECUTION_TIMESTAMP) +$(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: \ + $(EXECUTION_INPUT_DIR)/%.run \ + $(RUST_EXECUTION_TIMESTAMP) \ + parse-rust.sh \ + parse-test.sh mkdir -p $(EXECUTION_OUTPUT_DIR) krun \ "$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \ @@ -97,3 +135,22 @@ $(MX_TESTING_OUTPUT_DIR)/%.mx.executed.kore: $(MX_TESTING_INPUT_DIR)/%.mx $(MX_T --output-file $@.tmp cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())" mv -f $@.tmp $@ + +# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs +# as a dependency +$(MX_RUST_TESTING_OUTPUT_DIR)/%.run.executed.kore: \ + $(MX_RUST_TESTING_INPUT_DIR)/%.run \ + $(MX_RUST_TESTING_TIMESTAMP) \ + parse-mx-rust.sh \ + parse-mx-rust-test.sh + mkdir -p $(MX_RUST_TESTING_OUTPUT_DIR) + krun \ + "$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \ + --definition $(MX_RUST_TESTING_KOMPILED) \ + --parser $(CURDIR)/parse-mx-rust.sh \ + --output kore \ + --output-file $@.tmp \ + -cTEST='$(shell cat $<)' \ + -pTEST=$(CURDIR)/parse-mx-rust-test.sh + cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())" + mv -f $@.tmp $@ diff --git a/mx-rust-semantics/main/configuration.md b/mx-rust-semantics/main/configuration.md new file mode 100644 index 0000000..b7de223 --- /dev/null +++ b/mx-rust-semantics/main/configuration.md @@ -0,0 +1,17 @@ +```k + +requires "mx-semantics/main/configuration.md" +requires "rust-semantics/config.md" + +module MX-RUST-COMMON-CONFIGURATION + imports MX-COMMON-CONFIGURATION + imports RUST-CONFIGURATION + + configuration + + + + +endmodule + +``` diff --git a/mx-rust-semantics/main/expression.md b/mx-rust-semantics/main/expression.md new file mode 100644 index 0000000..1e6a692 --- /dev/null +++ b/mx-rust-semantics/main/expression.md @@ -0,0 +1,9 @@ +```k + +requires "expression/strings.md" + +module MX-RUST-EXPRESSION + imports private MX-RUST-EXPRESSION-STRINGS +endmodule + +``` \ No newline at end of file diff --git a/mx-rust-semantics/main/expression/strings.md b/mx-rust-semantics/main/expression/strings.md new file mode 100644 index 0000000..5edf1a0 --- /dev/null +++ b/mx-rust-semantics/main/expression/strings.md @@ -0,0 +1,34 @@ +```k + +module MX-RUST-EXPRESSION-STRINGS + imports private BOOL + imports private INT + imports private MX-RUST-REPRESENTATION + imports private RUST-VALUE-SYNTAX + imports private STRING + + rule concatString(ptrValue(_, S1:String), ptrValue(_, S2:String)) + => ptrValue(null, S1 +String S2) + + rule toString(ptrValue(_, i32(Value:MInt{32}))) + => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 32 divInt 4)) + rule toString(ptrValue(_, u32(Value:MInt{32}))) + => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 32 divInt 4)) + rule toString(ptrValue(_, i64(Value:MInt{64}))) + => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 64 divInt 4)) + rule toString(ptrValue(_, u64(Value:MInt{64}))) + => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 64 divInt 4)) + rule toString(ptrValue(_, u128(Value:MInt{128}))) + => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 128 divInt 4)) + rule toString(ptrValue(null, Value:String)) => ptrValue(null, Value) + // TODO: convert all Value entries to string + + syntax String ::= padLeftString(value:String, padding:String, count:Int) [function, total] + rule padLeftString(...value:S, padding:P, count:C) => S + requires C <=Int lengthString(S) orBool lengthString(P) =/=Int 1 + rule padLeftString(S:String => P +String S, P:String, _Count:Int) + [owise] + +endmodule + +``` diff --git a/mx-rust-semantics/main/glue.md b/mx-rust-semantics/main/glue.md new file mode 100644 index 0000000..9b9162d --- /dev/null +++ b/mx-rust-semantics/main/glue.md @@ -0,0 +1,50 @@ +```k + +module MX-RUST-GLUE + imports private COMMON-K-CELL + imports private MX-COMMON-SYNTAX + imports private RUST-EXECUTION-CONFIGURATION + imports private RUST-VALUE-SYNTAX + imports private MX-RUST-REPRESENTATION + + rule + + storeHostValue + (... destination: rustDestination(ValueId, _:MxRustType) + , value: wrappedRust(V:Value) + ) + => .K + ... + + Values:Map => Values[ValueId <- V] + requires ValueId >=Int 0 + + rule + (.K => mxRustEmptyValue(T)) + ~> storeHostValue + (... destination: rustDestination(_, T:MxRustType) + , value: mxWrappedEmpty + ) + rule + (ptrValue(_, V:Value) => .K) + ~> storeHostValue + (... value: mxWrappedEmpty => wrappedRust(V) + ) + + rule + + mxRustLoadPtr(P:Int) => ptrValue(ptr(P), V) + ... + + P |-> V:Value ... + + rule + mxRustNewValue(V:Value) => ptrValue(ptr(NextId), V) ... + NextId:Int => NextId +Int 1 + Values:Map => Values[NextId <- V] + + rule mxIntValue(I:Int) ~> mxValueToRust(T:Type) + => mxRustNewValue(integerToValue(I, T)) +endmodule + +``` diff --git a/mx-rust-semantics/main/modules.md b/mx-rust-semantics/main/modules.md new file mode 100644 index 0000000..c9aa757 --- /dev/null +++ b/mx-rust-semantics/main/modules.md @@ -0,0 +1,11 @@ +```k + +requires "modules/biguint.md" +requires "modules/storage.md" + +module MX-RUST-MODULES + imports private MX-RUST-MODULES-BIGUINT + imports private MX-RUST-MODULES-STORAGE +endmodule + +``` diff --git a/mx-rust-semantics/main/modules/biguint.md b/mx-rust-semantics/main/modules/biguint.md new file mode 100644 index 0000000..1e4e363 --- /dev/null +++ b/mx-rust-semantics/main/modules/biguint.md @@ -0,0 +1,48 @@ +```k + +module MX-RUST-MODULES-BIGUINT + imports private COMMON-K-CELL + imports private MX-COMMON-SYNTAX + imports private MX-RUST-REPRESENTATION + imports private RUST-EXECUTION-CONFIGURATION + imports private RUST-REPRESENTATION + imports private RUST-SHARED-SYNTAX + + rule + + normalizedMethodCall + ( #token("BigUint", "Identifier"):Identifier + , #token("from", "Identifier"):Identifier + , ( ptr(ValueId:Int) + , .NormalizedCallParams + ) + ) + // TODO: Should check that V >= 0 + => mxRustBigIntNew(valueToInteger(V)) + ... + + ValueId |-> V:Value ... + + // -------------------------------------- + + syntax MxRustInstruction ::= mxRustBigIntNew(IntOrError) + | "mxRustCreateBigUint" + + rule mxRustBigIntNew(V:Int) + => MX#bigIntNew(mxIntValue(V)) + ~> mxValueToRust(i32) + ~> mxRustCreateBigUint + + rule ptrValue(ptr(BigUintId:Int), _) ~> mxRustCreateBigUint + => mxRustNewValue + ( struct + ( #token("BigUint", "Identifier"):Identifier + , #token("mx_biguint_id", "Identifier"):Identifier |-> BigUintId + ) + ) + + rule mxRustEmptyValue(BigUint) => mxRustBigIntNew(0) + +endmodule + +``` diff --git a/mx-rust-semantics/main/modules/storage.md b/mx-rust-semantics/main/modules/storage.md new file mode 100644 index 0000000..582f64b --- /dev/null +++ b/mx-rust-semantics/main/modules/storage.md @@ -0,0 +1,113 @@ +```k + +module MX-RUST-MODULES-STORAGE + imports private COMMON-K-CELL + imports private MX-COMMON-SYNTAX + imports private MX-RUST-REPRESENTATION + imports private RUST-EXECUTION-CONFIGURATION + imports private RUST-REPRESENTATION + imports private RUST-SHARED-SYNTAX + + rule + normalizedMethodCall + ( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier + , #token("new", "Identifier"):Identifier + , ( ptr(KeyId:Int) + , ptr(ResultTypeId:Int) + , .NormalizedCallParams + ) + ) + => mxRustNewValue + ( struct + ( Type + , #token("storage_key", "Identifier"):Identifier |-> KeyId + #token("result_type", "Identifier"):Identifier |-> ResultTypeId + ) + ) + + rule + + normalizedMethodCall + ( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier + , #token("set", "Identifier"):Identifier + , ( ptr(SelfId:Int) + , ptr(ValueId:Int) + , .NormalizedCallParams + ) + ) + => MX#storageStore(mxStringValue(StorageKey), wrappedRust(V)) + ... + + + SelfId |-> struct + ( Type + , #token("storage_key", "Identifier"):Identifier |-> StorageKeyId:Int + _:Map + ) + StorageKeyId |-> StorageKey:String + ValueId |-> V:Value + ... + + + rule + + normalizedMethodCall + ( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier + , #token("set_if_empty", "Identifier"):Identifier + , ( ptr(SelfId:Int) + , ptr(ValueId:Int) + , .NormalizedCallParams + ) + ) + => MX#storageLoad(mxStringValue(StorageKey), rustDestination(-1, noType)) + ~> setIfEmpty + ~> MX#storageStore(mxStringValue(StorageKey), wrappedRust(V)) + ... + + + SelfId |-> struct + ( Type + , #token("storage_key", "Identifier"):Identifier |-> StorageKeyId:Int + _:Map + ) + StorageKeyId |-> StorageKey:String + ValueId |-> V:Value + ... + + + rule mxRustEmptyValue(noType) ~> storeHostValue(...) ~> setIfEmpty + => .K + rule storeHostValue(... value: wrappedRust(_)) + ~> setIfEmpty ~> MX#storageStore(_) + => .K + + rule + + normalizedMethodCall + ( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier + , #token("get", "Identifier"):Identifier + , ( ptr(SelfId:Int) + , .NormalizedCallParams + ) + ) + => MX#storageLoad(mxStringValue(StorageKey), rustDestination(NextId, ResultType)) + ~> mxRustLoadPtr(NextId) + ... + + + SelfId |-> struct + ( Type + , #token("storage_key", "Identifier"):Identifier |-> StorageKeyId:Int + #token("result_type", "Identifier"):Identifier |-> ResultTypeId:Int + _:Map + ) + StorageKeyId |-> StorageKey:String + ResultTypeId |-> ResultType:MxRustType + ... + + NextId:Int => NextId +Int 1 + + syntax MxRustInstruction ::= "setIfEmpty" +endmodule + +``` diff --git a/mx-rust-semantics/main/mx-rust-common.md b/mx-rust-semantics/main/mx-rust-common.md new file mode 100644 index 0000000..1758966 --- /dev/null +++ b/mx-rust-semantics/main/mx-rust-common.md @@ -0,0 +1,17 @@ +```k + +requires "expression.md" +requires "glue.md" +requires "modules.md" +requires "preprocessing.md" +requires "representation.md" + +module MX-RUST-COMMON + imports private MX-RUST-EXPRESSION + imports private MX-RUST-GLUE + imports private MX-RUST-MODULES + imports private MX-RUST-PREPROCESSING + imports private MX-RUST-REPRESENTATION +endmodule + +``` diff --git a/mx-rust-semantics/main/preprocessing.md b/mx-rust-semantics/main/preprocessing.md new file mode 100644 index 0000000..812d0c0 --- /dev/null +++ b/mx-rust-semantics/main/preprocessing.md @@ -0,0 +1,11 @@ +```k + +requires "preprocessing/methods.md" +requires "preprocessing/traits.md" + +module MX-RUST-PREPROCESSING + imports private MX-RUST-PREPROCESSING-METHODS + imports private MX-RUST-PREPROCESSING-TRAITS +endmodule + +``` diff --git a/mx-rust-semantics/main/preprocessing/methods.md b/mx-rust-semantics/main/preprocessing/methods.md new file mode 100644 index 0000000..5d4d3f9 --- /dev/null +++ b/mx-rust-semantics/main/preprocessing/methods.md @@ -0,0 +1,124 @@ +```k + +module MX-RUST-PREPROCESSING-METHODS + imports private COMMON-K-CELL + imports private K-EQUAL-SYNTAX + imports private LIST + imports private MX-RUST-REPRESENTATION + imports private RUST-PREPROCESSING-CONFIGURATION + imports private RUST-REPRESENTATION + imports private RUST-SHARED-SYNTAX + imports private STRING + + syntax Identifier ::= "storage_mapper" [token] + + syntax MxRustInstruction ::= mxRustPreprocessMethods(trait: TypePath, methodNames: List) + | mxRustPreprocessMethod(trait: TypePath, methodName: Identifier) + | addStorageMethodBody + ( trait: TypePath + , methodName: Identifier + , storageName:String + , mapperValueType:MxRustTypeOrError + ) + + rule + mxRustPreprocessMethods(T:TypePath) + => mxRustPreprocessMethods(T, MethodNames) + ... + + T + MethodNames:List + + rule mxRustPreprocessMethods(_:TypePath, .List) => .K + rule mxRustPreprocessMethods(T:TypePath, ListItem(MethodName:Identifier) Names:List) + => mxRustPreprocessMethod(T, MethodName) ~> mxRustPreprocessMethods(T, Names) + + rule + + mxRustPreprocessMethod(Trait:TypePath, Method:Identifier) + => addStorageMethodBody + (... trait: Trait, methodName: Method + , storageName: getStorageName(Atts) + , mapperValueType: getMapperValueType(MapperValue) + ) + ... + + Trait + Method + empty + Atts:OuterAttributes + + #token("SingleValueMapper", "Identifier") < MapperValue:GenericArg , .GenericArgList > + + requires getStorageName(Atts) =/=K "" + [priority(50)] + rule mxRustPreprocessMethod(_Trait:TypePath, _Method:Identifier) => .K + [priority(100)] + + rule + + addStorageMethodBody + (... trait: Trait:TypePath, methodName: Method:Identifier + , storageName: StorageName:String + , mapperValueType: MapperValueType:MxRustType) => .K + ... + + Trait + Method + Params:NormalizedFunctionParameterList + + empty => block(buildStorageMethodBody(Params, StorageName, MapperValueType)) + + + syntax String ::= getStorageName(atts:OuterAttributes) [function, total] + rule getStorageName() => "" + rule getStorageName(.NonEmptyOuterAttributes) => "" + rule getStorageName + ( (#[ #token("storage_mapper", "Identifier") :: .SimplePathList + ( Name:String, .CallParamsList ) + ]) + _:NonEmptyOuterAttributes + ) => Name + rule getStorageName + ( (#[ #token("view", "Identifier") :: .SimplePathList + ( _Name:PathExprSegments, .CallParamsList ) + ]) + Atts:NonEmptyOuterAttributes + ) + => getStorageName(Atts) + + syntax BlockExpression ::= buildStorageMethodBody + ( params: NormalizedFunctionParameterList + , storageName: String + , mapperValueType: MxRustType + ) [function, total] + rule buildStorageMethodBody + (... params: (_S:SelfSort : _), Params:NormalizedFunctionParameterList + , storageName: StorageName:String + , mapperValueType: ValueType:MxRustType + ) + => { .InnerAttributes + #token("SingleValueMapper", "Identifier"):Identifier + :: #token("new", "Identifier"):PathIdentSegment + ( concatString(StorageName, buildParamsConcat(Params)) + , ptrValue(null, ValueType) + , .CallParamsList + ) + } + + syntax Expression ::= buildParamsConcat(params: NormalizedFunctionParameterList) [function , total] + rule buildParamsConcat(.NormalizedFunctionParameterList) => "" + rule buildParamsConcat(Param:NormalizedFunctionParameter , L:NormalizedFunctionParameterList) + => concatString(paramToString(Param), buildParamsConcat(L)) + + syntax Expression ::= paramToString(NormalizedFunctionParameter) [function, total] + rule paramToString(I:Identifier : _:Type) => toString(I) + rule paramToString(S:SelfSort : _:Type) => toString(S) + + syntax MxRustTypeOrError ::= getMapperValueType(GenericArg) [function, total] + rule getMapperValueType(Type:GenericArg) => error("unknown Mx-Rust type", Type) + [owise] + rule getMapperValueType(#token("BigUint", "Identifier")) => BigUint +endmodule + +``` diff --git a/mx-rust-semantics/main/preprocessing/traits.md b/mx-rust-semantics/main/preprocessing/traits.md new file mode 100644 index 0000000..e37339e --- /dev/null +++ b/mx-rust-semantics/main/preprocessing/traits.md @@ -0,0 +1,27 @@ +```k + +module MX-RUST-PREPROCESSING-TRAITS + imports private COMMON-K-CELL + imports private LIST + imports private MX-RUST-REPRESENTATION + imports private RUST-PREPROCESSING-CONFIGURATION + imports private RUST-SHARED-SYNTAX + + syntax MxRustInstruction ::= mxRustPreprocessTraits(List) + | mxRustPreprocessTrait(TypePath) + + rule + + mxRustPreprocessTraits => mxRustPreprocessTraits(Traits) + ... + + Traits:List + + rule mxRustPreprocessTraits(.List) => .K + rule mxRustPreprocessTraits(ListItem(Trait:TypePath) Traits:List) + => mxRustPreprocessTrait(Trait) ~> mxRustPreprocessTraits(Traits) + + rule mxRustPreprocessTrait(Trait:TypePath) => mxRustPreprocessMethods(Trait) +endmodule + +``` diff --git a/mx-rust-semantics/main/representation.md b/mx-rust-semantics/main/representation.md new file mode 100644 index 0000000..a17f947 --- /dev/null +++ b/mx-rust-semantics/main/representation.md @@ -0,0 +1,28 @@ +```k + +module MX-RUST-REPRESENTATION + imports RUST-REPRESENTATION + imports RUST-SHARED-SYNTAX + + syntax MxRustInstruction ::= "mxRustPreprocessTraits" + | mxRustPreprocessMethods(TypePath) + | mxRustNewValue(ValueOrError) + | mxRustEmptyValue(MxRustType) + | mxValueToRust(Type) + | mxRustLoadPtr(Int) + + syntax MxRustType ::= "noType" | "BigUint" + syntax MxRustTypeOrError ::= MxRustType | SemanticsError + syntax Value ::= MxRustType + + syntax SemanticsError ::= unknownMxRustType(GenericArg) + + syntax MxWrappedValue ::= wrappedRust(Value) + + syntax Expression ::= concatString(Expression, Expression) [seqstrict] + | toString(Expression) [strict] + + syntax MxValue ::= rustDestination(Int, MxRustType) +endmodule + +``` diff --git a/mx-rust-semantics/targets/blockchain/configuration.md b/mx-rust-semantics/targets/blockchain/configuration.md new file mode 100644 index 0000000..8a1526a --- /dev/null +++ b/mx-rust-semantics/targets/blockchain/configuration.md @@ -0,0 +1,21 @@ +```k + +requires "../../main/configuration.md" + +module COMMON-K-CELL + configuration + .K +endmodule + +module MX-RUST-CONFIGURATION + imports COMMON-K-CELL + imports MX-RUST-COMMON-CONFIGURATION + + configuration + + + + +endmodule + +``` diff --git a/mx-rust-semantics/targets/blockchain/mx-rust.md b/mx-rust-semantics/targets/blockchain/mx-rust.md new file mode 100644 index 0000000..f12e9e3 --- /dev/null +++ b/mx-rust-semantics/targets/blockchain/mx-rust.md @@ -0,0 +1,21 @@ +```k + +requires "configuration.md" +requires "mx-semantics/main/mx-common.md" +requires "mx-semantics/main/syntax.md" +requires "rust-semantics/rust-common.md" +requires "rust-semantics/rust-common-syntax.md" +requires "../../main/mx-rust-common.md" + +module MX-RUST-SYNTAX + imports RUST-COMMON-SYNTAX +endmodule + +module MX-RUST + imports private MX-COMMON + imports private MX-RUST-COMMON + imports private MX-RUST-CONFIGURATION + imports private RUST-COMMON +endmodule + +``` diff --git a/mx-rust-semantics/targets/testing/configuration.md b/mx-rust-semantics/targets/testing/configuration.md new file mode 100644 index 0000000..724e3ec --- /dev/null +++ b/mx-rust-semantics/targets/testing/configuration.md @@ -0,0 +1,30 @@ +```k + +requires "../../main/configuration.md" +requires "../../test/configuration.md" + +module COMMON-K-CELL + imports MX-RUST-REPRESENTATION + imports RUST-PREPROCESSING-SYNTAX + imports RUST-SHARED-SYNTAX + + syntax MxRustTest + + configuration + crateParser($PGM:Crate) ~> mxRustPreprocessTraits ~> ($TEST:MxRustTest):KItem +endmodule + +module MX-RUST-CONFIGURATION + imports COMMON-K-CELL + imports MX-RUST-COMMON-CONFIGURATION + imports MX-RUST-EXECUTION-TEST-CONFIGURATION + + configuration + + + + + +endmodule + +``` diff --git a/mx-rust-semantics/targets/testing/mx-rust.md b/mx-rust-semantics/targets/testing/mx-rust.md new file mode 100644 index 0000000..3acfae8 --- /dev/null +++ b/mx-rust-semantics/targets/testing/mx-rust.md @@ -0,0 +1,31 @@ +```k + +requires "configuration.md" +requires "mx-semantics/main/mx-common.md" +requires "mx-semantics/main/syntax.md" +requires "mx-semantics/test/configuration.md" +requires "mx-semantics/test/execution.md" +requires "rust-semantics/rust-common.md" +requires "rust-semantics/rust-common-syntax.md" +requires "rust-semantics/test/configuration.md" +requires "rust-semantics/test/execution.md" +requires "../../main/mx-rust-common.md" +requires "../../main/representation.md" +requires "../../test/execution.md" + +module MX-RUST-SYNTAX + imports RUST-COMMON-SYNTAX + imports MX-RUST-TESTING-PARSING-SYNTAX +endmodule + +module MX-RUST + imports private MX-COMMON + imports private MX-RUST-TEST + imports private MX-RUST-CONFIGURATION + imports private MX-RUST-COMMON + imports private MX-TEST-EXECUTION + imports private RUST-COMMON + imports private RUST-EXECUTION-TEST +endmodule + +``` diff --git a/mx-rust-semantics/test/configuration.md b/mx-rust-semantics/test/configuration.md new file mode 100644 index 0000000..0701dcb --- /dev/null +++ b/mx-rust-semantics/test/configuration.md @@ -0,0 +1,15 @@ +```k + +module MX-RUST-EXECUTION-TEST-CONFIGURATION + imports MX-TEST-CONFIGURATION + imports RUST-EXECUTION-TEST-CONFIGURATION + + configuration + + + + .Map + +endmodule + +``` diff --git a/mx-rust-semantics/test/execution.md b/mx-rust-semantics/test/execution.md new file mode 100644 index 0000000..267e32f --- /dev/null +++ b/mx-rust-semantics/test/execution.md @@ -0,0 +1,54 @@ +```k + +module MX-RUST-TESTING-PARSING-SYNTAX + imports INT-SYNTAX + imports MX-TEST-EXECUTION-PARSING-SYNTAX + imports RUST-EXECUTION-TEST-PARSING-SYNTAX + imports RUST-SHARED-SYNTAX + imports RUST-VALUE-SYNTAX + imports STRING-SYNTAX + + syntax MxRustTest ::= ExecutionTest + syntax ExecutionItem ::= "set_named" String + | "push_named" String + | "get_bigint_from_struct" + | "check_eq" Int + | TestInstruction + +endmodule + +module MX-RUST-TEST + imports private COMMON-K-CELL + imports private MX-RUST-EXECUTION-TEST-CONFIGURATION + imports private MX-RUST-TESTING-PARSING-SYNTAX + imports private RUST-EXECUTION-CONFIGURATION + + rule + set_named Name:String => .K ... + ListItem(Value) => .List ... + M:Map => M[Name <- Value] + + rule + push_named Name:String => .K ... + .List => ListItem(Value) ... + Name |-> Value ... + + rule + + ptrValue + ( _ + , struct + ( #token("BigUint", "Identifier") + , #token("mx_biguint_id", "Identifier"):Identifier |-> BigUintIdId _:Map + ) + ) + ~> get_bigint_from_struct ; Test:ExecutionTest + => push mxIntValue(MInt2Unsigned(BigUintId)) + ~> get_big_int + ~> Test + ... + + BigUintIdId |-> i32(BigUintId:MInt{32}) ... +endmodule + +``` diff --git a/mx-semantics/targets/testing/configuration.md b/mx-semantics/targets/testing/configuration.md index 3f6e4b5..9e0155c 100644 --- a/mx-semantics/targets/testing/configuration.md +++ b/mx-semantics/targets/testing/configuration.md @@ -17,9 +17,9 @@ module MX-CONFIGURATION configuration - + endmodule diff --git a/mx-semantics/test/execution.md b/mx-semantics/test/execution.md index 2386f63..23a3d5c 100644 --- a/mx-semantics/test/execution.md +++ b/mx-semantics/test/execution.md @@ -18,7 +18,7 @@ module MX-TEST-EXECUTION-PARSING-SYNTAX | setCallee(String) | addAccount(String) | setBalance(account:String, token:String, nonce:Int, value:Int) - | setStorage(account:String, key:String, value:MxValue) + | setStorage(account:String, key:String, value:MxWrappedValue) | setBlockTimestamp(Int) | setMockCode(String, MxValue) @@ -238,7 +238,7 @@ module MX-ACCOUNTS-TEST setStorage (... account: Account:String , key: Key:String - , value: Value:MxValue + , value: Value:MxWrappedValue ) => .K ... @@ -251,7 +251,7 @@ module MX-ACCOUNTS-TEST setStorage (... account: Account:String , key: Key:String - , value: Value:MxValue + , value: Value:MxWrappedValue ) => .K ... @@ -260,7 +260,7 @@ module MX-ACCOUNTS-TEST .Bag => Key - wrappedMx(Value) + Value [priority(100)] diff --git a/parse-mx-rust-test.sh b/parse-mx-rust-test.sh new file mode 100755 index 0000000..abb0296 --- /dev/null +++ b/parse-mx-rust-test.sh @@ -0,0 +1,8 @@ +#! /bin/bash + +kast \ + --output kore \ + --definition .build/mx-rust-testing-kompiled \ + --module MX-RUST-SYNTAX \ + --sort MxRustTest \ + $1 diff --git a/parse-mx-rust.sh b/parse-mx-rust.sh new file mode 100755 index 0000000..c20b2ec --- /dev/null +++ b/parse-mx-rust.sh @@ -0,0 +1,8 @@ +#! /bin/bash + +kast \ + --output kore \ + --definition .build/mx-rust-testing-kompiled \ + --module RUST-COMMON-SYNTAX \ + --sort Crate \ + $1 diff --git a/rust-semantics/config.md b/rust-semantics/config.md index 2f7f00f..155771d 100644 --- a/rust-semantics/config.md +++ b/rust-semantics/config.md @@ -6,8 +6,8 @@ module RUST-CONFIGURATION configuration - + endmodule diff --git a/rust-semantics/expression/calls.md b/rust-semantics/expression/calls.md index 32abd98..3c2d535 100644 --- a/rust-semantics/expression/calls.md +++ b/rust-semantics/expression/calls.md @@ -14,6 +14,16 @@ module RUST-EXPRESSION-CALLS , params: CallParamsList , reversedNormalizedParams: NormalizedCallParams ) + syntax Instruction ::= staticMethodCall + ( traitName: TypePath + , method: Identifier + , params: CallParamsList + , reversedNormalizedParams: NormalizedCallParams + ) + syntax Instruction ::= reverseNormalizeParams + ( params: CallParamsList + , reversedNormalizedParams: NormalizedCallParams + ) syntax NormalizedCallParams ::= reverse(NormalizedCallParams, NormalizedCallParams) [function, total] rule reverse(.NormalizedCallParams, R:NormalizedCallParams) => R @@ -28,35 +38,50 @@ module RUST-EXPRESSION-CALLS rule - methodCall - (... self: ptrValue(ptr(A) #as P, _) - , method: MethodName:Identifier - , params: Args:CallParamsList - ) - => methodCall - (... traitName: TraitName - , method: MethodName - , params: Args - , reversedNormalizedParams: P, .NormalizedCallParams - ) + ( .K + => reverseNormalizeParams + (... params: Args + , reversedNormalizedParams: P, .NormalizedCallParams + ) + ~> TraitName + ) + ~> methodCall + (... self: ptrValue(ptr(A) #as P, _) + , method: _MethodName:Identifier + , params: Args:CallParamsList + ) ... A |-> struct(TraitName:TypePath, _) ... requires isValueWithPtr(Args) - rule methodCall - (... traitName: _TraitName:TypePath - , method: _MethodName:Identifier - , params: (ptrValue(ptr(_) #as P:Ptr, _:Value) , Cps:CallParamsList) => Cps + rule + ( reverseNormalizeParams + (... params: .CallParamsList + , reversedNormalizedParams: Args:NormalizedCallParams + ) + ~> TraitName:TypePath + ~> methodCall + (... self: _ + , method: MethodName:Identifier + , params: _:CallParamsList + ) + ) + => normalizedMethodCall + ( TraitName + , MethodName + , reverse(Args, .NormalizedCallParams) + ) + + rule reverseNormalizeParams + (... params: (ptrValue(ptr(_) #as P:Ptr, _:Value) , Cps:CallParamsList) => Cps , reversedNormalizedParams: Args:NormalizedCallParams => P, Args ) rule - methodCall - (... traitName: _TraitName:TypePath - , method: _MethodName:Identifier - , params: (ptrValue(null, V:Value) , Cps:CallParamsList) => Cps + reverseNormalizeParams + (... params: (ptrValue(null, V:Value) , Cps:CallParamsList) => Cps , reversedNormalizedParams: Args:NormalizedCallParams => ptr(NextId), Args ) @@ -64,13 +89,41 @@ module RUST-EXPRESSION-CALLS NextId:Int => NextId +Int 1 Values:Map => Values[NextId <- V] + + rule TraitName:Identifier :: MethodName:Identifier :: .PathExprSegments ( ) + => staticMethodCall(... trait: TraitName, method: MethodName, params: .CallParamsList) + rule TraitName:Identifier :: MethodName:Identifier :: .PathExprSegments + ( Args:CallParamsList ) + => staticMethodCall(... trait: TraitName, method: MethodName, params: Args) + rule TraitName:Identifier :: MethodName:Identifier :: .PathExprSegments + ( Args:CallParamsList , ) + => staticMethodCall(... trait: TraitName, method: MethodName, params: Args) + rule - methodCall - (... traitName: TraitName:TypePath - , method: MethodName:Identifier - , params: .CallParamsList - , reversedNormalizedParams: Args:NormalizedCallParams - ) + ( .K + => reverseNormalizeParams + (... params: Args + , reversedNormalizedParams: .NormalizedCallParams + ) + ) + ~> staticMethodCall + (... trait: _TraitName:TypePath + , method: _MethodName:Identifier + , params: Args:CallParamsList + ) + requires isValueWithPtr(Args) + + rule + ( reverseNormalizeParams + (... params: .CallParamsList + , reversedNormalizedParams: Args:NormalizedCallParams + ) + ~> staticMethodCall + (... trait: TraitName:TypePath + , method: MethodName:Identifier + , params: _:CallParamsList + ) + ) => normalizedMethodCall ( TraitName , MethodName diff --git a/rust-semantics/expression/casts.md b/rust-semantics/expression/casts.md index c7988eb..9138421 100644 --- a/rust-semantics/expression/casts.md +++ b/rust-semantics/expression/casts.md @@ -39,6 +39,7 @@ module RUST-CASTS rule implicitCast(V:Bool, bool) => V rule implicitCast(struct(T, _) #as V, T) => V + rule implicitCast(struct(T, _) #as V, T < _ >) => V // Rewrites diff --git a/rust-semantics/expression/literals.md b/rust-semantics/expression/literals.md index 437ab2e..c47e0d0 100644 --- a/rust-semantics/expression/literals.md +++ b/rust-semantics/expression/literals.md @@ -18,6 +18,7 @@ module RUST-EXPRESSION-INTEGER-LITERALS rule I:IntegerLiteral => wrapPtrValueOrError(null, parseInteger(I)) rule B:Bool:LiteralExpression => ptrValue(null, B:Bool:Value) + rule S:String => ptrValue(null, S) syntax ValueOrError ::= parseInteger(IntegerLiteral) [function, total] | parseInteger(String) [function, total] @@ -60,7 +61,6 @@ module RUST-EXPRESSION-INTEGER-LITERALS [owise] - syntax ValueOrError ::= integerToValue(Int, Type) [function, total] rule integerToValue(I:Int, i32) => i32(Int2MInt(I)) requires sminMInt(32) <=Int I andBool I <=Int smaxMInt(32) rule integerToValue(I:Int, u32) => u32(Int2MInt(I)) @@ -74,6 +74,13 @@ module RUST-EXPRESSION-INTEGER-LITERALS => error("integerToValue: unimplemented", ListItem(I:Int:KItem) ListItem(T:Type:KItem)) [owise] + rule valueToInteger(V:Value) => error("cannot convert to integer", ListItem(V)) [owise] + rule valueToInteger(i32(V:MInt{32})) => MInt2Signed(V) + rule valueToInteger(u32(V:MInt{32})) => MInt2Unsigned(V) + rule valueToInteger(i64(V:MInt{64})) => MInt2Signed(V) + rule valueToInteger(u64(V:MInt{64})) => MInt2Unsigned(V) + rule valueToInteger(u128(V:MInt{128})) => MInt2Unsigned(V) + syntax Bool ::= endsWith(containing:String, contained:String) [function, total] rule endsWith(Containing:String, Contained:String) => substrString diff --git a/rust-semantics/preprocessing/configuration.md b/rust-semantics/preprocessing/configuration.md index 01d33f6..fc3a6fd 100644 --- a/rust-semantics/preprocessing/configuration.md +++ b/rust-semantics/preprocessing/configuration.md @@ -14,6 +14,7 @@ module RUST-PREPROCESSING-CONFIGURATION tuple(.ValueList) + .List // List of TypePath my_identifier:TypePath diff --git a/rust-semantics/preprocessing/initialization.md b/rust-semantics/preprocessing/initialization.md index 83e0ad1..4828b65 100644 --- a/rust-semantics/preprocessing/initialization.md +++ b/rust-semantics/preprocessing/initialization.md @@ -10,6 +10,7 @@ module INITIALIZATION traitInitializer(Name:TypePath) => .K ... + .List => ListItem(Name) ... ... .Bag diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md index e3f2506..0ff511e 100644 --- a/rust-semantics/representation.md +++ b/rust-semantics/representation.md @@ -24,6 +24,7 @@ module RUST-VALUE-SYNTAX | tuple(ValueList) | struct(TypePath, Map) // Map from field name (Identifier) to value ID (Int) | Bool + | String syntax ValueList ::= List{Value, ","} syntax ValueOrError ::= Value | SemanticsError @@ -66,6 +67,12 @@ module RUST-REPRESENTATION , params: CallParamsList ) [seqstrict(1, 3), result(ValueWithPtr)] + | staticMethodCall + ( trait: TypePath + , method: Identifier + , params: CallParamsList + ) + [strict(3), result(ValueWithPtr)] syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError @@ -85,6 +92,10 @@ module RUST-REPRESENTATION syntax Bool ::= isLocalVariable(ValueName) [function, total] syntax Bool ::= isValueWithPtr(K) [function, total, symbol(isValueWithPtr)] + syntax IntOrError ::= Int | SemanticsError + syntax IntOrError ::= valueToInteger(Value) [function, total] + syntax ValueOrError ::= integerToValue(Int, Type) [function, total] + endmodule ``` diff --git a/rust-semantics/rust-common-syntax.md b/rust-semantics/rust-common-syntax.md index e9de99b..c3747ab 100644 --- a/rust-semantics/rust-common-syntax.md +++ b/rust-semantics/rust-common-syntax.md @@ -324,7 +324,6 @@ https://doc.rust-lang.org/reference/items/extern-crates.html | BreakExpression | UnderscoreExpression - | CallExpression | ErrorPropagationExpression | TypeCastExpression // TODO: Removed because it causes ambiguities. @@ -340,7 +339,11 @@ https://doc.rust-lang.org/reference/items/extern-crates.html > Expression "." Identifier // FieldExpression - // > CallExpression + // https://doc.rust-lang.org/reference/expressions/call-expr.html + // TODO: Not implemented properly to avoid ambiguities + > PathExpression "(" ")" + > PathExpression "(" CallParams ")" + | Expression "[" Expression "]" // > ErrorPropagationExpression @@ -527,9 +530,6 @@ https://doc.rust-lang.org/reference/items/extern-crates.html ```k - // TODO: Not implemented properly to avoid ambiguities - syntax CallExpression ::= PathExpression "(" MaybeCallParams ")" - syntax MaybeCallParams ::= "" | CallParams syntax CallParams ::= CallParamsList | CallParamsList "," syntax CallParamsList ::= NeList{Expression, ","} @@ -582,6 +582,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html syntax MacroInvocation ::= SimplePath "!" DelimTokenTree // TODO: Not implemented properly syntax DelimTokenTree ::= "(" MaybeCallParams ")" + syntax MaybeCallParams ::= "" | CallParams // TODO: Not implemented properly syntax MacroInvocationSemi ::= MacroInvocation ";" diff --git a/rust-semantics/targets/execution/configuration.md b/rust-semantics/targets/execution/configuration.md index c035ed0..bb59e86 100644 --- a/rust-semantics/targets/execution/configuration.md +++ b/rust-semantics/targets/execution/configuration.md @@ -15,9 +15,9 @@ module RUST-RUNNING-CONFIGURATION configuration - - + + endmodule diff --git a/rust-semantics/targets/preprocessing/configuration.md b/rust-semantics/targets/preprocessing/configuration.md index d122260..014bdc4 100644 --- a/rust-semantics/targets/preprocessing/configuration.md +++ b/rust-semantics/targets/preprocessing/configuration.md @@ -14,10 +14,10 @@ module RUST-RUNNING-CONFIGURATION configuration - + endmodule diff --git a/tests/mx-rust/storage.1.run b/tests/mx-rust/storage.1.run new file mode 100644 index 0000000..911768f --- /dev/null +++ b/tests/mx-rust/storage.1.run @@ -0,0 +1,12 @@ + +addAccount("Owner"); +setCallee("Owner"); +new Storage; +set_named "self"; +push_named "self"; +push 10u64; +call Storage.set_no_arg; +push_named "self"; +call Storage.get_no_arg; +get_bigint_from_struct; +check_eq mxIntValue(10) diff --git a/tests/mx-rust/storage.2.run b/tests/mx-rust/storage.2.run new file mode 100644 index 0000000..bdefa78 --- /dev/null +++ b/tests/mx-rust/storage.2.run @@ -0,0 +1,9 @@ + +addAccount("Owner"); +setCallee("Owner"); +new Storage; +set_named "self"; +push_named "self"; +call Storage.get_no_arg; +get_bigint_from_struct; +check_eq mxIntValue(0) diff --git a/tests/mx-rust/storage.3.run b/tests/mx-rust/storage.3.run new file mode 100644 index 0000000..7881110 --- /dev/null +++ b/tests/mx-rust/storage.3.run @@ -0,0 +1,20 @@ +addAccount("Owner"); +setCallee("Owner"); +new Storage; +set_named "self"; + +push_named "self"; +push 10u64; +call Storage.set_no_arg_if_empty; +push_named "self"; +call Storage.get_no_arg; +get_bigint_from_struct; +check_eq mxIntValue(10); + +push_named "self"; +push 20u64; +call Storage.set_no_arg_if_empty; +push_named "self"; +call Storage.get_no_arg; +get_bigint_from_struct; +check_eq mxIntValue(10) diff --git a/tests/mx-rust/storage.rs b/tests/mx-rust/storage.rs new file mode 100644 index 0000000..0b16596 --- /dev/null +++ b/tests/mx-rust/storage.rs @@ -0,0 +1,33 @@ +#![no_std] + +#[allow(unused_imports)] +use multiversx_sc::imports::*; + +#[multiversx_sc::contract] +pub trait Storage { + #[view(noArg)] + #[storage_mapper("no_arg")] + fn no_arg_storage(&self) -> SingleValueMapper; + + #[view(getName)] + #[storage_mapper("name")] + fn one_arg_storage(&self, key: u64) -> SingleValueMapper; + + #[init] + fn init(&self) {} + + #[upgrade] + fn upgrade(&self) {} + + fn set_no_arg(&self, value: u64) { + self.no_arg_storage().set(BigUint::from(value)) + } + + fn get_no_arg(&self) -> BigUint { + self.no_arg_storage().get() + } + + fn set_no_arg_if_empty(&self, value: u64) { + self.no_arg_storage().set_if_empty(BigUint::from(value)) + } +} diff --git a/tests/mx/storage/get-existing-storage.mx b/tests/mx/storage/get-existing-storage.mx index 0ebcd78..23a3457 100644 --- a/tests/mx/storage/get-existing-storage.mx +++ b/tests/mx/storage/get-existing-storage.mx @@ -1,6 +1,6 @@ addAccount("Owner"); setCallee("Owner"); -setStorage("Owner", "MyKey", mxStringValue("Hello")); +setStorage("Owner", "MyKey", wrappedMx(mxStringValue("Hello"))); push mxIntValue(12); push mxStringValue("MyKey"); diff --git a/tests/mx/storage/set-existing-storage.mx b/tests/mx/storage/set-existing-storage.mx index 094fc9b..58be307 100644 --- a/tests/mx/storage/set-existing-storage.mx +++ b/tests/mx/storage/set-existing-storage.mx @@ -1,6 +1,6 @@ addAccount("Owner"); setCallee("Owner"); -setStorage("Owner", "MyKey", mxStringValue("Hello")); +setStorage("Owner", "MyKey", wrappedMx(mxStringValue("Hello"))); push wrappedMx(mxStringValue("World")); push mxStringValue("MyKey");