-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Add solve fuzzer and fix the soundness bugs it surfaced #9105
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
base: main
Are you sure you want to change the base?
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -319,9 +319,42 @@ class Bounds : public IRVisitor { | |
| bool could_overflow = true; | ||
| if (to.can_represent(from) || to.is_float()) { | ||
| could_overflow = false; | ||
| } else if (from.is_float() && to.is_int() && to.bits() >= 32) { | ||
| // For int32+ destinations, float-to-signed-int is | ||
| // implementation-defined on out-of-range values. Halide's | ||
| // convention is to assume the value fits, so carry the | ||
| // float bounds through the cast UNLESS at least one | ||
| // endpoint is a constant we can prove exceeds the | ||
| // destination's range. In that case IntImm::make sign- | ||
| // extends the low bits and can invert the resulting | ||
| // interval, which is strictly worse than bounds_of_type. | ||
| // | ||
| // (Float-to-signed-int for bits <= 16 saturates, so it is | ||
| // handled by the narrower `a.is_bounded()` path below; we | ||
| // don't need to treat it specially here.) | ||
| Interval s = simplify(a); | ||
| double lo = -std::ldexp(1.0, to.bits() - 1); | ||
| double hi_exclusive = std::ldexp(1.0, to.bits() - 1); | ||
| bool const_oob = false; | ||
| if (s.has_lower_bound()) { | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This path may break pipelines that rely on Bounds inference "knowing" that |
||
| if (auto fmin = as_const_float(s.min)) { | ||
| const_oob = const_oob || !std::isfinite(*fmin) || *fmin < lo; | ||
| } | ||
| } | ||
| if (s.has_upper_bound()) { | ||
| if (auto fmax = as_const_float(s.max)) { | ||
| const_oob = const_oob || !std::isfinite(*fmax) || *fmax >= hi_exclusive; | ||
| } | ||
| } | ||
| if (!const_oob) { | ||
| could_overflow = false; | ||
| a = s; | ||
| } | ||
| } else if (to.is_int() && to.bits() >= 32) { | ||
| // If we cast to an int32 or greater, assume that it won't | ||
| // overflow. Signed 32-bit integer overflow is undefined. | ||
| // overflow. Signed 32-bit integer overflow is undefined, and | ||
| // Halide treats uint-to-signed-int narrowing as "assumed not | ||
| // to overflow" too (see PR #7814 context). | ||
| could_overflow = false; | ||
| } else if (a.is_bounded()) { | ||
| if (from.can_represent(to)) { | ||
|
|
@@ -742,7 +775,20 @@ class Bounds : public IRVisitor { | |
|
|
||
| Type t = op->type.element_of(); | ||
|
|
||
| // Mod is always positive | ||
| if (t.is_float()) { | ||
| // Halide mod is supposed to be non-negative (Euclidean), but | ||
| // the current float-mod lowering in CodeGen_LLVM is | ||
| // `a - b * floor(a/b)`, which can produce a negative result | ||
| // when b is negative (e.g. fmod(5, -3) = -1 under that | ||
| // formula). Until the lowering is tightened to enforce the | ||
| // Euclidean invariant, fall back to unbounded here -- the | ||
| // integer reasoning below would unsoundly claim the result | ||
| // is >= 0. | ||
| bounds_of_type(t); | ||
| return; | ||
| } | ||
|
|
||
| // Mod is always non-negative for integer types. | ||
| interval.min = make_zero(t); | ||
| interval.max = Interval::pos_inf(); | ||
|
|
||
|
|
@@ -765,11 +811,6 @@ class Bounds : public IRVisitor { | |
| // x % [-8, 10] -> [0,9] | ||
| interval.max = Max::make(interval.min, b.max - make_one(t)); | ||
| interval.max = Max::make(interval.max, make_const(t, -1) - b.min); | ||
| } else if (b.max.type().is_float()) { | ||
| // The floating point version has the same sign rules, | ||
| // but can reach all the way up to the original value, | ||
| // so there's no -1. | ||
| interval.max = Max::make(b.max, -b.min); | ||
| } | ||
| } | ||
| } | ||
|
|
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -110,13 +110,20 @@ Expr Simplify::visit(const Cast *op, ExprInfo *info) { | |
| } else if (cast && | ||
| op->type.is_int_or_uint() && | ||
| cast->type.is_int_or_uint() && | ||
| cast->value.type().is_int_or_uint() && | ||
| op->type.bits() <= cast->type.bits() && | ||
| op->type.bits() <= op->value.type().bits()) { | ||
| // If this is a cast between integer types, where the | ||
| // outer cast is narrower than the inner cast and the | ||
| // inner cast's argument, the inner cast can be | ||
| // eliminated. The inner cast is either a sign extend | ||
| // or a zero extend, and the outer cast truncates the extended bits | ||
| // or a zero extend, and the outer cast truncates the extended bits. | ||
| // The requirement that cast->value is itself int-or-uint is crucial: | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Comments should not spend this much space arguing why a hypothetical alternative version of this would be buggy. After the first sentence it's enough to just say that everything involved needs to be an int. |
||
| // a float source makes `cast` an fp-to-int conversion, whose low | ||
| // bits are not the same as an fp-to-int conversion of a narrower | ||
| // type. For example, int32(uint64(float64(-21))) evaluates to 0 | ||
| // (float-to-uint of a negative value saturates to 0 in Halide), | ||
| // while the stripped form int32(float64(-21)) evaluates to -21. | ||
| if (op->type == cast->value.type()) { | ||
| return mutate(cast->value, info); | ||
| } else { | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Aside: I think we should consider allowing one-line if statements.