From d2bbd834841ba3c8b2b482a02489bd4fac19f0fb Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 4 Apr 2019 11:07:14 +0200 Subject: [vm] x86_64 registers Backport https://github.com/ocaml/ocaml/commit/bc333918980b97a2c81031ec33e72a417f854376 from OCaml VM --- kernel/byterun/coq_interp.c | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 2293ae9dfd..e838519fe4 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -159,6 +159,11 @@ if (sp - num_args < coq_stack_threshold) { \ #define ACCU_REG asm("38") #define JUMPTBL_BASE_REG asm("39") #endif +#ifdef __x86_64__ +#define PC_REG asm("%r15") +#define SP_REG asm("%r14") +#define ACCU_REG asm("%r13") +#endif #endif #define CheckInt1() do{ \ -- cgit v1.2.3 From d1905fbcde5905de640657a820e531929e23dd8a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 5 Apr 2019 12:35:10 +0200 Subject: [vm] Arm 64 registers Backport https://github.com/ocaml/ocaml/commit/055d5c0379e42b4f561cb1fc5159659d8e9a7b6f from OCaml VM --- kernel/byterun/coq_interp.c | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index e838519fe4..1925ef5932 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -164,6 +164,12 @@ if (sp - num_args < coq_stack_threshold) { \ #define SP_REG asm("%r14") #define ACCU_REG asm("%r13") #endif +#ifdef __aarch64__ +#define PC_REG asm("%x19") +#define SP_REG asm("%x20") +#define ACCU_REG asm("%x21") +#define JUMPTBL_BASE_REG asm("%x22") +#endif #endif #define CheckInt1() do{ \ -- cgit v1.2.3 From 46896e9442e74cb78ad7396054cee76564f78ec3 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 5 Apr 2019 12:37:03 +0200 Subject: [vm] ARM registers Backport https://github.com/ocaml/ocaml/commit/eb1922c6ab88e832e39ba3972fab619081061928 from OCaml VM --- kernel/byterun/coq_interp.c | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 1925ef5932..9742768c5d 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -148,8 +148,9 @@ if (sp - num_args < coq_stack_threshold) { \ #define SP_REG asm("a4") #define ACCU_REG asm("d7") #endif -#if defined(__arm__) && !defined(__thumb2__) -#define PC_REG asm("r9") +/* OCaml PR#4953: these specific registers not available in Thumb mode */ +#if defined(__arm__) && !defined(__thumb__) +#define PC_REG asm("r6") #define SP_REG asm("r8") #define ACCU_REG asm("r7") #endif -- cgit v1.2.3 From df6328178a92d7a51e2a08acbec5013d080e73aa Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 5 Apr 2019 12:44:08 +0200 Subject: [vm] PPC64 registers Backport https://github.com/ocaml/ocaml/commit/c6ce97fe26e149d43ee2cf71ca821a4592ce1785 from OCaml VM --- kernel/byterun/coq_interp.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 9742768c5d..a8fd2fbe47 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -133,7 +133,7 @@ if (sp - num_args < coq_stack_threshold) { \ #define SP_REG asm("%edi") #define ACCU_REG #endif -#if defined(PPC) || defined(_POWER) || defined(_IBMR2) +#if defined(__ppc__) || defined(__ppc64__) #define PC_REG asm("26") #define SP_REG asm("27") #define ACCU_REG asm("28") -- cgit v1.2.3 From e9fec7c112a7792d67949ef5abe3de8a8832beda Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 5 Apr 2019 12:49:53 +0200 Subject: [vm] Backport from OCaml Backport https://github.com/ocaml/ocaml/commit/71b94fa3e8d73c40e298409fa5fd6501383d38a6 and https://github.com/ocaml/ocaml/commit/d3e86fdfcc8f40a99380303f16f9b782233e047e from OCaml VM --- kernel/byterun/coq_interp.c | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a8fd2fbe47..da152599ce 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -104,7 +104,8 @@ if (sp - num_args < coq_stack_threshold) { \ several architectures. */ -#if defined(__GNUC__) && !defined(DEBUG) +#if defined(__GNUC__) && !defined(DEBUG) && !defined(__INTEL_COMPILER) \ + && !defined(__llvm__) #ifdef __mips__ #define PC_REG asm("$16") #define SP_REG asm("$17") -- cgit v1.2.3 From dd60b4a292b870e08c23ddcb363630cbb2ed1227 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 2 May 2019 08:16:37 +0200 Subject: [primitive integers] Make div21 implems consistent with its specification There are three implementations of this primitive: * one in OCaml on 63 bits integer in kernel/uint63_amd64.ml * one in OCaml on Int64 in kernel/uint63_x86.ml * one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h Its specification is the axiom `diveucl_21_spec` in theories/Numbers/Cyclic/Int63/Int63.v * comment the implementations with loop invariants to enable an easy pen&paper proof of correctness (note to reviewers: the one in uint63_amd64.ml might be the easiest to read) * make sure the three implementations are equivalent * fix the specification in Int63.v (only the lowest part of the result is actually returned) * make a little optimisation in div21 enabled by the proof of correctness (cmp is computed at the end of the first loop rather than at the beginning, potentially saving one loop iteration while remaining correct) * update the proofs in Int63.v and Cyclic63.v to take into account the new specifiation of div21 * add a test --- kernel/byterun/coq_interp.c | 39 ++++------------------------ kernel/byterun/coq_uint63_native.h | 53 ++++++++++++++++++++++++++------------ 2 files changed, 41 insertions(+), 51 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 2293ae9dfd..e38d458b36 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1374,40 +1374,11 @@ value coq_interprete Instruct (CHECKDIV21INT63) { print_instr("DIV21INT63"); CheckInt3(); - /* spiwack: takes three int31 (the two first ones represent an - int62) and performs the euclidian division of the - int62 by the int31 */ - /* TODO: implement this - bigint = UI64_of_value(accu); - bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++)); - uint64 divisor; - divisor = UI64_of_value(*sp++); - Alloc_small(accu, 2, 1); */ /* ( _ , arity, tag ) */ - /* if (I64_is_zero (divisor)) { - Field(accu, 0) = 1; */ /* 2*0+1 */ - /* Field(accu, 1) = 1; */ /* 2*0+1 */ - /* } - else { - uint64 quo, mod; - I64_udivmod(bigint, divisor, &quo, &mod); - Field(accu, 0) = value_of_uint32(I64_to_int32(quo)); - Field(accu, 1) = value_of_uint32(I64_to_int32(mod)); - } */ - int b; - Uint63_eq0(b, sp[1]); - if (b) { - AllocPair(); - Field(accu, 0) = sp[1]; - Field(accu, 1) = sp[1]; - } - else { - Uint63_div21(accu, sp[0], sp[1], sp); - sp[1] = sp[0]; - Swap_accu_sp; - AllocPair(); - Field(accu, 0) = sp[1]; - Field(accu, 1) = sp[0]; - } + Uint63_div21(accu, sp[0], sp[1], &(sp[1])); + Swap_accu_sp; + AllocPair(); + Field(accu, 0) = sp[1]; + Field(accu, 1) = sp[0]; sp += 2; Next; } diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index d431dc1e5c..8dee0d69d3 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -109,37 +109,56 @@ value uint63_mulc(value x, value y, value* h) { #define lt128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_lt(xl,yl))) #define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl))) -value uint63_div21(value xh, value xl, value y, value* q) { - xh = (uint64_t)xh >> 1; - xl = ((uint64_t)xl >> 1) | ((uint64_t)xh << 63); - xh = (uint64_t)xh >> 1; +#define maxuint63 ((uint64_t)0x7FFFFFFFFFFFFFFF) +/* precondition: y <> 0 */ +/* outputs r and sets ql to q % 2^63 s.t. x = q * y + r, r < y */ +static value uint63_div21_aux(value xh, value xl, value y, value* ql) { + xh = uint63_of_value(xh); + xl = uint63_of_value(xl); + y = uint63_of_value(y); uint64_t maskh = 0; uint64_t maskl = 1; uint64_t dh = 0; - uint64_t dl = (uint64_t)y >> 1; + uint64_t dl = y; int cmp = 1; - while (dh >= 0 && cmp) { + /* int n = 0 */ + /* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0, d < 2^(2*63) */ + while (!(dh >> (63 - 1)) && cmp) { + dh = (dh << 1) | (dl >> (63 - 1)); + dl = (dl << 1) & maxuint63; + maskh = (maskh << 1) | (maskl >> (63 - 1)); + maskl = (maskl << 1) & maxuint63; + /* ++n */ cmp = lt128(dh,dl,xh,xl); - dh = (dh << 1) | (dl >> 63); - dl = dl << 1; - maskh = (maskh << 1) | (maskl >> 63); - maskl = maskl << 1; } uint64_t remh = xh; uint64_t reml = xl; - uint64_t quotient = 0; + /* uint64_t quotienth = 0; */ + uint64_t quotientl = 0; + /* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r, + mask = floor(2^n), d = mask * y, n >= -1 */ while (maskh | maskl) { - if (le128(dh,dl,remh,reml)) { - quotient = quotient | maskl; - if (uint63_lt(reml,dl)) {remh = remh - dh - 1;} else {remh = remh - dh;} + if (le128(dh,dl,remh,reml)) { /* if rem >= d, add one bit and subtract d */ + /* quotienth = quotienth | maskh */ + quotientl = quotientl | maskl; + remh = (uint63_lt(reml,dl)) ? (remh - dh - 1) : (remh - dh); reml = reml - dl; } - maskl = (maskl >> 1) | (maskh << 63); + maskl = (maskl >> 1) | ((maskh << (63 - 1)) & maxuint63); maskh = maskh >> 1; - dl = (dl >> 1) | (dh << 63); + dl = (dl >> 1) | ((dh << (63 - 1)) & maxuint63); dh = dh >> 1; + /* decr n */ } - *q = Val_int(quotient); + *ql = Val_int(quotientl); return Val_int(reml); } +value uint63_div21(value xh, value xl, value y, value* ql) { + if (uint63_of_value(y) == 0) { + *ql = Val_int(0); + return Val_int(0); + } else { + return uint63_div21_aux(xh, xl, y, ql); + } +} #define Uint63_div21(xh, xl, y, q) (accu = uint63_div21(xh, xl, y, q)) -- cgit v1.2.3 From 09cdf7b1fad8761cdf7048bf38a468c8558eb0d5 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 2 May 2019 08:41:45 +0200 Subject: Remove now useless commented code --- kernel/byterun/coq_interp.c | 15 +-------------- kernel/byterun/coq_uint63_emul.h | 2 ++ kernel/byterun/coq_uint63_native.h | 1 + 3 files changed, 4 insertions(+), 14 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index e38d458b36..1b348ae777 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -29,13 +29,6 @@ #include "coq_uint63_emul.h" #endif -/* spiwack: I append here a few macros for value/number manipulation */ -#define uint32_of_value(val) (((uint32_t)(val)) >> 1) -#define value_of_uint32(i) ((value)((((uint32_t)(i)) << 1) | 1)) -#define UI64_of_uint32(lo) ((uint64_t)((uint32_t)(lo))) -#define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val))) -/* /spiwack */ - /* Registers for the abstract machine: @@ -1298,12 +1291,6 @@ value coq_interprete /*returns the multiplication on a pair */ print_instr("MULCINT63"); CheckInt2(); - /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */ - /* TODO: implement - p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1)); - AllocPair(); */ - /* Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; */ /*higher part*/ - /* Field(accu, 1) = (value)(I64_to_int32(p)|1); */ /*lower part*/ Uint63_mulc(accu, *sp, sp); *--sp = accu; AllocPair(); @@ -1587,7 +1574,7 @@ value coq_push_vstack(value stk, value max_stack_size) { print_instr("push_vstack");print_int(len); for(i = 0; i < len; i++) coq_sp[i] = Field(stk,i); sp = coq_sp; - CHECK_STACK(uint32_of_value(max_stack_size)); + CHECK_STACK(uint_of_value(max_stack_size)); return Val_unit; } diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index d982f67566..528cc6fc1f 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -6,6 +6,8 @@ #define Is_uint63(v) (Tag_val(v) == Custom_tag) +#define uint_of_value(val) (((uint32_t)(val)) >> 1) + # define DECLARE_NULLOP(name) \ value uint63_##name() { \ static value* cb = 0; \ diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 8dee0d69d3..1fdafc9d8f 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -1,5 +1,6 @@ #define Is_uint63(v) (Is_long(v)) +#define uint_of_value(val) (((uint64_t)(val)) >> 1) #define uint63_of_value(val) ((uint64_t)(val) >> 1) /* 2^63 * y + x as a value */ -- cgit v1.2.3