aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cemitcodes.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-10-19 14:48:14 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-10-24 18:04:26 +0200
commit897ce077f11940adce406a20ad7d5c128e90cc28 (patch)
treedb359323a84ed17d180e01ffb6af67885a3ecbfc /kernel/cemitcodes.ml
parent1d769e02b3baba54246c942fe116abaf850892db (diff)
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.
Diffstat (limited to 'kernel/cemitcodes.ml')
-rw-r--r--kernel/cemitcodes.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 57e32684a..ccea67e41 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -226,6 +226,7 @@ let emit_instr = function
else (out opSETFIELD;out_int n)
| Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
| Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p)
+ | Kensurestackcapacity size -> out opENSURESTACKCAPACITY; out_int size
(* spiwack *)
| Kbranch lbl -> out opBRANCH; out_label lbl
| Kaddint31 -> out opADDINT31