From c1ec8e31bb760f4b250e23be442fff96e4b365d5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 12 Dec 2019 15:40:38 +0100 Subject: [vm] Untabify the VM C code. This is a follow up of #11010 ; I've realized that for example in #11123 a large part of the patch is detabification as indeed the files are mixed in tabs/space style so developers are forced to do the cleanup each time they work on them. Command used: ``` for i in `find . -name '*.c' -or -name '*.h'; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ``` Checked empty diff with `git diff --ignore-all-space` --- kernel/byterun/coq_fix_code.c | 14 +- kernel/byterun/coq_gc.h | 6 +- kernel/byterun/coq_interp.c | 1316 ++++++++++++++++++++--------------------- kernel/byterun/coq_memory.c | 12 +- kernel/byterun/coq_memory.h | 4 +- kernel/byterun/coq_values.c | 2 +- 6 files changed, 677 insertions(+), 677 deletions(-) diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 931b509f48..306643f758 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -12,7 +12,7 @@ for fast computation of bounded (31bits) integers */ #include -#include +#include #include #include #include @@ -42,7 +42,7 @@ void init_arity () { arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]= 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]=arity[MAKEPROD]= arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]= arity[LTFLOAT]=arity[LEFLOAT]= arity[ISINT]=arity[AREINT2]=0; @@ -76,7 +76,7 @@ void init_arity () { /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[PROJ]=2; - /* instruction with four operands */ + /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; /* instruction with arbitrary operands */ arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0; @@ -134,7 +134,7 @@ value coq_is_accumulate_code(value code){ #ifdef ARCH_BIG_ENDIAN #define Reverse_32(dst,src) { \ - char * _p, * _q; \ + char * _p, * _q; \ char _a, _b; \ _p = (char *) (src); \ _q = (char *) (dst); \ @@ -159,9 +159,9 @@ value coq_tcode_of_code (value code) { q = coq_stat_alloc(len); Code_val(res) = q; len /= sizeof(opcode_t); - for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) { + for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) { opcode_t instr; - COPY32(&instr,p); + COPY32(&instr,p); p++; if (instr < 0 || instr > STOP){ instr = STOP; @@ -183,7 +183,7 @@ value coq_tcode_of_code (value code) { for(i=1; i= 0; i--) newsp[i] = sp[i]; - sp = newsp; - pc = Code_val(accu); - coq_env = accu; - coq_extra_args += nargs - 1; - goto check_stack; + int nargs = *pc++; + int slotsize = *pc; + value * newsp; + int i; + print_instr("APPTERM"); + /* Slide the nargs bottom words of the current frame to the top + of the frame, and discard the remainder of the frame */ + newsp = sp + slotsize - nargs; + for (i = nargs - 1; i >= 0; i--) newsp[i] = sp[i]; + sp = newsp; + pc = Code_val(accu); + coq_env = accu; + coq_extra_args += nargs - 1; + goto check_stack; } Instruct(APPTERM1) { - value arg1 = sp[0]; - print_instr("APPTERM1"); - sp = sp + *pc - 1; - sp[0] = arg1; - pc = Code_val(accu); - coq_env = accu; - goto check_stack; + value arg1 = sp[0]; + print_instr("APPTERM1"); + sp = sp + *pc - 1; + sp[0] = arg1; + pc = Code_val(accu); + coq_env = accu; + goto check_stack; } Instruct(APPTERM2) { - value arg1 = sp[0]; - value arg2 = sp[1]; - print_instr("APPTERM2"); - sp = sp + *pc - 2; - sp[0] = arg1; - sp[1] = arg2; - pc = Code_val(accu); - print_lint(accu); - coq_env = accu; - coq_extra_args += 1; - goto check_stack; + value arg1 = sp[0]; + value arg2 = sp[1]; + print_instr("APPTERM2"); + sp = sp + *pc - 2; + sp[0] = arg1; + sp[1] = arg2; + pc = Code_val(accu); + print_lint(accu); + coq_env = accu; + coq_extra_args += 1; + goto check_stack; } Instruct(APPTERM3) { - value arg1 = sp[0]; - value arg2 = sp[1]; - value arg3 = sp[2]; - print_instr("APPTERM3"); - sp = sp + *pc - 3; - sp[0] = arg1; - sp[1] = arg2; - sp[2] = arg3; - pc = Code_val(accu); - coq_env = accu; - coq_extra_args += 2; - goto check_stack; - } - + value arg1 = sp[0]; + value arg2 = sp[1]; + value arg3 = sp[2]; + print_instr("APPTERM3"); + sp = sp + *pc - 3; + sp[0] = arg1; + sp[1] = arg2; + sp[2] = arg3; + pc = Code_val(accu); + coq_env = accu; + coq_extra_args += 2; + goto check_stack; + } + Instruct(RETURN) { - print_instr("RETURN"); - print_int(*pc); - sp += *pc++; - print_instr("stack="); - print_lint(sp[0]); - print_lint(sp[1]); - print_lint(sp[2]); - if (coq_extra_args > 0) { - print_instr("extra args > 0"); - print_lint(coq_extra_args); - coq_extra_args--; - pc = Code_val(accu); - coq_env = accu; - } else { - print_instr("extra args = 0"); - pc = (code_t)(sp[0]); - coq_env = sp[1]; - coq_extra_args = Long_val(sp[2]); - sp += 3; - } - Next; - } - + print_instr("RETURN"); + print_int(*pc); + sp += *pc++; + print_instr("stack="); + print_lint(sp[0]); + print_lint(sp[1]); + print_lint(sp[2]); + if (coq_extra_args > 0) { + print_instr("extra args > 0"); + print_lint(coq_extra_args); + coq_extra_args--; + pc = Code_val(accu); + coq_env = accu; + } else { + print_instr("extra args = 0"); + pc = (code_t)(sp[0]); + coq_env = sp[1]; + coq_extra_args = Long_val(sp[2]); + sp += 3; + } + Next; + } + Instruct(RESTART) { - int num_args = Wosize_val(coq_env) - 2; - int i; - print_instr("RESTART"); + int num_args = Wosize_val(coq_env) - 2; + 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); - coq_extra_args += num_args; - Next; + sp -= num_args; + for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2); + coq_env = Field(coq_env, 1); + coq_extra_args += num_args; + Next; } - + Instruct(GRAB) { - int required = *pc++; - print_instr("GRAB"); - /* printf("GRAB %d\n",required); */ - if (coq_extra_args >= required) { - coq_extra_args -= required; - } 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]; - Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */ - sp += num_args; - pc = (code_t)(sp[0]); - coq_env = sp[1]; - coq_extra_args = Long_val(sp[2]); - sp += 3; - } - Next; - } - - Instruct(GRABREC) { - 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 */ - } else { - if (coq_extra_args < rec_pos) { + int required = *pc++; + print_instr("GRAB"); + /* printf("GRAB %d\n",required); */ + if (coq_extra_args >= required) { + coq_extra_args -= required; + } 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]; + Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */ + sp += num_args; + pc = (code_t)(sp[0]); + coq_env = sp[1]; + coq_extra_args = Long_val(sp[2]); + sp += 3; + } + Next; + } + + Instruct(GRABREC) { + 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 */ + } 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; - sp += num_args; - pc = (code_t)(sp[0]); - coq_env = sp[1]; - coq_extra_args = Long_val(sp[2]); - sp += 3; - } else { - /* 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; - 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 */ - 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; - pc = (code_t)(sp[0]); - coq_env = sp[1]; - coq_extra_args = Long_val(sp[2]); - sp += 3; - } - } - Next; - } - + 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; + sp += num_args; + pc = (code_t)(sp[0]); + coq_env = sp[1]; + coq_extra_args = Long_val(sp[2]); + sp += 3; + } else { + /* 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; + 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 */ + 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; + pc = (code_t)(sp[0]); + coq_env = sp[1]; + coq_extra_args = Long_val(sp[2]); + sp += 3; + } + } + Next; + } + Instruct(CLOSURE) { - int nvars = *pc++; - int i; - print_instr("CLOSURE"); - print_int(nvars); - if (nvars > 0) *--sp = accu; - Alloc_small(accu, 1 + nvars, Closure_tag); - Code_val(accu) = pc + *pc; - pc++; - for (i = 0; i < nvars; i++) { - print_lint(sp[i]); - Field(accu, i + 1) = sp[i]; - } - sp += nvars; - Next; + int nvars = *pc++; + int i; + print_instr("CLOSURE"); + print_int(nvars); + if (nvars > 0) *--sp = accu; + Alloc_small(accu, 1 + nvars, Closure_tag); + Code_val(accu) = pc + *pc; + pc++; + for (i = 0; i < nvars; i++) { + print_lint(sp[i]); + Field(accu, i + 1) = sp[i]; + } + sp += nvars; + Next; } Instruct(CLOSUREREC) { - int nfuncs = *pc++; - int nvars = *pc++; - int start = *pc++; - int i; - value * p; - print_instr("CLOSUREREC"); - if (nvars > 0) *--sp = accu; - /* construction du vecteur de type */ + int nfuncs = *pc++; + int nvars = *pc++; + int start = *pc++; + int i; + value * p; + print_instr("CLOSUREREC"); + if (nvars > 0) *--sp = accu; + /* construction du vecteur de type */ Alloc_small(accu, nfuncs, Abstract_tag); - for(i = 0; i < nfuncs; i++) { - Field(accu,i) = (value)(pc+pc[i]); - } - 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++; - } - p = &Field(accu, 0); - *p = (value) (pc + pc[0]); - p++; - for (i = 1; i < nfuncs; i++) { - *p = Make_header(i * 2, Infix_tag, Caml_white); - p++; /* color irrelevant. */ - *p = (value) (pc + pc[i]); - p++; - } - pc += nfuncs; - accu = accu + 2 * start * sizeof(value); - Next; - } - - Instruct(CLOSURECOFIX){ - int nfunc = *pc++; - int nvars = *pc++; - int start = *pc++; - int i, j , size; - value * p; - print_instr("CLOSURECOFIX"); - if (nvars > 0) *--sp = accu; - /* construction du vecteur de type */ + for(i = 0; i < nfuncs; i++) { + Field(accu,i) = (value)(pc+pc[i]); + } + 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++; + } + p = &Field(accu, 0); + *p = (value) (pc + pc[0]); + p++; + for (i = 1; i < nfuncs; i++) { + *p = Make_header(i * 2, Infix_tag, Caml_white); + p++; /* color irrelevant. */ + *p = (value) (pc + pc[i]); + p++; + } + pc += nfuncs; + accu = accu + 2 * start * sizeof(value); + Next; + } + + Instruct(CLOSURECOFIX){ + int nfunc = *pc++; + int nvars = *pc++; + int start = *pc++; + int i, j , size; + value * p; + print_instr("CLOSURECOFIX"); + if (nvars > 0) *--sp = accu; + /* construction du vecteur de type */ Alloc_small(accu, nfunc, Abstract_tag); - for(i = 0; i < nfunc; i++) { - Field(accu,i) = (value)(pc+pc[i]); - } - pc += nfunc; - *--sp=accu; + for(i = 0; i < nfunc; i++) { + Field(accu,i) = (value)(pc+pc[i]); + } + pc += nfunc; + *--sp=accu; /* Creation des blocks accumulate */ for(i=0; i < nfunc; i++) { - Alloc_small(accu, 2, Accu_tag); - Code_val(accu) = accumulate; - Field(accu,1) = Val_int(1); - *--sp=accu; - } - /* creation des fonction cofix */ + Alloc_small(accu, 2, Accu_tag); + Code_val(accu) = accumulate; + Field(accu,1) = Val_int(1); + *--sp=accu; + } + /* creation des fonction cofix */ p = sp; - size = nfunc + nvars + 2; - 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, size - 1) = p[nfunc]; - for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = p[j]; - *--sp = accu; + size = nfunc + nvars + 2; + 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, size - 1) = p[nfunc]; + for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = 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++; - } - pc += nfunc; - accu = p[start]; + 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++; + } + pc += nfunc; + accu = p[start]; sp = p + nfunc + 1 + nvars; - print_instr("ici4"); - Next; + print_instr("ici4"); + Next; } - + Instruct(PUSHOFFSETCLOSURE) { - print_instr("PUSHOFFSETCLOSURE"); - *--sp = accu; + print_instr("PUSHOFFSETCLOSURE"); + *--sp = accu; } /* fallthrough */ Instruct(OFFSETCLOSURE) { - print_instr("OFFSETCLOSURE"); - accu = coq_env + *pc++ * sizeof(value); Next; + print_instr("OFFSETCLOSURE"); + accu = coq_env + *pc++ * sizeof(value); Next; } Instruct(PUSHOFFSETCLOSUREM2) { - print_instr("PUSHOFFSETCLOSUREM2"); - *--sp = accu; + print_instr("PUSHOFFSETCLOSUREM2"); + *--sp = accu; } /* fallthrough */ Instruct(OFFSETCLOSUREM2) { - print_instr("OFFSETCLOSUREM2"); - accu = coq_env - 2 * sizeof(value); Next; + print_instr("OFFSETCLOSUREM2"); + accu = coq_env - 2 * sizeof(value); Next; } Instruct(PUSHOFFSETCLOSURE0) { - print_instr("PUSHOFFSETCLOSURE0"); - *--sp = accu; + print_instr("PUSHOFFSETCLOSURE0"); + *--sp = accu; }/* fallthrough */ Instruct(OFFSETCLOSURE0) { - print_instr("OFFSETCLOSURE0"); - accu = coq_env; Next; + print_instr("OFFSETCLOSURE0"); + accu = coq_env; Next; } Instruct(PUSHOFFSETCLOSURE2){ - print_instr("PUSHOFFSETCLOSURE2"); - *--sp = accu; /* fallthrough */ + print_instr("PUSHOFFSETCLOSURE2"); + *--sp = accu; /* fallthrough */ } Instruct(OFFSETCLOSURE2) { - print_instr("OFFSETCLOSURE2"); - accu = coq_env + 2 * sizeof(value); Next; + print_instr("OFFSETCLOSURE2"); + accu = coq_env + 2 * sizeof(value); Next; } /* Access to global variables */ Instruct(PUSHGETGLOBAL) { - print_instr("PUSH"); - *--sp = accu; + print_instr("PUSH"); + *--sp = accu; } /* Fallthrough */ Instruct(GETGLOBAL){ - print_instr("GETGLOBAL"); - print_int(*pc); - accu = Field(coq_global_data, *pc); + print_instr("GETGLOBAL"); + print_int(*pc); + accu = Field(coq_global_data, *pc); pc++; Next; - } + } /* Allocation of blocks */ Instruct(MAKEBLOCK) { - mlsize_t wosize = *pc++; - tag_t tag = *pc++; - mlsize_t i; - value block; - print_instr("MAKEBLOCK, tag="); - Alloc_small(block, wosize, tag); - Field(block, 0) = accu; - for (i = 1; i < wosize; i++) Field(block, i) = *sp++; - accu = block; - Next; + mlsize_t wosize = *pc++; + tag_t tag = *pc++; + mlsize_t i; + value block; + print_instr("MAKEBLOCK, tag="); + Alloc_small(block, wosize, tag); + Field(block, 0) = accu; + for (i = 1; i < wosize; i++) Field(block, i) = *sp++; + accu = block; + Next; } Instruct(MAKEBLOCK1) { - - tag_t tag = *pc++; - value block; - print_instr("MAKEBLOCK1, tag="); - print_int(tag); - Alloc_small(block, 1, tag); - Field(block, 0) = accu; - accu = block; - Next; + + tag_t tag = *pc++; + value block; + print_instr("MAKEBLOCK1, tag="); + print_int(tag); + Alloc_small(block, 1, tag); + Field(block, 0) = accu; + accu = block; + Next; } Instruct(MAKEBLOCK2) { - - tag_t tag = *pc++; - value block; - print_instr("MAKEBLOCK2, tag="); - print_int(tag); - Alloc_small(block, 2, tag); - Field(block, 0) = accu; - Field(block, 1) = sp[0]; - sp += 1; - accu = block; - Next; + + tag_t tag = *pc++; + value block; + print_instr("MAKEBLOCK2, tag="); + print_int(tag); + Alloc_small(block, 2, tag); + Field(block, 0) = accu; + Field(block, 1) = sp[0]; + sp += 1; + accu = block; + Next; } Instruct(MAKEBLOCK3) { - tag_t tag = *pc++; - value block; - print_instr("MAKEBLOCK3, tag="); - print_int(tag); - Alloc_small(block, 3, tag); - Field(block, 0) = accu; - Field(block, 1) = sp[0]; - Field(block, 2) = sp[1]; - sp += 2; - accu = block; - Next; + tag_t tag = *pc++; + value block; + print_instr("MAKEBLOCK3, tag="); + print_int(tag); + Alloc_small(block, 3, tag); + Field(block, 0) = accu; + Field(block, 1) = sp[0]; + Field(block, 2) = sp[1]; + sp += 2; + accu = block; + Next; } Instruct(MAKEBLOCK4) { - tag_t tag = *pc++; - value block; - print_instr("MAKEBLOCK4, tag="); - print_int(tag); - Alloc_small(block, 4, tag); - Field(block, 0) = accu; - Field(block, 1) = sp[0]; - Field(block, 2) = sp[1]; - Field(block, 3) = sp[2]; - sp += 3; - accu = block; - Next; - } - - + tag_t tag = *pc++; + value block; + print_instr("MAKEBLOCK4, tag="); + print_int(tag); + Alloc_small(block, 4, tag); + Field(block, 0) = accu; + Field(block, 1) = sp[0]; + Field(block, 2) = sp[1]; + Field(block, 3) = sp[2]; + sp += 3; + accu = block; + Next; + } + + /* Access to components of blocks */ - + Instruct(SWITCH) { - uint32_t sizes = *pc++; - print_instr("SWITCH"); - print_int(sizes & 0xFFFFFF); - if (Is_block(accu)) { - long index = Tag_val(accu); - print_instr("block"); - print_lint(index); - pc += pc[(sizes & 0xFFFFFF) + index]; - } else { - long index = Long_val(accu); - print_instr("constant"); - print_lint(index); - pc += pc[index]; - } - Next; + uint32_t sizes = *pc++; + print_instr("SWITCH"); + print_int(sizes & 0xFFFFFF); + if (Is_block(accu)) { + long index = Tag_val(accu); + print_instr("block"); + print_lint(index); + pc += pc[(sizes & 0xFFFFFF) + index]; + } else { + long index = Long_val(accu); + print_instr("constant"); + print_lint(index); + pc += pc[index]; + } + Next; } Instruct(PUSHFIELDS){ - int i; - int size = *pc++; - print_instr("PUSHFIELDS"); - sp -= size; - for(i=0;i -#include +#include #include #include #include "coq_gc.h" @@ -31,7 +31,7 @@ int drawinstr; long coq_saved_sp_offset; value * coq_sp; -/* Some predefined pointer code */ +/* Some predefined pointer code */ code_t accumulate; /* functions over global environment */ @@ -80,7 +80,7 @@ void init_coq_stack() coq_stack_high = coq_stack_low + Coq_stack_size / sizeof (value); coq_stack_threshold = coq_stack_low + Coq_stack_threshold / sizeof(value); coq_max_stack_size = Coq_max_stack_size; -} +} void init_coq_interpreter() { @@ -96,14 +96,14 @@ value init_coq_vm(value unit) /* ML */ fprintf(stderr,"already open \n");fflush(stderr);} else { drawinstr=0; -#ifdef THREADED_CODE +#ifdef THREADED_CODE init_arity(); #endif /* THREADED_CODE */ /* Allocate the table of global and the stack */ init_coq_stack(); /* Initialing the interpreter */ init_coq_interpreter(); - + /* Some predefined pointer code. * It is typically contained in accumulator blocks whose tag is 0 and thus * scanned by the GC, so make it look like an OCaml block. */ @@ -117,7 +117,7 @@ value init_coq_vm(value unit) /* ML */ coq_prev_scan_roots_hook = scan_roots_hook; scan_roots_hook = coq_scan_roots; coq_vm_initialized = 1; - } + } return Val_unit;; } diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index 1ea461c5e5..7f982d0477 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -39,7 +39,7 @@ extern int drawinstr; /* interp state */ extern value * coq_sp; -/* Some predefined pointer code */ +/* Some predefined pointer code */ extern code_t accumulate; /* functions over global environment */ @@ -49,7 +49,7 @@ value coq_static_alloc(value size); /* ML */ value init_coq_vm(value unit); /* ML */ value re_init_coq_vm(value unit); /* ML */ -void realloc_coq_stack(asize_t required_space); +void realloc_coq_stack(asize_t required_space); value coq_set_transp_value(value transp); /* ML */ value get_coq_transp_value(value unit); /* ML */ #endif /* _COQ_MEMORY_ */ diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index e05f3fb82e..3613bc07a6 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -39,7 +39,7 @@ value coq_closure_arity(value clos) { if (Is_instruction(c,RESTART)) { c++; if (Is_instruction(c,GRAB)) return Val_int(3 + c[1] - Wosize_val(clos)); - else { + else { if (Wosize_val(clos) != 2) failwith("Coq Values : coq_closure_arity"); return Val_int(1); } -- cgit v1.2.3