aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun')
-rw-r--r--kernel/byterun/coq_fix_code.c182
-rw-r--r--kernel/byterun/coq_fix_code.h35
-rw-r--r--kernel/byterun/coq_gc.h59
-rw-r--r--kernel/byterun/coq_interp.c1614
-rw-r--r--kernel/byterun/coq_interp.h26
-rw-r--r--kernel/byterun/coq_memory.c156
-rw-r--r--kernel/byterun/coq_memory.h58
-rw-r--r--kernel/byterun/coq_uint63_emul.h97
-rw-r--r--kernel/byterun/coq_uint63_native.h125
-rw-r--r--kernel/byterun/coq_values.c94
-rw-r--r--kernel/byterun/coq_values.h43
-rw-r--r--kernel/byterun/dune13
-rw-r--r--kernel/byterun/libcoqrun.clib4
13 files changed, 2506 insertions, 0 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
new file mode 100644
index 0000000000..0865487c98
--- /dev/null
+++ b/kernel/byterun/coq_fix_code.c
@@ -0,0 +1,182 @@
+/***********************************************************************/
+/* */
+/* Coq Compiler */
+/* */
+/* Benjamin Gregoire, projets Logical and Cristal */
+/* INRIA Rocquencourt */
+/* */
+/* */
+/***********************************************************************/
+
+/* Arnaud Spiwack: expanded the virtual machine with operators used
+ for fast computation of bounded (31bits) integers */
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <stdint.h>
+#include <caml/config.h>
+#include <caml/misc.h>
+#include <caml/mlvalues.h>
+#include <caml/fail.h>
+#include <caml/alloc.h>
+#include <caml/memory.h>
+#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[APPLY4]=arity[RESTART]=arity[OFFSETCLOSUREM2]=
+ arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]=
+ arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]=
+ arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]=
+ arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
+ arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
+ arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]=
+ arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]=
+ arity[ISINT]=arity[AREINT2]=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[OFFSETCLOSURE]=
+ arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]=
+ arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]=
+ arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=
+ arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=
+ arity[BRANCH]=arity[ENSURESTACKCAPACITY]=
+ arity[CHECKADDINT63]=arity[CHECKADDCINT63]=arity[CHECKADDCARRYCINT63]=
+ arity[CHECKSUBINT63]=arity[CHECKSUBCINT63]=arity[CHECKSUBCARRYCINT63]=
+ arity[CHECKMULINT63]=arity[CHECKMULCINT63]=
+ arity[CHECKDIVINT63]=arity[CHECKMODINT63]=arity[CHECKDIVEUCLINT63]=
+ arity[CHECKDIV21INT63]=
+ arity[CHECKLXORINT63]=arity[CHECKLORINT63]=arity[CHECKLANDINT63]=
+ arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]=
+ arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]=
+ arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]=
+ arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=1;
+ /* instruction with two operands */
+ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
+ arity[PROJ]=2;
+ /* instruction with four operands */
+ arity[MAKESWITCHBLOCK]=4;
+ /* instruction with arbitrary operands */
+ arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0;
+}
+
+#endif /* THREADED_CODE */
+
+
+void * coq_stat_alloc (asize_t sz)
+{
+ void * result = malloc (sz);
+ if (result == NULL) raise_out_of_memory ();
+ return result;
+}
+
+value coq_makeaccu (value i) {
+ CAMLparam1(i);
+ CAMLlocal1(res);
+ code_t q = coq_stat_alloc(2 * sizeof(opcode_t));
+ res = caml_alloc_small(1, Abstract_tag);
+ Code_val(res) = q;
+ *q++ = VALINSTR(MAKEACCU);
+ *q = (opcode_t)Int_val(i);
+ CAMLreturn(res);
+}
+
+value coq_pushpop (value i) {
+ CAMLparam1(i);
+ CAMLlocal1(res);
+ code_t q;
+ res = caml_alloc_small(1, Abstract_tag);
+ int n = Int_val(i);
+ if (n == 0) {
+ q = coq_stat_alloc(sizeof(opcode_t));
+ Code_val(res) = q;
+ *q = VALINSTR(STOP);
+ CAMLreturn(res);
+ }
+ else {
+ q = coq_stat_alloc(3 * sizeof(opcode_t));
+ Code_val(res) = q;
+ *q++ = VALINSTR(POP);
+ *q++ = (opcode_t)n;
+ *q = VALINSTR(STOP);
+ CAMLreturn(res);
+ }
+}
+
+value coq_is_accumulate_code(value code){
+ code_t q = Code_val(code);
+ int res;
+ res = Is_instruction(q,ACCUMULATE);
+ return Val_bool(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 code) {
+ CAMLparam1 (code);
+ CAMLlocal1 (res);
+ code_t p, q;
+ asize_t len = (asize_t) caml_string_length(code);
+ res = caml_alloc_small(1, Abstract_tag);
+ q = coq_stat_alloc(len);
+ Code_val(res) = q;
+ 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_t i, sizes, const_size, block_size;
+ COPY32(q,p); p++;
+ sizes=*q++;
+ const_size = sizes & 0xFFFFFF;
+ block_size = sizes >> 24;
+ sizes = const_size + block_size;
+ for(i=0; i<sizes; i++) { COPY32(q,p); p++; q++; };
+ } else if (instr == CLOSUREREC || instr==CLOSURECOFIX) {
+ uint32_t 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_t i, ar;
+ ar = arity[instr];
+ for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
+ }
+ }
+ CAMLreturn(res);
+}
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
new file mode 100644
index 0000000000..5a233e6178
--- /dev/null
+++ b/kernel/byterun/coq_fix_code.h
@@ -0,0 +1,35 @@
+/***********************************************************************/
+/* */
+/* Coq Compiler */
+/* */
+/* Benjamin Gregoire, projets Logical and Cristal */
+/* INRIA Rocquencourt */
+/* */
+/* */
+/***********************************************************************/
+
+
+#ifndef _COQ_FIX_CODE_
+#define _COQ_FIX_CODE_
+
+#include <caml/mlvalues.h>
+void * coq_stat_alloc (asize_t sz);
+
+#ifdef THREADED_CODE
+extern char ** coq_instr_table;
+extern char * coq_instr_base;
+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 coq_makeaccu (value i);
+value coq_pushpop (value i);
+value coq_accucond (value i);
+value coq_is_accumulate_code(value code);
+
+#endif /* _COQ_FIX_CODE_ */
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
new file mode 100644
index 0000000000..f06275862c
--- /dev/null
+++ b/kernel/byterun/coq_gc.h
@@ -0,0 +1,59 @@
+/***********************************************************************/
+/* */
+/* Coq Compiler */
+/* */
+/* Benjamin Gregoire, projets Logical and Cristal */
+/* INRIA Rocquencourt */
+/* */
+/* */
+/***********************************************************************/
+
+#ifndef _COQ_CAML_GC_
+#define _COQ_CAML_GC_
+#include <caml/mlvalues.h>
+#include <caml/alloc.h>
+#include <caml/memory.h>
+
+typedef void (*scanning_action) (value, value *);
+
+
+CAMLextern char *young_ptr;
+CAMLextern char *young_limit;
+CAMLextern void (*scan_roots_hook) (scanning_action);
+CAMLextern void minor_collection (void);
+
+#define Caml_white (0 << 8)
+#define Caml_black (3 << 8)
+
+#ifdef HAS_OCP_MEMPROF
+
+/* This code is necessary to make the OCamlPro memory profiling branch of
+ OCaml compile. */
+
+#define Make_header(wosize, tag, color) \
+ caml_make_header(wosize, tag, color)
+
+#else
+
+#define Make_header(wosize, tag, color) \
+ (((header_t) (((header_t) (wosize) << 10) \
+ + (color) \
+ + (tag_t) (tag))) \
+ )
+#endif
+
+#define Alloc_small(result, wosize, tag) do{ \
+ young_ptr -= Bhsize_wosize (wosize); \
+ if (young_ptr < young_limit){ \
+ young_ptr += Bhsize_wosize (wosize); \
+ Setup_for_gc; \
+ minor_collection (); \
+ Restore_after_gc; \
+ young_ptr -= Bhsize_wosize (wosize); \
+ } \
+ Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black); \
+ (result) = Val_hp (young_ptr); \
+ }while(0)
+
+
+#endif /*_COQ_CAML_GC_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
new file mode 100644
index 0000000000..d2c88bffcc
--- /dev/null
+++ b/kernel/byterun/coq_interp.c
@@ -0,0 +1,1614 @@
+/***********************************************************************/
+/* */
+/* Coq Compiler */
+/* */
+/* Benjamin Gregoire, projets Logical and Cristal */
+/* INRIA Rocquencourt */
+/* */
+/* */
+/***********************************************************************/
+
+/* The bytecode interpreter */
+
+/* Spiwack: expanded the virtual machine with operators used
+ for fast computation of bounded (31bits) integers */
+
+#include <stdio.h>
+#include <signal.h>
+#include <stdint.h>
+#include <caml/memory.h>
+#include "coq_gc.h"
+#include "coq_instruct.h"
+#include "coq_fix_code.h"
+#include "coq_memory.h"
+#include "coq_values.h"
+
+#ifdef ARCH_SIXTYFOUR
+#include "coq_uint63_native.h"
+#else
+#include "coq_uint63_emul.h"
+#endif
+
+/* spiwack: I append here a few macros for value/number manipulation */
+#define uint32_of_value(val) (((uint32_t)(val)) >> 1)
+#define value_of_uint32(i) ((value)((((uint32_t)(i)) << 1) | 1))
+#define UI64_of_uint32(lo) ((uint64_t)((uint32_t)(lo)))
+#define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val)))
+/* /spiwack */
+
+
+
+/* Registers for the abstract machine:
+ pc the code pointer
+ sp the stack pointer (grows downward)
+ accu the accumulator
+ env heap-allocated environment
+ trapsp pointer to the current trap frame
+ extra_args number of extra arguments provided by the caller
+
+sp is a local copy of the global variable extern_sp. */
+
+
+
+/* Instruction decoding */
+
+
+#ifdef THREADED_CODE
+# define Instruct(name) coq_lbl_##name:
+# if defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
+# define coq_Jumptbl_base ((char *) &&coq_lbl_ACC0)
+# else
+# define coq_Jumptbl_base ((char *) 0)
+# define coq_jumptbl_base ((char *) 0)
+# endif
+# ifdef DEBUG
+# define Next goto next_instr
+# else
+# define Next goto *(void *)(coq_jumptbl_base + *pc++)
+# endif
+#else
+# define Instruct(name) case name:
+# define Next break
+#endif
+
+/* #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_lint(i) /*if (drawinstr)*/ printf("%ld\n",i)
+# else
+# define print_instr(s)
+# define print_int(i)
+# define print_lint(i)
+#endif
+
+#define CHECK_STACK(num_args) { \
+if (sp - num_args < coq_stack_threshold) { \
+ coq_sp = sp; \
+ realloc_coq_stack(num_args + Coq_stack_threshold / sizeof(value)); \
+ sp = coq_sp; \
+ } \
+}
+
+/* GC interface */
+#define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; }
+#define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; }
+
+
+/* Register optimization.
+ Some compilers underestimate the use of the local variables representing
+ the abstract machine registers, and don't put them in hardware registers,
+ which slows down the interpreter considerably.
+ For GCC, Xavier Leroy have hand-assigned hardware registers for
+ several architectures.
+*/
+
+#if defined(__GNUC__) && !defined(DEBUG)
+#ifdef __mips__
+#define PC_REG asm("$16")
+#define SP_REG asm("$17")
+#define ACCU_REG asm("$18")
+#endif
+#ifdef __sparc__
+#define PC_REG asm("%l0")
+#define SP_REG asm("%l1")
+#define ACCU_REG asm("%l2")
+#endif
+#ifdef __alpha__
+#ifdef __CRAY__
+#define PC_REG asm("r9")
+#define SP_REG asm("r10")
+#define ACCU_REG asm("r11")
+#define JUMPTBL_BASE_REG asm("r12")
+#else
+#define PC_REG asm("$9")
+#define SP_REG asm("$10")
+#define ACCU_REG asm("$11")
+#define JUMPTBL_BASE_REG asm("$12")
+#endif
+#endif
+#ifdef __i386__
+#define PC_REG asm("%esi")
+#define SP_REG asm("%edi")
+#define ACCU_REG
+#endif
+#if defined(PPC) || defined(_POWER) || defined(_IBMR2)
+#define PC_REG asm("26")
+#define SP_REG asm("27")
+#define ACCU_REG asm("28")
+#endif
+#ifdef __hppa__
+#define PC_REG asm("%r18")
+#define SP_REG asm("%r17")
+#define ACCU_REG asm("%r16")
+#endif
+#ifdef __mc68000__
+#define PC_REG asm("a5")
+#define SP_REG asm("a4")
+#define ACCU_REG asm("d7")
+#endif
+#if defined(__arm__) && !defined(__thumb2__)
+#define PC_REG asm("r9")
+#define SP_REG asm("r8")
+#define ACCU_REG asm("r7")
+#endif
+#ifdef __ia64__
+#define PC_REG asm("36")
+#define SP_REG asm("37")
+#define ACCU_REG asm("38")
+#define JUMPTBL_BASE_REG asm("39")
+#endif
+#endif
+
+#define CheckInt1() do{ \
+ if (Is_uint63(accu)) pc++; \
+ else{ \
+ *--sp=accu; \
+ accu = Field(coq_global_data, *pc++); \
+ goto apply1; \
+ } \
+ }while(0)
+
+#define CheckInt2() do{ \
+ if (Is_uint63(accu) && Is_uint63(sp[0])) pc++; \
+ else{ \
+ *--sp=accu; \
+ accu = Field(coq_global_data, *pc++); \
+ goto apply2; \
+ } \
+ }while(0)
+
+
+
+#define CheckInt3() do{ \
+ if (Is_uint63(accu) && Is_uint63(sp[0]) && Is_uint63(sp[1]) ) pc++; \
+ else{ \
+ *--sp=accu; \
+ accu = Field(coq_global_data, *pc++); \
+ goto apply3; \
+ } \
+ }while(0)
+
+#define AllocCarry(cond) Alloc_small(accu, 1, (cond)? coq_tag_C1 : coq_tag_C0)
+#define AllocPair() Alloc_small(accu, 2, coq_tag_pair)
+
+/* For signal handling, we hijack some code from the caml runtime */
+
+extern intnat caml_signals_are_pending;
+extern intnat caml_pending_signals[];
+extern void caml_process_pending_signals(void);
+
+/* The interpreter itself */
+
+value coq_interprete
+(code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args)
+{
+ /* coq_accu is not allocated on the OCaml heap */
+ CAMLparam2(coq_atom_tbl, coq_global_data);
+
+ /*Declaration des variables */
+#ifdef PC_REG
+ register code_t pc PC_REG;
+ register value * sp SP_REG;
+ register value accu ACCU_REG;
+#else
+ register code_t pc;
+ register value * sp;
+ register value accu;
+#endif
+#if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
+#ifdef JUMPTBL_BASE_REG
+ register char * coq_jumptbl_base JUMPTBL_BASE_REG;
+#else
+ register char * coq_jumptbl_base;
+#endif
+#endif
+#ifdef THREADED_CODE
+ static void * coq_jumptable[] = {
+# include "coq_jumptbl.h"
+ };
+#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;
+#endif
+ CAMLreturn(Val_unit);
+ }
+#if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
+ coq_jumptbl_base = coq_Jumptbl_base;
+#endif
+
+ /* Initialisation */
+ sp = coq_sp;
+ pc = coq_pc;
+ accu = coq_accu;
+
+ CHECK_STACK(0);
+
+#ifdef THREADED_CODE
+ goto *(void *)(coq_jumptbl_base + *pc++); /* Jump to the first instruction */
+#else
+ while(1) {
+ curr_instr = *pc++;
+ switch(curr_instr) {
+#endif
+/* Basic stack operations */
+
+ Instruct(ACC0){
+ print_instr("ACC0");
+ accu = sp[0]; Next;
+ }
+ Instruct(ACC1){
+ print_instr("ACC1");
+ accu = sp[1]; Next;
+ }
+ Instruct(ACC2){
+ print_instr("ACC2");
+ accu = sp[2]; Next;
+ }
+ Instruct(ACC3){
+ print_instr("ACC3");
+ accu = sp[3]; Next;
+ }
+ Instruct(ACC4){
+ print_instr("ACC4");
+ accu = sp[4]; Next;
+ }
+ Instruct(ACC5){
+ print_instr("ACC5");
+ accu = sp[5]; Next;
+ }
+ Instruct(ACC6){
+ print_instr("ACC6");
+ accu = sp[6]; Next;
+ }
+ Instruct(ACC7){
+ print_instr("ACC7");
+ accu = sp[7]; Next;
+ }
+ Instruct(PUSH){
+ print_instr("PUSH");
+ *--sp = accu; Next;
+ }
+ Instruct(PUSHACC0) {
+ print_instr("PUSHACC0");
+ *--sp = accu; Next;
+ }
+ Instruct(PUSHACC1){
+ print_instr("PUSHACC1");
+ *--sp = accu; accu = sp[1]; Next;
+ }
+ Instruct(PUSHACC2){
+ print_instr("PUSHACC2");
+ *--sp = accu; accu = sp[2]; Next;
+ }
+ Instruct(PUSHACC3){
+ print_instr("PUSHACC3");
+ *--sp = accu; accu = sp[3]; Next;
+ }
+ Instruct(PUSHACC4){
+ print_instr("PUSHACC4");
+ *--sp = accu; accu = sp[4]; Next;
+ }
+ Instruct(PUSHACC5){
+ print_instr("PUSHACC5");
+ *--sp = accu; accu = sp[5]; Next;
+ }
+ Instruct(PUSHACC6){
+ print_instr("PUSHACC5");
+ *--sp = accu; accu = sp[6]; Next;
+ }
+ Instruct(PUSHACC7){
+ print_instr("PUSHACC7");
+ *--sp = accu; accu = sp[7]; Next;
+ }
+ Instruct(PUSHACC){
+ print_instr("PUSHACC");
+ *--sp = accu;
+ }
+ /* Fallthrough */
+
+ Instruct(ACC){
+ print_instr("ACC");
+ accu = sp[*pc++];
+ Next;
+ }
+
+ Instruct(POP){
+ print_instr("POP");
+ sp += *pc++;
+ Next;
+ }
+ /* Access in heap-allocated environment */
+
+ Instruct(ENVACC1){
+ print_instr("ENVACC1");
+ accu = Field(coq_env, 1); Next;
+ }
+ Instruct(ENVACC2){
+ print_instr("ENVACC2");
+ accu = Field(coq_env, 2); Next;
+ }
+ Instruct(ENVACC3){
+ print_instr("ENVACC3");
+ accu = Field(coq_env, 3); Next;
+ }
+ Instruct(ENVACC4){
+ print_instr("ENVACC4");
+ accu = Field(coq_env, 4); Next;
+ }
+ Instruct(PUSHENVACC1){
+ print_instr("PUSHENVACC1");
+ *--sp = accu; accu = Field(coq_env, 1); Next;
+ }
+ Instruct(PUSHENVACC2){
+ print_instr("PUSHENVACC2");
+ *--sp = accu; accu = Field(coq_env, 2); Next;
+ }
+ Instruct(PUSHENVACC3){
+ print_instr("PUSHENVACC3");
+ *--sp = accu; accu = Field(coq_env, 3); Next;
+ }
+ Instruct(PUSHENVACC4){
+ print_instr("PUSHENVACC4");
+ *--sp = accu; accu = Field(coq_env, 4); Next;
+ }
+ Instruct(PUSHENVACC){
+ print_instr("PUSHENVACC");
+ *--sp = accu;
+ }
+ /* Fallthrough */
+ Instruct(ENVACC){
+ print_instr("ENVACC");
+ print_int(*pc);
+ accu = Field(coq_env, *pc++);
+ Next;
+ }
+ /* Function application */
+
+ Instruct(PUSH_RETADDR) {
+ print_instr("PUSH_RETADDR");
+ sp -= 3;
+ sp[0] = (value) (pc + *pc);
+ sp[1] = coq_env;
+ sp[2] = Val_long(coq_extra_args);
+ coq_extra_args = 0;
+ pc++;
+ Next;
+ }
+ Instruct(APPLY) {
+ print_instr("APPLY");
+ coq_extra_args = *pc - 1;
+ pc = Code_val(accu);
+ coq_env = accu;
+ goto check_stack;
+ }
+ Instruct(APPLY1) {
+ value arg1;
+ apply1:
+ print_instr("APPLY1");
+ arg1 = sp[0];
+ sp -= 3;
+ sp[0] = arg1;
+ sp[1] = (value)pc;
+ sp[2] = coq_env;
+ sp[3] = Val_long(coq_extra_args);
+ print_instr("call stack=");
+ print_lint(sp[1]);
+ print_lint(sp[2]);
+ print_lint(sp[3]);
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args = 0;
+ goto check_stack;
+ }
+
+ Instruct(APPLY2) {
+ value arg1;
+ value arg2;
+ apply2:
+ print_instr("APPLY2");
+ arg1 = sp[0];
+ arg2 = sp[1];
+ sp -= 3;
+ sp[0] = arg1;
+ sp[1] = arg2;
+ sp[2] = (value)pc;
+ sp[3] = coq_env;
+ sp[4] = Val_long(coq_extra_args);
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args = 1;
+ goto check_stack;
+ }
+
+ Instruct(APPLY3) {
+ value arg1;
+ value arg2;
+ value arg3;
+ apply3:
+ print_instr("APPLY3");
+ arg1 = sp[0];
+ arg2 = sp[1];
+ arg3 = sp[2];
+ sp -= 3;
+ sp[0] = arg1;
+ sp[1] = arg2;
+ sp[2] = arg3;
+ sp[3] = (value)pc;
+ sp[4] = coq_env;
+ sp[5] = Val_long(coq_extra_args);
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args = 2;
+ goto check_stack;
+ }
+
+ Instruct(APPLY4) {
+ value arg1 = sp[0];
+ value arg2 = sp[1];
+ value arg3 = sp[2];
+ value arg4 = sp[3];
+ print_instr("APPLY4");
+ sp -= 3;
+ sp[0] = arg1;
+ sp[1] = arg2;
+ sp[2] = arg3;
+ sp[3] = arg4;
+ sp[4] = (value)pc;
+ sp[5] = coq_env;
+ sp[6] = Val_long(coq_extra_args);
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args = 3;
+ goto check_stack;
+ }
+
+ /* Stack checks */
+
+ check_stack:
+ print_instr("check_stack");
+ CHECK_STACK(0);
+ /* We also check for signals */
+ if (caml_signals_are_pending) {
+ /* If there's a Ctrl-C, we reset the vm */
+ if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; }
+ caml_process_pending_signals();
+ }
+ Next;
+
+ Instruct(ENSURESTACKCAPACITY) {
+ print_instr("ENSURESTACKCAPACITY");
+ int size = *pc++;
+ /* CHECK_STACK may trigger here a useless allocation because of the
+ threshold, but check_stack: often does it anyway, so we prefer to
+ factorize the code. */
+ CHECK_STACK(size);
+ Next;
+ }
+
+ Instruct(APPTERM) {
+ int nargs = *pc++;
+ int slotsize = *pc;
+ value * newsp;
+ int i;
+ print_instr("APPTERM");
+ /* Slide the nargs bottom words of the current frame to the top
+ of the frame, and discard the remainder of the frame */
+ newsp = sp + slotsize - nargs;
+ for (i = nargs - 1; i >= 0; i--) newsp[i] = sp[i];
+ sp = newsp;
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args += nargs - 1;
+ goto check_stack;
+ }
+ Instruct(APPTERM1) {
+ value arg1 = sp[0];
+ print_instr("APPTERM1");
+ sp = sp + *pc - 1;
+ sp[0] = arg1;
+ pc = Code_val(accu);
+ coq_env = accu;
+ goto check_stack;
+ }
+ Instruct(APPTERM2) {
+ value arg1 = sp[0];
+ value arg2 = sp[1];
+ print_instr("APPTERM2");
+ sp = sp + *pc - 2;
+ sp[0] = arg1;
+ sp[1] = arg2;
+ pc = Code_val(accu);
+ print_lint(accu);
+ coq_env = accu;
+ coq_extra_args += 1;
+ goto check_stack;
+ }
+ Instruct(APPTERM3) {
+ value arg1 = sp[0];
+ value arg2 = sp[1];
+ value arg3 = sp[2];
+ print_instr("APPTERM3");
+ sp = sp + *pc - 3;
+ sp[0] = arg1;
+ sp[1] = arg2;
+ sp[2] = arg3;
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args += 2;
+ goto check_stack;
+ }
+
+ Instruct(RETURN) {
+ print_instr("RETURN");
+ print_int(*pc);
+ sp += *pc++;
+ print_instr("stack=");
+ print_lint(sp[0]);
+ print_lint(sp[1]);
+ print_lint(sp[2]);
+ if (coq_extra_args > 0) {
+ print_instr("extra args > 0");
+ print_lint(coq_extra_args);
+ coq_extra_args--;
+ pc = Code_val(accu);
+ coq_env = accu;
+ } else {
+ print_instr("extra args = 0");
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ }
+ Next;
+ }
+
+ Instruct(RESTART) {
+ int num_args = Wosize_val(coq_env) - 2;
+ int i;
+ print_instr("RESTART");
+ CHECK_STACK(num_args);
+ sp -= num_args;
+ for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2);
+ coq_env = Field(coq_env, 1);
+ coq_extra_args += num_args;
+ Next;
+ }
+
+ Instruct(GRAB) {
+ int required = *pc++;
+ print_instr("GRAB");
+ /* printf("GRAB %d\n",required); */
+ if (coq_extra_args >= required) {
+ coq_extra_args -= required;
+ } else {
+ mlsize_t num_args, i;
+ num_args = 1 + coq_extra_args; /* arg1 + extra args */
+ Alloc_small(accu, num_args + 2, Closure_tag);
+ Field(accu, 1) = coq_env;
+ for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+ Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
+ sp += num_args;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ }
+ Next;
+ }
+
+ Instruct(GRABREC) {
+ int rec_pos = *pc++; /* commence a zero */
+ print_instr("GRABREC");
+ if (rec_pos <= coq_extra_args && !Is_accu(sp[rec_pos])) {
+ pc++;/* On saute le Restart */
+ } else {
+ if (coq_extra_args < rec_pos) {
+ /* Partial application */
+ mlsize_t num_args, i;
+ num_args = 1 + coq_extra_args; /* arg1 + extra args */
+ Alloc_small(accu, num_args + 2, Closure_tag);
+ Field(accu, 1) = coq_env;
+ for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+ Code_val(accu) = pc - 3;
+ sp += num_args;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ } else {
+ /* The recursif argument is an accumulator */
+ mlsize_t num_args, i;
+ /* Construction of fixpoint applied to its [rec_pos-1] first arguments */
+ Alloc_small(accu, rec_pos + 2, Closure_tag);
+ Field(accu, 1) = coq_env; // We store the fixpoint in the first field
+ for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; // Storing args
+ Code_val(accu) = pc;
+ sp += rec_pos;
+ *--sp = accu;
+ /* Construction of the atom */
+ Alloc_small(accu, 2, ATOM_FIX_TAG);
+ Field(accu,1) = sp[0];
+ Field(accu,0) = sp[1];
+ sp++; sp[0] = accu;
+ /* Construction of the accumulator */
+ num_args = coq_extra_args - rec_pos;
+ Alloc_small(accu, 2+num_args, Accu_tag);
+ Code_val(accu) = accumulate;
+ Field(accu,1) = sp[0]; sp++;
+ for (i = 0; i < num_args;i++)Field(accu, i + 2) = sp[i];
+ sp += num_args;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ }
+ }
+ Next;
+ }
+
+ Instruct(CLOSURE) {
+ int nvars = *pc++;
+ int i;
+ print_instr("CLOSURE");
+ print_int(nvars);
+ if (nvars > 0) *--sp = accu;
+ Alloc_small(accu, 1 + nvars, Closure_tag);
+ Code_val(accu) = pc + *pc;
+ pc++;
+ for (i = 0; i < nvars; i++) {
+ print_lint(sp[i]);
+ Field(accu, i + 1) = sp[i];
+ }
+ sp += nvars;
+ Next;
+ }
+
+ Instruct(CLOSUREREC) {
+ int nfuncs = *pc++;
+ int nvars = *pc++;
+ int start = *pc++;
+ int i;
+ value * p;
+ print_instr("CLOSUREREC");
+ if (nvars > 0) *--sp = accu;
+ /* construction du vecteur de type */
+ Alloc_small(accu, nfuncs, Abstract_tag);
+ for(i = 0; i < nfuncs; i++) {
+ Field(accu,i) = (value)(pc+pc[i]);
+ }
+ pc += nfuncs;
+ *--sp=accu;
+ Alloc_small(accu, nfuncs * 2 + nvars, Closure_tag);
+ Field(accu, nfuncs * 2 + nvars - 1) = *sp++;
+ /* On remplie la partie pour les variables libres */
+ p = &Field(accu, nfuncs * 2 - 1);
+ for (i = 0; i < nvars; i++) {
+ *p++ = *sp++;
+ }
+ p = &Field(accu, 0);
+ *p = (value) (pc + pc[0]);
+ p++;
+ for (i = 1; i < nfuncs; i++) {
+ *p = Make_header(i * 2, Infix_tag, Caml_white);
+ p++; /* color irrelevant. */
+ *p = (value) (pc + pc[i]);
+ p++;
+ }
+ pc += nfuncs;
+ accu = accu + 2 * start * sizeof(value);
+ Next;
+ }
+
+ Instruct(CLOSURECOFIX){
+ int nfunc = *pc++;
+ int nvars = *pc++;
+ int start = *pc++;
+ int i, j , size;
+ value * p;
+ print_instr("CLOSURECOFIX");
+ if (nvars > 0) *--sp = accu;
+ /* construction du vecteur de type */
+ Alloc_small(accu, nfunc, Abstract_tag);
+ for(i = 0; i < nfunc; i++) {
+ Field(accu,i) = (value)(pc+pc[i]);
+ }
+ pc += nfunc;
+ *--sp=accu;
+
+ /* Creation des blocks accumulate */
+ for(i=0; i < nfunc; i++) {
+ Alloc_small(accu, 2, Accu_tag);
+ Code_val(accu) = accumulate;
+ Field(accu,1) = Val_int(1);
+ *--sp=accu;
+ }
+ /* creation des fonction cofix */
+
+ p = sp;
+ size = nfunc + nvars + 2;
+ for (i=0; i < nfunc; i++) {
+
+ Alloc_small(accu, size, Closure_tag);
+ Code_val(accu) = pc+pc[i];
+ for (j = 0; j < nfunc; j++) Field(accu, j+1) = p[j];
+ Field(accu, size - 1) = p[nfunc];
+ for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = p[j];
+ *--sp = accu;
+ /* creation du block contenant le cofix */
+
+ Alloc_small(accu,1, ATOM_COFIX_TAG);
+ Field(accu, 0) = sp[0];
+ *sp = accu;
+ /* mise a jour du block accumulate */
+ caml_modify(&Field(p[i], 1),*sp);
+ sp++;
+ }
+ pc += nfunc;
+ accu = p[start];
+ sp = p + nfunc + 1 + nvars;
+ print_instr("ici4");
+ Next;
+ }
+
+
+ Instruct(PUSHOFFSETCLOSURE) {
+ print_instr("PUSHOFFSETCLOSURE");
+ *--sp = accu;
+ } /* fallthrough */
+ Instruct(OFFSETCLOSURE) {
+ print_instr("OFFSETCLOSURE");
+ accu = coq_env + *pc++ * sizeof(value); Next;
+ }
+ Instruct(PUSHOFFSETCLOSUREM2) {
+ print_instr("PUSHOFFSETCLOSUREM2");
+ *--sp = accu;
+ } /* fallthrough */
+ Instruct(OFFSETCLOSUREM2) {
+ print_instr("OFFSETCLOSUREM2");
+ accu = coq_env - 2 * sizeof(value); Next;
+ }
+ Instruct(PUSHOFFSETCLOSURE0) {
+ print_instr("PUSHOFFSETCLOSURE0");
+ *--sp = accu;
+ }/* fallthrough */
+ Instruct(OFFSETCLOSURE0) {
+ print_instr("OFFSETCLOSURE0");
+ accu = coq_env; Next;
+ }
+ Instruct(PUSHOFFSETCLOSURE2){
+ print_instr("PUSHOFFSETCLOSURE2");
+ *--sp = accu; /* fallthrough */
+ }
+ Instruct(OFFSETCLOSURE2) {
+ print_instr("OFFSETCLOSURE2");
+ accu = coq_env + 2 * sizeof(value); Next;
+ }
+
+/* Access to global variables */
+
+ Instruct(PUSHGETGLOBAL) {
+ print_instr("PUSH");
+ *--sp = accu;
+ }
+ /* Fallthrough */
+ Instruct(GETGLOBAL){
+ print_instr("GETGLOBAL");
+ print_int(*pc);
+ accu = Field(coq_global_data, *pc);
+ pc++;
+ Next;
+ }
+
+/* Allocation of blocks */
+
+ Instruct(MAKEBLOCK) {
+ mlsize_t wosize = *pc++;
+ tag_t tag = *pc++;
+ mlsize_t i;
+ value block;
+ print_instr("MAKEBLOCK, tag=");
+ Alloc_small(block, wosize, tag);
+ Field(block, 0) = accu;
+ for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
+ accu = block;
+ Next;
+ }
+ Instruct(MAKEBLOCK1) {
+
+ tag_t tag = *pc++;
+ value block;
+ print_instr("MAKEBLOCK1, tag=");
+ print_int(tag);
+ Alloc_small(block, 1, tag);
+ Field(block, 0) = accu;
+ accu = block;
+ Next;
+ }
+ Instruct(MAKEBLOCK2) {
+
+ tag_t tag = *pc++;
+ value block;
+ print_instr("MAKEBLOCK2, tag=");
+ print_int(tag);
+ Alloc_small(block, 2, tag);
+ Field(block, 0) = accu;
+ Field(block, 1) = sp[0];
+ sp += 1;
+ accu = block;
+ Next;
+ }
+ Instruct(MAKEBLOCK3) {
+ tag_t tag = *pc++;
+ value block;
+ print_instr("MAKEBLOCK3, tag=");
+ print_int(tag);
+ Alloc_small(block, 3, tag);
+ Field(block, 0) = accu;
+ Field(block, 1) = sp[0];
+ Field(block, 2) = sp[1];
+ sp += 2;
+ accu = block;
+ Next;
+ }
+ Instruct(MAKEBLOCK4) {
+ tag_t tag = *pc++;
+ value block;
+ print_instr("MAKEBLOCK4, tag=");
+ print_int(tag);
+ Alloc_small(block, 4, tag);
+ Field(block, 0) = accu;
+ Field(block, 1) = sp[0];
+ Field(block, 2) = sp[1];
+ Field(block, 3) = sp[2];
+ sp += 3;
+ accu = block;
+ Next;
+ }
+
+
+/* Access to components of blocks */
+
+ Instruct(SWITCH) {
+ uint32_t sizes = *pc++;
+ print_instr("SWITCH");
+ print_int(sizes & 0xFFFFFF);
+ if (Is_block(accu)) {
+ long index = Tag_val(accu);
+ print_instr("block");
+ print_lint(index);
+ pc += pc[(sizes & 0xFFFFFF) + index];
+ } else {
+ long index = Long_val(accu);
+ print_instr("constant");
+ print_lint(index);
+ pc += pc[index];
+ }
+ Next;
+ }
+
+ Instruct(PUSHFIELDS){
+ int i;
+ int size = *pc++;
+ print_instr("PUSHFIELDS");
+ sp -= size;
+ for(i=0;i<size;i++)sp[i] = Field(accu,i);
+ Next;
+ }
+
+ Instruct(GETFIELD0){
+ print_instr("GETFIELD0");
+ accu = Field(accu, 0);
+ Next;
+ }
+
+ Instruct(GETFIELD1){
+ print_instr("GETFIELD1");
+ accu = Field(accu, 1);
+ Next;
+ }
+
+ Instruct(GETFIELD){
+ print_instr("GETFIELD");
+ accu = Field(accu, *pc);
+ pc++;
+ Next;
+ }
+
+ Instruct(SETFIELD0){
+ print_instr("SETFIELD0");
+ caml_modify(&Field(accu, 0),*sp);
+ sp++;
+ Next;
+ }
+
+ Instruct(SETFIELD1){
+ print_instr("SETFIELD1");
+ caml_modify(&Field(accu, 1),*sp);
+ sp++;
+ Next;
+ }
+
+ Instruct(SETFIELD){
+ print_instr("SETFIELD");
+ caml_modify(&Field(accu, *pc),*sp);
+ sp++; pc++;
+ Next;
+ }
+
+
+ Instruct(PROJ){
+ do_proj:
+ print_instr("PROJ");
+ if (Is_accu (accu)) {
+ *--sp = accu; // Save matched block on stack
+ accu = Field(accu, 1); // Save atom to accu register
+ switch (Tag_val(accu)) {
+ case ATOM_COFIX_TAG: // We are forcing a cofix
+ {
+ mlsize_t i, nargs;
+ sp -= 2;
+ // Push the current instruction as the return address
+ sp[0] = (value)(pc - 1);
+ sp[1] = coq_env;
+ coq_env = Field(accu, 0); // Pointer to suspension
+ accu = sp[2]; // Save accumulator to accu register
+ sp[2] = Val_long(coq_extra_args); // Push number of args for return
+ nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom)
+ // Push arguments to stack
+ CHECK_STACK(nargs + 1);
+ sp -= nargs;
+ for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 2);
+ *--sp = accu; // Last argument is the pointer to the suspension
+ coq_extra_args = nargs;
+ pc = Code_val(coq_env); // Trigger evaluation
+ goto check_stack;
+ }
+ case ATOM_COFIXEVALUATED_TAG:
+ {
+ accu = Field(accu, 1);
+ ++sp;
+ goto do_proj;
+ }
+ default:
+ {
+ value block;
+ /* Skip over the index of projected field */
+ ++pc;
+ /* Create atom */
+ Alloc_small(accu, 2, ATOM_PROJ_TAG);
+ Field(accu, 0) = Field(coq_global_data, *pc++);
+ Field(accu, 1) = *sp++;
+ /* Create accumulator */
+ Alloc_small(block, 2, Accu_tag);
+ Code_val(block) = accumulate;
+ Field(block, 1) = accu;
+ accu = block;
+ }
+ }
+ } else {
+ accu = Field(accu, *pc);
+ pc += 2;
+ }
+ Next;
+ }
+
+/* Integer constants */
+
+ Instruct(CONST0){
+ print_instr("CONST0");
+ accu = Val_int(0); Next;}
+ Instruct(CONST1){
+ print_instr("CONST1");
+ accu = Val_int(1); Next;}
+ Instruct(CONST2){
+ print_instr("CONST2");
+ accu = Val_int(2); Next;}
+ Instruct(CONST3){
+ print_instr("CONST3");
+ accu = Val_int(3); Next;}
+
+ Instruct(PUSHCONST0){
+ print_instr("PUSHCONST0");
+ *--sp = accu; accu = Val_int(0); Next;
+ }
+ Instruct(PUSHCONST1){
+ print_instr("PUSHCONST1");
+ *--sp = accu; accu = Val_int(1); Next;
+ }
+ Instruct(PUSHCONST2){
+ print_instr("PUSHCONST2");
+ *--sp = accu; accu = Val_int(2); Next;
+ }
+ Instruct(PUSHCONST3){
+ print_instr("PUSHCONST3");
+ *--sp = accu; accu = Val_int(3); Next;
+ }
+
+ Instruct(PUSHCONSTINT){
+ print_instr("PUSHCONSTINT");
+ *--sp = accu;
+ }
+ /* Fallthrough */
+ Instruct(CONSTINT) {
+ print_instr("CONSTINT");
+ print_int(*pc);
+ accu = Val_int(*pc);
+ pc++;
+ Next;
+ }
+
+ /* Special operations for reduction of open term */
+ Instruct(ACCUMULATE) {
+ mlsize_t i, size;
+ print_instr("ACCUMULATE");
+ size = Wosize_val(coq_env);
+ Alloc_small(accu, size + coq_extra_args + 1, Accu_tag);
+ for(i = 0; i < size; i++) Field(accu, i) = Field(coq_env, i);
+ for(i = size; i <= coq_extra_args + size; i++)
+ Field(accu, i) = *sp++;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ Next;
+ }
+ Instruct(MAKESWITCHBLOCK) {
+ print_instr("MAKESWITCHBLOCK");
+ *--sp = accu; // Save matched block on stack
+ accu = Field(accu,1); // Save atom to accu register
+ switch (Tag_val(accu)) {
+ case ATOM_COFIX_TAG: // We are forcing a cofix
+ {
+ mlsize_t i, nargs;
+ print_instr("COFIX_TAG");
+ sp-=2;
+ pc++;
+ // Push the return address
+ sp[0] = (value) (pc + *pc);
+ sp[1] = coq_env;
+ coq_env = Field(accu,0); // Pointer to suspension
+ accu = sp[2]; // Save accumulator to accu register
+ sp[2] = Val_long(coq_extra_args); // Push number of args for return
+ nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom)
+ // Push arguments to stack
+ CHECK_STACK(nargs+1);
+ sp -= nargs;
+ for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
+ *--sp = accu; // Leftmost argument is the pointer to the suspension
+ print_lint(nargs);
+ coq_extra_args = nargs;
+ pc = Code_val(coq_env); // Trigger evaluation
+ goto check_stack;
+ }
+ case ATOM_COFIXEVALUATED_TAG:
+ {
+ print_instr("COFIX_EVAL_TAG");
+ accu = Field(accu,1);
+ pc++;
+ pc = pc + *pc;
+ sp++;
+ Next;
+ }
+ default:
+ {
+ mlsize_t sz;
+ int i, annot;
+ code_t typlbl,swlbl;
+ print_instr("MAKESWITCHBLOCK");
+
+ typlbl = (code_t)pc + *pc;
+ pc++;
+ swlbl = (code_t)pc + *pc;
+ pc++;
+ annot = *pc++;
+ sz = *pc++;
+ *--sp=Field(coq_global_data, annot);
+ /* We save the stack */
+ if (sz == 0) accu = Atom(0);
+ else {
+ Alloc_small(accu, sz, Default_tag);
+ if (Field(*sp, 2) == Val_true) {
+ for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2];
+ }else{
+ for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5];
+ }
+ }
+ *--sp = accu;
+ /* Create bytecode wrappers */
+ Alloc_small(accu, 1, Abstract_tag);
+ Code_val(accu) = typlbl;
+ *--sp = accu;
+ Alloc_small(accu, 1, Abstract_tag);
+ Code_val(accu) = swlbl;
+ *--sp = accu;
+ /* We create the switch zipper */
+ Alloc_small(accu, 5, Default_tag);
+ Field(accu, 0) = sp[1];
+ Field(accu, 1) = sp[0];
+ Field(accu, 2) = sp[3];
+ Field(accu, 3) = sp[2];
+ Field(accu, 4) = coq_env;
+ sp += 3;
+ sp[0] = accu;
+ /* We create the atom */
+ Alloc_small(accu, 2, ATOM_SWITCH_TAG);
+ Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0];
+ sp++;sp[0] = accu;
+ /* We create the accumulator */
+ Alloc_small(accu, 2, Accu_tag);
+ Code_val(accu) = accumulate;
+ Field(accu,1) = *sp++;
+ }
+ }
+ Next;
+ }
+
+
+
+ Instruct(MAKEACCU) {
+ int i;
+ print_instr("MAKEACCU");
+ Alloc_small(accu, coq_extra_args + 3, Accu_tag);
+ Code_val(accu) = accumulate;
+ Field(accu,1) = Field(coq_atom_tbl, *pc);
+ for(i = 2; i < coq_extra_args + 3; i++) Field(accu, i) = *sp++;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ Next;
+ }
+
+ Instruct(MAKEPROD) {
+ print_instr("MAKEPROD");
+ *--sp=accu;
+ Alloc_small(accu,2,0);
+ Field(accu, 0) = sp[0];
+ Field(accu, 1) = sp[1];
+ sp += 2;
+ Next;
+ }
+
+ Instruct(BRANCH) {
+ /* unconditional branching */
+ print_instr("BRANCH");
+ pc += *pc;
+ /* pc = (code_t)(pc+*pc); */
+ Next;
+ }
+
+ Instruct(CHECKADDINT63){
+ print_instr("CHECKADDINT63");
+ CheckInt2();
+ }
+ Instruct(ADDINT63) {
+ /* Adds the integer in the accumulator with
+ the one ontop of the stack (which is poped)*/
+ print_instr("ADDINT63");
+ accu = uint63_add(accu, *sp++);
+ Next;
+ }
+
+ Instruct (CHECKADDCINT63) {
+ print_instr("CHECKADDCINT63");
+ CheckInt2();
+ /* returns the sum with a carry */
+ value s;
+ s = uint63_add(accu, *sp++);
+ AllocCarry(uint63_lt(s,accu));
+ Field(accu, 0) = s;
+ Next;
+ }
+
+ Instruct (CHECKADDCARRYCINT63) {
+ print_instr("ADDCARRYCINT63");
+ CheckInt2();
+ /* returns the sum plus one with a carry */
+ value s;
+ s = uint63_addcarry(accu, *sp++);
+ AllocCarry(uint63_leq(s, accu));
+ Field(accu, 0) = s;
+ Next;
+ }
+
+ Instruct (CHECKSUBINT63) {
+ print_instr("CHECKSUBINT63");
+ CheckInt2();
+ }
+ Instruct (SUBINT63) {
+ print_instr("SUBINT63");
+ /* returns the subtraction */
+ accu = uint63_sub(accu, *sp++);
+ Next;
+ }
+
+ Instruct (CHECKSUBCINT63) {
+ print_instr("SUBCINT63");
+ CheckInt2();
+ /* returns the subtraction with a carry */
+ value b;
+ value s;
+ b = *sp++;
+ s = uint63_sub(accu,b);
+ AllocCarry(uint63_lt(accu,b));
+ Field(accu, 0) = s;
+ Next;
+ }
+
+ Instruct (CHECKSUBCARRYCINT63) {
+ print_instr("SUBCARRYCINT63");
+ CheckInt2();
+ /* returns the subtraction minus one with a carry */
+ value b;
+ value s;
+ b = *sp++;
+ s = uint63_subcarry(accu,b);
+ AllocCarry(uint63_leq(accu,b));
+ Field(accu, 0) = s;
+ Next;
+ }
+
+ Instruct (CHECKMULINT63) {
+ print_instr("MULINT63");
+ CheckInt2();
+ /* returns the multiplication */
+ accu = uint63_mul(accu,*sp++);
+ Next;
+ }
+
+ Instruct (CHECKMULCINT63) {
+ /*returns the multiplication on a pair */
+ print_instr("MULCINT63");
+ CheckInt2();
+ /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */
+ /* TODO: implement
+ p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1));
+ AllocPair(); */
+ /* Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; */ /*higher part*/
+ /* Field(accu, 1) = (value)(I64_to_int32(p)|1); */ /*lower part*/
+ value x = accu;
+ AllocPair();
+ Field(accu, 1) = uint63_mulc(x, *sp++, &Field(accu, 0));
+ Next;
+ }
+
+ Instruct(CHECKDIVINT63) {
+ print_instr("CHEKDIVINT63");
+ CheckInt2();
+ /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag
+ since it probably only concerns negative number.
+ needs to be checked at this point */
+ value divisor;
+ divisor = *sp++;
+ if (uint63_eq0(divisor)) {
+ accu = divisor;
+ }
+ else {
+ accu = uint63_div(accu, divisor);
+ }
+ Next;
+ }
+
+ Instruct(CHECKMODINT63) {
+ print_instr("CHEKMODINT63");
+ CheckInt2();
+ value divisor;
+ divisor = *sp++;
+ if (uint63_eq0(divisor)) {
+ accu = divisor;
+ }
+ else {
+ accu = uint63_mod(accu,divisor);
+ }
+ Next;
+ }
+
+ Instruct (CHECKDIVEUCLINT63) {
+ print_instr("DIVEUCLINT63");
+ CheckInt2();
+ /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag
+ since it probably only concerns negative number.
+ needs to be checked at this point */
+ value divisor;
+ divisor = *sp++;
+ if (uint63_eq0(divisor)) {
+ Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
+ Field(accu, 0) = divisor;
+ Field(accu, 1) = divisor;
+ }
+ else {
+ value modulus;
+ modulus = accu;
+ Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
+ Field(accu, 0) = uint63_div(modulus,divisor);
+ Field(accu, 1) = uint63_mod(modulus,divisor);
+ }
+ Next;
+ }
+
+ Instruct (CHECKDIV21INT63) {
+ print_instr("DIV21INT63");
+ CheckInt3();
+ /* spiwack: takes three int31 (the two first ones represent an
+ int62) and performs the euclidian division of the
+ int62 by the int31 */
+ /* TODO: implement this
+ bigint = UI64_of_value(accu);
+ bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++));
+ uint64 divisor;
+ divisor = UI64_of_value(*sp++);
+ Alloc_small(accu, 2, 1); */ /* ( _ , arity, tag ) */
+ /* if (I64_is_zero (divisor)) {
+ Field(accu, 0) = 1; */ /* 2*0+1 */
+ /* Field(accu, 1) = 1; */ /* 2*0+1 */
+ /* }
+ else {
+ uint64 quo, mod;
+ I64_udivmod(bigint, divisor, &quo, &mod);
+ Field(accu, 0) = value_of_uint32(I64_to_int32(quo));
+ Field(accu, 1) = value_of_uint32(I64_to_int32(mod));
+ } */
+ value bigint; /* TODO: fix */
+ bigint = *sp++; /* TODO: take accu into account */
+ value divisor;
+ divisor = *sp++;
+ if (uint63_eq0(divisor)) {
+ Alloc_small(accu, 2, 1);
+ Field(accu, 0) = divisor;
+ Field(accu, 1) = divisor;
+ }
+ else {
+ value quo, mod;
+ mod = uint63_div21(accu, bigint, divisor, &quo);
+ Alloc_small(accu, 2, 1);
+ Field(accu, 0) = quo;
+ Field(accu, 1) = mod;
+ }
+ Next;
+ }
+
+ Instruct(CHECKLXORINT63) {
+ print_instr("CHECKLXORINT63");
+ CheckInt2();
+ accu = uint63_lxor(accu,*sp++);
+ Next;
+ }
+
+ Instruct(CHECKLORINT63) {
+ print_instr("CHECKLORINT63");
+ CheckInt2();
+ accu = uint63_lor(accu,*sp++);
+ Next;
+ }
+
+ Instruct(CHECKLANDINT63) {
+ print_instr("CHECKLANDINT63");
+ CheckInt2();
+ accu = uint63_land(accu,*sp++);
+ Next;
+ }
+
+ Instruct(CHECKLSLINT63) {
+ print_instr("CHECKLSLINT63");
+ CheckInt2();
+ value p = *sp++;
+ accu = uint63_lsl(accu,p);
+ Next;
+ }
+
+ Instruct(CHECKLSRINT63) {
+ print_instr("CHECKLSRINT63");
+ CheckInt2();
+ value p = *sp++;
+ accu = uint63_lsr(accu,p);
+ Next;
+ }
+
+ Instruct(CHECKLSLINT63CONST1) {
+ print_instr("CHECKLSLINT63CONST1");
+ if (Is_uint63(accu)) {
+ pc++;
+ accu = uint63_lsl1(accu);
+ Next;
+ } else {
+ *--sp = uint63_one();
+ *--sp = accu;
+ accu = Field(coq_global_data, *pc++);
+ goto apply2;
+ }
+ }
+
+ Instruct(CHECKLSRINT63CONST1) {
+ print_instr("CHECKLSRINT63CONST1");
+ if (Is_uint63(accu)) {
+ pc++;
+ accu = uint63_lsr1(accu);
+ Next;
+ } else {
+ *--sp = uint63_one();
+ *--sp = accu;
+ accu = Field(coq_global_data, *pc++);
+ goto apply2;
+ }
+ }
+
+ Instruct (CHECKADDMULDIVINT63) {
+ print_instr("CHECKADDMULDIVINT63");
+ CheckInt3();
+ value x;
+ value y;
+ x = *sp++;
+ y = *sp++;
+ accu = uint63_addmuldiv(accu,x,y);
+ Next;
+ }
+
+ Instruct (CHECKEQINT63) {
+ print_instr("CHECKEQINT63");
+ CheckInt2();
+ accu = uint63_eq(accu,*sp++) ? coq_true : coq_false;
+ Next;
+ }
+
+ Instruct (CHECKLTINT63) {
+ print_instr("CHECKLTINT63");
+ CheckInt2();
+ }
+ Instruct (LTINT63) {
+ print_instr("LTINT63");
+ accu = uint63_lt(accu,*sp++) ? coq_true : coq_false;
+ Next;
+ }
+
+ Instruct (CHECKLEINT63) {
+ print_instr("CHECKLEINT63");
+ CheckInt2();
+ }
+ Instruct (LEINT63) {
+ print_instr("LEINT63");
+ accu = uint63_leq(accu,*sp++) ? coq_true : coq_false;
+ Next;
+ }
+
+ Instruct (CHECKCOMPAREINT63) {
+ /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
+ /* assumes Inductive _ : _ := Eq | Lt | Gt */
+ print_instr("CHECKCOMPAREINT63");
+ CheckInt2();
+ if (uint63_eq(accu,*sp)) {
+ accu = coq_Eq;
+ sp++;
+ }
+ else accu = uint63_lt(accu,*sp++) ? coq_Lt : coq_Gt;
+ Next;
+ }
+
+ Instruct (CHECKHEAD0INT63) {
+ print_instr("CHECKHEAD0INT63");
+ CheckInt1();
+ accu = uint63_head0(accu);
+ Next;
+ }
+
+ Instruct (CHECKTAIL0INT63) {
+ print_instr("CHECKTAIL0INT63");
+ CheckInt1();
+ accu = uint63_tail0(accu);
+ Next;
+ }
+
+ Instruct (ISINT){
+ print_instr("ISINT");
+ accu = (Is_uint63(accu)) ? coq_true : coq_false;
+ Next;
+ }
+
+ Instruct (AREINT2){
+ print_instr("AREINT2");
+ accu = (Is_uint63(accu) && Is_uint63(sp[0])) ? coq_true : coq_false;
+ sp++;
+ Next;
+ }
+
+
+/* Debugging and machine control */
+
+ Instruct(STOP){
+ print_instr("STOP");
+ coq_sp = sp;
+ CAMLreturn(accu);
+ }
+
+
+#ifndef THREADED_CODE
+ default:
+ /*fprintf(stderr, "%d\n", *pc);*/
+ failwith("Coq VM: Fatal error: bad opcode");
+ }
+ }
+#endif
+}
+
+value coq_push_ra(value code) {
+ code_t tcode = Code_val(code);
+ print_instr("push_ra");
+ coq_sp -= 3;
+ coq_sp[0] = (value) tcode;
+ coq_sp[1] = Val_unit;
+ coq_sp[2] = Val_long(0);
+ return Val_unit;
+}
+
+value coq_push_val(value v) {
+ print_instr("push_val");
+ *--coq_sp = v;
+ return Val_unit;
+}
+
+value coq_push_arguments(value args) {
+ int nargs,i;
+ value * sp = coq_sp;
+ nargs = Wosize_val(args) - 2;
+ CHECK_STACK(nargs);
+ coq_sp -= nargs;
+ print_instr("push_args");print_int(nargs);
+ for(i = 0; i < nargs; i++) coq_sp[i] = Field(args, i+2);
+ return Val_unit;
+}
+
+value coq_push_vstack(value stk, value max_stack_size) {
+ int len,i;
+ value * sp = coq_sp;
+ len = Wosize_val(stk);
+ CHECK_STACK(len);
+ coq_sp -= len;
+ print_instr("push_vstack");print_int(len);
+ for(i = 0; i < len; i++) coq_sp[i] = Field(stk,i);
+ sp = coq_sp;
+ CHECK_STACK(uint32_of_value(max_stack_size));
+ return Val_unit;
+}
+
+value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea) {
+ // Registering the other arguments w.r.t. the OCaml GC is done by coq_interprete
+ CAMLparam1(tcode);
+ print_instr("coq_interprete");
+ CAMLreturn (coq_interprete(Code_val(tcode), a, t, g, e, Long_val(ea)));
+ print_instr("end coq_interprete");
+}
+
+value coq_interprete_byte(value* argv, int argn){
+ return coq_interprete_ml(argv[0], argv[1], argv[2], argv[3], argv[4], argv[5]);
+}
+
+value coq_eval_tcode (value tcode, value t, value g, value e) {
+ return coq_interprete_ml(tcode, Val_unit, t, g, e, 0);
+}
diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h
new file mode 100644
index 0000000000..c04e9e00b2
--- /dev/null
+++ b/kernel/byterun/coq_interp.h
@@ -0,0 +1,26 @@
+/***********************************************************************/
+/* */
+/* Coq Compiler */
+/* */
+/* Benjamin Gregoire, projets Logical and Cristal */
+/* INRIA Rocquencourt */
+/* */
+/* */
+/***********************************************************************/
+
+
+value coq_push_ra(value tcode);
+
+value coq_push_val(value v);
+
+value coq_push_arguments(value args);
+
+value coq_push_vstack(value stk);
+
+value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea);
+value coq_interprete_byte(value* argv, int argn);
+
+value coq_interprete
+ (code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args);
+
+value coq_eval_tcode (value tcode, value t, value g, value e);
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
new file mode 100644
index 0000000000..542a05fd25
--- /dev/null
+++ b/kernel/byterun/coq_memory.c
@@ -0,0 +1,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;
+}
+
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
new file mode 100644
index 0000000000..9375b15de2
--- /dev/null
+++ b/kernel/byterun/coq_memory.h
@@ -0,0 +1,58 @@
+/***********************************************************************/
+/* */
+/* Coq Compiler */
+/* */
+/* Benjamin Gregoire, projets Logical and Cristal */
+/* INRIA Rocquencourt */
+/* */
+/* */
+/***********************************************************************/
+
+#ifndef _COQ_MEMORY_
+#define _COQ_MEMORY_
+
+#include <caml/config.h>
+#include <caml/fail.h>
+#include <caml/misc.h>
+#include <caml/memory.h>
+#include <caml/mlvalues.h>
+
+
+#define Coq_stack_size (4096 * sizeof(value))
+#define Coq_stack_threshold (256 * sizeof(value))
+#define Coq_max_stack_size (256 * 1024)
+
+#define TRANSP 0
+#define BOXED 1
+
+/* stack */
+
+extern value * coq_stack_low;
+extern value * coq_stack_high;
+extern value * coq_stack_threshold;
+
+/* global_data */
+
+extern int coq_all_transp;
+
+extern int drawinstr;
+/* interp state */
+
+extern value * coq_sp;
+/* Some predefined pointer code */
+extern code_t accumulate;
+
+/* functions over global environment */
+
+value coq_static_alloc(value size); /* ML */
+
+value init_coq_vm(value unit); /* ML */
+value re_init_coq_vm(value unit); /* ML */
+
+void realloc_coq_stack(asize_t required_space);
+value coq_set_transp_value(value transp); /* ML */
+value get_coq_transp_value(value unit); /* ML */
+#endif /* _COQ_MEMORY_ */
+
+
+value coq_set_drawinstr(value unit);
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
new file mode 100644
index 0000000000..5499f124a2
--- /dev/null
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -0,0 +1,97 @@
+# pragma once
+
+# include <caml/callback.h>
+# include <caml/stack.h>
+
+
+#define Is_uint63(v) (Tag_val(v) == Custom_tag)
+
+# define DECLARE_NULLOP(name) \
+value uint63_##name() { \
+ static value* cb = 0; \
+ CAMLparam0(); \
+ if (!cb) cb = caml_named_value("uint63 " #name); \
+ CAMLreturn(*cb); \
+ }
+
+# define DECLARE_UNOP(name) \
+value uint63_##name(value x) { \
+ static value* cb = 0; \
+ CAMLparam1(x); \
+ if (!cb) cb = caml_named_value("uint63 " #name); \
+ CAMLreturn(caml_callback(*cb, x)); \
+ }
+
+# define DECLARE_PREDICATE(name) \
+value uint63_##name(value x) { \
+ static value* cb = 0; \
+ CAMLparam1(x); \
+ if (!cb) cb = caml_named_value("uint63 " #name); \
+ CAMLreturn(Int_val(caml_callback(*cb, x))); \
+ }
+
+# define DECLARE_BINOP(name) \
+value uint63_##name(value x, value y) { \
+ static value* cb = 0; \
+ CAMLparam2(x, y); \
+ if (!cb) cb = caml_named_value("uint63 " #name); \
+ CAMLreturn(caml_callback2(*cb, x, y)); \
+ }
+
+# define DECLARE_RELATION(name) \
+value uint63_##name(value x, value y) { \
+ static value* cb = 0; \
+ CAMLparam2(x, y); \
+ if (!cb) cb = caml_named_value("uint63 " #name); \
+ CAMLreturn(Int_val(caml_callback2(*cb, x, y))); \
+ }
+
+# define DECLARE_TEROP(name) \
+value uint63_##name(value x, value y, value z) { \
+ static value* cb = 0; \
+ CAMLparam3(x, y, z); \
+ if (!cb) cb = caml_named_value("uint63 " #name); \
+ CAMLreturn(caml_callback3(*cb, x, y, z)); \
+ }
+
+
+DECLARE_NULLOP(one)
+DECLARE_BINOP(add)
+DECLARE_BINOP(addcarry)
+DECLARE_TEROP(addmuldiv)
+DECLARE_BINOP(div)
+DECLARE_TEROP(div21_ml)
+DECLARE_RELATION(eq)
+DECLARE_PREDICATE(eq0)
+DECLARE_UNOP(head0)
+DECLARE_BINOP(land)
+DECLARE_RELATION(leq)
+DECLARE_BINOP(lor)
+DECLARE_BINOP(lsl)
+DECLARE_UNOP(lsl1)
+DECLARE_BINOP(lsr)
+DECLARE_UNOP(lsr1)
+DECLARE_RELATION(lt)
+DECLARE_BINOP(lxor)
+DECLARE_BINOP(mod)
+DECLARE_BINOP(mul)
+DECLARE_BINOP(mulc_ml)
+DECLARE_BINOP(sub)
+DECLARE_BINOP(subcarry)
+DECLARE_UNOP(tail0)
+
+value uint63_div21(value x, value y, value z, value* q) {
+ CAMLparam3(x, y, z);
+ CAMLlocal1(qr);
+ qr = uint63_div21_ml(x, y, z);
+ *q = Field(qr, 0);
+ CAMLreturn(Field(qr, 1));
+}
+
+value uint63_mulc(value x, value y, value* h) {
+ CAMLparam2(x, y);
+ CAMLlocal1(hl);
+ hl = uint63_mulc_ml(x, y);
+ *h = Field(hl, 0);
+ CAMLreturn(Field(hl, 1));
+}
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
new file mode 100644
index 0000000000..92f4dc79bc
--- /dev/null
+++ b/kernel/byterun/coq_uint63_native.h
@@ -0,0 +1,125 @@
+#define Is_uint63(v) (Is_long(v))
+
+#define uint63_of_value(val) ((uint64_t)(val) >> 1)
+
+/* 2^63 * y + x as a value */
+//#define Val_intint(x,y) ((value)(((uint64_t)(x)) << 1 + ((uint64_t)(y) << 64)))
+
+#define uint63_zero ((value) 1) /* 2*0 + 1 */
+#define uint63_one() ((value) 3) /* 2*1 + 1 */
+
+#define uint63_eq(x,y) ((x) == (y))
+#define uint63_eq0(x) ((x) == (uint64_t)1)
+#define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y))
+#define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y))
+
+#define uint63_add(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) - 1))
+#define uint63_addcarry(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) + 1))
+#define uint63_sub(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) + 1))
+#define uint63_subcarry(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) - 1))
+#define uint63_mul(x,y) (Val_long(uint63_of_value(x) * uint63_of_value(y)))
+#define uint63_div(x,y) (Val_long(uint63_of_value(x) / uint63_of_value(y)))
+#define uint63_mod(x,y) (Val_long(uint63_of_value(x) % uint63_of_value(y)))
+
+#define uint63_lxor(x,y) ((value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1))
+#define uint63_lor(x,y) ((value)((uint64_t)(x) | (uint64_t)(y)))
+#define uint63_land(x,y) ((value)((uint64_t)(x) & (uint64_t)(y)))
+
+/* TODO: is + or | better? OCAML uses + */
+/* TODO: is - or ^ better? */
+#define uint63_lsl(x,y) ((y) < (uint64_t) 127 ? ((value)((((uint64_t)(x)-1) << (uint63_of_value(y))) | 1)) : uint63_zero)
+#define uint63_lsr(x,y) ((y) < (uint64_t) 127 ? ((value)(((uint64_t)(x) >> (uint63_of_value(y))) | 1)) : uint63_zero)
+#define uint63_lsl1(x) ((value)((((uint64_t)(x)-1) << 1) +1))
+#define uint63_lsr1(x) ((value)(((uint64_t)(x) >> 1) |1))
+
+/* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */
+/* (modulo 2^63) for p <= 63 */
+value uint63_addmuldiv(uint64_t p, uint64_t x, uint64_t y) {
+ uint64_t shiftby = uint63_of_value(p);
+ value r = (value)((uint64_t)(x^1) << shiftby);
+ r |= ((uint64_t)y >> (63-shiftby)) | 1;
+ return r;
+}
+
+value uint63_head0(uint64_t x) {
+ int r = 0;
+ if (!(x & 0xFFFFFFFF00000000)) { x <<= 32; r += 32; }
+ if (!(x & 0xFFFF000000000000)) { x <<= 16; r += 16; }
+ if (!(x & 0xFF00000000000000)) { x <<= 8; r += 8; }
+ if (!(x & 0xF000000000000000)) { x <<= 4; r += 4; }
+ if (!(x & 0xC000000000000000)) { x <<= 2; r += 2; }
+ if (!(x & 0x8000000000000000)) { x <<=1; r += 1; }
+ return Val_int(r);
+}
+
+value uint63_tail0(value x) {
+ int r = 0;
+ x = (uint64_t)x >> 1;
+ if (!(x & 0xFFFFFFFF)) { x >>= 32; r += 32; }
+ if (!(x & 0x0000FFFF)) { x >>= 16; r += 16; }
+ if (!(x & 0x000000FF)) { x >>= 8; r += 8; }
+ if (!(x & 0x0000000F)) { x >>= 4; r += 4; }
+ if (!(x & 0x00000003)) { x >>= 2; r += 2; }
+ if (!(x & 0x00000001)) { x >>=1; r += 1; }
+ return Val_int(r);
+}
+
+value uint63_mulc(value x, value y, value* h) {
+ x = (uint64_t)x >> 1;
+ y = (uint64_t)y >> 1;
+ uint64_t lx = x & 0xFFFFFFFF;
+ uint64_t ly = y & 0xFFFFFFFF;
+ uint64_t hx = x >> 32;
+ uint64_t hy = y >> 32;
+ uint64_t hr = hx * hy;
+ uint64_t lr = lx * ly;
+ lx *= hy;
+ ly *= hx;
+ hr += (lx >> 32) + (ly >> 32);
+ lx <<= 32;
+ lr += lx;
+ if (lr < lx) { hr++; }
+ ly <<= 32;
+ lr += ly;
+ if (lr < ly) { hr++; }
+ hr = (hr << 1) | (lr >> 63);
+ *h = Val_int(hr);
+ return Val_int(lr);
+}
+
+#define lt128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_lt(xl,yl)))
+#define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl)))
+
+value uint63_div21(value xh, value xl, value y, value* q) {
+ xh = (uint64_t)xh >> 1;
+ xl = ((uint64_t)xl >> 1) | ((uint64_t)xh << 63);
+ xh = (uint64_t)xh >> 1;
+ uint64_t maskh = 0;
+ uint64_t maskl = 1;
+ uint64_t dh = 0;
+ uint64_t dl = (uint64_t)y >> 1;
+ int cmp = 1;
+ while (dh >= 0 && cmp) {
+ cmp = lt128(dh,dl,xh,xl);
+ dh = (dh << 1) | (dl >> 63);
+ dl = dl << 1;
+ maskh = (maskh << 1) | (maskl >> 63);
+ maskl = maskl << 1;
+ }
+ uint64_t remh = xh;
+ uint64_t reml = xl;
+ uint64_t quotient = 0;
+ while (maskh | maskl) {
+ if (le128(dh,dl,remh,reml)) {
+ quotient = quotient | maskl;
+ if (uint63_lt(reml,dl)) {remh = remh - dh - 1;} else {remh = remh - dh;}
+ reml = reml - dl;
+ }
+ maskl = (maskl >> 1) | (maskh << 63);
+ maskh = maskh >> 1;
+ dl = (dl >> 1) | (dh << 63);
+ dh = dh >> 1;
+ }
+ *q = Val_int(quotient);
+ return Val_int(reml);
+}
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
new file mode 100644
index 0000000000..e05f3fb82e
--- /dev/null
+++ b/kernel/byterun/coq_values.c
@@ -0,0 +1,94 @@
+/***********************************************************************/
+/* */
+/* Coq Compiler */
+/* */
+/* Benjamin Gregoire, projets Logical and Cristal */
+/* INRIA Rocquencourt */
+/* */
+/* */
+/***********************************************************************/
+
+#include <stdio.h>
+#include <caml/memory.h>
+#include "coq_fix_code.h"
+#include "coq_instruct.h"
+#include "coq_memory.h"
+#include "coq_values.h"
+#include <memory.h>
+/* KIND OF VALUES */
+
+#define Setup_for_gc
+#define Restore_after_gc
+
+value coq_kind_of_closure(value v) {
+ opcode_t * c;
+ int is_app = 0;
+ c = Code_val(v);
+ if (Is_instruction(c, GRAB)) return Val_int(0);
+ if (Is_instruction(c, RESTART)) {is_app = 1; c++;}
+ if (Is_instruction(c, GRABREC)) return Val_int(1+is_app);
+ if (Is_instruction(c, MAKEACCU)) return Val_int(3);
+ return Val_int(0);
+}
+
+
+/* DESTRUCT ACCU */
+
+value coq_closure_arity(value clos) {
+ opcode_t * c = Code_val(clos);
+ if (Is_instruction(c,RESTART)) {
+ c++;
+ if (Is_instruction(c,GRAB)) return Val_int(3 + c[1] - Wosize_val(clos));
+ else {
+ if (Wosize_val(clos) != 2) failwith("Coq Values : coq_closure_arity");
+ return Val_int(1);
+ }
+ }
+ if (Is_instruction(c,GRAB)) return Val_int(1 + c[1]);
+ return Val_int(1);
+}
+
+/* Fonction sur les fix */
+
+value coq_offset(value v) {
+ if (Tag_val(v) == Closure_tag) return Val_int(0);
+ else return Val_long(-Wsize_bsize(Infix_offset_val(v)));
+}
+
+value coq_offset_closure(value v, value offset){
+ return (value)&Field(v, Int_val(offset));
+}
+
+value coq_set_bytecode_field(value v, value i, value code) {
+ // No write barrier because the bytecode does not live on the OCaml heap
+ Field(v, Long_val(i)) = (value) Code_val(code);
+ return Val_unit;
+}
+
+value coq_offset_tcode(value code,value offset){
+ CAMLparam1(code);
+ CAMLlocal1(res);
+ res = caml_alloc_small(1, Abstract_tag);
+ Code_val(res) = Code_val(code) + Int_val(offset);
+ CAMLreturn(res);
+}
+
+value coq_int_tcode(value pc, value offset) {
+ code_t code = Code_val(pc);
+ return Val_int(*((code_t) code + Int_val(offset)));
+}
+
+value coq_tcode_array(value tcodes) {
+ CAMLparam1(tcodes);
+ CAMLlocal2(res, tmp);
+ int i;
+ /* Assumes that the vector of types is small. This was implicit in the
+ previous code which was building the type array using Alloc_small. */
+ res = caml_alloc_small(Wosize_val(tcodes), Default_tag);
+ for (i = 0; i < Wosize_val(tcodes); i++) {
+ tmp = caml_alloc_small(1, Abstract_tag);
+ Code_val(tmp) = (code_t) Field(tcodes, i);
+ Store_field(res, i, tmp);
+ }
+ CAMLreturn(res);
+}
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
new file mode 100644
index 0000000000..0cf6ccf532
--- /dev/null
+++ b/kernel/byterun/coq_values.h
@@ -0,0 +1,43 @@
+/***********************************************************************/
+/* */
+/* Coq Compiler */
+/* */
+/* Benjamin Gregoire, projets Logical and Cristal */
+/* INRIA Rocquencourt */
+/* */
+/* */
+/***********************************************************************/
+
+#ifndef _COQ_VALUES_
+#define _COQ_VALUES_
+
+#include <caml/alloc.h>
+#include <caml/mlvalues.h>
+
+#define Default_tag 0
+#define Accu_tag 0
+
+#define ATOM_ID_TAG 0
+#define ATOM_INDUCTIVE_TAG 1
+#define ATOM_TYPE_TAG 2
+#define ATOM_PROJ_TAG 3
+#define ATOM_FIX_TAG 4
+#define ATOM_SWITCH_TAG 5
+#define ATOM_COFIX_TAG 6
+#define ATOM_COFIXEVALUATED_TAG 7
+
+/* Les blocs accumulate */
+#define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
+#define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
+
+/* */
+#define coq_tag_C1 2
+#define coq_tag_C0 1
+#define coq_tag_pair 1
+#define coq_true Val_int(0)
+#define coq_false Val_int(1)
+#define coq_Eq Val_int(0)
+#define coq_Lt Val_int(1)
+#define coq_Gt Val_int(2)
+
+#endif /* _COQ_VALUES_ */
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
new file mode 100644
index 0000000000..20bdf28e54
--- /dev/null
+++ b/kernel/byterun/dune
@@ -0,0 +1,13 @@
+(library
+ (name byterun)
+ (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
+ (public_name coq.vm)
+ (c_names coq_fix_code coq_memory coq_values coq_interp))
+
+(rule
+ (targets coq_instruct.h)
+ (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe enum))))
+
+(rule
+ (targets coq_jumptbl.h)
+ (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump))))
diff --git a/kernel/byterun/libcoqrun.clib b/kernel/byterun/libcoqrun.clib
new file mode 100644
index 0000000000..c06e408672
--- /dev/null
+++ b/kernel/byterun/libcoqrun.clib
@@ -0,0 +1,4 @@
+coq_fix_code.o
+coq_memory.o
+coq_values.o
+coq_interp.o
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:02:21 +0000