/* 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. */
/* Beware: Alloc_small can only invoked for allocations smaller than Max_young_wosize, which is usually 256. For larger allocations, caml_alloc_shr needs to be used instead, and the block needs to be filled using caml_initialize. Note that these two functions never trigger a GC, so calling Setup_for_gc is not needed.
*/
/* If there is an asynchronous exception, we reset the vm */ #define Handle_potential_exception(res) \ if (Is_exception_result(res)) { \
rocq_sp = rocq_stack_high; \
caml_raise(Extract_exception(res)); \
}
/* 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.
*/
/* We should also check "Code_val(v) == accumulate" to be sure,
but Is_accu is only used in places where closures cannot occur. */ #define Is_accu(v) (Is_block(v) && Tag_val(v) == Closure_tag)
/* Beware: we cannot use caml_copy_double here as it doesn't use Alloc_small, hence doesn't protect the stack via
Setup_for_gc/Restore_after_gc. */ #define Rocq_copy_double(val) do{ \ double Rocq_copy_double_f__ = (val); \
Rocq_alloc_small(accu, Double_wosize, Double_tag);\
Store_double_val(accu, Rocq_copy_double_f__); \
}while(0);
/* Turn a code pointer into a stack value usable as a return address, and conversely. The least significant bit is set to 1 so that the GC does not mistake return
addresses for heap pointers. */ #define StoreRA(p) ((value)(p) + 1) #define LoadRA(p) ((code_t)((value)(p) - 1))
#if OCAML_VERSION < 41000 /* For signal handling, we hijack some code from the caml runtime */
value rocq_subst_instance(value arg, value tosubst)
{ staticconst value * closure_f = NULL; if (closure_f == NULL) { /* First time around, look up by name */
closure_f = caml_named_value("rocq_subst_instance");
} return caml_callback2_exn(*closure_f, arg, tosubst);
}
/* The interpreter itself */
value rocq_interprete
(code_t rocq_pc, value rocq_accu, value rocq_atom_tbl, value rocq_global_data, value rocq_env, long rocq_extra_args)
{ /* rocq_accu is not allocated on the OCaml heap */
CAMLparam2(rocq_atom_tbl, rocq_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 #ifdefined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32) #ifdef JUMPTBL_BASE_REG registerchar * rocq_jumptbl_base JUMPTBL_BASE_REG; #else registerchar * rocq_jumptbl_base; #endif #endif #ifdef THREADED_CODE staticvoid * rocq_jumptable[] = { # include "rocq_jumptbl.h"
}; #else
opcode_t curr_instr; #endif
print_instr("Enter Interpreter"); if (rocq_pc == NULL) { /* Interpreter is initializing */
print_instr("Interpreter is initializing"); #ifdef THREADED_CODE
rocq_init_thread_code(rocq_jumptable, rocq_Jumptbl_base); #endif
CAMLreturn(Val_unit);
} #ifdefined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
rocq_jumptbl_base = rocq_Jumptbl_base; #endif
check_stack:
print_instr("check_stack");
CHECK_STACK(0); /* We also check for signals */ #if OCAML_VERSION >= 50000 if (Caml_check_gc_interrupt(Caml_state)) {
Setup_for_gc;
value res = caml_process_pending_actions_exn();
Handle_potential_exception(res);
Restore_after_gc;
} #elif OCAML_VERSION >= 41000 if (caml_something_to_do) {
Setup_for_gc;
value res = caml_process_pending_actions_exn();
Handle_potential_exception(res);
Restore_after_gc;
} #else if (caml_signals_are_pending) { /* If there's a Ctrl-C, we reset the vm */
intnat sigint = caml_pending_signals[SIGINT]; if (sigint) { rocq_sp = rocq_stack_high; }
Setup_for_gc;
caml_process_pending_signals();
Restore_after_gc; if (sigint) {
caml_failwith("Rocq VM: Fatal error: SIGINT signal detected " "but no exception was raised");
}
} #endif
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);
rocq_env = accu;
rocq_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);
rocq_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);
rocq_env = accu;
rocq_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);
rocq_env = accu;
rocq_extra_args += 2; goto check_stack;
}
Instruct(RESTART) { int num_args = Wosize_val(rocq_env) - 3; int i;
print_instr("RESTART");
CHECK_STACK(num_args);
sp -= num_args; for (i = 0; i < num_args; i++) sp[i] = Field(rocq_env, i + 3);
rocq_env = Field(rocq_env, 2);
rocq_extra_args += num_args;
Next;
}
Instruct(GRAB) { int required = *pc++;
print_instr("GRAB"); /* printf("GRAB %d\n",required); */ if (rocq_extra_args >= required) {
rocq_extra_args -= required;
} else {
mlsize_t num_args, i;
num_args = 1 + rocq_extra_args; /* arg1 + extra args */
Rocq_alloc_small(accu, num_args + 3, Closure_tag);
Field(accu, 1) = Val_int(2);
Field(accu, 2) = rocq_env; for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i];
Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
sp += num_args;
pc = LoadRA(sp[0]);
rocq_env = sp[1];
rocq_extra_args = Long_val(sp[2]);
sp += 3;
}
Next;
}
Instruct(GRABREC) { int rec_pos = *pc++; /* commence a zero */
print_instr("GRABREC"); if (rec_pos <= rocq_extra_args && !Is_accu(sp[rec_pos])) {
pc++; /* Skip the next RESTART, then point rocq_env at the free variables. */
rocq_env = rocq_env + (Int_val(Field(rocq_env, 1)) - 2) * sizeof(value);
} else { if (rocq_extra_args < rec_pos) { /* Partial application */
mlsize_t num_args, i;
num_args = 1 + rocq_extra_args; /* arg1 + extra args */
Rocq_alloc_small(accu, num_args + 3, Closure_tag);
Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
Field(accu, 1) = Val_int(2);
Field(accu, 2) = rocq_env; for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i];
sp += num_args;
pc = LoadRA(sp[0]);
rocq_env = sp[1];
rocq_extra_args = Long_val(sp[2]);
sp += 3;
} else { /* The recursive argument is an accumulator */
mlsize_t num_args, sz, i;
value block; /* Construction of fixpoint applied to its [rec_pos-1] first arguments */
Rocq_alloc_small(accu, rec_pos + 3, Closure_tag);
Code_val(accu) = pc; /* Point to the next RESTART instr. */
Field(accu, 1) = Val_int(2);
Field(accu, 2) = rocq_env; // We store the fixpoint in the first field for (i = 0; i < rec_pos; i++) Field(accu, i + 3) = *sp++; // Storing args /* Construction of the atom */
Rocq_alloc_small(block, 2, ATOM_FIX_TAG);
Field(block, 0) = *sp++;
Field(block, 1) = accu;
accu = block; /* Construction of the accumulator */
num_args = rocq_extra_args - rec_pos;
sz = 3 + num_args; if (sz <= Max_young_wosize) {
Rocq_alloc_small(block, sz, Closure_tag);
Field(block, 2) = accu; for (i = 3; i < sz; ++i)
Field(block, i) = *sp++;
} else {
block = caml_alloc_shr(sz, Closure_tag);
caml_initialize(&Field(block, 2), accu); for (i = 3; i < sz; ++i)
caml_initialize(&Field(block, i), *sp++);
}
Code_val(block) = accumulate;
Field(block, 1) = Val_int(2);
accu = block;
pc = LoadRA(sp[0]);
rocq_env = sp[1];
rocq_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;
Rocq_alloc_small(accu, 2 + nvars, Closure_tag);
Field(accu, 1) = Val_int(2);
Code_val(accu) = pc + *pc;
pc++; for (i = 0; i < nvars; i++) {
print_lint(sp[i]);
Field(accu, i + 2) = 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 */
Rocq_alloc_small(accu, nfuncs, Abstract_tag); for(i = 0; i < nfuncs; i++) {
Field(accu,i) = (value)(pc+pc[i]);
}
pc += nfuncs;
*--sp=accu;
Rocq_alloc_small(accu, nfuncs * 3 + nvars, Closure_tag);
Field(accu, nfuncs * 3 + nvars - 1) = *sp++;
p = (value *) &Field(accu, 0);
*p++ = (value) (pc + pc[0]);
*p++ = Val_int(nfuncs * 3 - 1); for (i = 1; i < nfuncs; i++) {
*p++ = Make_header(i * 3, Infix_tag, 0); /* color irrelevant. */
*p++ = (value) (pc + pc[i]);
*p++ = Val_int((nfuncs - i) * 3 - 1);
} for (i = 0; i < nvars; i++) *p++ = *sp++;
pc += nfuncs;
accu = accu + start * 3 * 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 */
Rocq_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++) {
Rocq_alloc_small(accu, 3, Closure_tag);
Code_val(accu) = accumulate;
Field(accu, 1) = Val_int(2);
Field(accu, 2) = Val_int(1);
*--sp=accu;
} /* creation des fonction cofix */
Instruct(SWITCH) {
uint32_t sizes = *pc++;
print_instr("SWITCH"); if (Is_block(accu)) { long index = Tag_val(accu); if (index == Closure_tag) index = 0;
print_instr("block");
print_lint(index);
pc += pc[(sizes >> 8) + 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;
}
/* Special operations for reduction of open term */
Instruct(ACCUMULATE) {
mlsize_t i, size, sz;
print_instr("ACCUMULATE");
size = Wosize_val(rocq_env);
sz = size + rocq_extra_args + 1; if (sz <= Max_young_wosize) {
Rocq_alloc_small(accu, sz, Closure_tag); for (i = 0; i < size; ++i)
Field(accu, i) = Field(rocq_env, i); for (i = size; i < sz; ++i)
Field(accu, i) = *sp++;
} else {
accu = caml_alloc_shr(sz, Closure_tag); for (i = 0; i < size; ++i)
caml_initialize(&Field(accu, i), Field(rocq_env, i)); for (i = size; i < sz; ++i)
caml_initialize(&Field(accu, i), *sp++);
}
pc = LoadRA(sp[0]);
rocq_env = sp[1];
rocq_extra_args = Long_val(sp[2]);
sp += 3;
Next;
}
Instruct(MAKESWITCHBLOCK) {
print_instr("MAKESWITCHBLOCK");
*--sp = accu; // Save matched block on stack
accu = Field(accu, 2); // 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] = StoreRA(pc + *pc);
sp[1] = rocq_env;
rocq_env = Field(accu,0); // Pointer to suspension
accu = sp[2]; // Save accumulator to accu register
sp[2] = Val_long(rocq_extra_args); // Push number of args for return
nargs = Wosize_val(accu) - 3; // Number of args = size of accumulator - 2 (accumulator closure) - 1 (atom) // Push arguments to stack
CHECK_STACK(nargs+1);
sp -= nargs; for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 3);
*--sp = accu; // Leftmost argument is the pointer to the suspension
print_lint(nargs);
rocq_extra_args = nargs;
pc = Code_val(rocq_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;
value block;
print_instr("MAKESWITCHBLOCK");
typlbl = (code_t)pc + *pc;
pc++;
swlbl = (code_t)pc + *pc;
pc++;
annot = *pc++;
sz = *pc++;
*--sp=Field(rocq_global_data, annot); /* We save the stack */ if (sz == 0) accu = Atom(0); elseif (sz <= Max_young_wosize) {
Rocq_alloc_small(accu, sz, Default_tag); if (Is_tailrec_switch(*sp)) { 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];
}
} else {
accu = caml_alloc_shr(sz, Default_tag); if (Is_tailrec_switch(*sp)) { for (i = 0; i < sz; i++) caml_initialize(&Field(accu, i), sp[i+2]);
}else{ for (i = 0; i < sz; i++) caml_initialize(&Field(accu, i), sp[i+5]);
}
}
*--sp = accu; /* Create bytecode wrappers */
Rocq_alloc_small(accu, 1, Abstract_tag);
Code_val(accu) = typlbl;
*--sp = accu;
Rocq_alloc_small(accu, 1, Abstract_tag);
Code_val(accu) = swlbl; /* We create the switch zipper */
Rocq_alloc_small(block, 5, Default_tag);
Field(block, 0) = sp[0];
Field(block, 1) = accu;
Field(block, 2) = sp[2];
Field(block, 3) = sp[1];
Field(block, 4) = rocq_env;
sp += 3;
accu = block; /* We create the atom */
Rocq_alloc_small(block, 2, ATOM_SWITCH_TAG);
Field(block, 0) = *sp++;
Field(block, 1) = accu;
accu = block; /* We create the accumulator */
Rocq_alloc_small(block, 3, Closure_tag);
Code_val(block) = accumulate;
Field(block, 1) = Val_int(2);
Field(block, 2) = accu;
accu = block;
}
}
Next;
}
Instruct(MAKEACCU) {
mlsize_t i, sz;
print_instr("MAKEACCU");
sz = rocq_extra_args + 4; if (sz <= Max_young_wosize) {
Rocq_alloc_small(accu, sz, Closure_tag);
Field(accu, 2) = Field(rocq_atom_tbl, *pc); for (i = 3; i < sz; ++i)
Field(accu, i) = *sp++;
} else {
accu = caml_alloc_shr(sz, Closure_tag);
caml_initialize(&Field(accu, 2), Field(rocq_atom_tbl, *pc)); for (i = 3; i < sz; ++i)
caml_initialize(&Field(accu, i), *sp++);
}
Code_val(accu) = accumulate;
Field(accu, 1) = Val_int(2);
pc = LoadRA(sp[0]);
rocq_env = sp[1];
rocq_extra_args = Long_val(sp[2]);
sp += 3;
Next;
}
Instruct(BRANCH) { /* unconditional branching */
print_instr("BRANCH");
pc += *pc; /* pc = (code_t)(pc+*pc); */
Next;
}
Instruct(CHECKADDINT63){
print_instr("CHECKADDINT63");
CheckInt2(); /* Adds the integer in the accumulator with
the one ontop of the stack (which is poped)*/
Uint63_add(accu, *sp++);
Next;
}
Instruct (CHECKADDCINT63) {
print_instr("CHECKADDCINT63");
CheckInt2(); /* returns the sum with a carry */ int c;
Uint63_add(accu, *sp);
Uint63_lt(c, accu, *sp);
Swap_accu_sp;
AllocCarry(c);
Field(accu, 0) = *sp++;
Next;
}
Instruct (CHECKADDCARRYCINT63) {
print_instr("ADDCARRYCINT63");
CheckInt2(); /* returns the sum plus one with a carry */ int c;
Uint63_addcarry(accu, *sp);
Uint63_leq(c, accu, *sp);
Swap_accu_sp;
AllocCarry(c);
Field(accu, 0) = *sp++;
Next;
}
Instruct (CHECKSUBCINT63) {
print_instr("SUBCINT63");
CheckInt2(); /* returns the subtraction with a carry */ int c;
Uint63_lt(c, accu, *sp);
Uint63_sub(accu, *sp);
Swap_accu_sp;
AllocCarry(c);
Field(accu, 0) = *sp++;
Next;
}
Instruct (CHECKSUBCARRYCINT63) {
print_instr("SUBCARRYCINT63");
CheckInt2(); /* returns the subtraction minus one with a carry */ int c;
Uint63_leq(c,accu,*sp);
Uint63_subcarry(accu,*sp);
Swap_accu_sp;
AllocCarry(c);
Field(accu, 0) = *sp++;
Next;
}
Instruct (CHECKMULCINT63) { /*returns the multiplication on a pair */
print_instr("MULCINT63");
CheckInt2();
Uint63_mulc(accu, *sp, sp);
*--sp = accu;
AllocPair();
Field(accu, 1) = *sp++;
Field(accu, 0) = *sp++;
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 */ int b;
Uint63_eq0(b, *sp); if (b) {
accu = *sp++;
} else {
Uint63_div(accu, *sp++);
}
Next;
}
Instruct(CHECKMODINT63) {
print_instr("CHEKMODINT63");
CheckInt2(); int b;
Uint63_eq0(b, *sp); if (b) {
sp++;
} else {
Uint63_mod(accu,*sp++);
}
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 */ int b;
Uint63_eq0(b, *sp); if (b) {
value block;
Rocq_alloc_small(block, 2, rocq_tag_pair);
Field(block, 0) = *sp++;
Field(block, 1) = accu;
accu = block;
} else {
*--sp = accu;
Uint63_div(sp[0],sp[1]);
Swap_accu_sp;
Uint63_mod(accu,sp[1]);
sp[1] = sp[0];
Swap_accu_sp;
AllocPair();
Field(accu, 0) = sp[1];
Field(accu, 1) = sp[0];
sp += 2;
}
Next;
}
Instruct (CHECKEQUALFLOAT) { double x, y;
print_instr("CHECKEQUALFLOAT");
CheckFloat2();
x = Double_val(accu);
y = Double_val(*sp++); if (x == y) {
accu = (x != 0 || !signbit(x) == !signbit(y)) ? rocq_true : rocq_false; /* note that the spec of signbit only promises a "nonzero value"
so we need to normalize booleans with ! before comparing them */
} else {
accu = (x != x && y != y) ? rocq_true : rocq_false; /* is_nan(x) && is_nan(y) */
}
Next;
}
value rocq_push_arguments(value args) { int nargs,i;
value * sp = rocq_sp;
nargs = Wosize_val(args) - 3;
CHECK_STACK(nargs);
rocq_sp -= nargs;
print_instr("push_args");print_int(nargs); for (i = 0; i < nargs; i++) rocq_sp[i] = Field(args, i + 3); return Val_unit;
}
value rocq_push_vstack(value stk, value max_stack_size) { int len,i;
value * sp = rocq_sp;
len = Wosize_val(stk);
CHECK_STACK(len);
rocq_sp -= len;
print_instr("push_vstack");print_int(len); for(i = 0; i < len; i++) rocq_sp[i] = Field(stk,i);
sp = rocq_sp;
CHECK_STACK(uint_of_value(max_stack_size)); return Val_unit;
}
value rocq_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 rocq_interprete
CAMLparam1(tcode);
print_instr("rocq_interprete");
value res = rocq_interprete(Code_val(tcode), a, t, g, e, Long_val(ea));
print_instr("end rocq_interprete");
CAMLreturn(res);
}
value rocq_interprete_byte(value* argv, int argn){ return rocq_interprete_ml(argv[0], argv[1], argv[2], argv[3], argv[4], argv[5]);
}
¤ Dauer der Verarbeitung: 0.43 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
