Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fold FixedBoundedFloatStrategy into FloatStrategy #3327

Merged
merged 27 commits into from
May 24, 2022
Merged
Show file tree
Hide file tree
Changes from 11 commits
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
22fd4a7
Fold FixedBoundedFloatStrategy into FloatStrategy
pschanely May 2, 2022
90f8261
Update hypothesis-python/RELEASE.rst
pschanely May 2, 2022
f124a8b
Fix formatting and mypy issues
pschanely May 2, 2022
638f240
Remove bounds checking in FloatStrategy.permitted
pschanely May 2, 2022
ccf9f4b
Push more floats() logic down into FloatStrategy
pschanely May 6, 2022
31f7dee
Apply formatting
pschanely May 8, 2022
16ba49c
Fork on sign consistently
pschanely May 9, 2022
6c66b31
Fix float shrinking
pschanely May 10, 2022
2118d26
Type FloatStrategy bound params as float lint
pschanely May 10, 2022
590bb5d
Use bit-level draws for bounded float ranges
pschanely May 11, 2022
6117079
Add return type for make_float_clamper
pschanely May 11, 2022
dd005a1
Integrate float subnormal handling more deeply
pschanely May 12, 2022
b16953a
Allow zeros and use sign in float example bounds
pschanely May 13, 2022
8be1a42
Update float sampling range in test
pschanely May 13, 2022
ca81fd4
Make various improvements suggested from review
pschanely May 19, 2022
975a392
Remove type annotation for consistency
pschanely May 19, 2022
dfaf14d
Apply code formatting
pschanely May 19, 2022
c6fe05e
Add PBT for make_float_clamper()
pschanely May 20, 2022
348cf3c
Clamp floats by sampling linearly within bounds
pschanely May 23, 2022
9dc7195
Update release notes
pschanely May 23, 2022
3bc6bb8
Tighten float minimization tests
pschanely May 23, 2022
806f6f9
Revert test workaround for small floats
pschanely May 23, 2022
1bb6499
Tighten float list expectation
pschanely May 24, 2022
d3b7386
Correct FloatStrategy repr()
pschanely May 24, 2022
0975f19
Ensure nonzero magnitude is > 0
pschanely May 24, 2022
a1ee9ca
Add float test with asymetric bounds
pschanely May 24, 2022
b28fd27
Merge branch 'float_strategy_refactor' of github.com:pschanely/hypoth…
pschanely May 24, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions AUTHORS.rst
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,7 @@ their individual contributions.
* `Pax (R. Margret) W. <https://github.com/paxcodes>`_
* `Peadar Coyle <https://github.com/springcoil>`_ ([email protected])
* `Petr Viktorin <https://github.com/encukou>`_
* `Phillip Schanely <https://github.com/pschanely>`_ ([email protected])
* `Pierre-Jean Campigotto <https://github.com/PJCampi>`_
* `Przemek Konopko <https://github.com/soutys>`_
* `Richard Boulton <https://www.github.com/rboulton>`_ ([email protected])
Expand Down
4 changes: 4 additions & 0 deletions hypothesis-python/RELEASE.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
RELEASE_TYPE: patch

This patch by Phillip Schanely refactors some of our internals to support future integrations
with symbolic execution tools and fuzzers (:issue:`3086`). There is no user-visible change (yet!).
Zac-HD marked this conversation as resolved.
Show resolved Hide resolved
Original file line number Diff line number Diff line change
Expand Up @@ -225,15 +225,10 @@ def is_simple(f):
def draw_float(data):
try:
data.start_example(DRAW_FLOAT_LABEL)
f = lex_to_float(data.draw_bits(64))
if data.draw_bits(1):
f = -f
return f
return lex_to_float(data.draw_bits(64))
finally:
data.stop_example()


