compatibility with POWERPC

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7

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)