From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- kernel/byterun/coq_fix_code.c | 2 +- kernel/byterun/coq_gc.h | 13 ++++++- kernel/byterun/coq_instruct.h | 1 + kernel/byterun/coq_interp.c | 79 +++++++++++++++++++++++++++++++++---------- kernel/byterun/coq_memory.c | 16 --------- kernel/byterun/coq_values.c | 1 - kernel/byterun/coq_values.h | 19 ++++------- 7 files changed, 83 insertions(+), 48 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 1be3e651..29e33d34 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -60,7 +60,7 @@ void init_arity () { arity[BRANCH]=arity[ISCONST]= 1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= - arity[ARECONST]=2; + arity[ARECONST]=arity[PROJ]=2; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; /* instruction with arbitrary operands */ diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h index c7b18b90..f0627586 100644 --- a/kernel/byterun/coq_gc.h +++ b/kernel/byterun/coq_gc.h @@ -12,6 +12,7 @@ #define _COQ_CAML_GC_ #include #include +#include typedef void (*scanning_action) (value, value *); @@ -24,12 +25,22 @@ 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); \ diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index 9cbf4077..8c5ab0ec 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -36,6 +36,7 @@ enum instructions { SWITCH, PUSHFIELDS, GETFIELD0, GETFIELD1, GETFIELD, SETFIELD0, SETFIELD1, SETFIELD, + PROJ, CONST0, CONST1, CONST2, CONST3, CONSTINT, PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, ACCUMULATE, diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 0ab9f89f..dc571699 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -77,9 +77,11 @@ sp is a local copy of the global variable extern_sp. */ #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 /* GC interface */ @@ -339,6 +341,7 @@ value coq_interprete /* Fallthrough */ Instruct(ENVACC){ print_instr("ENVACC"); + print_int(*pc); accu = Field(coq_env, *pc++); Next; } @@ -369,6 +372,10 @@ value coq_interprete 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; @@ -456,6 +463,7 @@ value coq_interprete sp[0] = arg1; sp[1] = arg2; pc = Code_val(accu); + print_lint(accu); coq_env = accu; coq_extra_args += 1; goto check_stacks; @@ -479,11 +487,18 @@ value coq_interprete 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]); @@ -583,7 +598,10 @@ value coq_interprete Alloc_small(accu, 1 + nvars, Closure_tag); Code_val(accu) = pc + *pc; pc++; - for (i = 0; i < nvars; i++) Field(accu, i + 1) = sp[i]; + for (i = 0; i < nvars; i++) { + print_lint(sp[i]); + Field(accu, i + 1) = sp[i]; + } sp += nvars; Next; } @@ -718,6 +736,7 @@ value coq_interprete /* Fallthrough */ Instruct(GETGLOBAL){ print_instr("GETGLOBAL"); + print_int(*pc); accu = Field(coq_global_data, *pc); pc++; Next; @@ -730,7 +749,7 @@ value coq_interprete tag_t tag = *pc++; mlsize_t i; value block; - print_instr("MAKEBLOCK"); + print_instr("MAKEBLOCK, tag="); Alloc_small(block, wosize, tag); Field(block, 0) = accu; for (i = 1; i < wosize; i++) Field(block, i) = *sp++; @@ -741,7 +760,8 @@ value coq_interprete tag_t tag = *pc++; value block; - print_instr("MAKEBLOCK1"); + print_instr("MAKEBLOCK1, tag="); + print_int(tag); Alloc_small(block, 1, tag); Field(block, 0) = accu; accu = block; @@ -751,7 +771,8 @@ value coq_interprete tag_t tag = *pc++; value block; - print_instr("MAKEBLOCK2"); + print_instr("MAKEBLOCK2, tag="); + print_int(tag); Alloc_small(block, 2, tag); Field(block, 0) = accu; Field(block, 1) = sp[0]; @@ -762,7 +783,8 @@ value coq_interprete Instruct(MAKEBLOCK3) { tag_t tag = *pc++; value block; - print_instr("MAKEBLOCK3"); + print_instr("MAKEBLOCK3, tag="); + print_int(tag); Alloc_small(block, 3, tag); Field(block, 0) = accu; Field(block, 1) = sp[0]; @@ -774,7 +796,8 @@ value coq_interprete Instruct(MAKEBLOCK4) { tag_t tag = *pc++; value block; - print_instr("MAKEBLOCK4"); + print_instr("MAKEBLOCK4, tag="); + print_int(tag); Alloc_small(block, 4, tag); Field(block, 0) = accu; Field(block, 1) = sp[0]; @@ -795,12 +818,12 @@ value coq_interprete if (Is_block(accu)) { long index = Tag_val(accu); print_instr("block"); - print_int(index); + print_lint(index); pc += pc[(sizes & 0xFFFFFF) + index]; } else { long index = Long_val(accu); print_instr("constant"); - print_int(index); + print_lint(index); pc += pc[index]; } Next; @@ -842,7 +865,6 @@ value coq_interprete } Instruct(SETFIELD1){ - int i, j, size, size_aux; print_instr("SETFIELD1"); caml_modify(&Field(accu, 1),*sp); sp++; @@ -876,8 +898,30 @@ value coq_interprete caml_modify(&Field(accu, *pc),*sp); sp++; pc++; Next; - } - + } + + + Instruct(PROJ){ + print_instr("PROJ"); + if (Is_accu (accu)) { + value block; + /* Skip over the index of projected field */ + pc++; + /* Create atom */ + Alloc_small(block, 2, ATOM_PROJ_TAG); + Field(block, 0) = Field(coq_global_data, *pc); + Field(block, 1) = accu; + /* Create accumulator */ + Alloc_small(accu, 2, Accu_tag); + Code_val(accu) = accumulate; + Field(accu, 1) = block; + } else { + accu = Field(accu, *pc++); + } + pc++; + Next; + } + /* Integer constants */ Instruct(CONST0){ @@ -917,6 +961,7 @@ value coq_interprete /* Fallthrough */ Instruct(CONSTINT) { print_instr("CONSTINT"); + print_int(*pc); accu = Val_int(*pc); pc++; Next; @@ -957,7 +1002,7 @@ value coq_interprete sp -= nargs; for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); *--sp = accu; - print_int(nargs); + print_lint(nargs); coq_extra_args = nargs; pc = Code_val(coq_env); goto check_stacks; @@ -1084,7 +1129,6 @@ value coq_interprete /* returns the sum plus one with a carry */ uint32_t s; s = (uint32_t)accu + (uint32_t)*sp++ + 1; - value block; if( (uint32_t)s <= (uint32_t)accu ) { /* carry */ Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */ @@ -1226,16 +1270,17 @@ value coq_interprete shiftby = uint32_of_value(accu); if (shiftby > 31) { if (shiftby < 62) { - *sp++; - accu = (value)((((*sp++)^1) << (shiftby - 31)) | 1); + sp++; + accu = (value)(((((uint32_t)*sp++)^1) << (shiftby - 31)) | 1); } else { + sp+=2; accu = (value)(1); } } else{ /* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */ - accu = (value)(((*sp++)^1) << shiftby); + accu = (value)((((uint32_t)*sp++)^1) << shiftby); /* accu = 2^(shiftby+1)*x --> 2^(shifby+1)*x+2*y/2^(31-shiftby)+1 */ accu = (value)((accu | (((uint32_t)(*sp++)) >> (31-shiftby)))|1); } @@ -1244,7 +1289,7 @@ value coq_interprete Instruct (COMPAREINT31) { /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */ - /* assumes Inudctive _ : _ := Eq | Lt | Gt */ + /* assumes Inductive _ : _ := Eq | Lt | Gt */ print_instr("COMPAREINT31"); if ((uint32_t)accu == (uint32_t)*sp) { accu = 1; /* 2*0+1 */ diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 8d03829a..c9bcdc32 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -26,7 +26,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size; value coq_global_data; -int coq_all_transp; value coq_atom_tbl; int drawinstr; @@ -104,7 +103,6 @@ static int coq_vm_initialized = 0; value init_coq_vm(value unit) /* ML */ { - int i; if (coq_vm_initialized == 1) { fprintf(stderr,"already open \n");fflush(stderr);} else { @@ -117,7 +115,6 @@ value init_coq_vm(value unit) /* ML */ init_coq_global_data(Coq_global_data_Size); init_coq_atom_tbl(40); /* Initialing the interpreter */ - coq_all_transp = 0; init_coq_interpreter(); /* Some predefined pointer code */ @@ -137,7 +134,6 @@ void realloc_coq_stack(asize_t required_space) { asize_t size; value * new_low, * new_high, * new_sp; - value * p; size = coq_stack_high - coq_stack_low; do { size *= 2; @@ -207,18 +203,6 @@ value realloc_coq_atom_tbl(value size) /* ML */ return Val_unit; } - -value coq_set_transp_value(value transp) -{ - coq_all_transp = (transp == Val_true); - return Val_unit; -} - -value get_coq_transp_value(value unit) -{ - return Val_bool(coq_all_transp); -} - value coq_set_drawinstr(value unit) { drawinstr = 1; diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index 007f61b2..528babeb 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -21,7 +21,6 @@ value coq_kind_of_closure(value v) { opcode_t * c; - int res; int is_app = 0; c = Code_val(v); if (Is_instruction(c, GRAB)) return Val_int(0); diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 1bf493e2..bb0f0eb5 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -17,22 +17,17 @@ #define Default_tag 0 #define Accu_tag 0 - - #define ATOM_ID_TAG 0 -#define ATOM_IDDEF_TAG 1 -#define ATOM_INDUCTIVE_TAG 2 -#define ATOM_FIX_TAG 3 -#define ATOM_SWITCH_TAG 4 -#define ATOM_COFIX_TAG 5 -#define ATOM_COFIXEVALUATED_TAG 6 - - +#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)) #endif /* _COQ_VALUES_ */ - - -- cgit v1.2.3