def write_float(data, f):
data.draw_bits(64, forced=float_to_lex(abs(f)))
sign = float_to_int(f) >> 63
data.draw_bits(1, forced=sign)
Original file line number Diff line number Diff line change
Expand Up @@ -1071,7 +1071,7 @@ def minimize_floats(self, chooser):
self.examples,
lambda ex: (
ex.label == DRAW_FLOAT_LABEL
and len(ex.children) == 2
and len(ex.children) == 1
and ex.children[0].length == 8
),
)
Expand Down
29 changes: 29 additions & 0 deletions hypothesis-python/src/hypothesis/internal/floats.py
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@
import math
import struct
from sys import float_info
from typing import Callable, Tuple

# Format codes for (int, float) sized types, used for byte-wise casts.
# See https://docs.python.org/3/library/struct.html#format-characters
Expand Down Expand Up @@ -117,3 +118,31 @@ def next_up_normal(value, width, allow_subnormal):
64: 2 ** -(2 ** (11 - 1) - 2),
}
assert width_smallest_normals[64] == float_info.min


def _exp_and_mantissa(f: float) -> Tuple[int, int]:
i = float_to_int(f)
exponent = (i >> 52) & ((1 << 11) - 1)
mantissa = i & ((1 << 52) - 1)
return (exponent, mantissa)


def make_float_clamper(
minfloat: float = 0.0, maxfloat: float = math.inf
) -> Callable[[float], float]:
"""Return a function that clamps positive floats into the given bounds."""
# NOTE: Set minfloat = float_info.min to exclude subnormals
minexp, minman_at_bottom = _exp_and_mantissa(minfloat)
maxexp, maxman_at_top = _exp_and_mantissa(maxfloat)

def float_clamper(f: float) -> float:
exp, man = _exp_and_mantissa(f)
if not (minexp <= exp <= maxexp):
exp = minexp + (exp - minexp) % (1 + maxexp - minexp)
maxman = ((1 << 52) - 1) if exp < maxexp else maxman_at_top
minman = 0 if exp > minexp else minman_at_bottom
if not (minman <= man <= maxman):
man = minman + (man - minman) % (1 + maxman - minman)
return int_to_float((exp << 52) | man)

return float_clamper
196 changes: 68 additions & 128 deletions hypothesis-python/src/hypothesis/strategies/_internal/numbers.py
Original file line number Diff line number Diff line change
Expand Up @@ -9,23 +9,21 @@
# obtain one at https://mozilla.org/MPL/2.0/.

import math
import operator
from decimal import Decimal
from fractions import Fraction
from sys import float_info
from typing import Any, Optional, Union
from typing import Optional, Union

from hypothesis.control import assume, reject
from hypothesis.control import reject
from hypothesis.errors import InvalidArgument
from hypothesis.internal.conjecture import floats as flt, utils as d
from hypothesis.internal.conjecture.utils import calc_label_from_name
from hypothesis.internal.filtering import get_integer_predicate_bounds
from hypothesis.internal.floats import (
count_between_floats,
float_of,
float_to_int,
int_to_float,
is_negative,
make_float_clamper,
next_down_normal,
next_up,
next_up_normal,
Expand All @@ -36,7 +34,7 @@
check_valid_bound,
check_valid_interval,
)
from hypothesis.strategies._internal.misc import just, nothing
from hypothesis.strategies._internal.misc import nothing
from hypothesis.strategies._internal.strategies import SearchStrategy
from hypothesis.strategies._internal.utils import cacheable, defines_strategy

Expand Down Expand Up @@ -182,97 +180,84 @@ def integers(
)


def _sign_aware_lte(x: float, y: float) -> bool:
"""Less-than-or-equals, but strictly orders -0.0 and 0.0"""
if x == 0.0 == y:
return math.copysign(1.0, x) <= math.copysign(1.0, y)
else:
return x <= y


class FloatStrategy(SearchStrategy):
"""Generic superclass for strategies which produce floats."""
"""A strategy for floating point numbers."""

def __init__(self, allow_infinity, allow_nan, allow_subnormal, width):
def __init__(
self,
min_value: float = -math.inf,
max_value: float = math.inf,
allow_nan: bool = True,
):
super().__init__()
assert isinstance(allow_infinity, bool)
assert isinstance(allow_nan, bool)
assert isinstance(allow_subnormal, bool)
assert width in (16, 32, 64)
self.allow_infinity = allow_infinity
self.min_value = min_value
self.max_value = max_value
self.allow_nan = allow_nan
self.allow_subnormal = allow_subnormal
self.width = width

