Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
98 changes: 89 additions & 9 deletions .github/workflows/test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@ name: 'Test'
on:
pull_request:
workflow_dispatch:
permissions:
contents: read
packages: write
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
Expand Down Expand Up @@ -49,10 +52,14 @@ jobs:
- name: 'Run unit tests'
run: make test-unit

integration-tests:
build:
needs: code-quality-checks
name: 'Integration Tests'
name: 'Build'
runs-on: [self-hosted, linux, normal]
permissions:
packages: write
outputs:
image: ${{ steps.commit-image.outputs.image }}
steps:
- name: 'Check out code'
uses: actions/checkout@v4
Expand All @@ -62,14 +69,88 @@ jobs:
- name: 'Set up Docker'
uses: ./.github/actions/with-docker
with:
container-name: mir-semantics-ci-${{ github.sha }}
container-name: mir-semantics-build-${{ github.sha }}
- name: 'Build stable-mir-json and kmir'
run: docker exec --user github-user mir-semantics-ci-${GITHUB_SHA} make build
- name: 'Run integration tests'
run: docker exec --user github-user mir-semantics-ci-${GITHUB_SHA} make test-integration
run: docker exec --user github-user mir-semantics-build-${GITHUB_SHA} make stable-mir-json build
- name: 'Commit and push built image to GHCR'
id: commit-image
run: |
IMAGE="ghcr.io/runtimeverification/mir-semantics/ci:${GITHUB_SHA}"
docker commit mir-semantics-build-${GITHUB_SHA} ${IMAGE}
echo ${{ secrets.GITHUB_TOKEN }} | docker login ghcr.io -u ${{ github.actor }} --password-stdin
docker push ${IMAGE}
Comment on lines +79 to +81

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Avoid pushing images that contain checkout credentials

This job checks out with actions/checkout@v4 using secrets.JENKINS_GITHUB_PAT and then commits/pushes the running container, which already has the copied workspace under /home/github-user/workspace; in v4, checkout persists auth credentials for git commands, so the committed layer can include those credentials (for example via repo git config) and expose them to anyone who can pull ghcr.io/.../ci:<sha>. Avoid committing that workspace as-is (or set persist-credentials: false and scrub .git before docker commit).

Useful? React with 👍 / 👎.

echo "image=${IMAGE}" >> "${GITHUB_OUTPUT}"
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time 0 mir-semantics-build-${GITHUB_SHA} || true
docker rmi ${{ steps.commit-image.outputs.image }} || true

integration-tests-llvm:
needs: [code-quality-checks, build]
name: 'Integration Tests (LLVM)'
runs-on: [self-hosted, linux, normal]
permissions:
packages: read
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
token: ${{ secrets.JENKINS_GITHUB_PAT }}
submodules: recursive
- name: 'Pull pre-built image and start container'
run: |
echo ${{ secrets.GITHUB_TOKEN }} | docker login ghcr.io -u ${{ github.actor }} --password-stdin
docker pull ${{ needs.build.outputs.image }}
docker run \
--name mir-semantics-llvm-${GITHUB_SHA} \
--rm \
--interactive \
--tty \
--detach \
--workdir /home/github-user/workspace \
${{ needs.build.outputs.image }}
docker cp . mir-semantics-llvm-${GITHUB_SHA}:/home/github-user/workspace
docker exec --user root mir-semantics-llvm-${GITHUB_SHA} \
chown -R github-user:github-user /home/github-user/workspace
- name: 'Run LLVM integration tests'
run: docker exec --user github-user mir-semantics-llvm-${GITHUB_SHA} make test-integration-llvm
- name: 'Tear down Docker'
if: always()
run: docker stop --time 0 mir-semantics-ci-${GITHUB_SHA}
run: docker stop --time 0 mir-semantics-llvm-${GITHUB_SHA} || true

integration-tests-haskell:
needs: [code-quality-checks, build]
name: 'Integration Tests (Haskell)'
runs-on: [self-hosted, linux, normal]
permissions:
packages: read
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
token: ${{ secrets.JENKINS_GITHUB_PAT }}
submodules: recursive
- name: 'Pull pre-built image and start container'
run: |
echo ${{ secrets.GITHUB_TOKEN }} | docker login ghcr.io -u ${{ github.actor }} --password-stdin
docker pull ${{ needs.build.outputs.image }}
docker run \
--name mir-semantics-haskell-${GITHUB_SHA} \
--rm \
--interactive \
--tty \
--detach \
--workdir /home/github-user/workspace \
${{ needs.build.outputs.image }}
docker cp . mir-semantics-haskell-${GITHUB_SHA}:/home/github-user/workspace
docker exec --user root mir-semantics-haskell-${GITHUB_SHA} \
chown -R github-user:github-user /home/github-user/workspace
- name: 'Run Haskell integration tests'
run: docker exec --user github-user mir-semantics-haskell-${GITHUB_SHA} make test-integration-haskell
- name: 'Tear down Docker'
if: always()
run: docker stop --time 0 mir-semantics-haskell-${GITHUB_SHA} || true

stable-mir-json-integration-tests:
needs: code-quality-checks
Expand Down Expand Up @@ -181,7 +262,7 @@ jobs:
strategy:
fail-fast: false
matrix:
runner: [normal, MacM1] # MacM1 / normal are self-hosted,
runner: [normal, MacM1] # MacM1 / normal are self-hosted,
runs-on: ${{ matrix.runner }}
timeout-minutes: 20
steps:
Expand Down Expand Up @@ -212,4 +293,3 @@ jobs:
set -euxo pipefail
nix --version
nix flake check # build and run smoke test

10 changes: 10 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,16 @@ test-integration: stable-mir-json build
$(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration --maxfail=1 --verbose \
--durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS)

