Skip to content

Commit

Permalink
riscv-semantics: Improve memory byte handling and error logging
Browse files Browse the repository at this point in the history
- 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
  • Loading branch information
Stevengre committed Feb 14, 2025
1 parent f06872a commit e0eed85
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 5 deletions.
2 changes: 1 addition & 1 deletion src/kriscv/kdist/riscv-semantics/riscv.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
4 changes: 4 additions & 0 deletions src/kriscv/kdist/riscv-semantics/sparse-bytes.md
Original file line number Diff line number Diff line change
Expand Up @@ -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) => I
rule MaybeByte2Int(.Byte) => 0
syntax MaybeByte ::=
readByte (SparseBytes , Int) [function, total]
Expand Down
18 changes: 14 additions & 4 deletions src/kriscv/tools.py
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,13 @@
from pyk.kast.manip import split_config_from
from pyk.kore.match import kore_int
from pyk.ktool.krun import KRun
from pathlib import Path
from pyk.prelude.k import GENERATED_TOP_CELL

from kriscv import elf_parser, term_builder
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
Expand Down Expand Up @@ -50,12 +50,22 @@ def run_config(self, config: KInner) -> KInner:
try:
final_config_kore = self.krun.run_pattern(config_kore, check=True)
except CalledProcessError as e:
with open('krun_stdout.txt', 'w') as f:
path = Path.cwd()
stdout_path = path / 'krun_stdout.txt'
stderr_path = path / 'krun_stderr.txt'
input_path = path / 'krun_input.txt'

with open(stdout_path, 'w') as f:
f.write(e.stdout)
with open('krun_stderr.txt', 'w') as f:
with open(stderr_path, 'w') as f:
f.write(e.stderr)
with open('krun_input.txt', 'w') as f:
with open(input_path, 'w') as f:
config_kore.write(f)

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)

Expand Down

0 comments on commit e0eed85

Please sign in to comment.