Opened 14 months ago
Last modified 2 months ago
#8695 infoneeded feature request
Arithmetic overflow from (minBound :: Int) `quot` (-1)
Reported by: | rleslie | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 7.12.1 |
Component: | Core Libraries | Version: | 7.6.3 |
Keywords: | Cc: | erkokl@…, ekmett@…, me@… | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Incorrect result at runtime | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #1042 | Differential Revisions: |
Description
According to the documentation for Data.Int, “All arithmetic is performed modulo 2^n, where n is the number of bits in the type.”
However, this promise is broken by the following exception:
Prelude> (minBound :: Int) `quot` (-1) *** Exception: arithmetic overflow
(This also occurs with Int8, Int16, Int32, and Int64, and likewise for div.)
If all arithmetic is performed modulo 2^n, I would rather expect the above to evaluate to minBound, since after all minBound * (-1) == minBound. The fact that an exception is raised adds an unnecessary burden in pure code to ensure quot (or div) is never called with these specific arguments.
Attachments (2)
Change History (35)
comment:1 Changed 14 months ago by lerkok
- Cc erkokl@… added
comment:2 in reply to: ↑ description ; follow-up: ↓ 3 Changed 13 months ago by hvr
comment:3 in reply to: ↑ 2 Changed 13 months ago by rleslie
Replying to hvr:
Fwiw, you also have to avoid calling quot/div with a 0-divisor, otherwise a div-by-zero exception is raised. I wonder if this isn't rather a deficiency of the Haskell2010 report, failing to mention that the modulo-semantics make an exception for the quot/div operations.
I think a division-by-zero exception is reasonably well-understood, since there is no value q = d `quot` 0 that could be returned in general such that q * 0 == d, even with modulo arithmetic.
Most code performing division with arbitrary operands is well aware of the possibility of a division-by-zero exception, and defensively avoids it. Much less well known or understood, I think, is the possibility of overflow from the singular case of minBound `quot` (-1) which, if not accounted for, can also break one’s application (and possibly be a vector for denial-of-service attacks…)
I think I’d much rather have minBound `quot` (-1) == minBound under modulo arithmetic than a justification for the current exception.
comment:4 follow-up: ↓ 5 Changed 13 months ago by carter
@rleslie
any changes need to have clear meaning!
For example, why would minBound * (-1) == minBound?
Is this an artifact of twos-complement?
comment:5 in reply to: ↑ 4 Changed 13 months ago by rleslie
Replying to carter:
any changes need to have clear meaning!
For example, why would minBound * (-1) == minBound?
Is this an artifact of twos-complement?
I can’t find anything in the Haskell 2010 Language Report that specifically mentions two’s complement representation, however “All arithmetic is performed modulo 2ˆn, where n is the number of bits in the type.” So given a signed integer representation where maxBound == 2^(n - 1) - 1 and minBound == (-maxBound) - 1 as is the case in GHC, under modulo arithmetic it mathematically follows that (-minBound) == minBound, which is the same as minBound * (-1) == minBound.
maxBound == 2^(n - 1) - 1 minBound == (-maxBound) - 1 == (-(2^(n - 1) - 1)) - 1 == (-2^(n - 1)) + 1 - 1 == (-2^(n - 1)) (-minBound) == (-((-maxBound) - 1)) == maxBound + 1 == 2^(n - 1) - 1 + 1 == 2^(n - 1) == 2^(n - 1) - 2^n -- (mod 2^n) == (-2^(n - 1)) == minBound
Note that it is already true that minBound * (-1) == minBound for all of the signed fixed-precision integer types in GHC. The only change I am proposing is to also have minBound `quot` (-1) == minBound instead of raising an exception (and likewise for div).
Such a change is consistent with the modulo arithmetic behavior and also satisfies the class method laws of § 6.4.2 from the Language Report:
(x `quot` y)*y + (x `rem` y) == x (x `div` y)*y + (x `mod` y) == x
comment:6 follow-up: ↓ 7 Changed 13 months ago by hvr
Fwiw as a precedent, the following C99 program when compiled with gcc or clang, and executed on Linux results in a runtime exception as well:
#include <stdio.h> #include <inttypes.h> int main(int argc, char *argv[]) { volatile int32_t a = INT32_MIN; volatile int32_t b = -1; volatile int32_t c = a / b; printf("%" PRId32 "\n", c); return 0; }
Given that quot/div is already a partial function due to div-by-zero, and minBound `quot` -1 being the only special case (beside div-by-zero) for (quot/div) which leads to a result outside the [minBound..maxBound] range, so I'd rather have this exception thrown than to have a program which didn't take into account this non-obvious overflow silently misbehaving due to a flipped sign (as you pointed out yourself if I understood you correctly, but then dismissed it as not being worth an exception).
PS: I believe one may as well argue (as an academic exercise) in a parallel way, that quotRem by 0 could be assigned a value that satisfies the laws from § 6.4.2 as well, thus making it a total function.
comment:7 in reply to: ↑ 6 Changed 13 months ago by rleslie
Replying to hvr:
Fwiw as a precedent, the following C99 program when compiled with gcc or clang, and executed on Linux results in a runtime exception as well:
#include <stdio.h> #include <inttypes.h> int main(int argc, char *argv[]) { volatile int32_t a = INT32_MIN; volatile int32_t b = -1; volatile int32_t c = a / b; printf("%" PRId32 "\n", c); return 0; }
In C, the behavior of signed integer operations that overflow is undefined, so this is not unexpected.
In Haskell, we have Data.Int which declares that signed fixed-precision integer arithmetic operations are performed modulo 2^n, and thus do not overflow. Except minBound `quot` (-1) violates this rule.
Given that quot/div is already a partial function due to div-by-zero, and minBound `quot` -1 being the only special case (beside div-by-zero) for (quot/div) which leads to a result outside the [minBound..maxBound] range, so I'd rather have this exception thrown than to have a program which didn't take into account this non-obvious overflow silently misbehaving due to a flipped sign (as you pointed out yourself if I understood you correctly, but then dismissed it as not being worth an exception).
The same argument could be made for many other arithmetic operations, like minBound * (-1), as well as minBound - 1, maxBound + 1, etc. I don't see any reason to have a special case for minBound `quot` (-1).
It happens that the only reason I discovered this behavior and have reported it as a bug is that it unexpectedly caused a program to abort rather than return the (expected) modulo arithmetic result. So a non-obvious and unexpected exception can equally cause a program to misbehave. This can be especially devastating in a server application.
A program that is sensitive to overflow conditions probably ought not be using fixed-precision integers in the first place; Integer would be a better choice.
But despite what you or I might prefer, the fact remains that modulo arithmetic is the documented behavior for signed fixed-precision integers, so I still tend to view the exception thrown by minBound `quot` (-1) as a bug.
PS: I believe one may as well argue (as an academic exercise) in a parallel way, that quotRem by 0 could be assigned a value that satisfies the laws from § 6.4.2 as well, thus making it a total function.
While that might be an interesting exercise, the laws I quoted only apply “if y is non-zero”. So I argue the laws demand satisfaction when y is (-1).
comment:8 Changed 13 months ago by ekmett
One could argue that it is the status quo making the special case out of y = -1.
But, without prejudging the answer, let's look at what the class is attempting to model.
It has taken me a few times to get this to come out to the correct answer here, so I'm going to be very very pedantic. =)
The current class laws are insufficient to properly model the notion of a Euclidean domain.
To be a proper Euclidean domain
(x `quot` y)*y + (x `rem` y) == x
isn't the only law.
The standard statement of the Euclidean domain axiom is that there exists a Euclidean gauge function f :: r -> Nat such that if a and b are in the domain and b /= 0, then there are q and r such that a = bq + r and either r = 0 or f(r) < f(b).
Both the (div,mod) pair and the (quot, rem) pair (more or less) satisfy these conditions with f = abs, so whenever I say f in the sequel, you can just think abs, but I'm using it to keep my head straight. It'll only matter that I'm making this distinction at the very end.
The assumption that b is non-zero rules out Herbert's case directly, but if you remove the side-condition that b /= 0, it is ruled out by the conditions on r.
e.g. If (q,r) = quotRem x 0 then x = q*0 + r by the simplified definition, but then x = r, so f(x) < f(r) fails to hold and the r == 0 case only saves you when you divide 0 by 0.
These rules kind of rule out the tongue-in-cheek extension of quotRem to cover 0 in one sense.
In another, however, the definition doesn't say what happens when b == 0. For simplicity I'd like to carry on with the convention that either r = 0 or f(r) < f(y) holds regardless and continue to treat b == 0 as an error it makes sense both by convention and by the underlying mathematics.
With that as a warmup, let's get back to (x `quot` -1) in Z mod 2^n.
(minBound `quot` -1)* (-1) + (minBound `rem` y) minBound + (minBound `rem` y) = minBound
says that q = minBound and r = 0 would be the required answers.
The only issue here is that stating f = abs doesn't work as we have the wart forced on us by the asymmetry of 2s complement arithmetic
>>> abs (minBound :: Int) -9223372036854775808
on the other hand, we've been using abs as an approximation of an injection into the natural numbers f, which does not have this limitation!
Basically this requires f = abs . toInteger, then the side condition on f holds.
So all of this indicates to me that the extension to support
minBound `quot` -1 = minBound
is correct and _is_ consistent with the definition of a Euclidean domain independent of 2s complement concerns.
This frankly seems like a slam dunk to me and I'm in favor of the change.
comment:9 Changed 13 months ago by ekmett
- Cc ekmett@… added
comment:10 Changed 13 months ago by hvr
Fyi, while preparing a patch I found #1042 which introduced the exception in the first place.
Changed 13 months ago by hvr
Changed 13 months ago by hvr
comment:11 Changed 13 months ago by hvr
- Milestone set to 7.8.1
- Status changed from new to patch
comment:12 Changed 13 months ago by carter
great! seems like theres a principaled justification and the patch is simple. woot
comment:13 Changed 13 months ago by rleslie
Excellent. Thank you!
comment:14 follow-up: ↓ 21 Changed 13 months ago by rwbarton
Choosing the behavior to match the existing documentation is the wrong way around, in my opinion. If the current behavior is considered desirable, then there is a documentation bug, not a bug in the definition of division.
Unfortunately, there is no choice of behavior that is best in all contexts. For the kinds of programs I most often write, which are computations I run on my own computer, raising an exception is preferable ("safer"). I'm likely to not consider the possibility of dividing MIN_INT by -1, and the exception protects me: If my program runs to completion, then I know the answer is correct (and that such a division never occurred). In the unlikely event that I do get an exception, then I can consider what to do in the event of such a division and ensure that it is treated properly. If the division silently produces MIN_INT then there's some chance that this was the correct thing to do in my context, and some chance that I silently got a nonsense answer, which to me is the worst possible outcome.
On the other hand, for someone who is writing a server to, say, evaluate arithmetic expressions, it is a pain if a malicious user can crash the server by asking it to evaluate MIN_INT / (-1), and there's not really any sense in which answers are "right" or "wrong" anyways. For a program that does division and then does something with the result (like indexing into an array) I tend to worry about the security implications of working with a result that may not be expected by the developer (though something has likely gone wrong already, in the specific event that we are dividing MIN_INT by -1).
Personally I am against this change because it would make ghc less useful for me. Moreover, I tend to feel that servers are complicated bits of software that are prone to crashing for many other reasons already, and it is prudent to ensure that an exception raised while handling one request cannot bring down the whole server anyways.
comment:15 Changed 13 months ago by rwbarton
Edward, to be a Euclidean domain, Int would first of all have to be a domain, which it is not. (I don't think this is nit-picking because there are usually several possible definitions of concepts like "Euclidean domain", which are equivalent under the assumption (here) that the ring is an integral domain. It's potentially more or less an accident which equivalent definition becomes accepted as The Definition, and there's no reason to think it has any distinguished status when the assumption is broken.)
The algebraic law that I expect from division with limited-range numeric types is
if a, b, c :: Int and div a b == c then div (toInteger a) (toInteger b) == toInteger c.
In my opinion this is a lot more useful than a law involving fromInteger :: Integer -> Int, which doesn't play nicely with division.
comment:16 Changed 13 months ago by rleslie
It seems to me there is a desire for a fixed-precision integer type that throws an exception on overflow rather than performing modulo arithmetic -- in which case, I'd be fine with the present behavior, as long as all other overflow conditions were treated similarly.
But modulo arithmetic is also useful and desirable for some purposes, and I object to an integer type that performs modulo arithmetic in some cases, and throws an exception in others.
comment:17 Changed 13 months ago by carter
rleslie, have you considered using Word rather than Int in your use case?
i think this ticket raises a valid issue, and the proposal is a possibly valid one. But perhaps it should be evaluated on a slightly less compressed time scale as apart of a systematic program to incrementally improve the ghc numerical prelude and such?
comment:18 Changed 13 months ago by carter
I agree we should have "wrapping" overflow and "trapping/excepting" overflow variants. In fact, i emphatically agree.
perhaps it would be more effective if we work out a design for such a future rather than whack more on the current quirky kludge?
comment:19 Changed 13 months ago by carter
relevant to this discussion, heres the relevant paragraph in H2010 report section 6.4:
The standard numeric types are listed in Table 6.1. The finite-precision integer type Int covers at least the range [ −2^{29}, 2^{29}−1 ]. As Int is an instance of the Bounded class, maxBound and minBound can be used to determine the exact Int range defined by an implementation. Float is implementation-defined; it is desirable that this type be at least equal in range and precision to the IEEE single-precision type. Similarly, Double should cover IEEE double-precision. The results of exceptional conditions (such as overflow or underflow) on the fixed-precision numeric types are undefined; an implementation may choose error (⊥, semantically), a truncated value, or a special value such as infinity, indefinite, etc.
comment:20 Changed 13 months ago by carter
the referenced table is
Type | Class | Description |
---|---|---|
Integer | Integral | Arbitrary-precision integers |
Int | Integral | Fixed-precision integers |
(Integral a) => Ratio a | RealFrac | Rational numbers |
Float | RealFloat | Real floating-point, single precision |
Double | RealFloat | Real floating-point, double precision |
(RealFloat a) => Complex a | Floating | Complex floating-point |
comment:21 in reply to: ↑ 14 Changed 13 months ago by hvr
Replying to rwbarton:
[...]
Unfortunately, there is no choice of behavior that is best in all contexts. For the kinds of programs I most often write, which are computations I run on my own computer, raising an exception is preferable ("safer").
[...]
IMHO, different types should be used for different contexts. If you want exceptions on any kind of overflow, use something like hackage:safeint, if you don't want overflows at all, use Integer, and if want wrap-around on overflow, use plain Ints.
comment:22 Changed 13 months ago by ekmett
rwbarton: I fully expected to get dinged on the fact that Int can't be a proper domain. I should have included the caveat that it is 'insofar as it can be'.
That said, when a function can be continuously extended sensibly in only one way, I tend to favor extending it.
Re: div (toInteger a) (-1) == toInteger c, here (-1) is a even unit of Z mod 2^n, but we can't even multiply it by all of the ring and pass that law.
The only way to pass your condition without partiality would be to use 1s complement to fix the asymmetry between positive and negative values, but it of course comes with all sorts of other problems and is a complete non-starter.
That said, the operation can pass a slightly different condition, which is that the answers match mod 2^{n. }
In other words
c = div a b = fromInteger (div (toInteger a) (toInteger b))
>>> fromInteger $ toInteger (minBound :: Int) `div` (-1) :: Int -9223372036854775808 >>> fromInteger $ toInteger (minBound :: Int) `quot` (-1) :: Int -9223372036854775808
This extension to div and quot complies with doing this operation in the larger Integer domain and coming back down into the restricted range, just like (*), (-), (+), etc. do. Those operations also don't comply with your desired law.
carter: There are multiple packages that provide overflow protection. e.g. http://hackage.haskell.org/package/safeint
That said, Int explicitly does not.
2s complement introduces particularly hairy corner cases around minBound. -minBound = minBound, abs minBound < (0 :: Int) etc. and it is that same counter-intuitive corner case arising here.
comment:23 Changed 13 months ago by rwbarton
Division is a totally different kind of operation than addition, subtraction and multiplication! The reason that "performing arithmetic mod 2^{n}" is sensible for the latter three is that they respect equality mod 2^{n} (Z/2^{n}Z is a ring). Division does not. You can't take the Euclidean domain approach to defining division mod 2^{n} anyways because there are extra solutions, e.g. for div 100 3 (mod 2^{32}) we have 100 = 3 * 33 + 1, but also 100 = 3 * 1431655798 + 2 and 100 = 3 * 2863311564 + 0. The only sensible notion of division mod 2^{n} is modular division by odd numbers, but that's clearly not the role of div or quot.
So I don't give any weight to arguments-by-analogy such as "addition, subtraction and multiplication can be computed by injecting into Integer, performing the operation and reducing the result to an Int, hence so too should division be".
comment:24 Changed 13 months ago by rwbarton
Basically, I don't agree that minBound :: Int is a sensible value for div minBound (-1) :: Int. Division and modular arithmetic are fundamentally incompatible, so if you are using div or quot on Ints, you are not using Int for modular arithmetic but rather to compute more efficiently with integers that happen to be small. And as integers, -2147483648 divided by -1 is not -2147483648.
comment:25 Changed 13 months ago by lerkok
For whatever it is worth, the SMT community has faced this issue in the past. Their axiomatization impliesquot minBound (-1) = minBound holds for all sized types. See here for the axiomatization: http://smtlib.cs.uiowa.edu/logics/QF_BV.smt2
I think most theorem provers take either the approach of leaving it completely undefined, which they have the luxury of, or completing the operation similarly.
Having said that, the same axiomatization also speculates quot x 0 = 0 for any x; and obviously Haskell is not ready to take that plunge quite yet. (Which I actually find quite acceptable; but that's besides the point.)
One final thought: We strive for Haskell programs to be "semantically" well defined and yearn for tool support for proofs all the time. Losing this bit of connection from the established theorem proving community would be a shame; if nothing else. In particular, any system that hooks up Haskell to such automated tools would have to provision for such discrepancies. I think it would behoove us to follow the theorem proving community here.
comment:26 Changed 13 months ago by carter
@lerkok isn't that tantamount to having the 2s complement ops defined as being the same operationally as the unsigned operations of the same size?
you make an interesting point, At the same time haskell has more in common with coq / agda tradition than the SMT, though this is an informative remark.
@hvr, so heres the thing, one thing i want to dig into in the near future (among several) is improve the native Int / Word / Float / Double optimizations, in both the "correct/no flow" and "who cares about underflow/overflow" variants (the latter corresponding to -ffast-math in gcc / clang / llvm). Its kinda hard to provide decent optimization for those respective cases with the former is done as a userland library. Also, theres the fact that, to keep compatibility for the near term, we'd probably have the default int/ word be the wrap around one, BUT we'd probably want to encourage new users to use a sounder default. Its not about either or, but both. (I may have been a bit anti both the last time this debate)
I really really want to be able to help ghc have better numerical optimization, on both the bit fiddling and floating fronts. To do that, having clear cases when we want to preserve values in an (over/under)flow / NAN etc evading way is key for those who want to work in the "theres a clear unique solution".
Theres actually at least 3 different valid semantics for dealing with over/underflow for words/ints
a) exception / interrupts on over/underflow etc
b) wrapping style semantics
c) saturating (theres a max and min value, you can't go farther than that), this is more common on embedded systems / signal processing algorithms than on desktop/server settings, but its another valid "give a unique solution" approach, and many architectures give instructions for this semantics too.
the point being, the curren situation is a mess, and this whole discussion is symptomatic of a deeper problem that really gets in the way of improving the numerical sitch for ghc / haskell. Either solution is not unique, both are valid in different models, and currently theres not a clear stance on which model int's clearly fall on either side, because we're not providing consistent semantic models.
in summary: theres several different ways we can give unique semantics to many of these operations, and i don't think the current Int situation sits clearly on either side, and perhaps we should seriously consider what the implications of only providing one choice in semantics in ghc is, and either do it whole sale or provide both.
Providing both would actually be in alignment with some of the ideas i have for slightly decoupling Int proper from how array addressing works (because currently int is used implicitly as our model for doing address arithmetic on pointers, which even modern C has moved away from!)
comment:27 Changed 13 months ago by lelf
- Cc me@… added
comment:28 Changed 13 months ago by rleslie
May I ask what the next steps for this are? Is the patch likely to be merged into the 7.8 branch? Or does it still warrant further contemplation and discussion?
comment:29 Changed 13 months ago by carter
- Milestone changed from 7.8.1 to 7.10.1
- Type changed from bug to feature request
@rleslie, I spoke with a few ghc devs. We definitely want to improve this.
1) this won't happen for 7.8. For several main reasons
a) 7.8 is already in RC. So 7.8.1 is only going to get bug fixes relative to the current Release Candidate
b) its actually a pretty reasonable default currently, because as rwbarton argues, theres no "unique" solution concept.
c) it should really only be done as part of a whole sale cleanup of how ghc handles ints and friends internally.
Basically, this ticket is a great motivating example for cleaning up the numbers situation in ghc. And Fixing this up a bit more systematically is definitely something that can make it into 7.10 (time / resources permitting of course). It certainly is one of the 3-4 things highest on my personal priority list! :)
comment:30 Changed 7 months ago by thoughtpolice
- Status changed from patch to infoneeded
(Bumping this ticket out of patch status since there's quite a bit of discussion about it.)
comment:31 Changed 7 months ago by ekmett
It seems worth polling the whole core libraries committee to achieve a judgment on this.
I'll follow up there.
comment:32 Changed 5 months ago by thoughtpolice
- Component changed from libraries/haskell2010 to Core Libraries
Moving over to new owning component 'Core Libraries'.
comment:33 Changed 2 months ago by thoughtpolice
- Milestone changed from 7.10.1 to 7.12.1
Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.
Replying to rleslie:
Fwiw, you also have to avoid calling quot/div with a 0-divisor, otherwise a div-by-zero exception is raised. I wonder if this isn't rather a deficiency of the Haskell2010 report, failing to mention that the modulo-semantics make an exception for the quot/div operations.