Reuse prebuilt KMIR definition to avoid redundant llvm-kompile processes (#1069)

If a Rust file contains multiple targets to prove (e.g. [verify-rust-std
challenge
11](https://github.com/runtimeverification/mir-semantics/tree/master/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints))
then multiple `llvm-kompile` processes will be invoked by
[_prove](https://github.com/runtimeverification/mir-semantics/blob/c92c8ce0b4b0d762d679a15351b562fa243fd8f0/kmir/src/kmir/_prove.py#L70-L77).
This PR pushes this process earlier to create a KMIR definition with all
the required start symbols so that `llvm-kompile` is called once per
file.

In particular:
- `test_verify_rust_std` now compiles a prebuilt KMIR definition with
reduced start symbols. This definition is reused for all proof harnesses
in a file;
- `prove_with_kmir` is added as separate control-flow to `prove`. This
may not be _elegant_, but right now I think it is the clearest
separation, and I was hesitant to add flags or refactor too
aggressively;

Results from verify-std-rust challenge 11:
- Prior to this refactoring: 1 `llvm-kompile` / start-symbol = 138
`llvm-kompile` invocations
- After this refactoring: 1 `llvm-kompile` / file = 16 `llvm-kompile`
invocations
- Approximately 3x increase of performance

<details>

PRIOR:

real  31m16.872s
user 170m18.245s
 sys   5m51.240s

real  31m36.755s
user 175m15.830s
 sys   6m32.859s

AFTER:

real    10m20.730s
user    44m10.271s
sys     2m15.364s

real 10m58s
user 47m0s
 sys  2m24s

real 10m40.395s
user 45m54.822s
 sys  2m20.399s
 
real 10m38.370s
user 45m32.886s
 sys  2m19.782s


</details>

Author: dkcumming

kmir/src/kmir/_prove.py

@@ -32,6 +32,7 @@
 
 
 def prove(opts: ProveOpts) -> APRProof:
+    """Run a proof creating a new KMIR instance."""
     if not opts.rs_file.is_file():
         raise ValueError(f'Input file does not exist: {opts.rs_file}')
 
@@ -49,6 +50,33 @@ def prove(opts: ProveOpts) -> APRProof:
         return _prove(opts, target_path, label)
 
 
+def prove_with_kmir(
+    kmir: KMIR,
+    smir_info: SMIRInfo,
+    opts: ProveOpts,
+) -> APRProof:
+    """Run a proof using a pre-built KMIR instance, avoiding redundant kompilation."""
+
+    if opts.max_workers is not None and opts.max_workers < 1:
+        raise ValueError(f'Expected positive integer for `max_workers, got: {opts.max_workers}')
+
+    # No check for rs_file as smir_info already exists
+    label = f'{opts.rs_file.stem}.{opts.start_symbol}'
+
+    _LOGGER.info(f'Using pre-built KMIR for proof: {label}')
+    proof = apr_proof_from_smir(
+        kmir,
+        label,
+        smir_info,
+        start_symbol=opts.start_symbol,
+        proof_dir=opts.proof_dir,
+    )
+    if proof.proof_dir is not None and (proof.proof_dir / label).is_dir():
+        smir_info.dump(proof.proof_dir / proof.id / 'smir.json')
+
+    return _advance_proof(kmir, proof, opts, label)
+
+
 def _prove(opts: ProveOpts, target_path: Path, label: str) -> APRProof:
     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}')
@@ -107,6 +135,10 @@ def _prove(opts: ProveOpts, target_path: Path, label: str) -> APRProof:
         if proof.proof_dir is not None and (proof.proof_dir / label).is_dir():
             smir_info.dump(proof.proof_dir / proof.id / 'smir.json')
 
+    return _advance_proof(kmir, proof, opts, label)
+
+
+def _advance_proof(kmir: KMIR, proof: APRProof, opts: ProveOpts, label: str) -> APRProof:
     if proof.passed:
         return proof
 

kmir/src/kmir/kmir.py

@@ -126,6 +126,12 @@ def prove_program(opts: ProveOpts) -> APRProof:
 
         return prove(opts)
 
+    @staticmethod
+    def prove_program_with_kmir(kmir: KMIR, smir_info: SMIRInfo, opts: ProveOpts) -> APRProof:
+        from ._prove import prove_with_kmir
+
+        return prove_with_kmir(kmir, smir_info, opts)
+
 
 class KMIRSemantics(DefaultSemantics):
     terminate_on_thunk: bool

kmir/src/tests/integration/test_integration.py

@@ -305,6 +305,10 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None:
     ids=[f'{spec.parent.name}/{spec.stem}' for spec in VERIFY_RUST_STD_FILES],
 )
 def test_verify_rust_std(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None:
+    from kmir.kompile import kompile_smir
+
+    # kmir fixture is unused here; kept so a kompile failure fails fast before per-file work begins
+
     should_fail = rs_file.stem.endswith('fail')
     should_show = rs_file.stem in VERIFY_RUST_STD_SHOW_SPECS
 
@@ -313,33 +317,44 @@ def test_verify_rust_std(rs_file: Path, kmir: KMIR, update_expected_output: bool
 
     parsed_smir = cargo_get_smir_json(rs_file)
     prove_opts = ProveOpts(rs_file, terminate_on_thunk=True, parsed_smir=parsed_smir)
-    printer = PrettyPrinter(kmir.definition)
-    cterm_show = CTermShow(printer.print)
 
     start_symbols = ['main']
     if rs_file.stem in VERIFY_RUST_STD_START_SYMBOLS:
         start_symbols = VERIFY_RUST_STD_START_SYMBOLS[rs_file.stem]
 
-    for start_symbol in start_symbols:
-        prove_opts.start_symbol = start_symbol
-        apr_proof = kmir.prove_program(prove_opts)
-
-        if should_show:
-            display_opts = ShowOpts(
-                rs_file.parent, apr_proof.id, full_printer=False, smir_info=None, omit_current_body=False
-            )
-            shower = APRProofShow(kmir.definition, node_printer=KMIRAPRNodePrinter(cterm_show, apr_proof, display_opts))
-            show_res = '\n'.join(shower.show(apr_proof))
-            show_dir = rs_file.parent / 'show'
-            show_dir.mkdir(exist_ok=True)
-            assert_or_update_show_output(
-                show_res, show_dir / f'{rs_file.stem}.{start_symbol}.expected', update=update_expected_output
-            )
+    # Kompile once with full SMIR (reduced to all start symbols), reuse for all proofs
+    smir_info = SMIRInfo(parsed_smir)
+    smir_info = smir_info.reduce_to(start_symbols)
+    with tempfile.TemporaryDirectory() as tmp_dir:
+        target_path = Path(tmp_dir)  # required for kompilation
+        kompiled = kompile_smir(smir_info=smir_info, target_dir=target_path, symbolic=True)
+        prebuilt_kmir = kompiled.create_kmir()  # this KMIR has the kompiled function defs
+        printer = PrettyPrinter(prebuilt_kmir.definition)
+        cterm_show = CTermShow(printer.print)
 
-        if not should_fail:
-            assert apr_proof.passed
-        else:
-            assert apr_proof.failed
+        for start_symbol in start_symbols:
+            prove_opts.start_symbol = start_symbol
+            apr_proof = KMIR.prove_program_with_kmir(prebuilt_kmir, smir_info, prove_opts)
+
+            if should_show:
+                display_opts = ShowOpts(
+                    rs_file.parent, apr_proof.id, full_printer=False, smir_info=None, omit_current_body=False
+                )
+                shower = APRProofShow(
+                    prebuilt_kmir.definition,
+                    node_printer=KMIRAPRNodePrinter(cterm_show, apr_proof, display_opts),
+                )
+                show_res = '\n'.join(shower.show(apr_proof))
+                show_dir = rs_file.parent / 'show'
+                show_dir.mkdir(exist_ok=True)
+                assert_or_update_show_output(
+                    show_res, show_dir / f'{rs_file.stem}.{start_symbol}.expected', update=update_expected_output
+                )
+
+            if not should_fail:
+                assert apr_proof.passed
+            else:
+                assert apr_proof.failed
 
 
 MULTI_CRATE_DIR = (Path(__file__).parent / 'data' / 'crate-tests').resolve(strict=True)