Execute conformance tests (#30)

* Switch to a SparseBytes data structure to space-efficiently represent memory

* Fix JALR to overwrite PC rather than add to it

* Add --temp-dir flag to save temporaries

* Factor out elf_parser.read_unique_symbol helper

* Update riscof_kriscv.py to execute tests and dump signature

* Separate the riscof-based architectural tests from the integration tests

* Add sail_cSim as the riscof reference plugin

* Fix description for JALR

* term_builder.py: Add comment to end1 < start2 assertion

* Add comments to rules only included to preserve totality

* Add further documentation to README.md

* Set Version: 0.1.25

---------

Co-authored-by: devops <devops@runtimeverification.com>

.github/actions/with-docker/Dockerfile

@@ -4,6 +4,8 @@ ARG TOOLCHAIN_VERSION
 ARG TOOLCHAIN_VERSION
 FROM runtimeverificationinc/riscv-gnu-toolchain:ubuntu-jammy-${TOOLCHAIN_VERSION} as TOOLCHAIN
 
+FROM registry.gitlab.com/incoresemi/docker-images/compliance:latest as SAIL
+
 ARG K_VERSION
 FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION}
 
@@ -25,7 +27,9 @@ USER user
 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}
+
+COPY --from=SAIL /usr/bin/riscv_sim_RV32 /usr/bin/riscv_sim_RV32
+COPY --from=SAIL /usr/bin/riscv_sim_RV64 /usr/bin/riscv_sim_RV64

.github/workflows/test.yml

@@ -68,6 +68,8 @@ jobs:
         run: docker exec --user user ${CONTAINER} make test-unit
       - name: 'Run integration tests'
         run: docker exec --user user ${CONTAINER} make test-integration
+      - name: 'Run architectural tests'
+        run: docker exec --user user ${CONTAINER} make test-architectural
       - name: 'Tear down Docker'
         if: always()
         run: docker stop --time=0 ${CONTAINER}

Makefile

@@ -41,17 +41,14 @@ test-all: poetry-install
 test-unit: poetry-install
 	$(POETRY_RUN) pytest src/tests/unit --maxfail=1 --verbose $(TEST_ARGS)
 
-test-integration: tests/riscv-arch-test-compiled poetry-install
+test-integration: poetry-install
 	$(POETRY_RUN) pytest src/tests/integration --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
 
-test-simple: poetry-install
-	$(POETRY_RUN) pytest src/tests/integration/test_integration.py --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
+RISCOF_DIRS = $(shell find src/tests/riscof -type d)
+RISCOF_FILES = $(shell find src/tests/riscof -type f)
 
-RISCOF_DIRS = $(shell find src/tests/integration/riscof -type d)
-RISCOF_FILES = $(shell find src/tests/integration/riscof -type f)
-
-tests/riscv-arch-test-compiled: tests/riscv-arch-test $(RISCOF_DIRS) $(RISCOF_FILES)
-	$(POETRY_RUN) riscof run --suite tests/riscv-arch-test/riscv-test-suite --env tests/riscv-arch-test/riscv-test-suite/env --config src/tests/integration/riscof/config.ini --work-dir tests/riscv-arch-test-compiled --no-ref-run
+test-architectural: tests/riscv-arch-test $(RISCOF_DIRS) $(RISCOF_FILES)
+	$(POETRY_RUN) riscof run --suite tests/riscv-arch-test/riscv-test-suite --env tests/riscv-arch-test/riscv-test-suite/env --config src/tests/riscof/config.ini --work-dir tests/riscv-arch-test-compiled --no-browser
 
 # Coverage
 

README.md

@@ -22,6 +22,7 @@ Prerequsites: `python >= 3.10`, `pip >= 20.0.2`, `poetry >= 1.3.2`.
 poetry install
 make kdist-build
 ```
+
 ## Usage
 Execute a compiled RISC-V ELF file with the following command:
 ```bash
