Skip to content

Commit

Permalink
raise Unsatisfiable despite alt backend
Browse files Browse the repository at this point in the history
  • Loading branch information
Zac-HD committed Nov 28, 2024
1 parent eed8693 commit 8ebe5b8
Show file tree
Hide file tree
Showing 2 changed files with 40 additions and 14 deletions.
21 changes: 15 additions & 6 deletions hypothesis-python/src/hypothesis/internal/conjecture/engine.py
Original file line number Diff line number Diff line change
Expand Up @@ -284,6 +284,12 @@ def __init__(
self.__failed_realize_count = 0
self._verified_by = None # note unsound verification by alt backends

@property
def using_hypothesis_backend(self):
return (
self.settings.backend == "hypothesis" or self._switch_to_hypothesis_provider
)

def explain_next_call_as(self, explanation: str) -> None:
self.__pending_call_explanation = explanation

Expand Down Expand Up @@ -314,7 +320,7 @@ def should_optimise(self) -> bool:
return Phase.target in self.settings.phases

def __tree_is_exhausted(self) -> bool:
return self.tree.is_exhausted and self.settings.backend == "hypothesis"
return self.tree.is_exhausted and self.using_hypothesis_backend

def __stoppable_test_function(self, data: ConjectureData) -> None:
"""Run ``self._test_function``, but convert a ``StopTest`` exception
Expand Down Expand Up @@ -475,6 +481,9 @@ def test_function(self, data: ConjectureData) -> None:
and (self.__failed_realize_count / self.call_count) > 0.2
):
self._switch_to_hypothesis_provider = True
# skip the post-test-case tracking; we're pretending this never happened
interrupted = True
return
except BaseException:
self.save_buffer(data.buffer)
raise
Expand Down Expand Up @@ -562,7 +571,7 @@ def test_function(self, data: ConjectureData) -> None:
self.valid_examples += 1

if data.status == Status.INTERESTING:
if self.settings.backend != "hypothesis":
if not self.using_hypothesis_backend:
# drive the ir tree through the test function to convert it
# to a buffer
initial_origin = data.interesting_origin
Expand Down Expand Up @@ -1034,7 +1043,7 @@ def generate_new_examples(self) -> None:
# a buffer and uses HypothesisProvider as its backing provider,
# not whatever is specified by the backend. We can improve this
# once more things are on the ir.
if self.settings.backend != "hypothesis":
if not self.using_hypothesis_backend:
data = self.new_conjecture_data(prefix=b"", max_length=BUFFER_SIZE)
with suppress(BackendCannotProceed):
self.test_function(data)
Expand Down Expand Up @@ -1310,7 +1319,7 @@ def new_conjecture_data_ir(
HypothesisProvider if self._switch_to_hypothesis_provider else self.provider
)
observer = observer or self.tree.new_observer()
if self.settings.backend != "hypothesis":
if not self.using_hypothesis_backend:
observer = DataObserver()

return ConjectureData.for_ir_tree(
Expand All @@ -1331,7 +1340,7 @@ def new_conjecture_data(
HypothesisProvider if self._switch_to_hypothesis_provider else self.provider
)
observer = observer or self.tree.new_observer()
if self.settings.backend != "hypothesis":
if not self.using_hypothesis_backend:
observer = DataObserver()

return ConjectureData(
Expand Down Expand Up @@ -1499,7 +1508,7 @@ def check_result(
prefix=buffer, max_length=max_length, observer=observer
)

if self.settings.backend == "hypothesis":
if self.using_hypothesis_backend:
try:
self.tree.simulate_test_function(dummy_data)
except PreviouslyUnseenBehaviour:
Expand Down
33 changes: 25 additions & 8 deletions hypothesis-python/tests/conjecture/test_alt_backend.py
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
# v. 2.0. If a copy of the MPL was not distributed with this file, You can
# obtain one at https://mozilla.org/MPL/2.0/.

import itertools
import math
import sys
from contextlib import contextmanager
Expand All @@ -16,14 +17,15 @@

import pytest

from hypothesis import given, settings, strategies as st
from hypothesis import HealthCheck, assume, given, settings, strategies as st
from hypothesis.control import current_build_context
from hypothesis.database import InMemoryExampleDatabase
from hypothesis.errors import (
BackendCannotProceed,
Flaky,
HypothesisException,
InvalidArgument,
Unsatisfiable,
)
from hypothesis.internal.compat import int_to_bytes
from hypothesis.internal.conjecture.data import (
Expand Down Expand Up @@ -492,15 +494,13 @@ def test_function(_):
class FallibleProvider(TrivialProvider):
def __init__(self, conjecturedata: "ConjectureData", /) -> None:
super().__init__(conjecturedata)
self.prng = Random(0)
self._it = itertools.cycle([1, 1, 1, "discard_test_case", "other"])

def draw_integer(self, *args, **kwargs):
# This is frequent enough that we'll get coverage of the "give up and go
# back to Hypothesis' standard backend" code path.
if self.prng.getrandbits(1):
scope = self.prng.choice(["discard_test_case", "other"])
raise BackendCannotProceed(scope)
return 1
x = next(self._it)
if isinstance(x, str):
raise BackendCannotProceed(x)
return x


def test_falls_back_to_default_backend():
Expand All @@ -517,6 +517,23 @@ def test_function(x):
assert seen_other_ints # must have swapped backends then


def test_can_raise_unsatisfiable_after_falling_back():
with temp_register_backend("fallible", FallibleProvider):

@given(st.integers())
@settings(
backend="fallible",
database=None,
max_examples=100,
suppress_health_check=[HealthCheck.filter_too_much],
)
def test_function(x):
assume(x == "unsatisfiable")

with pytest.raises(Unsatisfiable):
test_function()


class ExhaustibleProvider(TrivialProvider):
scope = "exhausted"

Expand Down

0 comments on commit 8ebe5b8

Please sign in to comment.