Enable options for controlling booster execution (#2243)

* kevm-pyk/{utils,cli,__main__}: add options for quickly checking subsumption to KEVM proofs * kevm_pyk/{cli,__main__}: add options for controlling booster fallback reasons to CLI * Set Version: 1.0.408 * Set Version: 1.0.412 * Set Version: 1.0.417 * Set Version: 1.0.430 * kevm_pyk/{utils,cli,__main__}: use now upstreamed options for controlling backend * kevm-pyk/cli: better help * Set Version: 1.0.431 * Set Version: 1.0.444 * kevm-pyk/tests/{conftest,test_prove}: allow filtering by spec name * kevm-pyk/{cli,utils,__main__}: allow defaulting --fallback-on to None * kevm-pyk/__main__: turn all breaks off by default * Set Version: 1.0.446 * Update kevm-pyk/src/kevm_pyk/cli.py Co-authored-by: Andrei Văcaru <[email protected]> --------- Co-authored-by: devops <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]>
runtimeverification · Feb 7, 2024 · e2d5d20 · e2d5d20
1 parent ff65472
commit e2d5d20
Show file tree

Hide file tree

Showing 8 changed files with 105 additions and 9 deletions.
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.445"
+version = "1.0.446"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.445'
+VERSION: Final = '1.0.446'
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -52,6 +52,7 @@
     from pyk.kast.outer import KClaim
     from pyk.kcfg.kcfg import NodeIdLike
     from pyk.kcfg.tui import KCFGElem
+    from pyk.kore.rpc import FallbackReason
     from pyk.proof.proof import Proof
     from pyk.utils import BugReport
 
@@ -286,7 +287,7 @@ def exec_prove(
     workers: int = 1,
     break_every_step: bool = False,
     break_on_jumpi: bool = False,
-    break_on_calls: bool = True,
+    break_on_calls: bool = False,
     break_on_storage: bool = False,
     break_on_basic_blocks: bool = False,
     kore_rpc_command: str | Iterable[str] | None = None,
@@ -297,6 +298,11 @@ def exec_prove(
     failure_info: bool = True,
     auto_abstract_gas: bool = False,
     fail_fast: bool = False,
+    always_check_subsumption: bool = True,
+    fast_check_subsumption: bool = True,
+    fallback_on: Iterable[FallbackReason] | None = None,
+    interim_simplification: int | None = None,
+    post_exec_simplify: bool = True,
     **kwargs: Any,
 ) -> None:
     _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}')
@@ -367,6 +373,9 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]:
             smt_timeout=smt_timeout,
             smt_retry_limit=smt_retry_limit,
             trace_rewrites=trace_rewrites,
+            fallback_on=fallback_on,
+            interim_simplification=interim_simplification,
+            no_post_exec_simplify=(not post_exec_simplify),
         ) as kcfg_explore:
             proof_problem: Proof
             if is_functional(claim):
@@ -428,6 +437,8 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]:
                 ),
                 terminal_rules=KEVMSemantics.terminal_rules(break_every_step),
                 fail_fast=fail_fast,
+                always_check_subsumption=always_check_subsumption,
+                fast_check_subsumption=fast_check_subsumption,
             )
             end_time = time.time()
             _LOGGER.info(f'Proof timing {proof_problem.id}: {end_time - start_time}s')

diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py
@@ -5,6 +5,7 @@
 from typing import TYPE_CHECKING
 
 from pyk.cli.args import KCLIArgs
+from pyk.kore.rpc import FallbackReason
 
 from .utils import arg_pair_of
 
@@ -53,6 +54,32 @@ def kprove_args(self) -> ArgumentParser:
             default=[],
             help='Comma-separate list of equations to debug.',
         )
+        args.add_argument(
+            '--always-check-subsumption',
+            dest='always-check_subsumption',
+            default=True,
+            action='store_true',
+            help='Check subsumption even on non-terminal nodes.',
+        )
+        args.add_argument(
+            '--no-always-check-subsumption',
+            dest='always-check_subsumption',
+            action='store_false',
+            help='Do not check subsumption on non-terminal nodes.',
+        )
+        args.add_argument(
+            '--fast-check-subsumption',
+            dest='fast_check_subsumption',
+            default=True,
+            action='store_true',
+            help='Use fast-check on k-cell to determine subsumption.',
+        )
+        args.add_argument(
+            '--no-fast-check-subsumption',
+            dest='fast_check_subsumption',
+            action='store_false',
+            help='Do not use fast-check on k-cell to determine subsumption.',
+        )
         return args
 
     @cached_property
@@ -175,6 +202,31 @@ def rpc_args(self) -> ArgumentParser:
             action='store_true',
             help='Use the booster RPC server instead of kore-rpc.',
         )
