diff --git a/src/driver/call_provers.ml b/src/driver/call_provers.ml index 1b9c4dc4dddab3941f14c481247b7c8c1a66aafe..d91d08958eaf1505043c0f4837b38b150524e22a 100644 --- a/src/driver/call_provers.ml +++ b/src/driver/call_provers.ml @@ -91,23 +91,33 @@ let remove_file ?(debug=false) f = let () = Sys.set_signal Sys.sigpipe Sys.Signal_ignore -let timed_sys_command ?formatter ?(debug=false) ?timeout cmd = +let timed_sys_command ?formatter ?buffer ?(debug=false) ?timeout cmd = let t0 = Unix.times () in let cmd = match timeout with | None -> Format.sprintf "%s 2>&1" cmd | Some timeout -> Format.sprintf "%s %d %s 2>&1" !cpulimit timeout cmd in if debug then Format.eprintf "command line: %s@." cmd; let (cin,cout) as p = Unix.open_process cmd in + (* Write the formatter to the stdin of the prover *) begin try (match formatter with | None -> () | Some formatter -> let fmt = formatter_of_out_channel cout in formatter fmt); - close_out cout; with Sys_error s -> if debug then Format.eprintf "Sys_error : %s@." s end; + (* Write the buffer to the stdin of the prover *) + begin try + (match buffer with + | None -> () + | Some buffer -> + Buffer.output_buffer cout buffer); + with Sys_error s -> + if debug then Format.eprintf "Sys_error : %s@." s + end; + close_out cout; let out = Sysutil.channel_contents cin in let ret = Unix.close_process p in let t1 = Unix.times () in @@ -152,19 +162,25 @@ let treat_result pr (t,c,outerr) = | Unix.WSTOPPED 24 | Unix.WSIGNALED 24 | Unix.WEXITED 124 | Unix.WEXITED 152 -> (* (*128 +*) SIGXCPU signal (i.e. 24, /usr/include/bits/signum.h) *) + (* TODO : if somebody use why_cpulimit to call "why -timeout + 0", Why will think that he called why_cpulimit (WEXITED + 152) and will return Timeout instead of exit 152. In fact + in this case Why will receive a SIGXCPU in less than 1 + sec (soft limit) (ie man setrlimit ). The problem can be + here or in the use of why_cpulimit *) Timeout | Unix.WSTOPPED _ | Unix.WSIGNALED _ -> HighFailure | Unix.WEXITED c -> let rec greps res = function | [] -> HighFailure | (r,pa)::l -> - if grep r res - then match pa with - | Valid | Invalid -> pa - | Unknown s -> Unknown (Str.replace_matched s res) - | Failure s -> Failure (Str.replace_matched s res) - | Timeout | HighFailure -> assert false - else greps outerr l in + if grep r res + then match pa with + | Valid | Invalid -> pa + | Unknown s -> Unknown (Str.replace_matched s res) + | Failure s -> Failure (Str.replace_matched s res) + | Timeout | HighFailure -> assert false + else greps outerr l in greps outerr pr.pr_regexps in { pr_time = t; pr_answer = answer; @@ -199,7 +215,7 @@ and on_formatter ?debug ?timeout ?filename pr formatter = check_prover pr; match pr.pr_call_stdin with | Some cmd -> - let res = timed_sys_command ?debug ?timeout ~formatter:formatter cmd in + let res = timed_sys_command ?debug ?timeout ~formatter cmd in treat_result pr res | None -> match filename with @@ -210,3 +226,18 @@ and on_formatter ?debug ?timeout ?filename pr formatter = formatter fmt; pp_print_flush fmt (); on_file ?timeout ?debug pr file) + + +let on_buffer ?debug ?timeout ?filename pr buffer = + check_prover pr; + match pr.pr_call_stdin with + | Some cmd -> + let res = timed_sys_command ?debug ?timeout ~buffer cmd in + treat_result pr res + | None -> + match filename with + | None -> raise NoCommandlineProvided + | Some filename -> Sysutil.open_temp_file ?debug filename + (fun file cout -> + Buffer.output_buffer cout buffer; + on_file ?timeout ?debug pr file) diff --git a/src/driver/call_provers.mli b/src/driver/call_provers.mli index 510e9b54bb7045de0f6fb7681411223cd1f076f9..88aa8691f488f336af9b3f152c4004dfa870f0f7 100644 --- a/src/driver/call_provers.mli +++ b/src/driver/call_provers.mli @@ -64,3 +64,12 @@ val on_formatter : prover -> (formatter -> unit) -> prover_result + +val on_buffer : + ?debug:bool -> + ?timeout:int -> + ?filename:string -> (* used as the suffix of a tempfile if the prover can't + deal with stdin *) + prover -> + Buffer.t -> + prover_result diff --git a/src/driver/driver.ml b/src/driver/driver.ml index d5768ee323ba5e0a16eeb6cadafc0784c0428dac..31b0713e9234e72ff0b082c0c2d615b69d748384 100644 --- a/src/driver/driver.ml +++ b/src/driver/driver.ml @@ -443,6 +443,8 @@ let call_prover_on_file ?debug ?timeout drv filename = Call_provers.on_file drv.drv_prover filename let call_prover_on_formatter ?debug ?timeout ?filename drv ib = Call_provers.on_formatter ?debug ?timeout ?filename drv.drv_prover ib +let call_prover_on_buffer ?debug ?timeout ?filename drv ib = + Call_provers.on_buffer ?debug ?timeout ?filename drv.drv_prover ib let call_prover ?debug ?timeout drv task = @@ -453,6 +455,17 @@ let call_prover ?debug ?timeout drv task = let formatter fmt = print_task drv fmt task in call_prover_on_formatter ?debug ?timeout ?filename drv formatter +let call_prover_ext ?debug ?timeout drv task = + let filename = + match drv.drv_filename with + | None -> None + | Some _ -> Some (filename_of_goal drv "why" "call_prover" task) in + let formatter fmt = print_task drv fmt task in + let buf = Buffer.create 64 in + let fmt = formatter_of_buffer buf in + formatter fmt; + (fun () -> call_prover_on_buffer ?debug ?timeout ?filename drv buf) + (* diff --git a/src/driver/driver.mli b/src/driver/driver.mli index 7974cc578f1b0331c5dcc3133edbf67506595ee1..7a769334150ef0812dd0a8f52458b37e3b3edd6d 100644 --- a/src/driver/driver.mli +++ b/src/driver/driver.mli @@ -83,7 +83,8 @@ type prover_answer = Call_provers.prover_answer = val call_prover : ?debug:bool -> ?timeout:int -> driver -> task -> Call_provers.prover_result (** calls a prover on a given task - @param debug if on, prints on stderr the command line and the output of the prover + @param debug if on, prints on stderr the command line + and the output of the prover @param timeout specifies the CPU time limit given to the prover, if not set: unlimited time @param driver the driver to use @@ -91,6 +92,15 @@ val call_prover : ?debug:bool -> ?timeout:int -> driver -> task -> @return the prover's answer *) +val call_prover_ext : ?debug:bool -> ?timeout:int -> driver -> task -> + (unit -> Call_provers.prover_result) +(** same as {!Driver.call_prover} but split the function between + thread unsafe and thread safe operation. + call_prover_ext ~debug ~timeout driver task prepares the goal + and return a function which actually call the prover on the goal. + The returned function is thread safe. + *) + val call_prover_on_file : ?debug:bool -> ?timeout:int -> diff --git a/src/programs/pgm_ptree.mli b/src/programs/pgm_ptree.ml similarity index 100% rename from src/programs/pgm_ptree.mli rename to src/programs/pgm_ptree.ml diff --git a/src/programs/pgm_ttree.mli b/src/programs/pgm_ttree.ml similarity index 100% rename from src/programs/pgm_ttree.mli rename to src/programs/pgm_ttree.ml diff --git a/src/util/sysutil.ml b/src/util/sysutil.ml index 7412a92e11507c2d84c2c79345997e1e7626e884..ec7f4298697702ce715e4b2f921baca8039df7a6 100644 --- a/src/util/sysutil.ml +++ b/src/util/sysutil.ml @@ -72,3 +72,6 @@ let open_temp_file ?(debug=false) filesuffix usefile = if not debug then Sys.remove file; close_out cout; raise e + + +let call_asynchronous f = assert false diff --git a/src/util/sysutil.mli b/src/util/sysutil.mli index bd696d667de83c8c1de404b62e183cb30dd79668..99b9da4127c8e48787af9e8ad5fd82d3f03cd416 100644 --- a/src/util/sysutil.mli +++ b/src/util/sysutil.mli @@ -39,3 +39,16 @@ val open_temp_file : Create a temporary file with suffix suffix, and call usefile on this file (filename and open_out). usefile can close the file *) + +val call_asynchronous : (unit -> 'a) -> (unit -> 'a) + (* Transform a synchronous call to an + asynchronous in a separate memory. + call_asynchronous f forks and run the + function in the child process. In the parent + process the function returned will wait the end + of the child process*) + +(* With this function we can make fork in a thread + it is not as bad as it can be in 3.11.0 : + http://caml.inria.fr/mantis/view.php?id=4577 +*)