diff options
| -rw-r--r-- | dev/doc/critical-bugs | 12 | ||||
| -rw-r--r-- | doc/changelog/01-kernel/13867-changelog-for-13867.rst | 5 | ||||
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 4 | ||||
| -rwxr-xr-x | test-suite/misc/coqtop_print-mod-uid.sh | 6 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
5 files changed, 27 insertions, 2 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/doc/changelog/01-kernel/13867-changelog-for-13867.rst b/doc/changelog/01-kernel/13867-changelog-for-13867.rst new file mode 100644 index 0000000000..37e44b41c7 --- /dev/null +++ b/doc/changelog/01-kernel/13867-changelog-for-13867.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Fix arities of VM opcodes for some floating-point operations + that could cause memory corruption + (`#13867 <https://github.com/coq/coq/pull/13867>`_, + by Guillaume Melquiond). 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]= diff --git a/test-suite/misc/coqtop_print-mod-uid.sh b/test-suite/misc/coqtop_print-mod-uid.sh new file mode 100755 index 0000000000..db1df4bb4b --- /dev/null +++ b/test-suite/misc/coqtop_print-mod-uid.sh @@ -0,0 +1,6 @@ +#!/usr/bin/env bash + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +[ "$(coqtop -print-mod-uid prerequisite/admit.vo)" = "prerequisite/.coq-native/NTestSuite_admit" ] diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 16028be910..32e942f0d0 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -164,7 +164,7 @@ let init_toploop opts stm_opts injections = state let coqtop_init ({ run_mode; color_mode }, async_opts) injections ~opts = - if run_mode = Batch then Flags.quiet := true; + if run_mode != Interactive then Flags.quiet := true; init_color (if opts.config.print_emacs then `EMACS else color_mode); Flags.if_verbose print_header (); init_toploop opts async_opts injections |