diff --git a/docs/conf.py b/docs/conf.py index bde994e6e..30bf2f823 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.768' -release = '0.1.768' +version = '0.1.769' +release = '0.1.769' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index db3864d96..6a9b4158f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.768 +0.1.769 diff --git a/pyproject.toml b/pyproject.toml index f6d006b75..d5b33ecbc 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.768" +version = "0.1.769" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/regression-new/kprove-haskell/Makefile b/regression-new/kprove-haskell/Makefile index 0931f70ba..c2a4add4b 100644 --- a/regression-new/kprove-haskell/Makefile +++ b/regression-new/kprove-haskell/Makefile @@ -2,6 +2,7 @@ DEF=verif EXT=verif TESTDIR=. KOMPILE_BACKEND=haskell +KPROVE_FLAGS=--show-kcfg export KORE_EXEC_OPTS=--log-level error include ../include/ktest.mak diff --git a/regression-new/kprove-haskell/sum-spec.k.out b/regression-new/kprove-haskell/sum-spec.k.out index 3b312d930..35f9ea343 100644 --- a/regression-new/kprove-haskell/sum-spec.k.out +++ b/regression-new/kprove-haskell/sum-spec.k.out @@ -11,3 +11,126 @@ APRProof: 3b7070ca4603e18d26d032c0fe64dd71ffadc2c63dae9d57315e8e471a371bd3 bounded: 0 execution time: 0s Subproofs: 0 + +┌─ 1 (root, init) +│ +│ +│ addCounter ( N:Int ) +│ ~> K_CELL_fc656f08:K +│ +│ +│ C:Int +│ +│ +│ S:Int +│ +│ +│ GENERATEDCOUNTER_CELL_949ec677:Int +│ +│ +│ #And { true #Equals N:Int >=Int 0 } +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 3 +┃ │ +┃ │ +┃ │ addCounter ( N:Int +Int -1 ) +┃ │ ~> K_CELL_fc656f08:K +┃ │ +┃ │ +┃ │ C:Int +Int 1 +┃ │ +┃ │ +┃ │ S:Int +Int C:Int +┃ │ +┃ │ +┃ │ GENERATEDCOUNTER_CELL_949ec677:Int +┃ │ +┃ │ +┃ │ #And { true #Equals N:Int >Int 0 } +┃ │ #And { true #Equals N:Int >=Int 0 } +┃ │ +┃ │ (1 step) +┃ ├─ 5 +┃ │ +┃ │ +┃ │ K_CELL_fc656f08:K +┃ │ +┃ │ +┃ │ ?_COUNTER_CELL_af8c44a5:Int +┃ │ +┃ │ +┃ │ S:Int +Int C:Int +Int N:Int +Int -1 *Int C:Int +Int 1 +Int N:Int +Int -2 *Int N:Int +Int -1 /Int 2 +┃ │ +┃ │ +┃ │ ?_GENERATEDCOUNTER_CELL_5e3e01ba:Int +┃ │ +┃ │ +┃ │ #And { true #Equals N:Int >Int 0 } +┃ │ #And { true #Equals N:Int >=Int 0 } +┃ │ #And { true #Equals N:Int +Int -1 >=Int 0 } +┃ │ +┃ ┊ constraint: OMITTED CONSTRAINT +┃ ┊ subst: OMITTED SUBST +┃ └─ 2 (leaf, target) +┃ +┃ +┃ K_CELL_fc656f08:K ~> .K +┃ +┃ +┃ COUNTER_CELL_af8c44a5:Int +┃ +┃ +┃ ?S:Int +┃ +┃ +┃ GENERATEDCOUNTER_CELL_5e3e01ba:Int +┃ +┃ +┃ #And { true #Equals N:Int >=Int 0 } +┃ #And { true #Equals ?S:Int ==Int S:Int +Int N:Int *Int C:Int +Int N:Int -Int 1 *Int N:Int /Int 2 } +┃ +┗━━┓ + │ + ├─ 4 + │ + │ + │ K_CELL_fc656f08:K + │ + │ + │ C:Int + │ + │ + │ S:Int + │ + │ + │ GENERATEDCOUNTER_CELL_949ec677:Int + │ + │ + │ #And { N:Int #Equals 0 } + │ + ┊ constraint: OMITTED CONSTRAINT + ┊ subst: OMITTED SUBST + └─ 2 (leaf, target) + + + K_CELL_fc656f08:K ~> .K + + + COUNTER_CELL_af8c44a5:Int + + + ?S:Int + + + GENERATEDCOUNTER_CELL_5e3e01ba:Int + + + #And { true #Equals N:Int >=Int 0 } + #And { true #Equals ?S:Int ==Int S:Int +Int N:Int *Int C:Int +Int N:Int -Int 1 *Int N:Int /Int 2 } + + + + diff --git a/regression-new/kprove-haskell/test-fail-spec.k.out b/regression-new/kprove-haskell/test-fail-spec.k.out index 9611617f3..d69b3be35 100644 --- a/regression-new/kprove-haskell/test-fail-spec.k.out +++ b/regression-new/kprove-haskell/test-fail-spec.k.out @@ -26,3 +26,40 @@ Failing nodes: Failed to generate a model. Join the Runtime Verification Discord server for support: https://discord.gg/CurfmXNtbN + +┌─ 1 (root, stuck, leaf, init) +│ +│ +│ doIt ( -3 ) +│ ~> K_CELL_fc656f08:K +│ +│ +│ COUNTER_CELL +│ +│ +│ SUM_CELL +│ +│ +│ GENERATEDCOUNTER_CELL_c84b0b5f:Int +│ +│ + +┌─ 2 (root, leaf, target) +│ +│ +│ doIt ( 0 ) +│ ~> K_CELL_fc656f08:K +│ +│ +│ COUNTER_CELL +│ +│ +│ SUM_CELL +│ +│ +│ GENERATEDCOUNTER_CELL_6de8d71b:Int +│ +│ + + + diff --git a/regression-new/kprove-haskell/test-spec.k.out b/regression-new/kprove-haskell/test-spec.k.out index e527e16de..57c171d46 100644 --- a/regression-new/kprove-haskell/test-spec.k.out +++ b/regression-new/kprove-haskell/test-spec.k.out @@ -11,3 +11,61 @@ APRProof: 8b72c409e7e4e821e957233b93c93d850e4c2f79fa4be4a12f32ab064030dce7 bounded: 0 execution time: 0s Subproofs: 0 + +┌─ 1 (root, init) +│ +│ +│ doIt ( 3 ) +│ ~> K_CELL_fc656f08:K +│ +│ +│ COUNTER_CELL +│ +│ +│ SUM_CELL +│ +│ +│ GENERATEDCOUNTER_CELL_c84b0b5f:Int +│ +│ +│ +│ (3 steps) +├─ 3 +│ +│ +│ doIt ( 0 ) +│ ~> K_CELL_fc656f08:K +│ +│ +│ COUNTER_CELL:Int +│ +│ +│ SUM_CELL:Int +│ +│ +│ GENERATEDCOUNTER_CELL_c84b0b5f:Int +│ +│ +│ +┊ constraint: true +┊ subst: GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int +└─ 2 (leaf, target) + + + doIt ( 0 ) + ~> K_CELL_fc656f08:K + + + COUNTER_CELL + + + SUM_CELL + + + GENERATEDCOUNTER_CELL_6de8d71b:Int + + + + + + diff --git a/src/pyk/__main__.py b/src/pyk/__main__.py index 9a7b8e21c..c5e822c0e 100644 --- a/src/pyk/__main__.py +++ b/src/pyk/__main__.py @@ -13,7 +13,7 @@ from .cli.args import KCLIArgs from .cli.pyk import generate_options -from .cli.utils import LOG_FORMAT, dir_path, file_path, loglevel +from .cli.utils import LOG_FORMAT, dir_path, loglevel from .coverage import get_rule_by_id, strip_coverage_logger from .cterm import CTerm from .kast.inner import KInner @@ -30,14 +30,14 @@ from .kore.parser import KoreParser from .kore.rpc import ExecuteResult, StopReason from .kore.syntax import Pattern, kore_term -from .ktool import TypeInferenceMode from .ktool.kompile import Kompile, KompileBackend from .ktool.kprint import KPrint from .ktool.kprove import KProve from .ktool.krun import KRun from .prelude.k import GENERATED_TOP_CELL from .prelude.ml import is_top, mlAnd, mlOr -from .proof.reachability import APRFailureInfo +from .proof.reachability import APRFailureInfo, APRProof +from .proof.show import APRProofNodePrinter, APRProofShow from .utils import check_file_path, ensure_dir_path, exit_with_process_error if TYPE_CHECKING: @@ -248,17 +248,32 @@ def exec_prove(options: ProveOptions) -> None: _LOGGER.info(f'Using kompiled directory: {kompiled_directory}.') else: kompiled_directory = options.definition_dir - kprove = KProve(kompiled_directory) - proofs = kprove.prove_rpc(options=options) + kprove = KProve(kompiled_directory, use_directory=options.temp_directory) + try: + proofs = kprove.prove_rpc(options=options) + except RuntimeError as err: + _, _, _, cpe = err.args + exit_with_process_error(cpe) for proof in sorted(proofs, key=lambda p: p.id): print('\n'.join(proof.summary.lines)) if proof.failed and options.failure_info: failure_info = proof.failure_info if type(failure_info) is APRFailureInfo: print('\n'.join(failure_info.print())) + if options.show_kcfg and type(proof) is APRProof: + node_printer = APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False) + show = APRProofShow(kprove, node_printer=node_printer) + print('\n'.join(show.show(proof))) sys.exit(len([p.id for p in proofs if not p.passed])) +def exec_show(options: ProveOptions) -> None: + options.max_iterations = 0 + options.show_kcfg = True + options.failure_info = True + exec_prove(options) + + def exec_kompile(options: KompileCommandOptions) -> None: main_file = Path(options.main_file) check_file_path(main_file) @@ -453,15 +468,39 @@ def create_argument_parser() -> ArgumentParser: prove_args = pyk_args_command.add_parser( 'prove', help='Prove an input specification (using RPC based prover).', - parents=[k_cli_args.logging_args], + parents=[k_cli_args.logging_args, k_cli_args.spec_args], ) - prove_args.add_argument('spec_file', type=file_path, help='File with the specification module.') - prove_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.') - prove_args.add_argument('--spec-module', dest='spec_module', type=str, help='Module with claims to be proven.') prove_args.add_argument( - '--type-inference-mode', type=TypeInferenceMode, help='Mode for doing K rule type inference in.' + '--failure-info', + default=None, + action='store_true', + help='Print out more information about proof failures.', ) prove_args.add_argument( + '--show-kcfg', + default=None, + action='store_true', + help='Display the resulting proof KCFG.', + ) + prove_args.add_argument( + '--max-depth', + default=None, + type=int, + help='Maximum number of steps to take in symbolic execution per basic block.', + ) + prove_args.add_argument( + '--max-iterations', + default=None, + type=int, + help='Maximum number of KCFG explorations to take in attempting to discharge proof.', + ) + + show_args = pyk_args_command.add_parser( + 'show', + help='Display the status of a given proof.', + parents=[k_cli_args.logging_args, k_cli_args.spec_args], + ) + show_args.add_argument( '--failure-info', default=None, action='store_true', diff --git a/src/pyk/cli/args.py b/src/pyk/cli/args.py index d0891ded7..017b54843 100644 --- a/src/pyk/cli/args.py +++ b/src/pyk/cli/args.py @@ -8,9 +8,11 @@ from ..ktool.kompile import KompileBackend, LLVMKompileType, TypeInferenceMode, Warnings from .cli import Options -from .utils import bug_report_arg, ensure_dir_path, file_path +from .utils import bug_report_arg, dir_path, ensure_dir_path, file_path if TYPE_CHECKING: + from collections.abc import Iterable + from ..utils import BugReport @@ -82,24 +84,28 @@ def default() -> dict[str, Any]: class SaveDirOptions(Options): save_directory: Path | None + temp_directory: Path | None @staticmethod def default() -> dict[str, Any]: return { 'save_directory': None, + 'temp_directory': None, } class SpecOptions(SaveDirOptions): spec_file: Path - claim_labels: list[str] | None - exclude_claim_labels: list[str] + spec_module: str | None + claim_labels: Iterable[str] | None + exclude_claim_labels: Iterable[str] | None @staticmethod def default() -> dict[str, Any]: return { + 'spec_module': None, 'claim_labels': None, - 'exclude_claim_labels': [], + 'exclude_claim_labels': None, } @@ -387,7 +393,8 @@ def definition_args(self) -> ArgumentParser: def spec_args(self) -> ArgumentParser: args = ArgumentParser(add_help=False) args.add_argument('spec_file', type=file_path, help='Path to spec file.') - args.add_argument('--save-directory', type=ensure_dir_path, help='Path to where CFGs are stored.') + args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.') + args.add_argument('--spec-module', dest='spec_module', type=str, help='Module with claims to be proven.') args.add_argument( '--claim', type=str, @@ -402,4 +409,23 @@ def spec_args(self) -> ArgumentParser: action='append', help='Skip listed claims, MODULE_NAME.claim-id', ) + args.add_argument( + '--type-inference-mode', + dest='type_inference_mode', + type=TypeInferenceMode, + help='Mode for doing K rule type inference in.', + ) + args.add_argument( + '--save-directory', + default=None, + type=ensure_dir_path, + help='Directory to save proof artifacts at for reuse.', + ) + args.add_argument( + '--temp-directory', + dest='temp_directory', + default=None, + type=ensure_dir_path, + help='Directory to save intermediate temporaries to.', + ) return args diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index 97a445d33..3361d685d 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -11,6 +11,8 @@ KompileOptions, LoggingOptions, OutputFileOptions, + SaveDirOptions, + SpecOptions, WarningOptions, ) @@ -42,6 +44,8 @@ def generate_options(args: dict[str, Any]) -> LoggingOptions: return ProveLegacyOptions(args) case 'prove': return ProveOptions(args) + case 'show': + return ProveOptions(args) case 'kompile': return KompileCommandOptions(args) case 'run': @@ -121,20 +125,23 @@ def default() -> dict[str, Any]: } -class ProveOptions(LoggingOptions): - spec_file: Path +class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions): definition_dir: Path | None - spec_module: str | None type_inference_mode: TypeInferenceMode | None failure_info: bool + max_depth: int | None + max_iterations: int | None + show_kcfg: bool @staticmethod def default() -> dict[str, Any]: return { 'definition_dir': None, - 'spec_module': None, 'type_inference_mode': None, 'failure_info': False, + 'max_depth': None, + 'max_iterations': None, + 'show_kcfg': False, } diff --git a/src/pyk/ktool/kprint.py b/src/pyk/ktool/kprint.py index 422a91054..92c065e61 100644 --- a/src/pyk/ktool/kprint.py +++ b/src/pyk/ktool/kprint.py @@ -211,11 +211,12 @@ def __init__( self._bug_report = bug_report @contextmanager - def _temp_file(self, suffix: str | None = None) -> Iterator[_TemporaryFileWrapper]: + def _temp_file(self, prefix: str | None = None, suffix: str | None = None) -> Iterator[_TemporaryFileWrapper]: with NamedTemporaryFile( 'w', dir=self.use_directory, delete=not self.use_directory, + prefix=prefix, suffix=suffix, ) as ntf: _LOGGER.info(f'Created temporary file: {ntf.name}') diff --git a/src/pyk/ktool/kprove.py b/src/pyk/ktool/kprove.py index 5dd5ff55e..ef7179f48 100644 --- a/src/pyk/ktool/kprove.py +++ b/src/pyk/ktool/kprove.py @@ -105,7 +105,7 @@ def _kprove( return run_process(run_args, logger=_LOGGER, env=env, check=check) except CalledProcessError as err: raise RuntimeError( - f'Command kprove exited with code {err.returncode} for: {spec_file}', err.stdout, err.stderr + f'Command kprove exited with code {err.returncode} for: {spec_file}', err.stdout, err.stderr, err ) from err @@ -285,53 +285,72 @@ def prove_claim_rpc( fallback_on: Iterable[FallbackReason] | None = None, interim_simplification: int | None = None, no_post_exec_simplify: bool = False, + max_depth: int | None = None, + save_directory: Path | None = None, + max_iterations: int | None = None, ) -> Proof: - with cterm_symbolic( - self.definition, - self.kompiled_kore, - self.definition_dir, - id=id, - port=port, - kore_rpc_command=kore_rpc_command, - llvm_definition_dir=llvm_definition_dir, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - smt_tactic=smt_tactic, - bug_report=bug_report, - haskell_log_format=haskell_log_format, - haskell_log_entries=haskell_log_entries, - log_axioms_file=log_axioms_file, - trace_rewrites=trace_rewrites, - start_server=start_server, - maude_port=maude_port, - fallback_on=fallback_on, - interim_simplification=interim_simplification, - no_post_exec_simplify=no_post_exec_simplify, - ) as cts: - kcfg_explore = KCFGExplore(cts, kcfg_semantics=kcfg_semantics) - proof: Proof - prover: Prover - lhs_top = extract_lhs(claim.body) - if type(lhs_top) is KApply and self.definition.symbols[lhs_top.label.name] in self.definition.functions: - proof = EqualityProof.from_claim(claim, self.definition) - prover = ImpliesProver(proof, kcfg_explore) - else: - proof = APRProof.from_claim(self.definition, claim, {}) - prover = APRProver(proof, kcfg_explore) - prover.advance_proof() - if proof.passed: - _LOGGER.info(f'Proof passed: {proof.id}') - elif proof.failed: - _LOGGER.info(f'Proof failed: {proof.id}') - else: - _LOGGER.info(f'Proof pending: {proof.id}') - return proof + proof: Proof + prover: Prover + lhs_top = extract_lhs(claim.body) + is_functional_claim = ( + type(lhs_top) is KApply and self.definition.symbols[lhs_top.label.name] in self.definition.functions + ) + + if is_functional_claim: + proof = EqualityProof.from_claim(claim, self.definition, proof_dir=save_directory) + if save_directory is not None and EqualityProof.proof_data_exists(proof.id, save_directory): + _LOGGER.info(f'Reloading from disk {proof.id}: {save_directory}') + proof = EqualityProof.read_proof_data(save_directory, proof.id) + + else: + proof = APRProof.from_claim(self.definition, claim, {}, proof_dir=save_directory) + if save_directory is not None and APRProof.proof_data_exists(proof.id, save_directory): + _LOGGER.info(f'Reloading from disk {proof.id}: {save_directory}') + proof = APRProof.read_proof_data(save_directory, proof.id) + + if not proof.passed and (max_iterations is None or max_iterations > 0): + with cterm_symbolic( + self.definition, + self.kompiled_kore, + self.definition_dir, + id=id, + port=port, + kore_rpc_command=kore_rpc_command, + llvm_definition_dir=llvm_definition_dir, + smt_timeout=smt_timeout, + smt_retry_limit=smt_retry_limit, + smt_tactic=smt_tactic, + bug_report=bug_report, + haskell_log_format=haskell_log_format, + haskell_log_entries=haskell_log_entries, + log_axioms_file=log_axioms_file, + trace_rewrites=trace_rewrites, + start_server=start_server, + maude_port=maude_port, + fallback_on=fallback_on, + interim_simplification=interim_simplification, + no_post_exec_simplify=no_post_exec_simplify, + ) as cts: + kcfg_explore = KCFGExplore(cts, kcfg_semantics=kcfg_semantics) + if is_functional_claim: + assert type(proof) is EqualityProof + prover = ImpliesProver(proof, kcfg_explore) + else: + assert type(proof) is APRProof + prover = APRProver(proof, kcfg_explore, execute_depth=max_depth) + prover.advance_proof(max_iterations=max_iterations) + + if proof.passed: + _LOGGER.info(f'Proof passed: {proof.id}') + elif proof.failed: + _LOGGER.info(f'Proof failed: {proof.id}') + else: + _LOGGER.info(f'Proof pending: {proof.id}') + return proof def prove_rpc( self, options: ProveOptions, - claim_labels: Iterable[str] | None = None, - exclude_claim_labels: Iterable[str] | None = None, kcfg_semantics: KCFGSemantics | None = None, id: str | None = None, port: int | None = None, @@ -372,13 +391,16 @@ def _prove_claim_rpc(claim: KClaim) -> Proof: fallback_on=fallback_on, interim_simplification=interim_simplification, no_post_exec_simplify=no_post_exec_simplify, + max_depth=options.max_depth, + save_directory=options.save_directory, + max_iterations=options.max_iterations, ) all_claims = self.get_claims( options.spec_file, spec_module_name=options.spec_module, - claim_labels=claim_labels, - exclude_claim_labels=exclude_claim_labels, + claim_labels=options.claim_labels, + exclude_claim_labels=options.exclude_claim_labels, type_inference_mode=options.type_inference_mode, ) if all_claims is None: @@ -393,7 +415,7 @@ def get_claim_modules( md_selector: str | None = None, type_inference_mode: TypeInferenceMode | None = None, ) -> KFlatModuleList: - with self._temp_file() as ntf: + with self._temp_file(prefix=f'{spec_file.name}.parsed.json.') as ntf: _kprove( spec_file=spec_file, kompiled_dir=self.definition_dir, diff --git a/src/tests/integration/ktool/test_imp.py b/src/tests/integration/ktool/test_imp.py index bfc23b5d7..16079cadb 100644 --- a/src/tests/integration/ktool/test_imp.py +++ b/src/tests/integration/ktool/test_imp.py @@ -194,9 +194,9 @@ def test_prove_rpc( { 'spec_file': Path(spec_file), 'spec_module': spec_module, + 'claim_labels': [claim_id], } ), - claim_labels=[claim_id], kcfg_semantics=ImpSemantics(kprove.definition), ) )