From c908154f496a24dea567b0554ec4abfa93459bd3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Burak=20Bilge=20Yal=C3=A7=C4=B1nkaya?= Date: Fri, 13 Sep 2024 14:23:18 +0300 Subject: [PATCH] Add bug report support (#39) * Add `komet prove` bug report option * Set Version: 0.1.32 --------- Co-authored-by: devops --- package/version | 2 +- pyproject.toml | 2 +- src/komet/kasmer.py | 18 ++++++++++++++---- src/komet/komet.py | 10 +++++++--- src/komet/proof.py | 14 ++++++++++---- 5 files changed, 33 insertions(+), 13 deletions(-) diff --git a/package/version b/package/version index db7a480..28d0075 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.31 +0.1.32 diff --git a/pyproject.toml b/pyproject.toml index 8f0dcfc..fee36f2 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.31" +version = "0.1.32" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/komet/kasmer.py b/src/komet/kasmer.py index 4bef274..0507724 100644 --- a/src/komet/kasmer.py +++ b/src/komet/kasmer.py @@ -48,6 +48,7 @@ from pyk.kast.inner import KInner from pyk.kore.syntax import Pattern from pyk.proof import APRProof + from pyk.utils import BugReport from .utils import SorobanDefinition @@ -204,7 +205,12 @@ def make_steps(*args: KInner) -> Pattern: fuzz(self.definition.path, template_config_kore, template_subst, check_exit_code=True) def run_prove( - self, conf: KInner, subst: dict[str, KInner], binding: ContractBinding, proof_dir: Path | None = None + self, + conf: KInner, + subst: dict[str, KInner], + binding: ContractBinding, + proof_dir: Path | None = None, + bug_report: BugReport | None = None, ) -> APRProof: from_acct = account_id(b'test-account') to_acct = contract_id(b'test-contract') @@ -228,7 +234,7 @@ def make_steps(*args: KInner) -> KInner: claim, _ = cterm_build_claim(name, lhs, rhs) - return run_claim(name, claim, proof_dir) + return run_claim(name, claim, proof_dir, bug_report) def deploy_and_run(self, contract_wasm: Path, child_wasms: tuple[Path, ...]) -> None: """Run all of the tests in a soroban test contract. @@ -261,7 +267,11 @@ def deploy_and_run(self, contract_wasm: Path, child_wasms: tuple[Path, ...]) -> print(' Test passed.') def deploy_and_prove( - self, contract_wasm: Path, child_wasms: tuple[Path, ...], proof_dir: Path | None = None + self, + contract_wasm: Path, + child_wasms: tuple[Path, ...], + proof_dir: Path | None = None, + bug_report: BugReport | None = None, ) -> None: """Prove all of the tests in a soroban test contract. @@ -283,7 +293,7 @@ def deploy_and_prove( for binding in bindings: if not binding.name.startswith('test_'): continue - proof = self.run_prove(conf, subst, binding, proof_dir) + proof = self.run_prove(conf, subst, binding, proof_dir, bug_report) if proof.status == ProofStatus.FAILED: raise KSorobanError(proof.summary) diff --git a/src/komet/komet.py b/src/komet/komet.py index ed599c0..fd1fc6d 100644 --- a/src/komet/komet.py +++ b/src/komet/komet.py @@ -9,6 +9,7 @@ from tempfile import NamedTemporaryFile from typing import TYPE_CHECKING +from pyk.cli.args import bug_report_arg from pyk.cli.utils import file_path from pyk.kdist import kdist from pyk.ktool.kprint import KAstOutput, _kast @@ -25,6 +26,8 @@ from collections.abc import Iterator from subprocess import CompletedProcess + from pyk.utils import BugReport + sys.setrecursionlimit(4000) @@ -48,7 +51,7 @@ def main() -> None: elif args.command == 'prove': if args.prove_command is None or args.prove_command == 'run': wasm = Path(args.wasm.name) if args.wasm is not None else None - _exec_prove_run(wasm=wasm, proof_dir=args.proof_dir) + _exec_prove_run(wasm=wasm, proof_dir=args.proof_dir, bug_report=args.bug_report) if args.prove_command == 'view': assert args.proof_dir is not None _exec_prove_view(proof_dir=args.proof_dir, id=args.id) @@ -98,7 +101,7 @@ def _exec_test(*, wasm: Path | None) -> None: sys.exit(0) -def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None) -> None: +def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None, bug_report: BugReport | None = None) -> None: kasmer = Kasmer(symbolic_definition) child_wasms: tuple[Path, ...] = () @@ -107,7 +110,7 @@ def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None) -> None: wasm = kasmer.build_soroban_contract(Path.cwd()) child_wasms = _read_config_file() - kasmer.deploy_and_prove(wasm, child_wasms, proof_dir) + kasmer.deploy_and_prove(wasm, child_wasms, proof_dir, bug_report) sys.exit(0) @@ -172,6 +175,7 @@ def _argument_parser() -> ArgumentParser: ) prove_parser.add_argument('--wasm', type=FileType('r'), help='Prove a specific contract wasm file instead') prove_parser.add_argument('--proof-dir', type=ensure_dir_path, default=None, help='Output directory for proofs') + prove_parser.add_argument('--bug-report', type=bug_report_arg, default=None, help='Bug report directory for proofs') prove_parser.add_argument('--id', help='Name of the test function in the testing contract') return parser diff --git a/src/komet/proof.py b/src/komet/proof.py index f7300c2..7b1a581 100644 --- a/src/komet/proof.py +++ b/src/komet/proof.py @@ -15,24 +15,30 @@ from pathlib import Path from pyk.kast.outer import KClaim + from pyk.utils import BugReport @contextmanager -def _explore_context() -> Iterator[KCFGExplore]: - with cterm_symbolic(definition=symbolic_definition.kdefinition, definition_dir=symbolic_definition.path) as cts: +def _explore_context(id: str, bug_report: BugReport | None) -> Iterator[KCFGExplore]: + with cterm_symbolic( + definition=symbolic_definition.kdefinition, + definition_dir=symbolic_definition.path, + id=id if bug_report else None, + bug_report=bug_report, + ) as cts: yield KCFGExplore(cts) class SorobanSemantics(DefaultSemantics): ... -def run_claim(id: str, claim: KClaim, proof_dir: Path | None = None) -> APRProof: +def run_claim(id: str, claim: KClaim, proof_dir: Path | None = None, bug_report: BugReport | None = None) -> APRProof: if proof_dir is not None and APRProof.proof_data_exists(id, proof_dir): proof = APRProof.read_proof_data(proof_dir, id) else: proof = APRProof.from_claim(symbolic_definition.kdefinition, claim=claim, logs={}, proof_dir=proof_dir) - with _explore_context() as kcfg_explore: + with _explore_context(id, bug_report) as kcfg_explore: prover = APRProver(kcfg_explore) prover.advance_proof(proof)