Skip to content

Commit

Permalink
Stash the bytecode interpreter's internal structures when OCaml's run…
Browse files Browse the repository at this point in the history
…time is processing a signal.

Not doing so would cause the garbage collector to silently move the
carpet from under our feet, thus causing a memory corruption. The
chance it might have happened in the past is extremely low, because
it would have required a memory shortage at the exact time a signal
was processed. Something might have changed in the runtime of OCaml
5.1 that makes this conjunction of events more likely to occur,
e.g., systematically performing a collection before or after
processing a signal.

Note that using Setup_for_caml_call rather than Setup_for_gc might
be sufficient here, since "accu" is almost certainly always
irrelevant here (function application). But since performance does
not matter on this path, better safe than sorry.
  • Loading branch information
silene authored and louiseddp committed Feb 27, 2024
1 parent 9380a3d commit 4ec89c7
Showing 1 changed file with 6 additions and 0 deletions.
6 changes: 6 additions & 0 deletions kernel/byterun/coq_interp.c
Original file line number Diff line number Diff line change
Expand Up @@ -571,20 +571,26 @@ value coq_interprete
/* We also check for signals */
#if OCAML_VERSION >= 50000
if (Caml_check_gc_interrupt(Caml_state)) {
Setup_for_gc;
value res = caml_process_pending_actions_exn();
Handle_potential_exception(res);
Restore_after_gc;
}
#elif OCAML_VERSION >= 41000
if (caml_something_to_do) {
Setup_for_gc;
value res = caml_process_pending_actions_exn();
Handle_potential_exception(res);
Restore_after_gc;
}
#else
if (caml_signals_are_pending) {
/* If there's a Ctrl-C, we reset the vm */
intnat sigint = caml_pending_signals[SIGINT];
if (sigint) { coq_sp = coq_stack_high; }
Setup_for_gc;
caml_process_pending_signals();
Restore_after_gc;
if (sigint) {
caml_failwith("Coq VM: Fatal error: SIGINT signal detected "
"but no exception was raised");
Expand Down

0 comments on commit 4ec89c7

Please sign in to comment.