diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index bcc3adbae..3c495f5f9 100644 --- a/kmir/src/kmir/__main__.py +++ b/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, diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 747bc770e..314b21ce0 100644 --- a/kmir/src/kmir/kmir.py +++ b/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): diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index cda622524..c6c51ff45 100644 --- a/kmir/src/kmir/options.py +++ b/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