Begin implementing fuzzing

pyk/pyproject.toml

@@ -27,6 +27,7 @@ pytest = "*"
 textual = "^0.27.0"
 tomli = "^2.0.1"
 xdg-base-dirs = "^6.0.1"
+hypothesis = "^6.103.1"
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"

pyk/src/pyk/ktool/kfuzz.py

@@ -0,0 +1,104 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+from hypothesis import Phase, Verbosity, given, settings
+from hypothesis.strategies import builds, fixed_dictionaries, integers
+
+from ..kast.inner import KSort
+from ..konvert import _kast_to_kore
+from ..kore.parser import KoreParser
+from ..kore.syntax import Assoc, EVar
+from ..prelude.k import inj
+from ..prelude.kint import intToken
+from .krun import llvm_interpret_raw
+
+if TYPE_CHECKING:
+    from collections.abc import Callable, Mapping
+    from pathlib import Path
+
+    from hypothesis.strategies import SearchStrategy
+
+    from ..kast.inner import KInner
+    from ..kore.syntax import Pattern
+
+
+def kintegers(
+    *,
+    min_value: int | None = None,
+    max_value: int | None = None,
+    with_inj: KSort | None = None,
+) -> SearchStrategy[Pattern]:
+    """
+    Args:
+        min_value: Minimum value for the generated integers
+        max_value: Maximum value for the generated integers
+        with_inj: Return the integer as an injection into this sort
+
+    Returns:
+        A strategy which generates integer domain values.
+    """
+
+    def int_dv(value: int) -> Pattern:
+        res: KInner = intToken(value)
+        if with_inj is not None:
+            res = inj(KSort('Int'), with_inj, res)
+        return _kast_to_kore(res)
+
+    return builds(int_dv, integers(min_value=min_value, max_value=max_value))
+
+
+def fuzz(
+    definition_dir: str | Path,
+    template: Pattern,
+    subst_strategy: dict[EVar, SearchStrategy[Pattern]],
+    check_func: Callable[[Pattern], None] | None = None,
+    check_exit_code: bool = False,
+    max_examples: int = 50,
+) -> None:
+    """Use this to fuzz a property test with concrete execution over a K term.
+    Args:
+        definition_dir: The location of the K definition to run the interpreter for
+        template: The term which will be sent to the interpreter after randomizing inputs. It should contain at least one variable which will be substituted for a value.
+        subst_strategy: Should have each variable in the template term mapped to a strategy for generating values for it.
+        check_func: Will be called on the kore output from the interpreter. Should throw an AssertionError if it determines that the output indicates a test failure. A RuntimeError will be thrown if check_exit_code is True.
+        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 supplied.
+        max_examples: The number of test cases to run.
+
+    Raises:
+        RuntimeError: If check_func exists and check_exit_code is set, or check_func doesn't exist and check_exit_code is cleared
+    """
+    if bool(check_func) == check_exit_code:
+        raise RuntimeError('Must pass one of check_func or check_exit_code, and not both!')
+
+    def test(subst_case: Mapping[EVar, Pattern]) -> None:
+        def sub(p: Pattern) -> Pattern:
+            if isinstance(p, Assoc):
+                symbol = p.symbol()
+                args = (arg.top_down(sub) for arg in p.app.args)
+                return p.of(symbol, patterns=(p.app.let(args=args),))
+            if p in subst_case:
+                assert isinstance(p, EVar)
+                return subst_case[p]
+            return p
+
+        test_pattern = template.top_down(sub)
+        res = llvm_interpret_raw(definition_dir, test_pattern.text)
+
+        if check_exit_code:
+            assert res.returncode == 0
+        else:
+            assert check_func
+            res_pattern = KoreParser(res.stdout).pattern()
+            check_func(res_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)
+    )()

pyk/src/pyk/ktool/krun.py

