--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/watcher.ML Fri Jun 29 18:21:25 2007 +0200
@@ -0,0 +1,402 @@
+(* Title: Watcher.ML
+ ID: $Id$
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+ *)
+
+(* The watcher process starts a resolution process when it receives a *)
+(* message from Isabelle *)
+(* Signals Isabelle, puts output of child into pipe to Isabelle, *)
+(* and removes dead processes. Also possible to kill all the resolution *)
+(* processes currently running. *)
+
+signature WATCHER =
+sig
+
+(* Send request to Watcher for multiple spasses to be called for filenames in arg *)
+(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
+
+val callResProvers : TextIO.outstream * (string*string*string*string) list -> unit
+
+(* Send message to watcher to kill resolution provers *)
+val callSlayer : TextIO.outstream -> unit
+
+(* Start a watcher and set up signal handlers*)
+val createWatcher :
+ Proof.context * thm * string Vector.vector list ->
+ TextIO.instream * TextIO.outstream * Posix.Process.pid
+val killWatcher : Posix.Process.pid -> unit
+val killChild : ('a, 'b) Unix.proc -> OS.Process.status
+val command_sep : char
+val setting_sep : char
+val reapAll : unit -> unit
+end
+
+
+
+structure Watcher: WATCHER =
+struct
+
+(*Field separators, used to pack items onto a text line*)
+val command_sep = #"\t"
+and setting_sep = #"%";
+
+val goals_being_watched = ref 0;
+
+val trace_path = Path.basic "watcher_trace";
+
+fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
+ else ();
+
+(*Representation of a watcher process*)
+type proc = {pid : Posix.Process.pid,
+ instr : TextIO.instream,
+ outstr : TextIO.outstream};
+
+(*Representation of a child (ATP) process*)
+type cmdproc = {
+ prover: string, (* Name of the resolution prover used, e.g. "spass"*)
+ file: string, (* The file containing the goal for the ATP to prove *)
+ proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
+ instr : TextIO.instream, (*Output of the child process *)
+ outstr : TextIO.outstream}; (*Input to the child process *)
+
+
+fun fdReader (name : string, fd : Posix.IO.file_desc) =
+ Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
+
+fun fdWriter (name, fd) =
+ Posix.IO.mkTextWriter {
+ appendMode = false,
+ initBlkMode = true,
+ name = name,
+ chunkSize=4096,
+ fd = fd};
+
+fun openOutFD (name, fd) =
+ TextIO.mkOutstream (
+ TextIO.StreamIO.mkOutstream (
+ fdWriter (name, fd), IO.BLOCK_BUF));
+
+fun openInFD (name, fd) =
+ TextIO.mkInstream (
+ TextIO.StreamIO.mkInstream (
+ fdReader (name, fd), ""));
+
+
+(* Send request to Watcher for a vampire to be called for filename in arg*)
+fun callResProver (toWatcherStr, arg) =
+ (TextIO.output (toWatcherStr, arg^"\n");
+ TextIO.flushOut toWatcherStr)
+
+(* Send request to Watcher for multiple provers to be called*)
+fun callResProvers (toWatcherStr, []) =
+ (TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr)
+ | callResProvers (toWatcherStr,
+ (prover,proverCmd,settings,probfile) :: args) =
+ (trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile]));
+ (*Uses a special character to separate items sent to watcher*)
+ TextIO.output (toWatcherStr,
+ space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]);
+ inc goals_being_watched;
+ TextIO.flushOut toWatcherStr;
+ callResProvers (toWatcherStr,args))
+
+
+(*Send message to watcher to kill currently running vampires. NOT USED and possibly
+ buggy. Note that killWatcher kills the entire process group anyway.*)
+fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n");
+ TextIO.flushOut toWatcherStr)
+
+
+(* Get commands from Isabelle*)
+fun getCmds (toParentStr, fromParentStr, cmdList) =
+ let val thisLine = the_default "" (TextIO.inputLine fromParentStr)
+ in
+ trace("\nGot command from parent: " ^ thisLine);
+ if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
+ else if thisLine = "Kill children\n"
+ then (TextIO.output (toParentStr,thisLine);
+ TextIO.flushOut toParentStr;
+ [("","Kill children",[],"")])
+ else
+ let val [prover,proverCmd,settingstr,probfile,_] =
+ String.tokens (fn c => c = command_sep) thisLine
+ val settings = String.tokens (fn c => c = setting_sep) settingstr
+ in
+ trace ("\nprover: " ^ prover ^ " prover path: " ^ proverCmd ^
+ "\n problem file: " ^ probfile);
+ getCmds (toParentStr, fromParentStr,
+ (prover, proverCmd, settings, probfile)::cmdList)
+ end
+ handle Bind =>
+ (trace "\ngetCmds: command parsing failed!";
+ getCmds (toParentStr, fromParentStr, cmdList))
+ end
+
+
+(*Get Io-descriptor for polling of an input stream*)
+fun getInIoDesc someInstr =
+ let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
+ val _ = TextIO.output (TextIO.stdOut, buf)
+ val ioDesc =
+ case rd
+ of TextPrimIO.RD{ioDesc = SOME iod, ...} => SOME iod
+ | _ => NONE
+ in (* since getting the reader will have terminated the stream, we need
+ * to build a new stream. *)
+ TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
+ ioDesc
+ end
+
+fun pollChild fromStr =
+ case getInIoDesc fromStr of
+ SOME iod =>
+ (case OS.IO.pollDesc iod of
+ SOME pd =>
+ let val pd' = OS.IO.pollIn pd in
+ case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
+ [] => false
+ | pd''::_ => OS.IO.isIn pd''
+ end
+ | NONE => false)
+ | NONE => false
+
+
+(*************************************)
+(* Set up a Watcher Process *)
+(*************************************)
+
+fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
+
+val killChildren = List.app (ignore o killChild o #proc_handle) : cmdproc list -> unit;
+
+fun killWatcher (toParentStr, procList) =
+ (trace "\nWatcher timeout: Killing proof processes";
+ TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
+ TextIO.flushOut toParentStr;
+ killChildren procList;
+ Posix.Process.exit 0w0);
+
+(* take an instream and poll its underlying reader for input *)
+fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) =
+ case OS.IO.pollDesc fromParentIOD of
+ SOME pd =>
+ (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
+ [] => NONE
+ | pd''::_ => if OS.IO.isIn pd''
+ then SOME (getCmds (toParentStr, fromParentStr, []))
+ else NONE)
+ | NONE => NONE;
+
+(*get the number of the subgoal from the filename: the last digit string*)
+fun number_from_filename s =
+ let val numbers = "xxx" :: String.tokens (not o Char.isDigit) s
+ in valOf (Int.fromString (List.last numbers)) end
+ handle Option => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
+ error ("Watcher could not read subgoal nunber! " ^ s));
+
+(*Call ATP. Settings should be a list of strings ["-t 300", "-m 100000"],
+ which we convert below to ["-t", "300", "-m", "100000"] using String.tokens.
+ Otherwise, the SML/NJ version of Unix.execute will escape the spaces, and
+ Vampire will reject the switches.*)
+fun execCmds [] procList = procList
+ | execCmds ((prover,proverCmd,settings,file)::cmds) procList =
+ let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
+ val settings' = List.concat (map (String.tokens Char.isSpace) settings)
+ val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc =
+ Unix.execute(proverCmd, settings' @ [file])
+ val (instr, outstr) = Unix.streamsOf childhandle
+ val newProcList = {prover=prover, file=file, proc_handle=childhandle,
+ instr=instr, outstr=outstr} :: procList
+ val _ = trace ("\nFinished at " ^
+ Date.toString(Date.fromTimeLocal(Time.now())))
+ in execCmds cmds newProcList end
+
+fun checkChildren (ctxt, th, thm_names_list) toParentStr children =
+ let fun check [] = [] (* no children to check *)
+ | check (child::children) =
+ let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child
+ val _ = trace ("\nprobfile = " ^ file)
+ val sgno = number_from_filename file (*subgoal number*)
+ val thm_names = List.nth(thm_names_list, sgno-1);
+ val ppid = Posix.ProcEnv.getppid()
+ in
+ if pollChild childIn
+ then (* check here for prover label on child*)
+ let val _ = trace ("\nInput available from child: " ^ file)
+ val childDone = (case prover of
+ "vampire" => ResReconstruct.checkVampProofFound
+ (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
+ | "E" => ResReconstruct.checkEProofFound
+ (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
+ | "spass" => ResReconstruct.checkSpassProofFound
+ (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
+ | _ => (trace ("\nBad prover! " ^ prover); true) )
+ in
+ if childDone (*ATP has reported back (with success OR failure)*)
+ then (Unix.reap proc_handle;
+ if !Output.debugging then () else OS.FileSys.remove file;
+ check children)
+ else child :: check children
+ end
+ else (trace "\nNo child output"; child :: check children)
+ end
+ in
+ trace ("\nIn checkChildren, length of queue: " ^ Int.toString(length children));
+ check children
+ end;
+
+
+fun setupWatcher (ctxt, th, thm_names_list) =
+ let
+ val checkc = checkChildren (ctxt, th, thm_names_list)
+ val p1 = Posix.IO.pipe() (*pipes for communication between parent and watcher*)
+ val p2 = Posix.IO.pipe()
+ (****** fork a watcher process and get it set up and going ******)
+ fun startWatcher procList =
+ case Posix.Process.fork() of
+ SOME pid => pid (* parent - i.e. main Isabelle process *)
+ | NONE =>
+ let (* child - i.e. watcher *)
+ val oldchildin = #infd p1
+ val fromParent = Posix.FileSys.wordToFD 0w0
+ val oldchildout = #outfd p2
+ val toParent = Posix.FileSys.wordToFD 0w1
+ val fromParentIOD = Posix.FileSys.fdToIOD fromParent
+ val fromParentStr = openInFD ("_exec_in_parent", fromParent)
+ val toParentStr = openOutFD ("_exec_out_parent", toParent)
+ val pid = Posix.ProcEnv.getpid()
+ val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
+ (*set process group id: allows killing all children*)
+ val () = trace "\nsubgoals forked to startWatcher"
+ val limit = ref 200; (*don't let watcher run forever*)
+ (*Watcher Loop : Check running ATP processes for output*)
+ fun keepWatching procList =
+ (trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^
+ " length(procList) = " ^ Int.toString(length procList));
+ OS.Process.sleep (Time.fromMilliseconds 100); limit := !limit - 1;
+ if !limit < 0 then killWatcher (toParentStr, procList)
+ else
+ case pollParentInput(fromParentIOD, fromParentStr, toParentStr) of
+ SOME [(_,"Kill children",_,_)] =>
+ (trace "\nReceived Kill command";
+ killChildren procList; keepWatching [])
+ | SOME cmds => (* deal with commands from Isabelle process *)
+ let val _ = trace("\nCommands from parent: " ^
+ Int.toString(length cmds))
+ val newProcList' = checkc toParentStr (execCmds cmds procList)
+ in trace "\nCommands executed"; keepWatching newProcList' end
+ | NONE => (* No new input from Isabelle *)
+ (trace "\nNothing from parent...";
+ keepWatching(checkc toParentStr procList)))
+ handle exn => (*FIXME: exn handler is too general!*)
+ (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
+ keepWatching procList);
+ in
+ (*** Sort out pipes ********)
+ Posix.IO.close (#outfd p1); Posix.IO.close (#infd p2);
+ Posix.IO.dup2{old = oldchildin, new = fromParent};
+ Posix.IO.close oldchildin;
+ Posix.IO.dup2{old = oldchildout, new = toParent};
+ Posix.IO.close oldchildout;
+ keepWatching (procList)
+ end;
+
+ val _ = TextIO.flushOut TextIO.stdOut
+ val pid = startWatcher []
+ (* communication streams to watcher*)
+ val instr = openInFD ("_exec_in", #infd p2)
+ val outstr = openOutFD ("_exec_out", #outfd p1)
+ in
+ (* close the child-side fds*)
+ Posix.IO.close (#outfd p2); Posix.IO.close (#infd p1);
+ (* set the fds close on exec *)
+ Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
+ Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
+ {pid = pid, instr = instr, outstr = outstr}
+ end;
+
+
+
+(**********************************************************)
+(* Start a watcher and set up signal handlers *)
+(**********************************************************)
+
+(*Signal handler to tidy away zombie processes*)
+fun reapAll() =
+ (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
+ SOME _ => reapAll() | NONE => ())
+ handle OS.SysErr _ => ()
+
+(*FIXME: does the main process need something like this?
+ IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*)
+
+fun killWatcher pid =
+ (goals_being_watched := 0;
+ Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
+ reapAll());
+
+fun reapWatcher(pid, instr, outstr) = ignore
+ (TextIO.closeIn instr; TextIO.closeOut outstr;
+ Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
+ handle OS.SysErr _ => ()
+
+fun string_of_subgoal th i =
+ string_of_cterm (List.nth(cprems_of th, i-1))
+ handle Subscript => "Subgoal number out of range!"
+
+fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))
+
+fun read_proof probfile =
+ let val p = ResReconstruct.txt_path probfile
+ val _ = trace("\nReading proof from file " ^ Path.implode p)
+ val msg = File.read p
+ val _ = trace("\nProof:\n" ^ msg)
+ in if !Output.debugging then () else File.rm p; msg end;
+
+fun createWatcher (ctxt, th, thm_names_list) =
+ let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list)
+ fun decr_watched() =
+ (goals_being_watched := !goals_being_watched - 1;
+ if !goals_being_watched = 0
+ then
+ (Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid));
+ killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
+ else ())
+ fun proofHandler _ =
+ let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid)
+ val outcome = valOf (TextIO.inputLine childin)
+ handle Option => error "watcher: \"outcome\" line is missing"
+ val probfile = valOf (TextIO.inputLine childin)
+ handle Option => error "watcher: \"probfile\" line is missing"
+ val sgno = number_from_filename probfile
+ val text = string_of_subgoal th sgno
+ fun report s = priority ("Subgoal " ^ Int.toString sgno ^ ": " ^ s);
+ in
+ Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^
+ "\"\nprobfile = " ^ probfile ^
+ "\nGoals being watched: "^ Int.toString (!goals_being_watched)));
+ if String.isPrefix "Invalid" outcome
+ then (report ("Subgoal is not provable:\n" ^ text);
+ decr_watched())
+ else if String.isPrefix "Failure" outcome
+ then (report ("Proof attempt failed:\n" ^ text);
+ decr_watched())
+ (* print out a list of rules used from clasimpset*)
+ else if String.isPrefix "Success" outcome
+ then (report (read_proof probfile ^ "\n" ^ text);
+ decr_watched())
+ (* if proof translation failed *)
+ else if String.isPrefix "Translation failed" outcome
+ then (report (outcome ^ text);
+ decr_watched())
+ else (report "System error in proof handler";
+ decr_watched())
+ end
+ in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th));
+ IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
+ (childin, childout, childpid)
+ end
+
+end (* structure Watcher *)