From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- kernel/byterun/coq_fix_code.c | 166 +++++++ kernel/byterun/coq_fix_code.h | 34 ++ kernel/byterun/coq_gc.h | 48 +++ kernel/byterun/coq_instruct.h | 39 ++ kernel/byterun/coq_interp.c | 974 ++++++++++++++++++++++++++++++++++++++++++ kernel/byterun/coq_interp.h | 23 + kernel/byterun/coq_memory.c | 273 ++++++++++++ kernel/byterun/coq_memory.h | 70 +++ kernel/byterun/coq_values.c | 69 +++ kernel/byterun/coq_values.h | 28 ++ 10 files changed, 1724 insertions(+) create mode 100644 kernel/byterun/coq_fix_code.c create mode 100644 kernel/byterun/coq_fix_code.h create mode 100644 kernel/byterun/coq_gc.h create mode 100644 kernel/byterun/coq_instruct.h create mode 100644 kernel/byterun/coq_interp.c create mode 100644 kernel/byterun/coq_interp.h create mode 100644 kernel/byterun/coq_memory.c create mode 100644 kernel/byterun/coq_memory.h create mode 100644 kernel/byterun/coq_values.c create mode 100644 kernel/byterun/coq_values.h (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c new file mode 100644 index 00000000..4616580d --- /dev/null +++ b/kernel/byterun/coq_fix_code.c @@ -0,0 +1,166 @@ +/***********************************************************************/ +/* */ +/* Coq Compiler */ +/* */ +/* Benjamin Gregoire, projets Logical and Cristal */ +/* INRIA Rocquencourt */ +/* */ +/* */ +/***********************************************************************/ + +#include +#include +#include "config.h" +#include "misc.h" +#include "mlvalues.h" +#include "fail.h" +#include "memory.h" +#include "coq_instruct.h" +#include "coq_fix_code.h" + +#ifdef THREADED_CODE +char ** coq_instr_table; +char * coq_instr_base; +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[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[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= + arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= + arity[ACCUMULATE]=arity[STOP]=arity[FORCE]=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; + /* 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; +} + +#endif /* THREADED_CODE */ + + +void * coq_stat_alloc (asize_t sz) +{ + void * result = malloc (sz); + if (result == NULL) raise_out_of_memory (); + return result; +} + +value coq_makeaccu (value i) { + code_t q; + code_t res = coq_stat_alloc(8); + q = res; + *q++ = VALINSTR(MAKEACCU); + *q = (opcode_t)Int_val(i); + return (value)res; +} + +value coq_accucond (value i) { + code_t q; + code_t res = coq_stat_alloc(8); + q = res; + *q++ = VALINSTR(ACCUMULATECOND); + *q = (opcode_t)Int_val(i); + return (value)res; +} + +value coq_pushpop (value i) { + code_t res; + int n; + n = Int_val(i); + if (n == 0) { + res = coq_stat_alloc(4); + *res = VALINSTR(STOP); + return (value)res; + } + else { + code_t q; + res = coq_stat_alloc(12); + q = res; + *q++ = VALINSTR(POP); + *q++ = (opcode_t)n; + *q = VALINSTR(STOP); + return (value)res; + } +} + +value coq_is_accumulate_code(value code){ + code_t q; + int res; + q = (code_t)code; + res = Is_instruction(q,ACCUMULATECOND) || Is_instruction(q,ACCUMULATE); + return Val_bool(res); +} + +#ifdef ARCH_BIG_ENDIAN +#define Reverse_32(dst,src) { \ + char * _p, * _q; \ + char _a, _b; \ + _p = (char *) (src); \ + _q = (char *) (dst); \ + _a = _p[0]; \ + _b = _p[1]; \ + _q[0] = _p[3]; \ + _q[1] = _p[2]; \ + _q[3] = _a; \ + _q[2] = _b; \ +} +#define COPY32(dst,src) Reverse_32(dst,src) +#else +#define COPY32(dst,src) (*dst=*src) +#endif /* ARCH_BIG_ENDIAN */ + +value coq_tcode_of_code (value code, value size) { + code_t p, q, res; + asize_t len = (asize_t) Long_val(size); + res = coq_stat_alloc(len); + q = res; + len /= sizeof(opcode_t); + for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) { + opcode_t instr; + COPY32(&instr,p); + p++; + if (instr < 0 || instr > STOP){ + instr = STOP; + }; + *q++ = VALINSTR(instr); + if (instr == SWITCH) { + uint32 i, sizes, const_size, block_size; + COPY32(q,p); p++; + sizes=*q++; + const_size = sizes & 0xFFFF; + block_size = sizes >> 16; + sizes = const_size + block_size; + for(i=0; i +#include "coq_gc.h" +#include "coq_instruct.h" +#include "coq_fix_code.h" +#include "coq_memory.h" +#include "coq_values.h" + + +/* Registers for the abstract machine: + pc the code pointer + sp the stack pointer (grows downward) + accu the accumulator + env heap-allocated environment + trapsp pointer to the current trap frame + extra_args number of extra arguments provided by the caller + +sp is a local copy of the global variable extern_sp. */ + + + +/* Instruction decoding */ + + +#ifdef THREADED_CODE +# define Instruct(name) coq_lbl_##name: +# if defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32) +# define coq_Jumptbl_base ((char *) &&coq_lbl_ACC0) +# else +# define coq_Jumptbl_base ((char *) 0) +# define coq_jumptbl_base ((char *) 0) +# endif +# ifdef DEBUG +# define Next goto next_instr +# else +# ifdef __ia64__ +# define Next goto *(void *)(coq_jumptbl_base + *((uint32 *) pc)++) +# else +# define Next goto *(void *)(coq_jumptbl_base + *pc++) +# endif +# endif +#else +# define Instruct(name) case name: +# define Next break +#endif + +/* #define _COQ_DEBUG_ */ + +#ifdef _COQ_DEBUG_ +# define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s) +# define print_int(i) /*if (drawinstr)*/ printf("%d\n",i) +# else +# define print_instr(s) +# define print_int(i) +#endif + +/* GC interface */ +#define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } +#define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } + + +/* Register optimization. + Some compilers underestimate the use of the local variables representing + the abstract machine registers, and don't put them in hardware registers, + which slows down the interpreter considerably. + For GCC, Xavier Leroy have hand-assigned hardware registers for + several architectures. +*/ + +#if defined(__GNUC__) && !defined(DEBUG) +#ifdef __mips__ +#define PC_REG asm("$16") +#define SP_REG asm("$17") +#define ACCU_REG asm("$18") +#endif +#ifdef __sparc__ +#define PC_REG asm("%l0") +#define SP_REG asm("%l1") +#define ACCU_REG asm("%l2") +#endif +#ifdef __alpha__ +#ifdef __CRAY__ +#define PC_REG asm("r9") +#define SP_REG asm("r10") +#define ACCU_REG asm("r11") +#define JUMPTBL_BASE_REG asm("r12") +#else +#define PC_REG asm("$9") +#define SP_REG asm("$10") +#define ACCU_REG asm("$11") +#define JUMPTBL_BASE_REG asm("$12") +#endif +#endif +#ifdef __i386__ +#define PC_REG asm("%esi") +#define SP_REG asm("%edi") +#define ACCU_REG +#endif +#if defined(PPC) || defined(_POWER) || defined(_IBMR2) +#define PC_REG asm("26") +#define SP_REG asm("27") +#define ACCU_REG asm("28") +#endif +#ifdef __hppa__ +#define PC_REG asm("%r18") +#define SP_REG asm("%r17") +#define ACCU_REG asm("%r16") +#endif +#ifdef __mc68000__ +#define PC_REG asm("a5") +#define SP_REG asm("a4") +#define ACCU_REG asm("d7") +#endif +#ifdef __arm__ +#define PC_REG asm("r9") +#define SP_REG asm("r8") +#define ACCU_REG asm("r7") +#endif +#ifdef __ia64__ +#define PC_REG asm("36") +#define SP_REG asm("37") +#define ACCU_REG asm("38") +#define JUMPTBL_BASE_REG asm("39") +#endif +#endif + +/* The interpreter itself */ + +value coq_interprete +(code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args) +{ + /*Declaration des variables */ +#ifdef PC_REG + register code_t pc PC_REG; + register value * sp SP_REG; + register value accu ACCU_REG; +#else + register code_t pc; + register value * sp; + register value accu; +#endif +#if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32) +#ifdef JUMPTBL_BASE_REG + register char * coq_jumptbl_base JUMPTBL_BASE_REG; +#else + register char * coq_jumptbl_base; +#endif +#endif +#ifdef THREADED_CODE + static void * coq_jumptable[] = { +# include "coq_jumptbl.h" + }; +#else + opcode_t curr_instr; +#endif + print_instr("Enter Interpreter"); + if (coq_pc == NULL) { /* Interpreter is initializing */ + print_instr("Interpreter is initializing"); +#ifdef THREADED_CODE + coq_instr_table = (char **) coq_jumptable; + coq_instr_base = coq_Jumptbl_base; +#endif + return Val_unit; + } +#if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32) + coq_jumptbl_base = coq_Jumptbl_base; +#endif + + /* Initialisation */ + sp = coq_sp; + pc = coq_pc; + accu = coq_accu; +#ifdef THREADED_CODE + goto *(void *)(coq_jumptbl_base + *pc++); /* Jump to the first instruction */ +#else + while(1) { + curr_instr = *pc++; + switch(curr_instr) { +#endif +/* Basic stack operations */ + + Instruct(ACC0){ + print_instr("ACC0"); + accu = sp[0]; Next; + } + Instruct(ACC1){ + print_instr("ACC1"); + accu = sp[1]; Next; + } + Instruct(ACC2){ + print_instr("ACC2"); + accu = sp[2]; Next; + } + Instruct(ACC3){ + print_instr("ACC3"); + accu = sp[3]; Next; + } + Instruct(ACC4){ + print_instr("ACC4"); + accu = sp[4]; Next; + } + Instruct(ACC5){ + print_instr("ACC5"); + accu = sp[5]; Next; + } + Instruct(ACC6){ + print_instr("ACC6"); + accu = sp[6]; Next; + } + Instruct(ACC7){ + print_instr("ACC7"); + accu = sp[7]; Next; + } + Instruct(PUSH){ + 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; + } + Instruct(PUSHACC2){ + print_instr("PUSHACC2"); + *--sp = accu; accu = sp[2]; Next; + } + Instruct(PUSHACC3){ + print_instr("PUSHACC3"); + *--sp = accu; accu = sp[3]; Next; + } + Instruct(PUSHACC4){ + print_instr("PUSHACC4"); + *--sp = accu; accu = sp[4]; Next; + } + Instruct(PUSHACC5){ + print_instr("PUSHACC5"); + *--sp = accu; accu = sp[5]; Next; + } + Instruct(PUSHACC6){ + print_instr("PUSHACC5"); + *--sp = accu; accu = sp[6]; Next; + } + Instruct(PUSHACC7){ + print_instr("PUSHACC7"); + *--sp = accu; accu = sp[7]; Next; + } + Instruct(PUSHACC){ + print_instr("PUSHACC"); + *--sp = accu; + } + /* Fallthrough */ + + Instruct(ACC){ + print_instr("ACC"); + accu = sp[*pc++]; + Next; + } + + Instruct(POP){ + print_instr("POP"); + sp += *pc++; + Next; + } + /* Access in heap-allocated environment */ + + Instruct(ENVACC1){ + print_instr("ENVACC1"); + accu = Field(coq_env, 1); Next; + } + Instruct(ENVACC2){ + print_instr("ENVACC2"); + accu = Field(coq_env, 2); Next; + } + Instruct(ENVACC3){ + print_instr("ENVACC3"); + accu = Field(coq_env, 3); Next; + } + Instruct(ENVACC4){ + print_instr("ENVACC4"); + accu = Field(coq_env, 4); Next; + } + Instruct(PUSHENVACC1){ + print_instr("PUSHENVACC1"); + *--sp = accu; accu = Field(coq_env, 1); Next; + } + Instruct(PUSHENVACC2){ + print_instr("PUSHENVACC2"); + *--sp = accu; accu = Field(coq_env, 2); 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; + } + Instruct(PUSHENVACC){ + print_instr("PUSHENVACC"); + *--sp = accu; + } + /* Fallthrough */ + Instruct(ENVACC){ + print_instr("ENVACC"); + accu = Field(coq_env, *pc++); + Next; + } + /* Function application */ + + Instruct(PUSH_RETADDR) { + print_instr("PUSH_RETADDR"); + sp -= 3; + sp[0] = (value) (pc + *pc); + sp[1] = coq_env; + sp[2] = Val_long(coq_extra_args); + coq_extra_args = 0; + pc++; + Next; + } + Instruct(APPLY) { + print_instr("APPLY"); + coq_extra_args = *pc - 1; + pc = Code_val(accu); + coq_env = accu; + goto check_stacks; + } + Instruct(APPLY1) { + value arg1 = sp[0]; + print_instr("APPLY1"); + sp -= 3; + sp[0] = arg1; + sp[1] = (value)pc; + sp[2] = coq_env; + sp[3] = Val_long(coq_extra_args); + pc = Code_val(accu); + coq_env = accu; + coq_extra_args = 0; + goto check_stacks; + } + Instruct(APPLY2) { + value arg1 = sp[0]; + value arg2 = sp[1]; + print_instr("APPLY2"); + sp -= 3; + sp[0] = arg1; + sp[1] = arg2; + sp[2] = (value)pc; + sp[3] = coq_env; + sp[4] = Val_long(coq_extra_args); + pc = Code_val(accu); + coq_env = accu; + coq_extra_args = 1; + goto check_stacks; + } + Instruct(APPLY3) { + value arg1 = sp[0]; + value arg2 = sp[1]; + value arg3 = sp[2]; + print_instr("APPLY3"); + sp -= 3; + sp[0] = arg1; + sp[1] = arg2; + sp[2] = arg3; + sp[3] = (value)pc; + sp[4] = coq_env; + sp[5] = Val_long(coq_extra_args); + pc = Code_val(accu); + coq_env = accu; + coq_extra_args = 2; + goto check_stacks; + } + + Instruct(APPTERM) { + 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_stacks; + } + 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_stacks; + } + 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); + coq_env = accu; + coq_extra_args += 1; + goto check_stacks; + } + 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_stacks; + } + + Instruct(RETURN) { + print_instr("RETURN"); + sp += *pc++; + if (coq_extra_args > 0) { + coq_extra_args--; + pc = Code_val(accu); + coq_env = accu; + } else { + 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"); + 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(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"); + if (rec_pos <= coq_extra_args && !Is_accu(sp[rec_pos])) { + pc++;/* On saute le Restart */ + } else { + if (coq_extra_args < rec_pos) { + 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 { + /* L'argument recursif est un accumulateur */ + mlsize_t num_args, i; + /* Construction du PF partiellement appliqué */ + Alloc_small(accu, rec_pos + 2, Closure_tag); + Field(accu, 1) = coq_env; + for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; + Code_val(accu) = pc; + sp += rec_pos; + *--sp = accu; + /* Construction de l'atom */ + Alloc_small(accu, 2, ATOM_FIX_TAG); + Field(accu,1) = sp[0]; + Field(accu,0) = sp[1]; + sp++; sp[0] = accu; + /* Construction de l'accumulateur */ + 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++) 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 */ + Alloc_small(accu, nfuncs, 0); + 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(PUSHOFFSETCLOSURE) { + print_instr("PUSHOFFSETCLOSURE"); + *--sp = accu; + } /* 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; + } + Instruct(PUSHOFFSETCLOSURE0) { + print_instr("PUSHOFFSETCLOSURE0"); + *--sp = accu; + }/* fallthrough */ + Instruct(OFFSETCLOSURE0) { + print_instr("OFFSETCLOSURE0"); + accu = coq_env; Next; + } + Instruct(PUSHOFFSETCLOSURE2){ + print_instr("PUSHOFFSETCLOSURE2"); + *--sp = accu; /* fallthrough */ + } + Instruct(OFFSETCLOSURE2) { + print_instr("OFFSETCLOSURE2"); + accu = coq_env + 2 * sizeof(value); Next; + } + +/* Access to global variables */ + + Instruct(PUSHGETGLOBAL) { + print_instr("PUSHGETGLOBAL"); + *--sp = accu; + } + /* Fallthrough */ + Instruct(GETGLOBAL){ + print_instr("GETGLOBAL"); + 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"); + 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"); + Alloc_small(block, 1, tag); + Field(block, 0) = accu; + accu = block; + Next; + } + Instruct(MAKEBLOCK2) { + + tag_t tag = *pc++; + value block; + print_instr("MAKEBLOCK2"); + 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"); + Alloc_small(block, 3, tag); + Field(block, 0) = accu; + Field(block, 1) = sp[0]; + Field(block, 2) = sp[1]; + sp += 2; + 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); + if (Is_block(accu)) { + long index = Tag_val(accu); + print_instr("block"); + print_int(index); + pc += pc[(sizes & 0xFFFF) + index]; + } else { + long index = Long_val(accu); + print_instr("constant"); + print_int(index); + pc += pc[index]; + } + Next; + } + Instruct(PUSHFIELD){ + int i; + int size = *pc++; + print_instr("PUSHFIELD"); + sp -= size; + for(i=0;i +#include +#include "coq_gc.h" +#include "coq_instruct.h" +#include "coq_fix_code.h" +#include "coq_memory.h" + +/* stack */ + +value * coq_stack_low; +value * coq_stack_high; +value * coq_stack_threshold; +asize_t coq_max_stack_size = Coq_max_stack_size; +/* global_data */ + + +value coq_global_data; +value coq_global_boxed; +int coq_all_transp; +value coq_atom_tbl; + +int drawinstr; +/* interp state */ + +long coq_saved_sp_offset; +value * coq_sp; +value forcable; +/* Some predefined pointer code */ +code_t accumulate; + +/* functions over global environment */ + +void coq_stat_free (void * blk) +{ + free (blk); +} + +value coq_static_alloc(value size) /* ML */ +{ + return (value) coq_stat_alloc((asize_t) Long_val(size)); +} + +value coq_static_free(value blk) /* ML */ +{ + coq_stat_free((void *) blk); + return Val_unit; +} + +value accumulate_code(value unit) /* ML */ +{ + return (value) accumulate; +} + +static void (*coq_prev_scan_roots_hook) (scanning_action); + +static void coq_scan_roots(scanning_action action) +{ + register value * i; + /* Scan the global variables */ + (*action)(coq_global_data, &coq_global_data); + (*action)(coq_global_boxed, &coq_global_boxed); + (*action)(coq_atom_tbl, &coq_atom_tbl); + /* Scan the stack */ + for (i = coq_sp; i < coq_stack_high; i++) { + (*action) (*i, i); + }; + /* Hook */ + if (coq_prev_scan_roots_hook != NULL) (*coq_prev_scan_roots_hook)(action); + + +} + +void init_coq_stack() +{ + coq_stack_low = (value *) coq_stat_alloc(Coq_stack_size); + 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_global_data(long requested_size) +{ + int i; + coq_global_data = alloc_shr(requested_size, 0); + for (i = 0; i < requested_size; i++) + Field (coq_global_data, i) = Val_unit; +} + +void init_coq_global_boxed(long requested_size) +{ + int i; + coq_global_boxed = alloc_shr(requested_size, 0); + for (i = 0; i < requested_size; i++) + Field (coq_global_boxed, i) = Val_true; +} + +void init_coq_atom_tbl(long requested_size){ + int i; + coq_atom_tbl = alloc_shr(requested_size, 0); + for (i = 0; i < requested_size; i++) Field (coq_atom_tbl, i) = Val_unit; +} + +void init_coq_interpreter() +{ + coq_sp = coq_stack_high; + coq_interprete(NULL, Val_unit, Val_unit, 0); +} + +static int coq_vm_initialized = 0; + +value init_coq_vm(value unit) /* ML */ +{ + int i; + if (coq_vm_initialized == 1) { + fprintf(stderr,"already open \n");fflush(stderr);} + else { + drawinstr=0; +#ifdef THREADED_CODE + init_arity(); +#endif /* THREADED_CODE */ + /* Allocate the table of global and the stack */ + init_coq_stack(); + init_coq_global_data(Coq_global_data_Size); + init_coq_global_boxed(40); + init_coq_atom_tbl(40); + /* Initialing the interpreter */ + coq_all_transp = 0; + forcable = Val_false; + init_coq_interpreter(); + + /* Some predefined pointer code */ + accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t)); + *accumulate = VALINSTR(ACCUMULATE); + + /* Initialize GC */ + if (coq_prev_scan_roots_hook == NULL) + coq_prev_scan_roots_hook = scan_roots_hook; + scan_roots_hook = coq_scan_roots; + coq_vm_initialized = 1; + } + return Val_unit;; +} + +void realloc_coq_stack(asize_t required_space) +{ + asize_t size; + value * new_low, * new_high, * new_sp; + value * p; + size = coq_stack_high - coq_stack_low; + do { + size *= 2; + } while (size < coq_stack_high - coq_sp + required_space); + new_low = (value *) coq_stat_alloc(size * sizeof(value)); + new_high = new_low + size; + +#define shift(ptr) \ + ((char *) new_high - ((char *) coq_stack_high - (char *) (ptr))) + + new_sp = (value *) shift(coq_sp); + memmove((char *) new_sp, + (char *) coq_sp, + (coq_stack_high - coq_sp) * sizeof(value)); + coq_stat_free(coq_stack_low); + coq_stack_low = new_low; + coq_stack_high = new_high; + coq_stack_threshold = coq_stack_low + Coq_stack_threshold / sizeof(value); + coq_sp = new_sp; +#undef shift +} + +value get_coq_global_data(value unit) /* ML */ +{ + return coq_global_data; +} + +value get_coq_atom_tbl(value unit) /* ML */ +{ + return coq_atom_tbl; +} + +value get_coq_global_boxed(value unit) /* ML */ +{ + return coq_global_boxed; +} + +value realloc_coq_global_data(value size) /* ML */ +{ + mlsize_t requested_size, actual_size, i; + value new_global_data; + requested_size = Long_val(size); + actual_size = Wosize_val(coq_global_data); + if (requested_size >= actual_size) { + requested_size = (requested_size + 0x100) & 0xFFFFFF00; + new_global_data = alloc_shr(requested_size, 0); + for (i = 0; i < actual_size; i++) + initialize(&Field(new_global_data, i), Field(coq_global_data, i)); + for (i = actual_size; i < requested_size; i++){ + Field (new_global_data, i) = Val_long (0); + } + coq_global_data = new_global_data; + } + return Val_unit; +} + +value realloc_coq_global_boxed(value size) /* ML */ +{ + mlsize_t requested_size, actual_size, i; + value new_global_boxed; + requested_size = Long_val(size); + actual_size = Wosize_val(coq_global_boxed); + if (requested_size >= actual_size) { + requested_size = (requested_size + 0x100) & 0xFFFFFF00; + new_global_boxed = alloc_shr(requested_size, 0); + for (i = 0; i < actual_size; i++) + initialize(&Field(new_global_boxed, i), Field(coq_global_boxed, i)); + for (i = actual_size; i < requested_size; i++) + Field (new_global_boxed, i) = Val_long (0); + coq_global_boxed = new_global_boxed; + } + return Val_unit; +} + +value realloc_coq_atom_tbl(value size) /* ML */ +{ + mlsize_t requested_size, actual_size, i; + value new_atom_tbl; + requested_size = Long_val(size); + actual_size = Wosize_val(coq_atom_tbl); + if (requested_size >= actual_size) { + requested_size = (requested_size + 0x100) & 0xFFFFFF00; + new_atom_tbl = alloc_shr(requested_size, 0); + for (i = 0; i < actual_size; i++) + initialize(&Field(new_atom_tbl, i), Field(coq_atom_tbl, i)); + for (i = actual_size; i < requested_size; i++) + Field (new_atom_tbl, i) = Val_long (0); + coq_atom_tbl = new_atom_tbl; + } + return Val_unit; +} + + +value coq_set_transp_value(value transp) +{ + coq_all_transp = (transp == Val_true); + return Val_unit; +} + +value get_coq_transp_value(value unit) +{ + return Val_bool(coq_all_transp); +} + +value coq_set_drawinstr(value unit) +{ + drawinstr = 1; + return Val_unit; +} + +value coq_set_forcable (value unit) +{ + forcable = Val_true; + return Val_unit; +} diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h new file mode 100644 index 00000000..7c96e684 --- /dev/null +++ b/kernel/byterun/coq_memory.h @@ -0,0 +1,70 @@ +/***********************************************************************/ +/* */ +/* Coq Compiler */ +/* */ +/* Benjamin Gregoire, projets Logical and Cristal */ +/* INRIA Rocquencourt */ +/* */ +/* */ +/***********************************************************************/ + +#ifndef _COQ_MEMORY_ +#define _COQ_MEMORY_ + +#include "config.h" +#include "fail.h" +#include "misc.h" +#include "memory.h" +#include "mlvalues.h" + + +#define Coq_stack_size (4096 * sizeof(value)) +#define Coq_stack_threshold (256 * sizeof(value)) +#define Coq_global_data_Size (4096 * sizeof(value)) +#define Coq_max_stack_size (256 * 1024) + +#define TRANSP 0 +#define BOXED 1 + +/* stack */ + +extern value * coq_stack_low; +extern value * coq_stack_high; +extern value * coq_stack_threshold; + +/* global_data */ + +extern value coq_global_data; +extern value coq_global_boxed; +extern int coq_all_transp; +extern value coq_atom_tbl; + +extern int drawinstr; +/* interp state */ + +extern value * coq_sp; +extern value forcable; +/* Some predefined pointer code */ +extern code_t accumulate; + +/* functions over global environment */ + +value coq_static_alloc(value size); /* ML */ +value coq_static_free(value string); /* ML */ + +value init_coq_vm(value unit); /* ML */ +value re_init_coq_vm(value unit); /* ML */ + +void realloc_coq_stack(asize_t required_space); +value get_coq_global_data(value unit); /* ML */ +value realloc_coq_global_data(value size); /* ML */ +value get_coq_global_boxed(value unit); +value realloc_coq_global_boxed(value size); /* ML */ +value get_coq_atom_tbl(value unit); /* ML */ +value realloc_coq_atom_tbl(value size); /* ML */ +value coq_set_transp_value(value transp); /* ML */ +value get_coq_transp_value(value unit); /* ML */ +#endif /* _COQ_MEMORY_ */ + + +value coq_set_drawinstr(value unit); diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c new file mode 100644 index 00000000..baf3ab09 --- /dev/null +++ b/kernel/byterun/coq_values.c @@ -0,0 +1,69 @@ +/***********************************************************************/ +/* */ +/* Coq Compiler */ +/* */ +/* Benjamin Gregoire, projets Logical and Cristal */ +/* INRIA Rocquencourt */ +/* */ +/* */ +/***********************************************************************/ + +#include +#include "coq_fix_code.h" +#include "coq_instruct.h" +#include "coq_memory.h" +#include "coq_values.h" +#include "memory.h" +/* KIND OF VALUES */ + +#define Setup_for_gc +#define Restore_after_gc + +value coq_kind_of_closure(value v) { + opcode_t * c; + int res; + int is_app = 0; + c = Code_val(v); + if (Is_instruction(c, GRAB)) return Val_int(0); + if (Is_instruction(c, RESTART)) {is_app = 1; c++;} + if (Is_instruction(c, GRABREC)) return Val_int(1+is_app); + if (Is_instruction(c, COGRAB)) return Val_int(3+is_app); + if (Is_instruction(c, MAKEACCU)) return Val_int(5); + return Val_int(0); +} + + +/* DESTRUCT ACCU */ + +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)); + else { + if (Wosize_val(clos) != 2) failwith("Coq Values : coq_closure_arity"); + return Val_int(1); + } + } + if (Is_instruction(c,GRAB)) return Val_int(1 + c[1]); + return Val_int(1); +} + +/* Fonction sur les fix */ + +value coq_offset(value v) { + if (Tag_val(v) == Closure_tag) return Val_int(0); + else return Val_long(-Wsize_bsize(Infix_offset_val(v))); +} + +value coq_offset_closure(value v, value offset){ + return (value)&Field(v, Int_val(offset)); +} + +value coq_offset_tcode(value code,value offset){ + return((value)((code_t)code + Int_val(offset))); +} + +value coq_int_tcode(value code, value offset) { + return Val_int(*((code_t) code + Int_val(offset))); +} diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h new file mode 100644 index 00000000..a186d62a --- /dev/null +++ b/kernel/byterun/coq_values.h @@ -0,0 +1,28 @@ +/***********************************************************************/ +/* */ +/* Coq Compiler */ +/* */ +/* Benjamin Gregoire, projets Logical and Cristal */ +/* INRIA Rocquencourt */ +/* */ +/* */ +/***********************************************************************/ + +#ifndef _COQ_VALUES_ +#define _COQ_VALUES_ + +#include "alloc.h" +#include "mlvalues.h" + +#define ATOM_FIX_TAG 3 +#define ATOM_SWITCH_TAG 4 + +#define Accu_tag 0 +#define Default_tag 0 + +/* Les blocs accumulate */ +#define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) + +#endif /* _COQ_VALUES_ */ + + -- cgit v1.2.3