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 +++++---------------------------------- 1 file changed, 5 insertions(+), 34 deletions(-) (limited to 'kernel/byterun/coq_interp.c') 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; } -- 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 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) (limited to 'kernel/byterun/coq_interp.c') 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; } -- cgit v1.2.3