Commit 04dc9c43 authored by Johannes Kanig's avatar Johannes Kanig Committed by MARCHE Claude
Browse files

N211-037 refactoring

extract code to compute the actual command

* call_provers.ml
(actual_command): new function to compute the command string
(prover_on_file): call extracted function
parent c38e1957
......@@ -163,17 +163,14 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit =
pr_output = out;
pr_time = time }
let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
~res_parser
?(cleanup=false) ?(inplace=false) ?(redirect=true) fin =
let actualcommand command timelimit memlimit file =
let arglist = Cmdline.cmdline_split command in
let use_stdin = ref true in
let on_timelimit = ref false in
let cmd_regexp = Str.regexp "%\\(.\\)" in
let replace s = match Str.matched_group 1 s with
| "%" -> "%"
| "f" -> use_stdin := false; fin
| "f" -> file
| "t" -> on_timelimit := true; string_of_int timelimit
| "T" -> string_of_int (succ timelimit)
| "U" -> string_of_int (2 * timelimit + 1)
......@@ -186,22 +183,26 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
| "S" -> string_of_int stepslimit
| _ -> failwith "unknown specifier, use %%, %f, %t, %T, %U, %m, %l, or %d"
in
let subst s =
try
Str.global_substitute cmd_regexp replace s
List.map (Str.global_substitute cmd_regexp replace) arglist,
!use_stdin, !on_timelimit
let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
~res_parser
?(cleanup=false) ?(inplace=false) ?(redirect=true) fin =
let command, use_stdin, on_timelimit =
try actualcommand command timelimit memlimit fin
with e ->
if cleanup then Sys.remove fin;
if inplace then Sys.rename (save fin) fin;
raise e
in
let arglist = List.map subst arglist in
let command = List.hd arglist in
raise e in
let exec = List.hd command in
Debug.dprintf debug "@[<hov 2>Call_provers: command is: %a@]@."
(Pp.print_list Pp.space pp_print_string) arglist;
let argarray = Array.of_list arglist in
(Pp.print_list Pp.space pp_print_string) command;
let argarray = Array.of_list command in
fun () ->
let fd_in = if !use_stdin then Unix.openfile fin [Unix.O_RDONLY] 0 else Unix.stdin in
let fd_in = if use_stdin then Unix.openfile fin [Unix.O_RDONLY] 0 else Unix.stdin in
let fout,cout,fd_out,fd_err =
if redirect then
let fout,cout = Filename.open_temp_file (Filename.basename fin) ".out" in
......@@ -210,8 +211,8 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
else
"", stdout, Unix.stdout, Unix.stderr in
let time = Unix.gettimeofday () in
let pid = Unix.create_process command argarray fd_in fd_out fd_err in
if !use_stdin then Unix.close fd_in;
let pid = Unix.create_process exec argarray fd_in fd_out fd_err in
if use_stdin then Unix.close fd_in;
if redirect then close_out cout;
let call = fun ret ->
......@@ -232,7 +233,7 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
if inplace then swallow (Sys.rename (save fin)) fin;
if redirect then swallow Sys.remove fout
end;
parse_prover_run res_parser time out ret !on_timelimit timelimit
parse_prover_run res_parser time out ret on_timelimit timelimit
in
{ call = call; pid = pid }
......
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