Merge pull request #280 from herd/exc-timeout

[herd] Exception timeout
Use a specific exception for timeouts, in place of the standard `Misc.Exit`.

herd/herd.ml

@@ -671,18 +671,12 @@ let () =
 
 (* If interval timer enabled and triggered,
    then stop test with not output at all *)
-    begin match Config.timeout with
-    | None -> ()
-    | Some _ ->
-        Sys.set_signal
-          26 (* SIGVTALARM *)
-          (Sys.Signal_handle (fun _ -> raise Misc.Exit))
-    end ;
-
+    Itimer.set_signal Config.timeout (fun _ -> raise Misc.Timeout) ;
     Misc.fold_argv_or_stdin
       (fun name seen ->
         try from_file name seen
         with
+        | Misc.Timeout -> seen
         | Misc.Exit -> check_exit seen
         | Misc.Fatal msg ->
             Warn.warn_always "%a: %s" Pos.pp_pos0 name msg ;

herd/itimer.ml

@@ -14,21 +14,43 @@
 (* "http://www.cecill.info". We also give a copy in LICENSE.txt.            *)
 (****************************************************************************)
 
-let start timeout =
+open Unix
+
+let dbg = false
+
+let name = ref ""
+
+let set_signal timeout f =
+  match timeout with
+  | None -> ()
+  | Some _ ->
+     let g =
+       if dbg then
+         fun s ->
+           let n = !name in
+           if n <> "" then Printf.eprintf "Timeout for %s\n%!" n ;
+           f s
+       else f in
+     Sys.set_signal
+       26 (* SIGVTALARM *)
+       (Sys.Signal_handle g)
+
+let start n timeout =
   match timeout with
   | None -> ()
   | Some t ->
-      let open Unix in
-      let it =
-        {it_value=t; it_interval=0.0;} in
-      ignore (setitimer ITIMER_VIRTUAL it)
+     name := n ;
+     if dbg then Printf.eprintf "Start %s\n%!" n ;
+     let it =
+       {it_value=t; it_interval=0.0;} in
+     ignore (setitimer ITIMER_VIRTUAL it)
 
 and stop timeout =
   match timeout with
   | None -> ()
   | Some _ ->
-      let open Unix in
-      let it =
-        {it_value=0.0; it_interval=0.0;} in
-      ignore (setitimer ITIMER_VIRTUAL it)
-
+     if dbg then Printf.eprintf "Stop %s\n%!" !name ;
+     name := "" ;
+     let it =
+       {it_value=0.0; it_interval=0.0;} in
+     ignore (setitimer ITIMER_VIRTUAL it)

herd/itimer.mli

@@ -16,12 +16,17 @@
 
 (** Simple interface to interval timer in virtual processor time *)
 
+
+(** [set_signal timeout handle] set signal handle for timer.
+  * Argument timeout is an option, if [None] do nothing. *)
+val set_signal : float option -> (int -> unit) -> unit
+
 (** [start timeout] start interval for the given period.
   * Argument timeout is an option, if [None] do nothing,
-  * otherwise the option specifies the timer period *)
-val start : float option -> unit
+  * otherwise the option specifies the timer period. *)
+val start : string -> float option -> unit
 
 (** [stop timeout] stop interval timer.
   * Argument timeout is an option, if [None] do nothing,
-  * otherwise stop timer *)
+  * otherwise stop timer. *)
 val stop : float option -> unit

herd/parseTest.ml

@@ -533,7 +533,7 @@ module Top (TopConf:Config) = struct
 
   let from_file name env =
     (* Interval timer will be stopped just before output, see top_herd *)
-    Itimer.start TopConf.timeout ;
+    Itimer.start name TopConf.timeout ;
     let start_time = Sys.time () in
     Misc.input_protect (do_from_file start_time env name) name
 end

herd/valconstraint.ml

@@ -285,7 +285,7 @@ and type state = A.state =
 	   end
          (* Delay failure to preserve potential contradiction *)
          with
-         | Contradiction -> raise Contradiction
+         | Contradiction|Misc.Timeout as e -> raise e
          | e ->
             if C.debug then
               eprintf "Delaying exception in solver: %s\n"

lib/genParserUtils.ml

@@ -34,6 +34,7 @@ let call_parser name lexbuf lex parse =
       let start_loc = lexeme_start_p lexbuf
       and end_loc = lexeme_end_p lexbuf in
       Warn.user_error "%s: %s (in %s)" (Pos.str_pos2 (start_loc, end_loc)) msg name
+  | Misc.Timeout as e -> raise e
   | e ->
       Printf.eprintf
         "%a: Uncaught exception %s (in %s)\n"

lib/misc.ml

@@ -17,6 +17,7 @@
 open Printf
 
 exception Exit
+exception Timeout
 exception UserError of string
 exception Fatal of string
 exception NoIsync

lib/misc.mli

@@ -21,6 +21,7 @@
 (***********************************************************)
 
 exception Exit
+exception Timeout
 exception UserError of string
 exception Fatal of string
 exception NoIsync

litmus/CGenParser_litmus.ml

@@ -35,6 +35,7 @@ let call_parser name lexbuf lex parse =
         Pos.pp_pos2 (start_loc,end_loc)
         lxm name ;
       raise Misc.Exit
+  | Misc.Timeout as e -> raise e
   | e ->
       Printf.eprintf
         "%a: Uncaught exception %s (in %s)\n"