From 1df461d41634d1d1dc330f0aca99921d3fced1fd Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 20 Apr 2019 15:18:18 +0200 Subject: [build] Select uint63 using `ocamlc -config` variables. This seems more robust and avoids having another implementation of `cp`. --- Makefile.build | 2 +- kernel/dune | 11 +-- kernel/uint63_amd64.ml | 227 ---------------------------------------------- kernel/uint63_amd64_63.ml | 227 ++++++++++++++++++++++++++++++++++++++++++++++ kernel/uint63_i386_31.ml | 220 ++++++++++++++++++++++++++++++++++++++++++++ kernel/uint63_x86.ml | 220 -------------------------------------------- kernel/write_uint63.ml | 4 +- 7 files changed, 453 insertions(+), 458 deletions(-) delete mode 100644 kernel/uint63_amd64.ml create mode 100644 kernel/uint63_amd64_63.ml create mode 100644 kernel/uint63_i386_31.ml delete mode 100644 kernel/uint63_x86.ml diff --git a/Makefile.build b/Makefile.build index 034c9ea03c..f0c9e6af01 100644 --- a/Makefile.build +++ b/Makefile.build @@ -365,7 +365,7 @@ $(COQPP): $(COQPPCMO) coqpp/coqpp_main.ml ########################################################################### # Specific rules for Uint63 ########################################################################### -kernel/uint63.ml: kernel/write_uint63.ml kernel/uint63_x86.ml kernel/uint63_amd64.ml +kernel/uint63.ml: kernel/write_uint63.ml kernel/uint63_i386_31.ml kernel/uint63_amd64_63.ml $(SHOW)'WRITE $@' $(HIDE)(cd kernel && ocaml unix.cma $(shell basename $<)) diff --git a/kernel/dune b/kernel/dune index 5b23a705ae..4038bf5638 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,7 +3,7 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ genOpcodeFiles uint63_x86 uint63_amd64 write_uint63)) + (modules (:standard \ genOpcodeFiles uint63_i386_31 uint63_amd64_63 write_uint63)) (libraries lib byterun dynlink)) (executable @@ -14,15 +14,10 @@ (targets copcodes.ml) (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml)))) -(executable - (name write_uint63) - (modules write_uint63) - (libraries unix)) - (rule (targets uint63.ml) - (deps (:gen ./write_uint63.exe) uint63_x86.ml uint63_amd64.ml) - (action (run %{gen}))) + (deps (:gen-file uint63_%{ocaml-config:architecture}_%{ocaml-config:int_size}.ml)) + (action (copy# %{gen-file} %{targets}))) (documentation (package coq)) diff --git a/kernel/uint63_amd64.ml b/kernel/uint63_amd64.ml deleted file mode 100644 index 2d4d685775..0000000000 --- a/kernel/uint63_amd64.ml +++ /dev/null @@ -1,227 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 0 *) -(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *) -let div21 xh xl y = - let maskh = ref 0 in - let maskl = ref 1 in - let dh = ref 0 in - let dl = ref y in - let cmp = ref true in - (* n = ref 0 *) - (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *) - while !dh >= 0 && !cmp do (* dh >= 0 tests that dh highest bit is zero *) - (* We don't use addmuldiv below to avoid checks on 1 *) - dh := (!dh lsl 1) lor (!dl lsr (uint_size - 1)); - dl := !dl lsl 1; - maskh := (!maskh lsl 1) lor (!maskl lsr (uint_size - 1)); - maskl := !maskl lsl 1; - (* incr n *) - cmp := lt128 !dh !dl xh xl; - done; (* mask = 2^n, d = 2^n * y, 2 * d > x *) - let remh = ref xh in - let reml = ref xl in - (* quotienth = ref 0 *) - let quotientl = ref 0 in - (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r, - mask = floor(2^n), d = mask * y, n >= -1 *) - while !maskh lor !maskl <> 0 do - if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *) - (* quotienth := !quotienth lor !maskh *) - quotientl := !quotientl lor !maskl; - remh := if lt !reml !dl then !remh - !dh - 1 else !remh - !dh; - reml := !reml - !dl; - end; - maskl := (!maskl lsr 1) lor (!maskh lsl (uint_size - 1)); - maskh := !maskh lsr 1; - dl := (!dl lsr 1) lor (!dh lsl (uint_size - 1)); - dh := !dh lsr 1; - (* decr n *) - done; - !quotientl, !reml - -let div21 xh xl y = if y = 0 then 0, 0 else div21 xh xl y - - (* exact multiplication *) -(* TODO: check that none of these additions could be a logical or *) - - -(* size = 32 + 31 - (hx << 31 + lx) * (hy << 31 + ly) = - hxhy << 62 + (hxly + lxhy) << 31 + lxly -*) - -(* precondition : (x lsr 62 = 0 || y lsr 62 = 0) *) -let mulc_aux x y = - let lx = x land maxuint31 in - let ly = y land maxuint31 in - let hx = x lsr 31 in - let hy = y lsr 31 in - (* hx and hy are 32 bits value but at most one is 32 *) - let hxy = hx * hy in (* 63 bits *) - let hxly = hx * ly in (* 63 bits *) - let lxhy = lx * hy in (* 63 bits *) - let lxy = lx * ly in (* 62 bits *) - let l = lxy lor (hxy lsl 62) (* 63 bits *) in - let h = hxy lsr 1 in (* 62 bits *) - let hl = hxly + lxhy in (* We can have a carry *) - let h = if lt hl hxly then h + (1 lsl 31) else h in - let hl'= hl lsl 31 in - let l = l + hl' in - let h = if lt l hl' then h + 1 else h in - let h = h + (hl lsr 32) in - (h,l) - -let mulc x y = - if (x lsr 62 = 0 || y lsr 62 = 0) then mulc_aux x y - else - let yl = y lxor (1 lsl 62) in - let (h,l) = mulc_aux x yl in - (* h << 63 + l = x * yl - x * y = x * (1 << 62 + yl) = - x << 62 + x*yl = x << 62 + h << 63 + l *) - let l' = l + (x lsl 62) in - let h = if lt l' l then h + 1 else h in - (h + (x lsr 1), l') - -let equal (x : int) (y : int) = x = y -[@@ocaml.inline always] - -let compare (x:int) (y:int) = - let x = x lxor 0x4000000000000000 in - let y = y lxor 0x4000000000000000 in - if x > y then 1 - else if y > x then -1 - else 0 - - (* head tail *) - -let head0 x = - let r = ref 0 in - let x = ref x in - if !x land 0x7FFFFFFF00000000 = 0 then r := !r + 31 - else x := !x lsr 31; - if !x land 0xFFFF0000 = 0 then (x := !x lsl 16; r := !r + 16); - if !x land 0xFF000000 = 0 then (x := !x lsl 8; r := !r + 8); - if !x land 0xF0000000 = 0 then (x := !x lsl 4; r := !r + 4); - if !x land 0xC0000000 = 0 then (x := !x lsl 2; r := !r + 2); - if !x land 0x80000000 = 0 then (x := !x lsl 1; r := !r + 1); - if !x land 0x80000000 = 0 then ( r := !r + 1); - !r;; - -let tail0 x = - let r = ref 0 in - let x = ref x in - if !x land 0xFFFFFFFF = 0 then (x := !x lsr 32; r := !r + 32); - if !x land 0xFFFF = 0 then (x := !x lsr 16; r := !r + 16); - if !x land 0xFF = 0 then (x := !x lsr 8; r := !r + 8); - if !x land 0xF = 0 then (x := !x lsr 4; r := !r + 4); - if !x land 0x3 = 0 then (x := !x lsr 2; r := !r + 2); - if !x land 0x1 = 0 then ( r := !r + 1); - !r - -let is_uint63 t = - Obj.is_int t -[@@ocaml.inline always] diff --git a/kernel/uint63_amd64_63.ml b/kernel/uint63_amd64_63.ml new file mode 100644 index 0000000000..2d4d685775 --- /dev/null +++ b/kernel/uint63_amd64_63.ml @@ -0,0 +1,227 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* 0 *) +(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *) +let div21 xh xl y = + let maskh = ref 0 in + let maskl = ref 1 in + let dh = ref 0 in + let dl = ref y in + let cmp = ref true in + (* n = ref 0 *) + (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *) + while !dh >= 0 && !cmp do (* dh >= 0 tests that dh highest bit is zero *) + (* We don't use addmuldiv below to avoid checks on 1 *) + dh := (!dh lsl 1) lor (!dl lsr (uint_size - 1)); + dl := !dl lsl 1; + maskh := (!maskh lsl 1) lor (!maskl lsr (uint_size - 1)); + maskl := !maskl lsl 1; + (* incr n *) + cmp := lt128 !dh !dl xh xl; + done; (* mask = 2^n, d = 2^n * y, 2 * d > x *) + let remh = ref xh in + let reml = ref xl in + (* quotienth = ref 0 *) + let quotientl = ref 0 in + (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r, + mask = floor(2^n), d = mask * y, n >= -1 *) + while !maskh lor !maskl <> 0 do + if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *) + (* quotienth := !quotienth lor !maskh *) + quotientl := !quotientl lor !maskl; + remh := if lt !reml !dl then !remh - !dh - 1 else !remh - !dh; + reml := !reml - !dl; + end; + maskl := (!maskl lsr 1) lor (!maskh lsl (uint_size - 1)); + maskh := !maskh lsr 1; + dl := (!dl lsr 1) lor (!dh lsl (uint_size - 1)); + dh := !dh lsr 1; + (* decr n *) + done; + !quotientl, !reml + +let div21 xh xl y = if y = 0 then 0, 0 else div21 xh xl y + + (* exact multiplication *) +(* TODO: check that none of these additions could be a logical or *) + + +(* size = 32 + 31 + (hx << 31 + lx) * (hy << 31 + ly) = + hxhy << 62 + (hxly + lxhy) << 31 + lxly +*) + +(* precondition : (x lsr 62 = 0 || y lsr 62 = 0) *) +let mulc_aux x y = + let lx = x land maxuint31 in + let ly = y land maxuint31 in + let hx = x lsr 31 in + let hy = y lsr 31 in + (* hx and hy are 32 bits value but at most one is 32 *) + let hxy = hx * hy in (* 63 bits *) + let hxly = hx * ly in (* 63 bits *) + let lxhy = lx * hy in (* 63 bits *) + let lxy = lx * ly in (* 62 bits *) + let l = lxy lor (hxy lsl 62) (* 63 bits *) in + let h = hxy lsr 1 in (* 62 bits *) + let hl = hxly + lxhy in (* We can have a carry *) + let h = if lt hl hxly then h + (1 lsl 31) else h in + let hl'= hl lsl 31 in + let l = l + hl' in + let h = if lt l hl' then h + 1 else h in + let h = h + (hl lsr 32) in + (h,l) + +let mulc x y = + if (x lsr 62 = 0 || y lsr 62 = 0) then mulc_aux x y + else + let yl = y lxor (1 lsl 62) in + let (h,l) = mulc_aux x yl in + (* h << 63 + l = x * yl + x * y = x * (1 << 62 + yl) = + x << 62 + x*yl = x << 62 + h << 63 + l *) + let l' = l + (x lsl 62) in + let h = if lt l' l then h + 1 else h in + (h + (x lsr 1), l') + +let equal (x : int) (y : int) = x = y +[@@ocaml.inline always] + +let compare (x:int) (y:int) = + let x = x lxor 0x4000000000000000 in + let y = y lxor 0x4000000000000000 in + if x > y then 1 + else if y > x then -1 + else 0 + + (* head tail *) + +let head0 x = + let r = ref 0 in + let x = ref x in + if !x land 0x7FFFFFFF00000000 = 0 then r := !r + 31 + else x := !x lsr 31; + if !x land 0xFFFF0000 = 0 then (x := !x lsl 16; r := !r + 16); + if !x land 0xFF000000 = 0 then (x := !x lsl 8; r := !r + 8); + if !x land 0xF0000000 = 0 then (x := !x lsl 4; r := !r + 4); + if !x land 0xC0000000 = 0 then (x := !x lsl 2; r := !r + 2); + if !x land 0x80000000 = 0 then (x := !x lsl 1; r := !r + 1); + if !x land 0x80000000 = 0 then ( r := !r + 1); + !r;; + +let tail0 x = + let r = ref 0 in + let x = ref x in + if !x land 0xFFFFFFFF = 0 then (x := !x lsr 32; r := !r + 32); + if !x land 0xFFFF = 0 then (x := !x lsr 16; r := !r + 16); + if !x land 0xFF = 0 then (x := !x lsr 8; r := !r + 8); + if !x land 0xF = 0 then (x := !x lsr 4; r := !r + 4); + if !x land 0x3 = 0 then (x := !x lsr 2; r := !r + 2); + if !x land 0x1 = 0 then ( r := !r + 1); + !r + +let is_uint63 t = + Obj.is_int t +[@@ocaml.inline always] diff --git a/kernel/uint63_i386_31.ml b/kernel/uint63_i386_31.ml new file mode 100644 index 0000000000..fa45c90241 --- /dev/null +++ b/kernel/uint63_i386_31.ml @@ -0,0 +1,220 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* 0 *) +(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *) +let div21 xh xl y = + let maskh = ref zero in + let maskl = ref one in + let dh = ref zero in + let dl = ref y in + let cmp = ref true in + (* n = ref 0 *) + (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *) + while Int64.equal (l_sr !dh (of_int (uint_size - 1))) zero && !cmp do + (* We don't use addmuldiv below to avoid checks on 1 *) + dh := l_or (l_sl !dh one) (l_sr !dl (of_int (uint_size - 1))); + dl := l_sl !dl one; + maskh := l_or (l_sl !maskh one) (l_sr !maskl (of_int (uint_size - 1))); + maskl := l_sl !maskl one; + (* incr n *) + cmp := lt128 !dh !dl xh xl; + done; (* mask = 2^n, d = 2^n * d, 2 * d > x *) + let remh = ref xh in + let reml = ref xl in + (* quotienth = ref 0 *) + let quotientl = ref zero in + (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r, + mask = floor(2^n), d = mask * y, n >= -1 *) + while not (Int64.equal (l_or !maskh !maskl) zero) do + if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *) + (* quotienth := !quotienth lor !maskh *) + quotientl := l_or !quotientl !maskl; + remh := if lt !reml !dl then sub (sub !remh !dh) one else sub !remh !dh; + reml := sub !reml !dl + end; + maskl := l_or (l_sr !maskl one) (l_sl !maskh (of_int (uint_size - 1))); + maskh := l_sr !maskh one; + dl := l_or (l_sr !dl one) (l_sl !dh (of_int (uint_size - 1))); + dh := l_sr !dh one + (* decr n *) + done; + !quotientl, !reml + +let div21 xh xl y = if Int64.equal y zero then zero, zero else div21 xh xl y + + (* exact multiplication *) +let mulc x y = + let lx = ref (Int64.logand x maxuint31) in + let ly = ref (Int64.logand y maxuint31) in + let hx = Int64.shift_right x 31 in + let hy = Int64.shift_right y 31 in + let hr = ref (Int64.mul hx hy) in + let lr = ref (Int64.logor (Int64.mul !lx !ly) (Int64.shift_left !hr 62)) in + hr := (Int64.shift_right_logical !hr 1); + lx := Int64.mul !lx hy; + ly := Int64.mul hx !ly; + hr := Int64.logor !hr (Int64.add (Int64.shift_right !lx 32) (Int64.shift_right !ly 32)); + lr := Int64.add !lr (Int64.shift_left !lx 31); + hr := Int64.add !hr (Int64.shift_right_logical !lr 63); + lr := Int64.add (Int64.shift_left !ly 31) (mask63 !lr); + hr := Int64.add !hr (Int64.shift_right_logical !lr 63); + if Int64.logand !lr Int64.min_int <> 0L + then Int64.(sub !hr one, mask63 !lr) + else (!hr, !lr) + +let equal x y = mask63 x = mask63 y + +let compare x y = Int64.compare x y + +(* Number of leading zeroes *) +let head0 x = + let r = ref 0 in + let x = ref x in + if Int64.logand !x 0x7FFFFFFF00000000L = 0L then r := !r + 31 + else x := Int64.shift_right !x 31; + if Int64.logand !x 0xFFFF0000L = 0L then (x := Int64.shift_left !x 16; r := !r + 16); + if Int64.logand !x 0xFF000000L = 0L then (x := Int64.shift_left !x 8; r := !r + 8); + if Int64.logand !x 0xF0000000L = 0L then (x := Int64.shift_left !x 4; r := !r + 4); + if Int64.logand !x 0xC0000000L = 0L then (x := Int64.shift_left !x 2; r := !r + 2); + if Int64.logand !x 0x80000000L = 0L then (x := Int64.shift_left !x 1; r := !r + 1); + if Int64.logand !x 0x80000000L = 0L then (r := !r + 1); + Int64.of_int !r + +(* Number of trailing zeroes *) +let tail0 x = + let r = ref 0 in + let x = ref x in + if Int64.logand !x 0xFFFFFFFFL = 0L then (x := Int64.shift_right !x 32; r := !r + 32); + if Int64.logand !x 0xFFFFL = 0L then (x := Int64.shift_right !x 16; r := !r + 16); + if Int64.logand !x 0xFFL = 0L then (x := Int64.shift_right !x 8; r := !r + 8); + if Int64.logand !x 0xFL = 0L then (x := Int64.shift_right !x 4; r := !r + 4); + if Int64.logand !x 0x3L = 0L then (x := Int64.shift_right !x 2; r := !r + 2); + if Int64.logand !x 0x1L = 0L then (r := !r + 1); + Int64.of_int !r + +(* May an object be safely cast into an Uint63.t ? *) +let is_uint63 t = + Obj.is_block t && Int.equal (Obj.tag t) Obj.custom_tag + && le (Obj.magic t) maxuint63 + +(* Register all exported functions so that they can be called from C code *) + +let () = + Callback.register "uint63 add" add; + Callback.register "uint63 addcarry" addcarry; + Callback.register "uint63 addmuldiv" addmuldiv; + Callback.register "uint63 div" div; + Callback.register "uint63 div21_ml" div21; + Callback.register "uint63 eq" equal; + Callback.register "uint63 eq0" (equal Int64.zero); + Callback.register "uint63 head0" head0; + Callback.register "uint63 land" l_and; + Callback.register "uint63 leq" le; + Callback.register "uint63 lor" l_or; + Callback.register "uint63 lsl" l_sl; + Callback.register "uint63 lsl1" (fun x -> l_sl x Int64.one); + Callback.register "uint63 lsr" l_sr; + Callback.register "uint63 lsr1" (fun x -> l_sr x Int64.one); + Callback.register "uint63 lt" lt; + Callback.register "uint63 lxor" l_xor; + Callback.register "uint63 mod" rem; + Callback.register "uint63 mul" mul; + Callback.register "uint63 mulc_ml" mulc; + Callback.register "uint63 one" one; + Callback.register "uint63 sub" sub; + Callback.register "uint63 subcarry" subcarry; + Callback.register "uint63 tail0" tail0 diff --git a/kernel/uint63_x86.ml b/kernel/uint63_x86.ml deleted file mode 100644 index fa45c90241..0000000000 --- a/kernel/uint63_x86.ml +++ /dev/null @@ -1,220 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 0 *) -(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *) -let div21 xh xl y = - let maskh = ref zero in - let maskl = ref one in - let dh = ref zero in - let dl = ref y in - let cmp = ref true in - (* n = ref 0 *) - (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *) - while Int64.equal (l_sr !dh (of_int (uint_size - 1))) zero && !cmp do - (* We don't use addmuldiv below to avoid checks on 1 *) - dh := l_or (l_sl !dh one) (l_sr !dl (of_int (uint_size - 1))); - dl := l_sl !dl one; - maskh := l_or (l_sl !maskh one) (l_sr !maskl (of_int (uint_size - 1))); - maskl := l_sl !maskl one; - (* incr n *) - cmp := lt128 !dh !dl xh xl; - done; (* mask = 2^n, d = 2^n * d, 2 * d > x *) - let remh = ref xh in - let reml = ref xl in - (* quotienth = ref 0 *) - let quotientl = ref zero in - (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r, - mask = floor(2^n), d = mask * y, n >= -1 *) - while not (Int64.equal (l_or !maskh !maskl) zero) do - if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *) - (* quotienth := !quotienth lor !maskh *) - quotientl := l_or !quotientl !maskl; - remh := if lt !reml !dl then sub (sub !remh !dh) one else sub !remh !dh; - reml := sub !reml !dl - end; - maskl := l_or (l_sr !maskl one) (l_sl !maskh (of_int (uint_size - 1))); - maskh := l_sr !maskh one; - dl := l_or (l_sr !dl one) (l_sl !dh (of_int (uint_size - 1))); - dh := l_sr !dh one - (* decr n *) - done; - !quotientl, !reml - -let div21 xh xl y = if Int64.equal y zero then zero, zero else div21 xh xl y - - (* exact multiplication *) -let mulc x y = - let lx = ref (Int64.logand x maxuint31) in - let ly = ref (Int64.logand y maxuint31) in - let hx = Int64.shift_right x 31 in - let hy = Int64.shift_right y 31 in - let hr = ref (Int64.mul hx hy) in - let lr = ref (Int64.logor (Int64.mul !lx !ly) (Int64.shift_left !hr 62)) in - hr := (Int64.shift_right_logical !hr 1); - lx := Int64.mul !lx hy; - ly := Int64.mul hx !ly; - hr := Int64.logor !hr (Int64.add (Int64.shift_right !lx 32) (Int64.shift_right !ly 32)); - lr := Int64.add !lr (Int64.shift_left !lx 31); - hr := Int64.add !hr (Int64.shift_right_logical !lr 63); - lr := Int64.add (Int64.shift_left !ly 31) (mask63 !lr); - hr := Int64.add !hr (Int64.shift_right_logical !lr 63); - if Int64.logand !lr Int64.min_int <> 0L - then Int64.(sub !hr one, mask63 !lr) - else (!hr, !lr) - -let equal x y = mask63 x = mask63 y - -let compare x y = Int64.compare x y - -(* Number of leading zeroes *) -let head0 x = - let r = ref 0 in - let x = ref x in - if Int64.logand !x 0x7FFFFFFF00000000L = 0L then r := !r + 31 - else x := Int64.shift_right !x 31; - if Int64.logand !x 0xFFFF0000L = 0L then (x := Int64.shift_left !x 16; r := !r + 16); - if Int64.logand !x 0xFF000000L = 0L then (x := Int64.shift_left !x 8; r := !r + 8); - if Int64.logand !x 0xF0000000L = 0L then (x := Int64.shift_left !x 4; r := !r + 4); - if Int64.logand !x 0xC0000000L = 0L then (x := Int64.shift_left !x 2; r := !r + 2); - if Int64.logand !x 0x80000000L = 0L then (x := Int64.shift_left !x 1; r := !r + 1); - if Int64.logand !x 0x80000000L = 0L then (r := !r + 1); - Int64.of_int !r - -(* Number of trailing zeroes *) -let tail0 x = - let r = ref 0 in - let x = ref x in - if Int64.logand !x 0xFFFFFFFFL = 0L then (x := Int64.shift_right !x 32; r := !r + 32); - if Int64.logand !x 0xFFFFL = 0L then (x := Int64.shift_right !x 16; r := !r + 16); - if Int64.logand !x 0xFFL = 0L then (x := Int64.shift_right !x 8; r := !r + 8); - if Int64.logand !x 0xFL = 0L then (x := Int64.shift_right !x 4; r := !r + 4); - if Int64.logand !x 0x3L = 0L then (x := Int64.shift_right !x 2; r := !r + 2); - if Int64.logand !x 0x1L = 0L then (r := !r + 1); - Int64.of_int !r - -(* May an object be safely cast into an Uint63.t ? *) -let is_uint63 t = - Obj.is_block t && Int.equal (Obj.tag t) Obj.custom_tag - && le (Obj.magic t) maxuint63 - -(* Register all exported functions so that they can be called from C code *) - -let () = - Callback.register "uint63 add" add; - Callback.register "uint63 addcarry" addcarry; - Callback.register "uint63 addmuldiv" addmuldiv; - Callback.register "uint63 div" div; - Callback.register "uint63 div21_ml" div21; - Callback.register "uint63 eq" equal; - Callback.register "uint63 eq0" (equal Int64.zero); - Callback.register "uint63 head0" head0; - Callback.register "uint63 land" l_and; - Callback.register "uint63 leq" le; - Callback.register "uint63 lor" l_or; - Callback.register "uint63 lsl" l_sl; - Callback.register "uint63 lsl1" (fun x -> l_sl x Int64.one); - Callback.register "uint63 lsr" l_sr; - Callback.register "uint63 lsr1" (fun x -> l_sr x Int64.one); - Callback.register "uint63 lt" lt; - Callback.register "uint63 lxor" l_xor; - Callback.register "uint63 mod" rem; - Callback.register "uint63 mul" mul; - Callback.register "uint63 mulc_ml" mulc; - Callback.register "uint63 one" one; - Callback.register "uint63 sub" sub; - Callback.register "uint63 subcarry" subcarry; - Callback.register "uint63 tail0" tail0 diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml index beb59ce205..42bb5dfbb1 100644 --- a/kernel/write_uint63.ml +++ b/kernel/write_uint63.ml @@ -31,8 +31,8 @@ let ml_file_copy input output = let write_uint63 () = ml_file_copy - (if max_int = 1073741823 (* 32-bits *) then "uint63_x86.ml" - else (* 64 bits *) "uint63_amd64.ml") + (if max_int = 1073741823 (* 32-bits *) then "uint63_i386_31.ml" + else (* 64 bits *) "uint63_amd64_63.ml") "uint63.ml" let () = write_uint63 () -- cgit v1.2.3