pschanely / CrossHair

An analysis tool for Python that blurs the line between testing and type systems.
Other
996 stars 47 forks source link

Crash when integer has (way) too many digits #285

Open Zac-HD opened 1 month ago

Zac-HD commented 1 month ago

This is a horrible regression test for a case where Hypothesis wasn't handling large integers (https://github.com/HypothesisWorks/hypothesis/issues/3874), but I presume you'll want to do something which isn't crashing. And it looks like we have two meaningfully distinct issues in the same traceback! Relevant stdlib docs here; converting really big ints to strings is expensive if the base is not a power of two.

@given(st.integers(min_value=0, max_value=1 << 25_000))  # I'm so sorry about this...
def test_overrun_during_datatree_simulation_3874(n):
    pass
Traceback (most recent call last):
  File ".../hypothesis/internal/conjecture/data.py", line 2450, in draw
    return strategy.do_draw(self)
  File ".../hypothesis/strategies/_internal/lazy.py", line 167, in do_draw
    return data.draw(self.wrapped_strategy)
  File ".../hypothesis/internal/conjecture/data.py", line 2444, in draw
    return strategy.do_draw(self)
  File ".../hypothesis/strategies/_internal/numbers.py", line 85, in do_draw
    return data.draw_integer(
  File ".../hypothesis/internal/conjecture/data.py", line 2113, in draw_integer
    value = self.provider.draw_integer(
  File ".../hypothesis_crosshair_provider/crosshair_provider.py", line 195, in draw_integer
    conditions.append(symbolic <= max_value)
  File ".../crosshair/libimpl/builtinslib.py", line 910, in __le__
    return numeric_binop(ops.le, self, other)
  File ".../crosshair/libimpl/builtinslib.py", line 478, in numeric_binop
    return numeric_binop_internal(op, a, b)
  File ".../crosshair/libimpl/builtinslib.py", line 498, in numeric_binop_internal
    return binfn(op, a, b)
  File ".../crosshair/libimpl/builtinslib.py", line 741, in _
    return SymbolicBool(apply_smt(op, a.var, z3IntVal(b)))
  File ".../crosshair/z3util.py", line 43, in z3IntVal
    return IntNumRef(Z3_mk_numeral(ctx_ref, x.__index__().__str__(), int_sort_ast), ctx)
ValueError: Exceeds the limit (4300) for integer string conversion; use sys.set_int_max_str_digits() to increase the limit

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File ".../hypothesis/internal/conjecture/data.py", line 2457, in draw
    add_note(err, f"while generating {key[9:]!r} from {strategy!r}")
  File ".../crosshair/opcode_intercept.py", line 141, in __repr__
    self.formatted = repr(self.value)
  File ".../crosshair/libimpl/builtinslib.py", line 4521, in _repr
    return invoke_dunder(obj, "__repr__")
  File ".../crosshair/libimpl/builtinslib.py", line 254, in invoke_dunder
    return method(obj, *args, **kwargs)
  File ".../hypothesis/strategies/_internal/lazy.py", line 158, in __repr__
    self.__representation = repr_call(
  File ".../hypothesis/internal/reflection.py", line 496, in repr_call
    bits.append(f"{p.name}={nicerepr(kwargs.pop(p.name))}")
  File ".../hypothesis/internal/reflection.py", line 484, in nicerepr
    return re.sub(r"(\[)~([A-Z][a-z]*\])", r"\g<1>\g<2>", pretty(v))
  File ".../hypothesis/vendor/pretty.py", line 101, in pretty
    printer.pretty(obj)
  File ".../hypothesis/vendor/pretty.py", line 197, in pretty
    return self.type_pprinters[cls](obj, self, cycle)
  File ".../hypothesis/vendor/pretty.py", line 722, in _repr_pprint
    output = repr(obj)
  File ".../crosshair/libimpl/builtinslib.py", line 4521, in _repr
    return invoke_dunder(obj, "__repr__")
  File ".../crosshair/libimpl/builtinslib.py", line 254, in invoke_dunder
    return method(obj, *args, **kwargs)
  File ".../crosshair/core.py", line 333, in with_checked_self
    return native_method(self, *a, **kw)
ValueError: Exceeds the limit (4300) for integer string conversion; use sys.set_int_max_str_digits() to increase the limit

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File ".../hypothesis/internal/conjecture/data.py", line -1, in draw
  File ".../crosshair/opcode_intercept.py", line 262, in post_op
    frame_stack_write(frame, -1, wrapper.formatted)
AttributeError: 'FormatStashingValue' object has no attribute 'formatted'

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File ".../crosshair/opcode_intercept.py", line 262, in post_op
    frame_stack_write(frame, -1, wrapper.formatted)
AttributeError: 'FormatStashingValue' object has no attribute 'formatted'

(via https://github.com/HypothesisWorks/hypothesis/pull/4034)

pschanely commented 1 month ago

Oh wow. OOC, from a product perspective, what does hypothesis do about this? st.integers is by default unbounded, and stringification is common (logging etc). But most users probably don't care to think about this kind of failure case. I assume it takes hypothesis so long to attempt such an integer that it doesn't matter?

Also, does hypothesis do something to avoid hitting this limit internally? Someone might want to make a test to check how this limitation affects their code, but hypothesis still needs to display the counterexample.

Zac-HD commented 1 month ago

Currently we don't do anything particular to handle this case; unbounded integers only go up to 256-bits by default and that regression test would fail if we happened to convert to a string internally.

Having been reminded that this new error exists, I'm planning to upgrade the pretty-printer to display too-large integers in hexadecimal instead. https://github.com/HypothesisWorks/hypothesis/issues/4058