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,75 @@
+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 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]:
+    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:
+    if not ((check_func is not None) ^ 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 p in subst_case.keys():
+                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 is not None
+            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,84 @@
+from __future__ import annotations
+
+import logging
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+import pytest
+
+from pyk.kast.inner import KSort
+from pyk.kore.parser import KoreParser
+from pyk.kore.syntax import App, EVar, SortApp
+from pyk.ktool.kfuzz import fuzz, kintegers
+from pyk.testing import KompiledTest
+
+from ..utils import K_FILES, TEST_DATA_DIR
+
+if TYPE_CHECKING:
+    from collections.abc import Callable
+    from typing import Final
+
+    from hypothesis.strategies import SearchStrategy
+    from pytest import FixtureRequest
+
+    from pyk.kore.syntax import Pattern
+
+_LOGGER: Final = logging.getLogger(__name__)
+
+FUZZ_FILES: Path = TEST_DATA_DIR / 'fuzzing'
+
+
+class TestImpFuzz(KompiledTest):
+    KOMPILE_MAIN_FILE = K_FILES / 'imp.k'
+    KOMPILE_BACKEND = 'llvm'
+
+    @pytest.fixture
+    def template_config(self, request: FixtureRequest) -> Pattern:
+        if request.function.__name__ == 'test_fuzz':
+            return KoreParser(Path(FUZZ_FILES / 'imp_comm_config.kore').read_text()).pattern()
+        elif request.function.__name__ == 'test_fuzz_fail':
+            return KoreParser(Path(FUZZ_FILES / 'imp_lte_config.kore').read_text()).pattern()
+        else:
+            raise RuntimeError('Unexpected use of fixture template_config')
+
+    @pytest.fixture
+    def substs(self) -> dict[EVar, SearchStrategy[Pattern]]:
+        var_x = EVar(name='VarX', sort=SortApp('SortInt'))
+        var_y = EVar(name='VarY', sort=SortApp('SortInt'))
+        return {var_x: kintegers(with_inj=KSort('AExp')), var_y: kintegers(with_inj=KSort('AExp'))}
+
+    @pytest.fixture
+    def check_func(self) -> Callable[[Pattern], None]:
+
+        lbl = "Lbl'UndsPipe'-'-GT-Unds'"
+
+        def checkres(p: Pattern) -> Pattern:
+            if isinstance(p, App):
+                if p.symbol == lbl:
+                    left = p.args[0]
+                    right = p.args[1]
+                    if left.args[0].value.value == 'res':  # type: ignore[attr-defined]
+                        val = int(right.args[0].value.value)  # type: ignore[attr-defined]
+                        assert val == 0
+            return p
+
+        return lambda pattern: pattern.args[0].args[1].args[0].pattern.top_down(checkres)  # type: ignore[attr-defined]
+
+    def test_fuzz(
+        self,
+        definition_dir: Path,
+        template_config: Pattern,
+        substs: dict[EVar, SearchStrategy[Pattern]],
+        check_func: Callable[[Pattern], None],
+    ) -> None:
+        fuzz(definition_dir, template_config, substs, check_func)
+
+    def test_fuzz_fail(
+        self,
+        definition_dir: Path,
+        template_config: Pattern,
+        substs: dict[EVar, SearchStrategy[Pattern]],
+        check_func: Callable[[Pattern], None],
+    ) -> None:
+        with pytest.raises(AssertionError):
+            fuzz(definition_dir, template_config, substs, check_func)

pyk/src/tests/integration/test-data/fuzzing/imp_comm_config.kore

@@ -0,0 +1,16 @@
+// Tests for commutativity of the addition operation
+//
+// Source:
+//
+// int x, y, a, b, res;
+// x = X:Int;
+// y = Y:Int;
+// a = x + y;
+// b = y + x;
+// if ((a <= b) && (b <= a)) { // a == b
+//     res = 0;
+// } else {
+//     res = 1;
+// }
+
+Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortPgm{}, SortKItem{}}(Lblint'UndsSClnUnds'{}(Lbl'UndsCommUnds'{}(\dv{SortId{}}("x"),Lbl'UndsCommUnds'{}(\dv{SortId{}}("y"),Lbl'UndsCommUnds'{}(\dv{SortId{}}("a"),Lbl'UndsCommUnds'{}(\dv{SortId{}}("b"),Lbl'UndsCommUnds'{}(\dv{SortId{}}("res"),Lbl'Stop'List'LBraQuotUndsCommUndsQuotRBra'{}()))))),Lbl'UndsUnds'{}(Lbl'UndsUnds'{}(Lbl'UndsUnds'{}(Lbl'UndsUnds'{}(Lbl'UndsEqlsUndsSCln'{}(\dv{SortId{}}("x"),VarX : SortInt{}),Lbl'UndsEqlsUndsSCln'{}(\dv{SortId{}}("y"),VarY : SortInt{})),Lbl'UndsEqlsUndsSCln'{}(\dv{SortId{}}("a"),Lbl'UndsPlusUnds'{}(inj{SortId{}, SortAExp{}}(\dv{SortId{}}("x")),inj{SortId{}, SortAExp{}}(\dv{SortId{}}("y"))))),Lbl'UndsEqlsUndsSCln'{}(\dv{SortId{}}("b"),Lbl'UndsPlusUnds'{}(inj{SortId{}, SortAExp{}}(\dv{SortId{}}("y")),inj{SortId{}, SortAExp{}}(\dv{SortId{}}("x"))))),Lblif'LParUndsRParUnds'else'Unds'{}(Lbl'UndsAnd-And-Unds'{}(Lbl'Unds-LT-EqlsUnds'{}(inj{SortId{}, SortAExp{}}(\dv{SortId{}}("a")),inj{SortId{}, SortAExp{}}(\dv{SortId{}}("b"))),Lbl'Unds-LT-EqlsUnds'{}(inj{SortId{}, SortAExp{}}(\dv{SortId{}}("b")),inj{SortId{}, SortAExp{}}(\dv{SortId{}}("a")))),Lbl'LBraUndsRBra'{}(Lbl'UndsEqlsUndsSCln'{}(\dv{SortId{}}("res"),inj{SortInt{}, SortAExp{}}(\dv{SortInt{}}("0")))),Lbl'LBraUndsRBra'{}(Lbl'UndsEqlsUndsSCln'{}(\dv{SortId{}}("res"),inj{SortInt{}, SortAExp{}}(\dv{SortInt{}}("1")))))))),dotk{}())),Lbl'-LT-'state'-GT-'{}(Lbl'Stop'Map{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))

