Arithmetic overflow from (minBound :: Int) `quot` (-1)

changed weight to 5

added Tbug Trac import core libraries incorrect runtime result labels

Replying to rleslie:

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.

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.

Replying to [ticket:8695#comment:78457 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.

@rleslie

any changes need to have clear meaning!

For example, why would minBound * (-1) == minBound? Is this an artifact of twos-complement?

Replying to [ticket:8695#comment:78471 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

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.

Replying to [ticket:8695#comment:78515 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).

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 quoty)*y + (xrem 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.

Trac metadata

Trac field	Value
CC	erkokl@gmail.com → ekmett@gmail.com, erkokl@gmail.com

Fyi, while preparing a patch I found #1042 (closed) which introduced the exception in the first place.

Trac metadata

Trac field	Value
Related	→ #1042 (closed)

Attached file 0001-Change-div-quot-minBound-1-to-evaluate-to-minBound.patch (download).

Attached file 0001-Tweak-numrun013-testcase-for-8695.patch (download).

changed milestone to %7.8.1

great! seems like theres a principaled justification and the patch is simple. woot

Excellent. Thank you!

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.

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.

Trac field	Value
Version	7.6.3
Type	Bug
TypeOfFailure	IncorrectResultAtRuntime
Priority	normal
Resolution	Unresolved
Component	libraries/haskell2010
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

Arithmetic overflow from (minBound :: Int) `quot` (-1)

Child items ...

Activity

Arithmetic overflow from (minBound :: Int) `quot` (-1)

Relates to

Activity