From 86eda408ad28a80a33ae31743e9ae77ceb7967c2 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 1 Apr 2011 13:17:13 +0000 Subject: Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental) We simply reuse the ocaml flag caml_signals_are_pending and the function caml_process_pending_signals, and place a test at some place of the interpreter loop (at a similar location as in ocaml byterun/interp.c). The symbols caml_* we use are not officially made public in *.h installed alongside ocaml, but they seem pretty stable (there since at least ocaml 3.10, independent of arch and of byte/asm), so we access them via "extern". For once, thanks dirty C... In addition to that, when catching a Ctrl-C, we reset the vm via "coq_sp = coq_stack_high" as suggested by Benjamin G. This patch should be quite portable, it might even work in win32. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13947 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/byterun/coq_interp.c | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a45183f30..842ac5619 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -14,6 +14,7 @@ for fast computation of bounded (31bits) integers */ #include +#include #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -150,6 +151,12 @@ sp is a local copy of the global variable extern_sp. */ #endif #endif +/* For signal handling, we highjack some code from the caml runtime */ + +extern intnat caml_signals_are_pending; +extern intnat caml_pending_signals[]; +extern void caml_process_pending_signals(void); + /* The interpreter itself */ value coq_interprete @@ -407,8 +414,13 @@ value coq_interprete realloc_coq_stack(Coq_stack_threshold); sp = coq_sp; } + /* We also check for signals */ + if (caml_signals_are_pending) { + /* If there's a Ctrl-C, we reset the vm */ + if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; } + caml_process_pending_signals(); + } Next; - /* Fall through CHECK_SIGNALS */ Instruct(APPTERM) { int nargs = *pc++; -- cgit v1.2.3