aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun')
-rw-r--r--kernel/byterun/coq_fix_code.c246
-rw-r--r--kernel/byterun/coq_fix_code.h12
-rw-r--r--kernel/byterun/coq_interp.c8
-rw-r--r--kernel/byterun/coq_memory.c10
4 files changed, 113 insertions, 163 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 446c76498..4616580df 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -18,6 +18,45 @@
#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);
@@ -25,16 +64,11 @@ void * coq_stat_alloc (asize_t sz)
return result;
}
-#ifdef THREADED_CODE
-
-char ** coq_instr_table;
-char * coq_instr_base;
-
value coq_makeaccu (value i) {
code_t q;
code_t res = coq_stat_alloc(8);
q = res;
- *q++ = (opcode_t)(coq_instr_table[MAKEACCU] - coq_instr_base);
+ *q++ = VALINSTR(MAKEACCU);
*q = (opcode_t)Int_val(i);
return (value)res;
}
@@ -43,178 +77,90 @@ value coq_accucond (value i) {
code_t q;
code_t res = coq_stat_alloc(8);
q = res;
- *q++ = (opcode_t)(coq_instr_table[ACCUMULATECOND] - coq_instr_base);
+ *q++ = VALINSTR(ACCUMULATECOND);
*q = (opcode_t)Int_val(i);
return (value)res;
}
-value coq_is_accumulate_code(value code){
- code_t q;
- int res;
- q = (code_t)code;
- res =
- (*q == (opcode_t)(coq_instr_table[ACCUMULATECOND] - coq_instr_base))
- ||
- (*q == (opcode_t)(coq_instr_table[ACCUMULATE] - coq_instr_base));
- return Val_bool(res);
-}
-
value coq_pushpop (value i) {
code_t res;
int n;
n = Int_val(i);
if (n == 0) {
res = coq_stat_alloc(4);
- *res = (opcode_t)(coq_instr_table[STOP] - coq_instr_base);
+ *res = VALINSTR(STOP);
return (value)res;
}
else {
code_t q;
res = coq_stat_alloc(12);
q = res;
- *q++ = (opcode_t)(coq_instr_table[POP] - coq_instr_base);
+ *q++ = VALINSTR(POP);
*q++ = (opcode_t)n;
- *q = (opcode_t)(coq_instr_table[STOP] - coq_instr_base);
+ *q = VALINSTR(STOP);
return (value)res;
}
}
-
-code_t coq_thread_code (code_t code, asize_t len){
- opcode_t instr;
- code_t p, q;
- code_t res = coq_stat_alloc(len);
- int i;
- q = res;
- len /= sizeof(opcode_t);
- for (p=code; p < code + len; /*nothing*/) {
- instr = *p++;
- *q++ = (opcode_t)(coq_instr_table[instr] - coq_instr_base);
- switch(instr){
- /* instruction with zero operand */
- case ACC0: case ACC1: case ACC2: case ACC3: case ACC4: case ACC5:
- case ACC6: case ACC7: case PUSH: case PUSHACC0: case PUSHACC1:
- case PUSHACC2: case PUSHACC3: case PUSHACC4: case PUSHACC5: case PUSHACC6:
- case PUSHACC7: case ENVACC1: case ENVACC2: case ENVACC3: case ENVACC4:
- case PUSHENVACC1: case PUSHENVACC2: case PUSHENVACC3: case PUSHENVACC4:
- case APPLY1: case APPLY2: case APPLY3: case RESTART: case OFFSETCLOSUREM2:
- case OFFSETCLOSURE0: case OFFSETCLOSURE2: case PUSHOFFSETCLOSUREM2:
- case PUSHOFFSETCLOSURE0: case PUSHOFFSETCLOSURE2:
- case CONST0: case CONST1: case CONST2: case CONST3:
- case PUSHCONST0: case PUSHCONST1: case PUSHCONST2: case PUSHCONST3:
- case ACCUMULATE: case STOP: case FORCE: case MAKEPROD:
- break;
-
- /* instruction with one operand */
- case ACC: case PUSHACC: case POP: case ENVACC: case PUSHENVACC:
- case PUSH_RETADDR:
- case APPLY: case APPTERM1: case APPTERM2: case APPTERM3: case RETURN:
- case GRAB: case COGRAB:
- case OFFSETCLOSURE: case PUSHOFFSETCLOSURE:
- case GETGLOBAL: case PUSHGETGLOBAL:
- /* case GETGLOBALBOXED: case PUSHGETGLOBALBOXED: */
- case MAKEBLOCK1: case MAKEBLOCK2: case MAKEBLOCK3: case MAKEACCU:
- case CONSTINT: case PUSHCONSTINT: case GRABREC: case PUSHFIELD:
- case ACCUMULATECOND:
- *q++ = *p++;
- break;
-
- /* instruction with two operands */
- case APPTERM: case MAKEBLOCK: case CLOSURE:
- *q++ = *p++; *q++ = *p++;
- break;
-
- /* instruction with four operands */
- case MAKESWITCHBLOCK:
- *q++ = *p++; *q++ = *p++; *q++ = *p++; *q++ = *p++;
- break;
-
- /* instruction with arbitrary operands */
- case CLOSUREREC: {
- int i;
- uint32 n = 2*(*p) + 3; /* ndefs, nvars, start, typlbls,lbls*/
- for(i=0; i < n; i++) *q++ = *p++;
- }
- break;
-
- case SWITCH: {
- int i;
- uint32 sizes = *p;
- uint32 const_size = sizes & 0xFFFF;
- uint32 block_size = sizes >> 16;
- sizes = const_size + block_size + 1 ;/* sizes */
- for(i=0; i < sizes; i++) *q++ = *p++;
- }
- break;
-
- default:
- invalid_argument("Fatal error in coq_thread_code : bad opcode");
- break;
- }
- }
- if (p != code + len) fprintf(stderr, "error thread code\n");
- return res;
-}
-
-value coq_tcode_of_code(value code, value len){
- return (value)coq_thread_code((code_t)code,(asize_t) Long_val(len));
-}
-#else
-
-value coq_makeaccu (value i) {
- code_t q;
- code_t res = coq_stat_alloc(8);
- q = res;
- *q++ = (opcode_t)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++ = (opcode_t)ACCUMULATECOND;
- *q = (opcode_t)Int_val(i);
- return (value)res;
-}
value coq_is_accumulate_code(value code){
code_t q;
int res;
q = (code_t)code;
- res =
- (*q == ACCUMULATECOND) ||
- (*q == ACCUMULATE);
+ res = Is_instruction(q,ACCUMULATECOND) || Is_instruction(q,ACCUMULATE);
return Val_bool(res);
}
-value coq_pushpop (value i) {
- code_t res;
- int n;
- n = Int_val(i);
- if (n == 0) {
- res = coq_stat_alloc(4);
- *res = (opcode_t)STOP;
- return (value)res;
- }
- else {
- res = coq_stat_alloc(12);
- q = res;
- *q++ = (opcode_t)POP;
- *q++ = (opcode_t)n;
- *q = (opcode_t)STOP;
- return (value)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 s, value size)
-{
- void * new_s = coq_stat_alloc(Int_val(size));
- memmove(new_s, &Byte(s, 0), Int_val(size));
- return (value)new_s;
+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<sizes; i++) { COPY32(q,p); p++; q++; };
+ } else if (instr == CLOSUREREC) {
+ uint32 i, n;
+ COPY32(q,p); p++; /* ndefs */
+ n = 3 + 2*(*q); /* ndefs, nvars, start, typlbls,lbls*/
+ q++;
+ for(i=1; i<n; i++) { COPY32(q,p); p++; q++; };
+ } else {
+ uint32 i, ar;
+ ar = arity[instr];
+ for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
+ }
+ }
+ return (value)res;
}
-
-#endif /* THREADED_CODE */
-
-
-
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index e3296c0da..035d5b9b1 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -18,11 +18,13 @@ void * coq_stat_alloc (asize_t sz);
#ifdef THREADED_CODE
extern char ** coq_instr_table;
extern char * coq_instr_base;
-#define Is_instruction(i1,i2) \
- (*i1 == (opcode_t)(coq_instr_table[i2] - coq_instr_base))
-#else
-#define Is_instruction(i1,i2) (*i1 == i2)
-#endif
+void init_arity();
+#define VALINSTR(instr) ((opcode_t)(coq_instr_table[instr] - coq_instr_base))
+#else
+#define VALINSTR(instr) instr
+#endif /* THREADED_CODE */
+
+#define Is_instruction(pc,instr) (*pc == VALINSTR(instr))
value coq_tcode_of_code(value code, value len);
value coq_makeaccu (value i);
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 692baa7e7..48d91e4dc 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -55,11 +55,11 @@ sp is a local copy of the global variable extern_sp. */
# define Next break
#endif
-/*#define _COQ_DEBUG_*/
+/*#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)
+# 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)
@@ -164,7 +164,9 @@ value coq_interprete
#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;
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index f94d2fb9e..db6aacb92 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -124,9 +124,11 @@ value init_coq_vm(value unit) /* ML */
if (coq_vm_initialized == 1) {
fprintf(stderr,"already open \n");fflush(stderr);}
else {
-
- /* Allocate the table of global and the stack */
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);
@@ -138,9 +140,7 @@ value init_coq_vm(value unit) /* ML */
/* Some predefined pointer code */
accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t));
- *accumulate = ACCUMULATE;
- accumulate =
- (code_t) coq_tcode_of_code((value)accumulate, Val_int(sizeof(opcode_t)));
+ *accumulate = VALINSTR(ACCUMULATE);
/* Initialize GC */
if (coq_prev_scan_roots_hook == NULL)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 05:10:09 +0000