From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- kernel/byterun/coq_fix_code.c | 30 ++-- kernel/byterun/coq_instruct.h | 14 +- kernel/byterun/coq_interp.c | 356 ++++++++++++++++++++++++++++-------------- kernel/byterun/coq_memory.c | 7 +- kernel/byterun/coq_memory.h | 1 - kernel/byterun/coq_values.c | 3 +- kernel/byterun/coq_values.h | 14 +- 7 files changed, 281 insertions(+), 144 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 4616580d..70648b44 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -27,31 +27,31 @@ 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[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[RESTART]=arity[OFFSETCLOSUREM2]= + 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[RESTART]=arity[OFFSETCLOSUREM2]= arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]= arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]= + 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[FORCE]=arity[MAKEPROD]= 0; + arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= 0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= - arity[PUSH_RETADDR]= - arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=arity[APPTERM3]=arity[RETURN]= - arity[GRAB]=arity[COGRAB]= - arity[OFFSETCLOSURE]=arity[PUSHOFFSETCLOSURE]= - arity[GETGLOBAL]=arity[PUSHGETGLOBAL]= - arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEACCU]= - arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=arity[PUSHFIELD]= - arity[ACCUMULATECOND]= 1; + arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]= + arity[APPTERM3]=arity[RETURN]=arity[GRAB]=arity[OFFSETCLOSURE]= + arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]= + arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]= + arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]= + arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=arity[ACCUMULATECOND]= 1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=2; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; /* instruction with arbitrary operands */ - arity[CLOSUREREC]=arity[SWITCH]=0; + arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0; } #endif /* THREADED_CODE */ @@ -150,7 +150,7 @@ value coq_tcode_of_code (value code, value size) { block_size = sizes >> 16; sizes = const_size + block_size; for(i=0; i 0) { coq_extra_args--; @@ -485,30 +504,6 @@ value coq_interprete Next; } - Instruct(COGRAB){ - int required = *pc++; - print_instr("COGRAB"); - if(forcable == Val_true) { - print_instr("true"); - /* L'instruction précédante est FORCE */ - if (coq_extra_args > 0) coq_extra_args--; - pc++; - forcable = Val_false; - } else { /* L'instruction précédante est APPLY */ - 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"); @@ -607,7 +602,59 @@ value coq_interprete 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, 0); + 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 */ + + 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; + /* 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]; + sp = p + nfunc + 1 + nvars; + print_instr("ici4"); + Next; + } + + Instruct(PUSHOFFSETCLOSURE) { print_instr("PUSHOFFSETCLOSURE"); *--sp = accu; @@ -644,7 +691,7 @@ value coq_interprete /* Access to global variables */ Instruct(PUSHGETGLOBAL) { - print_instr("PUSHGETGLOBAL"); + print_instr("PUSH"); *--sp = accu; } /* Fallthrough */ @@ -703,38 +750,27 @@ value coq_interprete accu = block; Next; } + Instruct(MAKEBLOCK4) { + tag_t tag = *pc++; + value block; + print_instr("MAKEBLOCK4"); + 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 */ - -/* Branches and conditional branches */ - Instruct(FORCE) { - print_instr("FORCE"); - if (Is_block(accu) && Tag_val(accu) == Closure_tag) { - forcable = Val_true; - /* On pousse l'addresse de retour et l'argument */ - sp -= 3; - sp[0] = (value) (pc - 1); - sp[1] = coq_env; - sp[2] = Val_long(coq_extra_args); - /* On evalue le cofix */ - coq_extra_args = 0; - pc = Code_val(accu); - coq_env = accu; - goto check_stacks; - } else { - if (Is_block(accu)) print_int(Tag_val(accu)); - else print_instr("Not a block"); - } - Next; - } - - Instruct(SWITCH) { uint32 sizes = *pc++; print_instr("SWITCH"); - print_int(sizes); + print_int(sizes & 0xFFFF); if (Is_block(accu)) { long index = Tag_val(accu); print_instr("block"); @@ -748,68 +784,79 @@ value coq_interprete } Next; } - Instruct(PUSHFIELD){ + + Instruct(PUSHFIELDS){ int i; int size = *pc++; - print_instr("PUSHFIELD"); + print_instr("PUSHFIELDS"); sp -= size; for(i=0;i