Add option --zero-init

package/version

@@ -1 +1 @@
-0.1.50
+0.1.51

pyproject.toml

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

src/kriscv/__main__.py

@@ -24,6 +24,7 @@ class KRISCVOpts:
 class RunOpts(KRISCVOpts):
     input_file: Path
     end_symbol: str | None
+    zero_init: bool | None
 
 
 @dataclass
@@ -55,6 +56,7 @@ def _parse_args(args: Sequence[str]) -> KRISCVOpts:
                 temp_dir=ns.temp_dir,
                 input_file=ns.input_file.resolve(strict=True),
                 end_symbol=ns.end_symbol,
+                zero_init=ns.zero_init,
             )
         case 'run-arch-test':
             return RunArchTestOpts(
@@ -68,7 +70,8 @@ def _parse_args(args: Sequence[str]) -> KRISCVOpts:
 
 def _kriscv_run(opts: RunOpts) -> None:
     tools = semantics(temp_dir=opts.temp_dir)
-    final_conf = tools.run_elf(opts.input_file, end_symbol=opts.end_symbol)
+    regs = dict.fromkeys(range(32), 0) if opts.zero_init else {}
+    final_conf = tools.run_elf(opts.input_file, regs=regs, end_symbol=opts.end_symbol)
     print(tools.kprint.pretty_print(final_conf, sort_collections=True))
 
 
@@ -123,6 +126,7 @@ def _arg_parser() -> ArgumentParser:
     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_parser.add_argument('-z', '--zero-init', action='store_true', help='initialize registers to zero')
 
     run_arch_test_parser = command_parser.add_parser(
         'run-arch-test',

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

@@ -31,7 +31,7 @@ module RISCV-CONFIGURATION
   configuration
     <riscv>
       <instrs> #EXECUTE ~> .K </instrs>
-      <regs> .Map </regs> // Map{Register, Word}
+      <regs> $REGS:Map </regs> // Map{Register, Word}
       <pc> $PC:Word </pc>
       <mem> $MEM:SparseBytes </mem>
     </riscv>

src/kriscv/term_builder.py

@@ -5,6 +5,7 @@
 
 from pyk.kast.inner import KApply, KInner, KSort
 from pyk.prelude.bytes import bytesToken
+from pyk.prelude.collections import map_of
 from pyk.prelude.kint import intToken
 
 from kriscv.term_manip import normalize_memory
@@ -309,3 +310,8 @@ def load_byte(mem: KInner, addr: KInner) -> KInner:
 
 def store_byte(mem: KInner, addr: KInner, value: KInner) -> KInner:
     return KApply('Memory:storeByte', mem, addr, value)
+
+
+def regs(dct: dict[int, int]) -> KInner:
+    regs: dict[KInner, KInner] = {intToken(k): word(v) for k, v in dct.items()}
+    return map_of(regs)

src/kriscv/tools.py

@@ -66,7 +66,13 @@ def run_config(self, config: KInner) -> KInner:
             raise
         return self.krun.kore_to_kast(final_config_kore)
 
-    def run_elf(self, elf_file: Path, *, end_symbol: str | None = None) -> KInner:
+    def run_elf(
+        self,
+        elf_file: Path,
+        *,
+        regs: dict[int, int] | None = None,
+        end_symbol: str | None = None,
+    ) -> KInner:
         with open(elf_file, 'rb') as f:
             elf = ELFFile(f)
             if end_symbol is not None:
@@ -75,6 +81,7 @@ def run_elf(self, elf_file: Path, *, end_symbol: str | None = None) -> KInner:
             else:
                 halt_cond = term_builder.halt_never()
             config_vars = {
+                '$REGS': term_builder.regs(regs or {}),
                 '$MEM': elf_parser.memory(elf),
                 '$PC': elf_parser.entry_point(elf),
                 '$HALT': halt_cond,