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

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 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/byterun/coq_fix_code.c')

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 29e33d349b..d5feafbf91 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;
-- 
cgit v1.2.3