Commit 605ecfb3 authored by Francois Bobot's avatar Francois Bobot

ajout de call_prover_ext et ajout de dépendance dans le makefile

parent 05014749
......@@ -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)
......@@ -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
......@@ -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)
(*
......
......@@ -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 ->
......
......@@ -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
......@@ -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
*)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment