From 8a8b81c91631ad9b3cc920905277abfb33013eac Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Wed, 14 Aug 2024 23:44:20 -0700 Subject: [PATCH] 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 --- .github/actions/with-docker/Dockerfile | 6 +- .github/workflows/test.yml | 2 + Makefile | 13 +- README.md | 12 +- package/version | 2 +- pyproject.toml | 2 +- src/kriscv/__main__.py | 95 +++++++++++++- src/kriscv/build.py | 5 +- src/kriscv/elf_parser.py | 33 ++--- src/kriscv/kdist/riscv-semantics/riscv.md | 24 ++-- .../kdist/riscv-semantics/sparse-bytes.md | 99 ++++++++++++++ src/kriscv/kdist/riscv-semantics/word.md | 1 - src/kriscv/term_builder.py | 71 +++++++++- src/kriscv/term_manip.py | 69 +++++++++- src/kriscv/tools.py | 29 ++--- src/tests/integration/riscof/config.ini | 11 -- src/tests/integration/test_conformance.py | 62 --------- src/tests/integration/test_integration.py | 6 +- src/tests/{integration => }/riscof/README.md | 18 ++- src/tests/riscof/config.ini | 14 ++ .../riscof/kriscv/env/link.ld | 0 src/tests/riscof/kriscv/env/model_test.h | 52 ++++++++ .../riscof/kriscv/kriscv_isa.yaml | 0 .../riscof/kriscv/kriscv_platform.yaml | 0 .../riscof/kriscv/riscof_kriscv.py | 22 ++-- src/tests/riscof/sail_cSim/__init__.py | 3 + src/tests/riscof/sail_cSim/env/link.ld | 18 +++ .../sail_cSim}/env/model_test.h | 27 ++-- .../riscof/sail_cSim/riscof_sail_cSim.py | 122 ++++++++++++++++++ src/tests/riscof/sail_cSim/sail_isa.yaml | 38 ++++++ src/tests/riscof/sail_cSim/sail_platform.yaml | 4 + src/tests/unit/test_unit.py | 87 ++++++++++++- tests/simple/jalr.S | 33 +++-- 33 files changed, 779 insertions(+), 201 deletions(-) create mode 100644 src/kriscv/kdist/riscv-semantics/sparse-bytes.md delete mode 100644 src/tests/integration/riscof/config.ini delete mode 100644 src/tests/integration/test_conformance.py rename src/tests/{integration => }/riscof/README.md (61%) create mode 100644 src/tests/riscof/config.ini rename src/tests/{integration => }/riscof/kriscv/env/link.ld (100%) create mode 100644 src/tests/riscof/kriscv/env/model_test.h rename src/tests/{integration => }/riscof/kriscv/kriscv_isa.yaml (100%) rename src/tests/{integration => }/riscof/kriscv/kriscv_platform.yaml (100%) rename src/tests/{integration => }/riscof/kriscv/riscof_kriscv.py (88%) create mode 100644 src/tests/riscof/sail_cSim/__init__.py create mode 100644 src/tests/riscof/sail_cSim/env/link.ld rename src/tests/{integration/riscof/kriscv => riscof/sail_cSim}/env/model_test.h (71%) create mode 100644 src/tests/riscof/sail_cSim/riscof_sail_cSim.py create mode 100644 src/tests/riscof/sail_cSim/sail_isa.yaml create mode 100644 src/tests/riscof/sail_cSim/sail_platform.yaml diff --git a/.github/actions/with-docker/Dockerfile b/.github/actions/with-docker/Dockerfile index 264d7581..084eeffc 100644 --- a/.github/actions/with-docker/Dockerfile +++ b/.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 diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 0011cfc2..e670c78f 100644 --- a/.github/workflows/test.yml +++ b/.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} diff --git a/Makefile b/Makefile index 8a054d17..22c69b91 100644 --- a/Makefile +++ b/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 diff --git a/README.md b/README.md index a9d1e46c..9a436450 100644 --- a/README.md +++ b/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. diff --git a/package/version b/package/version index 5a48b6be..0e7400f1 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.24 +0.1.25 diff --git a/pyproject.toml b/pyproject.toml index 21959587..77aa5918 100644 --- a/pyproject.toml +++ b/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. ", diff --git a/src/kriscv/__main__.py b/src/kriscv/__main__.py index 870a5aa2..6577b35e 100644 --- a/src/kriscv/__main__.py +++ b/src/kriscv/__main__.py @@ -6,6 +6,9 @@ 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: @@ -13,7 +16,8 @@ @dataclass -class KRISCVOpts: ... +class KRISCVOpts: + temp_dir: Path | None @dataclass @@ -22,11 +26,19 @@ 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() @@ -34,17 +46,70 @@ def kriscv(args: Sequence[str]) -> None: 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: @@ -52,9 +117,25 @@ def _arg_parser() -> ArgumentParser: 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 diff --git a/src/kriscv/build.py b/src/kriscv/build.py index 6c2d5a5e..6fbeb42b 100644 --- a/src/kriscv/build.py +++ b/src/kriscv/build.py @@ -8,6 +8,7 @@ from .tools import Tools if TYPE_CHECKING: + from pathlib import Path from typing import Final importer.import_kllvm(kdist.get('riscv-semantics.kllvm')) @@ -15,5 +16,5 @@ 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) diff --git a/src/kriscv/elf_parser.py b/src/kriscv/elf_parser.py index 4392bab5..71756515 100644 --- a/src/kriscv/elf_parser.py +++ b/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: diff --git a/src/kriscv/kdist/riscv-semantics/riscv.md b/src/kriscv/kdist/riscv-semantics/riscv.md index 38241cb4..d18ac3ce 100644 --- a/src/kriscv/kdist/riscv-semantics/riscv.md +++ b/src/kriscv/kdist/riscv-semantics/riscv.md @@ -15,6 +15,7 @@ The `` 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 @@ -22,6 +23,7 @@ module RISCV-CONFIGURATION imports INT imports MAP imports RANGEMAP + imports SPARSE-BYTES imports WORD syntax KItem ::= "#EXECUTE" @@ -31,7 +33,7 @@ module RISCV-CONFIGURATION #EXECUTE ~> .K .Map // Map{Register, Word} $PC:Word - $MEM:Map // Map{Word, Int} + $MEM:SparseBytes $HALT:HaltCondition @@ -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 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)) < REGS => writeReg(REGS, RD, PC +Word W(4)) PC => PC +Word chop(OFFSET) ``` -`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 JALR RD, OFFSET ( RS1 ) => .K ... REGS => writeReg(REGS, RD, PC +Word W(4)) - PC => (PC +Word (readReg(REGS, RS1) +Word chop(OFFSET))) &Word chop(-1 < + PC => (readReg(REGS, RS1) +Word chop(OFFSET)) &Word chop(-1 < ``` `BEQ` increments `PC` by `OFFSET` so long as the values in registers `RS1` and `RS2` are equal. Otherwise, `PC` is incremented by `4`. ```k diff --git a/src/kriscv/kdist/riscv-semantics/sparse-bytes.md b/src/kriscv/kdist/riscv-semantics/sparse-bytes.md new file mode 100644 index 00000000..d0daafe5 --- /dev/null +++ b/src/kriscv/kdist/riscv-semantics/sparse-bytes.md @@ -0,0 +1,99 @@ +# Sparse Bytes Datatype +In this file, we define a `SparseBytes` datatype representing a byte array with large segments of uninitialized data, optimized for space efficiency. +```k +module SPARSE-BYTES + imports BOOL + imports BYTES + imports INT +``` +Concretely, a `SparseBytes` value is a list of items +```k + syntax BytesSBItem ::= #bytes(Bytes) [symbol(SparseBytes:#bytes)] + syntax EmptySBItem ::= #empty(Int) [symbol(SparseBytes:#empty)] +``` +where `#bytes(B)` represents a contiguous segment of initialized data `B:Bytes` and `#empty(N)` represents a contiguous segment of uninitialized data `N` bytes wide. + +We define `SparseBytes` in terms of two mutually recursive sorts: +-`SparseBytesEF`, representing a `SparseBytes` value which is either completely empty (`.SparseBytes`) or begins with an `#empty(_)` entry +-`SparseBytesBF`, representing a `SparseBytes` value which begins with a `#bytes(_)` entry + +Structuring `SparseBytes` in this way forces entries to always alternate between `#empty(_)` and `#bytes(_)`, i.e., ensuring contiguous uninitialized regions are packed together and contiguous initialized regions are packed together. As a result, many functions over `SparseBytes` are naturally implemented as mutually recursive functions over `SparseBytesEF` and `SparseBytesBF`. +```k + syntax SparseBytes ::= + SparseBytesEF + | SparseBytesBF + + // SparseBytes with a leading EmptySBItem (EF = Empty First) + syntax SparseBytesEF ::= + ".SparseBytes" [symbol(.SparseBytes)] + | EmptySBItem SparseBytesBF [symbol(SparseBytes:EmptyCons)] + + // SparseBytes with a leading BytesSBItem (BF = Bytes First) + syntax SparseBytesBF ::= + BytesSBItem SparseBytesEF [symbol(SparseBytes:BytesCons)] +``` +We provide helpers to prepend either data or an empty region to an existing `SparseBytes`. Note that `prepend` has worst-case time complexity `O(B + BS)` where `B` is the length of the prepended data and `BS` is the length of initialized data at the start of the list. +```k + syntax SparseBytesBF ::= prepend(Bytes, SparseBytes) [function, total] + rule prepend(B, EF:SparseBytesEF) => #bytes(B) EF + rule prepend(B, #bytes(BS) EF ) => #bytes(B +Bytes BS) EF +``` +`prependEmpty` has `O(1)` time complexity. +```k + syntax SparseBytes ::= prependEmpty(Int, SparseBytes) [function, total] + rule prependEmpty(I, _ ) => .SparseBytes requires I SBS requires I ==Int 0 + rule prependEmpty(I, .SparseBytes ) => .SparseBytes requires I >Int 0 + rule prependEmpty(I, #empty(N) BF ) => #empty(I +Int N) BF requires I >Int 0 + rule prependEmpty(I, BF:SparseBytesBF) => #empty(I) BF requires I >Int 0 +``` +`readByte` reads a single byte from a given index in `O(E)` time, where `E` is the number of `#empty(_)` or `#bytes(_)` entries in the list up to the location of the index. The result is either +- an `Int` in the range `[0, 255)` giving the byte value at the index, or +- `.Byte` if the index does not point to initialized data +```k + syntax MaybeByte ::= + Int + | ".Byte" + + syntax MaybeByte ::= + readByte (SparseBytes , Int) [function, total] + | readByteEF(SparseBytesEF, Int) [function, total] + | readByteBF(SparseBytesBF, Int) [function, total] + + rule readByte(EF:SparseBytesEF, I) => readByteEF(EF, I) + rule readByte(BF:SparseBytesBF, I) => readByteBF(BF, I) + + rule readByteEF(.SparseBytes, _) => .Byte + rule readByteEF(#empty(N) _ , I) => .Byte requires I readByteBF(BF, I -Int N) requires I >=Int N + + rule readByteBF(#bytes(_) _ , I) => .Byte requires I B[ I ] requires I >=Int 0 andBool I readByteEF(EF, I -Int lengthBytes(B)) + requires I >=Int lengthBytes(B) +``` +`writeByte` writes a single byte to a given index. With regards to time complexity, +- If the index is in the middle of an existing `#empty(_)` or `#bytes(_)` region, time complexity is `O(E)` where `E` is the number of entries up to the index. +- If the index happens to be the first or last index in an `#empty(_)` region directly boarding a `#bytes(_)` region, then the `#bytes(_)` region must be re-allocated to append the new value, giving worst-case `O(E + B)` time, where `E` is the number of entries up to the location of the index and `B` is the size of this existing `#bytes(_)`. +```k + syntax SparseBytes ::= + writeByte (SparseBytes , Int, Int) [function, total] + | writeByteEF(SparseBytesEF, Int, Int) [function, total] + | writeByteBF(SparseBytesBF, Int, Int) [function, total] + + rule writeByte(BF:SparseBytesBF, I, V) => writeByteBF(BF, I, V) + rule writeByte(EF:SparseBytesEF, I, V) => writeByteEF(EF, I, V) + + rule writeByteEF(_ , I, _) => .SparseBytes requires I #bytes(Int2Bytes(1, V, BE)) .SparseBytes requires I ==Int 0 + rule writeByteEF(.SparseBytes, I, V) => #empty(I) #bytes(Int2Bytes(1, V, BE)) .SparseBytes requires I >Int 0 + rule writeByteEF(#empty(N) BF, I, V) => prependEmpty(I, prepend(Int2Bytes(1, V, BE), prependEmpty((N -Int I) -Int 1, BF))) + requires I >=Int 0 andBool I prependEmpty(N, writeByteBF(BF, I -Int N, V)) requires I >=Int N + + rule writeByteBF(_ , I, _) => .SparseBytes requires I #bytes(B[ I <- V ]) EF requires I >=Int 0 andBool I prepend(B, writeByteEF(EF, I -Int lengthBytes(B), V)) + requires I >=Int lengthBytes(B) +endmodule +``` diff --git a/src/kriscv/kdist/riscv-semantics/word.md b/src/kriscv/kdist/riscv-semantics/word.md index df562126..cbaf15d0 100644 --- a/src/kriscv/kdist/riscv-semantics/word.md +++ b/src/kriscv/kdist/riscv-semantics/word.md @@ -1,5 +1,4 @@ # `XLEN`-bit Word Datatype - In this file, we define a `Word` datatype representing a sequence of `XLEN` bits, where `XLEN=32` for `RV32*` ISAs and `XLEN=64` for `RV64*` ISAs. ```k module WORD diff --git a/src/kriscv/term_builder.py b/src/kriscv/term_builder.py index 0b63443a..120a45cb 100644 --- a/src/kriscv/term_builder.py +++ b/src/kriscv/term_builder.py @@ -1,10 +1,14 @@ from __future__ import annotations -from typing import TYPE_CHECKING +import itertools +from typing import TYPE_CHECKING, cast from pyk.kast.inner import KApply, KInner, KSort +from pyk.prelude.bytes import bytesToken from pyk.prelude.kint import intToken +from kriscv.term_manip import normalize_memory + if TYPE_CHECKING: from collections.abc import Iterable from typing import TypeVar @@ -240,3 +244,68 @@ def word(bits: KInner | int | str | bytes) -> KInner: case bytes(): val = intToken(int.from_bytes(bits, 'big', signed=False)) return KApply('W', val) + + +def dot_sb() -> KInner: + return KApply('.SparseBytes') + + +def sb_empty(count: KInner) -> KInner: + return KApply('SparseBytes:#empty', count) + + +def sb_bytes(bs: KInner) -> KInner: + return KApply('SparseBytes:#bytes', bs) + + +def sb_empty_cons(empty: KInner, rest_bf: KInner) -> KInner: + return KApply('SparseBytes:EmptyCons', empty, rest_bf) + + +def sb_bytes_cons(bs: KInner, rest_ef: KInner) -> KInner: + return KApply('SparseBytes:BytesCons', bs, rest_ef) + + +def sparse_bytes(data: dict[int, bytes]) -> KInner: + clean_data: list[tuple[int, bytes]] = sorted(normalize_memory(data).items()) + + if len(clean_data) == 0: + return dot_sb() + + # Collect all empty gaps between segements + gaps = [] + start = clean_data[0][0] + if start != 0: + gaps.append((0, start)) + for (start1, val1), (start2, _) in itertools.pairwise(clean_data): + end1 = start1 + len(val1) + # normalize_memory should already have merged consecutive segments + assert end1 < start2 + gaps.append((end1, start2 - end1)) + + # Merge segments and gaps into a list of sparse bytes items + sparse_data: list[tuple[int, int | bytes]] = sorted( + cast('list[tuple[int, int | bytes]]', clean_data) + cast('list[tuple[int, int | bytes]]', gaps), reverse=True + ) + + sparse_k = dot_sb() + for _, gap_or_val in sparse_data: + if isinstance(gap_or_val, int): + sparse_k = sb_empty_cons(sb_empty(intToken(gap_or_val)), sparse_k) + elif isinstance(gap_or_val, bytes): + sparse_k = sb_bytes_cons(sb_bytes(bytesToken(gap_or_val)), sparse_k) + else: + raise AssertionError() + return sparse_k + + +def sort_memory() -> KSort: + return KSort('SparseBytes') + + +def load_byte(mem: KInner, addr: KInner) -> KInner: + return KApply('Memory:loadByte', mem, addr) + + +def store_byte(mem: KInner, addr: KInner, value: KInner) -> KInner: + return KApply('Memory:storeByte', mem, addr, value) diff --git a/src/kriscv/term_manip.py b/src/kriscv/term_manip.py index 7e2dbbb7..596b8c1d 100644 --- a/src/kriscv/term_manip.py +++ b/src/kriscv/term_manip.py @@ -2,8 +2,8 @@ from typing import TYPE_CHECKING -from pyk.kore.match import kore_int, match_app, match_symbol -from pyk.kore.syntax import App +from pyk.kore.match import kore_bytes, kore_int, match_app, match_symbol +from pyk.kore.syntax import App, SortApp if TYPE_CHECKING: from pyk.kore.syntax import Pattern @@ -34,3 +34,68 @@ def match_map(pattern: Pattern) -> tuple[tuple[Pattern, Pattern], ...]: match_symbol(app.symbol, cons_symbol) return match_map(app.args[0]) + match_map(app.args[1]) + + +def match_sparse_bytes(pattern: Pattern) -> tuple[Pattern, ...]: + app = match_app(pattern) + if app.symbol == 'inj' and ( + app.sorts == (SortApp('SortSparseBytesEF'), SortApp('SortSparseBytes')) + or app.sorts == (SortApp('SortSparseBytesBF'), SortApp('SortSparseBytes')) + ): + app = match_app(app.args[0]) + if app.symbol == "LblSparseBytes'Coln'EmptyCons" or app.symbol == "LblSparseBytes'Coln'BytesCons": + return (app.args[0],) + match_sparse_bytes(app.args[1]) + match_symbol(app.symbol, "Lbl'Stop'SparseBytes") + return () + + +def kore_sb_empty(empty: Pattern) -> int: + return kore_int(match_app(empty, "LblSparseBytes'ColnHash'empty").args[0]) + + +def kore_sb_bytes(bs: Pattern) -> bytes: + return kore_bytes(match_app(bs, "LblSparseBytes'ColnHash'bytes").args[0]) + + +def kore_sparse_bytes(sb: Pattern) -> dict[int, bytes]: + sparse_items: list[int | bytes] = [] + is_bytes = True + for sb_item in reversed(match_sparse_bytes(sb)): + if is_bytes: + sparse_items.append(kore_sb_bytes(sb_item)) + else: + sparse_items.append(kore_sb_empty(sb_item)) + is_bytes = not is_bytes + + sparse_dict = {} + addr = 0 + for gap_or_val in reversed(sparse_items): + if isinstance(gap_or_val, int): + addr += gap_or_val + elif isinstance(gap_or_val, bytes): + sparse_dict[addr] = gap_or_val + addr += len(gap_or_val) + else: + raise AssertionError() + return sparse_dict + + +def normalize_memory(memory: dict[int, bytes]) -> dict[int, bytes]: + # normalize sparse bytes data by merging contiguous segments + raw_memory = sorted(memory.items()) + merged_memory: dict[int, bytes] = {} + seg_idx = 0 + while seg_idx < len(raw_memory): + start, val = raw_memory[seg_idx] + seg_idx += 1 + while seg_idx < len(raw_memory): + start_next, val_next = raw_memory[seg_idx] + end_curr = start + len(val) + assert end_curr <= start_next + if end_curr == start_next: + val += val_next + seg_idx += 1 + else: + break + merged_memory[start] = val + return merged_memory diff --git a/src/kriscv/tools.py b/src/kriscv/tools.py index f250cd9e..1759d5a9 100644 --- a/src/kriscv/tools.py +++ b/src/kriscv/tools.py @@ -10,7 +10,7 @@ from pyk.prelude.k import GENERATED_TOP_CELL from kriscv import elf_parser, term_builder -from kriscv.term_manip import kore_word, match_map +from kriscv.term_manip import kore_sparse_bytes, kore_word, match_map if TYPE_CHECKING: from pathlib import Path @@ -24,12 +24,8 @@ class Tools: __krun: KRun __runtime: Runtime - def __init__( - self, - definition_dir: Path, - runtime: Runtime, - ) -> None: - self.__krun = KRun(definition_dir) + def __init__(self, definition_dir: Path, runtime: Runtime, *, temp_dir: Path | None = None) -> None: + self.__krun = KRun(definition_dir, use_directory=temp_dir) self.__runtime = runtime @property @@ -57,18 +53,12 @@ def run_elf(self, elf_file: Path, *, end_symbol: str | None = None) -> KInner: with open(elf_file, 'rb') as f: elf = ELFFile(f) if end_symbol is not None: - end_values = elf_parser.read_symbol(elf, end_symbol) - if len(end_values) == 0: - raise AssertionError(f'Cannot find end symbol {end_symbol!r}: {elf_file}') - if len(end_values) > 1: - raise AssertionError( - f'End symbol {end_symbol!r} should be unique, but found multiple instances: {elf_file}' - ) - halt_cond = term_builder.halt_at_address(term_builder.word(end_values[0])) + end_addr = elf_parser.read_unique_symbol(elf, end_symbol, error_loc=str(elf_file)) + halt_cond = term_builder.halt_at_address(term_builder.word(end_addr)) else: halt_cond = term_builder.halt_never() config_vars = { - '$MEM': elf_parser.memory_map(elf), + '$MEM': elf_parser.memory(elf), '$PC': elf_parser.entry_point(elf), '$HALT': halt_cond, } @@ -86,8 +76,9 @@ def get_registers(self, config: KInner) -> dict[int, int]: def get_memory(self, config: KInner) -> dict[int, int]: _, cells = split_config_from(config) - mem_kore = self.krun.kast_to_kore(cells['MEM_CELL'], sort=KSort('Map')) + mem_kore = self.krun.kast_to_kore(cells['MEM_CELL'], sort=KSort('SparseBytes')) mem = {} - for addr, val in match_map(mem_kore): - mem[kore_word(addr)] = kore_int(val) + for addr, data in kore_sparse_bytes(mem_kore).items(): + for idx, val in enumerate(data): + mem[addr + idx] = val return mem diff --git a/src/tests/integration/riscof/config.ini b/src/tests/integration/riscof/config.ini deleted file mode 100644 index 7b124715..00000000 --- a/src/tests/integration/riscof/config.ini +++ /dev/null @@ -1,11 +0,0 @@ -[RISCOF] -ReferencePlugin=kriscv -ReferencePluginPath=src/tests/integration/riscof/kriscv -DUTPlugin=kriscv -DUTPluginPath=src/tests/integration/riscof/kriscv - -[kriscv] -pluginpath=src/tests/integration/riscof/kriscv -ispec=src/tests/integration/riscof/kriscv/kriscv_isa.yaml -pspec=src/tests/integration/riscof/kriscv/kriscv_platform.yaml -target_run=0 diff --git a/src/tests/integration/test_conformance.py b/src/tests/integration/test_conformance.py deleted file mode 100644 index 9512d8c5..00000000 --- a/src/tests/integration/test_conformance.py +++ /dev/null @@ -1,62 +0,0 @@ -from __future__ import annotations - -import logging -from pathlib import Path -from typing import TYPE_CHECKING - -import pytest -import yaml - -from ..utils import FAILING_TESTS, 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 = Path(__file__).parent / 'riscof' - -ARCH_SUITE_DIR: Final = REPO_ROOT / 'tests' / 'riscv-arch-test' / 'riscv-test-suite' -ARCH_TEST_COMPILED_DIR: Final = REPO_ROOT / 'tests' / 'riscv-arch-test-compiled' -TEST_LIST: Final = ARCH_TEST_COMPILED_DIR / 'test_list.yaml' -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 FAILING_TESTS) -REST_ARCH_TESTS: Final = tuple(test for test in ALL_ARCH_TESTS if test['test_path'] in FAILING_TESTS) - - -def _test(test_dir: Path, name: str, isa: str) -> None: - asm = test_dir / f'{name}.s' - elf = test_dir / f'{name}.elf' - disass = test_dir / f'{name}.disass' - - assert asm.exists() - assert elf.exists() - assert disass.exists() - - -@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: - _test( - Path(test_entry['work_dir']) / 'dut', - Path(test_entry['test_path']).relative_to(ARCH_SUITE_DIR).stem, - test_entry['isa'].lower(), - ) - - -@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: - _test( - Path(test_entry['work_dir']) / 'dut', - Path(test_entry['test_path']).relative_to(ARCH_SUITE_DIR).stem, - test_entry['isa'].lower(), - ) diff --git a/src/tests/integration/test_integration.py b/src/tests/integration/test_integration.py index 54ee72e5..c03062bb 100644 --- a/src/tests/integration/test_integration.py +++ b/src/tests/integration/test_integration.py @@ -16,6 +16,7 @@ if TYPE_CHECKING: from typing import Final + from kriscv.tools import Tools SIMPLE_DIR: Final = TESTS_DIR / 'simple' SIMPLE_TESTS: Final = tuple(asm_file for asm_file in SIMPLE_DIR.rglob('*.S')) @@ -75,8 +76,7 @@ def _check_mem_entry(assert_file: Path, mem_symbol: int, memory: dict[int, int], raise AssertionError(err_msg.format(reason=f'found {actual} (0x{actual:02X})')) -def _test_simple(elf_file: Path, assert_file: Path, final_config_output: Path | None) -> None: - tools = semantics() +def _test_simple(tools: Tools, elf_file: Path, assert_file: Path, final_config_output: Path | None) -> None: final_config = tools.run_elf(elf_file, end_symbol='_halt') if final_config_output is not None: @@ -152,4 +152,4 @@ def test_simple(asm_file: Path, save_final_config: bool, temp_dir: Path) -> None assert elf_file.exists() assert_file = Path(str(asm_file) + '.assert') final_config_output = (Path(temp_dir) / (asm_file.name + '.out')) if save_final_config else None - _test_simple(elf_file, assert_file, final_config_output) + _test_simple(semantics(temp_dir=temp_dir), elf_file, assert_file, final_config_output) diff --git a/src/tests/integration/riscof/README.md b/src/tests/riscof/README.md similarity index 61% rename from src/tests/integration/riscof/README.md rename to src/tests/riscof/README.md index 48092f15..ce3488fd 100644 --- a/src/tests/integration/riscof/README.md +++ b/src/tests/riscof/README.md @@ -3,13 +3,13 @@ This directory contains the configuration for the `riscof` tool used to execute ## Contents ### 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. +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 +The [DUT (Design Under Test) plugin](https://riscof.readthedocs.io/en/1.24.0/plugins.html) which builds and executes the test suite for our RISC-V implementation. Consists of - env - link.ld - - Linker script used when compiling each test. + - Linker script used when compiling each test. - Unmodified from the riscof model template. - model_test.h - Definition of macros used in the test suite. @@ -19,12 +19,10 @@ The [DUT plugin](https://riscof.readthedocs.io/en/1.24.0/plugins.html) for our R - 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 only supports compiling but not executing the tests. + - The actual plugin implementation for initializing, building, and running the test suite with riscof. -## 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. +### sail_cSim +The [reference plugin](https://riscof.readthedocs.io/en/1.24.0/plugins.html) against which our RISC-V implementation is compared. Both plugins execute the test suite, then the results are compared by `riscof`. Based on [https://gitlab.com/incoresemi/riscof-plugins/-/tree/master/sail_cSim](https://gitlab.com/incoresemi/riscof-plugins/-/tree/master/sail_cSim). -### riscof -The full riscof DUT plugin is still under construction, so execution with riscof is currently unsupported. +## Running the Tests +Execute the tests with `make test-architectural`. diff --git a/src/tests/riscof/config.ini b/src/tests/riscof/config.ini new file mode 100644 index 00000000..4461d629 --- /dev/null +++ b/src/tests/riscof/config.ini @@ -0,0 +1,14 @@ +[RISCOF] +ReferencePlugin=sail_cSim +ReferencePluginPath=src/tests/riscof/sail_cSim +DUTPlugin=kriscv +DUTPluginPath=src/tests/riscof/kriscv + +[kriscv] +pluginpath=src/tests/riscof/kriscv +ispec=src/tests/riscof/kriscv/kriscv_isa.yaml +pspec=src/tests/riscof/kriscv/kriscv_platform.yaml +target_run=1 + +[sail_cSim] +pluginpath=src/tests/riscof/sail_cSim diff --git a/src/tests/integration/riscof/kriscv/env/link.ld b/src/tests/riscof/kriscv/env/link.ld similarity index 100% rename from src/tests/integration/riscof/kriscv/env/link.ld rename to src/tests/riscof/kriscv/env/link.ld diff --git a/src/tests/riscof/kriscv/env/model_test.h b/src/tests/riscof/kriscv/env/model_test.h new file mode 100644 index 00000000..ac6a91f0 --- /dev/null +++ b/src/tests/riscof/kriscv/env/model_test.h @@ -0,0 +1,52 @@ +#ifndef _COMPLIANCE_MODEL_H +#define _COMPLIANCE_MODEL_H +#define RVMODEL_DATA_SECTION \ + .align 8; .global begin_regstate; begin_regstate: \ + .word 128; \ + .align 8; .global end_regstate; end_regstate: \ + .word 4; + +//RV_COMPLIANCE_HALT +#define RVMODEL_HALT \ + _halt: \ + nop; + +#define RVMODEL_BOOT + +//RV_COMPLIANCE_DATA_BEGIN +#define RVMODEL_DATA_BEGIN \ + RVMODEL_DATA_SECTION \ + .align 4; \ + .global begin_signature; begin_signature: + +//RV_COMPLIANCE_DATA_END +#define RVMODEL_DATA_END \ + .global end_signature; end_signature: + +//RVTEST_IO_INIT +#define RVMODEL_IO_INIT +//RVTEST_IO_WRITE_STR +#define RVMODEL_IO_WRITE_STR(_R, _STR) +//RVTEST_IO_CHECK +#define RVMODEL_IO_CHECK() +//RVTEST_IO_ASSERT_GPR_EQ +#define RVMODEL_IO_ASSERT_GPR_EQ(_S, _R, _I) +//RVTEST_IO_ASSERT_SFPR_EQ +#define RVMODEL_IO_ASSERT_SFPR_EQ(_F, _R, _I) +//RVTEST_IO_ASSERT_DFPR_EQ +#define RVMODEL_IO_ASSERT_DFPR_EQ(_D, _R, _I) + +#define RVMODEL_SET_MSW_INT \ + li t1, 1; \ + li t2, 0x2000000; \ + sw t1, 0(t2); + +#define RVMODEL_CLEAR_MSW_INT \ + li t2, 0x2000000; \ + sw x0, 0(t2); + +#define RVMODEL_CLEAR_MTIMER_INT + +#define RVMODEL_CLEAR_MEXT_INT + +#endif // _COMPLIANCE_MODEL_H diff --git a/src/tests/integration/riscof/kriscv/kriscv_isa.yaml b/src/tests/riscof/kriscv/kriscv_isa.yaml similarity index 100% rename from src/tests/integration/riscof/kriscv/kriscv_isa.yaml rename to src/tests/riscof/kriscv/kriscv_isa.yaml diff --git a/src/tests/integration/riscof/kriscv/kriscv_platform.yaml b/src/tests/riscof/kriscv/kriscv_platform.yaml similarity index 100% rename from src/tests/integration/riscof/kriscv/kriscv_platform.yaml rename to src/tests/riscof/kriscv/kriscv_platform.yaml diff --git a/src/tests/integration/riscof/kriscv/riscof_kriscv.py b/src/tests/riscof/kriscv/riscof_kriscv.py similarity index 88% rename from src/tests/integration/riscof/kriscv/riscof_kriscv.py rename to src/tests/riscof/kriscv/riscof_kriscv.py index bd584ae2..6a8a5c16 100644 --- a/src/tests/integration/riscof/kriscv/riscof_kriscv.py +++ b/src/tests/riscof/kriscv/riscof_kriscv.py @@ -26,17 +26,12 @@ def __init__(self, *args: Any, **kwargs: Any) -> None: config = kwargs.get('config') if config is None: logger.error('Config for kriscv is missing.') - raise SystemExit + raise SystemExit(1) self.num_jobs = str(config['jobs'] if 'jobs' in config else 1) self.pluginpath = os.path.abspath(config['pluginpath']) self.isa_spec = os.path.abspath(config['ispec']) self.platform_spec = os.path.abspath(config['pspec']) self.target_run = ('target_run' not in config) or config['target_run'] == '1' - if self.target_run: - logger.error( - "Executing tests with riscof not yet supported. Set 'target_run=0' in config.ini to just compile the tests" - ) - raise SystemExit def initialise(self, suite: str, workdir: str, env: str) -> None: self.suite = suite @@ -49,6 +44,7 @@ def initialise(self, suite: str, workdir: str, env: str) -> None: def build(self, isa_yaml: str, platform_yaml: str) -> None: ispec = utils.load_yaml(isa_yaml)['hart0'] self.mabi = _mabi(ispec['ISA']) + _check_exec_exists('kriscv') _check_exec_exists('riscv64-unknown-elf-gcc') _check_exec_exists('riscv64-unknown-elf-objdump') _check_exec_exists('make') @@ -76,10 +72,16 @@ def runTests(self, testlist: dict[str, dict[str, Any]]) -> None: # noqa N802 input=f'{test_name}.elf', output=f'{test_name}.disass', ) - work_dir = entry['work_dir'] - execute = f'@cd {work_dir}; {compile_asm_cmd}; {compile_elf_cmd}; {objdump_cmd}' + work_dir = Path(entry['work_dir']).resolve(strict=True) + sig_file = work_dir / (name + '.signature') + execute_cmd = ( + f'kriscv run-arch-test {test_name}.elf --output {sig_file}' if self.target_run else 'echo "NO RUN"' + ) + execute = f'@cd {work_dir}; {compile_asm_cmd}; {compile_elf_cmd}; {objdump_cmd}; {execute_cmd}' make.add_target(execute, tname=test_name) make.execute_all(self.workdir) + if not self.target_run: + raise SystemExit(0) def _mabi(spec_isa: str) -> str: @@ -92,10 +94,10 @@ def _mabi(spec_isa: str) -> str: if '32E' in spec_isa: return 'ilp32e' logger.error(f'Bad ISA string in ISA YAML: {spec_isa}') - raise SystemExit + raise SystemExit(1) def _check_exec_exists(executable: str) -> None: if shutil.which(executable) is None: logger.error(f'{executable}: executable not found. Please check environment setup.') - raise SystemExit + raise SystemExit(1) diff --git a/src/tests/riscof/sail_cSim/__init__.py b/src/tests/riscof/sail_cSim/__init__.py new file mode 100644 index 00000000..b36383a6 --- /dev/null +++ b/src/tests/riscof/sail_cSim/__init__.py @@ -0,0 +1,3 @@ +from pkgutil import extend_path + +__path__ = extend_path(__path__, __name__) diff --git a/src/tests/riscof/sail_cSim/env/link.ld b/src/tests/riscof/sail_cSim/env/link.ld new file mode 100644 index 00000000..8ad95e04 --- /dev/null +++ b/src/tests/riscof/sail_cSim/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 = .; +} + diff --git a/src/tests/integration/riscof/kriscv/env/model_test.h b/src/tests/riscof/sail_cSim/env/model_test.h similarity index 71% rename from src/tests/integration/riscof/kriscv/env/model_test.h rename to src/tests/riscof/sail_cSim/env/model_test.h index bf58e3b2..1a129ad4 100644 --- a/src/tests/integration/riscof/kriscv/env/model_test.h +++ b/src/tests/riscof/sail_cSim/env/model_test.h @@ -1,5 +1,6 @@ #ifndef _COMPLIANCE_MODEL_H #define _COMPLIANCE_MODEL_H + #define RVMODEL_DATA_SECTION \ .pushsection .tohost,"aw",@progbits; \ .align 8; .global tohost; tohost: .dword 0; \ @@ -19,17 +20,16 @@ #define RVMODEL_BOOT -//RV_COMPLIANCE_DATA_BEGIN -#define RVMODEL_DATA_BEGIN \ - RVMODEL_DATA_SECTION \ - .align 4;\ - .global begin_signature; begin_signature: - -//RV_COMPLIANCE_DATA_END -#define RVMODEL_DATA_END \ - .align 4;\ +//RV_COMPLIANCE_DATA_BEGIN +#define RVMODEL_DATA_BEGIN \ + RVMODEL_DATA_SECTION \ + .align 4; .global begin_signature; begin_signature: + +//RV_COMPLIANCE_DATA_END +#define RVMODEL_DATA_END \ .global end_signature; end_signature: + //RVTEST_IO_INIT #define RVMODEL_IO_INIT //RVTEST_IO_WRITE_STR @@ -43,14 +43,9 @@ //RVTEST_IO_ASSERT_DFPR_EQ #define RVMODEL_IO_ASSERT_DFPR_EQ(_D, _R, _I) -#define RVMODEL_SET_MSW_INT \ - li t1, 1; \ - li t2, 0x2000000; \ - sw t1, 0(t2); +#define RVMODEL_SET_MSW_INT -#define RVMODEL_CLEAR_MSW_INT \ - li t2, 0x2000000; \ - sw x0, 0(t2); +#define RVMODEL_CLEAR_MSW_INT #define RVMODEL_CLEAR_MTIMER_INT diff --git a/src/tests/riscof/sail_cSim/riscof_sail_cSim.py b/src/tests/riscof/sail_cSim/riscof_sail_cSim.py new file mode 100644 index 00000000..20a49408 --- /dev/null +++ b/src/tests/riscof/sail_cSim/riscof_sail_cSim.py @@ -0,0 +1,122 @@ +from __future__ import annotations + +import logging +import os +import shutil +from importlib.metadata import version +from typing import TYPE_CHECKING + +import riscof.utils as utils # type: ignore +from riscof.pluginTemplate import pluginTemplate # type: ignore + +if TYPE_CHECKING: + from typing import Any + +logger = logging.getLogger() + + +class sail_cSim(pluginTemplate): # noqa N801 + __model__ = 'sail_cSim' + __version__ = version('kriscv') + + def __init__(self, *args: Any, **kwargs: Any) -> None: + super().__init__(*args, **kwargs) + + config = kwargs.get('config') + if config is None: + logger.error('Config node for sail_cSim missing.') + raise SystemExit(1) + self.num_jobs = str(config['jobs'] if 'jobs' in config else 1) + self.pluginpath = os.path.abspath(config['pluginpath']) + path = config['PATH'] if 'PATH' in config else '' + + self.sail_exe = {'32': os.path.join(path, 'riscv_sim_RV32'), '64': os.path.join(path, 'riscv_sim_RV64')} + self.isa_spec = os.path.abspath(config['ispec']) if 'ispec' in config else '' + self.platform_spec = os.path.abspath(config['pspec']) if 'ispec' in config else '' + self.make = config['make'] if 'make' in config else 'make' + logger.debug('SAIL CSim plugin initialised using the following configuration.') + for entry in config: + logger.debug(entry + ' : ' + config[entry]) + + def initialise(self, suite: str, workdir: str, env: str) -> None: + self.suite = suite + self.workdir = workdir + self.objdump_cmd = 'riscv64-unknown-elf-objdump -D {0} > {1};' + self.env = env + self.compile_cmd = 'riscv64-unknown-elf-gcc -march={0} \ + -static -mcmodel=medany -fvisibility=hidden -nostdlib -nostartfiles' + self.compile_cmd += ( + ' -T ' + + self.pluginpath + + '/env/link.ld\ + -I ' + + self.pluginpath + + '/env/\ + -I ' + + env + ) + + def build(self, isa_yaml: str, platform_yaml: str) -> None: + ispec = utils.load_yaml(isa_yaml)['hart0'] + self.xlen = '64' if 64 in ispec['supported_xlen'] else '32' + self.isa = 'rv' + self.xlen + if '64I' in ispec['ISA']: + self.compile_cmd = self.compile_cmd + ' -mabi=' + 'lp64 ' + elif '32I' in ispec['ISA']: + self.compile_cmd = self.compile_cmd + ' -mabi=' + 'ilp32 ' + elif '32E' in ispec['ISA']: + self.compile_cmd = self.compile_cmd + ' -mabi=' + 'ilp32e ' + if 'I' in ispec['ISA']: + self.isa += 'i' + if 'E' in ispec['ISA']: + self.isa += 'e' + if 'M' in ispec['ISA']: + self.isa += 'm' + if 'C' in ispec['ISA']: + self.isa += 'c' + if 'F' in ispec['ISA']: + self.isa += 'f' + if 'D' in ispec['ISA']: + self.isa += 'd' + objdump = 'riscv64-unknown-elf-objdump' + if shutil.which(objdump) is None: + logger.error(objdump + ': executable not found. Please check environment setup.') + raise SystemExit(1) + compiler = 'riscv64-unknown-elf-gcc' + if shutil.which(compiler) is None: + logger.error(compiler + ': executable not found. Please check environment setup.') + raise SystemExit(1) + if shutil.which(self.sail_exe[self.xlen]) is None: + logger.error(self.sail_exe[self.xlen] + ': executable not found. Please check environment setup.') + raise SystemExit(1) + if shutil.which(self.make) is None: + logger.error(self.make + ': executable not found. Please check environment setup.') + raise SystemExit(1) + + def runTests(self, testlist: dict[str, dict[str, Any]]) -> None: # noqa N802 + make = utils.makeUtil(makefilePath=os.path.join(self.workdir, 'Makefile.' + self.name[:-1])) + make.makeCommand = self.make + ' -j' + self.num_jobs + for file in testlist: + testentry = testlist[file] + test = testentry['test_path'] + test_dir = testentry['work_dir'] + test_name = test.rsplit('/', 1)[1][:-2] + sig_file = self.name[:-1] + '.signature' + elf = 'ref.elf' + execute = '@cd ' + test_dir + ';' + + cmd = self.compile_cmd.format(testentry['isa'].lower()) + ' ' + test + ' -o ' + elf + compile_cmd = cmd + ' -D' + ' -D'.join(testentry['macros']) + execute += compile_cmd + ';' + + execute += self.objdump_cmd.format(elf, 'ref.disass') + + if 'c' not in self.isa: + cmd = self.sail_exe[self.xlen] + ' -C' + else: + cmd = self.sail_exe[self.xlen] + execute += cmd + f' --test-signature={sig_file} {elf} > {test_name}.log 2>&1;' + + make.add_target(execute, tname=test_name) + + make.execute_all(self.workdir) diff --git a/src/tests/riscof/sail_cSim/sail_isa.yaml b/src/tests/riscof/sail_cSim/sail_isa.yaml new file mode 100644 index 00000000..eeb44ab3 --- /dev/null +++ b/src/tests/riscof/sail_cSim/sail_isa.yaml @@ -0,0 +1,38 @@ +hart_ids: [0] +hart0: + ISA: RV32IMACZicsr_Zifencei + physical_addr_sz: 32 + supported_xlen: [32] + misa: + reset-val: 0x0 + rv32: + mxl: + implemented: false + extensions: + implemented: false + accessible: true + rv64: + accessible: false + mtvec: + reset-val: 0x80000000 + rv32: + base: + implemented: true + type: + warl: + dependency_fields: [] + legal: + - base[29:0] in [0x20000000] + wr_illegal: + - Unchanged + mode: + implemented: true + type: + warl: + dependency_fields: [] + legal: + - mode[1:0] in [0x0] + wr_illegal: + - Unchanged + + accessible: true diff --git a/src/tests/riscof/sail_cSim/sail_platform.yaml b/src/tests/riscof/sail_cSim/sail_platform.yaml new file mode 100644 index 00000000..4b99ed9c --- /dev/null +++ b/src/tests/riscof/sail_cSim/sail_platform.yaml @@ -0,0 +1,4 @@ +nmi: + label: nmi_vector +reset: + label: reset_vector diff --git a/src/tests/unit/test_unit.py b/src/tests/unit/test_unit.py index 0449289e..52f4a290 100644 --- a/src/tests/unit/test_unit.py +++ b/src/tests/unit/test_unit.py @@ -8,17 +8,34 @@ # isort: on import pytest from pyk.kllvm.convert import llvm_to_pattern, pattern_to_llvm -from pyk.prelude.kint import intToken +from pyk.kore.match import kore_int +from pyk.prelude.kint import INT, intToken from kriscv import term_builder from kriscv.term_builder import register +from kriscv.term_manip import kore_sparse_bytes, normalize_memory if TYPE_CHECKING: from typing import Final - from pyk.kast.inner import KInner + from pyk.kast.inner import KInner, KSort + from pyk.kore.syntax import Pattern -DISASS_TEST_DATA: Final = ( + from kriscv.tools import Tools + + +def _eval_call(tools: Tools, call: KInner, sort: KSort) -> KInner: + return tools.krun.kore_to_kast(_eval_call_to_kore(tools, call, sort)) + + +def _eval_call_to_kore(tools: Tools, call: KInner, sort: KSort) -> Pattern: + llvm_input = pattern_to_llvm(tools.krun.kast_to_kore(call, sort)) + llvm_res = tools.runtime.evaluate(llvm_input) + return llvm_to_pattern(llvm_res) + + +# test id, instruction binary as a string of 0s/1s, disassembled instruction +DISASS_TEST_DATA: Final[tuple[tuple[str, str, KInner], ...]] = ( ( 'addi x1, x2, 3', '00000000010100010000000010010011', @@ -237,7 +254,65 @@ def test_disassemble(instr_bits: str, expected: KInner) -> None: assert len(instr_bits) == 32 tools = semantics() disass_call = term_builder.disassemble(intToken(int(instr_bits, 2))) - disass_call_llvm = pattern_to_llvm(tools.krun.kast_to_kore(disass_call, term_builder.sort_instruction())) - actual_llvm = tools.runtime.evaluate(disass_call_llvm) - actual = tools.krun.kore_to_kast(llvm_to_pattern(actual_llvm)) + actual = _eval_call(tools, disass_call, term_builder.sort_instruction()) assert actual == expected + + +# test id, initial memory, addr to write, byte to write +MEMORY_TEST_DATA: Final[tuple[tuple[str, dict[int, bytes], int, int], ...]] = ( + ('empty_start', {}, 0, 0x1A), + ('empty_later', {}, 10, 0x1A), + ('mid_bytes', {1: b'\x7F\x7F'}, 2, 0x1A), + ('start_pre_bytes', {1: b'\x7F\x7F'}, 0, 0x1A), + ('empty_pre_bytes', {2: b'\x7F\x7F'}, 1, 0x1A), + ('end_post_bytes', {2: b'\x7F\x7F'}, 4, 0x1A), + ('empty_post_bytes', {2: b'\x7F\x7F', 6: b'\x7F'}, 4, 0x1A), + ('end', {2: b'\x7F\x7F'}, 5, 0x1A), + ('merge_bytes', {1: b'\x7F\x7F', 4: b'\x7F'}, 3, 0x1A), +) + + +@pytest.mark.parametrize( + 'memory,addr,byte', + [(memory, addr, byte) for (_, memory, addr, byte) in MEMORY_TEST_DATA], + ids=[test_id for test_id, *_ in MEMORY_TEST_DATA], +) +def test_memory(memory: dict[int, bytes], addr: int, byte: int) -> None: + assert 0 <= byte <= 0xFF + for val in memory.values(): + for byte in val: + assert 0 <= byte <= 0xFF + + byte_val = byte.to_bytes(1, 'big') + + # Manually compute the expected final memory state + memory_expect: dict[int, bytes] = {} + stored = False + for start, val in memory.items(): + if start <= addr and addr < start + len(val): + val_idx = addr - start + memory_expect[start] = val[:val_idx] + byte_val + val[val_idx + 1 :] + stored = True + else: + memory_expect[start] = val + if not stored: + memory_expect[addr] = byte_val + memory_expect = normalize_memory(memory_expect) + + # Execute storeByte to get the actual final memory state + tools = semantics() + memory_sb = term_builder.sparse_bytes(memory) + addr_word = term_builder.word(addr) + + store_call = term_builder.store_byte(memory_sb, addr_word, intToken(byte)) + memory_actual_sb_kore = _eval_call_to_kore(tools, store_call, term_builder.sort_memory()) + memory_actual = kore_sparse_bytes(memory_actual_sb_kore) + + assert memory_actual == memory_expect + + # Also execute loadByte and check that we correctly read back the written value + memory_actual_sb = tools.krun.kore_to_kast(memory_actual_sb_kore) + load_call = term_builder.load_byte(memory_actual_sb, addr_word) + load_actual = kore_int(_eval_call_to_kore(tools, load_call, INT)) + + assert load_actual == byte diff --git a/tests/simple/jalr.S b/tests/simple/jalr.S index fd857d8d..95ebb3b2 100644 --- a/tests/simple/jalr.S +++ b/tests/simple/jalr.S @@ -1,20 +1,25 @@ #include "simple.h" START_TEXT - addi x15, x0, 1 - jalr x1, x15, 3 // x1 = PC_4 + 4 - auipc x2, 0 // x2 = PC_5 = PC_4 + 4 = x1 - sub x3, x1, x2 // x3 = 0 + auipc x15, 0 // x15 = PC_4 + addi x15, x15, 5 // x15 = PC_4 + 5 + jalr x1, x15, 7 // x1 = PC_6 + 4, jump to PC_4 + 12 = PC_7 + auipc x2, 0 // x2 = PC_5 = PC_4 + 4 = x1 + sub x3, x1, x2 // x3 = 0 - addi x4, x0, 0 // x4 = 0 - jalr x0, x0, 9 - addi x4, x4, 1 // should be skipped - nop // still x4 = 0 + addi x4, x0, 0 // x4 = 0 + auipc x14, 0 // x14 = PC_11 + jalr x0, x14, 13 // jump to PC_11 + 13 = PC_14 + addi x4, x4, 1 // should be skipped + nop // still x4 = 0 - addi x5, x0, 0 // x5 = 0 - jalr x0, x0, 12 // jump to line 18 - addi x5, x5, 1 // x5 += 1 - jalr x0, x0, 8 // jump to line 19 - jalr x0, x0, -7 // jump to line 16 - nop // now x5 = 1 + addi x5, x0, 0 // x5 = 0 + auipc x13, 0 // x13 = PC_17 + jalr x0, x13, 20 // jump to PC_17 + 20 = PC_22 + addi x5, x5, 1 // x5 += 1 + auipc x12, 0 // x12 = PC_20 + jalr x0, x12, 16 // jump to PC_20 + 16 = PC_24 + auipc x11, 0 // x11 = PC_22 + jalr x0, x11, -11 // jump to PC_22 - 11 = PC_19 + nop // now x5 = 1 END_TEXT