Add and use `realize` and `avoid_realization` backend hooks #4029

tybug · 2024-07-04T20:38:46Z

post_test_case_hook has been renamed to realize and is used in more places where we want to realize symbolic values
avoid_realization backend class variable added, which backends can set to disable features that would cause premature realization
I've tentatively exposed hypothesis.provisional.realize as part of our unstable-but-public api, to address Storing symbolic values outside of the test case lifetime pschanely/hypothesis-crosshair#7 among others. If we want to make this less public, we can put it in hypothesis.internal.conjecture.data for now.

@pschanely here are the local modifications I made to hypothesis-crosshair:

class CrossHairPrimitiveProvider(PrimitiveProvider):
    avoid_realization = True
    ...
    def realize(self, value):
        return self.export_value(value)

This includes a fix for observability crashes (#3914 (comment)). However, I get the following z3 unknown sat error when running crosshair with observability - any ideas @pschanely?

@given(st.integers(), st.integers())
@settings(database=None, deadline=None, backend="crosshair")
def f(n1, n2):
    assert n1 != 123454 or n2 != 12983
f()

1835780.259|                    |solver_is_sat() Z3 unknown sat reason: canceled
1835780.266|                    |solver_is_sat() Unknown satisfiability. Solver state follows:
 (declare-fun int_01 () Int)
(declare-fun newline (Int) Bool)
(declare-fun int_02 () Int)
(assert (not (> 0 int_01)))
(assert (not (<= 10 int_01)))
(assert (forall ((c Int))
  (! (= (newline c)
        (or (= 10 c)
            (= 11 c)
            (= 12 c)
            (= 13 c)
            (= 28 c)
            (= 29 c)
            (= 30 c)
            (= 133 c)
            (= 8232 c)
            (= 8233 c)))
     :pattern ((newline c)))))
(assert (not (newline (+ 48 int_01))))
(assert (not (and (= 10 (+ 48 int_01)))))
(assert (not (> 0 int_02)))
(assert (<= 10 int_02))
(assert (not (= 10 0)))
(assert (>= 10 0))
(assert (>= int_02 0))
(assert (<= 10 (div int_02 10)))
(assert (>= (div int_02 10) 0))
(assert (<= 10 (div (div int_02 10) 10)))
(assert (>= (div (div int_02 10) 10) 0))
(assert (<= 10 (div (div (div int_02 10) 10) 10)))
(assert (>= (div (div (div int_02 10) 10) 10) 0))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
  (<= 10 a!1)))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
  (>= a!1 0)))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
  (<= 10 (div a!1 10))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
  (>= (div a!1 10) 0)))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
  (<= 10 (div (div a!1 10) 10))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
  (>= (div (div a!1 10) 10) 0)))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
  (<= 10 (div (div (div a!1 10) 10) 10))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
  (>= (div (div (div a!1 10) 10) 10) 0)))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
  (<= 10 a!2))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
  (>= a!2 0))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
  (<= 10 (div a!2 10)))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
  (>= (div a!2 10) 0))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
  (<= 10 (div (div a!2 10) 10)))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
  (>= (div (div a!2 10) 10) 0))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
  (<= 10 (div (div (div a!2 10) 10) 10)))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
  (>= (div (div (div a!2 10) 10) 10) 0))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
(let ((a!3 (div (div (div (div a!2 10) 10) 10) 10)))
  (not (<= 10 a!3))))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
(let ((a!3 (div (div (div (div a!2 10) 10) 10) 10)))
  (not (newline (+ 48 a!3)))))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
(let ((a!3 (mod (div (div (div a!2 10) 10) 10) 10)))
  (not (newline (+ 48 a!3)))))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
(let ((a!3 (+ 48 (mod (div (div a!2 10) 10) 10))))
  (not (newline a!3))))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
