diff options
| author | Pierre-Marie Pédrot | 2021-02-19 10:44:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-02-19 10:44:18 +0100 |
| commit | bbb9876da3093658c9eca206a585b045ed258220 (patch) | |
| tree | 9086466ddacde4c37c2567ff5dde5c38d6770955 | |
| parent | c55b5b8575f2f717d6d9c759996173e250dd1c75 (diff) | |
| parent | c150f3ab8dc9d1824d88b6fb9b1da14cb544ffc7 (diff) | |
Merge PR #13867: Fix missing arities of VM opcodes.
Reviewed-by: ppedrot
| -rw-r--r-- | dev/doc/critical-bugs | 12 | ||||
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 4 |
2 files changed, 15 insertions, 1 deletions
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 79c2155823..4452baf513 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -332,6 +332,18 @@ Conversion machines GH issue number: ocaml/ocaml#6385, #11170 risk: unlikely to be activated by chance, might happen for autogenerated code + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: buffer overflow, arbitrary code execution on floating-point operations + introduced: 8.13 + impacted released versions: 8.13.0 + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: 8.13.1 + found by: Melquiond + GH issue number: #13867 + risk: none, unless using floating-point operations; high otherwise; + noticeable if activated by chance, since it usually breaks + control-flow integrity + Side-effects component: side-effects diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 4bc6848ba7..2c0b580e24 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -70,7 +70,9 @@ void init_arity () { arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]= - arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1; + arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]= + arity[CHECKNEXTUPFLOATINPLACE]=arity[CHECKNEXTDOWNFLOATINPLACE]= + 1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[CHECKCAMLCALL1]=arity[CHECKCAMLCALL2_1]= |