Commit 69b8ed31 authored by Johannes Kanig's avatar Johannes Kanig

replace prover spawning by connection to why3server

* previous implementations of call_on_file and call_on_buffer are
  removed, and now directly use the prove_file_server function
* now, both blocking and nonblocking reading is supported on the socket
* wait_on_call and query_call are implemented by blocking and
  nonblocking read, together with a result buffer, if results for other
  prover runs are returned
* logging of the server is now optional
parent 3fdc58e0
......@@ -197,15 +197,6 @@ let rec grep out l = match l with
| HighFailure -> assert false
with Not_found -> grep out l end
type post_prover_call = unit -> prover_result
type prover_call = {
call : Unix.process_status -> post_prover_call;
pid : int
}
type pre_prover_call = unit -> prover_call
let save f = f ^ ".save"
let debug_print_model model =
......@@ -290,89 +281,6 @@ let actualcommand command ~use_why3cpulimit limit interactive file =
args in
args, !use_stdin, !on_timelimit
let call_on_file ~command
~limit
~res_parser
~printer_mapping
?(cleanup=false) ?(inplace=false) ?(interactive=false)
?(redirect=true) fin =
let command, use_stdin, on_timelimit =
try actualcommand command ~use_why3cpulimit:true limit interactive fin
with e ->
if cleanup then Sys.remove fin;
if inplace then Sys.rename (save fin) fin;
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) 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 fout,cout,fd_out,fd_err =
if redirect then
let fout,cout =
Filename.open_temp_file (Filename.basename fin) ".out" in
let fd_out = Unix.descr_of_out_channel cout in
fout, cout, fd_out, fd_out
else
"", stdout, Unix.stdout, Unix.stderr in
let time = Unix.gettimeofday () 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 ->
let time = Unix.gettimeofday () -. time in
let out =
if redirect then
let cout = open_in fout in
let out = Sysutil.channel_contents cout in
close_in cout;
out
else "" in
fun () ->
if Debug.test_noflag debug then begin
let swallow f x =
try f x with Sys_error s -> eprintf "Call_provers: %s@." s in
if cleanup then swallow Sys.remove fin;
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 limit
~printer_mapping
in
{ call = call; pid = pid }
let call_on_buffer ~command ~limit ~res_parser ~filename
~printer_mapping
?(inplace=false) ?interactive buffer =
let fin,cin =
if inplace then begin
Sys.rename filename (save filename);
filename, open_out filename
end else
Filename.open_temp_file "why_" ("_" ^ filename) in
Buffer.output_buffer cin buffer; close_out cin;
call_on_file ~command ~limit
~res_parser ~printer_mapping ~cleanup:true
~inplace ?interactive fin
let query_call pc =
let pid, ret = Unix.waitpid [Unix.WNOHANG] pc.pid in
if pid = 0 then None else Some (pc.call ret)
let wait_on_call pc =
let _, ret = Unix.waitpid [] pc.pid in pc.call ret
let post_wait_call pc ret = pc.call ret
let prover_call_pid pc = pc.pid
let set_socket_name =
Prove_client.set_socket_name
......@@ -395,9 +303,11 @@ type save_data =
let regexs : (int, save_data) Hashtbl.t = Hashtbl.create 17
let prove_file_server ~res_parser ~command ~limit
~printer_mapping ?(inplace=false) ?(interactive=false) file =
~printer_mapping ?(inplace=false) ?(interactive=false)
file =
let id = gen_id () in
let cmd, _, _ = actualcommand command ~use_why3cpulimit:false limit interactive file in
let cmd, _, _ =
actualcommand command ~use_why3cpulimit:false limit interactive file in
let saved_data =
{ vc_file = file;
is_temporary = not inplace;
......@@ -443,5 +353,49 @@ let handle_answer answer =
in
id, ans
let wait_for_server_result () =
List.map handle_answer (Prove_client.read_answers ())
let wait_for_server_result ~blocking =
List.map handle_answer (Prove_client.read_answers ~blocking)
type post_prover_call = unit -> prover_result
type prover_call = server_id
type pre_prover_call = unit -> prover_call
let result_buffer : (server_id, prover_result) Hashtbl.t = Hashtbl.create 17
let call_on_file ~command ~limit ~res_parser ~printer_mapping
?(cleanup=false) ?(inplace=false) ?(interactive=false)
?(redirect=true) fin =
fun () ->
prove_file_server ~res_parser ~command ~limit ~printer_mapping
~inplace ~interactive fin
let get_new_results ~blocking =
List.iter (fun (id, r) -> Hashtbl.add result_buffer id r)
(wait_for_server_result ~blocking)
let query_call id =
try
get_new_results ~blocking:false;
Some (let r = Hashtbl.find result_buffer id in (fun () -> r))
with Not_found -> None
let rec wait_on_call id =
try let r = Hashtbl.find result_buffer id in (fun () -> r)
with Not_found ->
get_new_results ~blocking:true;
wait_on_call id
let call_on_buffer ~command ~limit ~res_parser ~filename ~printer_mapping
?(inplace=false) ?(interactive=false) buffer =
let fin,cin =
if inplace then begin
Sys.rename filename (save filename);
filename, open_out filename
end else
Filename.open_temp_file "why_" ("_" ^ filename) in
Buffer.output_buffer cin buffer; close_out cin;
call_on_file ~command ~limit ~res_parser ~printer_mapping
~cleanup:true ~inplace ~interactive fin
......@@ -182,13 +182,6 @@ val query_call : prover_call -> post_prover_call option
val wait_on_call : prover_call -> post_prover_call
(** Thread-safe blocking function that waits until the prover finishes. *)
val post_wait_call : prover_call -> Unix.process_status -> post_prover_call
(** Thread-safe non-blocking function that should be called when the
prover's exit status was obtained from a prior call of Unix.waitpid *)
val prover_call_pid : prover_call -> int
(** Return the pid of the prover *)
val set_socket_name : string -> unit
type server_id = int
......@@ -202,4 +195,4 @@ val prove_file_server :
?interactive : bool ->
string -> server_id
val wait_for_server_result : unit -> (server_id * prover_result) list
val wait_for_server_result : blocking:bool -> (server_id * prover_result) list
let standalone : bool ref = ref true
let socket : Unix.file_descr option ref = ref None
let client_connect socket_name =
......@@ -7,6 +8,7 @@ let client_connect socket_name =
end else begin
let sock = Unix.socket Unix.PF_UNIX Unix.SOCK_STREAM 0 in
Unix.connect sock (Unix.ADDR_UNIX socket_name);
Unix.set_nonblock sock;
socket := Some sock
end
......@@ -28,12 +30,18 @@ let send_request_string msg =
let read_from_client =
let buf = String.make 1024 ' ' in
fun () ->
fun blocking ->
match !socket with
| None -> assert false
| Some sock ->
let read = Unix.read sock buf 0 1024 in
String.sub buf 0 read
if blocking then
let _ = Unix.select [sock] [] [] (-1.0) in
let read = Unix.read sock buf 0 1024 in
String.sub buf 0 read
else try
let read = Unix.read sock buf 0 1024 in
String.sub buf 0 read
with Unix.Unix_error ((Unix.EAGAIN | Unix.EWOULDBLOCK), _, _) -> ""
type answer =
{
......@@ -44,7 +52,7 @@ type answer =
out_file : string;
}
let socket_name : string ref = ref ""
let socket_name : string ref = ref "why3server.sock"
let set_socket_name s =
socket_name := s
......@@ -58,7 +66,28 @@ let connect () =
let disconnect () =
client_disconnect ()
let run_server () =
let id =
Unix.create_process "why3server"
[|"why3server"; "--socket"; !socket_name|]
Unix.stdin Unix.stdout Unix.stderr
in
at_exit (fun () ->
Unix.kill id 9;
if Sys.os_type <> "Win32" then Sys.remove !socket_name
)
let force_connect () =
match !socket with
| None when !standalone ->
run_server ();
(* sleep is needed before connecting, or the server will not be ready yet *)
ignore (Unix.select [] [] [] 0.1);
connect()
| _ -> ()
let send_request ~id ~timelimit ~memlimit ~cmd =
force_connect ();
let buf = Buffer.create 128 in
Buffer.add_string buf (string_of_int id);
Buffer.add_char buf ';';
......@@ -73,8 +102,8 @@ let send_request ~id ~timelimit ~memlimit ~cmd =
let s = Buffer.contents buf in
send_request_string s
let rec read_lines () =
let s = read_from_client () in
let rec read_lines blocking =
let s = read_from_client blocking in
if String.contains s '\n' then begin
let s = Buffer.contents buf ^ s in
Buffer.clear buf;
......@@ -91,7 +120,7 @@ let rec read_lines () =
end
end else begin
Buffer.add_string buf s;
read_lines ()
read_lines blocking
end
let bool_of_timeout_string s =
......@@ -114,5 +143,5 @@ let read_answer s =
|_ ->
assert false
let read_answers () =
List.map read_answer (List.filter (fun x -> x <> "") (read_lines ()))
let read_answers ~blocking =
List.map read_answer (List.filter (fun x -> x <> "") (read_lines blocking))
val standalone : bool ref
val set_socket_name : string -> unit
val connect : unit -> unit
......@@ -18,6 +20,6 @@ type answer =
out_file : string;
}
val read_answers : unit -> answer list
val read_answers : blocking:bool -> answer list
val disconnect : unit -> unit
#include <stdio.h>
#include <stdlib.h>
#include "logging.h"
#include "options.h"
FILE* logfile;
void init_logging() {
if (logging) {
logfile = fopen("why3server.log", "w");
}
}
void log_msg(char* s) {
if (logging) {
fprintf (logfile, "%s\n", s);
}
}
void logging_shutdown(char* s) {
if (logging) {
log_msg(s);
fclose(logfile);
}
exit(1);
}
......@@ -6,11 +6,13 @@
int parallel = 1;
char* basename = NULL;
bool logging = false;
void parse_options(int argc, char **argv) {
static struct option long_options[] = {
/* These options set a flag. */
{"socket", required_argument, 0, 's'},
{"logging", no_argument, 0, 'l'},
{0, 0, 0, 0}
};
while (1) {
......@@ -41,6 +43,9 @@ void parse_options(int argc, char **argv) {
}
break;
case 'l':
logging = true;
break;
case 's':
basename = optarg;
break;
......
#ifndef OPTIONS_H
#define OPTIONS_H
#include <stdbool.h>
extern int parallel;
extern char* basename;
extern bool logging;
//parse command line options and set the variables <basename> and <parallel>
void parse_options(int argc, char **argv);
......
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