compatibility with POWERPC

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

1 files changed, 96 insertions, 150 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 446c764989..4616580dfc 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 */
-
-
-