Commit 740951f5 authored by Andrei Paskevich's avatar Andrei Paskevich

make Call_provers a bit more legible

parent 6b85cd40
......@@ -79,6 +79,10 @@ let call_prover command opt_cout buffer =
Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
ret, out, time
type post_prover_call = unit -> prover_result
type bare_prover_call = unit -> post_prover_call
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
~regexps ~exitcodes ~filename buffer =
let on_stdin = ref true in
......@@ -92,42 +96,36 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
| _ -> failwith "unknown format specifier, use %%f, %%t or %%m"
in
let cmd = Str.global_substitute cmd_regexp (replace "") command in
let f = if !on_stdin then
fun () -> call_prover cmd None buffer
else begin
let fout,cout = Filename.open_temp_file "why_" ("_" ^ filename) in
try
let cmd = Str.global_substitute cmd_regexp (replace fout) command in
fun () ->
let res = call_prover cmd (Some cout) buffer in
if Debug.nottest_flag debug then Sys.remove fout;
res
with e ->
close_out cout;
if Debug.nottest_flag debug then Sys.remove fout;
raise e
end
let on_stdin = !on_stdin in
let cmd,fout,cout = if on_stdin then cmd, "", None else
let fout,cout = Filename.open_temp_file "why_" ("_" ^ filename) in
let cmd =
try Str.global_substitute cmd_regexp (replace fout) command
with e -> close_out cout; Sys.remove fout; raise e
in
cmd, fout, Some cout
in
fun () ->
let ret,out,time = f () in
let ret,out,time = call_prover cmd cout buffer in
fun () ->
let ans = match ret with
| Unix.WSTOPPED n ->
Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
HighFailure
| Unix.WSIGNALED n ->
Debug.dprintf debug "Call_provers: killed by signal %d@." n;
HighFailure
| Unix.WEXITED n ->
Debug.dprintf debug "Call_provers: exited with status %d@." n;
(try List.assoc n exitcodes with Not_found -> grep out regexps)
in
let ans = match ans with
| HighFailure when !on_timelimit && timelimit > 0
&& time >= (0.9 *. float timelimit) -> Timeout
| _ -> ans
in
{ pr_answer = ans;
pr_output = out;
pr_time = time }
if not on_stdin && Debug.nottest_flag debug then Sys.remove fout;
let ans = match ret with
| Unix.WSTOPPED n ->
Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
HighFailure
| Unix.WSIGNALED n ->
Debug.dprintf debug "Call_provers: killed by signal %d@." n;
HighFailure
| Unix.WEXITED n ->
Debug.dprintf debug "Call_provers: exited with status %d@." n;
(try List.assoc n exitcodes with Not_found -> grep out regexps)
in
let ans = match ans with
| HighFailure when !on_timelimit && timelimit > 0
&& time >= (0.9 *. float timelimit) -> Timeout
| _ -> ans
in
{ pr_answer = ans;
pr_output = out;
pr_time = time }
......@@ -52,11 +52,18 @@ val print_prover_result : Format.formatter -> prover_result -> unit
a [HighFailure] *)
val debug : Debug.flag
(** debug flag for the calling procedure (option "--debug
call_prover")
(** debug flag for the calling procedure (option "--debug call_prover")
If set [call_on_buffer] prints on stderr the commandline called
and the output of the prover.
*)
and the output of the prover. *)
type post_prover_call = unit -> prover_result
(** Thread-unsafe closure that processes a prover's output
and returns the final result. Once again: this closure
may use internal Why structures and is therefore not
thread-safe. *)
type bare_prover_call = unit -> post_prover_call
(** Thread-safe closure that executes a prover on a task. *)
val call_on_buffer :
command : string ->
......@@ -65,23 +72,22 @@ val call_on_buffer :
regexps : (Str.regexp * prover_answer) list ->
exitcodes : (int * prover_answer) list ->
filename : string ->
Buffer.t -> unit -> unit -> prover_result
Buffer.t -> bare_prover_call
(** Call a prover on the task printed in the {!type: Buffer.t} given.
Only the computation between the two [unit] is parallelisable.
@param timelimit : set the available time limit (default 0 : unlimited)
@param memlimit : set the available time limit (default 0 :
unlimited)
@param timelimit : set the available time limit (def. 0 : unlimited)
@param memlimit : set the available time limit (def. 0 : unlimited)
@param regexps : if the first field matches the prover output,
the second field is the answer. Regexp groups present in
the first field are substituted in the second field (\0,\1,...).
The regexps are tested in the order of the list.
@param regexps : if the first field match the prover output the
second field is the answer. Regexp groups present in the first field are
substituted in the second field (\0,\1,...). The regexp are tested in the
order of the list.
@param exitcodes : if the first field is the exit code the second
field is the answer. No subtitution are done. Exit codes are tested
in the order of the list and before the regexps.
@param exitcodes : if the first field is the exit code, then
the second field is the answer. Exit codes are tested in the order
of the list and before the regexps.
@param filename : if the prover doesn't accept stdin, a temporary
file is used. In the case the suffix of the temporary file is
[filename] *)
file is used. In this case the suffix of the temporary file is
[filename]. *)
......@@ -41,7 +41,7 @@ val call_on_buffer :
command : string ->
?timelimit : int ->
?memlimit : int ->
driver -> Buffer.t -> unit -> unit -> Call_provers.prover_result
driver -> Buffer.t -> Call_provers.bare_prover_call
val print_task :
?old : in_channel ->
......@@ -52,5 +52,5 @@ val prove_task :
?timelimit : int ->
?memlimit : int ->
?old : in_channel ->
driver -> Task.task -> (unit -> unit -> Call_provers.prover_result)
driver -> Task.task -> Call_provers.bare_prover_call
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