prove_client.ml 7.59 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12
let socket : Unix.file_descr option ref = ref None
13

14 15 16 17 18 19
exception NotConnected
exception AlreadyConnected
exception InvalidAnswer of string

let is_connected () = !socket <> None

MARCHE Claude's avatar
MARCHE Claude committed
20
let client_connect ~fail socket_name =
21
  if !socket <> None then raise AlreadyConnected;
MARCHE Claude's avatar
MARCHE Claude committed
22 23 24 25 26 27 28
  try
    let sock =
      if Sys.os_type = "Win32" then
        let name = "\\\\.\\pipe\\" ^ socket_name in
        Unix.openfile name [Unix.O_RDWR] 0
      else
      let sock = Unix.socket Unix.PF_UNIX Unix.SOCK_STREAM 0 in
29
      Unix.connect sock (Unix.ADDR_UNIX socket_name);
MARCHE Claude's avatar
MARCHE Claude committed
30 31 32 33 34 35 36 37 38 39 40
      sock
    in
    socket := Some sock
  with
  | Unix.Unix_error(err, func, arg) when fail ->
     Format.eprintf "client_connect: connection failed: %s (%s,%s) (socket_name=%s)@." (Unix.error_message err) func arg socket_name;
     exit 2
  | e when fail ->
     Format.eprintf "client_connect failed for some unexpected reason: %s@\nAborting.@."
                    (Printexc.to_string e);
     exit 2
41 42 43

let client_disconnect () =
  match !socket with
44 45
  | None -> raise NotConnected
  | Some sock ->
46
      socket := None;
47 48
      if Sys.os_type <> "Win32" then
        Unix.shutdown sock Unix.SHUTDOWN_ALL;
49
      Unix.close sock
50 51 52

let send_request_string msg =
  match !socket with
53
  | None -> raise NotConnected
54 55 56 57 58 59 60 61 62 63
  | Some sock ->
      let to_write = String.length msg in
      let rec write pointer =
        if pointer < to_write then
          let written = Unix.write sock msg pointer (to_write - pointer) in
          write (pointer + written)
      in write 0

let read_from_client =
  let buf = String.make 1024 ' ' in
64
  fun blocking ->
65
    match !socket with
66
    | None -> raise NotConnected
67
    | Some sock ->
68 69
        (* we only call read() if we are allowed to block
           or if the socket is ready *)
70 71 72 73 74
        let do_read =
          blocking ||
          (let l,_,_ = Unix.select [sock] [] [] 0.0 in l <> [])
        in
        if do_read then
75 76
          let read = Unix.read sock buf 0 1024 in
          String.sub buf 0 read
77
        else ""
78

79 80 81 82 83 84
(* TODO/FIXME: should we be able to change this setting when
   using an external server? *)
(* TODO/FIXME: this number should be stored server-side and
   consulted via a protocol request, if ever needed. The only
   reason for this reference to be here is to store the config
   setting before the first connection request is issued. *)
85
let max_running_provers : int ref = ref 1
86

87 88 89
let set_max_running_provers x =
  if x <= 0 then invalid_arg "Prove_client.set_max_running_provers";
  max_running_provers := x;
90 91 92 93 94 95 96 97 98 99
  if is_connected () then
    send_request_string ("parallel;" ^ string_of_int x ^ "\n")

let send_buf : Buffer.t = Buffer.create 512
let recv_buf : Buffer.t = Buffer.create 1024

(* FIXME? should we send !max_running_provers once connected? *)
let connect_external socket_name =
  if is_connected () then raise AlreadyConnected;
  Buffer.clear recv_buf;
MARCHE Claude's avatar
MARCHE Claude committed
100
  client_connect ~fail:true socket_name
101 102 103 104 105 106

let connect_internal () =
  if is_connected () then raise AlreadyConnected;
  Buffer.clear recv_buf;
  let cwd = Unix.getcwd () in
  Unix.chdir (Filename.get_temp_dir_name ());
107 108 109 110
  let socket_name = (* Filename.concat (Unix.getcwd ())
    ("why3server." ^ string_of_int (Unix.getpid ()) ^ ".sock") *)
    Filename.temp_file "why3server" "sock"
  in
111
  let exec = Filename.concat Config.libdir "why3server" in
112
  let pid = Unix.create_process exec
113
    [|exec; "--socket"; socket_name;
114
      "--single-client";
115 116 117 118
      "-j"; string_of_int !max_running_provers|]
    Unix.stdin Unix.stdout Unix.stderr in
  Unix.chdir cwd;
  (* sleep before connecting, or the server will not be ready yet *)
