Merge pull request #4092 from Zac-HD/backend-cannot-proceed

Add `BackendCannotProceed` to improve integration

hypothesis-python/RELEASE.rst

@@ -0,0 +1,4 @@
+RELEASE_TYPE: minor
+
+This release adds ``hypothesis.errors.BackendCannotProceed``, an unstable API
+for use by :ref:`alternative-backends`.

hypothesis-python/src/hypothesis/core.py

@@ -55,6 +55,7 @@
 )
 from hypothesis.control import BuildContext
 from hypothesis.errors import (
+    BackendCannotProceed,
     DeadlineExceeded,
     DidNotReproduce,
     FailedHealthCheck,
@@ -1063,7 +1064,7 @@ def _execute_once_for_engine(self, data: ConjectureData) -> None:
                 # This was unexpected, meaning that the assume was flaky.
                 # Report it as such.
                 raise self._flaky_replay_to_failure(err, e) from None
-        except StopTest:
+        except (StopTest, BackendCannotProceed):
             # The engine knows how to handle this control exception, so it's
             # OK to re-raise it.
             raise
@@ -1122,10 +1123,15 @@ def _execute_once_for_engine(self, data: ConjectureData) -> None:
                     self.settings.backend != "hypothesis"
                     and not getattr(runner, "_switch_to_hypothesis_provider", False)
                 )
