diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index ddf6175df..eda33a37e 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -21,12 +21,17 @@ jobs: run: | git config user.name devops git config user.email devops@runtimeverification.com + - name: 'Install uv' + uses: astral-sh/setup-uv@v5 + with: + version: 0.7.2 - name: 'Update version' run: | og_version=$(git show origin/${GITHUB_BASE_REF}:package/version) ./package/version.sh bump ${og_version} ./package/version.sh sub new_version=$(cat package/version) + uv --directory kmir lock --no-upgrade git add --update && git commit --message "Set Version: $(cat package/version)" || true - name: 'Push updates' run: git push origin HEAD:${GITHUB_HEAD_REF} diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 8c41293fc..7de9bb80b 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kmir" -version = "0.3.133" +version = "0.3.134" description = "" requires-python = "~=3.10" dependencies = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 7dc40f5da..217b0a44a 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.133' +VERSION: Final = '0.3.134' diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 19bdfea8c..f87f5847d 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -3,17 +3,17 @@ import logging import sys from argparse import ArgumentParser -from dataclasses import dataclass from pathlib import Path from typing import TYPE_CHECKING -from pyk.cli.args import KCLIArgs, LoggingOptions +from pyk.cli.args import KCLIArgs from pyk.kast.outer import KFlatModule, KImport from pyk.proof.reachability import APRProof, APRProver from pyk.proof.tui import APRProofViewer from .build import HASKELL_DEF_DIR, LLVM_LIB_DIR, haskell_semantics, llvm_semantics from .kmir import KMIR, KMIRAPRNodePrinter +from .options import GenSpecOpts, ProvePruneOpts, ProveRSOpts, ProveRunOpts, ProveViewOpts, RunOpts from .parse.parser import parse_json from .rust import CargoProject @@ -22,103 +22,12 @@ from collections.abc import Sequence from typing import Final + from .options import KMirOpts + _LOGGER: Final = logging.getLogger(__name__) _LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s' -@dataclass -class KMirOpts(LoggingOptions): ... - - -@dataclass -class RunOpts(KMirOpts): - bin: str | None - file: str | None - depth: int - start_symbol: str - haskell_backend: bool - - -@dataclass -class GenSpecOpts(KMirOpts): - input_file: Path - output_file: Path | None - start_symbol: str - - def __init__(self, input_file: Path, output_file: Path | str | None, start_symbol: str) -> None: - self.input_file = input_file - if output_file is None: - self.output_file = None - else: - self.output_file = Path(output_file).resolve() - self.start_symbol = start_symbol - - -@dataclass -class ProveRSOpts(KMirOpts): - rs_file: Path - bug_report: Path | None - max_depth: int | None - max_iterations: int | None - - def __init__( - self, - rs_file: Path, - bug_report: Path | None = None, - max_depth: int | None = None, - max_iterations: int | None = None, - ) -> None: - self.rs_file = rs_file - self.bug_report = bug_report - self.max_depth = max_depth - self.max_iterations = max_iterations - - -@dataclass -class ProveRunOpts(KMirOpts): - spec_file: Path - proof_dir: Path | None - include_labels: tuple[str, ...] | None - exclude_labels: tuple[str, ...] | None - bug_report: Path | None - max_depth: int | None - max_iterations: int | None - reload: bool - - def __init__( - self, - spec_file: Path, - proof_dir: Path | str | None, - include_labels: str | None, - exclude_labels: str | None, - bug_report: Path | None = None, - max_depth: int | None = None, - max_iterations: int | None = None, - reload: bool = False, - ) -> None: - self.spec_file = spec_file - self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None - self.include_labels = tuple(include_labels.split(',')) if include_labels is not None else None - self.exclude_labels = tuple(exclude_labels.split(',')) if exclude_labels is not None else None - self.bug_report = bug_report - self.max_depth = max_depth - self.max_iterations = max_iterations - self.reload = reload - - -@dataclass -class ProveViewOpts(KMirOpts): - proof_dir: Path - id: str - - -@dataclass -class ProvePruneOpts(KMirOpts): - proof_dir: Path - id: str - node_id: int - - def _kmir_run(opts: RunOpts) -> None: tools = haskell_semantics() if opts.haskell_backend else llvm_semantics() @@ -143,10 +52,8 @@ def _kmir_run(opts: RunOpts) -> None: def _kmir_prove_rs(opts: ProveRSOpts) -> None: - if not opts.rs_file.is_file(): - raise ValueError(f'Rust spec file does not exist: {opts.rs_file}') kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR, bug_report=opts.bug_report) - proof = kmir.prove_rs(opts.rs_file, max_depth=opts.max_depth, max_iterations=opts.max_iterations) + proof = kmir.prove_rs(opts) print(str(proof.summary)) if not proof.passed: sys.exit(1) @@ -264,12 +171,19 @@ def _arg_parser() -> ArgumentParser: '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from' ) + prove_args = ArgumentParser(add_help=False) + 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( + '--max-iterations', metavar='ITERATIONS', type=int, help='max number of proof iterations to take' + ) + prove_parser = command_parser.add_parser( 'prove', help='Utilities for working with proofs over SMIR', parents=[kcli_args.logging_args] ) prove_command_parser = prove_parser.add_subparsers(dest='prove_command', required=True) - prove_run_parser = prove_command_parser.add_parser('run', help='Run the prover on a spec') + prove_run_parser = prove_command_parser.add_parser('run', help='Run the prover on a spec', parents=[prove_args]) prove_run_parser.add_argument('input_file', metavar='FILE', help='K File with the spec module') prove_run_parser.add_argument('--proof-dir', metavar='DIR', help='Proof directory') prove_run_parser.add_argument( @@ -278,14 +192,7 @@ def _arg_parser() -> ArgumentParser: prove_run_parser.add_argument( '--exclude-labels', metavar='LABELS', help='Comma separated list of claim labels to exclude' ) - prove_run_parser.add_argument('--bug-report', metavar='PATH', help='path to optional bug report') - prove_run_parser.add_argument( - '--max-depth', metavar='DEPTH', type=int, help='max steps to take between nodes in kcfg' - ) prove_run_parser.add_argument('--reload', action='store_true', help='Force restarting proof') - prove_run_parser.add_argument( - '--max-iterations', metavar='ITERATIONS', type=int, help='max number of proof iterations to take' - ) prove_view_parser = prove_command_parser.add_parser('view', help='View a saved proof') prove_view_parser.add_argument('id', metavar='PROOF_ID', help='The id of the proof to view') @@ -299,18 +206,11 @@ def _arg_parser() -> ArgumentParser: prove_prune_parser.add_argument('node_id', metavar='NODE', type=int, help='The node to prune') prove_rs_parser = command_parser.add_parser( - 'prove-rs', help='Prove a rust program', parents=[kcli_args.logging_args] + 'prove-rs', help='Prove a rust program', parents=[kcli_args.logging_args, prove_args] ) prove_rs_parser.add_argument( 'rs_file', type=Path, metavar='FILE', help='Rust file with the spec function (e.g. main)' ) - prove_rs_parser.add_argument('--bug-report', metavar='PATH', help='path to optional bug report') - prove_rs_parser.add_argument( - '--max-depth', metavar='DEPTH', type=int, help='max steps to take between nodes in kcfg' - ) - prove_rs_parser.add_argument( - '--max-iterations', metavar='ITERATIONS', type=int, help='max number of proof iterations to take' - ) return parser diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 7e8bc9604..3b30bcbf7 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -27,6 +27,8 @@ from pyk.utils import BugReport + from .options import ProveRSOpts + class KMIR(KProve, KRun): llvm_library_dir: Path | None @@ -68,24 +70,21 @@ def apr_proof_from_kast(self, id: str, kmir_kast: KInner, sort: str = 'Generated target_node = kcfg.create_node(rhs) return APRProof(id, kcfg, [], init_node.id, target_node.id, {}) - def prove_rs( - self, - rs_file: Path, - max_depth: int | None = None, - max_iterations: int | None = None, - ) -> APRProof: - smir_json = cargo_get_smir_json(rs_file) + def prove_rs(self, opts: ProveRSOpts) -> APRProof: + if not opts.rs_file.is_file(): + raise ValueError(f'Rust spec file does not exist: {opts.rs_file}') + smir_json = cargo_get_smir_json(opts.rs_file) parser = Parser(self.definition) parse_result = parser.parse_mir_json(smir_json, 'Pgm') assert parse_result is not None kmir_kast, _ = parse_result assert isinstance(kmir_kast, KInner) - apr_proof = self.apr_proof_from_kast(str(rs_file.stem), kmir_kast) + apr_proof = self.apr_proof_from_kast(str(opts.rs_file.stem), kmir_kast) with self.kcfg_explore('PROOF-TEST') as kcfg_explore: - prover = APRProver(kcfg_explore, execute_depth=max_depth) - prover.advance_proof(apr_proof, max_iterations=max_iterations) + prover = APRProver(kcfg_explore, execute_depth=opts.max_depth) + prover.advance_proof(apr_proof, max_iterations=opts.max_iterations) return apr_proof diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py new file mode 100644 index 000000000..548f1c879 --- /dev/null +++ b/kmir/src/kmir/options.py @@ -0,0 +1,118 @@ +from __future__ import annotations + +import logging +from dataclasses import dataclass +from pathlib import Path +from typing import TYPE_CHECKING + +from pyk.cli.args import LoggingOptions + +if TYPE_CHECKING: + from typing import Final + +_LOGGER: Final = logging.getLogger(__name__) +_LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s' + + +@dataclass +class KMirOpts(LoggingOptions): ... + + +@dataclass +class RunOpts(KMirOpts): + bin: str | None + file: str | None + depth: int + start_symbol: str + haskell_backend: bool + + +@dataclass +class ProveOpts(KMirOpts): + bug_report: Path | None + max_depth: int | None + max_iterations: int | None + + def __init__( + self, + bug_report: Path | None = None, + max_depth: int | None = None, + max_iterations: int | None = None, + ) -> None: + self.bug_report = bug_report + self.max_depth = max_depth + self.max_iterations = max_iterations + + +@dataclass +class GenSpecOpts(KMirOpts): + input_file: Path + output_file: Path | None + start_symbol: str + + def __init__(self, input_file: Path, output_file: Path | str | None, start_symbol: str) -> None: + self.input_file = input_file + if output_file is None: + self.output_file = None + else: + self.output_file = Path(output_file).resolve() + self.start_symbol = start_symbol + + +@dataclass +class ProveRSOpts(ProveOpts): + rs_file: Path + + def __init__( + self, + rs_file: Path, + bug_report: Path | None = None, + max_depth: int | None = None, + max_iterations: int | None = None, + ) -> None: + self.rs_file = rs_file + self.bug_report = bug_report + self.max_depth = max_depth + self.max_iterations = max_iterations + + +@dataclass +class ProveRunOpts(ProveOpts): + spec_file: Path + proof_dir: Path | None + include_labels: tuple[str, ...] | None + exclude_labels: tuple[str, ...] | None + reload: bool + + def __init__( + self, + spec_file: Path, + proof_dir: Path | str | None, + include_labels: str | None, + exclude_labels: str | None, + bug_report: Path | None = None, + max_depth: int | None = None, + max_iterations: int | None = None, + reload: bool = False, + ) -> None: + self.spec_file = spec_file + self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None + self.include_labels = tuple(include_labels.split(',')) if include_labels is not None else None + self.exclude_labels = tuple(exclude_labels.split(',')) if exclude_labels is not None else None + self.bug_report = bug_report + self.max_depth = max_depth + self.max_iterations = max_iterations + self.reload = reload + + +@dataclass +class ProveViewOpts(KMirOpts): + proof_dir: Path + id: str + + +@dataclass +class ProvePruneOpts(KMirOpts): + proof_dir: Path + id: str + node_id: int diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 8942ecef0..ca6277a05 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -11,6 +11,7 @@ from kmir.__main__ import GenSpecOpts, ProveRunOpts, _kmir_gen_spec, _kmir_prove_run from kmir.build import haskell_semantics, llvm_semantics +from kmir.options import ProveRSOpts from kmir.parse.parser import Parser if TYPE_CHECKING: @@ -437,7 +438,8 @@ def test_prove(spec: Path, tmp_path: Path, kmir: KMIR) -> None: ) def test_prove_rs(rs_file: Path, kmir: KMIR) -> None: should_fail = rs_file.stem.endswith('fail') - apr_proof = kmir.prove_rs(rs_file) + prove_rs_opts = ProveRSOpts(rs_file) + apr_proof = kmir.prove_rs(prove_rs_opts) if not should_fail: assert apr_proof.passed else: diff --git a/kmir/uv.lock b/kmir/uv.lock index cc7b0cbfe..9d71d30aa 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -488,7 +488,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.133" +version = "0.3.134" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index b6ecdf03f..d6f2cdd3f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.133 +0.3.134