Commit 86d4f8ff authored by Francois Bobot's avatar Francois Bobot
Browse files

Utilisation de formatter au lieu d'un buffer intermediaire

parent ce462fc1
......@@ -49,7 +49,8 @@ let print_prover_result fmt pr =
type prover =
{ pr_call_stdin : string option; (* %f pour le nom du fichier *)
pr_call_file : string option;
pr_regexps : (Str.regexp * prover_answer) list; (* \1,... sont remplacés *)
pr_regexps : (Str.regexp * prover_answer) list;
(* \1,... sont remplacés *)
}
......@@ -69,16 +70,18 @@ let remove_file ?(debug=false) f =
(*let environment = Unix.environment ()*)
let timed_sys_command ?stdin ?(debug=false) ?timeout cmd =
let timed_sys_command ?formatter ?(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
(match stdin with
(match formatter with
| None -> ()
| Some stdin -> Buffer.output_buffer cout stdin);
| Some formatter ->
let fmt = formatter_of_out_channel cout in
formatter fmt);
close_out cout;
let out = Sysutil.channel_contents cin in
let ret = Unix.close_process p in
......@@ -113,7 +116,8 @@ let grep re str =
(* 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." *)
(* "Calldp.gen_prover_call : filename must be given if the prover
can't use stdin." *)
(* in *)
......@@ -163,20 +167,21 @@ let rec on_file ?debug ?timeout pr filename =
let res = timed_sys_command ?debug ?timeout cmd in
treat_result pr res
| None ->
let buf = Sysutil.file_contents_buf filename in
on_buffer ?timeout ?debug pr buf
let formatter = Sysutil.file_contents_fmt filename in
on_formatter ?timeout ?debug pr formatter
and on_buffer ?debug ?timeout ?filename pr buf =
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 ~stdin:buf cmd in
let res = timed_sys_command ?debug ?timeout ~formatter: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 ->
Buffer.output_buffer cout buf;
flush cout;
let fmt = formatter_of_out_channel cout in
formatter fmt;
pp_print_flush fmt ();
on_file ?timeout ?debug pr file)
......@@ -40,7 +40,8 @@ val print_prover_result : formatter -> prover_result -> unit
type prover =
{ pr_call_stdin : string option; (* %f pour le nom du fichier *)
pr_call_file : string option;
pr_regexps : (Str.regexp * prover_answer) list; (* \1,... sont remplacés *)
pr_regexps : (Str.regexp * prover_answer) list;
(* \1,... sont remplacés *)
}
exception CommandError
......@@ -55,11 +56,11 @@ val on_file :
string ->
prover_result
val on_buffer :
val on_formatter :
?debug:bool ->
?timeout:int ->
?filename:string -> (* used as the suffix of a tempfile if the prover can't
deal with stdin *)
prover ->
Buffer.t ->
(formatter -> unit) ->
prover_result
......@@ -415,8 +415,8 @@ let file_printer =
let call_prover_on_file ?debug ?timeout drv filename =
Call_provers.on_file drv.drv_raw.drv_prover filename
let call_prover_on_buffer ?debug ?timeout ?filename drv ib =
Call_provers.on_buffer ?debug ?timeout ?filename drv.drv_raw.drv_prover ib
let call_prover_on_formatter ?debug ?timeout ?filename drv ib =
Call_provers.on_formatter ?debug ?timeout ?filename drv.drv_raw.drv_prover ib
let call_prover ?debug ?timeout drv task =
......@@ -424,9 +424,8 @@ let call_prover ?debug ?timeout drv task =
match drv.drv_raw.drv_filename with
| None -> None
| Some _ -> Some (filename_of_goal drv file_printer "" "" task) in
let buffer = Buffer.create 128 in
bprintf buffer "%a@?" (print_task drv) task;
call_prover_on_buffer ?debug ?timeout ?filename drv buffer
let formatter fmt = print_task drv fmt task in
call_prover_on_formatter ?debug ?timeout ?filename drv formatter
......
......@@ -95,12 +95,12 @@ val call_prover_on_file :
string ->
Call_provers.prover_result
val call_prover_on_buffer :
val call_prover_on_formatter :
?debug:bool ->
?timeout:int ->
?filename:string ->
driver ->
Buffer.t ->
(formatter -> unit) ->
Call_provers.prover_result
(* error reporting *)
......
......@@ -17,6 +17,18 @@
(* *)
(**************************************************************************)
let channel_contents_fmt cin fmt =
let buff = String.make 1024 ' ' in
let n = ref 0 in
while n := input cin buff 0 1024; !n <> 0 do
Format.pp_print_string fmt
(if !n = 1024 then
buff
else
String.sub buff 0 !n)
done
let channel_contents_buf cin =
let buf = Buffer.create 1024
and buff = String.make 1024 ' ' in
......@@ -28,6 +40,14 @@ let channel_contents_buf cin =
let channel_contents cin = Buffer.contents (channel_contents_buf cin)
let file_contents_fmt f fmt =
try
let cin = open_in f in
channel_contents_fmt cin fmt;
close_in cin
with _ ->
invalid_arg (Printf.sprintf "(cannot open %s)" f)
let file_contents_buf f =
try
let cin = open_in f in
......
......@@ -20,12 +20,18 @@
(* return the content of an in-channel *)
val channel_contents : in_channel -> string
(* Put the content of an in_channel in a formatter *)
val channel_contents_fmt : in_channel -> Format.formatter -> unit
(* return the content of a file *)
val file_contents : string -> string
(* return the content of a file *)
val file_contents_buf : string -> Buffer.t
(* Put the content of a file in a formatter *)
val file_contents_fmt : string -> Format.formatter -> unit
val open_temp_file :
?debug:bool -> (* don't remove the file *)
string -> (string -> out_channel -> 'a) -> 'a
......
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