src/HOL/Tools/watcher.ML
author wenzelm
Thu Mar 27 14:41:09 2008 +0100 (2008-03-27)
changeset 26424 a6cad32a27b0
parent 25551 87d89b0f847a
child 26928 ca87aff1ad2d
permissions -rw-r--r--
eliminated theory ProtoPure;
     1 (*  Title:      HOL/Tools/watcher.ML
     2     ID:         $Id$
     3     Author:     Claire Quigley
     4     Copyright   2004  University of Cambridge
     5  *)
     6 
     7 (*  The watcher process starts a resolution process when it receives a     *)
     8 (*  message from Isabelle                                                  *)
     9 (*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
    10 (*  and removes dead processes.  Also possible to kill all the resolution  *)
    11 (*  processes currently running.                                           *)
    12 
    13 signature WATCHER =
    14 sig
    15 
    16 (*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
    17 (* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
    18 
    19 val callResProvers : TextIO.outstream * (string*string*string*string) list -> unit
    20 
    21 (* Send message to watcher to kill resolution provers *)
    22 val callSlayer : TextIO.outstream -> unit
    23 
    24 (* Start a watcher and set up signal handlers*)
    25 val createWatcher : 
    26 	Proof.context * thm * string Vector.vector list ->
    27 	TextIO.instream * TextIO.outstream * Posix.Process.pid
    28 val killWatcher : Posix.Process.pid -> unit
    29 val killChild  : ('a, 'b) Unix.proc -> OS.Process.status
    30 val command_sep : char
    31 val setting_sep : char
    32 val reapAll : unit -> unit
    33 end
    34 
    35 
    36 
    37 structure Watcher: WATCHER =
    38 struct
    39 
    40 (*Field separators, used to pack items onto a text line*)
    41 val command_sep = #"\t"
    42 and setting_sep = #"%";
    43 
    44 val goals_being_watched = ref 0;
    45 
    46 val trace_path = Path.basic "watcher_trace";
    47 
    48 fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
    49               else ();
    50 
    51 (*Representation of a watcher process*)
    52 type proc = {pid : Posix.Process.pid,
    53              instr : TextIO.instream,
    54              outstr : TextIO.outstream};
    55 
    56 (*Representation of a child (ATP) process*)
    57 type cmdproc = {
    58         prover: string,       (* Name of the resolution prover used, e.g. "spass"*)
    59         file:  string,        (* The file containing the goal for the ATP to prove *)
    60         proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    61         instr : TextIO.instream,     (*Output of the child process *)
    62         outstr : TextIO.outstream};  (*Input to the child process *)
    63 
    64 
    65 fun fdReader (name : string, fd : Posix.IO.file_desc) =
    66 	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    67 
    68 fun fdWriter (name, fd) =
    69           Posix.IO.mkTextWriter {
    70 	      appendMode = false,
    71               initBlkMode = true,
    72               name = name,
    73               chunkSize=4096,
    74               fd = fd};
    75 
    76 fun openOutFD (name, fd) =
    77 	  TextIO.mkOutstream (
    78 	    TextIO.StreamIO.mkOutstream (
    79 	      fdWriter (name, fd), IO.BLOCK_BUF));
    80 
    81 fun openInFD (name, fd) =
    82 	  TextIO.mkInstream (
    83 	    TextIO.StreamIO.mkInstream (
    84 	      fdReader (name, fd), ""));
    85 
    86 
    87 (*  Send request to Watcher for a vampire to be called for filename in arg*)
    88 fun callResProver (toWatcherStr,  arg) =
    89       (TextIO.output (toWatcherStr, arg^"\n");
    90        TextIO.flushOut toWatcherStr)
    91 
    92 (*  Send request to Watcher for multiple provers to be called*)
    93 fun callResProvers (toWatcherStr,  []) =
    94       (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
    95   | callResProvers (toWatcherStr,
    96                     (prover,proverCmd,settings,probfile)  ::  args) =
    97       (trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile]));
    98        (*Uses a special character to separate items sent to watcher*)
    99        TextIO.output (toWatcherStr,
   100           space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]);
   101        inc goals_being_watched;
   102        TextIO.flushOut toWatcherStr;
   103        callResProvers (toWatcherStr,args))
   104 
   105 
   106 (*Send message to watcher to kill currently running vampires. NOT USED and possibly
   107   buggy. Note that killWatcher kills the entire process group anyway.*)
   108 fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n");
   109                             TextIO.flushOut toWatcherStr)
   110 
   111 
   112 (* Get commands from Isabelle*)
   113 fun getCmds (toParentStr, fromParentStr, cmdList) =
   114   let val thisLine = the_default "" (TextIO.inputLine fromParentStr)
   115   in
   116      trace("\nGot command from parent: " ^ thisLine);
   117      if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
   118      else if thisLine = "Kill children\n"
   119      then (TextIO.output (toParentStr,thisLine);
   120 	   TextIO.flushOut toParentStr;
   121 	   [("","Kill children",[],"")])
   122      else
   123        let val [prover,proverCmd,settingstr,probfile,_] =
   124                    String.tokens (fn c => c = command_sep) thisLine
   125            val settings = String.tokens (fn c => c = setting_sep) settingstr
   126        in
   127            trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd ^
   128                   "\n  problem file: " ^ probfile);
   129            getCmds (toParentStr, fromParentStr,
   130                     (prover, proverCmd, settings, probfile)::cmdList)
   131        end
   132        handle Bind =>
   133           (trace "\ngetCmds: command parsing failed!";
   134            getCmds (toParentStr, fromParentStr, cmdList))
   135   end
   136 	
   137 
   138 (*Get Io-descriptor for polling of an input stream*)
   139 fun getInIoDesc someInstr =
   140     let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
   141         val _ = TextIO.output (TextIO.stdOut, buf)
   142         val ioDesc =
   143 	    case rd
   144 	      of TextPrimIO.RD{ioDesc = SOME iod, ...} => SOME iod
   145 	       | _ => NONE
   146      in (* since getting the reader will have terminated the stream, we need
   147 	 * to build a new stream. *)
   148 	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
   149 	ioDesc
   150     end
   151 
   152 fun pollChild fromStr =
   153    case getInIoDesc fromStr of
   154      SOME iod =>
   155        (case OS.IO.pollDesc iod of
   156 	  SOME pd =>
   157 	      let val pd' = OS.IO.pollIn pd in
   158 		case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
   159 		    [] => false
   160 		  | pd''::_ => OS.IO.isIn pd''
   161 	      end
   162 	 | NONE => false)
   163    | NONE => false
   164 
   165 
   166 (*************************************)
   167 (*  Set up a Watcher Process         *)
   168 (*************************************)
   169 
   170 fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
   171 
   172 val killChildren = List.app (ignore o killChild o #proc_handle) : cmdproc list -> unit;
   173 
   174 fun killWatcher (toParentStr, procList) =
   175       (trace "\nWatcher timeout: Killing proof processes";
   176        TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   177        TextIO.flushOut toParentStr;
   178        killChildren procList;
   179        Posix.Process.exit 0w0);
   180 
   181 (* take an instream and poll its underlying reader for input *)
   182 fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) =
   183   case OS.IO.pollDesc fromParentIOD of
   184      SOME pd =>
   185 	(case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
   186 	     [] => NONE
   187 	   | pd''::_ => if OS.IO.isIn pd''
   188 			then SOME (getCmds (toParentStr, fromParentStr, []))
   189 			else NONE)
   190   | NONE => NONE;
   191 
   192 (*get the number of the subgoal from the filename: the last digit string*)
   193 fun number_from_filename s =
   194   let val numbers = "xxx" :: String.tokens (not o Char.isDigit) s 
   195   in  valOf (Int.fromString (List.last numbers))  end
   196   handle Option => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
   197                     error ("Watcher could not read subgoal nunber! " ^ s));
   198 
   199 (*Call ATP.  Settings should be a list of strings  ["-t 300", "-m 100000"],
   200   which we convert below to ["-t", "300", "-m", "100000"] using String.tokens.
   201   Otherwise, the SML/NJ version of Unix.execute will escape the spaces, and
   202   Vampire will reject the switches.*)
   203 fun execCmds [] procList = procList
   204   | execCmds ((prover,proverCmd,settings,file)::cmds) procList  =
   205       let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
   206           val settings' = List.concat (map (String.tokens Char.isSpace) settings)
   207 	  val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  =
   208 	       Unix.execute(proverCmd, settings' @ [file])
   209 	  val (instr, outstr) = Unix.streamsOf childhandle
   210 	  val newProcList = {prover=prover, file=file, proc_handle=childhandle,
   211 			     instr=instr, outstr=outstr} :: procList
   212 	  val _ = trace ("\nFinished at " ^
   213 			 Date.toString(Date.fromTimeLocal(Time.now())))
   214       in execCmds cmds newProcList end
   215 
   216 fun checkChildren (ctxt, th, thm_names_list) toParentStr children =
   217   let fun check [] = []  (* no children to check *)
   218 	| check (child::children) =
   219 	   let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child
   220 	       val _ = trace ("\nprobfile = " ^ file)
   221 	       val i = number_from_filename file  (*subgoal number*)
   222 	       val thm_names = List.nth(thm_names_list, i-1);
   223 	       val ppid = Posix.ProcEnv.getppid()
   224 	   in
   225 	     if pollChild childIn
   226 	     then (* check here for prover label on child*)
   227 	       let val _ = trace ("\nInput available from child: " ^ file)
   228 		   val childDone = (case prover of
   229 		       "vampire" => ResReconstruct.checkVampProofFound
   230 			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
   231 		     | "E" => ResReconstruct.checkEProofFound
   232 			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
   233 		     | "spass" => ResReconstruct.checkSpassProofFound
   234 			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
   235 		     | _ => (trace ("\nBad prover! " ^ prover); true) )
   236 		in
   237 		 if childDone (*ATP has reported back (with success OR failure)*)
   238 		 then (Unix.reap proc_handle;
   239 		       if !Output.debugging then () else OS.FileSys.remove file;
   240 		       check children)
   241 		 else child :: check children
   242 	      end
   243 	    else (trace "\nNo child output";  child :: check children)
   244 	   end
   245   in
   246     trace ("\nIn checkChildren, length of queue: " ^  Int.toString(length children));
   247     check children
   248   end;
   249 
   250 
   251 fun setupWatcher (ctxt, th, thm_names_list) =
   252   let
   253     val checkc = checkChildren (ctxt, th, thm_names_list)
   254     val p1 = Posix.IO.pipe()   (*pipes for communication between parent and watcher*)
   255     val p2 = Posix.IO.pipe()
   256     (****** fork a watcher process and get it set up and going ******)
   257     fun startWatcher procList =
   258       case  Posix.Process.fork() of
   259          SOME pid => pid (* parent - i.e. main Isabelle process *)
   260        | NONE =>
   261           let            (* child - i.e. watcher  *)
   262 	    val oldchildin = #infd p1
   263 	    val fromParent = Posix.FileSys.wordToFD 0w0
   264 	    val oldchildout = #outfd p2
   265 	    val toParent = Posix.FileSys.wordToFD 0w1
   266 	    val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   267 	    val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   268 	    val toParentStr = openOutFD ("_exec_out_parent", toParent)
   269 	    val pid = Posix.ProcEnv.getpid()
   270 	    val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
   271 		     (*set process group id: allows killing all children*)
   272 	    val () = trace "\nsubgoals forked to startWatcher"
   273 	    val limit = ref 200;  (*don't let watcher run forever*)
   274 	    (*Watcher Loop : Check running ATP processes for output*)
   275 	    fun keepWatching procList =
   276 	      (trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^
   277 				"  length(procList) = " ^ Int.toString(length procList));
   278 	       OS.Process.sleep (Time.fromMilliseconds 100);  limit := !limit - 1;
   279 	       if !limit < 0 then killWatcher (toParentStr, procList)
   280 	       else
   281 	       case pollParentInput(fromParentIOD, fromParentStr, toParentStr) of
   282 		  SOME [(_,"Kill children",_,_)] =>
   283 		    (trace "\nReceived Kill command";
   284 		     killChildren procList; keepWatching [])
   285 		| SOME cmds => (*  deal with commands from Isabelle process *)
   286 		      let val _ = trace("\nCommands from parent: " ^
   287 					Int.toString(length cmds))
   288 			  val newProcList' = checkc toParentStr (execCmds cmds procList)
   289 		      in trace "\nCommands executed"; keepWatching newProcList' end
   290 		| NONE => (* No new input from Isabelle *)
   291 		    (trace "\nNothing from parent...";
   292 		     keepWatching(checkc toParentStr procList)))
   293 	     handle exn => (*FIXME: exn handler is too general!*)
   294 	       (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
   295 		keepWatching procList);
   296 	  in
   297 	    (*** Sort out pipes ********)
   298 	    Posix.IO.close (#outfd p1);  Posix.IO.close (#infd p2);
   299 	    Posix.IO.dup2{old = oldchildin, new = fromParent};
   300 	    Posix.IO.close oldchildin;
   301 	    Posix.IO.dup2{old = oldchildout, new = toParent};
   302 	    Posix.IO.close oldchildout;
   303 	    keepWatching (procList)
   304 	  end;
   305 
   306     val _ = TextIO.flushOut TextIO.stdOut
   307     val pid = startWatcher []
   308     (* communication streams to watcher*)
   309     val instr = openInFD ("_exec_in", #infd p2)
   310     val outstr = openOutFD ("_exec_out", #outfd p1)
   311   in
   312    (* close the child-side fds*)
   313     Posix.IO.close (#outfd p2);  Posix.IO.close (#infd p1);
   314     (* set the fds close on exec *)
   315     Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   316     Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   317     {pid = pid, instr = instr, outstr = outstr}
   318   end;
   319 
   320 
   321 
   322 (**********************************************************)
   323 (* Start a watcher and set up signal handlers             *)
   324 (**********************************************************)
   325 
   326 (*Signal handler to tidy away zombie processes*)
   327 fun reapAll() =
   328      (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
   329 	  SOME _ => reapAll() | NONE => ())
   330      handle OS.SysErr _ => ()
   331 
   332 (*FIXME: does the main process need something like this?
   333     IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*)
   334 
   335 fun killWatcher pid =
   336   (goals_being_watched := 0;
   337    Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
   338    reapAll());
   339 
   340 fun reapWatcher(pid, instr, outstr) = ignore
   341   (TextIO.closeIn instr; TextIO.closeOut outstr;
   342    Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
   343   handle OS.SysErr _ => ()
   344 
   345 fun string_of_subgoal th i =
   346     string_of_cterm (List.nth(cprems_of th, i-1))
   347     handle Subscript => "Subgoal number out of range!"
   348 
   349 fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))
   350 
   351 fun read_proof probfile =
   352   let val p = ResReconstruct.txt_path probfile
   353       val _ = trace("\nReading proof from file " ^ Path.implode p)
   354       val msg = File.read p 
   355       val _ = trace("\nProof:\n" ^ msg)
   356   in  if !Output.debugging then () else File.rm p;  msg  end;
   357 
   358 (*Non-successful outcomes*)
   359 fun report i s = priority ("Subgoal " ^ Int.toString i ^ ": " ^ s);
   360 
   361 (*Successful outcome: auto-insertion of commands into the PG buffer. Thanks to D Aspinall!!*)
   362 fun report_success i s sgtx = 
   363   let val sgline = "Subgoal " ^ string_of_int i ^ ":"
   364       val outlines = 
   365 	case split_lines s of
   366 	    [] => ["Received bad string: " ^ s]
   367 	  | line::lines => ["  Try this command:", (*Markup.markup Markup.sendback*) line, ""]
   368 	                   @ lines
   369   in priority (cat_lines (sgline::sgtx::outlines)) end;
   370   
   371 fun createWatcher (ctxt, th, thm_names_list) =
   372  let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list)
   373      fun decr_watched() =
   374 	  (goals_being_watched := !goals_being_watched - 1;
   375 	   if !goals_being_watched = 0
   376 	   then
   377 	     (Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid));
   378 	      killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
   379 	    else ())
   380      fun proofHandler _ =
   381        let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid)
   382            val outcome  = valOf (TextIO.inputLine childin)
   383                           handle Option => error "watcher: \"outcome\" line is missing"
   384 	   val probfile = valOf (TextIO.inputLine childin)
   385                           handle Option => error "watcher: \"probfile\" line is missing"
   386 	   val i = number_from_filename probfile
   387 	   val text = "\n" ^ string_of_subgoal th i
   388        in
   389 	 Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^
   390 		       "\"\nprobfile = " ^ probfile ^
   391 		       "\nGoals being watched: "^  Int.toString (!goals_being_watched)));
   392 	 if String.isPrefix "Invalid" outcome
   393 	 then (report i ("Subgoal is not provable:" ^ text);
   394 	       decr_watched())
   395 	 else if String.isPrefix "Failure" outcome
   396 	 then (report i ("Proof attempt failed:" ^ text);
   397 	       decr_watched())
   398 	(* print out a list of rules used from clasimpset*)
   399 	 else if String.isPrefix "Success" outcome
   400 	 then (report_success i (read_proof probfile) text;
   401 	       decr_watched())
   402 	  (* if proof translation failed *)
   403 	 else if String.isPrefix "Translation failed" outcome
   404 	 then (report i (outcome ^ text);
   405 	       decr_watched())
   406 	 else (report i "System error in proof handler";
   407 	       decr_watched())
   408        end
   409  in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th));
   410     IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
   411     (childin, childout, childpid)
   412   end
   413 
   414 end (* structure Watcher *)