Bug 1236615

The bytecode compiler (ocamlc) works.

Created attachment 1044384 [details]
div.c

Attached is what I think would be an equivalent C program.

It gives the same results as the (x86-64) OCaml program when
I use gcc -O3:

$ gcc -O3 -Wall div.c -o div
$ ./div
i = INT64_MIN = -9223372036854775808
j = -1 = -1
rem i j = 0
div i j = -9223372036854775808

Strangely, on x86-64, with gcc -O0 I get this:

$ gcc -Wall div.c -o div
$ ./div
i = INT64_MIN = -9223372036854775808
j = -1 = -1
Floating point exception

On ppc64le, with gcc -O0, I get:

i = INT64_MIN = -9223372036854775808
j = -1 = -1
rem i j = 9223372036854775807
div i j = -1

Carlos O'Donell points on that the code in comment 3 invokes
signed integer overflow (in the division) and so the behaviour
is undefined.

(In reply to Richard W.M. Jones from comment #4)
> Carlos O'Donell points on that the code in comment 3 invokes
> signed integer overflow (in the division) and so the behaviour
> is undefined.

The result of the division is "(-1)(INT64_MIN)" and is unrepresentable as a signed 64-bit two's compliment value. The signed integer overflow results in undefined behaviour both in the C program, and possibly in the Ocaml program (though there you would have to look at the language standard to see what it says). Even if Ocaml allowed it the result is unrepresentable in a type of the same width of storage e.g. 64-bits. The test case would be valid only if you used larger types e.g. 128-bits. The undefined behaviour allows the compiler to do anything it wants with the division and remainder operations, so you see a variety of results. It is my opinion that the highest quality result is that for x86_64 at -O0 which yields SIGFPE as it should since the result is unrepresentable.

The Ocaml test case is IMO likely invalid and should be fixed upstream.

The OCaml test is actually testing the wraparound case, because
int64 is supposed to wrap there.

Int64.min_int ÷ -1 -> Int64.max_int + 1 -> Int64.min_int
                                     wraparound

Extract from -dlambda output:

               (apply (field 1 (global Printf!))
                 [0:
                  [11:
                   "Int64.rem i j = "
                   [7: 0a 0a 0a [11: " (expecting 0)\n" 0a]]]
                  "Int64.rem i j = %Ld (expecting 0)\n"]
                 (Int64.mod i/1008 j/1009))
               (apply (field 1 (global Printf!))
                 [0:
                  [11:
                   "Int64.div i j = "
                   [7: 0a 0a 0a [11: " (expecting min_int)\n" 0a]]]
                  "Int64.div i j = %Ld (expecting min_int)\n"]
                 (Int64.div i/1008 j/1009)))))))

and from -dclambda output:

         (apply
           (apply* camlPrintf__fprintf_1025 
             (field 23 (global camlPervasives!))
             "camlTest__18"=block(0,"camlTest__16"=block(11,"camlTest__12"="Int64.rem i j = ","camlTest__15"=block(7,0a,0a,0a,"camlTest__14"=block(11,"camlTest__13"=" (expecting 0)\n",0a))),"camlTest__17"="Int64.rem i j = %Ld (expecting 0)\n"))
           "camlTest__19"=9223372036854775807L)
         (apply
           (apply* camlPrintf__fprintf_1025 
             (field 23 (global camlPervasives!))
             "camlTest__26"=block(0,"camlTest__24"=block(11,"camlTest__20"="Int64.div i j = ","camlTest__23"=block(7,0a,0a,0a,"camlTest__22"=block(11,"camlTest__21"=" (expecting min_int)\n",0a))),"camlTest__25"="Int64.div i j = %Ld (expecting min_int)\n"))
           "camlTest__7"=-1L)))

This shows that some kind of constant folding is happening
between these two stages.

Answer from upstream is to set:
let division_crashes_on_overflow = true                                         

See: https://groups.google.com/d/msg/ocaml-aggregation-list/WoT1x7q3EVY/6X5bjxgFv9YJ

This is a fix for the problem in Fedora:

https://git.fedorahosted.org/cgit/fedora-ocaml.git/patch/?id=cf026cf66315609afe8f76272e493259bade255f

I will leave this bug open because we need to fix it in RHEL too.

Since the problem described in this bug report should be
resolved in a recent advisory, it has been closed with a
resolution of ERRATA.

For information on the advisory, and where to find the updated
files, follow the link below.

If the solution does not work for you, open a new bug report.

https://rhn.redhat.com/errata/RHBA-2015-2185.html