Remove option to skip simplifing init nodes (#2138)

* kevm-pyk/{cli,__main__}: remove options --[no-]simplify-init

* kevm-pyk/__main__: setup temporary directory for saving proofs if needed

* Set Version: 1.0.328

* Set Version: 1.0.329

* Set Version: 1.0.331

* Set Version: 1.0.332

* Set Version: 1.0.333

* kevm-pyk/test_prove: remove kserver

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.332"
+version = "1.0.333"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.332'
+VERSION: Final = '1.0.333'

kevm-pyk/src/kevm_pyk/__main__.py

@@ -6,6 +6,7 @@
 import logging
 import os
 import sys
+import tempfile
 import time
 from argparse import ArgumentParser
 from dataclasses import dataclass
@@ -278,7 +279,6 @@ def exec_prove(
     max_depth: int = 1000,
     max_iterations: int | None = None,
     workers: int = 1,
-    simplify_init: bool = True,
     break_every_step: bool = False,
     break_on_jumpi: bool = False,
     break_on_calls: bool = True,
@@ -305,6 +305,9 @@ def exec_prove(
     if smt_retry_limit is None:
         smt_retry_limit = 10
 
+    if save_directory is None:
+        save_directory = Path(tempfile.TemporaryDirectory().name)
+
     kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=bug_report)
 
     include_dirs = [Path(include) for include in includes]
@@ -388,18 +391,13 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]:
                     _LOGGER.info(f'Computing definedness constraint for initial node: {claim.label}')
                     new_init = kcfg_explore.cterm_assume_defined(new_init)
 
-                    if simplify_init:
-                        _LOGGER.info(f'Simplifying initial and target node: {claim.label}')
-                        new_init, _ = kcfg_explore.cterm_simplify(new_init)
-                        new_target, _ = kcfg_explore.cterm_simplify(new_target)
-                        if CTerm._is_bottom(new_init.kast):
-                            raise ValueError(
-                                'Simplifying initial node led to #Bottom, are you sure your LHS is defined?'
-                            )
-                        if CTerm._is_top(new_target.kast):
-                            raise ValueError(
-                                'Simplifying target node led to #Bottom, are you sure your RHS is defined?'
-                            )
+                    _LOGGER.info(f'Simplifying initial and target node: {claim.label}')
+                    new_init, _ = kcfg_explore.cterm_simplify(new_init)
+                    new_target, _ = kcfg_explore.cterm_simplify(new_target)
+                    if CTerm._is_bottom(new_init.kast):
+                        raise ValueError('Simplifying initial node led to #Bottom, are you sure your LHS is defined?')
+                    if CTerm._is_top(new_target.kast):
+                        raise ValueError('Simplifying target node led to #Bottom, are you sure your RHS is defined?')
 
                     kcfg.replace_node(init_node_id, new_init)
                     kcfg.replace_node(target_node_id, new_target)

kevm-pyk/src/kevm_pyk/cli.py

@@ -210,19 +210,6 @@ def explore_args(self) -> ArgumentParser:
             action='store_false',
             help='Do not store a node for every EVM call made.',
         )
-        args.add_argument(
-            '--simplify-init',
-            dest='simplify_init',
-            default=True,
-            action='store_true',
-            help='Simplify the initial and target states at startup.',
-        )
-        args.add_argument(
-            '--no-simplify-init',
-            dest='simplify_init',
-            action='store_false',
-            help='Do not simplify the initial and target states at startup.',
-        )
         args.add_argument(
             '--max-depth',
             dest='max_depth',

kevm-pyk/src/tests/integration/test_prove.py

@@ -2,14 +2,10 @@
 
 import dataclasses
 import logging
-import subprocess
 import sys
-from pathlib import Path
 from typing import TYPE_CHECKING, NamedTuple
 
-import inotify.adapters  # type: ignore
 import pytest
-from filelock import FileLock
 from pyk.cterm import CTerm
 from pyk.proof.reachability import APRProof
 
@@ -21,7 +17,8 @@
 from ..utils import REPO_ROOT
 
 if TYPE_CHECKING:
-    from collections.abc import Callable, Iterator
+    from collections.abc import Callable
+    from pathlib import Path
     from typing import Any, Final
 
     from pyk.utils import BugReport
@@ -134,34 +131,8 @@ def __call__(self, output_dir: Path) -> Path:
         )
 
 
-@pytest.fixture(scope='session')
-def kserver(tmp_path_factory: TempPathFactory, worker_id: str) -> Iterator[Path]:
-    if worker_id == 'master':
-        root_tmp_dir = tmp_path_factory.getbasetemp()
-    else:
-        root_tmp_dir = tmp_path_factory.getbasetemp().parent
-
-    lock = root_tmp_dir / 'kserver'
-    kserver = None
-    kserver_dir = Path.home() / '.kserver'
-    kserver_dir.mkdir(exist_ok=True)
-    with FileLock(str(lock) + '.lock'):
-        if not lock.exists():
-            i = inotify.adapters.Inotify()
-            i.add_watch(str(Path.home() / '.kserver'))
-            kserver = subprocess.Popen(['kserver'], stdout=subprocess.PIPE)
-            for _, types, _, filename in i.event_gen(yield_nones=False):
-                if filename == 'socket' and 'IN_CREATE' in types:
-                    break
-            lock.touch()
-
-    yield lock
-    if kserver is not None:
-        kserver.terminate()
-
-
 @pytest.fixture(scope='module')
-def kompiled_target_for(tmp_path_factory: TempPathFactory, kserver: Path) -> Callable[[Path, bool], Path]:
+def kompiled_target_for(tmp_path_factory: TempPathFactory) -> Callable[[Path, bool], Path]:
     cache_dir = tmp_path_factory.mktemp('target')
     cache: dict[Target, Path] = {}
 
@@ -241,7 +212,6 @@ def test_pyk_prove(
             definition_dir=definition_dir,
             includes=[str(include_dir) for include_dir in config.INCLUDE_DIRS],
             save_directory=use_directory,
-            max_depth=300,  # Workaround for ecrecover00-siginvalid issue
             smt_timeout=300,
             smt_retry_limit=10,
             md_selector='foo',  # TODO Ignored flag, this is to avoid KeyError

package/version

@@ -1 +1 @@
-1.0.332
+1.0.333