Fix #5127 Memory corruption with the VM

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.

4 files changed, 62 insertions, 55 deletions

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;