Kompile and cache full p-token.smir.json, add --target-dir for prove-rs

kmir/src/kmir/__main__.py

@@ -66,10 +66,22 @@ def run(target_dir: Path):
 
 
 def _kmir_prove_rs(opts: ProveRSOpts) -> None:
-    proof = KMIR.prove_rs(opts)
-    print(str(proof.summary))
-    if not proof.passed:
-        sys.exit(1)
+    label = f'{opts.rs_file.stem}.{opts.start_symbol}'
+    proof_data_dir = (opts.proof_dir / label) if opts.proof_dir is not None else None
+
+    def prove(target_dir: Path) -> APRProof:
+        proof = KMIR.prove_rs(opts, target_dir=target_dir)
+        print(str(proof.summary))
+        if not proof.passed:
+            sys.exit(1)
+
+    if opts.target_dir is not None:
+        prove(Path(opts.target_dir))
+    elif proof_data_dir is not None:
+        prove(proof_data_dir)
+    else:
+        with tempfile.TemporaryDirectory() as target_dir:
+            prove(Path(target_dir))
 
 
 def _kmir_view(opts: ViewOpts) -> None:
@@ -151,7 +163,7 @@ def _kmir_section_edge(opts: SectionEdgeOpts) -> None:
 
     target_path = opts.proof_dir / opts.id
 
-    _LOGGER.info(f'Reading proof from disc: {opts.proof_dir}, {opts.id}')
+    _LOGGER.info(f'Reading proof from disk: {opts.proof_dir}, {opts.id}')
     apr_proof = APRProof.read_proof_data(opts.proof_dir, opts.id)
 
     smir_info = SMIRInfo.from_file(target_path / 'smir.json')
@@ -239,6 +251,7 @@ def _arg_parser() -> ArgumentParser:
 
     prove_args = ArgumentParser(add_help=False)
     prove_args.add_argument('--proof-dir', metavar='DIR', help='Proof directory')
