Commit e59c5618 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

minor

parent 8d93a81c
......@@ -108,7 +108,7 @@ let call_on_buffer ?(debug=false) ~command ?(timelimit=0) ?(memlimit=0)
(try List.assoc n exitcodes with Not_found -> grep out regexps)
in
let ans = match ans with
| HighFailure when !on_timelimit && timelimit > 0
| HighFailure when !on_timelimit && timelimit > 0
&& time >= (0.9 *. float timelimit) -> Timeout
| _ -> ans
in
......@@ -116,197 +116,3 @@ let call_on_buffer ?(debug=false) ~command ?(timelimit=0) ?(memlimit=0)
pr_output = out;
pr_time = time }
(*
let is_true_cygwin = Sys.os_type = "Cygwin"
(* this should be replaced by a proper use of fork/waitpid() *)
let dirname = Filename.dirname Sys.argv.(0)
let cpulimit_local = Filename.concat dirname "why-cpulimit"
let cpulimit_commands = ["why-cpulimit"; cpulimit_local ; "timeout"]
let cpulimit = (
let tmp = ref "" in
try
List.iter
(fun s ->
(*let r = Sys.command (s^" 1 echo") in
if r=0 then (tmp:=s; raise Exit)*)
let pid = Unix.create_process s [|s;"1";"true"|]
Unix.stdin Unix.stdout Unix.stderr in
match Unix.waitpid [] pid with
| _,Unix.WEXITED 0 -> (tmp:=s; raise Exit)
| _ -> ()
)
cpulimit_commands;
failwith ("need shell command among: "^
(String.concat " ," cpulimit_commands))
with Exit -> tmp)
(* Utils *)
let remove_file ?(debug=false) f =
if not debug then try Sys.remove f with _ -> ()
(*let environment = Unix.environment ()*)
let () = Sys.set_signal Sys.sigpipe Sys.Signal_ignore
let timed_sys_command ?formatter ?buffer ?(debug=false) ?timeout cmd =
let t0 = Unix.times () in
let cmd = match timeout with
| None -> sprintf "%s 2>&1" cmd
| Some timeout -> sprintf "%s %d %s 2>&1" !cpulimit timeout cmd in
if debug then 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);
with Sys_error s ->
if debug then 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 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
let cpu_time = t1.Unix.tms_cutime -. t0.Unix.tms_cutime in
if debug then eprintf "Call_provers : Command output : %s@." out;
(cpu_time,ret,out)
let grep re str =
try
let _ = Str.search_forward re str 0 in true
with Not_found -> false
(* match buffers,p.DpConfig.stdin_switch,filename with *)
(* | None,_, Some f -> *)
(* let cmd = sprintf "%s %s %s %s" *)
(* p.DpConfig.command p.DpConfig.command_switches switch f *)
(* in *)
(* cmd,timed_sys_command ~debug timeout cmd *)
(* | Some buffers, Some stdin_s, _ -> *)
(* let cmd = sprintf "%s %s %s %s" *)
(* p.DpConfig.command p.DpConfig.command_switches switch stdin_s *)
(* in *)
(* cmd,timed_sys_command ~stdin:buffers ~debug timeout cmd *)
(* | Some buffers, None, Some f -> *)
(* let f = Filename.temp_file "" f in *)
(* let cout = open_out f in *)
(* List.iter (Buffer.output_buffer cout) buffers; *)
(* close_out cout; *)
(* let cmd = sprintf "%s %s %s %s" *)
(* p.DpConfig.command p.DpConfig.command_switches switch f *)
(* in *)
(* cmd,timed_sys_command ~debug timeout cmd *)
(* | _ -> invalid_arg *)
(* "Calldp.gen_prover_call : filename must be given if the prover
can't use stdin." *)
(* in *)
let treat_result pr (t,c,outerr) =
let answer =
match c with
| 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 _ ->
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
greps outerr pr.pr_regexps in
{ pr_time = t;
pr_answer = answer;
pr_stderr = ""; (*Fill it with something real*)
pr_stdout = outerr} (* Split it in two...*)
(* *)
let check_prover prover =
if prover.pr_call_file = None && prover.pr_call_stdin = None then
raise NoCommandlineProvided
let regexp_call_file = Str.regexp "%\\([a-z]\\)"
let rec on_file ?debug ?timeout pr filename =
check_prover pr;
match pr.pr_call_file with
| Some cmd ->
let filename = if is_true_cygwin
then
let cin = Unix.open_process_in
(sprintf "cygpath -am \"%s\"" filename) in
let f = input_line cin in
close_in cin; f
else filename in
let cmd =
let repl_fun s =
match Str.matched_group 1 s with
| "s" -> filename
| _ -> assert false in (*TODO mettre une belle exception*)
Str.global_substitute regexp_call_file repl_fun cmd in
let res = timed_sys_command ?debug ?timeout cmd in
treat_result pr res
| None ->
let formatter = Sysutil.file_contents_fmt filename in
on_formatter ?timeout ?debug pr formatter
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 cmd in
treat_result pr res
| None ->
match filename with
| None -> raise NoCommandlineProvided
| Some filename -> Sysutil.open_temp_file ?debug filename
(fun file cout ->
let fmt = formatter_of_out_channel cout in
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)
*)
......@@ -20,23 +20,23 @@
(** Call provers and parse there outputs *)
type prover_answer =
| Valid
| Valid
(** The task is valid according to the prover *)
| Invalid
| Invalid
(** The task is invalid *)
| Timeout
(** the task timeout, ie it takes more time than specified*)
| Unknown of string
(** The prover can't determined the validity or not of the task *)
| Timeout
(** the task timeout, ie it takes more time than specified *)
| Unknown of string
(** The prover can't determine if the task is valid *)
| Failure of string
(** The prover report a failure *)
| HighFailure
(** An error occured during the call to the prover or none of
the given regexp match the output of the prover *)
(** The prover reports a failure *)
| HighFailure
(** An error occured during the call to the prover or none
of the given regexps match the output of the prover *)
type prover_result = {
pr_answer : prover_answer;
(* The answer of the prover on the given task*)
(* The answer of the prover on the given task *)
pr_output : string;
(* The output of the prover currently stderr and stdout *)
pr_time : float;
......@@ -48,19 +48,19 @@ val print_prover_answer : Format.formatter -> prover_answer -> unit
val print_prover_result : Format.formatter -> prover_result -> unit
(** Pretty-print a prover_result. The answer and the time are output.
The output of the prover is printed if and only if the answer is an
[HighFailure] *)
The output of the prover is printed if and only if the answer is
a [HighFailure] *)
val call_on_buffer :
?debug : bool ->
command : string ->
?debug : bool ->
command : string ->
?timelimit : int ->
?memlimit : int ->
regexps : (Str.regexp * prover_answer) list ->
exitcodes : (int * prover_answer) list ->
filename : string ->
Buffer.t ->
unit -> prover_result
regexps : (Str.regexp * prover_answer) list ->
exitcodes : (int * prover_answer) list ->
filename : string ->
Buffer.t -> unit -> prover_result
(** Call a prover on the task printed in the {!type: Buffer.t} given.
@param debug : set the debug flag.
@param debug : set the debug flag.
Print on stderr the commandline called and the output of the prover. *)
......@@ -64,8 +64,8 @@ val get_transform : driver -> string list
val file_of_task : driver -> string -> string -> task -> string
val call_on_buffer :
?debug : bool ->
command : string ->
?debug : bool ->
command : string ->
?timelimit : int ->
?memlimit : int ->
driver -> Buffer.t -> unit -> Call_provers.prover_result
......
......@@ -22,8 +22,8 @@
val print_task : Driver.driver -> Format.formatter -> Task.task -> unit
val prove_task :
?debug : bool ->
command : string ->
?debug : bool ->
command : string ->
?timelimit : int ->
?memlimit : int ->
Driver.driver -> Task.task -> unit -> Call_provers.prover_result
......
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