Skip to content

Commit f54ce95

Browse files
committed
Use parsed .smir.json to avoid repeated LLVM compilation
Tested with `time make test-verify-rust-std TEST_ARGS='-k unchecked_add'` which resulted in a 17.8% reduction in time (110.643 seconds): - Before: 10m22.304s - After: 8m31.661s
1 parent a737317 commit f54ce95

1 file changed

Lines changed: 5 additions & 4 deletions

File tree

kmir/src/tests/integration/test_integration.py

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212
from pyk.kast.pretty import PrettyPrinter
1313
from pyk.proof.show import APRProofShow
1414

15-
from kmir.cargo import CargoProject
15+
from kmir.cargo import CargoProject, cargo_get_smir_json
1616
from kmir.kmir import KMIR, KMIRAPRNodePrinter
1717
from kmir.options import ProveOpts, ShowOpts
1818
from kmir.parse.parser import Parser
@@ -312,7 +312,8 @@ def test_verify_rust_std(rs_file: Path, kmir: KMIR, update_expected_output: bool
312312
if update_expected_output and not should_show:
313313
pytest.skip()
314314

315-
prove_rs_opts = ProveRSOpts(rs_file, terminate_on_thunk=True)
315+
parsed_smir = cargo_get_smir_json(rs_file)
316+
prove_opts = ProveOpts(rs_file, terminate_on_thunk=True, parsed_smir=parsed_smir)
316317
printer = PrettyPrinter(kmir.definition)
317318
cterm_show = CTermShow(printer.print)
318319

@@ -321,8 +322,8 @@ def test_verify_rust_std(rs_file: Path, kmir: KMIR, update_expected_output: bool
321322
start_symbols = VERIFY_RUST_STD_START_SYMBOLS[rs_file.stem]
322323

323324
for start_symbol in start_symbols:
324-
prove_rs_opts.start_symbol = start_symbol
325-
apr_proof = kmir.prove_rs(prove_rs_opts)
325+
prove_opts.start_symbol = start_symbol
326+
apr_proof = kmir.prove_program(prove_opts)
326327

327328
if should_show:
328329
display_opts = ShowOpts(

0 commit comments

Comments
 (0)