+    prove_args.add_argument('--target-dir', type=Path, metavar='TARGET_DIR', help='SMIR kompilation target directory')
     prove_args.add_argument('--bug-report', metavar='PATH', help='path to optional bug report')
     prove_args.add_argument('--max-depth', metavar='DEPTH', type=int, help='max steps to take between nodes in kcfg')
     prove_args.add_argument(
@@ -486,6 +499,7 @@ def _parse_args(ns: Namespace) -> KMirOpts:
             return ProveRSOpts(
                 rs_file=Path(ns.rs_file),
                 proof_dir=ns.proof_dir,
+                target_dir=ns.target_dir,
                 bug_report=ns.bug_report,
                 max_depth=ns.max_depth,
                 max_iterations=ns.max_iterations,

kmir/src/kmir/kmir.py

@@ -1,10 +1,8 @@
 from __future__ import annotations
 
 import logging
-import tempfile
 from contextlib import contextmanager
 from functools import cached_property
-from pathlib import Path
 from typing import TYPE_CHECKING
 
 from pyk.cli.utils import bug_report_arg
@@ -28,6 +26,7 @@
 
 if TYPE_CHECKING:
     from collections.abc import Iterator
+    from pathlib import Path
     from typing import Final
 
     from pyk.cterm.show import CTermShow
@@ -192,78 +191,75 @@ def apr_proof_from_smir(
         return APRProof(id, kcfg, [], init_node.id, target_node.id, {}, proof_dir=proof_dir)
 
     @staticmethod
-    def prove_rs(opts: ProveRSOpts) -> APRProof:
+    def prove_rs(opts: ProveRSOpts, target_dir: Path) -> APRProof:
         if not opts.rs_file.is_file():
             raise ValueError(f'Input file does not exist: {opts.rs_file}')
 
         label = str(opts.rs_file.stem) + '.' + opts.start_symbol
 
-        with tempfile.TemporaryDirectory() as tmp_dir:
-            target_path = opts.proof_dir / label if opts.proof_dir is not None else Path(tmp_dir)
+        proof_data_dir = (opts.proof_dir / label) if opts.proof_dir is not None else None
 
-            if not opts.reload and opts.proof_dir is not None and APRProof.proof_data_exists(label, opts.proof_dir):
-                _LOGGER.info(f'Reading proof from disc: {opts.proof_dir}, {label}')
-                apr_proof = APRProof.read_proof_data(opts.proof_dir, label)
+        target_dir.mkdir(parents=True, exist_ok=True)
 
-                smir_info = SMIRInfo.from_file(target_path / 'smir.json')
-                kmir = KMIR.from_kompiled_kore(
-                    smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=target_path
-                )
+        if not opts.reload and opts.proof_dir is not None and APRProof.proof_data_exists(label, opts.proof_dir):
+            _LOGGER.info(f'Reading proof from disk: {opts.proof_dir}, {label}')
+            apr_proof = APRProof.read_proof_data(opts.proof_dir, label)
+
+            smir_info = SMIRInfo.from_file(proof_data_dir / 'smir.json')
+
+            kmir = KMIR.from_kompiled_kore(smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=target_dir)
+        else:
+            _LOGGER.info(f'Constructing initial proof: {label}')
+            if opts.smir:
+                smir_info = SMIRInfo.from_file(opts.rs_file)
             else:
-                _LOGGER.info(f'Constructing initial proof: {label}')
-                if opts.smir:
-                    smir_info = SMIRInfo.from_file(opts.rs_file)
-                else:
-                    smir_info = SMIRInfo(cargo_get_smir_json(opts.rs_file, save_smir=opts.save_smir))
-
-                smir_info = smir_info.reduce_to(opts.start_symbol)
-                # Report whether the reduced call graph includes any functions without MIR bodies
-                missing_body_syms = [
-                    sym
-                    for sym, item in smir_info.items.items()
-                    if 'MonoItemFn' in item['mono_item_kind']
-                    and item['mono_item_kind']['MonoItemFn'].get('body') is None
-                ]
-                has_missing = len(missing_body_syms) > 0
-                _LOGGER.info(f'Reduced items table size {len(smir_info.items)}')
-                if has_missing:
-                    _LOGGER.info(f'missing-bodies-present={has_missing} count={len(missing_body_syms)}')
-                    _LOGGER.debug(f'Missing-body function symbols (first 5): {missing_body_syms[:5]}')
-
-                kmir = KMIR.from_kompiled_kore(
-                    smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=target_path
-                )
-
-                apr_proof = kmir.apr_proof_from_smir(
-                    label, smir_info, start_symbol=opts.start_symbol, proof_dir=opts.proof_dir
-                )
-                if apr_proof.proof_dir is not None and (apr_proof.proof_dir / label).is_dir():
-                    smir_info.dump(apr_proof.proof_dir / apr_proof.id / 'smir.json')
-
-            if apr_proof.passed:
-                return apr_proof
-
-            cut_point_rules = KMIR.cut_point_rules(
-                break_on_calls=opts.break_on_calls,
-                break_on_function_calls=opts.break_on_function_calls,
-                break_on_intrinsic_calls=opts.break_on_intrinsic_calls,
-                break_on_thunk=opts.break_on_thunk,
-                break_every_statement=opts.break_every_statement,
-                break_on_terminator_goto=opts.break_on_terminator_goto,
-                break_on_terminator_switch_int=opts.break_on_terminator_switch_int,
-                break_on_terminator_return=opts.break_on_terminator_return,
-                break_on_terminator_call=opts.break_on_terminator_call,
-                break_on_terminator_assert=opts.break_on_terminator_assert,
-                break_on_terminator_drop=opts.break_on_terminator_drop,
-                break_on_terminator_unreachable=opts.break_on_terminator_unreachable,
-                break_every_terminator=opts.break_every_terminator,
-                break_every_step=opts.break_every_step,
+                smir_info = SMIRInfo(cargo_get_smir_json(opts.rs_file, save_smir=opts.save_smir))
+
+            smir_exec = smir_info.reduce_to(opts.start_symbol)
+            # Report whether the reduced call graph includes any functions without MIR bodies
+            missing_body_syms = [
+                sym
+                for sym, item in smir_exec.items.items()
+                if 'MonoItemFn' in item['mono_item_kind'] and item['mono_item_kind']['MonoItemFn'].get('body') is None
+            ]
+            has_missing = len(missing_body_syms) > 0
+            _LOGGER.info(f'Reduced items table size {len(smir_exec.items)}')
+            if has_missing:
+                _LOGGER.info(f'missing-bodies-present={has_missing} count={len(missing_body_syms)}')
+                _LOGGER.debug(f'Missing-body function symbols (first 5): {missing_body_syms[:5]}')
+
+            kmir = KMIR.from_kompiled_kore(smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=target_dir)
+
+            apr_proof = kmir.apr_proof_from_smir(
+                label, smir_exec, start_symbol=opts.start_symbol, proof_dir=opts.proof_dir
             )
+            if apr_proof.proof_dir is not None and (apr_proof.proof_dir / label).is_dir():
+                smir_info.dump(apr_proof.proof_dir / apr_proof.id / 'smir.json')
+
+        if apr_proof.passed:
+            return apr_proof
+
+        cut_point_rules = KMIR.cut_point_rules(
+            break_on_calls=opts.break_on_calls,
+            break_on_function_calls=opts.break_on_function_calls,
+            break_on_intrinsic_calls=opts.break_on_intrinsic_calls,
+            break_on_thunk=opts.break_on_thunk,
+            break_every_statement=opts.break_every_statement,
+            break_on_terminator_goto=opts.break_on_terminator_goto,
+            break_on_terminator_switch_int=opts.break_on_terminator_switch_int,
+            break_on_terminator_return=opts.break_on_terminator_return,
+            break_on_terminator_call=opts.break_on_terminator_call,
+            break_on_terminator_assert=opts.break_on_terminator_assert,
+            break_on_terminator_drop=opts.break_on_terminator_drop,
+            break_on_terminator_unreachable=opts.break_on_terminator_unreachable,
+            break_every_terminator=opts.break_every_terminator,
+            break_every_step=opts.break_every_step,
+        )
 
-            with kmir.kcfg_explore(label) as kcfg_explore:
-                prover = APRProver(kcfg_explore, execute_depth=opts.max_depth, cut_point_rules=cut_point_rules)
-                prover.advance_proof(apr_proof, max_iterations=opts.max_iterations)
-                return apr_proof
+        with kmir.kcfg_explore(label) as kcfg_explore:
+            prover = APRProver(kcfg_explore, execute_depth=opts.max_depth, cut_point_rules=cut_point_rules)
+            prover.advance_proof(apr_proof, max_iterations=opts.max_iterations)
+            return apr_proof
 
 
 class KMIRSemantics(DefaultSemantics):

kmir/src/kmir/options.py

@@ -105,11 +105,13 @@ class ProveRSOpts(ProveOpts):
     save_smir: bool
     smir: bool
     start_symbol: str
+    target_dir: Path | None
 
     def __init__(
         self,
         rs_file: Path,
         proof_dir: Path | str | None = None,
+        target_dir: Path | str | None = None,
         bug_report: Path | None = None,
         max_depth: int | None = None,
         max_iterations: int | None = None,
@@ -134,6 +136,7 @@ def __init__(
     ) -> None:
         self.rs_file = rs_file
         self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None
+        self.target_dir = Path(target_dir).resolve() if target_dir is not None else None
         self.bug_report = bug_report
         self.max_depth = max_depth
         self.max_iterations = max_iterations