@@ -37,5 +38,14 @@ Use `make` to run common tasks (see the [Makefile](Makefile) for a complete list
 * `make format`: Format code
 * `make test-unit`: Run unit tests
 * `make test-integration`: Run integration tests
-
+* `make test-architectural`: Run the RISC-V Architectural Test Suite
 For interactive use, spawn a shell with `poetry shell` (after `poetry install`), then run an interpreter.
+
+### Running Tests
+The integration and architectural tests require the [RISC-V GNU Toolchain](https://github.com/riscv-collab/riscv-gnu-toolchain). During installation, follow instructions to build the Newlib-based cross-compiler. The `riscv64-unknown-elf-*` binaries must be available on your `PATH`.
+
+Prior to running `make test-architectural`, you must also fetch the RISC-V Architectural Test Suite
+```bash
+git submodule update --init --recursive -- tests/riscv-arch-test
+```
+and install the [Sail RISC-V model](https://github.com/riscv/sail-riscv) for use as a reference implementation.

package/version

@@ -1 +1 @@
-0.1.24
+0.1.25

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.24"
+version = "0.1.25"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/kriscv/__main__.py

@@ -6,14 +6,18 @@
 from pathlib import Path
 from typing import TYPE_CHECKING
 
+from elftools.elf.elffile import ELFFile  # type: ignore
+
+from kriscv import elf_parser
 from kriscv.build import semantics
 
 if TYPE_CHECKING:
     from collections.abc import Sequence
 
 
 @dataclass
-class KRISCVOpts: ...
+class KRISCVOpts:
+    temp_dir: Path | None
 
 
 @dataclass
@@ -22,39 +26,116 @@ class RunOpts(KRISCVOpts):
     end_symbol: str | None
 
 
+@dataclass
+class RunArchTestOpts(KRISCVOpts):
+    input_file: Path
+    output_file: Path | None
+
+
 def kriscv(args: Sequence[str]) -> None:
     opts = _parse_args(args)
     match opts:
         case RunOpts():
             _kriscv_run(opts)
+        case RunArchTestOpts():
+            _kriscv_run_arch_test(opts)
         case _:
             raise AssertionError()
 
 
 def _parse_args(args: Sequence[str]) -> KRISCVOpts:
     ns = _arg_parser().parse_args(args)
 
+    if ns.temp_dir is not None:
+        ns.temp_dir = ns.temp_dir.resolve(strict=True)
+
     match ns.command:
         case 'run':
-            return RunOpts(input_file=Path(ns.input_file).resolve(strict=True), end_symbol=ns.end_symbol)
+            return RunOpts(
+                temp_dir=ns.temp_dir,
+                input_file=ns.input_file.resolve(strict=True),
+                end_symbol=ns.end_symbol,
+            )
+        case 'run-arch-test':
+            return RunArchTestOpts(
+                temp_dir=ns.temp_dir,
+                input_file=ns.input_file.resolve(strict=True),
+                output_file=ns.output_file,
+            )
         case _:
             raise AssertionError()
 
 
 def _kriscv_run(opts: RunOpts) -> None:
-    tools = semantics()
+    tools = semantics(temp_dir=opts.temp_dir)
     final_conf = tools.run_elf(opts.input_file, end_symbol=opts.end_symbol)
-    print(tools.kprint.pretty_print(final_conf))
+    print(tools.kprint.pretty_print(final_conf, sort_collections=True))
+
+
+def _kriscv_run_arch_test(opts: RunArchTestOpts) -> None:
+    input = opts.input_file
+    tools = semantics(temp_dir=opts.temp_dir)
+    final_conf = tools.run_elf(input, end_symbol='_halt')
+    memory = tools.get_memory(final_conf)
+
+    with open(input, 'rb') as f:
+        elf = ELFFile(f)
+        begin_sig_addr = elf_parser.read_unique_symbol(elf, 'begin_signature', error_loc=str(input))
+        end_sig_addr = elf_parser.read_unique_symbol(elf, 'end_signature', error_loc=str(input))
+
+    if begin_sig_addr % 4 != 0:
+        raise AssertionError(
+            'Signature region must begin at an XLEN-bit boundary, but begins at address 0x{begin_sig_addr:08X}.'
+        )
+    if (end_sig_addr - begin_sig_addr) % 4 != 0:
+        raise AssertionError(
+            'Signature region must contain a series 32-bit words, but spans addresses 0x{begin_sig_addr:08X}-0x{end_sig_addr:08X}.'
+        )
+
+    def _addr_to_hex(addr: int) -> str:
+        if addr not in memory:
+            return '--'
+        byte = memory[addr]
+        assert 0 <= byte <= 0xFF
+        return f'{byte:02x}'
+
+    merged_sig = [_addr_to_hex(addr) for addr in range(begin_sig_addr, end_sig_addr)]
+    signature = [''.join(reversed(merged_sig[i : i + 4])) for i in range(0, len(merged_sig), 4)]
+
+    if opts.output_file is None:
+        for word in signature:
+            print(word)
+        return
+
+    with open(opts.output_file, 'w') as out:
+        for word in signature:
+            out.write(word + '\n')
 
 
 def _arg_parser() -> ArgumentParser:
     parser = ArgumentParser(prog='kriscv')
 
     command_parser = parser.add_subparsers(dest='command', required=True)
 
-    run_parser = command_parser.add_parser('run', help='execute RISC-V ELF files programs')
-    run_parser.add_argument('input_file', metavar='FILE', help='RISC-V ELF file to run')
-    run_parser.add_argument('--end-symbol', type=str, help='Symbol marking the address which terminates execution')
+    common_parser = ArgumentParser(add_help=False)
+    common_parser.add_argument('--temp-dir', type=Path, help='directory where temporary files should be saved')
+
+    run_parser = command_parser.add_parser('run', help='execute a RISC-V ELF file', parents=[common_parser])
+    run_parser.add_argument('input_file', type=Path, metavar='FILE', help='RISC-V ELF file to run')
+    run_parser.add_argument('--end-symbol', type=str, help='symbol marking the address which terminates execution')
+
+    run_arch_test_parser = command_parser.add_parser(
+        'run-arch-test',
+        help='execute a RISC-V Architectural Test ELF file and dump the test signature',
+        parents=[common_parser],
+    )
+    run_arch_test_parser.add_argument(
+        'input_file', type=Path, metavar='FILE', help='RISC-V Architectural Test ELF file to run'
+    )
+    run_arch_test_parser.add_argument(
+        '-o', '--output', dest='output_file', type=Path, help='output file for the test signature'
+    )
+
     return parser
 
 

src/kriscv/build.py

@@ -8,12 +8,13 @@
 from .tools import Tools
 
 if TYPE_CHECKING:
+    from pathlib import Path
     from typing import Final
 
 importer.import_kllvm(kdist.get('riscv-semantics.kllvm'))
 
 runtime: Final = importer.import_runtime(kdist.get('riscv-semantics.kllvm-runtime'))
 
 
-def semantics() -> Tools:
-    return Tools(definition_dir=kdist.get('riscv-semantics.llvm'), runtime=runtime)
+def semantics(*, temp_dir: Path | None = None) -> Tools:
+    return Tools(definition_dir=kdist.get('riscv-semantics.llvm'), runtime=runtime, temp_dir=temp_dir)

src/kriscv/elf_parser.py

@@ -2,40 +2,43 @@
 
 from typing import TYPE_CHECKING
 
-from pyk.prelude.collections import map_of
-from pyk.prelude.kint import intToken
-
-from kriscv.term_builder import word
+from kriscv.term_builder import sparse_bytes, word
 
 if TYPE_CHECKING:
     from elftools.elf.elffile import ELFFile  # type: ignore
     from pyk.kast.inner import KInner
 
 
-def _memory_segments(elf: ELFFile) -> dict[tuple[int, int], bytes]:
-    segments: dict[tuple[int, int], bytes] = {}
+def _memory_segments(elf: ELFFile) -> dict[int, bytes]:
+    segments: dict[int, bytes] = {}
     for seg in elf.iter_segments():
         if seg['p_type'] == 'PT_LOAD':
             start = seg['p_vaddr']
             file_size = seg['p_filesz']
-            data = seg.data() + b'\0' * (seg['p_memsz'] - file_size)
-            segments[(start, start + file_size)] = data
+            mem_size = seg['p_memsz']
+            data = seg.data() + b'\0' * (mem_size - file_size)
+            segments[start] = data
     return segments
 
 
-def memory_map(elf: ELFFile) -> KInner:
-    mem_map: dict[KInner, KInner] = {}
-    for addr_range, data in _memory_segments(elf).items():
-        start, end = addr_range
-        for addr in range(start, end):
-            mem_map[word(addr)] = intToken(data[addr - start])
-    return map_of(mem_map)
+def memory(elf: ELFFile) -> KInner:
+    return sparse_bytes(_memory_segments(elf))
 
 
 def entry_point(elf: ELFFile) -> KInner:
     return word(elf.header['e_entry'])
 
 
+def read_unique_symbol(elf: ELFFile, symbol: str, *, error_loc: str | None) -> int:
+    values = read_symbol(elf, symbol)
+    error_loc = error_loc if error_loc else ''
+    if len(values) == 0:
+        raise AssertionError(f'{error_loc}: Cannot find symbol {symbol!r}.')
+    if len(values) > 1:
+        raise AssertionError(f'{error_loc}: Symbol {symbol!r} should be unique, but found multiple instances.')
+    return values[0]
+
+
 def read_symbol(elf: ELFFile, symbol: str) -> list[int]:
     symtab = elf.get_section_by_name('.symtab')
     if symtab is None:

src/kriscv/kdist/riscv-semantics/riscv.md

@@ -15,13 +15,15 @@ The `<test>` section currently contains on a single cell:
 ```k
 requires "riscv-disassemble.md"
 requires "riscv-instructions.md"
+requires "sparse-bytes.md"
 requires "word.md"
 
 module RISCV-CONFIGURATION
   imports BOOL
   imports INT
   imports MAP
   imports RANGEMAP
+  imports SPARSE-BYTES
   imports WORD
 
   syntax KItem ::= "#EXECUTE"
@@ -31,7 +33,7 @@ module RISCV-CONFIGURATION
       <instrs> #EXECUTE ~> .K </instrs>
       <regs> .Map </regs> // Map{Register, Word}
       <pc> $PC:Word </pc>
-      <mem> $MEM:Map </mem> // Map{Word, Int}
+      <mem> $MEM:SparseBytes </mem>
     </riscv>
     <test>
       <haltCond> $HALT:HaltCondition </haltCond>
@@ -95,28 +97,30 @@ module RISCV-MEMORY
   imports RISCV-DISASSEMBLE
   imports RISCV-INSTRUCTIONS
   imports WORD
+
+  syntax Memory = SparseBytes
 ```
 We abstract the particular memory representation behind `loadByte` and `storeByte` functions.
 ```k
-  syntax Int ::= loadByte(memory: Map, address: Word) [function]
-  rule loadByte(MEM, ADDR) => { MEM[ADDR] } :>Int
+  syntax Int ::= loadByte(memory: Memory, address: Word) [function, symbol(Memory:loadByte)]
+  rule loadByte(MEM, W(ADDR)) => { readByte(MEM, ADDR) }:>Int
 
-  syntax Map ::= storeByte(memory: Map, address: Word, byte: Int) [function, total]
-  rule storeByte(MEM, ADDR, B) => MEM[ADDR <- B]
+  syntax Memory ::= storeByte(memory: Memory, address: Word, byte: Int) [function, total, symbol(Memory:storeByte)]
+  rule storeByte(MEM, W(ADDR), B) => writeByte(MEM, ADDR, B)
 ```
 For multi-byte loads and stores, we presume a little-endian architecture.
 ```k
-  syntax Int ::= loadBytes(memory: Map, address: Word, numBytes: Int) [function]
+  syntax Int ::= loadBytes(memory: Memory, address: Word, numBytes: Int) [function]
   rule loadBytes(MEM, ADDR, 1  ) => loadByte(MEM, ADDR)
   rule loadBytes(MEM, ADDR, NUM) => (loadBytes(MEM, ADDR +Word W(1), NUM -Int 1) <<Int 8) |Int loadByte(MEM, ADDR) requires NUM >Int 1
 
-  syntax Map ::= storeBytes(memory: Map, address: Word, bytes: Int, numBytes: Int) [function]
+  syntax Memory ::= storeBytes(memory: Memory, address: Word, bytes: Int, numBytes: Int) [function]
   rule storeBytes(MEM, ADDR, BS, 1  ) => storeByte(MEM, ADDR, BS)
   rule storeBytes(MEM, ADDR, BS, NUM) => storeBytes(storeByte(MEM, ADDR, BS &Int 255), ADDR +Word W(1), BS >>Int 8, NUM -Int 1) requires NUM >Int 1
 ```
 Instructions are always 32-bits, and are stored in little-endian format regardless of the endianness of the overall architecture.
 ```k
-  syntax Instruction ::= fetchInstr(memory: Map, address: Word) [function]
+  syntax Instruction ::= fetchInstr(memory: Memory, address: Word) [function]
   rule fetchInstr(MEM, ADDR) =>
     disassemble((loadByte(MEM, ADDR +Word W(3)) <<Int 24) |Int
                 (loadByte(MEM, ADDR +Word W(2)) <<Int 16) |Int
@@ -266,11 +270,11 @@ The following instructions behave analogously to their `I`-suffixed counterparts
        <regs> REGS => writeReg(REGS, RD, PC +Word W(4)) </regs>
        <pc> PC => PC +Word chop(OFFSET) </pc>
 ```
-`JALR` stores `PC + 4` in `RD`, increments `PC` by the value in register `RS1` plus `OFFSET`, then sets the least-significant bit of this new `PC` to `0`.
+`JALR` stores `PC + 4` in `RD`, sets `PC` to the value in register `RS1` plus `OFFSET`, then sets the least-significant bit of this new `PC` to `0`.
 ```k
   rule <instrs> JALR RD, OFFSET ( RS1 ) => .K ...</instrs>
        <regs> REGS => writeReg(REGS, RD, PC +Word W(4)) </regs>
-       <pc> PC => (PC +Word (readReg(REGS, RS1) +Word chop(OFFSET))) &Word chop(-1 <<Int 1) </pc>
+       <pc> PC => (readReg(REGS, RS1) +Word chop(OFFSET)) &Word chop(-1 <<Int 1) </pc>
 ```
 `BEQ` increments `PC` by `OFFSET` so long as the values in registers `RS1` and `RS2` are equal. Otherwise, `PC` is incremented by `4`.
 ```k