Update dependency: deps/k_release (#55)

* deps/k_release: Set Version 7.1.178 * Set Version: 0.1.46 * pyproject.toml: sync pyk version 7.1.178 * deps/k_release: Set Version 7.1.179 * pyproject.toml: sync pyk version 7.1.179 * deps/k_release: Set Version 7.1.180 * pyproject.toml: sync pyk version 7.1.180 * deps/k_release: Set Version 7.1.181 * pyproject.toml: sync pyk version 7.1.181 * deps/k_release: Set Version 7.1.182 * pyproject.toml: sync pyk version 7.1.182 * deps/k_release: Set Version 7.1.183 * pyproject.toml: sync pyk version 7.1.183 * deps/k_release: Set Version 7.1.184 * deps/k_release: Set Version 7.1.186 * pyproject.toml: sync pyk version 7.1.186 * deps/k_release: Set Version 7.1.187 * pyproject.toml: sync pyk version 7.1.187 * deps/k_release: Set Version 7.1.191 * pyproject.toml: sync pyk version 7.1.191 * deps/k_release: Set Version 7.1.193 * pyproject.toml: sync pyk version 7.1.193 * deps/k_release: Set Version 7.1.194 * pyproject.toml: sync pyk version 7.1.194 * pyproject.toml: sync pyk version 7.1.194 * deps/k_release: Set Version 7.1.195 * pyproject.toml: sync pyk version 7.1.195 * pyproject.toml: sync pyk version 7.1.195 * pyproject.toml: sync pyk version 7.1.195 * deps/k_release: Set Version 7.1.198 * pyproject.toml: sync pyk version 7.1.198 * pyproject.toml: sync pyk version 7.1.198 * deps/k_release: Set Version 7.1.199 * pyproject.toml: sync pyk version 7.1.199 * deps/k_release: Set Version 7.1.201 * pyproject.toml: sync pyk version 7.1.201 * deps/k_release: Set Version 7.1.202 * pyproject.toml: sync pyk version 7.1.202 * deps/k_release: Set Version 7.1.203 * pyproject.toml: sync pyk version 7.1.203 * pyproject.toml: sync pyk version 7.1.203 * deps/k_release: Set Version 7.1.204 * pyproject.toml: sync pyk version 7.1.204 * pyproject.toml: sync pyk version 7.1.204 * deps/k_release: Set Version 7.1.205 * pyproject.toml: sync pyk version 7.1.205 * deps/k_release: Set Version 7.1.207 * pyproject.toml: sync pyk version 7.1.207 * deps/k_release: Set Version 7.1.208 * pyproject.toml: sync pyk version 7.1.208 * pyproject.toml: sync pyk version 7.1.208 * deps/k_release: Set Version 7.1.211 * pyproject.toml: sync pyk version 7.1.211 * deps/k_release: Set Version 7.1.212 * pyproject.toml: sync pyk version 7.1.212 * test_unit.py: Update byte representation in memory test data * pyproject.toml: sync pyk version 7.1.212 * tools.py: Improve error handling for krun pattern execution - Capture stdout, stderr, and input configuration when krun pattern fails - Write error details to separate files for debugging - Preserve original exception raising * riscv-semantics: Improve memory byte handling and error logging - Update loadByte rule to convert MaybeByte to Int - Add MaybeByte2Int function to handle byte conversion - Enhance debug logging for krun pattern execution with resolved file paths * tools.py: Refactor debug file generation and import order - Reorganize import statements for better readability - Standardize string quotes to single quotes - Minor formatting improvements in debug file logging * Update src/kriscv/tools.py Co-authored-by: Tamás Tóth <[email protected]> * Update src/kriscv/kdist/riscv-semantics/sparse-bytes.md Co-authored-by: Tamás Tóth <[email protected]> --------- Co-authored-by: devops <[email protected]> Co-authored-by: Stevengre <[email protected]> Co-authored-by: Tamás Tóth <[email protected]>
runtimeverification · Feb 14, 2025 · 20cb2ba · 20cb2ba
1 parent f29a607
commit 20cb2ba
Show file tree

Hide file tree

Showing 8 changed files with 686 additions and 279 deletions.
diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-7.1.174
+7.1.212
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.45
+0.1.46
diff --git a/poetry.lock b/poetry.lock
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.45"
+version = "0.1.46"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -18,7 +18,7 @@ riscv-semantics = "kriscv.kdist.plugin"
 
 [tool.poetry.dependencies]
 python = "^3.10"
-kframework = "7.1.174"
+kframework = "7.1.212"
 pyyaml = "^6.0.1"
 types-pyyaml = "^6.0.12.20240311"
 filelock = "^3.14.0"

diff --git a/src/kriscv/kdist/riscv-semantics/riscv.md b/src/kriscv/kdist/riscv-semantics/riscv.md
@@ -103,7 +103,7 @@ module RISCV-MEMORY
 We abstract the particular memory representation behind `loadByte` and `storeByte` functions.
 ```k
   syntax Int ::= loadByte(memory: Memory, address: Word) [function, symbol(Memory:loadByte)]
-  rule loadByte(MEM, W(ADDR)) => { readByte(MEM, ADDR) }:>Int
+  rule loadByte(MEM, W(ADDR)) => MaybeByte2Int(readByte(MEM, ADDR))
 
   syntax Memory ::= storeByte(memory: Memory, address: Word, byte: Int) [function, total, symbol(Memory:storeByte)]
   rule storeByte(MEM, W(ADDR), B) => writeByte(MEM, ADDR, B)

diff --git a/src/kriscv/kdist/riscv-semantics/sparse-bytes.md b/src/kriscv/kdist/riscv-semantics/sparse-bytes.md
@@ -54,6 +54,10 @@ We provide helpers to prepend either data or an empty region to an existing `Spa
   syntax MaybeByte ::=
       Int
     | ".Byte"
+  
+  syntax Int ::= MaybeByte2Int(MaybeByte) [function, total]
+  rule MaybeByte2Int(I:Int) => I
+  rule MaybeByte2Int(.Byte) => 0
 
   syntax MaybeByte ::=
       readByte  (SparseBytes  , Int) [function, total]

diff --git a/src/kriscv/tools.py b/src/kriscv/tools.py
@@ -1,5 +1,7 @@
 from __future__ import annotations
 
+from pathlib import Path
+from subprocess import CalledProcessError
 from typing import TYPE_CHECKING
 
 from elftools.elf.elffile import ELFFile  # type: ignore
@@ -13,7 +15,6 @@
 from kriscv.term_manip import kore_sparse_bytes, kore_word, match_map
 
 if TYPE_CHECKING:
-    from pathlib import Path
 
     from pyk.kast.inner import KInner
     from pyk.kllvm.runtime import Runtime
@@ -46,7 +47,23 @@ def init_config(self, config_vars: dict[str, KInner]) -> KInner:
 
     def run_config(self, config: KInner) -> KInner:
         config_kore = self.krun.kast_to_kore(config, sort=GENERATED_TOP_CELL)
-        final_config_kore = self.krun.run_pattern(config_kore, check=True)
+        try:
+            final_config_kore = self.krun.run_pattern(config_kore, check=True)
+        except CalledProcessError as e:
+            path = Path.cwd()
+            stdout_path = path / 'krun_stdout.txt'
+            stderr_path = path / 'krun_stderr.txt'
+            input_path = path / 'krun_input.txt'
+
+            stdout_path.write_text(e.stdout)
+            stderr_path.write_text(e.stderr)
+            input_path.write_text(config_kore.text)
+
+            print('Generated debug files:')
+            print(f'- {stdout_path.resolve()}: KRun standard output')
+            print(f'- {stderr_path.resolve()}: KRun error output')
+            print(f'- {input_path.resolve()}: Input configuration in Kore format')
+            raise
         return self.krun.kore_to_kast(final_config_kore)
 
     def run_elf(self, elf_file: Path, *, end_symbol: str | None = None) -> KInner:

diff --git a/src/tests/unit/test_unit.py b/src/tests/unit/test_unit.py
@@ -262,13 +262,13 @@ def test_disassemble(instr_bits: str, expected: KInner) -> None:
 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),
+    ('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),
 )