From 897ce077f11940adce406a20ad7d5c128e90cc28 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 19 Oct 2016 14:48:14 +0200 Subject: Fix #5127 Memory corruption with the VM MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The bytecode interpreter ensures that the stack space available at some points is above a static threshold. However, arbitrary large stack space can be needed between two check points, leading to segmentation faults in some cases. We track the use of stack space at compilation time and add an instruction to ensure greater stack capacity when required. This is inspired from OCaml's PR#339 and PR#7168. Patch written with Benjamin Grégoire. --- kernel/byterun/coq_fix_code.c | 8 ++-- kernel/byterun/coq_instruct.h | 1 + kernel/byterun/coq_interp.c | 107 ++++++++++++++++++++++-------------------- kernel/byterun/coq_memory.c | 1 + 4 files changed, 62 insertions(+), 55 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 29e33d349..d5feafbf9 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -57,7 +57,7 @@ void init_arity () { 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[ISCONST]= 1; + arity[BRANCH]=arity[ISCONST]=arity[ENSURESTACKCAPACITY]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[ARECONST]=arity[PROJ]=2; @@ -79,7 +79,7 @@ void * coq_stat_alloc (asize_t sz) value coq_makeaccu (value i) { code_t q; - code_t res = coq_stat_alloc(8); + code_t res = coq_stat_alloc(2 * sizeof(opcode_t)); q = res; *q++ = VALINSTR(MAKEACCU); *q = (opcode_t)Int_val(i); @@ -91,13 +91,13 @@ value coq_pushpop (value i) { int n; n = Int_val(i); if (n == 0) { - res = coq_stat_alloc(4); + res = coq_stat_alloc(sizeof(opcode_t)); *res = VALINSTR(STOP); return (value)res; } else { code_t q; - res = coq_stat_alloc(12); + res = coq_stat_alloc(3 * sizeof(opcode_t)); q = res; *q++ = VALINSTR(POP); *q++ = (opcode_t)n; diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index 8c5ab0ecb..dc3a88818 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -37,6 +37,7 @@ enum instructions { GETFIELD0, GETFIELD1, GETFIELD, SETFIELD0, SETFIELD1, SETFIELD, PROJ, + ENSURESTACKCAPACITY, 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 d634b726b..35abd011b 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -84,6 +84,14 @@ sp is a local copy of the global variable extern_sp. */ # 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; } @@ -206,6 +214,9 @@ value coq_interprete 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 @@ -362,7 +373,7 @@ value coq_interprete coq_extra_args = *pc - 1; pc = Code_val(accu); coq_env = accu; - goto check_stacks; + goto check_stack; } Instruct(APPLY1) { value arg1 = sp[0]; @@ -379,7 +390,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args = 0; - goto check_stacks; + goto check_stack; } Instruct(APPLY2) { value arg1 = sp[0]; @@ -394,7 +405,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args = 1; - goto check_stacks; + goto check_stack; } Instruct(APPLY3) { value arg1 = sp[0]; @@ -411,17 +422,13 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args = 2; - goto check_stacks; + goto check_stack; } /* Stack checks */ - check_stacks: - print_instr("check_stacks"); - if (sp < coq_stack_threshold) { - coq_sp = sp; - realloc_coq_stack(Coq_stack_threshold); - sp = coq_sp; - } + 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 */ @@ -430,6 +437,16 @@ value coq_interprete } 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; @@ -444,7 +461,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args += nargs - 1; - goto check_stacks; + goto check_stack; } Instruct(APPTERM1) { value arg1 = sp[0]; @@ -453,7 +470,7 @@ value coq_interprete sp[0] = arg1; pc = Code_val(accu); coq_env = accu; - goto check_stacks; + goto check_stack; } Instruct(APPTERM2) { value arg1 = sp[0]; @@ -466,7 +483,7 @@ value coq_interprete print_lint(accu); coq_env = accu; coq_extra_args += 1; - goto check_stacks; + goto check_stack; } Instruct(APPTERM3) { value arg1 = sp[0]; @@ -480,7 +497,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args += 2; - goto check_stacks; + goto check_stack; } Instruct(RETURN) { @@ -511,6 +528,7 @@ value coq_interprete 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); @@ -870,29 +888,7 @@ value coq_interprete sp++; Next; } - - /* *sp = accu; - * Netoyage des cofix * - size = Wosize_val(accu); - for (i = 2; i < size; i++) { - accu = Field(*sp, i); - if (IS_EVALUATED_COFIX(accu)) { - size_aux = Wosize_val(accu); - *--sp = accu; - Alloc_small(accu, size_aux, Accu_tag); - for(j = 0; j < size_aux; j++) Field(accu, j) = Field(*sp, j); - *sp = accu; - Alloc_small(accu, 1, ATOM_COFIX_TAG); - Field(accu, 0) = Field(Field(*sp, 1), 0); - caml_modify(&Field(*sp, 1), accu); - accu = *sp; sp++; - caml_modify(&Field(*sp, i), accu); - } - } - sp++; - Next; - } */ - + Instruct(SETFIELD){ print_instr("SETFIELD"); caml_modify(&Field(accu, *pc),*sp); @@ -986,28 +982,31 @@ value coq_interprete } Instruct(MAKESWITCHBLOCK) { print_instr("MAKESWITCHBLOCK"); - *--sp = accu; - accu = Field(accu,1); + *--sp = accu; // Save matched block on stack + accu = Field(accu,1); // Save atom to accu register switch (Tag_val(accu)) { - case ATOM_COFIX_TAG: + 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); - accu = sp[2]; - sp[2] = Val_long(coq_extra_args); - nargs = Wosize_val(accu) - 2; + 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; + for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); + *--sp = accu; // Last argument is the pointer to the suspension print_lint(nargs); coq_extra_args = nargs; - pc = Code_val(coq_env); - goto check_stacks; + pc = Code_val(coq_env); // Trigger evaluation + goto check_stack; } case ATOM_COFIXEVALUATED_TAG: { @@ -1464,26 +1463,32 @@ value coq_push_val(value v) { 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 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 e, value ea) { print_instr("coq_interprete"); return coq_interprete((code_t)tcode, a, e, Long_val(ea)); - print_instr("end coq_interprete"); + print_instr("end coq_interprete"); } value coq_eval_tcode (value tcode, value e) { diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index c9bcdc32f..45cfae509 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -130,6 +130,7 @@ value init_coq_vm(value unit) /* ML */ return Val_unit;; } +/* [required_space] is a size in words */ void realloc_coq_stack(asize_t required_space) { asize_t size; -- cgit v1.2.3