From 5aa6d99982a9d6e2736f1eedb7fcdf6b9d05b6a0 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 24 Aug 2020 15:11:16 +0200 Subject: Modify bytecode representation of closures to please OCaml's GC (fix #12636). The second field of a closure can no longer be the value of the first free variable (or another closure of a mutually recursive block) but must be an offset to the first free variable. This commit makes the bytecode compiler and interpreter agnostic to the actual representation of closures. To do so, the execution environment (variable coq_env) no longer points to the currently executed closure but to the last one. This has the following consequences: - OFFSETCLOSURE(n) now always loads the n-th closure of a recursive block (counted from last to first); - ENVACC(n) now always loads the value of the n-th free variable. These two changes make the bytecode compiler simpler, since it no longer has to track the relative position of closures and free variables. The last change makes the interpreter a bit slower, since it has to adjust coq_env when executing GRABREC. Hopefully, cache locality will make the overhead negligible. --- kernel/byterun/coq_fix_code.c | 12 ++-- kernel/byterun/coq_interp.c | 139 ++++++++++++++++++++++-------------------- kernel/byterun/coq_values.c | 16 +++-- 3 files changed, 89 insertions(+), 78 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 814cdfe1d8..9118410549 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -33,12 +33,12 @@ void init_arity () { arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]= arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]= arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]= - arity[PUSHACC6]=arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]= - arity[ENVACC3]=arity[ENVACC4]=arity[PUSHENVACC1]=arity[PUSHENVACC2]= - arity[PUSHENVACC3]=arity[PUSHENVACC4]=arity[APPLY1]=arity[APPLY2]= - arity[APPLY3]=arity[APPLY4]=arity[RESTART]=arity[OFFSETCLOSUREM2]= - arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]= - arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]= + arity[PUSHACC6]=arity[PUSHACC7]= + arity[ENVACC0]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]= + arity[PUSHENVACC0]=arity[PUSHENVACC1]=arity[PUSHENVACC2]=arity[PUSHENVACC3]= + 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[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 15cc451ea8..b44ae34582 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -383,37 +383,49 @@ value coq_interprete } /* Access in heap-allocated environment */ + Instruct(ENVACC0){ + print_instr("ENVACC0"); + accu = Field(coq_env, 2); + Next; + } Instruct(ENVACC1){ print_instr("ENVACC1"); - accu = Field(coq_env, 1); Next; + accu = Field(coq_env, 3); + Next; } Instruct(ENVACC2){ print_instr("ENVACC2"); - accu = Field(coq_env, 2); Next; + accu = Field(coq_env, 4); + Next; } Instruct(ENVACC3){ print_instr("ENVACC3"); - accu = Field(coq_env, 3); Next; + accu = Field(coq_env, 5); + Next; } - Instruct(ENVACC4){ - print_instr("ENVACC4"); - accu = Field(coq_env, 4); Next; + Instruct(PUSHENVACC0){ + print_instr("PUSHENVACC0"); + *--sp = accu; + accu = Field(coq_env, 2); + Next; } Instruct(PUSHENVACC1){ print_instr("PUSHENVACC1"); - *--sp = accu; accu = Field(coq_env, 1); Next; + *--sp = accu; + accu = Field(coq_env, 3); + Next; } Instruct(PUSHENVACC2){ print_instr("PUSHENVACC2"); - *--sp = accu; accu = Field(coq_env, 2); Next; + *--sp = accu; + accu = Field(coq_env, 4); + Next; } Instruct(PUSHENVACC3){ print_instr("PUSHENVACC3"); - *--sp = accu; accu = Field(coq_env, 3); Next; - } - Instruct(PUSHENVACC4){ - print_instr("PUSHENVACC4"); - *--sp = accu; accu = Field(coq_env, 4); Next; + *--sp = accu; + accu = Field(coq_env, 5); + Next; } Instruct(PUSHENVACC){ print_instr("PUSHENVACC"); @@ -423,7 +435,7 @@ value coq_interprete Instruct(ENVACC){ print_instr("ENVACC"); print_int(*pc); - accu = Field(coq_env, *pc++); + accu = Field(coq_env, 2 + *pc++); Next; } /* Function application */ @@ -598,7 +610,6 @@ value coq_interprete sp[0] = arg1; sp[1] = arg2; pc = Code_val(accu); - print_lint(accu); coq_env = accu; coq_extra_args += 1; goto check_stack; @@ -643,13 +654,13 @@ value coq_interprete } Instruct(RESTART) { - int num_args = Wosize_val(coq_env) - 2; + int num_args = Wosize_val(coq_env) - 3; int i; print_instr("RESTART"); CHECK_STACK(num_args); sp -= num_args; - for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2); - coq_env = Field(coq_env, 1); + for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 3); + coq_env = Field(coq_env, 2); coq_extra_args += num_args; Next; } @@ -663,9 +674,10 @@ value coq_interprete } else { mlsize_t num_args, i; num_args = 1 + coq_extra_args; /* arg1 + extra args */ - Alloc_small(accu, num_args + 2, Closure_tag); - Field(accu, 1) = coq_env; - for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i]; + Alloc_small(accu, num_args + 3, Closure_tag); + Field(accu, 1) = Val_int(2); + Field(accu, 2) = coq_env; + for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i]; Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */ sp += num_args; pc = (code_t)(sp[0]); @@ -680,16 +692,18 @@ value coq_interprete int rec_pos = *pc++; /* commence a zero */ print_instr("GRABREC"); if (rec_pos <= coq_extra_args && !Is_accu(sp[rec_pos])) { - pc++;/* On saute le Restart */ + pc++; /* Skip the next RESTART, then point coq_env at the free variables. */ + coq_env = coq_env + (Int_val(Field(coq_env, 1)) - 2) * sizeof(value); } else { if (coq_extra_args < rec_pos) { /* Partial application */ mlsize_t num_args, i; num_args = 1 + coq_extra_args; /* arg1 + extra args */ - Alloc_small(accu, num_args + 2, Closure_tag); - Field(accu, 1) = coq_env; - for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i]; - Code_val(accu) = pc - 3; + Alloc_small(accu, num_args + 3, Closure_tag); + Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */ + Field(accu, 1) = Val_int(2); + Field(accu, 2) = coq_env; + for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i]; sp += num_args; pc = (code_t)(sp[0]); coq_env = sp[1]; @@ -699,10 +713,11 @@ value coq_interprete /* The recursif argument is an accumulator */ mlsize_t num_args, i; /* Construction of fixpoint applied to its [rec_pos-1] first arguments */ - Alloc_small(accu, rec_pos + 2, Closure_tag); - Field(accu, 1) = coq_env; // We store the fixpoint in the first field - for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; // Storing args - Code_val(accu) = pc; + Alloc_small(accu, rec_pos + 3, Closure_tag); + Code_val(accu) = pc; /* Point to the next RESTART instr. */ + Field(accu, 1) = Val_int(2); + Field(accu, 2) = coq_env; // We store the fixpoint in the first field + for (i = 0; i < rec_pos; i++) Field(accu, i + 3) = sp[i]; // Storing args sp += rec_pos; *--sp = accu; /* Construction of the atom */ @@ -732,12 +747,13 @@ value coq_interprete print_instr("CLOSURE"); print_int(nvars); if (nvars > 0) *--sp = accu; - Alloc_small(accu, 1 + nvars, Closure_tag); + Alloc_small(accu, 2 + nvars, Closure_tag); + Field(accu, 1) = Val_int(2); Code_val(accu) = pc + *pc; pc++; for (i = 0; i < nvars; i++) { print_lint(sp[i]); - Field(accu, i + 1) = sp[i]; + Field(accu, i + 2) = sp[i]; } sp += nvars; Next; @@ -758,24 +774,19 @@ value coq_interprete } pc += nfuncs; *--sp=accu; - Alloc_small(accu, nfuncs * 2 + nvars, Closure_tag); - Field(accu, nfuncs * 2 + nvars - 1) = *sp++; - /* On remplie la partie pour les variables libres */ - p = &Field(accu, nfuncs * 2 - 1); - for (i = 0; i < nvars; i++) { - *p++ = *sp++; - } + Alloc_small(accu, nfuncs * 3 + nvars, Closure_tag); + Field(accu, nfuncs * 3 + nvars - 1) = *sp++; p = &Field(accu, 0); - *p = (value) (pc + pc[0]); - p++; + *p++ = (value) (pc + pc[0]); + *p++ = Val_int(nfuncs * 3 - 1); for (i = 1; i < nfuncs; i++) { - *p = Make_header(i * 2, Infix_tag, Caml_white); - p++; /* color irrelevant. */ - *p = (value) (pc + pc[i]); - p++; + *p++ = Make_header(i * 3, Infix_tag, Caml_white); /* color irrelevant. */ + *p++ = (value) (pc + pc[i]); + *p++ = Val_int((nfuncs - i) * 3 - 1); } + for (i = 0; i < nvars; i++) *p++ = *sp++; pc += nfuncs; - accu = accu + 2 * start * sizeof(value); + accu = accu + start * 3 * sizeof(value); Next; } @@ -805,14 +816,15 @@ value coq_interprete /* creation des fonction cofix */ p = sp; - size = nfunc + nvars + 2; + size = nfunc + nvars + 3; for (i=0; i < nfunc; i++) { Alloc_small(accu, size, Closure_tag); Code_val(accu) = pc+pc[i]; - for (j = 0; j < nfunc; j++) Field(accu, j+1) = p[j]; + Field(accu, 1) = Val_int(2); + for (j = 0; j < nfunc; ++j) Field(accu, j + 2) = p[j]; Field(accu, size - 1) = p[nfunc]; - for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = p[j]; + for (j = nfunc + 1; j <= nfunc + nvars; ++j) Field(accu, j + 1) = p[j]; *--sp = accu; /* creation du block contenant le cofix */ @@ -837,15 +849,8 @@ value coq_interprete } /* fallthrough */ Instruct(OFFSETCLOSURE) { print_instr("OFFSETCLOSURE"); - accu = coq_env + *pc++ * sizeof(value); Next; - } - Instruct(PUSHOFFSETCLOSUREM2) { - print_instr("PUSHOFFSETCLOSUREM2"); - *--sp = accu; - } /* fallthrough */ - Instruct(OFFSETCLOSUREM2) { - print_instr("OFFSETCLOSUREM2"); - accu = coq_env - 2 * sizeof(value); Next; + accu = coq_env - *pc++ * 3 * sizeof(value); + Next; } Instruct(PUSHOFFSETCLOSURE0) { print_instr("PUSHOFFSETCLOSURE0"); @@ -853,15 +858,17 @@ value coq_interprete }/* fallthrough */ Instruct(OFFSETCLOSURE0) { print_instr("OFFSETCLOSURE0"); - accu = coq_env; Next; + accu = coq_env; + Next; } - Instruct(PUSHOFFSETCLOSURE2){ - print_instr("PUSHOFFSETCLOSURE2"); + Instruct(PUSHOFFSETCLOSURE1){ + print_instr("PUSHOFFSETCLOSURE1"); *--sp = accu; /* fallthrough */ } - Instruct(OFFSETCLOSURE2) { - print_instr("OFFSETCLOSURE2"); - accu = coq_env + 2 * sizeof(value); Next; + Instruct(OFFSETCLOSURE1) { + print_instr("OFFSETCLOSURE1"); + accu = coq_env - 3 * sizeof(value); + Next; } /* Access to global variables */ @@ -1875,11 +1882,11 @@ value coq_push_val(value v) { value coq_push_arguments(value args) { int nargs,i; value * sp = coq_sp; - nargs = Wosize_val(args) - 2; + nargs = Wosize_val(args) - 3; CHECK_STACK(nargs); coq_sp -= nargs; print_instr("push_args");print_int(nargs); - for(i = 0; i < nargs; i++) coq_sp[i] = Field(args, i+2); + for (i = 0; i < nargs; i++) coq_sp[i] = Field(args, i + 3); return Val_unit; } diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index bbe91da628..adfd4e8954 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -38,9 +38,9 @@ value coq_closure_arity(value clos) { opcode_t * c = Code_val(clos); if (Is_instruction(c,RESTART)) { c++; - if (Is_instruction(c,GRAB)) return Val_int(3 + c[1] - Wosize_val(clos)); + if (Is_instruction(c,GRAB)) return Val_int(4 + c[1] - Wosize_val(clos)); else { - if (Wosize_val(clos) != 2) caml_failwith("Coq Values : coq_closure_arity"); + if (Wosize_val(clos) != 3) caml_failwith("Coq Values : coq_closure_arity"); return Val_int(1); } } @@ -50,13 +50,17 @@ value coq_closure_arity(value clos) { /* Fonction sur les fix */ -value coq_offset(value v) { +value coq_current_fix(value v) { if (Tag_val(v) == Closure_tag) return Val_int(0); - else return Val_long(-Wsize_bsize(Infix_offset_val(v))); + else return Val_long(Wsize_bsize(Infix_offset_val(v)) / 3); } -value coq_offset_closure(value v, value offset){ - return (value)&Field(v, Int_val(offset)); +value coq_shift_fix(value v, value offset) { + return v + Int_val(offset) * 3 * sizeof(value); +} + +value coq_last_fix(value v) { + return v + (Int_val(Field(v, 1)) - 2) * sizeof(value); } value coq_set_bytecode_field(value v, value i, value code) { -- cgit v1.2.3 From 2d63a61a991ab42f2124775b184898d7af6725dd Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 26 Aug 2020 08:34:25 +0200 Subject: Use the same memory layout as closures for accumulators. That way, accumulators again can be used directly as execution environments by the bytecode interpreter. This fixes the issue of the first argument of accumulators being dropped when strongly normalizing. --- kernel/byterun/coq_interp.c | 103 ++++++++++++++++++++++---------------------- kernel/byterun/coq_values.h | 1 - 2 files changed, 52 insertions(+), 52 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index b44ae34582..40ddcbb213 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -712,26 +712,26 @@ value coq_interprete } else { /* The recursif argument is an accumulator */ mlsize_t num_args, i; + value block; /* Construction of fixpoint applied to its [rec_pos-1] first arguments */ Alloc_small(accu, rec_pos + 3, Closure_tag); Code_val(accu) = pc; /* Point to the next RESTART instr. */ Field(accu, 1) = Val_int(2); Field(accu, 2) = coq_env; // We store the fixpoint in the first field - for (i = 0; i < rec_pos; i++) Field(accu, i + 3) = sp[i]; // Storing args - sp += rec_pos; - *--sp = accu; - /* Construction of the atom */ - Alloc_small(accu, 2, ATOM_FIX_TAG); - Field(accu,1) = sp[0]; - Field(accu,0) = sp[1]; - sp++; sp[0] = accu; - /* Construction of the accumulator */ + for (i = 0; i < rec_pos; i++) Field(accu, i + 3) = *sp++; // Storing args + /* Construction of the atom */ + Alloc_small(block, 2, ATOM_FIX_TAG); + Field(block, 0) = *sp++; + Field(block, 1) = accu; + accu = block; + /* Construction of the accumulator */ num_args = coq_extra_args - rec_pos; - Alloc_small(accu, 2+num_args, Accu_tag); - Code_val(accu) = accumulate; - Field(accu,1) = sp[0]; sp++; - for (i = 0; i < num_args;i++)Field(accu, i + 2) = sp[i]; - sp += num_args; + Alloc_small(block, 3 + num_args, Accu_tag); + Code_val(block) = accumulate; + Field(block, 1) = Val_int(2); + Field(block, 2) = accu; + for (i = 0; i < num_args; i++) Field(block, i + 3) = *sp++; + accu = block; pc = (code_t)(sp[0]); coq_env = sp[1]; coq_extra_args = Long_val(sp[2]); @@ -808,9 +808,10 @@ value coq_interprete /* Creation des blocks accumulate */ for(i=0; i < nfunc; i++) { - Alloc_small(accu, 2, Accu_tag); + Alloc_small(accu, 3, Accu_tag); Code_val(accu) = accumulate; - Field(accu,1) = Val_int(1); + Field(accu, 1) = Val_int(2); + Field(accu, 2) = Val_int(1); *--sp=accu; } /* creation des fonction cofix */ @@ -818,22 +819,17 @@ value coq_interprete p = sp; size = nfunc + nvars + 3; for (i=0; i < nfunc; i++) { - + value block; Alloc_small(accu, size, Closure_tag); Code_val(accu) = pc+pc[i]; Field(accu, 1) = Val_int(2); for (j = 0; j < nfunc; ++j) Field(accu, j + 2) = p[j]; Field(accu, size - 1) = p[nfunc]; for (j = nfunc + 1; j <= nfunc + nvars; ++j) Field(accu, j + 1) = p[j]; - *--sp = accu; - /* creation du block contenant le cofix */ - - Alloc_small(accu,1, ATOM_COFIX_TAG); - Field(accu, 0) = sp[0]; - *sp = accu; - /* mise a jour du block accumulate */ - caml_modify(&Field(p[i], 1),*sp); - sp++; + Alloc_small(block, 1, ATOM_COFIX_TAG); + Field(block, 0) = accu; + /* update the accumulate block */ + caml_modify(&Field(p[i], 2), block); } pc += nfunc; accu = p[start]; @@ -1028,7 +1024,7 @@ value coq_interprete print_instr("PROJ"); if (Is_accu (accu)) { *--sp = accu; // Save matched block on stack - accu = Field(accu, 1); // Save atom to accu register + accu = Field(accu, 2); // Save atom to accu register switch (Tag_val(accu)) { case ATOM_COFIX_TAG: // We are forcing a cofix { @@ -1040,11 +1036,11 @@ value coq_interprete coq_env = Field(accu, 0); // Pointer to suspension accu = sp[2]; // Save accumulator to accu register sp[2] = Val_long(coq_extra_args); // Push number of args for return - nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom) + nargs = Wosize_val(accu) - 3; // Number of args = size of accumulator - 2 (accumulator closure) - 1 (atom) // Push arguments to stack CHECK_STACK(nargs + 1); sp -= nargs; - for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 2); + for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 3); *--sp = accu; // Last argument is the pointer to the suspension coq_extra_args = nargs; pc = Code_val(coq_env); // Trigger evaluation @@ -1066,9 +1062,10 @@ value coq_interprete Field(accu, 0) = Field(coq_global_data, *pc++); Field(accu, 1) = *sp++; /* Create accumulator */ - Alloc_small(block, 2, Accu_tag); + Alloc_small(block, 3, Accu_tag); Code_val(block) = accumulate; - Field(block, 1) = accu; + Field(block, 1) = Val_int(2); + Field(block, 2) = accu; accu = block; } } @@ -1142,7 +1139,7 @@ value coq_interprete Instruct(MAKESWITCHBLOCK) { print_instr("MAKESWITCHBLOCK"); *--sp = accu; // Save matched block on stack - accu = Field(accu,1); // Save atom to accu register + accu = Field(accu, 2); // Save atom to accu register switch (Tag_val(accu)) { case ATOM_COFIX_TAG: // We are forcing a cofix { @@ -1156,11 +1153,11 @@ value coq_interprete coq_env = Field(accu,0); // Pointer to suspension accu = sp[2]; // Save accumulator to accu register sp[2] = Val_long(coq_extra_args); // Push number of args for return - nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom) + nargs = Wosize_val(accu) - 3; // Number of args = size of accumulator - 2 (accumulator closure) - 1 (atom) // Push arguments to stack CHECK_STACK(nargs+1); sp -= nargs; - for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); + for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 3); *--sp = accu; // Leftmost argument is the pointer to the suspension print_lint(nargs); coq_extra_args = nargs; @@ -1181,6 +1178,7 @@ value coq_interprete mlsize_t sz; int i, annot; code_t typlbl,swlbl; + value block; print_instr("MAKESWITCHBLOCK"); typlbl = (code_t)pc + *pc; @@ -1207,24 +1205,26 @@ value coq_interprete *--sp = accu; Alloc_small(accu, 1, Abstract_tag); Code_val(accu) = swlbl; - *--sp = accu; /* We create the switch zipper */ - Alloc_small(accu, 5, Default_tag); - Field(accu, 0) = sp[1]; - Field(accu, 1) = sp[0]; - Field(accu, 2) = sp[3]; - Field(accu, 3) = sp[2]; - Field(accu, 4) = coq_env; + Alloc_small(block, 5, Default_tag); + Field(block, 0) = sp[0]; + Field(block, 1) = accu; + Field(block, 2) = sp[2]; + Field(block, 3) = sp[1]; + Field(block, 4) = coq_env; sp += 3; - sp[0] = accu; + accu = block; /* We create the atom */ - Alloc_small(accu, 2, ATOM_SWITCH_TAG); - Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; - sp++;sp[0] = accu; + Alloc_small(block, 2, ATOM_SWITCH_TAG); + Field(block, 0) = *sp++; + Field(block, 1) = accu; + accu = block; /* We create the accumulator */ - Alloc_small(accu, 2, Accu_tag); - Code_val(accu) = accumulate; - Field(accu,1) = *sp++; + Alloc_small(block, 3, Accu_tag); + Code_val(block) = accumulate; + Field(block, 1) = Val_int(2); + Field(block, 2) = accu; + accu = block; } } Next; @@ -1235,10 +1235,11 @@ value coq_interprete Instruct(MAKEACCU) { int i; print_instr("MAKEACCU"); - Alloc_small(accu, coq_extra_args + 3, Accu_tag); + Alloc_small(accu, coq_extra_args + 4, Accu_tag); Code_val(accu) = accumulate; - Field(accu,1) = Field(coq_atom_tbl, *pc); - for(i = 2; i < coq_extra_args + 3; i++) Field(accu, i) = *sp++; + Field(accu, 1) = Val_int(2); + Field(accu, 2) = Field(coq_atom_tbl, *pc); + for (i = 2; i < coq_extra_args + 3; i++) Field(accu, i + 1) = *sp++; pc = (code_t)(sp[0]); coq_env = sp[1]; coq_extra_args = Long_val(sp[2]); diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index a19f9b56c1..bde6e14367 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -30,7 +30,6 @@ /* Les blocs accumulate */ #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) -#define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) #define Is_double(v) (Tag_val(v) == Double_tag) #define Is_tailrec_switch(v) (Field(v,1) == Val_true) -- cgit v1.2.3 From 27695b52413f9fd6bcb60d77e0bdba538c16201f Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 26 Aug 2020 11:40:24 +0200 Subject: Use the closure tag for accumulators. The first field of accumulators points out of the OCaml heap, so using closures instead of tag-0 objects is better for the GC. Accumulators are distinguished from closures because their code pointer necessarily is the "accumulate" address, which points to an ACCUMULATE instruction. --- kernel/byterun/coq_interp.c | 15 +++++++++------ kernel/byterun/coq_memory.c | 2 +- kernel/byterun/coq_values.h | 3 --- 3 files changed, 10 insertions(+), 10 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 40ddcbb213..1b6da7dd6f 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -193,6 +193,8 @@ if (sp - num_args < coq_stack_threshold) { \ #endif #endif +#define Is_accu(v) (Is_block(v) && Tag_val(v) == Closure_tag && Code_val(v) == accumulate) + #define CheckPrimArgs(cond, apply_lbl) do{ \ if (cond) pc++; \ else{ \ @@ -726,7 +728,7 @@ value coq_interprete accu = block; /* Construction of the accumulator */ num_args = coq_extra_args - rec_pos; - Alloc_small(block, 3 + num_args, Accu_tag); + Alloc_small(block, 3 + num_args, Closure_tag); Code_val(block) = accumulate; Field(block, 1) = Val_int(2); Field(block, 2) = accu; @@ -808,7 +810,7 @@ value coq_interprete /* Creation des blocks accumulate */ for(i=0; i < nfunc; i++) { - Alloc_small(accu, 3, Accu_tag); + Alloc_small(accu, 3, Closure_tag); Code_val(accu) = accumulate; Field(accu, 1) = Val_int(2); Field(accu, 2) = Val_int(1); @@ -957,6 +959,7 @@ value coq_interprete print_int(sizes & 0xFFFFFF); if (Is_block(accu)) { long index = Tag_val(accu); + if (index == Closure_tag) index = 0; print_instr("block"); print_lint(index); pc += pc[(sizes & 0xFFFFFF) + index]; @@ -1062,7 +1065,7 @@ value coq_interprete Field(accu, 0) = Field(coq_global_data, *pc++); Field(accu, 1) = *sp++; /* Create accumulator */ - Alloc_small(block, 3, Accu_tag); + Alloc_small(block, 3, Closure_tag); Code_val(block) = accumulate; Field(block, 1) = Val_int(2); Field(block, 2) = accu; @@ -1126,7 +1129,7 @@ value coq_interprete mlsize_t i, size; print_instr("ACCUMULATE"); size = Wosize_val(coq_env); - Alloc_small(accu, size + coq_extra_args + 1, Accu_tag); + Alloc_small(accu, size + coq_extra_args + 1, Closure_tag); for(i = 0; i < size; i++) Field(accu, i) = Field(coq_env, i); for(i = size; i <= coq_extra_args + size; i++) Field(accu, i) = *sp++; @@ -1220,7 +1223,7 @@ value coq_interprete Field(block, 1) = accu; accu = block; /* We create the accumulator */ - Alloc_small(block, 3, Accu_tag); + Alloc_small(block, 3, Closure_tag); Code_val(block) = accumulate; Field(block, 1) = Val_int(2); Field(block, 2) = accu; @@ -1235,7 +1238,7 @@ value coq_interprete Instruct(MAKEACCU) { int i; print_instr("MAKEACCU"); - Alloc_small(accu, coq_extra_args + 4, Accu_tag); + Alloc_small(accu, coq_extra_args + 4, Closure_tag); Code_val(accu) = accumulate; Field(accu, 1) = Val_int(2); Field(accu, 2) = Field(coq_atom_tbl, *pc); diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 6233675c66..ae5251c252 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -108,7 +108,7 @@ value init_coq_vm(value unit) /* ML */ init_coq_interpreter(); /* Some predefined pointer code. - * It is typically contained in accumulator blocks whose tag is 0 and thus + * It is typically contained in accumulator blocks and thus might be * scanned by the GC, so make it look like an OCaml block. */ value accu_block = (value) coq_stat_alloc(2 * sizeof(value)); Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \ diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index bde6e14367..f07018711b 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -17,7 +17,6 @@ #include #define Default_tag 0 -#define Accu_tag 0 #define ATOM_ID_TAG 0 #define ATOM_INDUCTIVE_TAG 1 @@ -28,8 +27,6 @@ #define ATOM_COFIX_TAG 6 #define ATOM_COFIXEVALUATED_TAG 7 -/* Les blocs accumulate */ -#define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) #define Is_double(v) (Tag_val(v) == Double_tag) #define Is_tailrec_switch(v) (Field(v,1) == Val_true) -- cgit v1.2.3