src/HOL/Tools/ATP/watcher.ML
author paulson
Thu Oct 06 10:14:22 2005 +0200 (2005-10-06)
changeset 17772 818cec5f82a4
parent 17764 fde495b9e24b
child 17773 a7258e1020b7
permissions -rw-r--r--
major simplification: removal of the goalstring argument
     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 :
    20     TextIO.outstream * (string*string*string*string) list -> unit
    21 
    22 (* Send message to watcher to kill resolution provers *)
    23 val callSlayer : TextIO.outstream -> unit
    24 
    25 (* Start a watcher and set up signal handlers             *)
    26 val createWatcher : 
    27     thm * (ResClause.clause * thm) Array.array -> 
    28     TextIO.instream * TextIO.outstream * Posix.Process.pid
    29 val killWatcher : Posix.Process.pid -> unit
    30 val setting_sep : char
    31 end
    32 
    33 
    34 
    35 structure Watcher: WATCHER =
    36 struct
    37 
    38 (*Field separators, used to pack items onto a text line*)
    39 val command_sep = #"\t"
    40 and setting_sep = #"%";
    41 
    42 open Recon_Transfer
    43 
    44 val goals_being_watched = ref 0;
    45 
    46 val trace_path = Path.basic "watcher_trace";
    47 
    48 fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
    49               else ();
    50 
    51 (*  The result of calling createWatcher  *)
    52 datatype proc = PROC of {pid : Posix.Process.pid,
    53 			 instr : TextIO.instream,
    54 			 outstr : TextIO.outstream};
    55 
    56 (*  The result of calling executeToList  *)
    57 datatype cmdproc = CMDPROC of {
    58         prover: string,       (* Name of the resolution prover used, e.g. Vampire*)
    59         cmd:  string,         (* The file containing the goal for res prover to prove *)     
    60         proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    61         instr : TextIO.instream,   (*  Input stream to child process *)
    62         outstr : TextIO.outstream};  (*  Output stream from 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 fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
    87 
    88 fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
    89 
    90 fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
    91 
    92 fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,instr,outstr}) = 
    93   (prover,(cmd, (instr,outstr)));
    94 
    95 fun cmdchildHandle (CMDPROC{prover,cmd,proc_handle,instr,outstr})  = 
    96   proc_handle;
    97 
    98 fun cmdProver (CMDPROC{prover,cmd,proc_handle,instr,outstr}) = prover;
    99 
   100 
   101 (*    gets individual args from instream and concatenates them into a list      *)
   102 fun getArgs (fromParentStr, toParentStr, ys) =  
   103   let val thisLine = TextIO.input fromParentStr
   104   in ys@[thisLine] end
   105 
   106                             
   107 (*  Send request to Watcher for a vampire to be called for filename in arg      *)
   108                    
   109 fun callResProver (toWatcherStr,  arg) = 
   110       (TextIO.output (toWatcherStr, arg^"\n"); 
   111        TextIO.flushOut toWatcherStr)
   112 
   113 (*****************************************************************************************)
   114 (*  Send request to Watcher for multiple provers to be called for filenames in arg       *)
   115 (*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
   116 (*****************************************************************************************)
   117 
   118 fun callResProvers (toWatcherStr,  []) = 
   119       (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
   120 |   callResProvers (toWatcherStr,
   121                     (prover,proverCmd,settings,probfile)  ::  args) =
   122       let val _ = trace (space_implode ", " 
   123 		         (["\ncallResProvers:", prover, proverCmd, probfile]))
   124       in TextIO.output (toWatcherStr,
   125                         (*Uses a special character to separate items sent to watcher*)
   126       	                space_implode (str command_sep)
   127                           [prover, proverCmd, settings, probfile, "\n"]);
   128          goals_being_watched := (!goals_being_watched) + 1;
   129 	 TextIO.flushOut toWatcherStr;
   130 	 callResProvers (toWatcherStr,args)
   131       end   
   132                                                 
   133                                     
   134  
   135 
   136 (*Send message to watcher to kill currently running vampires. NOT USED and possibly
   137   buggy. Note that killWatcher kills the entire process group anyway.*)
   138 fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n"); 
   139                             TextIO.flushOut toWatcherStr)
   140 
   141                     
   142 (**************************************************************)
   143 (* Get commands from Isabelle                                 *)
   144 (**************************************************************)
   145 fun getCmds (toParentStr, fromParentStr, cmdList) = 
   146   let val thisLine = TextIO.inputLine fromParentStr 
   147   in
   148      trace("\nGot command from parent: " ^ thisLine);
   149      if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
   150      else if thisLine = "Kill children\n"
   151      then (TextIO.output (toParentStr,thisLine); 
   152 	   TextIO.flushOut toParentStr;
   153 	   [("","Kill children",[],"")])
   154      else
   155        let val [prover,proverCmd,settingstr,probfile,_] = 
   156                    String.tokens (fn c => c = command_sep) thisLine
   157            val settings = String.tokens (fn c => c = setting_sep) settingstr
   158        in
   159            trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd ^
   160                   "\n  problem file: " ^ probfile);
   161            getCmds (toParentStr, fromParentStr, 
   162                     (prover, proverCmd, settings, probfile)::cmdList) 
   163        end
   164        handle Bind => 
   165           (trace "getCmds: command parsing failed!";
   166            getCmds (toParentStr, fromParentStr, cmdList))
   167   end
   168 	    
   169                                                                   
   170 (**************************************************************)
   171 (*  Get Io-descriptor for polling of an input stream          *)
   172 (**************************************************************)
   173 
   174 fun getInIoDesc someInstr = 
   175     let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
   176         val _ = TextIO.output (TextIO.stdOut, buf)
   177         val ioDesc = 
   178 	    case rd
   179 	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
   180 	       | _ => NONE
   181      in (* since getting the reader will have terminated the stream, we need
   182 	 * to build a new stream. *)
   183 	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
   184 	ioDesc
   185     end
   186 
   187 
   188 (*************************************)
   189 (*  Set up a Watcher Process         *)
   190 (*************************************)
   191 
   192 (* for tracing: encloses each string element in brackets. *)
   193 val concat_with_and = space_implode " & " o map (enclose "(" ")");
   194 
   195 fun prems_string_of th = concat_with_and (map string_of_cterm (cprems_of th))
   196 
   197 fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
   198 
   199 fun killChildren procs = List.app (ignore o killChild) procs;
   200 
   201  (*************************************************************)
   202  (* take an instream and poll its underlying reader for input *)
   203  (*************************************************************)
   204  
   205  fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = 
   206    case OS.IO.pollDesc fromParentIOD of
   207       SOME pd =>
   208 	 (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
   209 	      [] => NONE
   210 	    | pd''::_ => if OS.IO.isIn pd''
   211 	 	         then SOME (getCmds (toParentStr, fromParentStr, []))
   212 	 	         else NONE)
   213    | NONE => NONE;
   214 
   215 (*get the number of the subgoal from the filename: the last digit string*)
   216 fun number_from_filename s =
   217   case String.tokens (not o Char.isDigit) s of
   218       [] => (trace ("\nWatcher could not read subgoal nunber! " ^ s); 
   219              raise ERROR)
   220     | numbers => valOf (Int.fromString (List.last numbers));
   221 
   222 fun setupWatcher (thm,clause_arr) = 
   223   let
   224     val p1 = Posix.IO.pipe()   (*pipes for communication between parent and watcher*)
   225     val p2 = Posix.IO.pipe()
   226     fun closep () = 
   227 	 (Posix.IO.close (#outfd p1); Posix.IO.close (#infd p1);
   228 	  Posix.IO.close (#outfd p2); Posix.IO.close (#infd p2))
   229     (****** fork a watcher process and get it set up and going ******)
   230     fun startWatcher procList =
   231      (case  Posix.Process.fork() 
   232       of SOME pid => pid (* parent - i.e. main Isabelle process *)
   233        | NONE => let                (* child - i.e. watcher  *)
   234 	  val oldchildin = #infd p1  
   235 	  val fromParent = Posix.FileSys.wordToFD 0w0
   236 	  val oldchildout = #outfd p2
   237 	  val toParent = Posix.FileSys.wordToFD 0w1
   238 	  val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   239 	  val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   240 	  val toParentStr = openOutFD ("_exec_out_parent", toParent)
   241 	  val pid = Posix.ProcEnv.getpid()
   242 	  val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
   243                    (*set process group id: allows killing all children*)
   244 	  val () = trace "\nsubgoals forked to startWatcher"
   245 	 
   246 	  fun pollChildInput fromStr = 
   247 	     case getInIoDesc fromStr of
   248 	       SOME iod => 
   249 		 (case OS.IO.pollDesc iod of
   250 		    SOME pd =>
   251 			let val pd' = OS.IO.pollIn pd in
   252 			  case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
   253 			      [] => false
   254 			    | pd''::_ => OS.IO.isIn pd''
   255 			end
   256 		   | NONE => false)
   257 	     | NONE => false
   258 
   259 	  (* Check all ATP processes currently running for output                 *)
   260 	  fun checkChildren ([], toParentStr) = []  (* no children to check *)
   261 	  |   checkChildren (childProc::otherChildren, toParentStr) = 
   262 	       let val _ = trace ("\nIn check child, length of queue:"^
   263 			          Int.toString (length (childProc::otherChildren)))
   264 		   val (childInput,childOutput) = cmdstreamsOf childProc
   265 		   val child_handle = cmdchildHandle childProc
   266 		   val childCmd = #1(#2(cmdchildInfo childProc)) (*name of problem file*)
   267 		   val _ = trace ("\nchildCmd = " ^ childCmd)
   268 		   val sg_num = number_from_filename childCmd
   269 		   val childIncoming = pollChildInput childInput
   270 		   val parentID = Posix.ProcEnv.getppid()
   271 		   val prover = cmdProver childProc
   272 	       in 
   273 		 if childIncoming
   274 		 then (* check here for prover label on child*)
   275 		   let val _ = trace ("\nInput available from child: " ^ childCmd ^ 
   276 				      "\nprover is " ^ prover)
   277 		       val childDone = (case prover of
   278 			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID, childCmd, clause_arr)  
   279 		         | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID, childCmd, clause_arr)             
   280 			 | "spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID, childCmd, thm, sg_num,clause_arr)  
   281 			 | _ => (trace "\nBad prover!"; true) )
   282 		    in
   283 		     if childDone
   284 		     then (* child has found a proof and transferred it *)
   285 			(* Remove this child and go on to check others*)
   286 			(Unix.reap child_handle;
   287 			 OS.FileSys.remove childCmd;
   288 			 checkChildren(otherChildren, toParentStr))
   289 		     else (* Keep this child and go on to check others  *)
   290 		       childProc :: checkChildren (otherChildren, toParentStr)
   291 		  end
   292 		else (trace "\nNo child output";
   293 		      childProc::(checkChildren (otherChildren, toParentStr)))
   294 	       end
   295 
   296 	
   297 	(* call resolution processes                                        *)
   298 	(* settings should be a list of strings  ["-t 300", "-m 100000"]    *)
   299 	(* takes list of (string, string, string list, string)list proclist *)
   300 	fun execCmds [] procList = procList
   301 	|   execCmds ((prover,proverCmd,settings,file)::cmds) procList  =
   302 	      let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ 
   303 	                         file)
   304 	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   305 		       Unix.execute(proverCmd, settings@[file])
   306 		  val (instr, outstr) = Unix.streamsOf childhandle
   307 		  val newProcList = CMDPROC{prover = prover,
   308 					    cmd = file,
   309 					    proc_handle = childhandle,
   310 					    instr = instr,
   311 					    outstr = outstr} :: procList
   312      		  val _ = trace ("\nFinished at " ^
   313 			         Date.toString(Date.fromTimeLocal(Time.now())))
   314 	      in execCmds cmds newProcList end
   315 
   316          (******** Watcher Loop ********)
   317          val limit = ref 200;  (*don't let it run forever*)
   318 
   319 	 fun keepWatching (procList) = 
   320 	   let fun loop procList =  
   321 	      let val _ = trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^ 
   322 	                         "  length(procList) = " ^ Int.toString (length procList));
   323 		  val cmdsFromIsa = pollParentInput 
   324 				     (fromParentIOD, fromParentStr, toParentStr)
   325 	      in 
   326 		OS.Process.sleep (Time.fromMilliseconds 100);
   327 		limit := !limit - 1;
   328 		if !limit = 0 
   329 		then 
   330 		 (trace "\nTimeout: Killing proof processes";
   331 		  TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   332 		  TextIO.flushOut toParentStr;
   333 		  killChildren (map cmdchildHandle procList);
   334 		  Posix.Process.exit 0w0)
   335 		else case cmdsFromIsa of
   336 		    SOME [(_,"Kill children",_,_)] => 
   337 		      let val child_handles = map cmdchildHandle procList 
   338 		      in  trace "\nReceived command to kill children";
   339 			  killChildren child_handles; loop [] 
   340 		      end
   341 		  | SOME cmds => (*  deal with commands from Isabelle process *)
   342 		      if length procList < 40
   343 		      then                        (* Execute locally  *)
   344 			let 
   345 			  val _ = trace ("\nCommands from parent: " ^ Int.toString(length cmds))
   346 			  val newProcList = execCmds cmds procList
   347 			  val newProcList' = checkChildren (newProcList, toParentStr) 
   348 			in
   349 			  trace "\nCommands executed"; loop newProcList'
   350 			end
   351 		      else  (* Execute remotely [FIXME: NOT REALLY]  *)
   352 			let 
   353 			  val newProcList = execCmds cmds procList
   354 			  val newProcList' = checkChildren (newProcList, toParentStr) 
   355 			in loop newProcList' end
   356 		  | NONE => (* No new input from Isabelle *)
   357 		      let val newProcList = checkChildren (procList, toParentStr)
   358 		      in
   359 			trace "\nNothing from parent, still watching"; loop newProcList
   360 		      end
   361 	       end
   362 	   in  loop procList   end
   363 	 in
   364 	   (*** Sort out pipes ********)
   365 	   Posix.IO.close (#outfd p1);  Posix.IO.close (#infd p2);
   366 	   Posix.IO.dup2{old = oldchildin, new = fromParent};
   367 	   Posix.IO.close oldchildin;
   368 	   Posix.IO.dup2{old = oldchildout, new = toParent};
   369 	   Posix.IO.close oldchildout;
   370 	   keepWatching (procList)
   371 	 end);   (* end case *)
   372 
   373     val _ = TextIO.flushOut TextIO.stdOut
   374     val pid = startWatcher []
   375     (* communication streams to watcher*)
   376     val instr = openInFD ("_exec_in", #infd p2)
   377     val outstr = openOutFD ("_exec_out", #outfd p1)
   378   in
   379    (* close the child-side fds*)
   380     Posix.IO.close (#outfd p2);  Posix.IO.close (#infd p1);
   381     (* set the fds close on exec *)
   382     Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   383     Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   384     PROC{pid = pid, instr = instr, outstr = outstr}
   385   end;
   386 
   387 
   388 
   389 (**********************************************************)
   390 (* Start a watcher and set up signal handlers             *)
   391 (**********************************************************)
   392 
   393 fun killWatcher pid = Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
   394 
   395 fun reapWatcher(pid, instr, outstr) = ignore
   396   (TextIO.closeIn instr; TextIO.closeOut outstr;
   397    Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
   398   handle OS.SysErr _ => ()
   399 
   400 fun string_of_subgoal th i =
   401     string_of_cterm (List.nth(cprems_of th, i-1))
   402     handle Subscript => "Subgoal number out of range!"
   403 
   404 fun createWatcher (th, clause_arr) =
   405  let val (childpid,(childin,childout)) = childInfo (setupWatcher(th,clause_arr))
   406      fun decr_watched() =
   407 	  (goals_being_watched := !goals_being_watched - 1;
   408 	   if !goals_being_watched = 0
   409 	   then 
   410 	     (debug ("\nReaping a watcher, childpid = "^
   411 		     LargeWord.toString (Posix.Process.pidToWord childpid));
   412 	      killWatcher childpid; reapWatcher (childpid,childin, childout))
   413 	    else ())
   414      val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of th);
   415      fun proofHandler n = 
   416        let val outcome = TextIO.inputLine childin
   417 	   val probfile = TextIO.inputLine childin
   418 	   val sg_num = number_from_filename probfile
   419 	   val text = string_of_subgoal th sg_num
   420 	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
   421 		        "\"\nprobfile = " ^ probfile ^
   422 		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
   423        in 
   424 	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
   425 	 then (priority (Recon_Transfer.apply_res_thm outcome);
   426 	       decr_watched())
   427 	 else if String.isPrefix "Invalid" outcome
   428 	 then (priority ("Subgoal is not provable:\n" ^ text);
   429 	       decr_watched())
   430 	 else if String.isPrefix "Failure" outcome
   431 	 then (priority ("Proof attempt failed:\n" ^ text);
   432 	       decr_watched()) 
   433 	(* print out a list of rules used from clasimpset*)
   434 	 else if String.isPrefix "Success" outcome
   435 	 then (priority (outcome ^ text);
   436 	       decr_watched())
   437 	  (* if proof translation failed *)
   438 	 else if String.isPrefix "Translation failed" outcome
   439 	 then (priority (outcome ^ text);
   440 	       decr_watched())
   441 	 else (priority "System error in proof handler";
   442 	       decr_watched())
   443        end
   444  in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
   445     (childin, childout, childpid)
   446   end
   447 
   448 end (* structure Watcher *)