From d009572893913b889320f2fa3435543ee4c63f82 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 27 Dec 2020 10:36:31 +0100 Subject: Remove PUSHACC0, as it is strictly equivalent to PUSH. --- kernel/byterun/coq_fix_code.c | 3 ++- kernel/byterun/coq_interp.c | 4 ---- 2 files changed, 2 insertions(+), 5 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 1ba6a8c8fe..f562c15aa8 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -31,7 +31,8 @@ int arity[STOP+1]; void init_arity () { /* instruction with zero operand */ arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]= - arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]= + arity[ACC6]=arity[ACC7]= + arity[PUSH]=arity[PUSHACC1]= arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]= arity[PUSHACC6]=arity[PUSHACC7]= arity[ENVACC0]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 6255250218..a124a51c7d 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -338,10 +338,6 @@ value coq_interprete print_instr("PUSH"); *--sp = accu; Next; } - Instruct(PUSHACC0) { - print_instr("PUSHACC0"); - *--sp = accu; Next; - } Instruct(PUSHACC1){ print_instr("PUSHACC1"); *--sp = accu; accu = sp[1]; Next; -- cgit v1.2.3 From 944757e10651fda0d63d9291a6bcb1b6fdbaa256 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 27 Dec 2020 10:42:33 +0100 Subject: Remove LSLINT63CONST1 and LSRINT63CONST1 as they are unused. --- kernel/byterun/coq_fix_code.c | 1 - kernel/byterun/coq_interp.c | 28 ---------------------------- kernel/byterun/coq_uint63_emul.h | 4 ---- kernel/byterun/coq_uint63_native.h | 2 -- 4 files changed, 35 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index f562c15aa8..ab6e393178 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -61,7 +61,6 @@ void init_arity () { arity[CHECKDIV21INT63]= arity[CHECKLXORINT63]=arity[CHECKLORINT63]=arity[CHECKLANDINT63]= arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]= - arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]= arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]= arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a124a51c7d..62683b87a6 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1497,34 +1497,6 @@ value coq_interprete Next; } - Instruct(CHECKLSLINT63CONST1) { - print_instr("CHECKLSLINT63CONST1"); - if (Is_uint63(accu)) { - pc++; - Uint63_lsl1(accu); - Next; - } else { - *--sp = uint63_one(); - *--sp = accu; - accu = Field(coq_global_data, *pc++); - goto apply2; - } - } - - Instruct(CHECKLSRINT63CONST1) { - print_instr("CHECKLSRINT63CONST1"); - if (Is_uint63(accu)) { - pc++; - Uint63_lsr1(accu); - Next; - } else { - *--sp = uint63_one(); - *--sp = accu; - accu = Field(coq_global_data, *pc++); - goto apply2; - } - } - Instruct (CHECKADDMULDIVINT63) { print_instr("CHECKADDMULDIVINT63"); CheckInt3(); diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index 13568957c2..dd9b9e55be 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -119,12 +119,8 @@ DECLARE_BINOP(lor) #define Uint63_lor(x, y) CALL_BINOP(lor, x, y) DECLARE_BINOP(lsl) #define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y) -DECLARE_UNOP(lsl1) -#define Uint63_lsl1(x) CALL_UNOP(lsl1, x) DECLARE_BINOP(lsr) #define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y) -DECLARE_UNOP(lsr1) -#define Uint63_lsr1(x) CALL_UNOP(lsr1, x) DECLARE_BINOP(lt) #define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y) DECLARE_BINOP(lxor) diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 27696e8856..731ae8f46e 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -55,8 +55,6 @@ else \ accu = uint63_zero; \ }while(0) -#define Uint63_lsl1(x) (accu = (value)((((uint64_t)(x)-1) << 1) +1)) -#define Uint63_lsr1(x) (accu = (value)(((uint64_t)(x) >> 1) |1)) /* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */ /* (modulo 2^63) for p <= 63 */ -- cgit v1.2.3 From d1215d47c3cda09f4df2f07ce9362b3e6fc5b164 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 27 Dec 2020 11:29:51 +0100 Subject: Remove SETFIELD0 and SETFIELD1. The generated bytecode almost never needs to modify the field of an OCaml object. The only exception is the laziness mechanism of coinductive types. But it modifies field 2, and thus uses the generic opcode SETFIELD anyway. --- kernel/byterun/coq_fix_code.c | 2 +- kernel/byterun/coq_interp.c | 14 -------------- 2 files changed, 1 insertion(+), 15 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index ab6e393178..51ac290ad0 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -40,7 +40,7 @@ void init_arity () { arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[APPLY4]=arity[RESTART]= arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE1]= arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE1]= - arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]= + arity[GETFIELD0]=arity[GETFIELD1]= arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 62683b87a6..a1537cd963 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1011,20 +1011,6 @@ value coq_interprete Next; } - Instruct(SETFIELD0){ - print_instr("SETFIELD0"); - caml_modify(&Field(accu, 0),*sp); - sp++; - Next; - } - - Instruct(SETFIELD1){ - print_instr("SETFIELD1"); - caml_modify(&Field(accu, 1),*sp); - sp++; - Next; - } - Instruct(SETFIELD){ print_instr("SETFIELD"); caml_modify(&Field(accu, *pc),*sp); -- cgit v1.2.3 From 5820a964a5b380d82923be7905cdacd6fa6bd6c3 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 27 Dec 2020 14:55:17 +0100 Subject: Remove MAKEPROD. MAKEPROD is just MAKEBLOCK2(0), but one word shorter. Since this opcode is never encountered in the fast path, this optimization is not worth the extra complexity. --- kernel/byterun/coq_fix_code.c | 2 +- kernel/byterun/coq_interp.c | 10 ---------- 2 files changed, 1 insertion(+), 11 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 51ac290ad0..4bc6848ba7 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -43,7 +43,7 @@ void init_arity () { arity[GETFIELD0]=arity[GETFIELD1]= arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= - arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= + arity[ACCUMULATE]=arity[STOP]= 0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a1537cd963..a9ea6d9f46 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1270,16 +1270,6 @@ value coq_interprete Next; } - Instruct(MAKEPROD) { - print_instr("MAKEPROD"); - *--sp=accu; - Alloc_small(accu,2,0); - Field(accu, 0) = sp[0]; - Field(accu, 1) = sp[1]; - sp += 2; - Next; - } - Instruct(BRANCH) { /* unconditional branching */ print_instr("BRANCH"); -- cgit v1.2.3