diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-10-19 14:48:14 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-10-24 18:04:26 +0200 |
commit | 897ce077f11940adce406a20ad7d5c128e90cc28 (patch) | |
tree | db359323a84ed17d180e01ffb6af67885a3ecbfc /kernel/byterun/coq_instruct.h | |
parent | 1d769e02b3baba54246c942fe116abaf850892db (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/byterun/coq_instruct.h')
-rw-r--r-- | kernel/byterun/coq_instruct.h | 1 |
1 files changed, 1 insertions, 0 deletions
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, |