119
  let rec try_connect n d =
MARCHE Claude's avatar
MARCHE Claude committed
120 121
    if n <= 0 then client_connect ~fail:true socket_name else
    try client_connect ~fail:false socket_name with _ ->
122 123
      ignore (Unix.select [] [] [] d);
      try_connect (pred n) (d *. 4.0) in
MARCHE Claude's avatar
MARCHE Claude committed
124
  try_connect 5 0.1; (* 0.1, 0.4, 1.6, 6.4, 25.6 *)
125 126 127
  at_exit (fun () -> (* only if succesfully connected *)
    (try client_disconnect () with NotConnected -> ());
    ignore (Unix.waitpid [] pid))
128 129 130 131 132 133

(* TODO/FIXME: how should we handle disconnect if there are still
   tasks in queue? What are the use cases for disconnect? *)
let disconnect = client_disconnect

(* TODO/FIXME: is this the right place to connect-on-demand? *)
134
let send_request ~id ~timelimit ~memlimit ~use_stdin ~cmd =
135 136 137 138 139 140 141 142 143 144
  if not (is_connected ()) then connect_internal ();
  Buffer.clear send_buf;
  let servercommand =
    if use_stdin <> None then "runstdin;" else "run;" in
  Buffer.add_string send_buf servercommand;
  Buffer.add_string send_buf (string_of_int id);
  Buffer.add_char send_buf ';';
  Buffer.add_string send_buf (string_of_int timelimit);
  Buffer.add_char send_buf ';';
  Buffer.add_string send_buf (string_of_int memlimit);
145
  List.iter (fun x ->
146 147
      Buffer.add_char send_buf ';';
      Buffer.add_string send_buf x)
148
    cmd;
149 150 151
  begin match use_stdin with
  | None -> ()
  | Some s ->
152 153
      Buffer.add_char send_buf ';';
      Buffer.add_string send_buf s
154
  end;
155 156
  Buffer.add_char send_buf '\n';
  let s = Buffer.contents send_buf in
157 158
  send_request_string s

159 160
let rec read_lines blocking =
  let s = read_from_client blocking in
161 162 163 164 165
  (* TODO: should we detect and handle EOF here? *)
  if s = "" then [] else
  if String.contains s '\n' then begin
    let s = Buffer.contents recv_buf ^ s in
    Buffer.clear recv_buf;
166 167 168 169 170 171 172 173
    let l = Strings.rev_split '\n' s in
    match l with
    | [] -> assert false
    | [x] -> [x]
    | (x::xs) as l ->
      if x = "" then List.rev xs else
      if x.[String.length x - 1] = '\n' then List.rev l
      else begin
174
        Buffer.add_string recv_buf x;
175 176 177
        List.rev xs
      end
  end else begin
178
    Buffer.add_string recv_buf s;
179
    read_lines blocking
180 181
  end

182
type final_answer = {
183 184 185 186
  id        : int;
  time      : float;
  timeout   : bool;
  out_file  : string;
187
  exit_code : int64;
188
}
189

190 191 192 193
type answer =
  | Started of int
  | Finished of final_answer

194 195 196 197 198 199 200 201 202 203
let read_answer s =
  try
    match Strings.split ';' s with
    | "F":: id :: exit_s :: time_s :: timeout_s :: ( (_ :: _) as rest) ->
        (* same trick we use in other parsing code. The file name may contain
           ';'. Luckily, the file name comes last, so we still split on ';',
           and put the pieces back together afterwards *)
        Finished { id = int_of_string id;
          out_file = Strings.join ";" rest;
          time = float_of_string time_s;
204
          exit_code = Int64.of_string exit_s;
205 206 207 208 209 210 211
          timeout = (timeout_s = "1"); }
    | "S" :: [id] ->
        Started (int_of_string id)
    | _ ->
        raise (InvalidAnswer s)
  with Failure "int_of_string" ->
    raise (InvalidAnswer s)
212

213 214
let read_answers ~blocking =
  List.map read_answer (List.filter (fun x -> x <> "") (read_lines blocking))
215 216 217 218 219 220 221 222 223

let () = Exn_printer.register (fun fmt exn -> match exn with
  | NotConnected ->
      Format.fprintf fmt "Not connected to the proof server"
  | AlreadyConnected ->
      Format.fprintf fmt "Already connected to the proof server"
  | InvalidAnswer s ->
      Format.fprintf fmt "Invalid server answer: %s" s
  | _ -> raise exn)