pyk/src/tests/integration/test-data/fuzzing/imp_lte_config.kore

@@ -0,0 +1,14 @@
+// Tests for x <= y
+//
+// Source:
+//
+// int x, y, res;
+// x = X:Int;
+// y = Y:Int;
+// if (x <= y) {
+//     res = 0;
+// } else {
+//     res = 1;
+// }
+
+Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortPgm{}, SortKItem{}}(Lblint'UndsSClnUnds'{}(Lbl'UndsCommUnds'{}(\dv{SortId{}}("x"),Lbl'UndsCommUnds'{}(\dv{SortId{}}("y"),Lbl'UndsCommUnds'{}(\dv{SortId{}}("res"),Lbl'Stop'List'LBraQuotUndsCommUndsQuotRBra'{}()))),Lbl'UndsUnds'{}(Lbl'UndsUnds'{}(Lbl'UndsEqlsUndsSCln'{}(\dv{SortId{}}("x"),VarX : SortInt{}),Lbl'UndsEqlsUndsSCln'{}(\dv{SortId{}}("y"),VarY : SortInt{})),Lblif'LParUndsRParUnds'else'Unds'{}(Lbl'Unds-LT-EqlsUnds'{}(inj{SortId{}, SortAExp{}}(\dv{SortId{}}("x")),inj{SortId{}, SortAExp{}}(\dv{SortId{}}("y"))),Lbl'LBraUndsRBra'{}(Lbl'UndsEqlsUndsSCln'{}(\dv{SortId{}}("res"),inj{SortInt{}, SortAExp{}}(\dv{SortInt{}}("0")))),Lbl'LBraUndsRBra'{}(Lbl'UndsEqlsUndsSCln'{}(\dv{SortId{}}("res"),inj{SortInt{}, SortAExp{}}(\dv{SortInt{}}("1")))))))),dotk{}())),Lbl'-LT-'state'-GT-'{}(Lbl'Stop'Map{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))