(let ((a!3 (newline (+ 48 (mod (div a!2 10) 10)))))
  (not a!3)))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
  (not (newline (+ 48 (mod a!2 10)))))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (mod (div (div (div a!1 10) 10) 10) 10)))
  (not (newline (+ 48 a!2))))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (+ 48 (mod (div (div a!1 10) 10) 10))))
  (not (newline a!2)))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (newline (+ 48 (mod (div a!1 10) 10)))))
  (not a!2))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
  (not (newline (+ 48 (mod a!1 10))))))
(assert (let ((a!1 (mod (div (div (div int_02 10) 10) 10) 10)))
  (not (newline (+ 48 a!1)))))
(assert (let ((a!1 (+ 48 (mod (div (div int_02 10) 10) 10))))
  (not (newline a!1))))
(assert (let ((a!1 (newline (+ 48 (mod (div int_02 10) 10)))))
  (not a!1)))
(assert (not (newline (+ 48 (mod int_02 10)))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
(let ((a!3 (div (div (div (div a!2 10) 10) 10) 10)))
  (not (and (= 10 (+ 48 a!3))))))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
(let ((a!3 (mod (div (div (div a!2 10) 10) 10) 10)))
  (not (and (= 10 (+ 48 a!3))))))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
(let ((a!3 (+ 48 (mod (div (div a!2 10) 10) 10))))
  (not (and (= 10 a!3)))))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
(let ((a!3 (= 10 (+ 48 (mod (div a!2 10) 10)))))
  (not (and a!3))))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (div (div (div (div a!1 10) 10) 10) 10)))
(let ((a!3 (and (= 10 (+ 48 (mod a!2 10))))))
  (not a!3)))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (mod (div (div (div a!1 10) 10) 10) 10)))
  (not (and (= 10 (+ 48 a!2)))))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (+ 48 (mod (div (div a!1 10) 10) 10))))
  (not (and (= 10 a!2))))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (= 10 (+ 48 (mod (div a!1 10) 10)))))
  (not (and a!2)))))
(assert (let ((a!1 (div (div (div (div int_02 10) 10) 10) 10)))
(let ((a!2 (and (= 10 (+ 48 (mod a!1 10))))))
  (not a!2))))
(assert (let ((a!1 (mod (div (div (div int_02 10) 10) 10) 10)))
  (not (and (= 10 (+ 48 a!1))))))
(assert (let ((a!1 (+ 48 (mod (div (div int_02 10) 10) 10))))
  (not (and (= 10 a!1)))))
(assert (let ((a!1 (= 10 (+ 48 (mod (div int_02 10) 10)))))
  (not (and a!1))))
(assert (let ((a!1 (and (= 10 (+ 48 (mod int_02 10))))))
  (not a!1)))
(assert (not (<= 9223372036854775808 (ite (< int_01 0) (- int_01) int_01))))
(assert (not (<= 9223372036854775808 (ite (< int_02 0) (- int_02) int_02))))
(assert (distinct 123454 int_01))
(assert (= 0 int_01))
(assert (= 1009639649990 int_02))
(assert (= 48 (+ 48 int_01)))

