wip: hacky impl of BackendCannotProceed

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,
@@ -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,

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):
 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.
+
+        not_realizable:
+            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", "not_realizable", "other"] = "other",
+        /,
+    ) -> None:
+        self.scope = scope

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

@@ -1243,7 +1243,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`.
         """
         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,
@@ -51,6 +52,7 @@
     NotRequired,
     TypeAlias,
     TypedDict,
+    add_note,
     ceil,
     int_from_bytes,
     override,
@@ -269,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.__backend_claimed_verified = False
+
     def explain_next_call_as(self, explanation: str) -> None:
         self.__pending_call_explanation = explanation
 
@@ -424,7 +429,18 @@ def test_function(self, data: ConjectureData) -> None:
         except KeyboardInterrupt:
             interrupted = True
             raise
-        except BaseException:
+        except BaseException as err:
+            if isinstance(err, BackendCannotProceed):
+                if err.scope in ("verified", "exhausted"):
+                    self._switch_to_hypothesis_provider = True
+                    self.__backend_claimed_verified = err.scope == "verified"
+                elif err.scope == "not_realizable":
+                    self.__failed_realize_count += 1
+                    if self.__failed_realize_count > 10:
+                        self._switch_to_hypothesis_provider = True
+            elif self.__backend_claimed_verified:
+                msg = f"backend={self.settings.backend!r} verified this test passes - please report that as a bug!"
+                add_note(err, msg)
             self.save_buffer(data.buffer)
             raise
         finally:
@@ -975,7 +991,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"