Add test harness for K functions (#61)

Adds a target `riscv-semantics.func-test` and a corresponding
integration test.

---------

Co-authored-by: devops <[email protected]>

Author: tothtamas28

Makefile

@@ -23,7 +23,7 @@ poetry-install:
 # Semantics
 
 kdist-build: poetry-install
-	$(POETRY) run kdist -v build riscv-semantics.llvm riscv-semantics.kllvm riscv-semantics.kllvm-runtime
+	$(POETRY) run kdist -v build riscv-semantics.*
 
 kdist-clean: poetry-install
 	$(POETRY) run kdist clean

package/version

@@ -1 +1 @@
-0.1.47
+0.1.48

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.47"
+version = "0.1.48"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/kriscv/kdist/plugin.py

@@ -78,8 +78,17 @@ def context(self) -> dict[str, str]:
     'llvm': KompileTarget(
         lambda src_dir: {
             'main_file': src_dir / 'riscv-semantics/riscv.md',
+            'include_dirs': [src_dir],
             'syntax_module': 'RISCV',
+            'md_selector': 'k',
+            'warnings_to_errors': True,
+        },
+    ),
+    'func-test': KompileTarget(
+        lambda src_dir: {
+            'main_file': src_dir / 'riscv-semantics/func-test.md',
             'include_dirs': [src_dir],
+            'syntax_module': 'FUNC-TEST',
             'md_selector': 'k',
             'warnings_to_errors': True,
         },

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

@@ -0,0 +1,7 @@
+```k
+requires "riscv-disassemble.md"
+
+module FUNC-TEST
+  imports RISCV-DISASSEMBLE
+endmodule
+```

src/tests/integration/test_functions.py

@@ -0,0 +1,74 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+import pytest
+from pyk.kdist import kdist
+from pyk.kore.prelude import INT, SORT_K_ITEM, generated_counter, generated_top, inj, int_dv, k, kseq
+from pyk.kore.syntax import App, SortApp
+from pyk.ktool.krun import llvm_interpret
+
+if TYPE_CHECKING:
+    from pathlib import Path
+    from typing import Final
+
+    from pyk.kore.syntax import Pattern
+
+
+@pytest.fixture(scope='module')
+def definition_dir() -> Path:
+    return kdist.get('riscv-semantics.func-test')
+
+
+def sw(rs2: int, imm: int, rs1: int) -> App:
+    return App(
+        'LblRegImmRegInstr',
+        (),
+        (
+            App('LblSW'),
+            reg(rs2),
+            int_dv(imm),
+            reg(rs1),
+        ),
+    )
+
+
+def reg(x: int) -> App:
+    return inj(INT, SortApp('SortRegister'), int_dv(x))
+
+
+DISASSEMBLE_TEST_DATA: Final = (
+    ('sw s0,296(sp)', b'\x12\x81\x24\x23', SortApp('SortRegImmRegInstr'), sw(8, 296, 2)),
+    ('sw s1,292(sp)', b'\x12\x91\x22\x23', SortApp('SortRegImmRegInstr'), sw(9, 292, 2)),
+)
+
+
+@pytest.mark.parametrize(
+    'test_id,code,sort,pattern',
+    DISASSEMBLE_TEST_DATA,
+    ids=[test_id for test_id, *_ in DISASSEMBLE_TEST_DATA],
+)
+def test_disassemble(definition_dir: Path, test_id: str, code: bytes, sort: SortApp, pattern: Pattern) -> None:
+    # Given
+    n = int.from_bytes(code, byteorder='big')
+    init = config(inj(SortApp('SortInstruction'), SORT_K_ITEM, disassemble(n)))
+    expected = config(inj(sort, SORT_K_ITEM, pattern))
+
+    # When
+    actual = llvm_interpret(definition_dir, init)
+
+    # Then
+    assert actual == expected
+
+
+def config(kitem: Pattern) -> App:
+    return generated_top(
+        (
+            k(kseq((kitem,))),
+            generated_counter(int_dv(0)),
+        ),
+    )
+
+
+def disassemble(n: int) -> App:
+    return App('Lbldisassemble', (), (int_dv(n),))