Bytes hooks

Makefile

@@ -64,7 +64,7 @@ DEMOS_TESTING_OUTPUT_DIR ::= .build/demos/output
 DEMOS_TESTING_INPUTS ::= $(wildcard $(DEMOS_TESTING_INPUT_DIR)/*.run)
 DEMOS_TESTING_OUTPUTS ::= $(patsubst $(DEMOS_TESTING_INPUT_DIR)/%,$(DEMOS_TESTING_OUTPUT_DIR)/%.executed.kore,$(DEMOS_TESTING_INPUTS))
 
-UKM_SEMANTICS_FILES ::= $(shell find mx-rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
+UKM_SEMANTICS_FILES ::= $(shell find ukm-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
 
 UKM_EXECUTION_KOMPILED ::= .build/ukm-execution-kompiled
 UKM_EXECUTION_TIMESTAMP ::= $(UKM_EXECUTION_KOMPILED)/timestamp
@@ -75,7 +75,14 @@ UKM_PREPROCESSING_TIMESTAMP ::= $(UKM_PREPROCESSING_KOMPILED)/timestamp
 UKM_TESTING_KOMPILED ::= .build/ukm-testing-kompiled
 UKM_TESTING_TIMESTAMP ::= $(UKM_TESTING_KOMPILED)/timestamp
 
-.PHONY: clean build build-legacy test test-legacy syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test
+UKM_CONTRACTS_TESTING_INPUT_DIR ::= tests/ukm-contracts
+
+UKM_NO_CONTRACT_TESTING_INPUT_DIR ::= tests/ukm-no-contract
+UKM_NO_CONTRACT_TESTING_OUTPUT_DIR ::= .build/ukm-no-contract/output
+UKM_NO_CONTRACT_TESTING_INPUTS ::= $(wildcard $(UKM_NO_CONTRACT_TESTING_INPUT_DIR)/*.run)
+UKM_NO_CONTRACT_TESTING_OUTPUTS ::= $(patsubst $(UKM_NO_CONTRACT_TESTING_INPUT_DIR)/%,$(UKM_NO_CONTRACT_TESTING_OUTPUT_DIR)/%.executed.kore,$(UKM_NO_CONTRACT_TESTING_INPUTS))
+
+.PHONY: clean build build-legacy test test-legacy syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test ukm-no-contracts-test
 
 all: build test
 
@@ -96,7 +103,7 @@ build-legacy: \
 		$(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP)
 
 
-test: build syntax-test preprocessing-test execution-test crates-test
+test: build syntax-test preprocessing-test execution-test crates-test ukm-no-contracts-test
 
 test-legacy: mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test
 
@@ -118,6 +125,8 @@ mx-rust-two-contracts-test: $(MX_RUST_TWO_CONTRACTS_TESTING_OUTPUTS)
 
 demos-test: $(DEMOS_TESTING_OUTPUTS)
 
+ukm-no-contracts-test: $(UKM_NO_CONTRACT_TESTING_OUTPUTS)
+
 $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(RUST_PREPROCESSING_KOMPILED)
@@ -373,3 +382,45 @@ $(CRATES_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 		-pTEST=$(CURDIR)/parsers/test-rust.sh
 	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f $@.tmp $@
+
+
+# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs
+# as a dependency
+$(UKM_NO_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
+			$(UKM_NO_CONTRACT_TESTING_INPUT_DIR)/%.run \
+			$(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs \
+			$(UKM_CONTRACTS_TESTING_INPUT_DIR)/ukm.rs \
+			$(UKM_TESTING_TIMESTAMP) \
+			$(wildcard parsers/inc-*.sh) \
+			parsers/crates-ukm-testing-execution.sh \
+			parsers/test-ukm-testing-execution.sh
+	mkdir -p $(UKM_NO_CONTRACT_TESTING_OUTPUT_DIR)
+
+	echo "<(<" > [email protected]
+	echo "::bytes_hooks" >> [email protected]
+	echo "<|>" >> [email protected]
+	cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs >> [email protected]
+	echo ">)>" >> [email protected]
+
+	# echo "<(<" > [email protected]
+	# echo "::ukm" >> [email protected]
+	# echo "<|>" >> [email protected]
+	# cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/ukm.rs >> [email protected]
+	# echo ">)>" >> [email protected]
+
+	echo "<(<" >> [email protected]
+	echo "$<" | sed 's%^.*/%%' | sed 's/\..*//' | sed 's/^/::/' >> [email protected]
+	echo "<|>" >> [email protected]
+	cat "$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" >> [email protected]
+	echo ">)>" >> [email protected]
+
+	krun \
+		[email protected] \
+		--parser $(CURDIR)/parsers/crates-ukm-testing-execution.sh \
+		--definition $(UKM_TESTING_KOMPILED) \
+		--output kore \
+		--output-file [email protected] \
+		-cTEST='$(shell cat $<)' \
+		-pTEST=$(CURDIR)/parsers/test-ukm-testing-execution.sh
+	cat [email protected] | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
+	mv -f [email protected] $@

parsers/crates-ukm-testing-execution.sh

@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source ${BASH_SOURCE%/*}/inc-crates.sh
+
+parse_crates .build/ukm-testing-kompiled $1

parsers/test-ukm-testing-execution.sh

@@ -0,0 +1,8 @@
+#! /bin/bash
+
+kast \
+    --output kore \
+    --definition .build/ukm-testing-kompiled \
+    --module UKM-TARGET-SYNTAX \
+    --sort ExecutionTest \
+    $1

rust-semantics/expression/expression-list.md

@@ -6,8 +6,9 @@ module RUST-EXPRESSION-EXPRESSION-LIST
     imports private RUST-VALUE-SYNTAX
 
     rule evaluate(L:ExpressionList) => evaluate(expressionListToValueList(L))
+        requires isValueWithPtr(L)
 
-    rule isValueWithPtr(.ExpressionList) => true
+      rule isValueWithPtr(.ExpressionList) => true
     rule isValueWithPtr(E:Expression , T:ExpressionList)
         => isValueWithPtr(E) andBool isValueWithPtr(T)
 

rust-semantics/expression/tuple.md

@@ -12,8 +12,6 @@ module RUST-EXPRESSION-TUPLE
     rule (E:Expression , T:TupleElementsNoEndComma,):TupleExpression
         => tupleExpression(E , T)
 
-    syntax Instruction ::= tupleExpression(TupleElementsNoEndComma)
-
     rule (.K => evaluate(tupleElementsToExpressionList(Es)))
         ~> tupleExpression(Es:TupleElementsNoEndComma)
     rule (evaluate(L:ValueList) ~> tupleExpression(_:TupleElementsNoEndComma))

rust-semantics/helpers.md

@@ -20,8 +20,27 @@ module RUST-HELPERS
     rule isSameType(u16(_), u16) => true
     rule isSameType(i8(_), i8) => true
     rule isSameType(u8(_), u8) => true
+    rule isSameType(_:String, str) => true
     rule isSameType(struct(T, _), T:TypePath) => true
     rule isSameType(struct(T, _), T:Identifier _:GenericArgs ) => true
 
+    syntax Bool ::= isUnsignedInt(Type)  [function, total]
+    rule isUnsignedInt(_) => false [owise]
+    rule isUnsignedInt(u8) => true
+    rule isUnsignedInt(u16) => true
+    rule isUnsignedInt(u32) => true
+    rule isUnsignedInt(u64) => true
+    rule isUnsignedInt(u128) => true
+    rule isUnsignedInt(&T => T)
+
+    syntax Bool ::= isSignedInt(Type)  [function, total]
+    rule isSignedInt(_) => false [owise]
+    rule isSignedInt(u8) => true
+    rule isSignedInt(u16) => true
+    rule isSignedInt(u32) => true
+    rule isSignedInt(u64) => true
+    rule isSignedInt(u128) => true
+    rule isSignedInt(&T => T)
+
 endmodule
 ```

rust-semantics/preprocessing.md.orig

@@ -0,0 +1,34 @@
+```k
+
+requires "preprocessing/constants.md"
+requires "preprocessing/crate.md"
+requires "preprocessing/configuration.md"
+<<<<<<< HEAD
+requires "preprocessing/extern-block.md"
+=======
+>>>>>>> 2f2c6f5 (Run global functions)
+requires "preprocessing/functions.md"
+requires "preprocessing/helpers.md"
+requires "preprocessing/initialization.md"
+requires "preprocessing/module.md"
+requires "preprocessing/syntax.md"
+requires "preprocessing/tools.md"
+requires "preprocessing/trait.md"
+requires "preprocessing/trait-methods.md"
+
+module RUST-PREPROCESSING
+    imports private CRATE
+    imports private INITIALIZATION
+    imports private RUST-CONSTANTS
+    imports private RUST-MODULE
+<<<<<<< HEAD
+    imports private RUST-PREPROCESSING-EXTERN-BLOCK
+=======
+>>>>>>> 2f2c6f5 (Run global functions)
+    imports private RUST-PREPROCESSING-FUNCTIONS
+    imports private RUST-PREPROCESSING-TOOLS
+    imports private TRAIT
+    imports private TRAIT-METHODS
+endmodule
+
+```

rust-semantics/preprocessing/crate.md.orig

@@ -0,0 +1,59 @@
+```k
+
+module CRATE
+    imports private COMMON-K-CELL
+    imports private LIST
+    imports private MAP
+    imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
+    imports private RUST-PREPROCESSING-SYNTAX
+    imports private RUST-REPRESENTATION
+
+    rule cratesParser(.WrappedCrateList) => .K
+    rule cratesParser(<(< Path:TypePath <|> Crate:Crate >)> Crates:WrappedCrateList)
+        => crateParser(Crate, Path) ~> cratesParser(Crates)
+
+    rule crateParser
+        ( (_Atts:InnerAttributes (_A:OuterAttributes _U:UseDeclaration):Item Is:Items):Crate
+          => (.InnerAttributes Is):Crate
+        , _:TypePath
+        )
+    rule (.K => moduleParser(M, CratePath))
+        ~> crateParser
+          ( (_Atts:InnerAttributes (_ItemAtts:OuterAttributes _V:MaybeVisibility M:Module):Item Is:Items):Crate
+            => (.InnerAttributes Is):Crate
+          , CratePath:TypePath
+          )
+    rule
+        (.K => traitParser(T, CratePath, ItemAtts))
+        ~> crateParser
+          ( (_Atts:InnerAttributes (ItemAtts:OuterAttributes _V:MaybeVisibility T:Trait):Item Is:Items):Crate
+            => (.InnerAttributes Is):Crate
+          , CratePath:TypePath
+          )
+    rule (.K => constantParser(CI:ConstantItem, CratePath))
+        ~> crateParser
+          ( (Atts:InnerAttributes (_ItemAtts:OuterAttributes _:MaybeVisibility CI:ConstantItem):Item Is:Items):Crate
+            => (Atts Is):Crate
+          , CratePath:TypePath
+          )
+    rule (.K => functionParser(Fn, CratePath, ItemAtts))
+        ~> crateParser
+          ( (Atts:InnerAttributes (ItemAtts:OuterAttributes _:MaybeVisibility Fn:Function):Item Is:Items):Crate
+            => (Atts Is):Crate
+          , CratePath:TypePath
+          )
+<<<<<<< HEAD
+    rule (.K => externBlockParser(Block, CratePath))
+        ~> crateParser
+          ( (Atts:InnerAttributes (_ItemAtts:OuterAttributes _:MaybeVisibility Block:ExternBlock):Item Is:Items):Crate
+            => (Atts Is):Crate
+          , CratePath:TypePath
+          )
+=======
+>>>>>>> 2f2c6f5 (Run global functions)
+
+    rule crateParser( (_Atts:InnerAttributes .Items):Crate, _Path:TypePath)
+        => .K //resolveCrateNames(Path)
+endmodule
+
+```

rust-semantics/preprocessing/syntax.md.orig

@@ -0,0 +1,54 @@
+```k
+
+module RUST-PREPROCESSING-SYNTAX
+    imports RUST-CRATE-LIST-SYNTAX
+    imports RUST-SHARED-SYNTAX
+
+    syntax Initializer  ::= cratesParser(crates: WrappedCrateList)
+                          | crateParser(crate: Crate, crateModule: TypePath)
+endmodule
+
+module RUST-PREPROCESSING-PRIVATE-SYNTAX
+    imports LIST
+    imports MAP
+    imports RUST-REPRESENTATION
+    imports RUST-SHARED-SYNTAX
+
+    syntax Initializer  ::= traitParser(Trait, MaybeTypePath, OuterAttributes)
+                          | traitMethodsParser(AssociatedItems, traitName:TypePath)
+                          | traitInitializer
+                                ( traitName: TypePath
+                                , atts: OuterAttributes
+                                )
+    syntax Initializer  ::= moduleParser(Module, TypePath)
+                          | moduleItemsParser(Items, TypePath)
+                          | constantParser(ConstantItem, TypePath)  [strict(1)]
+                          | functionParser(Function, TypePath, OuterAttributes)
+<<<<<<< HEAD
+                          | externBlockParser(ExternBlock, TypePath)
+=======
+>>>>>>> 2f2c6f5 (Run global functions)
+                          | resolveCrateNames(TypePath)
+
+    syntax Initializer  ::= addMethod(traitName : TypePath, function: Function, atts:OuterAttributes)
+                          | #addMethod(
+                                TypePath,
+                                Identifier,
+                                NormalizedFunctionParameterListOrError,
+                                Type,
+                                BlockExpressionOrSemicolon,
+                                OuterAttributes
+                            )
+                          | addFunction(parentName : TypePath, function: Function, atts:OuterAttributes)
+                          | #addFunction(
+                                TypePath,
+                                Identifier,
+                                NormalizedFunctionParameterListOrError,
+                                Type,
+                                BlockExpressionOrSemicolon,
+                                OuterAttributes
+                            )
+
+endmodule
+
+```

rust-semantics/representation.md

@@ -89,6 +89,7 @@ module RUST-REPRESENTATION
                               , reversedNormalizedParams: PtrList
                               )
                           | "clearValue"
+                          | tupleExpression(TupleElementsNoEndComma)
 
     syntax PtrList ::= reverse(PtrList, PtrList) [function, total]
 

rust-semantics/test/execution.md

@@ -10,6 +10,7 @@ module RUST-EXECUTION-TEST-PARSING-SYNTAX
                             | "call" TypePath "." Identifier
                             | "call" PathInExpression
                             | "return_value"
+                            | "return_value_to_arg"
                             | "check_eq" Expression  [strict]
                             | "push" Expression [strict]
 endmodule
@@ -79,6 +80,8 @@ module RUST-EXECUTION-TEST
         <k> (V:PtrValue ~> return_value) => .K ... </k>
         <test-stack> .List => ListItem(V) ... </test-stack>
 
+    rule (V:PtrValue ~> return_value_to_arg) => push V
+
     rule
         <k> check_eq ptrValue(_, V:Value) => .K ... </k>
         <test-stack> ListItem(ptrValue(_, V)) => .List ... </test-stack>

tests/execution/top_level_fn.1.run.orig

@@ -0,0 +1,9 @@
+new :: top_level_fn :: TopLevelFn;
+push 125_u64;
+call :: top_level_fn :: TopLevelFn.call_top_level;
+return_value;
+<<<<<<< HEAD
+check_eq 128_u64
+=======
+check_eq 128_u64
+>>>>>>> 2f2c6f5 (Run global functions)

tests/execution/top_level_fn.rs.orig

@@ -0,0 +1,41 @@
+#![no_std]
+
+#[allow(unused_imports)]
+use multiversx_sc::imports::*;
+
+#[multiversx_sc::contract]
+pub trait TopLevelFn {
+    #[init]
+    fn init(&self) {
+    }
+
+    #[upgrade]
+    fn upgrade(&self) {}
+<<<<<<< HEAD
+
+    fn call_top_level(&self, v: u64) -> u64 { 
+      ::top_level_fn::top_level(v)
+    }
+
+    fn call_top_level_no_arg(&self) -> u64 { 
+      ::top_level_fn::top_level_no_arg()
+    }
+=======
+
+    fn call_top_level(&self, v: u64) -> u64 { 
+      ::top_level_fn::top_level(v)
+    }
+>>>>>>> 2f2c6f5 (Run global functions)
+}
+
+fn top_level(v: u64) -> u64 {
+  v + 3_u64
+<<<<<<< HEAD
+}
+
+fn top_level_no_arg() -> u64 {
+  3_u64
+}
+=======
+}
+>>>>>>> 2f2c6f5 (Run global functions)

tests/ukm-contracts/bytes_hooks.rs

@@ -0,0 +1,18 @@
+extern "C" {
+  fn empty() -> u64;
+  fn length(bytes_id: u64) -> u32;
+
+  fn append_u128(bytes_id: u64, value: u128) -> u64;
+  fn append_u64(bytes_id: u64, value: u64) -> u64;
+  fn append_u32(bytes_id: u64, value: u32) -> u64;
+  fn append_u16(bytes_id: u64, value: u16) -> u64;
+  fn append_u7(bytes_id: u64, value: u8) -> u64;
+  fn append_str(bytes_id: u64, value: &str) -> u64;
+
+  fn decode_u128(bytes_id: u64) -> (u64, u128);
+  fn decode_u64(bytes_id: u64) -> (u64, u64);
+  fn decode_u32(bytes_id: u64) -> (u64, u32);
+  fn decode_u16(bytes_id: u64) -> (u64, u16);
+  fn decode_u8(bytes_id: u64) -> (u64, u8);
+  fn decode_str(bytes_id: u64) -> (u64, str);
+}