Add option --depth to kriscv run (#89)

Co-authored-by: devops <devops@runtimeverification.com>

Author: tothtamas28

package/version

@@ -1 +1 @@
-0.1.67
+0.1.68

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.67"
+version = "0.1.68"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/kriscv/__main__.py

@@ -23,6 +23,7 @@ class KRISCVOpts:
 @dataclass
 class RunOpts(KRISCVOpts):
     input_file: Path
+    depth: int | None
     end_symbol: str | None
     zero_init: bool | None
 
@@ -55,6 +56,7 @@ def _parse_args(args: Sequence[str]) -> KRISCVOpts:
             return RunOpts(
                 temp_dir=ns.temp_dir,
                 input_file=ns.input_file.resolve(strict=True),
+                depth=ns.depth if ns.depth is not None and ns.depth >= 0 else None,
                 end_symbol=ns.end_symbol,
                 zero_init=ns.zero_init,
             )
@@ -71,7 +73,12 @@ def _parse_args(args: Sequence[str]) -> KRISCVOpts:
 def _kriscv_run(opts: RunOpts) -> None:
     tools = semantics(temp_dir=opts.temp_dir)
     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)
+    final_conf = tools.run_elf(
+        opts.input_file,
+        depth=opts.depth,
+        regs=regs,
+        end_symbol=opts.end_symbol,
+    )
     print(tools.kprint.pretty_print(final_conf, sort_collections=True))
 
 
@@ -125,6 +132,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('-d', '--depth', type=int, help='execution depth (set negative for unbounded execution)')
     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')
 

src/kriscv/tools.py

@@ -38,10 +38,10 @@ def init_config(self, config_vars: dict[str, KInner]) -> KInner:
         conf = self.krun.definition.init_config(sort=GENERATED_TOP_CELL)
         return Subst(config_vars)(conf)
 
-    def run_config(self, config: KInner) -> KInner:
+    def run_config(self, config: KInner, *, depth: int | None = None) -> KInner:
         config_kore = self.krun.kast_to_kore(config, sort=GENERATED_TOP_CELL)
         try:
-            final_config_kore = self.krun.run_pattern(config_kore, check=True)
+            final_config_kore = self.krun.run_pattern(config_kore, depth=depth, check=True)
         except CalledProcessError as e:
             path = Path.cwd()
             stdout_path = path / 'krun_stdout.txt'
@@ -63,6 +63,7 @@ def run_elf(
         self,
         elf_file: Path,
         *,
+        depth: int | None = None,
         regs: dict[int, int] | None = None,
         end_symbol: str | None = None,
     ) -> KInner:
@@ -79,7 +80,7 @@ def run_elf(
                 '$PC': elf_parser.entry_point(elf),
                 '$HALT': halt_cond,
             }
-            return self.run_config(self.init_config(config_vars))
+        return self.run_config(self.init_config(config_vars), depth=depth)
 
     def get_registers(self, config: KInner) -> dict[int, int]:
         _, cells = split_config_from(config)