prove_client.ml 7.02 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10 11
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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

20
let client_connect socket_name =
21
  if !socket <> None then raise AlreadyConnected;
22 23 24 25
  if Sys.os_type = "Win32" then begin
    let name = "\\\\.\\pipe\\" ^ socket_name in
    socket := Some (Unix.openfile name [Unix.O_RDWR] 0)
  end else begin
26
    let sock = Unix.socket Unix.PF_UNIX Unix.SOCK_STREAM 0 in
27 28 29 30 31 32
    Unix.connect sock (Unix.ADDR_UNIX socket_name);
    socket := Some sock
  end

let client_disconnect () =
  match !socket with
33 34
  | None -> raise NotConnected
  | Some sock ->
35
      socket := None;
36 37
      if Sys.os_type <> "Win32" then
        Unix.shutdown sock Unix.SHUTDOWN_ALL;
38
      Unix.close sock
39 40 41

let send_request_string msg =
  match !socket with
42
  | None -> raise NotConnected
43 44 45 46 47 48 49 50 51 52
  | 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
53
  fun blocking ->
54
    match !socket with
55
    | None -> raise NotConnected
56
    | Some sock ->
57 58
        (* we only call read() if we are allowed to block
           or if the socket is ready *)
59 60 61 62 63
        let do_read =
          blocking ||
          (let l,_,_ = Unix.select [sock] [] [] 0.0 in l <> [])
        in
        if do_read then
64 65
          let read = Unix.read sock buf 0 1024 in
          String.sub buf 0 read
66
        else ""
67

68 69 70 71 72 73
(* 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. *)
74
let max_running_provers : int ref = ref 1
75

76 77 78
let set_max_running_provers x =
  if x <= 0 then invalid_arg "Prove_client.set_max_running_provers";
  max_running_provers := x;
79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
  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;
  client_connect socket_name

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 ());
  let socket_name = Filename.concat (Unix.getcwd ())
    ("why3server." ^ string_of_int (Unix.getpid ()) ^ ".sock") in
98
  let exec = Filename.concat Config.libdir "why3server" in
99
  let pid = Unix.create_process exec
100
    [|exec; "--socket"; socket_name;
101
      "--single-client";
102 103 104 105
      "-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 *)
106 107 108 109 110 111 112 113 114
  let rec try_connect n d =
    if n <= 0 then client_connect socket_name else
    try client_connect socket_name with _ ->
      ignore (Unix.select [] [] [] d);
      try_connect (pred n) (d *. 4.0) in
  try_connect 4 0.1; (* 0.1, 0.4, 1.6, 6.4 *)
  at_exit (fun () -> (* only if succesfully connected *)
    (try client_disconnect () with NotConnected -> ());
    ignore (Unix.waitpid [] pid))
115 116 117 118 119 120

(* 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? *)
121
let send_request ~id ~timelimit ~memlimit ~use_stdin ~cmd =
122 123 124 125 126 127 128 129 130 131
  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);
132
  List.iter (fun x ->
133 134
      Buffer.add_char send_buf ';';
      Buffer.add_string send_buf x)
135
    cmd;
136 137 138
  begin match use_stdin with
  | None -> ()
  | Some s ->
139 140
      Buffer.add_char send_buf ';';
      Buffer.add_string send_buf s
141
  end;
142 143
  Buffer.add_char send_buf '\n';
  let s = Buffer.contents send_buf in
144 145
  send_request_string s

146 147
let rec read_lines blocking =
  let s = read_from_client blocking in
148 149 150 151 152
  (* 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;
153 154 155 156 157 158 159 160
    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
161
        Buffer.add_string recv_buf x;
162 163 164
        List.rev xs
      end
  end else begin
165
    Buffer.add_string recv_buf s;
166
    read_lines blocking
167 168
  end

169
type final_answer = {
170 171 172 173 174 175
  id        : int;
  time      : float;
  timeout   : bool;
  out_file  : string;
  exit_code : int;
}
176

177 178 179 180
type answer =
  | Started of int
  | Finished of final_answer

181
let read_answer s = match Strings.split ';' s with
182
  | "F":: id :: exit_s :: time_s :: timeout_s :: ( (_ :: _) as rest) ->
183
      (* same trick we use in other parsing code. The file name may contain
184 185
         ';'. Luckily, the file name comes last, so we still split on ';',
         and put the pieces back together afterwards *)
186
      Finished { id = int_of_string id;
187
        out_file = Strings.join ";" rest;
188 189
        time = float_of_string time_s;
        exit_code = int_of_string exit_s;
190
        timeout = (timeout_s = "1"); }
191 192
  | "S" :: [id] ->
      Started (int_of_string id)
193 194
  | _ ->
      raise (InvalidAnswer s)
195

196 197
let read_answers ~blocking =
  List.map read_answer (List.filter (fun x -> x <> "") (read_lines blocking))
198 199 200 201 202 203 204 205 206

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)