Set up conformance testing

.github/actions/with-docker/Dockerfile

@@ -1,3 +1,9 @@
+ARG K_VERSION
+ARG TOOLCHAIN_VERSION
+
+ARG TOOLCHAIN_VERSION
+FROM runtimeverificationinc/riscv-gnu-toolchain:ubuntu-jammy-${TOOLCHAIN_VERSION} as TOOLCHAIN
+
 ARG K_VERSION
 FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION}
 
@@ -20,3 +26,6 @@ WORKDIR /home/user
 
 ENV PATH=/home/user/.local/bin:${PATH}
 RUN curl -sSL https://install.python-poetry.org | python3 -
+
+COPY --from=TOOLCHAIN /opt/riscv /home/user/riscv
+ENV PATH=/home/user/riscv/bin:${PATH}

.github/actions/with-docker/action.yml

@@ -15,10 +15,12 @@ runs:
       CONTAINER_NAME=${{ inputs.container-name }}
       TAG=runtimeverificationinc/${CONTAINER_NAME}
       K_VERSION=$(cat deps/k_release)
+      TOOLCHAIN_VERSION=$(cat deps/riscv-gnu-toolchain_release)
       docker build .                                  \
         --file .github/actions/with-docker/Dockerfile \
         --tag ${TAG}                                  \
-        --build-arg K_VERSION=${K_VERSION}
+        --build-arg K_VERSION=${K_VERSION}            \
+        --build-arg TOOLCHAIN_VERSION=${TOOLCHAIN_VERSION}
       docker run                          \
         --name ${CONTAINER_NAME}          \
         --rm                              \

.github/workflows/test.yml

@@ -57,6 +57,7 @@ jobs:
         uses: actions/checkout@v3
         with:
           fetch-depth: 0
+          submodules: recursive
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:

.gitignore

@@ -1,3 +1,5 @@
 /dist/
 __pycache__/
 .coverage
+tests/riscof/work.lock
+tests/riscof/work

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "tests/riscv-arch-test"]
+	path = tests/riscof/riscv-arch-test
+	url = [email protected]:riscv-non-isa/riscv-arch-test.git

deps/riscv-gnu-toolchain_release

@@ -0,0 +1 @@
+2024.04.12

package/version

@@ -1 +1 @@
-0.1.7
+0.1.8

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.7"
+version = "0.1.8"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -16,6 +16,10 @@ riscv-semantics = "kriscv.kdist.plugin"
 [tool.poetry.dependencies]
 python = "^3.10"
 pyk = { git = "https://github.com/runtimeverification/k.git", tag = "v7.0.120", subdirectory = "pyk" }
+pyyaml = "^6.0.1"
+types-pyyaml = "^6.0.12.20240311"
+filelock = "^3.14.0"
+riscof = "^1.25.3"
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"

src/tests/integration/test_conformance.py

