Skip to content

GitLab

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

Simplify calls to external provers

parent 90e35d59
Hide whitespace changes
Inline Side-by-side
src/driver/call_provers.ml
View file @ cd770632
......@@ -34,8 +34,6 @@ type prover_result = {
pr_time : float;
}
type prover_regexp = Str.regexp * prover_answer
let print_prover_answer fmt = function
| Valid -> fprintf fmt "Valid"
| Invalid -> fprintf fmt "Invalid"
......@@ -44,10 +42,9 @@ let print_prover_answer fmt = function
| Failure s -> fprintf fmt "Failure: %s" s
| HighFailure -> fprintf fmt "HighFailure"
let print_prover_result fmt pr =
fprintf fmt "%a (%.2fs)" print_prover_answer pr.pr_answer pr.pr_time;
if pr.pr_answer == HighFailure then
fprintf fmt "@\nstdout-stderr:@\n%s@." pr.pr_output
let print_prover_result fmt {pr_answer=ans; pr_output=out; pr_time=t} =
fprintf fmt "%a (%.2fs)" print_prover_answer ans t;
if ans == HighFailure then fprintf fmt "@\nProver output:@\n%s@." out
let rec grep out l = match l with
| [] -> HighFailure
......@@ -55,75 +52,82 @@ let rec grep out l = match l with
begin try
ignore (Str.search_forward re out 0);
match pa with
| Valid | Invalid | Timeout -> pa
| Unknown s -> Unknown (Str.replace_matched s out)
| Failure s -> Failure (Str.replace_matched s out)
| HighFailure -> assert false
| Valid | Invalid | Timeout -> pa
| Unknown s -> Unknown (Str.replace_matched s out)
| Failure s -> Failure (Str.replace_matched s out)
| HighFailure -> assert false
with Not_found -> grep out l end
let call_prover debug command regexps opt_cout buffer =
let t0 = Unix.time () in
let call_prover debug command opt_cout buffer =
let time = Unix.time () in
let (cin,cout) as p = Unix.open_process command in
let cout = match opt_cout with Some c -> c | _ -> cout in
Buffer.output_buffer cout buffer; close_out cout;
let out = channel_contents cin in
let ret = Unix.close_process p in
let t1 = Unix.time () in
if debug then Format.eprintf "Call_provers: Command output:@\n%s@." out;
let time = Unix.time () -. time in
if debug then eprintf "Call_provers: prover output:@\n%s@." out;
ret, out, time
let call_on_buffer ?(debug=false) ~command ~timelimit ~memlimit
~regexps ~exitcodes ~filename buffer () =
let on_stdin = ref false in
let cmd_regexp = Str.regexp "%\\(.\\)" in
let replace file s = match Str.matched_group 1 s with
| "%" -> "%"
| "f" -> on_stdin := false; file
| "t" -> string_of_int timelimit
| "m" -> string_of_int memlimit
| _ -> failwith "unknown format specifier, use %%f, %%t or %%m"
in
let cmd = Str.global_substitute cmd_regexp (replace "") command in
let ret, out, time =
if !on_stdin then call_prover debug 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
let res = call_prover debug cmd (Some cout) buffer in
if not debug then Sys.remove fout;
res
with e ->
close_out cout;
if not debug then Sys.remove fout;
raise e
end
in
let ans = match ret with
| Unix.WSTOPPED n ->
if debug then Format.eprintf "Call_provers: stopped on signal %d@." n;
if debug then eprintf "Call_provers: stopped by signal %d@." n;
HighFailure
| Unix.WSIGNALED 24 (* SIGXCPU signal cf. /usr/include/bits/signum.h *) ->
if debug then Format.eprintf "Call_provers: killed by signal SIGXCPU@.";
Timeout
| Unix.WSIGNALED n ->
if debug then Format.eprintf "Call_provers: killed by signal %d@." n;
if debug then eprintf "Call_provers: killed by signal %d@." n;
HighFailure
| Unix.WEXITED n ->
if debug then Format.eprintf "Call_provers: exited with status %d@." n;
grep out regexps
if debug then eprintf "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 time >= (0.9 *. float timelimit) -> Timeout
| _ -> ans
in
{ pr_answer = ans;
pr_output = out;
pr_time = t1 -. t0 }
pr_time = time }
let call_on_buffer ?(debug=false) ?(suffix=".dump")
~command ~timelimit ~memlimit ~regexps buffer () =
let on_stdin = ref false in
let cmd_regexp = Str.regexp "%\\(.\\)" in
let replace filename s = match Str.matched_group 1 s with
| "%" -> "%"
| "f" -> on_stdin := false; filename
| "t" -> string_of_int timelimit
| "m" -> string_of_int memlimit
| _ -> failwith "unknown format specifier, use %%f, %%t or %%m"
in
let cmd_stdin = Str.global_substitute cmd_regexp (replace "") command in
if !on_stdin then call_prover debug cmd_stdin regexps None buffer
else
let fout,cout = Filename.open_temp_file "why" suffix in
try
let cmd = Str.global_substitute cmd_regexp (replace fout) command in
let res = call_prover debug cmd regexps (Some cout) buffer in
if not debug then Sys.remove fout;
res
with e ->
close_out cout;
if not debug then Sys.remove fout;
raise e
let call_on_formatter ?debug ?suffix
(*
let call_on_formatter ?debug ?filename
~command ~timelimit ~memlimit ~regexps formatter =
let buffer = Buffer.create 1024 in
let fmt = formatter_of_buffer buffer in
formatter fmt; pp_print_flush fmt ();
call_on_buffer ?debug ?suffix ~command ~timelimit ~memlimit ~regexps buffer
call_on_buffer ?debug ?filename ~command ~timelimit ~memlimit ~regexps buffer
let call_on_file ?debug ?suffix
let call_on_file ?debug ?filename
~command ~timelimit ~memlimit ~regexps filename =
let buffer = file_contents_buf filename in
call_on_buffer ?debug ?suffix ~command ~timelimit ~memlimit ~regexps buffer
call_on_buffer ?debug ?filename ~command ~timelimit ~memlimit ~regexps buffer
*)
(*
let is_true_cygwin = Sys.os_type = "Cygwin"
......@@ -164,9 +168,9 @@ 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 -> 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;
| 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
......@@ -176,7 +180,7 @@ let timed_sys_command ?formatter ?buffer ?(debug=false) ?timeout cmd =
let fmt = formatter_of_out_channel cout in
formatter fmt);
with Sys_error s ->
if debug then Format.eprintf "Sys_error : %s@." s
if debug then eprintf "Sys_error : %s@." s
end;
(* Write the buffer to the stdin of the prover *)
begin try
......@@ -185,14 +189,14 @@ let timed_sys_command ?formatter ?buffer ?(debug=false) ?timeout cmd =
| Some buffer ->
Buffer.output_buffer cout buffer);
with Sys_error s ->
if debug then Format.eprintf "Sys_error : %s@." 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 Format.eprintf "Call_provers : Command output : %s@." out;
if debug then eprintf "Call_provers : Command output : %s@." out;
(cpu_time,ret,out)
let grep re str =
......
src/driver/call_provers.mli
View file @ cd770632
......@@ -31,38 +31,17 @@ type prover_result = {
pr_time : float;
}
type prover_regexp = Str.regexp * prover_answer
val print_prover_answer : Format.formatter -> prover_answer -> unit
val print_prover_result : Format.formatter -> prover_result -> unit
val call_on_buffer :
?debug : bool ->
?suffix : string ->
command : string ->
?debug : bool ->
command : string ->
timelimit : int ->
memlimit : int ->
regexps : prover_regexp list ->
memlimit : int ->
regexps : (Str.regexp * prover_answer) list ->
exitcodes : (int * prover_answer) list ->
filename : string ->
Buffer.t ->
(unit -> prover_result)
val call_on_formatter :
?debug : bool ->
?suffix : string ->
command : string ->
timelimit : int ->
memlimit : int ->
regexps : prover_regexp list ->
(Format.formatter -> unit) ->
(unit -> prover_result)
val call_on_file :
?debug : bool ->
?suffix : string ->
command : string ->
timelimit : int ->
memlimit : int ->
regexps : prover_regexp list ->
string ->
(unit -> prover_result)
unit -> prover_result
src/driver/driver.ml
View file @ cd770632
......@@ -166,9 +166,7 @@ let load_file file =
f
let string_of_qualid thl idl =
let thl = String.concat "." thl in
let idl = String.concat "." idl in
thl^"."^idl
String.concat "." thl ^ "." ^ String.concat "." idl
let add_htheory tmap cloned id t =
try
......@@ -220,7 +218,7 @@ let load_rules env (pmap,tmap) { thr_name = (loc,qualid); thr_rules = trl } =
in
List.fold_left add (pmap,tmap) trl
let load_driver file env =
let load_driver env file =
let prelude = ref [] in
let regexps = ref [] in
let exitcodes = ref [] in
......@@ -245,7 +243,7 @@ let load_driver file env =
| ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown t)
| ExitCodeFailure (s,t) -> add_to_list exitcodes (s, Failure t)
| Filename s -> set_or_raise loc filename s "filename"
| Printer s -> begin
| Printer s -> begin
try set_or_raise loc printer (Hashtbl.find printers s) "printer"
with Not_found -> errorm ~loc "unknown printer %s" s end
| Transform s -> begin
......@@ -290,8 +288,6 @@ let query_ident drv clone =
Hid.add h id tr;
tr
let get_regexps drv = drv.drv_regexps
(** using drivers *)
let apply_transforms drv =
......@@ -324,21 +320,38 @@ let print_task drv fmt task =
print_prelude drv (task_used task) fmt;
Format.fprintf fmt "@[%a@]@?" printer task
let file_of_task drv input_file theory_name task =
let filename_regexp = Str.regexp "%\\(.\\)" in
let filename_regexp = Str.regexp "%\\(.\\)"
let get_filename drv input_file theory_name goal_name =
let file = match drv.drv_filename with
| Some f -> f
| None -> "%f-%t-%g.dump"
in
let replace s = match Str.matched_group 1 s with
| "%" -> "%"
| "f" -> input_file
| "t" -> theory_name
| "g" -> (task_goal task).pr_name.id_short
| "g" -> goal_name
| _ -> errorm "unknown format specifier, use %%f, %%t or %%g"
in
let file = match drv.drv_filename with
| Some f -> f
| None -> "%f_%t_%g.dump"
in
Str.global_substitute filename_regexp replace file
let file_of_task drv input_file theory_name task =
get_filename drv input_file theory_name (task_goal task).pr_name.id_short
let call_on_buffer ?debug ~command ~timelimit ~memlimit drv buffer =
let regexps = drv.drv_regexps in
let exitcodes = drv.drv_exitcodes in
let filename = get_filename drv "" "" "" in
Call_provers.call_on_buffer
?debug ~command ~timelimit ~memlimit ~regexps ~exitcodes ~filename buffer
let prove_task ?debug ~command ~timelimit ~memlimit drv task =
let buf = Buffer.create 1024 in
let fmt = Format.formatter_of_buffer buf in
print_task drv fmt task; Format.pp_print_flush fmt ();
call_on_buffer ?debug ~command ~timelimit ~memlimit drv buf
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. test"
......
src/driver/driver.mli
View file @ cd770632
......@@ -29,10 +29,10 @@ open Env
type driver
val load_driver : string -> env -> driver
val load_driver : env -> string -> driver
(** loads a driver from a file
@param string driver file name
@param env TODO
@param string driver file name
*)
(** {2 query a driver} *)
......@@ -47,9 +47,6 @@ val syntax_arguments : string -> (formatter -> 'a -> unit) ->
(** (syntax_argument templ print_arg fmt l) prints in the formatter fmt
the list l using the template templ and the printer print_arg *)
val get_regexps : driver -> Call_provers.prover_regexp list
(** fetch the regular expressions to parse the prover's output *)
(** {2 register printers and transformations} *)
type printer = (ident -> translation) -> formatter -> task -> unit
......@@ -73,6 +70,20 @@ val print_task : driver -> formatter -> task -> unit
val file_of_task : driver -> string -> string -> task -> string
(** file_of_task input_file theory_name task *)
val prove_task :
?debug : bool ->
command : string ->
timelimit : int ->
memlimit : int ->
driver -> task -> unit -> Call_provers.prover_result
val call_on_buffer :
?debug : bool ->
command : string ->
timelimit : int ->
memlimit : int ->
driver -> Buffer.t -> unit -> Call_provers.prover_result
(** {2 error reporting} *)
type error
......
src/main.ml
View file @ cd770632
......@@ -260,36 +260,29 @@ let print_th_namespace fmt th =
let fname_printer = ref (Ident.create_ident_printer [])
let do_task _env drv fname tname (th : Why.Theory.theory) (task : Task.task) =
let dest =
let fname =
let fname = Filename.basename fname in
try Filename.chop_extension fname
with Invalid_argument _ -> fname
in
let tname = th.th_name.Ident.id_short in
Driver.file_of_task drv fname tname task
in
let print_task fmt =
fprintf fmt "@[%a@]@?" (Driver.print_task drv) task
in
match !opt_output, !opt_command with
| None, Some command ->
let regexps = Driver.get_regexps drv in
let res = Call_provers.call_on_formatter ~debug ~suffix:dest
~command ~timelimit ~memlimit ~regexps print_task ()
let res =
Driver.prove_task ~debug ~command ~timelimit ~memlimit drv task ()
in
printf "%s %s %s : %a@." fname tname
(task_goal task).Decl.pr_name.Ident.id_long
Call_provers.print_prover_result res
| None, None ->
print_task std_formatter
Driver.print_task drv std_formatter task
| Some dir, _ ->
let fname = Filename.basename fname in
let fname =
try Filename.chop_extension fname with _ -> fname
in
let tname = th.th_name.Ident.id_short in
let dest = Driver.file_of_task drv fname tname task in
(* Uniquify the filename before the extension if it exists*)
let i = try String.rindex dest '.' with _ -> String.length dest in
let name = Ident.string_unique !fname_printer (String.sub dest 0 i) in
let ext = String.sub dest i (String.length dest - i) in
let cout = open_out (Filename.concat dir (name ^ ext)) in
print_task (formatter_of_out_channel cout);
Driver.print_task drv (formatter_of_out_channel cout) task;
close_out cout
let do_task env drv fname tname th task =
......@@ -361,7 +354,7 @@ let do_input env drv = function
let () =
try
let env = Env.create_env (Typing.retrieve !opt_loadpath) in
let drv = Util.option_map (fun f -> load_driver f env) !opt_driver in
let drv = Util.option_map (load_driver env) !opt_driver in
Queue.iter (do_input env drv) opt_queue
with e when not debug ->
eprintf "%a@." report e;
......
src/manager/db.ml
View file @ cd770632
......@@ -1481,15 +1481,7 @@ let try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver
in
if debug then Format.eprintf "Task for prover: %a@." (Why.Driver.print_task driver) task;
let callback =
let dest =
Why.Driver.file_of_task driver "" "" task
in
let print_task fmt =
Format.fprintf fmt "@[%a@]@?" (Why.Driver.print_task driver) task
in
let regexps = Why.Driver.get_regexps driver in
Why.Call_provers.call_on_formatter ~debug ~suffix:dest
~command ~timelimit ~memlimit ~regexps print_task
Why.Driver.prove_task ~debug ~command ~timelimit ~memlimit driver task
in
fun () ->
if debug then Format.printf "setting attempt status to Running@.";
......
src/manager/test.ml
View file @ cd770632
......@@ -64,7 +64,7 @@ let () = Db.init_base (fname ^ ".db")
let get_driver name =
let pi = Util.Mstr.find name config.provers in
Why.Driver.load_driver pi.Whyconf.driver env
Why.Driver.load_driver env pi.Whyconf.driver
type prover_data =
{ prover : Db.prover;
......
src/util/sysutil.ml
View file @ cd770632
......@@ -28,7 +28,6 @@ let channel_contents_fmt cin fmt =
String.sub buff 0 !n)
done
let channel_contents_buf cin =
let buf = Buffer.create 1024
and buff = String.make 1024 ' ' in
......@@ -57,7 +56,6 @@ let file_contents_buf f =
with _ ->
invalid_arg (Printf.sprintf "(cannot open %s)" f)
let file_contents f = Buffer.contents (file_contents_buf f)
let open_temp_file ?(debug=false) filesuffix usefile =
......@@ -73,7 +71,6 @@ let open_temp_file ?(debug=false) filesuffix usefile =
close_out cout;
raise e
type 'a result =
| Result of 'a
| Exception of exn
......@@ -108,3 +105,4 @@ let call_asynchronous (f : unit -> 'a) =
end
| _ -> raise (Bad_execution ps) in
f
src/util/sysutil.mli
View file @ cd770632
......@@ -20,16 +20,19 @@
(* return the content of an in-channel *)
val channel_contents : in_channel -> string
(* Put the content of an in_channel in a formatter *)
(* return the content of an in_channel in a buffer *)
val channel_contents_buf : in_channel -> Buffer.t
(* 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 *)
(* return the content of a file in a buffer *)
val file_contents_buf : string -> Buffer.t
(* Put the content of a file in a formatter *)
(* put the content of a file in a formatter *)
val file_contents_fmt : string -> Format.formatter -> unit
val open_temp_file :
......
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