1835780.266|                     |__init__() UnknownSatisfiability 
1835780.267|           |condition_parser() Using parsers:  []
1835780.269|           |condition_parser() Using parsers:  []
1835780.271|           |condition_parser() Using parsers:  []
1835780.273|           |condition_parser() Using parsers:  []
1835780.275|           |condition_parser() Using parsers:  []
1835780.277|           |condition_parser() Using parsers:  []
1835780.279|           |condition_parser() Using parsers:  []
1835780.281|           |condition_parser() Using parsers:  []
You can add @seed(190406573799112539951356386259003876502) to this test to reproduce this failure.
Traceback (most recent call last):
  File "/Users/tybug/Desktop/Liam/coding/sandbox/hypothesis_/sandbox4.py", line 117, in <module>
    f()
  File "/Users/tybug/Desktop/Liam/coding/sandbox/hypothesis_/sandbox4.py", line 115, in f
    def f(n1, n2):
                   
  File "/Users/tybug/Desktop/Liam/coding/hypothesis/hypothesis-python/src/hypothesis/core.py", line 1661, in wrapped_test
    raise the_error_hypothesis_found
  File "/Users/tybug/Desktop/Liam/coding/hypothesis/hypothesis-python/src/hypothesis/core.py", line 1628, in wrapped_test
    state.run_engine()
  File "/Users/tybug/Desktop/Liam/coding/hypothesis/hypothesis-python/src/hypothesis/core.py", line 1156, in run_engine
    runner.run()
  File "/Users/tybug/Desktop/Liam/coding/hypothesis/hypothesis-python/src/hypothesis/internal/conjecture/engine.py", line 759, in run
    self._run()
  File "/Users/tybug/Desktop/Liam/coding/hypothesis/hypothesis-python/src/hypothesis/internal/conjecture/engine.py", line 1221, in _run
    self.generate_new_examples()
  File "/Users/tybug/Desktop/Liam/coding/hypothesis/hypothesis-python/src/hypothesis/internal/conjecture/engine.py", line 977, in generate_new_examples
    self.test_function(data)
  File "/Users/tybug/Desktop/Liam/coding/hypothesis/hypothesis-python/src/hypothesis/internal/conjecture/engine.py", line 434, in test_function
    self.__stoppable_test_function(data)
  File "/Users/tybug/Desktop/Liam/coding/hypothesis/hypothesis-python/src/hypothesis/internal/conjecture/engine.py", line 307, in __stoppable_test_function
    self._test_function(data)
  File "/Users/tybug/Desktop/Liam/coding/hypothesis/hypothesis-python/src/hypothesis/core.py", line 1119, in _execute_once_for_engine
    self._string_repr = data.provider.realize(self._string_repr)
                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/lib/python3.12/site-packages/hypothesis_crosshair_provider/crosshair_provider.py", line 297, in realize
    return self.export_value(value)
           ^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/lib/python3.12/site-packages/hypothesis_crosshair_provider/crosshair_provider.py", line 294, in export_value
    return deep_realize(value)
           ^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/lib/python3.12/site-packages/crosshair/core.py", line 251, in deep_realize
    return deepcopyext(value, CopyMode.REALIZE, {})
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/lib/python3.12/site-packages/crosshair/copyext.py", line 37, in deepcopyext
    obj = obj.__ch_realize__()  # type: ignore
          ^^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/lib/python3.12/site-packages/crosshair/libimpl/builtinslib.py", line 3149, in __ch_realize__
    return "".join(chr(realize(x)) for x in codepoints)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/lib/python3.12/site-packages/crosshair/libimpl/builtinslib.py", line 3149, in <genexpr>
    return "".join(chr(realize(x)) for x in codepoints)
                       ^^^^^^^^^^
  File "/opt/homebrew/lib/python3.12/site-packages/crosshair/core.py", line 244, in realize
    return value.__ch_realize__()  # type: ignore
           ^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/lib/python3.12/site-packages/crosshair/libimpl/builtinslib.py", line 1112, in __ch_realize__
    return context_statespace().find_model_value(self.var)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/lib/python3.12/site-packages/crosshair/statespace.py", line 927, in find_model_value
    ModelValueNode(self._random, expr, self.solver)
  File "/opt/homebrew/lib/python3.12/site-packages/crosshair/statespace.py", line 667, in __init__
    WorstResultNode.__init__(self, rand, expr == self.condition_value, solver)
  File "/opt/homebrew/lib/python3.12/site-packages/crosshair/statespace.py", line 598, in __init__
    if _PERFORM_EXTRA_SAT_CHECKS and not solver_is_sat(solver, expr):
                                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/lib/python3.12/site-packages/crosshair/statespace.py", line 355, in solver_is_sat
    raise UnknownSatisfiability