@@ -0,0 +1,166 @@
+from __future__ import annotations
+
+import logging
+import os
+import shutil
+import subprocess
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+import pytest
+import yaml
+from filelock import FileLock
+
+from ..utils import REPO_ROOT
+
+if TYPE_CHECKING:
+    from typing import Any, Final
+
+_LOGGER: Final = logging.getLogger(__name__)
+_LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
+
+RISCOF: Final = REPO_ROOT / 'tests' / 'riscof'
+
+
+def _skipped_tests() -> set[Path]:
+    return {REPO_ROOT / test_path for test_path in (RISCOF / 'failing.txt').read_text().splitlines()}
+
+
+# Failing tests pulled from tests/riscof/failing.txt
+SKIPPED_TESTS: Final = _skipped_tests()
+
+ARCH_SUITE_DIR: Final = RISCOF / 'riscv-arch-test' / 'riscv-test-suite'
+
+
+def _mod_time(path: Path) -> float:
+    """Get the modification time of a directory, accounting for all its recursive contents."""
+    if path.is_file():
+        return os.path.getmtime(path)
+    return max(
+        os.path.getmtime(entry)
+        for root, _, files in os.walk(path)
+        for entry in [os.path.join(root, name) for name in files] + [root]
+    )
+
+
+def _test_list() -> Path:
+    """Get the path to test_list.yaml, regenerating if needed."""
+    work_dir = RISCOF / 'work'
+    test_list = work_dir / 'test_list.yaml'
+    config = RISCOF / 'config.ini'
+    # Lock file to avoid every worker trying to regenerate the test list when using pytest-xdist
+    with FileLock(RISCOF / 'work.lock'):
+        if not test_list.exists() or _mod_time(test_list) < max(_mod_time(ARCH_SUITE_DIR), _mod_time(config)):
+            if work_dir.exists():
+                shutil.rmtree(work_dir)
+            subprocess.run(
+                [
+                    'riscof',
+                    'testlist',
+                    f'--suite={ARCH_SUITE_DIR}',
+                    f'--env={ARCH_SUITE_DIR / "env"}',
+                    f'--config={config}',
+                    f'--work-dir={work_dir}',
+                ],
+                check=True,
+            )
+    assert test_list.exists()
+    return test_list
+
+
+TEST_LIST: Final = _test_list()
+ALL_ARCH_TESTS: Final = tuple(yaml.safe_load(TEST_LIST.read_text()).values())
+ARCH_TESTS: Final = tuple(test for test in ALL_ARCH_TESTS if test['test_path'] not in SKIPPED_TESTS)
+REST_ARCH_TESTS: Final = tuple(test for test in ALL_ARCH_TESTS if test['test_path'] in SKIPPED_TESTS)
+
+
+def _isa_spec() -> dict[str, Any]:
+    isa_yaml = RISCOF / 'kriscv' / 'kriscv_isa.yaml'
+    return yaml.safe_load(isa_yaml.read_text())['hart0']
+
+
+ISA_SPEC: Final = _isa_spec()
+
+
+def _mabi() -> str:
+    spec_isa = ISA_SPEC['ISA']
+    if '64I' in spec_isa:
+        return 'lp64'
+    if '64E' in spec_isa:
+        return 'lp64e'
+    if '32I' in spec_isa:
+        return 'ilp32'
+    if '32E' in spec_isa:
+        return 'ilp32e'
+    raise AssertionError(f'Bad ISA spec: {spec_isa}')
+
+
+def _compile_test(test: dict[str, Any]) -> Path:
+    """Compile the test for the given test entry from test_list.yaml.
+
+    Produces the compiled <test>.elf file and returns the path to its disassembly <test>.diss."
+    """
+    test_file = Path(test['test_path'])
+    _LOGGER.info(f'Running test: {test_file}')
+    march = test['isa'].lower()
+    plugin_env = RISCOF / 'kriscv' / 'env'
+    plugin_link = plugin_env / 'link.ld'
+    suite_env = ARCH_SUITE_DIR / 'env'
+    work_dir = Path(test['work_dir'])
+    elf_output = work_dir / (work_dir.stem + '.elf')
+    diss_output = work_dir / (work_dir.stem + '.diss')
+    compile_cmd = [
+        'riscv64-unknown-elf-gcc',
+        f'-march={march}',
+        f'-mabi={_mabi()}',
+        '-static',
+        '-mcmodel=medany',
+        '-fvisibility=hidden',
+        '-nostdlib',
+        '-nostartfiles',
+        '-T',
+        f'{plugin_link}',
+        '-I',
+        f'{plugin_env}',
+        '-I',
+        f'{suite_env}',
+        f'{test_file}',
+        '-o',
+        f'{elf_output}',
+    ]
+    compile_cmd += [f'-D{macro}' for macro in test['macros']]
+    subprocess.run(
+        compile_cmd,
+        check=True,
+    )
+    assert elf_output.exists()
+    with open(diss_output, 'w') as out:
+        subprocess.run(
+            ['riscv64-unknown-elf-objdump', '--no-addresses', '--no-show-raw-insn', '-D', elf_output], stdout=out
+        )
+    return diss_output
+
+
+def _test(diss_file: Path) -> None:
+    """Execute a compiled test given its disassembled ELF file."""
+
+
+@pytest.mark.parametrize(
+    'test_entry',
+    ARCH_TESTS,
+    ids=[str(Path(test['test_path']).relative_to(ARCH_SUITE_DIR)) for test in ARCH_TESTS],
+)
+def test_arch(test_entry: dict[str, Any]) -> None:
+    diss_file = _compile_test(test_entry)
+    _test(diss_file)
+
+
+@pytest.mark.skip(reason='failing arch tests')
+@pytest.mark.parametrize(
+    'test_entry',
+    REST_ARCH_TESTS,
+    ids=[str(Path(test['test_path']).relative_to(ARCH_SUITE_DIR)) for test in REST_ARCH_TESTS],
+)
+def test_rest_arch(test_entry: dict[str, Any]) -> None:
+    diss_file = _compile_test(test_entry)
+    _test(diss_file)

src/tests/utils.py

@@ -0,0 +1,10 @@
+from __future__ import annotations
+
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+if TYPE_CHECKING:
+    from typing import Final
+
+
+REPO_ROOT: Final = Path(__file__).parents[2].resolve(strict=True)

tests/riscof/README.md

