Merge remote-tracking branch 'origin/develop'

pyk/src/pyk/ktool/kfuzz.py

@@ -2,15 +2,12 @@
 
 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.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 +17,48 @@
 
     from hypothesis.strategies import SearchStrategy
 
-    from ..kast.inner import KInner
     from ..kore.syntax import Pattern
 
 
+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],
+        **hypothesis_args: Any,
+    ) -> None:
+        """Fuzz over a property test using check_func to check for a passing test.
+
+        See :any:`fuzz` for info on the parameters.
+        """
+        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]],
+        **hypothesis_args: Any,
+    ) -> None:
+        """Fuzz over a property test using the exit code from the interpreter to check for a passing test.
+
+        See :any:`fuzz` for info on the parameters.
+        """
+        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,12 +72,12 @@ 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(
@@ -56,7 +86,7 @@ def fuzz(
     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 +100,12 @@ 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.
@@ -80,10 +115,10 @@ def fuzz(
 
     def test(subst_case: Mapping[EVar, Pattern]) -> None:
         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 +132,8 @@ 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)
-    )()
+    # 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)