Merge branch 'master' into dc/documentation

.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}

.github/workflows/update-version.yml

@@ -34,7 +34,6 @@ jobs:
         run: |
           K_VERSION=$(cat deps/k_release)
           sed -i 's!    k-framework.url = "github:runtimeverification/k/[v0-9\.]*"!    k-framework.url = "github:runtimeverification/k/v'"${K_VERSION}"'"!' flake.nix
-          sed -i 's!    pyk.url = "github:runtimeverification/k/[v0-9\.]*?dir=pyk"!    pyk.url = "github:runtimeverification/k/v'"${K_VERSION}"'?dir=pyk"!' flake.nix
           nix --extra-experimental-features 'nix-command flakes' --show-trace flake update
           git add flake.nix flake.lock
           git commit -m 'flake.{nix,lock}: update Nix derivations' || true

.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); \

deps/k_release

@@ -1 +1 @@
-7.1.112
+7.1.165