Begin implementing fuzzing (#4454)

This introduces the most basic functionality for doing fuzz testing of a
property in K.

It adds a function `fuzz` to the `ktool.kfuzz` pyk module which takes
the location of an llvm-kompiled definition, a template configuration in
kore containing input variables to be randomized, a strategy for
substituting those variables (so far, only with integers using
`kintegers`), and either a function to check the resulting kore or a
flag to check the exit code of the interpreter. It will invoke
hypothesis to randomize the inputs and run the interpreter.

pyk/pyproject.toml

@@ -21,6 +21,7 @@ cmd2 = "^2.4.2"
 coloredlogs = "^15.0.1"
 filelock = "^3.9.0"
 graphviz = "^0.20.1"
+hypothesis = "^6.103.1"
 psutil = "5.9.5"
 pybind11 = "^2.10.3"
 pytest = "*"

pyk/src/pyk/ktool/kfuzz.py

@@ -0,0 +1,111 @@
+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 typing import Any
+
+    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]:
+    """Return a search strategy for K integers.
+
+    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], Any] | None = None,
+    check_exit_code: bool = False,
+    max_examples: int = 50,
+) -> None:
+    """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 this is passed as an argument and 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 passed as an argument.
+        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

@@ -315,18 +315,33 @@ def llvm_interpret(definition_dir: str | Path, pattern: Pattern, *, depth: int |
     Raises:
         RuntimeError: If the interpreter fails.
     """
-    definition_dir = Path(definition_dir)
-    check_dir_path(definition_dir)
+    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()
+
+
+def llvm_interpret_raw(definition_dir: str | Path, kore: str, depth: int | None = None) -> CompletedProcess:
+    """Execute the `interpreter` binary generated by the LLVM Backend, with no processing of input/output.
+
+    Args:
+        definition_dir: Path to the kompiled definition directory.
+        pattern: KORE string to start rewriting from.
+        depth: Maximal number of rewrite steps to take.
+
+    Returns:
+        The CompletedProcess of the interpreter.
 
+    Raises:
+        CalledProcessError: If the interpreter fails.
+    """
+    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,125 @@
+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 pathlib import Path
+    from typing import Final
+
+    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'
+    SUBSTS = {VAR_X: kintegers(with_inj=KSort('AExp')), VAR_Y: kintegers(with_inj=KSort('AExp'))}
+
+    @staticmethod
+    def check(p: Pattern) -> None:
+        def check_inner(p: Pattern) -> Pattern:
+            match p:
+                case Assoc():
+                    symbol = p.symbol()
+                    args = (arg.top_down(check_inner) 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
+
+        p.top_down(check_inner)
+
+    @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)
+
+        # Then
+        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)
+
+        # Then
+        with pytest.raises(AssertionError):
+            fuzz(definition_dir, init_pattern, self.SUBSTS, self.check)