From f14d29c829417a6be1a04789f6201af1981d7c20 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 1 Nov 2023 13:02:14 -0600 Subject: [PATCH] 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 Co-authored-by: rv-jenkins --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- kevm-pyk/src/kevm_pyk/__main__.py | 24 ++++++------- kevm-pyk/src/kevm_pyk/cli.py | 13 ------- kevm-pyk/src/tests/integration/test_prove.py | 36 ++------------------ package/version | 2 +- 6 files changed, 17 insertions(+), 62 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 3188c4b38d..58bb5b9401 100644 --- 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.332" +version = "1.0.333" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index d0cab81dab..c22ed709f8 100644 --- 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.332' +VERSION: Final = '1.0.333' diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index a874f750b0..d649e0222b 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/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) diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 956ccf464f..14633bd3a1 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/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', diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index f98102dd48..a70c539f47 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/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 diff --git a/package/version b/package/version index 51dda02714..50b74d4d07 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.332 +1.0.333