Execution tests framework

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 > [email protected] && mv -f [email protected] $@
@@ -43,3 +56,16 @@ $(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: $(PREPROCESSING_INPUT_DIR)/%
 	cat [email protected] | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f [email protected] $@
 
+# 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 [email protected] \
+		-cTEST="$(shell cat $<)" \
+		-pTEST=$(CURDIR)/run-test.sh
+	cat [email protected] | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
+	mv -f [email protected] $@

run-test.sh

@@ -0,0 +1,8 @@
+#! /bin/bash
+
+kast \
+    --output kore \
+    --definition .build/rust-execution-kompiled \
+    --module RUST-SYNTAX \
+    --sort ExecutionTest \
+    $1

rust-semantics/config.md

@@ -1,11 +1,13 @@
 ```k
 
 module RUST-CONFIGURATION
+    imports RUST-EXECUTION-CONFIGURATION
     imports RUST-PREPROCESSING-CONFIGURATION
 
     configuration
         <rust>
             <preprocessed/>
+            <execution/>
         </rust>
 
 endmodule

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
+
+```

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
+
+```

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
+        <k>
+            normalizedMethodCall(
+                TraitName:TypePath,
+                MethodName:Identifier,
+                Args:NormalizedCallParams
+            ) => pushLocalState
+                ~> clearLocalState
+                ~> setArgs(Args, Params)
+                ~> FunctionBody
+                ~> popLocalState
+            ...
+        </k>
+        <trait-path> TraitName </trait-path>
+        <method-name> MethodName </method-name>
+        <method-params> Params:NormalizedFunctionParameterList </method-params>
+        <method-implementation> block(FunctionBody) </method-implementation>
+
+    rule
+        <k>
+            clearLocalState => .K
+            ...
+        </k>
+        <locals> _ => .Map </locals>
+
+    rule
+        <k>
+            setArgs(
+                (ValueId:Int , Ids:NormalizedCallParams) => Ids,
+                ((Name:Identifier : T:Type) , Ps:NormalizedFunctionParameterList) => Ps
+            )
+            ...
+        </k>
+        <locals> Locals:Map => Locals[Name <- ValueId] </locals>
+        <values> ValueId |-> Value ... </values>
+        requires notBool Name in_keys(Locals) andBool isSameType(Value, T)
+
+    rule setArgs(.NormalizedCallParams, .NormalizedFunctionParameterList) => .K
+
+endmodule
+
+```

rust-semantics/execution/configuration.md

@@ -0,0 +1,17 @@
+```k
+
+module RUST-EXECUTION-CONFIGURATION
+    imports INT
+    imports LIST
+    imports MAP
+
+    configuration
+        <execution>
+            <values> .Map </values>  // Map from ValueId:Int |-> Value
+            <locals> .Map </locals>  // Map from Identifier |-> ValueId:Int
+            <stack> .List </stack>  // list of locals map.
+            <next-value-id> 0 </next-value-id>
+        </execution>
+endmodule
+
+```

rust-semantics/execution/stack.md

@@ -0,0 +1,28 @@
+```k
+
+module RUST-STACK
+    imports LIST
+    imports RUST-RUNNING-CONFIGURATION
+
+    syntax Instruction  ::= "pushLocalState"
+                          | "popLocalState"
+
+    rule
+        <k>
+            pushLocalState => .K
+            ...
+        </k>
+        <locals> Locals </locals>
+        <stack> .List => ListItem(Locals) ... </stack>
+
+    rule
+        <k>
+            popLocalState => .K
+            ...
+        </k>
+        <locals> _ => Locals </locals>
+        <stack> ListItem(Locals) => .List ... </stack>
+
+endmodule
+
+```

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
+```

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
 
-```
+```

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
-
-```

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
+        <rust-mx>
+            <k> crateParser($PGM:Crate) ~> $TEST:ExecutionTest </k>
+            <rust/>
+            <rust-test/>
+        </rust-mx>
+endmodule
+
+```

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
+
+```

rust-semantics/targets/preprocessing/configuration.md

@@ -1,11 +1,14 @@
 ```k
+
 module RUST-RUNNING-CONFIGURATION
     imports private RUST-PREPROCESSING-SYNTAX
     imports RUST-CONFIGURATION
+
     configuration
         <rust-mx>
             <k> crateParser($PGM:Crate) </k>
             <rust/>
         </rust-mx>
 endmodule
+
 ```

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

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
+
+```

rust-semantics/test/configuration.md

@@ -0,0 +1,12 @@
+```k
+
+module RUST-EXECUTION-TEST-CONFIGURATION
+    imports LIST
+
+    configuration
+        <rust-test>
+            <test-stack> .List </test-stack>
+        </rust-test>
+endmodule
+
+```