crosshair.util.UnknownSatisfiability

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

hypothesis-python/src/hypothesis/provisional.py

Zac-HD · 2024-07-04T21:58:26Z

aside from minor tactical comments above, this looks good to me!

Zac-HD

LGTM!

Should we synchronise our release with hypothesis-crosshair, and update he version that our extra depends on?

tybug · 2024-07-05T04:51:36Z

good point, let's wait to sync 👍. Wouldn't be a great first experience if hypothesis[crosshair] errored.

pschanely · 2024-07-07T00:07:33Z

good point, let's wait to sync 👍. Wouldn't be a great first experience if hypothesis[crosshair] errored.

Yup yup. These are the correct changes, right? Shipped in 0.0.7

tybug · 2024-07-07T03:04:11Z

Let's cherrypick #4032 (+ a hypothesis-crosshair==0.0.7 bump) into this pr and then merge? Or however you want to do it Zac. I've double checked with hypothesis-crosshair and this is ready to merge from my perspective.

Zac-HD · 2024-07-07T04:15:08Z

Let's cherrypick #4032 (+ a hypothesis-crosshair==0.0.7 bump) into this pr and then merge? Or however you want to do it Zac. I've double checked with hypothesis-crosshair and this is ready to merge from my perspective.

That plan sounds perfect to me, one moment... ah, merge conflicts. Simpler to just run make upgrade-requirements locally then, and... more diff, never mind, let's just take the crosshair upgrades and worry about the rest next week.

tybug added 4 commits July 3, 2024 23:56

rename to realize, realize symbolics at entry points

c57d316

no need to realize kwargs after

1ca0c6c

add PrimitiveProvider.avoid_realization

9d87a9c

realize observability args

ae355fc

tybug requested a review from Zac-HD as a code owner July 4, 2024 20:38

add release notes

22e9e52

Zac-HD reviewed Jul 4, 2024

View reviewed changes

hypothesis-python/src/hypothesis/internal/conjecture/data.py Outdated Show resolved Hide resolved

hypothesis-python/src/hypothesis/provisional.py Outdated Show resolved Hide resolved

tybug added 2 commits July 4, 2024 18:26

move realize to data.py, add tests

3d4fc6f

add dependent draw test case

6196973

Zac-HD approved these changes Jul 5, 2024

View reviewed changes

Zac-HD added 2 commits July 6, 2024 21:18

use new crosshair versions

cc40a6f

Merge branch 'master' into backend-realize

6d70cf0

Zac-HD enabled auto-merge July 7, 2024 04:23

Zac-HD merged commit d40ff56 into HypothesisWorks:master Jul 7, 2024
58 checks passed

tybug deleted the backend-realize branch July 7, 2024 06:26

Zac-HD mentioned this pull request Jul 12, 2024

[experimental] Run crosshair in CI #4034

Draft

33 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add and use `realize` and `avoid_realization` backend hooks #4029

Add and use `realize` and `avoid_realization` backend hooks #4029

tybug commented Jul 4, 2024

Zac-HD commented Jul 4, 2024

Zac-HD left a comment

tybug commented Jul 5, 2024

pschanely commented Jul 7, 2024

tybug commented Jul 7, 2024

Zac-HD commented Jul 7, 2024 •

edited

Loading

Add and use realize and avoid_realization backend hooks #4029

Add and use realize and avoid_realization backend hooks #4029

Conversation

tybug commented Jul 4, 2024

Zac-HD commented Jul 4, 2024

Zac-HD left a comment

Choose a reason for hiding this comment

tybug commented Jul 5, 2024

pschanely commented Jul 7, 2024

tybug commented Jul 7, 2024

Zac-HD commented Jul 7, 2024 • edited Loading

Add and use `realize` and `avoid_realization` backend hooks #4029

Add and use `realize` and `avoid_realization` backend hooks #4029

Zac-HD commented Jul 7, 2024 •

edited

Loading