From 6b055c835c22bc82a840567c21ede54d9f76ac6e Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 13 Jun 2024 09:57:02 -0500 Subject: [PATCH 01/16] Pull out llvm_interpret_raw --- pyk/src/pyk/ktool/krun.py | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/pyk/src/pyk/ktool/krun.py b/pyk/src/pyk/ktool/krun.py index f3823a33723..1e1c85363cc 100644 --- a/pyk/src/pyk/ktool/krun.py +++ b/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) From db2931a5e549ea279ed795a9df978e886be70ed9 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 14 Jun 2024 12:35:40 -0500 Subject: [PATCH 02/16] Add hypothesis to poetry project --- pyk/poetry.lock | 46 +++++++++++++++++++++++++++++++++++++++++++++- pyk/pyproject.toml | 1 + 2 files changed, 46 insertions(+), 1 deletion(-) diff --git a/pyk/poetry.lock b/pyk/poetry.lock index dd3686d98e3..bf579447ade 100644 --- a/pyk/poetry.lock +++ b/pyk/poetry.lock @@ -373,6 +373,39 @@ files = [ [package.dependencies] pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_version >= \"3.8\""} +[[package]] +name = "hypothesis" +version = "6.103.1" +description = "A library for property-based testing" +optional = false +python-versions = ">=3.8" +files = [ + {file = "hypothesis-6.103.1-py3-none-any.whl", hash = "sha256:d3c959fab6233e78867499e2117ae9db8dc40eeed936d71a2cfc7b6094972e74"}, + {file = "hypothesis-6.103.1.tar.gz", hash = "sha256:d299d5c21d6408eab3be670c94c974f3acf0b511c61fe81804b09091e393ee1f"}, +] + +[package.dependencies] +attrs = ">=22.2.0" +exceptiongroup = {version = ">=1.0.0", markers = "python_version < \"3.11\""} +sortedcontainers = ">=2.1.0,<3.0.0" + +[package.extras] +all = ["backports.zoneinfo (>=0.2.1)", "black (>=19.10b0)", "click (>=7.0)", "crosshair-tool (>=0.0.54)", "django (>=3.2)", "dpcontracts (>=0.4)", "hypothesis-crosshair (>=0.0.4)", "lark (>=0.10.1)", "libcst (>=0.3.16)", "numpy (>=1.17.3)", "pandas (>=1.1)", "pytest (>=4.6)", "python-dateutil (>=1.4)", "pytz (>=2014.1)", "redis (>=3.0.0)", "rich (>=9.0.0)", "tzdata (>=2024.1)"] +cli = ["black (>=19.10b0)", "click (>=7.0)", "rich (>=9.0.0)"] +codemods = ["libcst (>=0.3.16)"] +crosshair = ["crosshair-tool (>=0.0.54)", "hypothesis-crosshair (>=0.0.4)"] +dateutil = ["python-dateutil (>=1.4)"] +django = ["django (>=3.2)"] +dpcontracts = ["dpcontracts (>=0.4)"] +ghostwriter = ["black (>=19.10b0)"] +lark = ["lark (>=0.10.1)"] +numpy = ["numpy (>=1.17.3)"] +pandas = ["pandas (>=1.1)"] +pytest = ["pytest (>=4.6)"] +pytz = ["pytz (>=2014.1)"] +redis = ["redis (>=3.0.0)"] +zoneinfo = ["backports.zoneinfo (>=0.2.1)", "tzdata (>=2024.1)"] + [[package]] name = "importlib-metadata" version = "7.1.0" @@ -866,6 +899,17 @@ docs = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "pygments testing = ["build[virtualenv]", "filelock (>=3.4.0)", "importlib-metadata", "ini2toml[lite] (>=0.9)", "jaraco.develop (>=7.21)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "mypy (==1.9)", "packaging (>=23.2)", "pip (>=19.1)", "pytest (>=6,!=8.1.1)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-home (>=0.5)", "pytest-mypy", "pytest-perf", "pytest-ruff (>=0.2.1)", "pytest-timeout", "pytest-xdist (>=3)", "tomli", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel"] testing-integration = ["build[virtualenv] (>=1.0.3)", "filelock (>=3.4.0)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "packaging (>=23.2)", "pytest", "pytest-enabler", "pytest-xdist", "tomli", "virtualenv (>=13.0.0)", "wheel"] +[[package]] +name = "sortedcontainers" +version = "2.4.0" +description = "Sorted Containers -- Sorted List, Sorted Dict, Sorted Set" +optional = false +python-versions = "*" +files = [ + {file = "sortedcontainers-2.4.0-py2.py3-none-any.whl", hash = "sha256:a163dcaede0f1c021485e957a39245190e74249897e2ae4b2aa38595db237ee0"}, + {file = "sortedcontainers-2.4.0.tar.gz", hash = "sha256:25caa5a06cc30b6b83d11423433f65d1f9d76c4c6a0c90e3379eaa43b9bfdb88"}, +] + [[package]] name = "textual" version = "0.27.0" @@ -984,4 +1028,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "887f594c54788d5dc671ec50bf1bbd5430d8d126e270ef6dc373f93a96bc8a5e" +content-hash = "f3d66605bb742dce60ff2f3df9a904dc7732201d27888470bb8a3decd04e59ef" diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml index 400e0e2e674..3e671aa9d80 100644 --- a/pyk/pyproject.toml +++ b/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 = "*" From d16088be8d074257d3877a7e21f92dd2e0cc4efb Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 14 Jun 2024 13:51:38 -0500 Subject: [PATCH 03/16] First pass of fuzzing function, with kintegers --- pyk/src/pyk/ktool/krun.py | 62 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) diff --git a/pyk/src/pyk/ktool/krun.py b/pyk/src/pyk/ktool/krun.py index 1e1c85363cc..f9b08536bb5 100644 --- a/pyk/src/pyk/ktool/krun.py +++ b/pyk/src/pyk/ktool/krun.py @@ -6,9 +6,17 @@ from subprocess import CalledProcessError from typing import TYPE_CHECKING +from hypothesis import Phase, Verbosity, given, settings +from hypothesis.strategies import builds, fixed_dictionaries, integers + from ..cli.utils import check_dir_path, check_file_path +from ..kast.inner import KSort +from ..konvert import _kast_to_kore from ..kore.parser import KoreParser +from ..kore.syntax import EVar from ..kore.tools import PrintOutput, kore_print +from ..prelude.k import inj +from ..prelude.kint import intToken from ..utils import run_process from .kprint import KPrint @@ -18,6 +26,8 @@ from subprocess import CompletedProcess from typing import Final + from hypothesis.strategies import SearchStrategy + from ..kast.inner import KInner from ..kast.outer import KFlatModule from ..kast.pretty import SymbolTable @@ -187,6 +197,58 @@ def krun(self, input_file: Path) -> tuple[int, KInner]: return (result.returncode, kast) +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) + )() + + def _krun( command: str = 'krun', *, From b011d55ac5aebb14a212f25617182bcafff6523c Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 18 Jun 2024 19:00:51 -0500 Subject: [PATCH 04/16] Test fuzzing --- pyk/src/tests/integration/ktool/test_fuzz.py | 84 +++++++++++++++++++ .../test-data/fuzzing/imp_comm_config.kore | 16 ++++ .../test-data/fuzzing/imp_lte_config.kore | 14 ++++ 3 files changed, 114 insertions(+) create mode 100644 pyk/src/tests/integration/ktool/test_fuzz.py create mode 100644 pyk/src/tests/integration/test-data/fuzzing/imp_comm_config.kore create mode 100644 pyk/src/tests/integration/test-data/fuzzing/imp_lte_config.kore diff --git a/pyk/src/tests/integration/ktool/test_fuzz.py b/pyk/src/tests/integration/ktool/test_fuzz.py new file mode 100644 index 00000000000..51c8d7f658e --- /dev/null +++ b/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.krun 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) diff --git a/pyk/src/tests/integration/test-data/fuzzing/imp_comm_config.kore b/pyk/src/tests/integration/test-data/fuzzing/imp_comm_config.kore new file mode 100644 index 00000000000..ef3ef14afc7 --- /dev/null +++ b/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"))) diff --git a/pyk/src/tests/integration/test-data/fuzzing/imp_lte_config.kore b/pyk/src/tests/integration/test-data/fuzzing/imp_lte_config.kore new file mode 100644 index 00000000000..10ae09ea128 --- /dev/null +++ b/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"))) From 4fdabcecf8ee634f747189619f9cd46d8c0f1ba5 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 18 Jun 2024 19:10:27 -0500 Subject: [PATCH 05/16] Move fuzzing into ktool.kfuzz --- pyk/src/pyk/ktool/kfuzz.py | 75 ++++++++++++++++++++ pyk/src/pyk/ktool/krun.py | 62 ---------------- pyk/src/tests/integration/ktool/test_fuzz.py | 2 +- 3 files changed, 76 insertions(+), 63 deletions(-) create mode 100644 pyk/src/pyk/ktool/kfuzz.py diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py new file mode 100644 index 00000000000..566467ceea3 --- /dev/null +++ b/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) + )() diff --git a/pyk/src/pyk/ktool/krun.py b/pyk/src/pyk/ktool/krun.py index f9b08536bb5..1e1c85363cc 100644 --- a/pyk/src/pyk/ktool/krun.py +++ b/pyk/src/pyk/ktool/krun.py @@ -6,17 +6,9 @@ from subprocess import CalledProcessError from typing import TYPE_CHECKING -from hypothesis import Phase, Verbosity, given, settings -from hypothesis.strategies import builds, fixed_dictionaries, integers - from ..cli.utils import check_dir_path, check_file_path -from ..kast.inner import KSort -from ..konvert import _kast_to_kore from ..kore.parser import KoreParser -from ..kore.syntax import EVar from ..kore.tools import PrintOutput, kore_print -from ..prelude.k import inj -from ..prelude.kint import intToken from ..utils import run_process from .kprint import KPrint @@ -26,8 +18,6 @@ from subprocess import CompletedProcess from typing import Final - from hypothesis.strategies import SearchStrategy - from ..kast.inner import KInner from ..kast.outer import KFlatModule from ..kast.pretty import SymbolTable @@ -197,58 +187,6 @@ def krun(self, input_file: Path) -> tuple[int, KInner]: return (result.returncode, kast) -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) - )() - - def _krun( command: str = 'krun', *, diff --git a/pyk/src/tests/integration/ktool/test_fuzz.py b/pyk/src/tests/integration/ktool/test_fuzz.py index 51c8d7f658e..2bfb4b0fce7 100644 --- a/pyk/src/tests/integration/ktool/test_fuzz.py +++ b/pyk/src/tests/integration/ktool/test_fuzz.py @@ -9,7 +9,7 @@ from pyk.kast.inner import KSort from pyk.kore.parser import KoreParser from pyk.kore.syntax import App, EVar, SortApp -from pyk.ktool.krun import fuzz, kintegers +from pyk.ktool.kfuzz import fuzz, kintegers from pyk.testing import KompiledTest from ..utils import K_FILES, TEST_DATA_DIR From af0a798b2d549925c6167ffab090965dc889f269 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 20 Jun 2024 13:47:48 -0500 Subject: [PATCH 06/16] Turn fixtures into static methods --- pyk/src/tests/integration/ktool/test_fuzz.py | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/pyk/src/tests/integration/ktool/test_fuzz.py b/pyk/src/tests/integration/ktool/test_fuzz.py index 2bfb4b0fce7..bb9e5f2633d 100644 --- a/pyk/src/tests/integration/ktool/test_fuzz.py +++ b/pyk/src/tests/integration/ktool/test_fuzz.py @@ -41,14 +41,14 @@ def template_config(self, request: FixtureRequest) -> Pattern: else: raise RuntimeError('Unexpected use of fixture template_config') - @pytest.fixture - def substs(self) -> dict[EVar, SearchStrategy[Pattern]]: + @staticmethod + def substs() -> 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]: + @staticmethod + def check() -> Callable[[Pattern], None]: lbl = "Lbl'UndsPipe'-'-GT-Unds'" @@ -68,17 +68,13 @@ 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) + fuzz(definition_dir, template_config, self.substs(), self.check()) 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) + fuzz(definition_dir, template_config, self.substs(), self.check()) From 0cafd57f22d4d7459ee25af57e13f0bc1c659027 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 20 Jun 2024 16:25:27 -0500 Subject: [PATCH 07/16] Generate input kore for the tests --- pyk/src/pyk/ktool/kfuzz.py | 6 +- pyk/src/tests/integration/ktool/test_fuzz.py | 84 ++++++++++++++----- .../test-data/fuzzing/imp_comm_config.kore | 16 ---- .../test-data/fuzzing/imp_lte_config.kore | 14 ---- 4 files changed, 70 insertions(+), 50 deletions(-) delete mode 100644 pyk/src/tests/integration/test-data/fuzzing/imp_comm_config.kore delete mode 100644 pyk/src/tests/integration/test-data/fuzzing/imp_lte_config.kore diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index 566467ceea3..92855098347 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -8,7 +8,7 @@ from ..kast.inner import KSort from ..konvert import _kast_to_kore from ..kore.parser import KoreParser -from ..kore.syntax import EVar +from ..kore.syntax import Assoc, EVar from ..prelude.k import inj from ..prelude.kint import intToken from .krun import llvm_interpret_raw @@ -48,6 +48,10 @@ def fuzz( 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.keys(): assert isinstance(p, EVar) return subst_case[p] diff --git a/pyk/src/tests/integration/ktool/test_fuzz.py b/pyk/src/tests/integration/ktool/test_fuzz.py index bb9e5f2633d..6e288e6d3d3 100644 --- a/pyk/src/tests/integration/ktool/test_fuzz.py +++ b/pyk/src/tests/integration/ktool/test_fuzz.py @@ -1,25 +1,26 @@ 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.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.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 pytest import FixtureRequest from pyk.kore.syntax import Pattern @@ -27,25 +28,17 @@ 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' - @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') - @staticmethod def substs() -> 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'))} + return {VAR_X: kintegers(with_inj=KSort('AExp')), VAR_Y: kintegers(with_inj=KSort('AExp'))} @staticmethod def check() -> Callable[[Pattern], None]: @@ -64,17 +57,70 @@ def checkres(p: Pattern) -> Pattern: return lambda pattern: pattern.args[0].args[1].args[0].pattern.top_down(checkres) # type: ignore[attr-defined] + @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, - template_config: Pattern, ) -> None: - fuzz(definition_dir, template_config, self.substs(), self.check()) + # 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, - template_config: Pattern, ) -> 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, template_config, self.substs(), self.check()) + fuzz(definition_dir, init_pattern, self.substs(), self.check()) diff --git a/pyk/src/tests/integration/test-data/fuzzing/imp_comm_config.kore b/pyk/src/tests/integration/test-data/fuzzing/imp_comm_config.kore deleted file mode 100644 index ef3ef14afc7..00000000000 --- a/pyk/src/tests/integration/test-data/fuzzing/imp_comm_config.kore +++ /dev/null @@ -1,16 +0,0 @@ -// 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"))) diff --git a/pyk/src/tests/integration/test-data/fuzzing/imp_lte_config.kore b/pyk/src/tests/integration/test-data/fuzzing/imp_lte_config.kore deleted file mode 100644 index 10ae09ea128..00000000000 --- a/pyk/src/tests/integration/test-data/fuzzing/imp_lte_config.kore +++ /dev/null @@ -1,14 +0,0 @@ -// 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"))) From 70ba7ee9b09eefa14e4dadf8e412528165cc17fa Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 21 Jun 2024 12:19:43 -0500 Subject: [PATCH 08/16] Use matching on output imp configuration --- pyk/src/tests/integration/ktool/test_fuzz.py | 27 +++++++++++--------- 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/pyk/src/tests/integration/ktool/test_fuzz.py b/pyk/src/tests/integration/ktool/test_fuzz.py index 6e288e6d3d3..1c4a02e38e6 100644 --- a/pyk/src/tests/integration/ktool/test_fuzz.py +++ b/pyk/src/tests/integration/ktool/test_fuzz.py @@ -8,7 +8,7 @@ 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.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 @@ -42,20 +42,23 @@ def substs() -> dict[EVar, SearchStrategy[Pattern]]: @staticmethod def check() -> 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 + 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: pattern.args[0].args[1].args[0].pattern.top_down(checkres) # type: ignore[attr-defined] + return lambda pattern: (None, pattern.top_down(checkres))[0] @staticmethod def setup_program(definition_dir: Path, text: str) -> Pattern: From ba418fc1e928402088ab72440226e6fae27cf6b8 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 21 Jun 2024 12:30:39 -0500 Subject: [PATCH 09/16] Logic refactorings --- pyk/src/pyk/ktool/kfuzz.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index 92855098347..02a6d11825c 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -43,7 +43,7 @@ def fuzz( check_exit_code: bool = False, max_examples: int = 50, ) -> None: - if not ((check_func is not None) ^ check_exit_code): + 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: @@ -52,7 +52,7 @@ def sub(p: Pattern) -> Pattern: 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.keys(): + if p in subst_case: assert isinstance(p, EVar) return subst_case[p] return p @@ -63,7 +63,7 @@ def sub(p: Pattern) -> Pattern: if check_exit_code: assert res.returncode == 0 else: - assert check_func is not None + assert check_func res_pattern = KoreParser(res.stdout).pattern() check_func(res_pattern) From c09d6bf1ef20edb00f508631e6683ef10113d590 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 21 Jun 2024 13:13:58 -0500 Subject: [PATCH 10/16] Document the kfuzz methods --- pyk/src/pyk/ktool/kfuzz.py | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index 02a6d11825c..36b4562e95b 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -26,6 +26,16 @@ 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: @@ -43,6 +53,18 @@ def fuzz( 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!') From 716e7002852eed02dfd1dd2bb4668a8ba0a59e6f Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 21 Jun 2024 13:16:40 -0500 Subject: [PATCH 11/16] Make kintegers parameters keyword arguments --- pyk/src/pyk/ktool/kfuzz.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index 36b4562e95b..4d5ea101811 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -24,7 +24,10 @@ def kintegers( - min_value: int | None = None, max_value: int | None = None, with_inj: KSort | None = None + *, + min_value: int | None = None, + max_value: int | None = None, + with_inj: KSort | None = None, ) -> SearchStrategy[Pattern]: """ Args: From 3688b86e696d4c24fa10b52fbfa788596d46c0e3 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Mon, 24 Jun 2024 11:17:49 -0500 Subject: [PATCH 12/16] Refactor check function for fuzz integration tests. Also loosen the return type for it. --- pyk/src/pyk/ktool/kfuzz.py | 3 ++- pyk/src/tests/integration/ktool/test_fuzz.py | 15 ++++++++------- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index 4d5ea101811..e9901ba2c71 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -16,6 +16,7 @@ if TYPE_CHECKING: from collections.abc import Callable, Mapping from pathlib import Path + from typing import Any from hypothesis.strategies import SearchStrategy @@ -52,7 +53,7 @@ def fuzz( definition_dir: str | Path, template: Pattern, subst_strategy: dict[EVar, SearchStrategy[Pattern]], - check_func: Callable[[Pattern], None] | None = None, + check_func: Callable[[Pattern], Any] | None = None, check_exit_code: bool = False, max_examples: int = 50, ) -> None: diff --git a/pyk/src/tests/integration/ktool/test_fuzz.py b/pyk/src/tests/integration/ktool/test_fuzz.py index 1c4a02e38e6..c8d5e4cec55 100644 --- a/pyk/src/tests/integration/ktool/test_fuzz.py +++ b/pyk/src/tests/integration/ktool/test_fuzz.py @@ -16,7 +16,6 @@ from ..utils import K_FILES, TEST_DATA_DIR if TYPE_CHECKING: - from collections.abc import Callable from pathlib import Path from typing import Final @@ -41,12 +40,12 @@ 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: + def check(p: Pattern) -> None: + def check_inner(p: Pattern) -> Pattern: match p: case Assoc(): symbol = p.symbol() - args = (arg.top_down(checkres) for arg in p.app.args) + 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: @@ -58,7 +57,7 @@ def checkres(p: Pattern) -> Pattern: return p - return lambda pattern: (None, pattern.top_down(checkres))[0] + p.top_down(check_inner) @staticmethod def setup_program(definition_dir: Path, text: str) -> Pattern: @@ -104,7 +103,8 @@ def test_fuzz( init_pattern = self.setup_program(definition_dir, program_text) - fuzz(definition_dir, init_pattern, self.substs(), self.check()) + # Then + fuzz(definition_dir, init_pattern, self.substs(), self.check) def test_fuzz_fail( self, @@ -125,5 +125,6 @@ def test_fuzz_fail( init_pattern = self.setup_program(definition_dir, program_text) + # Then with pytest.raises(AssertionError): - fuzz(definition_dir, init_pattern, self.substs(), self.check()) + fuzz(definition_dir, init_pattern, self.substs(), self.check) From f19d933736da5693cf4cdf3b1d4ec796e19ef96d Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Mon, 24 Jun 2024 12:17:45 -0500 Subject: [PATCH 13/16] Make substs a constant --- pyk/src/tests/integration/ktool/test_fuzz.py | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/pyk/src/tests/integration/ktool/test_fuzz.py b/pyk/src/tests/integration/ktool/test_fuzz.py index c8d5e4cec55..76d34f9d6af 100644 --- a/pyk/src/tests/integration/ktool/test_fuzz.py +++ b/pyk/src/tests/integration/ktool/test_fuzz.py @@ -19,8 +19,6 @@ from pathlib import Path from typing import Final - from hypothesis.strategies import SearchStrategy - from pyk.kore.syntax import Pattern _LOGGER: Final = logging.getLogger(__name__) @@ -34,10 +32,7 @@ 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'))} + SUBSTS = {VAR_X: kintegers(with_inj=KSort('AExp')), VAR_Y: kintegers(with_inj=KSort('AExp'))} @staticmethod def check(p: Pattern) -> None: @@ -104,7 +99,7 @@ def test_fuzz( init_pattern = self.setup_program(definition_dir, program_text) # Then - fuzz(definition_dir, init_pattern, self.substs(), self.check) + fuzz(definition_dir, init_pattern, self.SUBSTS, self.check) def test_fuzz_fail( self, @@ -127,4 +122,4 @@ def test_fuzz_fail( # Then with pytest.raises(AssertionError): - fuzz(definition_dir, init_pattern, self.substs(), self.check) + fuzz(definition_dir, init_pattern, self.SUBSTS, self.check) From d87cae53f53f38d9fc74ef42769abd2876df9102 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Mon, 24 Jun 2024 11:21:21 -0500 Subject: [PATCH 14/16] Sort the dependencies --- pyk/pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml index 3e671aa9d80..9099924036a 100644 --- a/pyk/pyproject.toml +++ b/pyk/pyproject.toml @@ -21,13 +21,13 @@ 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 = "*" textual = "^0.27.0" tomli = "^2.0.1" xdg-base-dirs = "^6.0.1" -hypothesis = "^6.103.1" [tool.poetry.group.dev.dependencies] autoflake = "*" From 2d55fcb2c4564585a34389dd3a624e9023506f31 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Mon, 24 Jun 2024 11:55:36 -0500 Subject: [PATCH 15/16] Update docs --- pyk/src/pyk/ktool/kfuzz.py | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index e9901ba2c71..6370ff38a18 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -31,6 +31,8 @@ def kintegers( 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 @@ -57,17 +59,23 @@ def fuzz( check_exit_code: bool = False, max_examples: int = 50, ) -> None: - """Use this to fuzz a property test with concrete execution over a K term. + """ + 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 + 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. + 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 + 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!') From 9df146b8a0f4fedd01af6e939b5c3c8b221bd490 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Mon, 24 Jun 2024 12:59:54 -0500 Subject: [PATCH 16/16] Doc formatting --- pyk/src/pyk/ktool/kfuzz.py | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index 6370ff38a18..b2d02971564 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -30,8 +30,7 @@ def kintegers( max_value: int | None = None, with_inj: KSort | None = None, ) -> SearchStrategy[Pattern]: - """ - Return a search strategy for K integers. + """Return a search strategy for K integers. Args: min_value: Minimum value for the generated integers @@ -59,8 +58,7 @@ def fuzz( check_exit_code: bool = False, max_examples: int = 50, ) -> None: - """ - Fuzz a property test with concrete execution over a K term. + """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.