Pyk: Wrap fuzzing in an interface

pyk/src/pyk/ktool/kfuzz.py

@@ -1,16 +1,16 @@
 from __future__ import annotations
 
+import sys
+import warnings
 from typing import TYPE_CHECKING
 
-from hypothesis import Phase, Verbosity, given, settings
-from hypothesis.strategies import builds, fixed_dictionaries, integers
+from hypothesis import Phase, given, settings
+from hypothesis.errors import HypothesisWarning
+from hypothesis.strategies import fixed_dictionaries, integers
 
-from ..kast.inner import KSort
-from ..konvert import _kast_to_kore
 from ..kore.parser import KoreParser
-from ..kore.syntax import EVar
-from ..prelude.k import inj
-from ..prelude.kint import intToken
+from ..kore.prelude import inj
+from ..kore.syntax import DV, EVar, SortApp, String
 from .krun import llvm_interpret_raw
 
 if TYPE_CHECKING:
@@ -20,15 +20,41 @@
 
     from hypothesis.strategies import SearchStrategy
 
-    from ..kast.inner import KInner
     from ..kore.syntax import Pattern
 
 
+REC_LIMIT = 10**7
+
+
+class KFuzz:
+    """Interface for fuzzing over property tests in K."""
+
+    definition_dir: Path
+
+    def __init__(self, definition_dir: Path) -> None:
+        self.definition_dir = definition_dir
+
+    def fuzz_with_check(
+        self,
+        template: Pattern,
+        subst_strategy: dict[EVar, SearchStrategy[Pattern]],
+        check_func: Callable[[Pattern], Any],
+    ) -> None:
+        _fuzz(self.definition_dir, template, subst_strategy, check_func=check_func)
+
+    def fuzz_with_exit_code(
+        self,
+        template: Pattern,
+        subst_strategy: dict[EVar, SearchStrategy[Pattern]],
+    ) -> None:
+        _fuzz(self.definition_dir, template, subst_strategy, check_exit_code=True)
+
+
 def kintegers(
     *,
     min_value: int | None = None,
     max_value: int | None = None,
-    with_inj: KSort | None = None,
+    with_inj: str | None = None,
 ) -> SearchStrategy[Pattern]:
     """Return a search strategy for K integers.
 
@@ -42,21 +68,21 @@ def kintegers(
     """
 
     def int_dv(value: int) -> Pattern:
-        res: KInner = intToken(value)
+        res: Pattern = DV(SortApp('SortInt'), value=String(str(value)))
         if with_inj is not None:
-            res = inj(KSort('Int'), with_inj, res)
-        return _kast_to_kore(res)
+            res = inj(SortApp('SortInt'), SortApp(f'Sort{with_inj}'), res)
+        return res
 
-    return builds(int_dv, integers(min_value=min_value, max_value=max_value))
+    return integers(min_value=min_value, max_value=max_value).map(int_dv)
 
 
-def fuzz(
+def _fuzz(
     definition_dir: str | Path,
     template: Pattern,
     subst_strategy: dict[EVar, SearchStrategy[Pattern]],
     check_func: Callable[[Pattern], Any] | None = None,
     check_exit_code: bool = False,
-    max_examples: int = 50,
+    **hypothesis_args: Any,
 ) -> None:
     """Fuzz a property test with concrete execution over a K term.
 
@@ -70,7 +96,10 @@ def fuzz(
         check_exit_code: Check the exit code of the interpreter for a test failure instead of using check_func.
           An exit code of 0 indicates a passing test.
           A RuntimeError will be thrown if this is True and check_func is also passed as an argument.
-        max_examples: The number of test cases to run.
+        hypothesis_args: Keyword arguments that will be passed as settings for the hypothesis test. Defaults:
+          deadline: 5000
+          phases: (Phase.explicit, Phase.reuse, Phase.generate)
+
 
     Raises:
         RuntimeError: If check_func exists and check_exit_code is set, or check_func doesn't exist and check_exit_code is cleared.
@@ -79,11 +108,15 @@ 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 p in subst_case:
-                assert isinstance(p, EVar)
+            if isinstance(p, EVar) and p in subst_case:
                 return subst_case[p]
-            return p
+            else:
+                return p
 
         test_pattern = template.top_down(sub)
         res = llvm_interpret_raw(definition_dir, test_pattern.text)
@@ -97,11 +130,11 @@ def sub(p: Pattern) -> Pattern:
 
     strat: SearchStrategy = fixed_dictionaries(subst_strategy)
 
-    given(strat)(
-        settings(
-            deadline=50000,
-            max_examples=max_examples,
-            verbosity=Verbosity.verbose,
-            phases=(Phase.generate, Phase.target, Phase.shrink),
-        )(test)
-    )()
+    # 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))
+
+    given(strat)(settings(**hypothesis_args)(test))()

pyk/src/tests/integration/ktool/test_fuzz.py

@@ -5,11 +5,10 @@
 
 import pytest
 
-from pyk.kast.inner import KSort
 from pyk.kore.parser import KoreParser
 from pyk.kore.prelude import inj, top_cell_initializer
 from pyk.kore.syntax import DV, App, EVar, SortApp, String
-from pyk.ktool.kfuzz import fuzz, kintegers
+from pyk.ktool.kfuzz import KFuzz, kintegers
 from pyk.ktool.kprint import _kast
 from pyk.testing import KompiledTest
 
@@ -32,7 +31,11 @@
 class TestImpFuzz(KompiledTest):
     KOMPILE_MAIN_FILE = K_FILES / 'imp.k'
     KOMPILE_BACKEND = 'llvm'
-    SUBSTS = {VAR_X: kintegers(with_inj=KSort('AExp')), VAR_Y: kintegers(with_inj=KSort('AExp'))}
+    SUBSTS = {VAR_X: kintegers(with_inj='AExp'), VAR_Y: kintegers(with_inj='AExp')}
+
+    @pytest.fixture
+    def kfuzz(self, definition_dir: Path) -> KFuzz:
+        return KFuzz(definition_dir)
 
     @staticmethod
     def check(p: Pattern) -> None:
@@ -76,6 +79,7 @@ def replace_var_ids(p: Pattern) -> Pattern:
     def test_fuzz(
         self,
         definition_dir: Path,
+        kfuzz: KFuzz,
     ) -> None:
         # Given
         program_text = """
@@ -95,11 +99,12 @@ def test_fuzz(
         init_pattern = self.setup_program(definition_dir, program_text)
 
         # Then
-        fuzz(definition_dir, init_pattern, self.SUBSTS, self.check)
+        kfuzz.fuzz_with_check(init_pattern, self.SUBSTS, self.check)
 
     def test_fuzz_fail(
         self,
         definition_dir: Path,
+        kfuzz: KFuzz,
     ) -> None:
         # Given
         program_text = """
@@ -118,4 +123,4 @@ def test_fuzz_fail(
 
         # Then
         with pytest.raises(AssertionError):
-            fuzz(definition_dir, init_pattern, self.SUBSTS, self.check)
+            kfuzz.fuzz_with_check(init_pattern, self.SUBSTS, self.check)