Add parameter temp_dir to K tools

Author: tothtamas28

pyk/src/pyk/ktool/kprint.py

@@ -66,6 +66,7 @@ def _kast(
     expression: str | None = None,
     module: str | None = None,
     sort: str | None = None,
+    temp_dir: str | Path | None = None,
     gen_glr_parser: bool = False,
     # ---
     check: bool = True,
@@ -83,6 +84,9 @@ def _kast(
         definition_dir = Path(definition_dir)
         check_dir_path(definition_dir)
 
+    if temp_dir is not None:
+        temp_dir = Path(temp_dir)
+
     if input is not None:
         input = KAstInput(input)
 
@@ -98,6 +102,7 @@ def _kast(
         expression=expression,
         module=module,
         sort=sort,
+        temp_dir=temp_dir,
         gen_glr_parser=gen_glr_parser,
     )
 
@@ -116,6 +121,7 @@ def gen_glr_parser(
     definition_dir: str | Path | None = None,
     module: str | None = None,
     sort: str | None = None,
+    temp_dir: str | Path | None = None,
 ) -> Path:
     parser_file = Path(parser_file)
     _kast(
@@ -124,6 +130,7 @@ def gen_glr_parser(
         definition_dir=definition_dir,
         module=module,
         sort=sort,
+        temp_dir=temp_dir,
         gen_glr_parser=True,
         check=True,
     )
@@ -141,6 +148,7 @@ def _build_arg_list(
     expression: str | None,
     module: str | None,
     sort: str | None,
+    temp_dir: Path | None,
     gen_glr_parser: bool,
 ) -> list[str]:
     args = [command if command is not None else 'kast']
@@ -158,6 +166,8 @@ def _build_arg_list(
         args += ['--module', module]
     if sort:
         args += ['--sort', sort]
+    if temp_dir:
+        args += ['--temp-dir', str(temp_dir)]
     if gen_glr_parser:
         args += ['--gen-glr-parser']
     return args
@@ -311,6 +321,7 @@ def _expression_kast(
                 output=output,
                 module=module,
                 sort=sort,
+                temp_dir=self.use_directory,
                 check=check,
             )
 
@@ -326,5 +337,6 @@ def _expression_kast(
                 output=output,
                 module=module,
                 sort=sort,
+                temp_dir=self.use_directory,
                 check=check,
             )

pyk/src/pyk/ktool/kprove.py

@@ -61,6 +61,7 @@ def _kprove(
     output: KProveOutput | None = None,
     depth: int | None = None,
     claims: Iterable[str] = (),
+    temp_dir: Path | None = None,
     haskell_backend_command: str | None = None,
     dry_run: bool = False,
     # --
@@ -86,6 +87,7 @@ def _kprove(
         output=output,
         depth=depth,
         claims=claims,
+        temp_dir=temp_dir,
         haskell_backend_command=haskell_backend_command,
         dry_run=dry_run,
     )
@@ -109,6 +111,7 @@ def _build_arg_list(
     output: KProveOutput | None,
     depth: int | None,
     claims: Iterable[str],
+    temp_dir: Path | None,
     haskell_backend_command: str | None,
     dry_run: bool,
 ) -> list[str]:
@@ -136,6 +139,9 @@ def _build_arg_list(
     if claims:
         args += ['--claims', ','.join(claims)]
 
+    if temp_dir:
+        args += ['--temp-dir', str(temp_dir)]
+
     if haskell_backend_command:
         args += ['--haskell-backend-command', haskell_backend_command]
 
@@ -225,6 +231,7 @@ def prove(
             include_dirs=include_dirs,
             md_selector=md_selector,
             output=KProveOutput.JSON,
+            temp_dir=self.use_directory,
             dry_run=dry_run,
             args=self.prover_args + list(args),
             env=env,

pyk/src/pyk/ktool/krun.py

@@ -74,9 +74,10 @@ def run(
                 definition_dir=self.definition_dir,
                 output=KRunOutput.JSON,
                 depth=depth,
-                no_expand_macros=not expand_macros,
                 cmap=cmap,
                 pmap=pmap,
+                temp_dir=self.use_directory,
+                no_expand_macros=not expand_macros,
                 bug_report=self._bug_report,
                 check=(expect_rc == 0),
             )
@@ -108,6 +109,7 @@ def run_kore(
                 output=KRunOutput.KORE,
                 parser='cat',
                 depth=depth,
+                temp_dir=self.use_directory,
                 no_expand_macros=not expand_macros,
                 bug_report=self._bug_report,
                 check=(expect_rc == 0),
@@ -143,6 +145,7 @@ def run_kore_term(
                 parser='cat',
                 term=True,
                 depth=depth,
+                temp_dir=self.use_directory,
                 no_expand_macros=not expand_macros,
                 search_final=search_final,
                 no_pattern=no_pattern,
@@ -236,6 +239,7 @@ def _krun(
     pmap: Mapping[str, str] | None = None,
     cmap: Mapping[str, str] | None = None,
     term: bool = False,
+    temp_dir: Path | None = None,
     no_expand_macros: bool = False,
     search_final: bool = False,
     no_pattern: bool = False,
@@ -264,6 +268,7 @@ def _krun(
         pmap=pmap,
         cmap=cmap,
         term=term,
+        temp_dir=temp_dir,
         no_expand_macros=no_expand_macros,
         search_final=search_final,
         no_pattern=no_pattern,
@@ -296,6 +301,7 @@ def _build_arg_list(
     pmap: Mapping[str, str] | None,
     cmap: Mapping[str, str] | None,
     term: bool,
+    temp_dir: Path | None,
     no_expand_macros: bool,
     search_final: bool,
     no_pattern: bool,
@@ -317,6 +323,8 @@ def _build_arg_list(
         args += [f'-c{name}={value}']
     if term:
         args += ['--term']
+    if temp_dir:
+        args += ['--temp-dir', str(temp_dir)]
     if no_expand_macros:
         args += ['--no-expand-macros']
     if search_final:

pyk/src/tests/unit/ktool/test_krun.py

@@ -7,37 +7,38 @@
 
 from pyk.ktool.krun import KRunOutput, _build_arg_list
 
-# fmt: off
-required_args: dict[str, Any] = OrderedDict([
-    ('command', 'krun'),
-    ('input_file', None),
-    ('definition_dir', None),
-    ('output', None),
-    ('parser', None),
-    ('depth', None),
-    ('pmap', None),
-    ('cmap', None),
-    ('term', False),
-    ('no_expand_macros', False),
-    ('search_final', False),
-    ('no_pattern', False),
-])
+required_args: dict[str, Any] = OrderedDict(
+    [
+        ('command', 'krun'),
+        ('input_file', None),
+        ('definition_dir', None),
+        ('output', None),
+        ('parser', None),
+        ('depth', None),
+        ('pmap', None),
+        ('cmap', None),
+        ('term', False),
+        ('temp_dir', None),
+        ('no_expand_macros', False),
+        ('search_final', False),
+        ('no_pattern', False),
+    ]
+)
+
 optional_args: dict[str, tuple[Any, list[str]]] = {
-    'input_file':       (Path('input/path'),    ['input/path']),
-    'definition_dir':   (Path('def/path'),      ['--definition', 'def/path']),
-    'output':           (KRunOutput.JSON,       ['--output', 'json']),
-    'parser':           ('cat',                 ['--parser', 'cat']),
-    'depth':            (1234,                  ['--depth', '1234']),
-    'pmap':             ({'FOO': 'bar', 'BUZZ': 'kill'},
-                                                ['-pFOO=bar', '-pBUZZ=kill']),
-    'cmap':             ({'COO': 'car', 'FUZZ': 'bill'},
-                                                ['-cCOO=car', '-cFUZZ=bill']),
-    'term':             (True,                  ['--term']),
-    'no_expand_macros': (True,                  ['--no-expand-macros']),
-    'search_final':     (True,                  ['--search-final']),
-    'no_pattern':       (True,                  ['--no-pattern']),
+    'input_file': (Path('input/path'), ['input/path']),
+    'definition_dir': (Path('def/path'), ['--definition', 'def/path']),
+    'output': (KRunOutput.JSON, ['--output', 'json']),
+    'parser': ('cat', ['--parser', 'cat']),
+    'depth': (1234, ['--depth', '1234']),
+    'pmap': ({'FOO': 'bar', 'BUZZ': 'kill'}, ['-pFOO=bar', '-pBUZZ=kill']),
+    'cmap': ({'COO': 'car', 'FUZZ': 'bill'}, ['-cCOO=car', '-cFUZZ=bill']),
+    'term': (True, ['--term']),
+    'temp_dir': (Path('/tmp/path'), ['--temp-dir', '/tmp/path']),
+    'no_expand_macros': (True, ['--no-expand-macros']),
+    'search_final': (True, ['--search-final']),
+    'no_pattern': (True, ['--no-pattern']),
 }
-# fmt: on
 
 
 def make_kwargs(test_id: str, keys: list[str]) -> tuple[str, dict[str, Any], list[str]]: