411 simple integration test using old simple rust programs (#413)

This PR adds a set of simple rust programs (from prior art) for a simple
parser test:
* salvages [old test programs from `run-rs` in the `textual-mir`
branch](https://github.com/runtimeverification/mir-semantics/tree/textual-mir/kmir/src/tests/integration/test-data/run-rs)
* [sets up
`smir_pretty`](https://github.com/runtimeverification/smir_pretty) as a
submodule for integration tests
* adds `make` targets to manage the submodule build (including a
bootstrap of `rustc`, which [should be set up as a recursive
submodule](runtimeverification/stable-mir-json#8)
in the future)
* adds a `make` target for a simple integration test: convert each
`run-rs` program to Stable-MIR and parse the result.

Remarks: 
* The tests are currently only proving that the parser succeeds. We can
add better checks later when the format is stable enough to not cause
noise in golden tests.
* In order to run `smir_pretty`, information about the rust target
architecture is needed. To circumvent this, the related script (within
`smir_pretty` repo) is patched (but only the copy in the docker file
system). This is a workaround and could be addressed properly by
  - crafting a github action to set up K and removing the dockerised K,
- or preparing `smir_pretty` to run within `nix` and using a nix shell.
- or (not recommended) placing the custom `rust` build and `smir_pretty`
within the docker image or container.

---------

Co-authored-by: devops <[email protected]>

.github/workflows/test.yml

@@ -76,3 +76,62 @@ jobs:
       - name: 'Tear down Docker'
         if: always()
         run: docker stop --time 0 mir-semantics-ci-${GITHUB_SHA}
+
+  smir-integration-tests:
+    needs: code-quality-checks
+    name: "Integration with smir_pretty"
+    runs-on: [self-hosted, linux, normal]
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+        with:
+          token: ${{ secrets.JENKINS_GITHUB_PAT }}
+          submodules: recursive
+
+      - name: "Set up nightly Rust" # https://github.com/rust-lang/rustup/issues/3409
+        uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: nightly-2024-08-28
+
+      - name: 'Set up tree for rust dependency of smir_pretty'
+        run: make smir-pretty-setup
+
+      - name: 'Cache smir_pretty and rustc'
+        uses: Swatinem/rust-cache@v2
+        with:
+          workspaces: |
+            deps/smir_pretty
+            deps/smir_pretty/deps/rust/src
+          cache-directories: |
+            deps/smir_pretty/deps/rust/src/build
+
+      - name: 'Build smir_pretty and its rustc dependency'
+        run: | # rustc bootstrap checks this and refuses stage 1 in "CI"
+          export GITHUB_ACTIONS="in denial" && \
+          echo "GITHUB_ACTIONS = ${GITHUB_ACTIONS}" && \
+          make smir-pretty
+
+      - name: 'Set up Docker'
+        uses: ./.github/actions/with-docker
+        with:
+          container-name: mir-smir-ci-${{ github.sha }}
+
+      - name: 'Build kmir (within docker)'
+        run: docker exec --user user mir-smir-ci-${GITHUB_SHA} make build
+
+      - name: 'HACK: patch rustc_arch.sh script (within docker)'
+        run: |
+          arch=$(rustc -vV | sed -n -e 's/host: \(.*\)$/\1/p')
+          docker exec --user user mir-smir-ci-${GITHUB_SHA} \
+              bash -c "printf '#!/bin/sh\necho \"$arch\"\n' > deps/smir_pretty/rustc_arch.sh"
+          docker exec --user user mir-smir-ci-${GITHUB_SHA} \
+              cat deps/smir_pretty/rustc_arch.sh
+          docker exec --user user mir-smir-ci-${GITHUB_SHA} \
+              deps/smir_pretty/rustc_arch.sh
+
+      - name: 'Run parser tests (within docker)'
+        run: docker exec --user user mir-smir-ci-${GITHUB_SHA} make smir-parse-tests
+
+      - name: 'Tear down Docker'
+        if: always()
+        run: docker stop --time 0 mir-smir-ci-${GITHUB_SHA}

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "deps/smir_pretty"]
+	path = deps/smir_pretty
+	url = https://github.com/runtimeverification/smir_pretty

Makefile

@@ -9,3 +9,38 @@ kmir:
 
 build: kmir
 	$(POETRY) run kdist -v build mir-semantics.\* -j4
+
+##################################################
+# for integration tests: build smir_pretty in-tree
+
+##################################################
+# This will change when we set up rustc as a submodule in smir_pretty
+smir-pretty-setup: deps/smir_pretty/deps/rust/src
+
+deps/smir_pretty/deps/rust/src:
+	cd deps/smir_pretty && make setup
+
+##################################################
+
+smir-pretty: smir-pretty-setup deps/smir_pretty/target/debug/smir_pretty
+
+deps/smir_pretty/target/debug/smir_pretty: deps/smir_pretty
+	cd deps/smir_pretty && make build_all
+
+# generate smir and parse given test files (from parameter or run-rs subdirectory)
+smir-parse-tests: TESTS = $(shell find kmir/src/tests/integration/data/run-rs -type f -name "*.rs")
+smir-parse-tests: SMIR = deps/smir_pretty/run.sh
+smir-parse-tests: build smir-pretty
+	errors=""; \
+	report() { echo $$2; errors="$$errors $$1"; }; \
+	for source in ${TESTS}; do \
+	    echo -n "$$source: "; \
+	    dir=$$(dirname $${source}); \
+	    target=$${dir}/$$(basename $${source%.rs}).smir.json; \
+	    ${SMIR} -Z no-codegen --out-dir $${dir} $$source \
+		&& (echo -n "smir-ed "; \
+		    ${POETRY_RUN} convert-from-definition $${target} Pgm > /dev/null \
+			&& (echo "and parsed!"; rm $${target}) || report "$$source" "PARSE ERROR!") \
+		|| report "$$source" "SMIR ERROR!" ; \
+	    done; \
+	[ -z "$$errors" ] || (echo "FAILING TESTS:"; printf ". %s\n" $${errors}; exit 1); \

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.41"
+version = "0.3.42"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.41'
+VERSION: Final = '0.3.42'

kmir/src/kmir/convert_from_definition/v2parser.py

@@ -138,7 +138,8 @@ def _mir_productions_for_sort(self, sort: KSort) -> tuple[KProduction, ...]:
     # aiming for optimization (cache?) in the future.
     def _mir_production_for_symbol(self, sort: KSort, symbol: str) -> KProduction:
         prods = [p for p in self._mir_productions_for_sort(sort) if _get_label(p) == symbol]
-        assert len(prods) == 1
+        assert len(prods) > 0, f"No production for `{symbol}' in sort `{sort.name}'"
+        assert len(prods) == 1, f"Expected a single production for `{symbol}' as sort `{sort.name}'"
         return prods[0]
 
     # Parse the provided json term, with expected Sort name sort.
@@ -155,7 +156,7 @@ def _parse_mir_json(self, json: JSON, sort: KSort) -> ParseResult:
         # correct rule to apply. In the other cases there should only be one
         # production anyway, which is asserted as needed.
         prods = self._mir_productions_for_sort(sort)
-        assert len(prods) > 0
+        assert len(prods) > 0, f"Don't know how to parse sort `{sort.name}'"
         prod = prods[0]
         assert prod in self._mir_productions
 

kmir/src/kmir/kdist/mir-semantics/body.md

@@ -137,7 +137,7 @@ syntax BinOp ::= "binOpAdd"          [group(mir-enum), symbol(BinOp::Add)]
                | "binOpOffset"       [group(mir-enum), symbol(BinOp::Offset)]
 
 syntax UnOp ::= "unOpNot"            [group(mir-enum), symbol(UnOp::Not)]
-              | "unOpNeg"            [group(mir-enum), symbol(UnOp::Net)]
+              | "unOpNeg"            [group(mir-enum), symbol(UnOp::Neg)]
               | "unOpPtrMetadata"    [group(mir-enum), symbol(UnOp::PtrMetadata)]
 
 syntax NullOp ::= "nullOpSizeOf"                         [group(mir-enum), symbol(NullOp::SizeOf)]
@@ -302,7 +302,7 @@ syntax AssertMessage ::= assertMessageBoundsCheck(len: Operand, index: Operand)
                        | assertMessageResumedAfterPanic(CoroutineKind)
                          [group(mir-enum),                   symbol(AssertMessage::ResumedAfterPanic)]
                        | assertMessageMisalignedPointerDereference(required: Operand, found: Operand)
-                         [group(mir-enum---required--found), symbol(AssertMessage::MisalignedPointerDerefence)]
+                         [group(mir-enum---required--found), symbol(AssertMessage::MisalignedPointerDereference)]
 
 syntax InlineAsmOperand  ::= inlineAsmOperand(inValue: MaybeOperand, outValue: MaybePlace, rawPtr: MIRString)
                              [group(mir---in-value--out-place--raw-rpr)]

kmir/src/kmir/kdist/mir-semantics/mono.md

@@ -37,7 +37,7 @@ syntax MonoItemKind ::= monoItemFn(name: Symbol, id: DefId, body: Bodies)
 syntax MonoItem ::= monoItem(symbolName: Symbol, monoItemKind: MonoItemKind)
                       [symbol(monoItemWrapper), group(mir---symbol-name--mono-item-kind)]
 syntax MonoItems ::= List {MonoItem, ""}
-                      [symbol(monoItems), terminator-symbol(.monoItems), group(mir-list)]
+                      [symbol(MonoItems::append), terminator-symbol(MonoItems::empty), group(mir-list)]
 
 ////////////////////////////////////////// unused for parsing?
 

kmir/src/tests/integration/data/run-rs/arrays/array.rs

@@ -0,0 +1,5 @@
+fn main() {
+    let a = [1, 2, 3, 4];
+
+    assert!(a == [1, 2, 3, 4]);
+}

kmir/src/tests/integration/data/run-rs/assert/assert_eq.rs

@@ -0,0 +1,6 @@
+fn main() {
+    let a = 42;
+    let b = 3 + 39;
+
+    assert_eq!(b, a);
+}

kmir/src/tests/integration/data/run-rs/closures/closure-args.rs

@@ -0,0 +1,5 @@
+fn main() {
+    let sum = |x, y| -> i32 { x + y };
+
+    assert!(sum(20, 22) == 42);
+}

kmir/src/tests/integration/data/run-rs/closures/closure-no-args.rs

@@ -0,0 +1,5 @@
+fn main() {
+    let sum = || -> u32 { 42 };
+
+    assert!(sum() == 42);
+}

kmir/src/tests/integration/data/run-rs/enums/enum.rs

@@ -0,0 +1,10 @@
+#![allow(unused)]
+#![allow(dead_code)]
+enum Letter {
+    A,
+    B,
+}
+
+fn main() {
+    let a = Letter::A;
+}

kmir/src/tests/integration/data/run-rs/floats/float.rs

@@ -0,0 +1,11 @@
+fn main() {
+    let a:f32 = 3.5;
+    let b:f32 = 1.2;
+
+    assert!(a + b == 4.7);
+
+    let c:f64 = 3.5;
+    let d:f64 = 1.2;
+
+    assert!(c + d == 4.7);
+}

kmir/src/tests/integration/data/run-rs/functions/sum-to-n.rs

@@ -0,0 +1,23 @@
+fn sum_to_n(n:usize) -> usize {
+    let mut sum = 0;
+    let mut counter = n;
+
+    while counter > 0 {
+      sum += counter;
+      counter = counter - 1;
+    }
+    return sum;
+}
+
+fn test_sum_to_n() -> () {
+    let n = 10;
+    let golden = 55;
+    let sucess = sum_to_n(n) == golden;
+    assert!(sucess);
+}
+
+
+fn main() {
+  test_sum_to_n();
+  return ();
+}

kmir/src/tests/integration/data/run-rs/generics/generic.rs

@@ -0,0 +1,14 @@
+fn index_slice<T>(slice:&[T], index: usize) -> &T {
+    &(slice[index])
+}
+
+fn main() {
+    let numbers = [1, 2, 3, 4, 5];
+    let letters = ['a', 'b', 'c', 'd', 'e'];
+
+    let middle_number:&i32  = index_slice(&numbers[..], 2);
+    let middle_letter:&char = index_slice(&letters[..], 2);
+
+    assert!(*middle_number == 3);
+    assert!(*middle_letter == 'c');
+}

kmir/src/tests/integration/data/run-rs/integers/binop.rs

@@ -0,0 +1,74 @@
+fn test_binop(x:i32, y:i32) -> () {
+// Arithmetic
+    // Addition
+    assert!(x + y == 52);
+    assert!(52 == x + y);
+    assert!(x + y == y + x);
+
+    // Subtraction
+    assert!(x - y == 32);
+    assert!(y - x == -32);
+    assert!(y - x != x - y);
+
+    // Multiplication
+    assert!(x * y == 420);
+    assert!(x * -y == -420);
+    assert!(-x * y == -420);
+    assert!(-x * -y == 420);
+
+    // Division
+    // assert!(420 / 10 == 42); // FAILING SEE div.rs and div.mir
+
+    // Modulo
+    // assert!(x % 10 == 2); // FAILING SEE modulo.rs and modulo.mir
+
+// Bitwise
+    // Xor
+    assert!(1 ^ 2 == 3);
+    assert!(1 ^ 3 == 2);
+
+    // Or
+    assert!(1 | 2 == 3);
+    assert!(1 | 3 == 3);
+
+    // And
+    assert!(1 & 2 == 0);
+    assert!(1 & 3 == 1);
+
+    // // Shl
+    assert!(2 << 1 == 4);
+    // assert!(-128_i8 << 1 == 0); FAILS SEE shl_min.rs and shl_min.mir
+    // assert!(-32768_i16 << 1 == 0); FAILS SEE shl_min.rs and shl_min.mir
+    // assert!(-2147483648_i32 << 1 == 0); FAILS SEE shl_min.rs and shl_min.mir
+    // assert!(-9223372036854775808_i64 << 1 == 0); FAILS SEE shl_min.rs and shl_min.mir
+    // assert!(-17014118346046923173168730371588410572_i128 << 1 == 0); FAILS SEE shl_min.rs and shl_min.mir
+
+
+    // // Shr
+    assert!(2 >> 1 == 1);
+    assert!(3 >> 1 == 1);
+    assert!(1 >> 1 == 0);
+
+// Comparisions
+    // Less Then
+    assert!(x < x + y);
+
+    // Less Then or Equal
+    assert!(x <= x + y);
+    assert!(x <= x + y - y);
+
+    // Greater Then
+    assert!(x + y > x);
+
+    // Greater Then or Equal 
+    assert!(x + y >= x);
+    assert!(x + y - y >= x);
+}
+
+
+fn main() {
+  let x = 42;
+  let y = 10;
+  test_binop(x, y);
+  return ();
+}

kmir/src/tests/integration/data/run-rs/integers/const-arithm-simple.rs

@@ -0,0 +1,12 @@
+fn test(x: usize, y:usize) -> bool {
+    return x > y;
+}
+
+
+fn main() {
+  let x:usize = 42;
+  let y:usize = 0;
+  let z:bool = test(x, y);
+  assert!(z);
+  return ();
+}

kmir/src/tests/integration/data/run-rs/integers/div.rs

@@ -0,0 +1,3 @@
+fn main() {
+    assert!(420 / 10 ==42);
+}

kmir/src/tests/integration/data/run-rs/integers/modulo.rs

@@ -0,0 +1,3 @@
+fn main() {
+    assert!(42 % 10 == 2);
+}

kmir/src/tests/integration/data/run-rs/integers/primitive-type-bounds.rs

@@ -0,0 +1,5 @@
+fn main () {
+    let a:u32 = 4294967295;
+    let b:u32 = 4294967294 + 1;
+    assert!(a == b)
+}

kmir/src/tests/integration/data/run-rs/integers/shl_min.rs

@@ -0,0 +1,7 @@
+fn main() {
+    assert!(-128_i8 << 1 == 0);
+    assert!(-32768_i16 << 1 == 0);
+    assert!(-2147483648_i32 << 1 == 0);
+    assert!(-9223372036854775808_i64 << 1 == 0);
+    assert!(-170141183460469231731687303715884105728_i128 << 1 == 0);
+}

kmir/src/tests/integration/data/run-rs/memory/box.rs

@@ -0,0 +1,9 @@
+fn main() {
+    let a = Box::new(5);
+    let b = Box::new(5);
+
+    assert!(a == b);
+    assert!(*a == *b);
+    assert!(*a == 5);
+    // assert!(a == 5); // Not possible to equate Box::(Type) with Type
+}

kmir/src/tests/integration/data/run-rs/option/option-construction.rs

@@ -0,0 +1,6 @@
+#![allow(unused)]
+fn main() {
+    let a:Option<u32> = Some(42);
+    let b:Option<u32> = None;
+    let c:u32 = a.unwrap();
+}