@@ -0,0 +1,57 @@
+# RISC-V Architectural Tests
+This directory contains the RISC-V Architectural Test Suite and associated configuration.
+
+## Contents
+### riscv-arch-test
+The submodule containing the actual test files under `riscv-arch-test/riscv-test-suite`.
+
+### failing.txt
+A list of tests that are known to fail with the current implementation. Each line gives the path to a failing test file relative to the `riscv-semantics` repo root.
+
+### config.ini
+The [riscof configuration file](https://riscof.readthedocs.io/en/1.24.0/inputs.html?highlight=config.ini#config-ini-syntax) specifying the paths to our DUT and golden reference plugins. 
+
+### krsicv
+The [DUT plugin](https://riscof.readthedocs.io/en/1.24.0/plugins.html) for our RISC-V implementation. Consists of
+- env
+  - link.ld
+     - Linker script used when compiling each test. 
+     - Unmodified from the riscof model template.
+   - model_test.h
+     - Definition of macros used in the test suite.
+     - Unmodified from the riscof model template, except that `RVMODEL_HALT` uses `t2` rather than `t5` because `t5` does not exist for the `rv32e` and `rv64e` ISAs.
+- kriscv_isa.yaml
+  - Specification of the supported ISA and extensions as described in [https://riscv-config.readthedocs.io/en/3.3.1/yaml-specs.html#isa-yaml-spec](https://riscv-config.readthedocs.io/en/3.3.1/yaml-specs.html#isa-yaml-spec)
+- kriscv_platform.yaml
+   - Specification of the platform as described in [https://riscv-config.readthedocs.io/en/3.3.1/yaml-specs.html#platform-yaml-spec](https://riscv-config.readthedocs.io/en/3.3.1/yaml-specs.html#platform-yaml-spec)
+- riscof_kriscv.py
+   - The actual plugin implementation for initializing, building, and running the test suite  with riscof.
+   - Currently under construction.
+
+### sail_cSim
+Analogous to `kriscv`, but for the golden reference [Sail RISC-V model](https://github.com/riscv/sail-riscv). Taken from [https://gitlab.com/incoresemi/riscof-plugins/-/tree/master/sail_cSim](https://gitlab.com/incoresemi/riscof-plugins/-/tree/master/sail_cSim)
+
+### work
+The test working directory generated during a test run. After a test run, this will contain:
+ - kriscv_isa_checked.yaml
+   - Completion of `kriscv_isa.yaml` with all defaults made explicit.
+ - kriscv_platform_checked.yaml
+   - Completion of `kriscv_platform.yaml` with all defaults made explicit.  
+ - database.yaml
+    -  A database of all tests in the test suite and their associated info pulled from the various `RVTEST` macros.
+- test_list.yaml
+   - The list of supported tests to run based on the `kriscv` ISA and platform specs.
+- rv(32|64)_(i|e)...
+   - The working directory for each individual test.
+   - Follows the same directory structure as the tests in `riscv-arch-test/riscv-test-suite`, but each `.S` file is replaced by a directory of the same name containing the compiled `.elf` and disassembled `.diss` files.
+
+### work.lock
+A lock file used to control concurrent accesses to the `work` directory by different test workers.
+
+## Running the Tests
+### PyTest
+These tests are run as part of `make test-integration` under `src/tests/integration/test_conformance.py`. Tests are selected based on the riscof-generated `test_list.yaml`. Failing tests under `failing.txt` will automatically be skipped.
+
+### riscof
+The full riscof DUT plugin is still under construction, so execution with riscof is currently unsupported.
+

tests/riscof/config.ini

@@ -0,0 +1,14 @@
+[RISCOF]
+ReferencePlugin=sail_cSim
+ReferencePluginPath=tests/riscof/sail_cSim
+DUTPlugin=kriscv
+DUTPluginPath=tests/riscof/kriscv
+
+[kriscv]
+pluginpath=tests/riscof/kriscv
+ispec=tests/riscof/kriscv/kriscv_isa.yaml
+pspec=tests/riscof/kriscv/kriscv_platform.yaml
+target_run=1
+
+[sail_cSim]
+pluginpath=tests/riscof/sail_cSim

tests/riscof/kriscv/env/link.ld

@@ -0,0 +1,18 @@
+OUTPUT_ARCH( "riscv" )
+ENTRY(rvtest_entry_point)
+
+SECTIONS
+{
+  . = 0x80000000;
+  .text.init : { *(.text.init) }
+  . = ALIGN(0x1000);
+  .tohost : { *(.tohost) }
+  . = ALIGN(0x1000);
+  .text : { *(.text) }
+  . = ALIGN(0x1000);
+  .data : { *(.data) }
+  .data.string : { *(.data.string)}
+  .bss : { *(.bss) }
+  _end = .;
+}
+