@@ -311,19 +311,20 @@ def llvm_interpret(definition_dir: str | Path, pattern: Pattern, *, depth: int |
     :return: A pattern resulting from the rewrites
     :raises RuntimeError: If the interpreter fails
     """
+    try:
+        res = llvm_interpret_raw(definition_dir, pattern.text, depth)
+    except CalledProcessError as err:
+        raise RuntimeError(f'Interpreter failed with status {err.returncode}: {err.stderr}') from err
+
+    return KoreParser(res.stdout).pattern()
 
-    definition_dir = Path(definition_dir)
-    check_dir_path(definition_dir)
 
+def llvm_interpret_raw(definition_dir: str | Path, kore: str, depth: int | None = None) -> CompletedProcess:
+    definition_dir = Path(definition_dir)
     interpreter_file = definition_dir / 'interpreter'
     check_file_path(interpreter_file)
 
     depth = depth if depth is not None else -1
     args = [str(interpreter_file), '/dev/stdin', str(depth), '/dev/stdout']
 
-    try:
-        res = run_process(args, input=pattern.text, pipe_stderr=True)
-    except CalledProcessError as err:
-        raise RuntimeError(f'Interpreter failed with status {err.returncode}: {err.stderr}') from err
-
-    return KoreParser(res.stdout).pattern()
+    return run_process(args, input=kore, pipe_stderr=True)

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

@@ -0,0 +1,129 @@
+from __future__ import annotations
+
+import logging
+from typing import TYPE_CHECKING
+
+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, Assoc, EVar, SortApp, String
+from pyk.ktool.kfuzz import fuzz, kintegers
+from pyk.ktool.kprint import _kast
+from pyk.testing import KompiledTest
+
+from ..utils import K_FILES, TEST_DATA_DIR
+
+if TYPE_CHECKING:
+    from collections.abc import Callable
+    from pathlib import Path
+    from typing import Final
+
+    from hypothesis.strategies import SearchStrategy
+
+    from pyk.kore.syntax import Pattern
+
+_LOGGER: Final = logging.getLogger(__name__)
+
+FUZZ_FILES: Path = TEST_DATA_DIR / 'fuzzing'
+
+VAR_X = EVar(name='VarX', sort=SortApp('SortInt'))
+VAR_Y = EVar(name='VarY', sort=SortApp('SortInt'))
+
+
+class TestImpFuzz(KompiledTest):
+    KOMPILE_MAIN_FILE = K_FILES / 'imp.k'
+    KOMPILE_BACKEND = 'llvm'
+
+    @staticmethod
+    def substs() -> dict[EVar, SearchStrategy[Pattern]]:
+        return {VAR_X: kintegers(with_inj=KSort('AExp')), VAR_Y: kintegers(with_inj=KSort('AExp'))}
+
+    @staticmethod
+    def check() -> Callable[[Pattern], None]:
+        def checkres(p: Pattern) -> Pattern:
+            match p:
+                case Assoc():
+                    symbol = p.symbol()
+                    args = (arg.top_down(checkres) for arg in p.app.args)
+                    return p.of(symbol, patterns=(p.app.let(args=args),))
+                case App("Lbl'UndsPipe'-'-GT-Unds'", args=(key, val)):
+                    match key, val:
+                        case (
+                            App('inj', args=(DV(value=String('res')),)),
+                            App('inj', args=(DV(value=String(resval)),)),
+                        ):
+                            assert resval == '0'
+
+            return p
+
+        return lambda pattern: (None, pattern.top_down(checkres))[0]
+
+    @staticmethod
+    def setup_program(definition_dir: Path, text: str) -> Pattern:
+        kore_text = _kast(definition_dir=definition_dir, input='program', output='kore', expression=text).stdout
+
+        program_pattern = KoreParser(kore_text).pattern()
+
+        def replace_var_ids(p: Pattern) -> Pattern:
+            match p:
+                case App('inj', _, (DV(_, String('varx')),)):
+                    return VAR_X
+                case App('inj', _, (DV(_, String('vary')),)):
+                    return VAR_Y
+            return p
+
+        program_pattern = program_pattern.top_down(replace_var_ids)
+        init_pattern = top_cell_initializer(
+            {
+                '$PGM': inj(SortApp('SortPgm'), SortApp('SortKItem'), program_pattern),
+            }
+        )
+
+        return init_pattern
+
+    def test_fuzz(
+        self,
+        definition_dir: Path,
+    ) -> None:
+        # Given
+        program_text = """
+            // Checks the commutativity of addition
+            int x, y, a, b, res;
+            x = varx;
+            y = vary;
+            a = x + y;
+            b = y + x;
+            if ((a <= b) && (b <= a)) { // a == b
+                res = 0;
+            } else {
+                res = 1;
+            }
+            """
+
+        init_pattern = self.setup_program(definition_dir, program_text)
+
+        fuzz(definition_dir, init_pattern, self.substs(), self.check())
+
+    def test_fuzz_fail(
+        self,
+        definition_dir: Path,
+    ) -> None:
+        # Given
+        program_text = """
+            // Checks that x <= y
+            int x, y, res;
+            x = varx;
+            y = vary;
+            if (x <= y) {
+                res = 0;
+            } else {
+                res = 1;
+            }
+            """
+
+        init_pattern = self.setup_program(definition_dir, program_text)
+
+        with pytest.raises(AssertionError):
+            fuzz(definition_dir, init_pattern, self.substs(), self.check())