Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Pyk: Wrap fuzzing in an interface #4492

Merged
merged 10 commits into from
Jul 3, 2024
Prev Previous commit
Next Next commit
Don't try to maintain the recursion limit. Our traversals are no longer
deeply nested.
  • Loading branch information
gtrepta committed Jul 3, 2024
commit 71bc069f479a88aa7d5bbf51aec5a201191bc019
13 changes: 0 additions & 13 deletions pyk/src/pyk/ktool/kfuzz.py
Original file line number Diff line number Diff line change
@@ -1,11 +1,8 @@
from __future__ import annotations

import sys
import warnings
from typing import TYPE_CHECKING

from hypothesis import Phase, given, settings
from hypothesis.errors import HypothesisWarning
from hypothesis.strategies import fixed_dictionaries, integers

from ..kore.parser import KoreParser
@@ -23,9 +20,6 @@
from ..kore.syntax import Pattern


REC_LIMIT = 10**7


class KFuzz:
"""Interface for fuzzing over property tests in K."""

@@ -108,10 +102,6 @@ def _fuzz(
raise RuntimeError('Must pass one of check_func or check_exit_code, and not both!')

def test(subst_case: Mapping[EVar, Pattern]) -> None:
if sys.getrecursionlimit() < REC_LIMIT:
# Reset the recursion limit, hypothesis changes it.
sys.setrecursionlimit(REC_LIMIT)

def sub(p: Pattern) -> Pattern:
if isinstance(p, EVar) and p in subst_case:
return subst_case[p]
@@ -130,9 +120,6 @@ def sub(p: Pattern) -> Pattern:

strat: SearchStrategy = fixed_dictionaries(subst_strategy)

# Suppress warnings from hypothesis about changing the recursion limit
warnings.filterwarnings('ignore', message='The recursion limit', category=HypothesisWarning, append=True)

# Default settings for hypothesis
hypothesis_args.setdefault('deadline', 5000)
hypothesis_args.setdefault('phases', (Phase.explicit, Phase.reuse, Phase.generate))
Loading