1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
/***********************************************************************/
/* */
/* Coq Compiler */
/* */
/* Benjamin Gregoire, projets Logical and Cristal */
/* INRIA Rocquencourt */
/* */
/* */
/***********************************************************************/
#include <stdio.h>
#include <string.h>
#include <caml/alloc.h>
#include <caml/address_class.h>
#include "coq_gc.h"
#include "coq_instruct.h"
#include "coq_fix_code.h"
#include "coq_memory.h"
#include "coq_interp.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 */
int drawinstr;
/* interp state */
long coq_saved_sp_offset;
value * coq_sp;
/* 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 accumulate_code(value unit) /* ML */
{
CAMLparam1(unit);
CAMLlocal1(res);
res = caml_alloc_small(1, Abstract_tag);
Code_val(res) = accumulate;
CAMLreturn(res);
}
static void (*coq_prev_scan_roots_hook) (scanning_action);
static void coq_scan_roots(scanning_action action)
{
register value * i;
/* Scan the stack */
for (i = coq_sp; i < coq_stack_high; i++) {
#ifdef NO_NAKED_POINTERS
/* The VM stack may contain C-allocated bytecode */
if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue;
#endif
(*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_interpreter()
{
coq_sp = coq_stack_high;
coq_interprete(NULL, Val_unit, Atom(0), Atom(0), Val_unit, 0);
}
static int coq_vm_initialized = 0;
value init_coq_vm(value unit) /* ML */
{
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();
/* Initialing the interpreter */
init_coq_interpreter();
/* Some predefined pointer code.
* It is typically contained in accumlator blocks whose tag is 0 and thus
* scanned by the GC, so make it look like an OCaml block. */
value accu_block = (value) coq_stat_alloc(2 * sizeof(value));
Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \
accumulate = (code_t) Val_hp(accu_block);
*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;;
}
/* [required_space] is a size in words */
void realloc_coq_stack(asize_t required_space)
{
asize_t size;
value * new_low, * new_high, * new_sp;
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 coq_set_drawinstr(value unit)
{
drawinstr = 1;
return Val_unit;
}
|
