From fe1674dbda3818100a23f38b259bff58c9c4d19d Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 28 Jun 2024 11:23:48 -0500 Subject: [PATCH 1/8] KFuzz class --- pyk/src/pyk/ktool/kfuzz.py | 58 +++++++++++++------- pyk/src/tests/integration/ktool/test_fuzz.py | 12 ++-- 2 files changed, 47 insertions(+), 23 deletions(-) diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index b2d02971564..59bc1e64eb8 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/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 Assoc, EVar -from ..prelude.k import inj -from ..prelude.kint import intToken +from ..kore.prelude import inj +from ..kore.syntax import DV, Assoc, EVar, SortApp, String from .krun import llvm_interpret_raw if TYPE_CHECKING: @@ -20,15 +17,37 @@ from hypothesis.strategies import SearchStrategy - from ..kast.inner import KInner from ..kore.syntax import Pattern + +class KFuzz: + 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], + ) -> None: + _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]], + ) -> None: + _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,15 +61,15 @@ 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( +def _fuzz( definition_dir: str | Path, template: Pattern, subst_strategy: dict[EVar, SearchStrategy[Pattern]], @@ -80,14 +99,15 @@ 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: assert isinstance(p, EVar) return subst_case[p] - return p + elif 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),)) + else: + return p test_pattern = template.top_down(sub) res = llvm_interpret_raw(definition_dir, test_pattern.text) diff --git a/pyk/src/tests/integration/ktool/test_fuzz.py b/pyk/src/tests/integration/ktool/test_fuzz.py index 76d34f9d6af..1c819b29ca9 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.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.kfuzz import KFuzz, kintegers from pyk.ktool.kprint import _kast from pyk.testing import KompiledTest @@ -32,7 +32,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: @@ -99,7 +103,7 @@ 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, @@ -122,4 +126,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) From 4310cea8bdfe7a2e66007266315d69eb8a94adc9 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 28 Jun 2024 12:17:52 -0500 Subject: [PATCH 2/8] Improve performance. `p in subst` hashes the term and is very expensive, but we only need to do it if p is an EVar. --- pyk/src/pyk/ktool/kfuzz.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index 59bc1e64eb8..d4838452d96 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -99,8 +99,7 @@ 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] elif isinstance(p, Assoc): symbol = p.symbol() From 6d8214143091d37abda8996e19948ef4480fbddb Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Mon, 1 Jul 2024 15:21:07 -0500 Subject: [PATCH 3/8] Check recursion limit, as hypothesis sometimes resets it. --- pyk/src/pyk/ktool/kfuzz.py | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index d4838452d96..47610d328a3 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -1,8 +1,11 @@ from __future__ import annotations +import sys +import warnings from typing import TYPE_CHECKING from hypothesis import Phase, given, settings +from hypothesis.errors import HypothesisWarning from hypothesis.strategies import fixed_dictionaries, integers from ..kore.parser import KoreParser @@ -20,6 +23,7 @@ from ..kore.syntax import Pattern +REC_LIMIT = 10**7 class KFuzz: definition_dir: Path @@ -98,6 +102,10 @@ def _fuzz( raise RuntimeError('Must pass one of check_func or check_exit_code, and not both!') def test(subst_case: Mapping[EVar, Pattern]) -> None: + if sys.getrecursionlimit() < REC_LIMIT: + # Reset the recursion limit, hypothesis changes it. + sys.setrecursionlimit(REC_LIMIT) + def sub(p: Pattern) -> Pattern: if isinstance(p, EVar) and p in subst_case: return subst_case[p] @@ -120,6 +128,9 @@ def sub(p: Pattern) -> Pattern: strat: SearchStrategy = fixed_dictionaries(subst_strategy) + # Suppress warnings from hypothesis about changing the recursion limit + warnings.filterwarnings('ignore', message='The recursion limit', category=HypothesisWarning, append=True) + given(strat)( settings( deadline=50000, From 104d40a4a8d9d8f22f77f9ddcf90619fec005d41 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Mon, 1 Jul 2024 16:25:29 -0500 Subject: [PATCH 4/8] Update tests --- pyk/src/tests/integration/ktool/test_fuzz.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pyk/src/tests/integration/ktool/test_fuzz.py b/pyk/src/tests/integration/ktool/test_fuzz.py index 1c819b29ca9..16cab6c0306 100644 --- a/pyk/src/tests/integration/ktool/test_fuzz.py +++ b/pyk/src/tests/integration/ktool/test_fuzz.py @@ -5,7 +5,6 @@ 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 @@ -84,6 +83,7 @@ def replace_var_ids(p: Pattern) -> Pattern: def test_fuzz( self, definition_dir: Path, + kfuzz: KFuzz, ) -> None: # Given program_text = """ @@ -108,6 +108,7 @@ def test_fuzz( def test_fuzz_fail( self, definition_dir: Path, + kfuzz: KFuzz, ) -> None: # Given program_text = """ From 5cc6f7c2bede0f955f7d91faf4332eb0f5d61302 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Mon, 1 Jul 2024 15:22:07 -0500 Subject: [PATCH 5/8] More flexibility with hypothesis settings --- pyk/src/pyk/ktool/kfuzz.py | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index 47610d328a3..38f7e48d748 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -25,6 +25,7 @@ REC_LIMIT = 10**7 + class KFuzz: definition_dir: Path @@ -79,7 +80,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. @@ -93,7 +94,10 @@ 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. @@ -131,11 +135,8 @@ def sub(p: Pattern) -> Pattern: # Suppress warnings from hypothesis about changing the recursion limit warnings.filterwarnings('ignore', message='The recursion limit', category=HypothesisWarning, append=True) - 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))() From d451505610585b7a4bf92c961ee19449bd9a6efc Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Mon, 1 Jul 2024 16:45:26 -0500 Subject: [PATCH 6/8] Add a docstring --- pyk/src/pyk/ktool/kfuzz.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index 38f7e48d748..7d762cdaaef 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -27,6 +27,8 @@ class KFuzz: + """Interface for fuzzing over property tests in K.""" + definition_dir: Path def __init__(self, definition_dir: Path) -> None: From 71bc069f479a88aa7d5bbf51aec5a201191bc019 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Wed, 3 Jul 2024 10:12:27 -0500 Subject: [PATCH 7/8] Don't try to maintain the recursion limit. Our traversals are no longer deeply nested. --- pyk/src/pyk/ktool/kfuzz.py | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index 3a7c95aad35..51e8b907191 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -1,11 +1,8 @@ from __future__ import annotations -import sys -import warnings from typing import TYPE_CHECKING from hypothesis import Phase, given, settings -from hypothesis.errors import HypothesisWarning from hypothesis.strategies import fixed_dictionaries, integers from ..kore.parser import KoreParser @@ -23,9 +20,6 @@ from ..kore.syntax import Pattern -REC_LIMIT = 10**7 - - class KFuzz: """Interface for fuzzing over property tests in K.""" @@ -108,10 +102,6 @@ def _fuzz( raise RuntimeError('Must pass one of check_func or check_exit_code, and not both!') def test(subst_case: Mapping[EVar, Pattern]) -> None: - if sys.getrecursionlimit() < REC_LIMIT: - # Reset the recursion limit, hypothesis changes it. - sys.setrecursionlimit(REC_LIMIT) - def sub(p: Pattern) -> Pattern: if isinstance(p, EVar) and p in subst_case: return subst_case[p] @@ -130,9 +120,6 @@ def sub(p: Pattern) -> Pattern: strat: SearchStrategy = fixed_dictionaries(subst_strategy) - # Suppress warnings from hypothesis about changing the recursion limit - warnings.filterwarnings('ignore', message='The recursion limit', category=HypothesisWarning, append=True) - # Default settings for hypothesis hypothesis_args.setdefault('deadline', 5000) hypothesis_args.setdefault('phases', (Phase.explicit, Phase.reuse, Phase.generate)) From 47a187bfb104aff9eb504bb111538e8d6a8b4b37 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Wed, 3 Jul 2024 15:44:56 -0500 Subject: [PATCH 8/8] Docstrings --- pyk/src/pyk/ktool/kfuzz.py | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index 51e8b907191..15c8e79a0e4 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -33,15 +33,25 @@ def fuzz_with_check( template: Pattern, subst_strategy: dict[EVar, SearchStrategy[Pattern]], check_func: Callable[[Pattern], Any], + **hypothesis_args: Any, ) -> None: - _fuzz(self.definition_dir, template, subst_strategy, check_func=check_func) + """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(self.definition_dir, template, subst_strategy, check_exit_code=True) + """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( @@ -70,7 +80,7 @@ def int_dv(value: int) -> Pattern: return integers(min_value=min_value, max_value=max_value).map(int_dv) -def _fuzz( +def fuzz( definition_dir: str | Path, template: Pattern, subst_strategy: dict[EVar, SearchStrategy[Pattern]], @@ -91,7 +101,9 @@ def _fuzz( 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. hypothesis_args: Keyword arguments that will be passed as settings for the hypothesis test. Defaults: + deadline: 5000 + phases: (Phase.explicit, Phase.reuse, Phase.generate)