Pure OCaml implementation of Clock.gmtime on xen

[dbuenzli]

The code may not be as efficient as the C @talex5 was refering to. But at least I understand the algorithms behind the proposal modulo the well sourced calendrical formulae (see the comments in the patch).

If I understand correctly the english from the specification gmtime is only defined on non-negative timestamps (or strictly positive, unclear). We still do implement it on negative values by using the proleptic gregorian calendar which is what gmtime seems to be doing on both macosx and linux according to my cross-checks.

Testing. The PR has a function in lib_test/xen_gmtime.ml that was used to test the implementation for differences against the Unix.gmtime of both linux and macosx.

One test is randomized tests with time values that span 200 years around the epoch, this includes negative values. The other is a sequential test that tests every second since a particular point in time (in the patch, 0. the epoch) until you get bored.

Here are the results:

1. MacOS X 10.9.5 64-bits & Ubuntu 14.04 64 bits. Randomized tests for a while don't seem to show any difference. Then each second from -95 BC to 95 AD was tested and no difference was found. Finally each non-negative second from the epoch (0.) was tested until 2430 AD and no difference was found.
2. Ubuntu 12.04.3 32-bits. Randomized tests often have differencies, this is because the range of the randoms exceeds a signed 32-bits which is problematic for linux's 32-bits gmtime. So rather I did a sequential test starting from the minimal signed (-2_147_483_648.) 32 bits timestamp at ~1901 AD and ran the sequence until I witnessed the 2038 bug, i.e. past
   2^31 - 1:

   year: 1901
   [...]
   year: 2037
   year: 2038
   time 2147483648.000000 differs on tm_sec: 8 <> 52
   time 2147483648.000000 differs on tm_min: 14 <> 45
   time 2147483648.000000 differs on tm_hour: 3 <> 20
   time 2147483648.000000 differs on tm_mday: 19 <> 13
   time 2147483648.000000 differs on tm_mon: 0 <> 11
   time 2147483648.000000 differs on tm_year: 138 <> 1
   time 2147483648.000000 differs on tm_wday: 2 <> 5
   time 2147483648.000000 differs on tm_yday: 18 <> 346

No difference was found in between.

I hope this can improve our confidence in the correctness of the function, at least w.r.t. the implementation of other unixes. I'll still be glad if someone can review this thoroughly.

[dbuenzli]

In fact I forgot to kill the testing program so on osx no difference was was found on all the seconds between 1970 AD to 3200 AD.