Use multiple crates

Makefile

@@ -19,6 +19,11 @@ PREPROCESSING_OUTPUTS ::= $(patsubst $(PREPROCESSING_INPUT_DIR)/%,$(PREPROCESSIN
 EXECUTION_INPUTS ::= $(wildcard $(EXECUTION_INPUT_DIR)/*.*.run)
 EXECUTION_OUTPUTS ::= $(patsubst $(EXECUTION_INPUT_DIR)/%,$(EXECUTION_OUTPUT_DIR)/%.executed.kore,$(EXECUTION_INPUTS))
 
+CRATES_TESTING_INPUT_DIR ::= tests/crates
+CRATES_TESTING_OUTPUT_DIR ::= .build/crates/output
+CRATES_TESTING_INPUTS ::= $(wildcard $(CRATES_TESTING_INPUT_DIR)/*.run)
+CRATES_TESTING_OUTPUTS ::= $(patsubst $(CRATES_TESTING_INPUT_DIR)/%,$(CRATES_TESTING_OUTPUT_DIR)/%.executed.kore,$(CRATES_TESTING_INPUTS))
+
 MX_SEMANTICS_FILES ::= $(shell find mx-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
 MX_TESTING_KOMPILED ::= .build/mx-testing-kompiled
 MX_TESTING_TIMESTAMP ::= $(MX_TESTING_KOMPILED)/timestamp
@@ -91,7 +96,7 @@ build-legacy: \
 		$(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP)
 
 
-test: build syntax-test preprocessing-test execution-test
+test: build syntax-test preprocessing-test execution-test crates-test
 
 test-legacy: mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test
 
@@ -101,6 +106,8 @@ preprocessing-test: $(PREPROCESSING_OUTPUTS)
 
 execution-test: $(EXECUTION_OUTPUTS)
 
+crates-test: $(CRATES_TESTING_OUTPUTS)
+
 mx-test: $(MX_TESTING_OUTPUTS)
 
 mx-rust-test: $(MX_RUST_TESTING_OUTPUTS)
@@ -207,14 +214,17 @@ $(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: \
 			parsers/contract-rust.sh \
 			parsers/test-rust.sh
 	mkdir -p $(EXECUTION_OUTPUT_DIR)
+	echo "<(<" > $@.in.tmp
+	echo "$<" | sed 's%^.*/%%' | sed 's/\..*//' | sed 's/^/::/' >> $@.in.tmp
+	echo "<|>" >> $@.in.tmp
+	cat "$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" >> $@.in.tmp
+	echo ">)>" >> $@.in.tmp
 	krun \
-		"$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \
+		$@.in.tmp \
 		--definition $(RUST_EXECUTION_KOMPILED) \
-		--parser $(CURDIR)/parsers/contract-rust.sh \
+		--parser $(CURDIR)/parsers/crates-rust-execution.sh \
 		--output kore \
 		--output-file $@.tmp \
-		-cCRATE_PATH="$(shell echo "$<" | sed 's%^.*/%%' | sed 's/\..*//' | sed 's/^/::/')" \
-		-pCRATE_PATH=$(CURDIR)/parsers/type-path-rust.sh \
 		-cTEST="$(shell cat $<)" \
 		-pTEST=$(CURDIR)/parsers/test-rust.sh
 	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
@@ -326,3 +336,36 @@ $(DEMOS_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 		-pARGS=$(CURDIR)/parsers/args-mx-rust-contract.sh
 	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f $@.tmp $@
+
+
+# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs
+# as a dependency
+$(CRATES_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
+			$(CRATES_TESTING_INPUT_DIR)/%.run \
+			$(CRATES_TESTING_INPUT_DIR)/crate_1.rs \
+			$(CRATES_TESTING_INPUT_DIR)/crate_2.rs \
+			$(RUST_EXECUTION_TIMESTAMP) \
+			$(wildcard parsers/inc-*.sh) \
+			parsers/crates-rust-execution.sh \
+			parsers/test-rust.sh
+	mkdir -p $(CRATES_TESTING_OUTPUT_DIR)
+	echo "<(<" > $@.in.tmp
+	echo "::crate_1" >> $@.in.tmp
+	echo "<|>" >> $@.in.tmp
+	cat $(CRATES_TESTING_INPUT_DIR)/crate_1.rs >> $@.in.tmp
+	echo ">)>" >> $@.in.tmp
+	echo "<(<" >> $@.in.tmp
+	echo "::crate_2" >> $@.in.tmp
+	echo "<|>" >> $@.in.tmp
+	cat $(CRATES_TESTING_INPUT_DIR)/crate_2.rs >> $@.in.tmp
+	echo ">)>" >> $@.in.tmp
+	krun \
+		$@.in.tmp \
+		--parser $(CURDIR)/parsers/crates-rust-execution.sh \
+		--definition $(RUST_EXECUTION_KOMPILED) \
+		--output kore \
+		--output-file $@.tmp \
+		-cTEST="$(shell cat $<)" \
+		-pTEST=$(CURDIR)/parsers/test-rust.sh
+	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
+	mv -f $@.tmp $@

parsers/crates-rust-execution.sh

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

parsers/inc-crates.sh

@@ -0,0 +1,8 @@
+function parse_crates() {
+    kast \
+        --output kore \
+        --definition $1 \
+        --module RUST-CRATES-SYNTAX \
+        --sort WrappedCrateList \
+        $2
+}

rust-semantics/helpers.md

@@ -20,7 +20,7 @@ module RUST-HELPERS
     rule isSameType(u16(_), u16) => true
     rule isSameType(i8(_), i8) => true
     rule isSameType(u8(_), u8) => true
-    rule isSameType(struct(T, _), T:Type) => true
+    rule isSameType(struct(T, _), T:TypePath) => true
     rule isSameType(struct(T, _), T:Identifier _:GenericArgs ) => true
 
 endmodule

rust-semantics/preprocessing/crate.md

@@ -8,6 +8,10 @@ module CRATE
     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

rust-semantics/targets/execution/configuration.md

@@ -5,7 +5,7 @@ module COMMON-K-CELL
     imports private RUST-PREPROCESSING-SYNTAX
 
     configuration
-        <k> crateParser($PGM:Crate, $CRATE_PATH:TypePath)
+        <k> cratesParser($PGM:WrappedCrateList)
             ~> $TEST:ExecutionTest
         </k>
 endmodule

tests/crates/crate.1.run

@@ -0,0 +1,6 @@
+new :: crate_1 :: First;
+new :: crate_2 :: Second;
+push 123_u64;
+call :: crate_1 :: First.call_second;
+return_value;
+check_eq 126_u64

tests/crates/crate_1.rs

@@ -0,0 +1,9 @@
+#![no_std]
+
+use crate_2::*;
+
+pub trait First {
+    fn call_second(&self, second: ::crate_2::Second, value: u64) -> u64 {
+        second.f(value)
+    }
+}

tests/crates/crate_2.rs

@@ -0,0 +1,7 @@
+#![no_std]
+
+pub trait Second {
+    fn f(&self, value: u64) -> u64 {
+        value + 3_u64
+    }
+}