+        args.add_argument(
+            '--fallback-on',
+            dest='fallback_on',
+            type=list_of(FallbackReason, delim=','),
+            help='Comma-separated reasons to fallback from booster to kore, only usable with --use-booster. Options [Branching,Aborted,Stuck].',
+        )
+        args.add_argument(
+            '--post-exec-simplify',
+            dest='post_exec_simplify',
+            default=True,
+            action='store_true',
+            help='Always simplify states with kore backend after booster execution, only usable with --use-booster.',
+        )
+        args.add_argument(
+            '--no-post-exec-simplify',
+            dest='post_exec_simplify',
+            action='store_false',
+            help='Do not simplify states with kore backend after booster execution, only usable with --use-booster.',
+        )
+        args.add_argument(
+            '--interim-simplification',
+            dest='interim_simplification',
+            type=int,
+            help='Max number of steps to execute before applying simplifier to term in booster backend, only usable with --use-booster.',
+        )
         args.add_argument(
             '--port',
             dest='port',

diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py
@@ -30,6 +30,7 @@
     from pyk.kast.outer import KClaim, KDefinition
     from pyk.kcfg import KCFG
     from pyk.kcfg.semantics import KCFGSemantics
+    from pyk.kore.rpc import FallbackReason
     from pyk.ktool.kprint import KPrint
     from pyk.ktool.kprove import KProve
     from pyk.proof.proof import Proof
@@ -101,13 +102,27 @@ def run_prover(
     abstract_node: Callable[[CTerm], CTerm] | None = None,
     fail_fast: bool = False,
     counterexample_info: bool = False,
+    always_check_subsumption: bool = False,
+    fast_check_subsumption: bool = False,
 ) -> bool:
     proof = proof
     prover: APRBMCProver | APRProver | EqualityProver
     if type(proof) is APRBMCProof:
-        prover = APRBMCProver(proof, kcfg_explore, counterexample_info=counterexample_info)
+        prover = APRBMCProver(
+            proof,
+            kcfg_explore,
+            counterexample_info=counterexample_info,
+            always_check_subsumption=always_check_subsumption,
+            fast_check_subsumption=fast_check_subsumption,
+        )
     elif type(proof) is APRProof:
-        prover = APRProver(proof, kcfg_explore, counterexample_info=counterexample_info)
+        prover = APRProver(
+            proof,
+            kcfg_explore,
+            counterexample_info=counterexample_info,
+            always_check_subsumption=always_check_subsumption,
+            fast_check_subsumption=fast_check_subsumption,
+        )
     elif type(proof) is EqualityProof:
         prover = EqualityProver(kcfg_explore=kcfg_explore, proof=proof)
     else:
@@ -313,6 +328,9 @@ def legacy_explore(
     trace_rewrites: bool = False,
     start_server: bool = True,
     maude_port: int | None = None,
+    fallback_on: Iterable[FallbackReason] | None = None,
+    interim_simplification: int | None = None,
+    no_post_exec_simplify: bool = False,
 ) -> Iterator[KCFGExplore]:
     if start_server:
         # Old way of handling KCFGExplore, to be removed
@@ -329,9 +347,9 @@ def legacy_explore(
             haskell_log_format=haskell_log_format,
             haskell_log_entries=haskell_log_entries,
             log_axioms_file=log_axioms_file,
-            fallback_on=None,
-            interim_simplification=None,
-            no_post_exec_simplify=None,
+            fallback_on=fallback_on,
+            interim_simplification=interim_simplification,
+            no_post_exec_simplify=no_post_exec_simplify,
         ) as server:
             with KoreClient('localhost', server.port, bug_report=bug_report, bug_report_id=id) as client:
                 yield KCFGExplore(

diff --git a/kevm-pyk/src/tests/conftest.py b/kevm-pyk/src/tests/conftest.py
@@ -21,6 +21,12 @@ def pytest_addoption(parser: Parser) -> None:
         default=False,
         help='Use the kore-rpc-booster binary instead of kore-rpc',
     )
+    parser.addoption(
+        '--spec-name',
+        default=None,
+        type=str,
+        help='Run only this specific specification (skip others)',
+    )
 
 
 @pytest.fixture
@@ -31,3 +37,8 @@ def update_expected_output(request: FixtureRequest) -> bool:
 @pytest.fixture(scope='session')
 def use_booster(request: FixtureRequest) -> bool:
     return request.config.getoption('--use-booster')
+
+
+@pytest.fixture(scope='session')
+def spec_name(request: FixtureRequest) -> str | None:
+    return request.config.getoption('--spec-name')
diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py
@@ -189,12 +189,16 @@ def test_pyk_prove(
     caplog: LogCaptureFixture,
     use_booster: bool,
     bug_report: BugReport | None,
+    spec_name: str | None,
 ) -> None:
     caplog.set_level(logging.INFO)
 
     if (not use_booster and spec_file in FAILING_PYK_TESTS) or (use_booster and spec_file in FAILING_BOOSTER_TESTS):
         pytest.skip()
 
+    if spec_name is not None and str(spec_file).find(spec_name) < 0:
+        pytest.skip()
+
     # Given
     log_file = tmp_path / 'log.txt'
     use_directory = tmp_path / 'kprove'

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.445
+1.0.446