search

HypothesisWorks / hypothesis

Hypothesis is a powerful, flexible, and easy to use library for property-based testing.
https://hypothesis.works
Other
7.58k stars 587 forks source link

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

Closed tybug closed 4 months ago

tybug commented 4 months ago

@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 (https://github.com/HypothesisWorks/hypothesis/issues/3914#issuecomment-2045735039). 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 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 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 ```
Zac-HD commented 4 months ago

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

tybug commented 4 months ago

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

pschanely commented 4 months ago

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 commented 4 months ago

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 commented 4 months ago

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.