-                data._observability_args = data.provider.realize(
-                    data._observability_args
-                )
-                self._string_repr = data.provider.realize(self._string_repr)
+                try:
+                    data._observability_args = data.provider.realize(
+                        data._observability_args
+                    )
+                    self._string_repr = data.provider.realize(self._string_repr)
+                except BackendCannotProceed:
+                    data._observability_args = {}
+                    self._string_repr = "<backend failed to realize symbolic arguments>"
+
                 tc = make_testcase(
                     start_timestamp=self._start_timestamp,
                     test_name_or_nodeid=self.test_identifier,
@@ -1335,10 +1341,17 @@ def run_engine(self):
                 # finished and they can't draw more data from it.
                 ran_example.freeze()  # pragma: no branch
                 # No branch is possible here because we never have an active exception.
-        _raise_to_user(errors_to_report, self.settings, report_lines)
+        _raise_to_user(
+            errors_to_report,
+            self.settings,
+            report_lines,
+            verified_by=runner._verified_by,
+        )
 
 
-def _raise_to_user(errors_to_report, settings, target_lines, trailer=""):
+def _raise_to_user(
+    errors_to_report, settings, target_lines, trailer="", verified_by=None
+):
     """Helper function for attaching notes and grouping multiple errors."""
     failing_prefix = "Falsifying example: "
     ls = []
@@ -1362,6 +1375,11 @@ def _raise_to_user(errors_to_report, settings, target_lines, trailer=""):
     if settings.verbosity >= Verbosity.normal:
         for line in target_lines:
             add_note(the_error_hypothesis_found, line)
+
+    if verified_by:
+        msg = f"backend={verified_by!r} claimed to verify this test passes - please send them a bug report!"
+        add_note(err, msg)
+
     raise the_error_hypothesis_found
 
 

hypothesis-python/src/hypothesis/errors.py

@@ -8,6 +8,8 @@
 # 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/.
 
+from typing import Literal
+
 from hypothesis.internal.compat import ExceptionGroup
 
 
@@ -237,3 +239,36 @@ def __init__(self, target: object) -> None:
 class SmallSearchSpaceWarning(HypothesisWarning):
     """Indicates that an inferred strategy does not span the search space
     in a meaningful way, for example by only creating default instances."""
+
+
+class BackendCannotProceed(HypothesisException):
+    """UNSTABLE API
+
+    Raised by alternative backends when the PrimitiveProvider cannot proceed.
+    This is expected to occur inside one of the `.draw_*()` methods, or for
+    symbolic execution perhaps in `.realize(...)`.
+
+    The optional `scope` argument can enable smarter integration:
+
+        verified:
+            Do not request further test cases from this backend.  We _may_
+            generate more test cases with other backends; if one fails then
+            Hypothesis will report unsound verification in the backend too.
+
+        exhausted:
+            Do not request further test cases from this backend; finish testing
+            with test cases generated with the default backend.  Common if e.g.
+            native code blocks symbolic reasoning very early.
+
+        discard_test_case:
+            This particular test case could not be converted to concrete values;
+            skip any further processing and continue with another test case from
+            this backend.
+    """
+
+    def __init__(
+        self,
+        scope: Literal["verified", "exhausted", "discard_test_case", "other"] = "other",
+        /,
+    ) -> None:
+        self.scope = scope

hypothesis-python/src/hypothesis/internal/conjecture/data.py

@@ -1254,7 +1254,8 @@ def realize(self, value: T) -> T:
         symbolic before calling `realize`, so you should handle the case where
         `value` is non-symbolic.
 
-        The returned value should be non-symbolic.
+        The returned value should be non-symbolic.  If you cannot provide a value,
+        raise hypothesis.errors.BackendCannotProceed("discard_test_case")
         """
         return value
 

hypothesis-python/src/hypothesis/internal/conjecture/engine.py

@@ -13,7 +13,7 @@
 import textwrap
 import time
 from collections import defaultdict
-from contextlib import contextmanager
+from contextlib import contextmanager, suppress
 from datetime import timedelta
 from enum import Enum
 from random import Random, getrandbits
@@ -41,6 +41,7 @@
 from hypothesis._settings import local_settings
 from hypothesis.database import ExampleDatabase
 from hypothesis.errors import (
+    BackendCannotProceed,
     FlakyReplay,
     HypothesisException,
     InvalidArgument,
@@ -270,6 +271,9 @@ def __init__(
         self.__pending_call_explanation: Optional[str] = None
         self._switch_to_hypothesis_provider: bool = False
 
+        self.__failed_realize_count = 0
+        self._verified_by = None  # note unsound verification by alt backends
+
     def explain_next_call_as(self, explanation: str) -> None:
         self.__pending_call_explanation = explanation
 
@@ -425,6 +429,18 @@ def test_function(self, data: ConjectureData) -> None:
         except KeyboardInterrupt:
             interrupted = True
             raise
+        except BackendCannotProceed as exc:
+            if exc.scope in ("verified", "exhausted"):
+                self._switch_to_hypothesis_provider = True
+                if exc.scope == "verified":
+                    self._verified_by = self.settings.backend
+            elif exc.scope == "discard_test_case":
+                self.__failed_realize_count += 1
+                if (
+                    self.__failed_realize_count > 10
+                    and (self.__failed_realize_count / self.call_count) > 0.2
+                ):
+                    self._switch_to_hypothesis_provider = True
         except BaseException:
             self.save_buffer(data.buffer)
             raise
@@ -976,7 +992,8 @@ def generate_new_examples(self) -> None:
             # once more things are on the ir.
             if self.settings.backend != "hypothesis":
                 data = self.new_conjecture_data(prefix=b"", max_length=BUFFER_SIZE)
-                self.test_function(data)
+                with suppress(BackendCannotProceed):
+                    self.test_function(data)
                 continue
 
             self._current_phase = "generate"

hypothesis-python/tests/conjecture/test_alt_backend.py

@@ -19,7 +19,12 @@
 from hypothesis import given, settings, strategies as st
 from hypothesis.control import current_build_context
 from hypothesis.database import InMemoryExampleDatabase
-from hypothesis.errors import Flaky, HypothesisException, InvalidArgument
+from hypothesis.errors import (
+    BackendCannotProceed,
+    Flaky,
+    HypothesisException,
+    InvalidArgument,
+)
 from hypothesis.internal.compat import int_to_bytes
 from hypothesis.internal.conjecture.data import (
     AVAILABLE_PROVIDERS,
@@ -454,6 +459,10 @@ def observe_information_messages(self, *, lifetime):
             yield {"type": "alert", "title": "Trivial alert", "content": "message here"}
             yield {"type": "info", "title": "trivial-data", "content": {"k2": "v2"}}
 
+    def realize(self, value):
+        # Get coverage of the can't-realize path for observability outputs
+        raise BackendCannotProceed
+
 
 def test_custom_observations_from_backend():
     with temp_register_backend("observable", ObservableProvider):
@@ -470,10 +479,75 @@ def test_function(_):
     cases = [t["metadata"]["backend"] for t in ls if t["type"] == "test_case"]
     assert {"msg_key": "some message", "data_key": [1, "2", {}]} in cases
 
+    assert "<backend failed to realize symbolic arguments>" in repr(ls)
+
     infos = [
         {k: v for k, v in t.items() if k in ("title", "content")}
         for t in ls
         if t["type"] != "test_case"
     ]
     assert {"title": "Trivial alert", "content": "message here"} in infos
     assert {"title": "trivial-data", "content": {"k2": "v2"}} in infos
+
+
+class FallibleProvider(TrivialProvider):
+    def __init__(self, conjecturedata: "ConjectureData", /) -> None:
+        super().__init__(conjecturedata)
+        self.prng = Random(0)
+
+    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
+
+
+def test_falls_back_to_default_backend():
+    with temp_register_backend("fallible", FallibleProvider):
+        seen_other_ints = False
+
+        @given(st.integers())
+        @settings(backend="fallible", database=None, max_examples=100)
+        def test_function(x):
+            nonlocal seen_other_ints
+            seen_other_ints |= x != 1
+
+        test_function()
+        assert seen_other_ints  # must have swapped backends then
+
+
+class ExhaustibleProvider(TrivialProvider):
+    scope = "exhausted"
+
+    def __init__(self, conjecturedata: "ConjectureData", /) -> None:
+        super().__init__(conjecturedata)
+        self._calls = 0
+
+    def draw_integer(self, *args, **kwargs):
+        self._calls += 1
+        if self._calls > 20:
+            # This is complete nonsense of course, so we'll see Hypothesis complain
+            # that we found a problem after the backend reported verification.
+            raise BackendCannotProceed(self.scope)
+        return 1
+
+
+class UnsoundVerifierProvider(ExhaustibleProvider):
+    scope = "verified"
+
+
+@pytest.mark.parametrize("provider", [ExhaustibleProvider, UnsoundVerifierProvider])
+def test_notes_incorrect_verification(provider):
+    msg = "backend='p' claimed to verify this test passes - please send them a bug report!"
+    with temp_register_backend("p", provider):
+
+        @given(st.integers())
+        @settings(backend="p", database=None, max_examples=100)
+        def test_function(x):
+            assert x == 1  # True from this backend, false in general!
+
+        with pytest.raises(AssertionError) as ctx:
+            test_function()
+        assert (msg in ctx.value.__notes__) == (provider is UnsoundVerifierProvider)

hypothesis-python/tests/cover/test_regressions.py

@@ -137,6 +137,7 @@ def test_prng_state_unpolluted_by_given_issue_1266():
         interesting_origins=[InterestingOrigin.from_exception(BaseException())],
     ),
     errors.FlakyFailure("check with BaseException", [BaseException()]),
+    errors.BackendCannotProceed("verified"),
 ]