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]>

Author: 4 people

deps/k_release

@@ -1 +1 @@
-7.1.174
+7.1.212

package/version

@@ -1 +1 @@
-0.1.45
+0.1.46

poetry.lock

@@ -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"

pyproject.toml

@@ -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)

src/kriscv/kdist/riscv-semantics/riscv.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]

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

@@ -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:

src/kriscv/tools.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),
 )