← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to kernel/byterun/coq_fix_code.c

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
kernel/byterun/coq_fix_code.c
 
1
/***********************************************************************/
 
2
/*                                                                     */
 
3
/*                           Coq Compiler                              */
 
4
/*                                                                     */
 
5
/*        Benjamin Gregoire, projets Logical and Cristal               */
 
6
/*                        INRIA Rocquencourt                           */
 
7
/*                                                                     */
 
8
/*                                                                     */
 
9
/***********************************************************************/
 
10
 
 
11
/* Arnaud Spiwack: expanded the virtual machine with operators used
 
12
   for fast computation of bounded (31bits) integers */
 
13
 
 
14
#include <stdio.h>
 
15
#include <stdlib.h> 
 
16
#include <caml/config.h>
 
17
#include <caml/misc.h>
 
18
#include <caml/mlvalues.h>
 
19
#include <caml/fail.h>
 
20
#include <caml/memory.h>
 
21
#include "coq_instruct.h"
 
22
#include "coq_fix_code.h"
 
23
 
 
24
#ifdef THREADED_CODE
 
25
char ** coq_instr_table;
 
26
char * coq_instr_base;
 
27
int arity[STOP+1];
 
28
 
 
29
void init_arity () {
 
30
  /* instruction with zero operand */
 
31
  arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]=
 
32
    arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]=
 
33
    arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]=
 
34
    arity[PUSHACC6]=arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]=
 
35
    arity[ENVACC3]=arity[ENVACC4]=arity[PUSHENVACC1]=arity[PUSHENVACC2]=
 
36
    arity[PUSHENVACC3]=arity[PUSHENVACC4]=arity[APPLY1]=arity[APPLY2]=
 
37
    arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]=
 
38
    arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]=
 
39
    arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]=
 
40
    arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]=
 
41
    arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
 
42
    arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
 
43
    arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= 
 
44
    arity[ADDINT31]=arity[ADDCINT31]=arity[ADDCARRYCINT31]=
 
45
    arity[SUBINT31]=arity[SUBCINT31]=arity[SUBCARRYCINT31]=
 
46
    arity[MULCINT31]=arity[MULINT31]=arity[COMPAREINT31]=
 
47
    arity[DIV21INT31]=arity[DIVINT31]=arity[ADDMULDIVINT31]=
 
48
    arity[HEAD0INT31]=arity[TAIL0INT31]=
 
49
    arity[COMPINT31]=arity[DECOMPINT31]=0;
 
50
  /* instruction with one operand */
 
51
  arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
 
52
    arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=
 
53
    arity[APPTERM3]=arity[RETURN]=arity[GRAB]=arity[OFFSETCLOSURE]=
 
54
    arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]=
 
55
    arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]=
 
56
    arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=
 
57
    arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=arity[ACCUMULATECOND]=
 
58
    arity[BRANCH]=arity[ISCONST]= 1;
 
59
  /* instruction with two operands */
 
60
  arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
 
61
  arity[ARECONST]=2;
 
62
  /* instruction with four operands */ 
 
63
  arity[MAKESWITCHBLOCK]=4;
 
64
  /* instruction with arbitrary operands */
 
65
  arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0;
 
66
}
 
67
 
 
68
#endif /*  THREADED_CODE */
 
69
 
 
70
 
 
71
void * coq_stat_alloc (asize_t sz)
 
72
{
 
73
  void * result = malloc (sz);
 
74
  if (result == NULL) raise_out_of_memory ();
 
75
  return result;
 
76
}
 
77
 
 
78
value coq_makeaccu (value i) {
 
79
  code_t q;
 
80
  code_t res = coq_stat_alloc(8);
 
81
  q = res;
 
82
  *q++ = VALINSTR(MAKEACCU);
 
83
  *q = (opcode_t)Int_val(i);
 
84
  return (value)res;
 
85
}
 
86
 
 
87
value coq_accucond (value i) {
 
88
  code_t q;
 
89
  code_t res = coq_stat_alloc(8);
 
90
  q = res;
 
91
  *q++ = VALINSTR(ACCUMULATECOND);
 
92
  *q = (opcode_t)Int_val(i);
 
93
  return (value)res;
 
94
}
 
95
 
 
96
value coq_pushpop (value i) {
 
97
  code_t res;
 
98
  int n;
 
99
  n = Int_val(i);
 
100
  if (n == 0) {
 
101
    res = coq_stat_alloc(4);
 
102
    *res = VALINSTR(STOP);
 
103
    return (value)res;
 
104
  }
 
105
  else {
 
106
    code_t q;
 
107
    res = coq_stat_alloc(12);
 
108
    q = res;
 
109
    *q++ = VALINSTR(POP);
 
110
    *q++ = (opcode_t)n;
 
111
    *q = VALINSTR(STOP);
 
112
    return (value)res;
 
113
  }
 
114
}
 
115
 
 
116
value coq_is_accumulate_code(value code){
 
117
  code_t q;
 
118
  int res;
 
119
  q = (code_t)code;
 
120
  res = Is_instruction(q,ACCUMULATECOND) || Is_instruction(q,ACCUMULATE);
 
121
  return Val_bool(res);
 
122
}
 
123
 
 
124
#ifdef ARCH_BIG_ENDIAN
 
125
#define Reverse_32(dst,src) {                                               \
 
126
  char * _p, * _q;                                                          \
 
127
  char _a, _b;                                                              \
 
128
  _p = (char *) (src);                                                      \
 
129
  _q = (char *) (dst);                                                      \
 
130
  _a = _p[0];                                                               \
 
131
  _b = _p[1];                                                               \
 
132
  _q[0] = _p[3];                                                            \
 
133
  _q[1] = _p[2];                                                            \
 
134
  _q[3] = _a;                                                               \
 
135
  _q[2] = _b;                                                               \
 
136
}
 
137
#define COPY32(dst,src) Reverse_32(dst,src)
 
138
#else
 
139
#define COPY32(dst,src) (*dst=*src)
 
140
#endif /* ARCH_BIG_ENDIAN */
 
141
 
 
142
value coq_tcode_of_code (value code, value size) {
 
143
  code_t p, q, res; 
 
144
  asize_t len = (asize_t) Long_val(size);
 
145
  res = coq_stat_alloc(len);
 
146
  q = res;
 
147
  len /= sizeof(opcode_t);
 
148
  for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) {  
 
149
    opcode_t instr;
 
150
    COPY32(&instr,p); 
 
151
    p++;
 
152
    if (instr < 0 || instr > STOP){
 
153
      instr = STOP;
 
154
    };
 
155
    *q++ = VALINSTR(instr);
 
156
    if (instr == SWITCH) {
 
157
      uint32 i, sizes, const_size, block_size;
 
158
      COPY32(q,p); p++;
 
159
      sizes=*q++;
 
160
      const_size = sizes & 0xFFFF;
 
161
      block_size = sizes >> 16;
 
162
      sizes = const_size + block_size;
 
163
      for(i=0; i<sizes; i++) { COPY32(q,p); p++; q++; };
 
164
    } else if (instr == CLOSUREREC || instr==CLOSURECOFIX) {
 
165
      uint32 i, n;
 
166
      COPY32(q,p); p++; /* ndefs */
 
167
      n = 3 + 2*(*q);  /* ndefs, nvars, start, typlbls,lbls*/
 
168
      q++;
 
169
      for(i=1; i<n; i++) { COPY32(q,p); p++; q++; };
 
170
    } else {
 
171
      uint32 i, ar;
 
172
      ar = arity[instr]; 
 
173
      for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
 
174
    }
 
175
  }
 
176
  return (value)res;
 
177
}