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