ide: Make SIGINT interrupt subprocesses, not just F* computations

The original code was an attempt to do this, but signals sent to the main thread were dropped. Comments in the code explain the new implementation.
FStarLang · Apr 25, 2018 · 417750b · 417750b
1 parent e6804a8
commit 417750b
Showing 1 changed file with 65 additions and 19 deletions.
diff --git a/src/basic/ml/FStar_Util.ml b/src/basic/ml/FStar_Util.ml
@@ -30,7 +30,6 @@ let string_of_time = string_of_float
 exception Impos
 exception NYI of string
 exception HardError of string
-exception Interrupt
 
 let cur_sigint_handler : Sys.signal_behavior ref =
   ref Sys.Signal_default
@@ -143,18 +142,65 @@ let process_read_all_output (p: proc) =
   (* Pass cleanup:false because kill_process closes both fds already. *)
   BatIO.read_all (BatIO.input_channel ~autoclose:true ~cleanup:false p.inc)
 
+(** Feed `stdin` to `p`, and call `reader_fn` in a separate thread to read the
+    response.
+
+    Signal handling makes this function fairly hairy.  The usual design is to
+    launch a reader thread, then write to the process on the main thread and use
+    `Thread.join` to wait for the reader to complete.
+
+    When we get a signal, Caml routes it to either of the threads.  If it
+    reaches the reader thread, we're good: the reader thread is most likely
+    waiting in input_line at that point, and input_line polls for signals fairly
+    frequently.  If the signal reaches the writer (main) thread, on the other
+    hand, we're toast: `Thread.join` isn't interruptible, so Caml will save the
+    signal until the child tread exits and `join` returns, and at that point the
+    Z3 query is complete and the signal is useless.
+
+    There are three possible solutions to this problem:
+    1. Use an interruptible version of Thread.join written in C
+    2. Ensure that signals are always delivered to the reader thread
+    3. Use a different synchronization mechanism between th reader and the writer.
+
+    Option 1 is bad because building F* doesn't currently require a C compiler.
+    Option 2 is easy to implement with `Unix.sigprocmask`, but that isn't
+    available on Windows.  Option 3 is what the code below does: it uses a pipe
+    and a 1-byte write as a way for the writer thread to wait on the reader
+    thread.  That's what `reader_fn` is passed a `signal_exit` function.
+
+    If a SIGINT reaches the reader, it should still call `signal_exit`.  If
+    a SIGINT reaches the writer, it should make sure that the reader exits.
+    These two things are the responsibility of the caller of this function. **)
+
 let process_read_async p stdin reader_fn =
-  let child_thread = Thread.create reader_fn () in
-  (match stdin with
-   | Some s -> output_string p.outc s; flush p.outc
-   | None -> ());
-  Thread.join child_thread
+  let fd_r, fd_w = Unix.pipe () in
+  BatPervasives.finally (fun () -> Unix.close fd_w; Unix.close fd_r)
+    (fun () ->
+      let wait_for_exit () =
+        ignore (Unix.read fd_r (Bytes.create 1) 0 1) in
+      let signal_exit () =
+        try ignore (Unix.write fd_w (Bytes.create 1) 0 1)
+        with (* ‘write’ will fail if called after the finalizer above *)
+        | Unix.Unix_error (Unix.EBADF, _, _) -> () in
+
+      let write_input = function
+        | Some str -> output_string p.outc str; flush p.outc
+        | None -> () in
+
+      (* In the following we can get a signal at any point; it's the caller's
+         responsibility to ensure that reader_fn will exit in that case *)
+      let t = Thread.create reader_fn signal_exit in
+      write_input stdin;
+      wait_for_exit ();
+      Thread.join t) ()
 
 let run_process (id: string) (prog: string) (args: string list) (stdin: string option): string =
   let p = start_process' id prog args None in
   let output = ref "" in
-  process_read_async p stdin (fun () -> output := process_read_all_output p);
-  kill_process p;
+  let reader_fn signal_fn =
+    output := process_read_all_output p; signal_fn () in
+  BatPervasives.finally (fun () -> kill_process p)
+    (fun () -> process_read_async p stdin reader_fn) ();
   !output
 
 type read_result = EOF | SIGINT
@@ -166,25 +212,25 @@ let ask_process
   let out = Buffer.create 16 in
   let stop_marker = BatOption.default (fun s -> false) p.stop_marker in
 
-  let reader_fn () =
+  let reader_fn signal_fn =
     let rec loop p out =
-      let s = BatString.trim (input_line p.inc) in (* raises EOF *)
-      if stop_marker s then ()
-      else (Buffer.add_string out (s ^ "\n"); loop p out) in
-
-    try loop p out;
-    with | SigInt -> result := Some SIGINT
-         | End_of_file -> result := Some EOF in
+      let line = BatString.trim (input_line p.inc) in (* raises EOF *)
+      if not (stop_marker line) then
+        (Buffer.add_string out (line ^ "\n"); loop p out) in
+    (try loop p out
+     with | SigInt -> result := Some SIGINT
+          | End_of_file -> result := Some EOF);
+    signal_fn () in
 
   try
     process_read_async p (Some stdin) reader_fn;
     (match !result with
      | Some EOF -> kill_process p; Buffer.add_string out (exn_handler ())
-     | Some SIGINT -> raise SigInt (* Though this thread should have received it as well *)
+     | Some SIGINT -> raise SigInt
      | None -> ());
     Buffer.contents out
-  with SigInt ->
-    kill_process p; raise SigInt
+  with e -> (* Ensure that reader_fn gets an EOF and exits *)
+    kill_process p; raise e
 
 let get_file_extension (fn:string) : string = snd (BatString.rsplit fn ".")
 let is_path_absolute path_str =