test-integration-llvm: stable-mir-json build
$(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration --maxfail=1 --verbose \
--durations=0 --numprocesses=$(PARALLEL) --dist=worksteal \
-k "llvm or test_decode_value or test_run_smir_random or test_python_decode_value" $(TEST_ARGS)

test-integration-haskell: stable-mir-json build
$(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration --maxfail=1 --verbose \
--durations=0 --numprocesses=$(PARALLEL) --dist=worksteal \
-k "haskell or test_prove or test_crate_examples or test_schema_parse or test_schema_kapply_parse or test_prove_termination or test_functions or test_cli" $(TEST_ARGS)

.PHONY: test-stable-mir-ui
test-stable-mir-ui: stable-mir-json build
@test -n "$(RUST_DIR_ROOT)" || (echo "RUST_DIR_ROOT is required. Example: RUST_DIR_ROOT=/path/to/rust make test-stable-mir-ui"; exit 2)
Expand Down
75 changes: 75 additions & 0 deletions kmir/src/tests/integration/conftest.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,75 @@
from __future__ import annotations

import hashlib
import time
from typing import TYPE_CHECKING

import pytest

if TYPE_CHECKING:
from pathlib import Path

from pytest import TempPathFactory


def _smir_kompile_key(smir_json: Path, symbolic: bool) -> str:
"""Return a short stable key for a (smir_json, symbolic) pair."""
path_hash = hashlib.sha256(str(smir_json).encode()).hexdigest()[:16]
suffix = 'symbolic' if symbolic else 'concrete'
return f'{path_hash}-{suffix}'


@pytest.fixture(scope='session')
def kompile_cache_dir(tmp_path_factory: TempPathFactory) -> Path:
"""Session-scoped base directory for kompile cache.

Returns a stable temporary directory that persists across the test session,
allowing KompileDigest caching in kompile_smir to avoid redundant llvm-kompile calls
when multiple test_exec_smir parametrizations share the same smir_json + symbolic combo.
"""
return tmp_path_factory.mktemp('kompile-cache', numbered=False)


@pytest.fixture(scope='session')
def exec_smir_kompile_dirs(kompile_cache_dir: Path) -> dict[str, Path]:
"""Session-scoped mapping from (smir_json, symbolic) key to shared kompile output dir.

Multiple test_exec_smir invocations that share the same smir_json + symbolic flag
will reuse the same target_dir, letting KompileDigest skip redundant kompile calls.
"""
return {}


def get_exec_smir_target_dir(
smir_json: Path,
symbolic: bool,
kompile_cache_dir: Path,
exec_smir_kompile_dirs: dict[str, Path],
) -> Path:
"""Return a shared target directory for a given (smir_json, symbolic) pair.

Uses a file lock to avoid concurrent kompile races when running under pytest-xdist.
"""
key = _smir_kompile_key(smir_json, symbolic)
if key in exec_smir_kompile_dirs:
return exec_smir_kompile_dirs[key]

target = kompile_cache_dir / key
lock_file = kompile_cache_dir / f'{key}.lock'

try:
# Attempt to claim the lock (atomic create)
with open(lock_file, 'x'):
target.mkdir(parents=True, exist_ok=True)
exec_smir_kompile_dirs[key] = target
lock_file.unlink(missing_ok=True)
Comment on lines +62 to +65

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Keep the lock held until kompilation has finished

The lock file is removed immediately after creating the target directory, but the expensive work (KMIR.from_kompiled_kore(...)) happens later in the test, so concurrent xdist workers that hit the same (smir_json, symbolic) key can still enter kompilation at the same time and write into the same target_dir, causing flaky or corrupted integration outputs. The critical section needs to include the actual kompile step, not just directory creation.

Useful? React with 👍 / 👎.

except FileExistsError:
# Another worker is building; wait for the lock to be released (max 5 min)
target.mkdir(parents=True, exist_ok=True)
secs = 0
while lock_file.exists() and secs < 300:
time.sleep(1)
secs += 1
exec_smir_kompile_dirs[key] = target
Comment on lines +70 to +73

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Raise on lock timeout instead of using a possibly partial dir

When another worker holds the lock longer than 300 seconds, this code still records and returns target even if lock_file still exists, so callers may proceed against a partially built kompile directory and fail nondeterministically. If the timeout is reached, this should error out (or continue waiting) rather than pretending the cache entry is ready.

Useful? React with 👍 / 👎.


return target
8 changes: 6 additions & 2 deletions kmir/src/tests/integration/test_integration.py
Original file line number Diff line number Diff line change
Expand Up @@ -390,11 +390,15 @@ def test_exec_smir(
test_case: tuple[str, Path, Path, int],
symbolic: bool,
update_expected_output: bool,
tmp_path: Path,
kompile_cache_dir: Path,
exec_smir_kompile_dirs: dict[str, Path],
) -> None:
from .conftest import get_exec_smir_target_dir

_, input_json, output_kast, depth = test_case
smir_info = SMIRInfo.from_file(input_json)
kmir_backend = KMIR.from_kompiled_kore(smir_info, target_dir=tmp_path, symbolic=symbolic)
target_dir = get_exec_smir_target_dir(input_json, symbolic, kompile_cache_dir, exec_smir_kompile_dirs)
kmir_backend = KMIR.from_kompiled_kore(smir_info, target_dir=target_dir, symbolic=symbolic)
result = kmir_backend.run_smir(smir_info, depth=depth)
result_pretty = kmir_backend.kore_to_pretty(result).rstrip()
assert_or_update_show_output(result_pretty, output_kast, update=update_expected_output)
Expand Down
Loading