self.nasty_floats = [
float_of(f, self.width) for f in NASTY_FLOATS if self.permitted(f)
]
self.nasty_floats = [f for f in NASTY_FLOATS if self.permitted(f)]
Zac-HD marked this conversation as resolved.
Show resolved Hide resolved
weights = [0.2 * len(self.nasty_floats)] + [0.8] * len(self.nasty_floats)
self.sampler = d.Sampler(weights)
self.sampler = d.Sampler(weights) if self.nasty_floats else None

self.forced_sign_bit: Optional[int] = None
if _sign_aware_lte(0.0, max_value):
self.pos_clamper = make_float_clamper(max(0.0, min_value), max_value)
if _sign_aware_lte(0.0, min_value):
self.forced_sign_bit = 0
if not _sign_aware_lte(0.0, min_value):
self.neg_clamper = make_float_clamper(-min(-0.0, max_value), -min_value)
if not _sign_aware_lte(0.0, max_value):
self.forced_sign_bit = 1

def __repr__(self):
return "{}(allow_infinity={}, allow_nan={}, width={})".format(
self.__class__.__name__, self.allow_infinity, self.allow_nan, self.width
return "{}(min_value={}, max_value={}, allow_nan={})".format(
self.__class__.__name__,
self.min_value,
self.max_value,
self.allow_nan,
Zac-HD marked this conversation as resolved.
Show resolved Hide resolved
)

def permitted(self, f):
assert isinstance(f, float)
if not self.allow_infinity and math.isinf(f):
return False
if not self.allow_nan and math.isnan(f):
return False
if self.width < 64:
try:
float_of(f, self.width)
except OverflowError:
return False
if not self.allow_subnormal and 0 < abs(f) < width_smallest_normals[self.width]:
return False
return True
if math.isnan(f):
return self.allow_nan
return _sign_aware_lte(self.min_value, f) and _sign_aware_lte(f, self.max_value)

def do_draw(self, data):
while True:
data.start_example(FLOAT_STRATEGY_DO_DRAW_LABEL)
i = self.sampler.sample(data)
i = self.sampler.sample(data) if self.sampler else 0
if i == 0:
result = flt.draw_float(data)
is_negative = data.draw_bits(1, forced=self.forced_sign_bit)
data.start_example(flt.DRAW_FLOAT_LABEL)
result = flt.lex_to_float(data.draw_bits(64))
Zac-HD marked this conversation as resolved.
Show resolved Hide resolved
clamper = self.neg_clamper if is_negative else self.pos_clamper
clamped = clamper(result)
if clamped != result:
data.stop_example(discard=True)
data.start_example(flt.DRAW_FLOAT_LABEL)
flt.write_float(data, clamped)
result = clamped
if is_negative:
result = -result
data.stop_example()
else:
result = self.nasty_floats[i - 1]
flt.write_float(data, result)
if self.permitted(result):
data.stop_example()
if self.width < 64:
return float_of(result, self.width)
return result
data.stop_example(discard=True)

sign = flt.float_to_int(result) >> 63
data.draw_bits(1, forced=sign)
flt.write_float(data, result)

class FixedBoundedFloatStrategy(SearchStrategy):
"""A strategy for floats distributed between two endpoints.

The conditional distribution tries to produce values clustered
closer to one of the ends.
"""

def __init__(self, lower_bound, upper_bound, allow_subnormal, width):
super().__init__()
assert isinstance(lower_bound, float)
assert isinstance(upper_bound, float)
assert 0 <= lower_bound < upper_bound
assert math.copysign(1, lower_bound) == 1, "lower bound may not be -0.0"
assert width in (16, 32, 64)
self.lower_bound = lower_bound
self.upper_bound = upper_bound
self.allow_subnormal = allow_subnormal
self.width = width

def __repr__(self):
return "FixedBoundedFloatStrategy({}, {}, {})".format(
self.lower_bound, self.upper_bound, self.width
)

def do_draw(self, data):
f = self.lower_bound + (
self.upper_bound - self.lower_bound
) * d.fractional_float(data)
if self.width < 64:
f = float_of(f, self.width)
assume(self.lower_bound <= f <= self.upper_bound)
if not self.allow_subnormal:
assume(f == 0 or abs(f) >= width_smallest_normals[self.width])
return f
data.stop_example() # (FLOAT_STRATEGY_DO_DRAW_LABEL)
return result


@cacheable
Expand Down Expand Up @@ -486,60 +471,15 @@ def floats(
f"smallest negative normal {-smallest_normal}"
)

# Any type hint silences mypy when we unpack these parameters
kw: Any = {"allow_subnormal": allow_subnormal, "width": width}
unbounded_floats = FloatStrategy(
allow_infinity=allow_infinity, allow_nan=allow_nan, **kw
)
if min_value is None and max_value is None:
return unbounded_floats
elif min_value is not None and max_value is not None:
if min_value == max_value:
assert isinstance(min_value, float)
result = just(min_value)
elif is_negative(min_value):
if is_negative(max_value):
return floats(min_value=-max_value, max_value=-min_value, **kw).map(
operator.neg
)
else:
return floats(min_value=0.0, max_value=max_value, **kw) | floats(
min_value=0.0, max_value=-min_value, **kw
).map(
operator.neg # type: ignore
)
elif (
count_between_floats(min_value, max_value, width) > 1000
or not allow_subnormal
):
return FixedBoundedFloatStrategy(
lower_bound=min_value, upper_bound=max_value, **kw
)
else:
ub_int = float_to_int(max_value, width)
lb_int = float_to_int(min_value, width)
assert lb_int <= ub_int
result = integers(min_value=lb_int, max_value=ub_int).map(
lambda x: int_to_float(x, width)
)
elif min_value is not None:
assert isinstance(min_value, float)
if is_negative(min_value):
# Ignore known bug https://github.com/python/mypy/issues/6697
return unbounded_floats.map(abs) | floats( # type: ignore
min_value=min_value, max_value=-0.0, **kw
)
else:
result = unbounded_floats.map(lambda x: min_value + abs(x))
else:
assert isinstance(max_value, float)
if not is_negative(max_value):
return floats(
min_value=0.0, max_value=max_value, **kw
) | unbounded_floats.map(lambda x: -abs(x))
else:
result = unbounded_floats.map(lambda x: max_value - abs(x))
min_value = min_value if min_value is not None else float("-inf")
max_value = max_value if max_value is not None else float("inf")
Zac-HD marked this conversation as resolved.
Show resolved Hide resolved
assert isinstance(min_value, float)
assert isinstance(max_value, float)
result: SearchStrategy = FloatStrategy(min_value, max_value, allow_nan=allow_nan)

if not allow_subnormal:
smallest = width_smallest_normals[width]
result = result.filter(lambda x: abs(x) >= smallest)
Zac-HD marked this conversation as resolved.
Show resolved Hide resolved
if width < 64:

def downcast(x):
Expand Down
2 changes: 1 addition & 1 deletion hypothesis-python/tests/conjecture/test_float_encoding.py
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ def test_double_reverse(i):

@example(1.25)
@example(1.0)
@given(st.floats())
@given(st.floats(min_value=0.0))
def test_draw_write_round_trip(f):
Zac-HD marked this conversation as resolved.
Show resolved Hide resolved
d = ConjectureData.for_buffer(bytes(10))
flt.write_float(d, f)
Expand Down
2 changes: 1 addition & 1 deletion hypothesis-python/tests/conjecture/test_shrinker.py
Original file line number Diff line number Diff line change
Expand Up @@ -313,7 +313,7 @@ def test_float_shrink_can_run_when_canonicalisation_does_not_work(monkeypatch):
# This should be an error when called
monkeypatch.setattr(Float, "shrink", None)

base_buf = int_to_bytes(flt.base_float_to_lex(1000.0), 8) + bytes(1)
base_buf = int_to_bytes(flt.base_float_to_lex(1000.0), 8)

@shrinking_from(base_buf)
def shrinker(data):
Expand Down
Loading