From 3cab1b5e1ccf6a7ed50ff707d25f5e34b89c54a7 Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <roberto.rosmaninho@pi2.network>
Date: Fri, 31 Jan 2025 16:17:02 -0300
Subject: [PATCH] Adding `--save-temps` and `--statistics` to krun

---
 pyk/src/pyk/ktool/krun.py             | 22 ++++++++++++++++++++++
 pyk/src/tests/unit/ktool/test_krun.py |  4 ++++
 2 files changed, 26 insertions(+)

diff --git a/pyk/src/pyk/ktool/krun.py b/pyk/src/pyk/ktool/krun.py
index 6b09c28fc3f..90f4e170932 100644
--- a/pyk/src/pyk/ktool/krun.py
+++ b/pyk/src/pyk/ktool/krun.py
@@ -78,6 +78,8 @@ def run_process(
         pipe_stderr: bool = True,
         bug_report: BugReport | None = None,
         debugger: bool = False,
+        save_temps: bool = False,
+        statistics: bool = False,
     ) -> CompletedProcess:
         with self._temp_file() as ntf:
             pgm.write(ntf)
@@ -94,6 +96,8 @@ def run_process(
                 pmap=pmap,
                 term=term,
                 temp_dir=self.use_directory,
+                save_temps=save_temps,
+                statistics=statistics,
                 no_expand_macros=not expand_macros,
                 search_final=search_final,
                 no_pattern=no_pattern,
@@ -113,6 +117,8 @@ def run_proof_hint(
         parser: str | None = None,
         term: bool = False,
         temp_dir: Path | None = None,
+        save_temps: bool = False,
+        statistics: bool = False,
         depth: int | None = None,
         expand_macros: bool = True,
         search_final: bool = False,
@@ -137,6 +143,8 @@ def run_proof_hint(
                 cmap=cmap,
                 term=term,
                 temp_dir=temp_dir,
+                save_temps=save_temps,
+                statistics=statistics,
                 no_expand_macros=not expand_macros,
                 search_final=search_final,
                 no_pattern=no_pattern,
@@ -216,6 +224,8 @@ def run(
         check: bool = False,
         pipe_stderr: bool = True,
         bug_report: BugReport | None = None,
+        save_temps: bool = False,
+        statistics: bool = False,
         debugger: bool = False,
     ) -> None:
         result = self.run_process(
@@ -230,6 +240,8 @@ def run(
             output=output,
             pipe_stderr=pipe_stderr,
             bug_report=bug_report,
+            save_temps=save_temps,
+            statistics=statistics,
             debugger=debugger,
         )
 
@@ -301,6 +313,8 @@ def _krun(
     pmap: Mapping[str, str] | None = None,
     term: bool = False,
     temp_dir: Path | None = None,
+    save_temps: bool = False,
+    statistics: bool = False,
     no_expand_macros: bool = False,
     search_final: bool = False,
     no_pattern: bool = False,
@@ -334,6 +348,8 @@ def _krun(
         cmap=cmap,
         term=term,
         temp_dir=temp_dir,
+        save_temps=save_temps,
+        statistics=statistics,
         no_expand_macros=no_expand_macros,
         search_final=search_final,
         no_pattern=no_pattern,
@@ -364,6 +380,8 @@ def _build_arg_list(
     cmap: Mapping[str, str] | None,
     term: bool,
     temp_dir: Path | None,
+    save_temps: bool,
+    statistics: bool,
     no_expand_macros: bool,
     search_final: bool,
     no_pattern: bool,
@@ -389,6 +407,10 @@ def _build_arg_list(
         args += ['--term']
     if temp_dir:
         args += ['--temp-dir', str(temp_dir)]
+    if save_temps:
+        args += ['--save-temps']
+    if statistics:
+        args += ['--statistics']
     if no_expand_macros:
         args += ['--no-expand-macros']
     if search_final:
diff --git a/pyk/src/tests/unit/ktool/test_krun.py b/pyk/src/tests/unit/ktool/test_krun.py
index 69ff022e7f2..bdee7e20320 100644
--- a/pyk/src/tests/unit/ktool/test_krun.py
+++ b/pyk/src/tests/unit/ktool/test_krun.py
@@ -19,6 +19,8 @@
         ('cmap', None),
         ('term', False),
         ('temp_dir', None),
+        ('save_temps', False),
+        ('statistics', False),
         ('no_expand_macros', False),
         ('search_final', False),
         ('no_pattern', False),
@@ -37,6 +39,8 @@
     'cmap': ({'COO': 'car', 'FUZZ': 'bill'}, ['-cCOO=car', '-cFUZZ=bill']),
     'term': (True, ['--term']),
     'temp_dir': (Path('/tmp/path'), ['--temp-dir', '/tmp/path']),
+    'save_temps': (True, ['--save-temps']),
+    'statistics': (True, ['--statistics']),
     'no_expand_macros': (True, ['--no-expand-macros']),
     'search_final': (True, ['--search-final']),
     'no_pattern': (True, ['--no-pattern']),