call_provers.ml 8.86 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

21 22
open Format

23 24 25 26 27 28 29
(** time regexp "%h:%m:%s" *)
type timeunit =
  | Hour
  | Min
  | Sec
  | Msec

30 31 32
type timeregexp = {
  re    : Str.regexp;
  group : timeunit array; (* i-th corresponds to the group i+1 *)
33 34
}

35
let timeregexp s =
36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
  let cmd_regexp = Str.regexp "%\\(.\\)" in
  let nb = ref 0 in
  let l = ref [] in
  let add_unit x = l := (!nb,x) :: !l; incr nb; "\\([0-9]+.?[0-9]*\\)" in
  let replace s = match Str.matched_group 1 s with
    | "%" -> "%"
    | "h" -> add_unit Hour
    | "m" -> add_unit Min
    | "s" -> add_unit Sec
    | "i" -> add_unit Msec
    | _ -> failwith "unknown format specifier, use %%h, %%m, %%s, %%i"
  in
  let s = Str.global_substitute cmd_regexp replace s in
  let group = Array.make !nb Hour in
  List.iter (fun (i,u) -> group.(i) <- u) !l;
  { re = Str.regexp s; group = group}

let rec grep_time out = function
  | [] -> None
  | re :: l ->
    begin try
            ignore (Str.search_forward re.re out 0);
            let t = ref 0. in
            Array.iteri (fun i u ->
              let v = float_of_string (Str.matched_group (succ i) out) in
              match u with
                | Hour -> t := !t +. v *. 3600.
                | Min  -> t := !t +. v *. 60.
                | Sec  -> t := !t +. v
                | Msec -> t := !t +. v /. 1000.) re.group;
            Some !t
      with _ -> grep_time out l end

(** *)

71
type prover_answer =
72 73 74
  | Valid
  | Invalid
  | Timeout
75
  | OutOfMemory
76 77
  | Unknown of string
  | Failure of string
78 79
  | HighFailure

80 81
type prover_result = {
  pr_answer : prover_answer;
82
  pr_status : Unix.process_status;
83 84 85 86
  pr_output : string;
  pr_time   : float;
}

87 88 89
let print_prover_answer fmt = function
  | Valid -> fprintf fmt "Valid"
  | Invalid -> fprintf fmt "Invalid"
90
  | Timeout -> fprintf fmt "Timeout"
91
  | OutOfMemory -> fprintf fmt "Ouf Of Memory"
92 93
  | Unknown "" -> fprintf fmt "Unknown"
  | Failure "" -> fprintf fmt "Failure"
94 95
  | Unknown s -> fprintf fmt "Unknown (%s)" s
  | Failure s -> fprintf fmt "Failure (%s)" s
96 97
  | HighFailure -> fprintf fmt "HighFailure"

98 99 100 101 102 103 104
let print_prover_status fmt = function
  | Unix.WSTOPPED n -> fprintf fmt "stopped by signal %d" n
  | Unix.WSIGNALED n -> fprintf fmt "killed by signal %d" n
  | Unix.WEXITED n -> fprintf fmt "exited with status %d" n

let print_prover_result fmt
  {pr_answer=ans; pr_status=status; pr_output=out; pr_time=t} =
105
  fprintf fmt "%a (%.2fs)" print_prover_answer ans t;
106 107 108
  if ans == HighFailure then
    fprintf fmt "@\nProver exit status: %a@\nProver output:@\n%s@."
      print_prover_status status out
109

110
let rec grep out l = match l with
111
  | [] ->
112 113
      HighFailure
  | (re,pa) :: l ->
114 115 116
      begin try
        ignore (Str.search_forward re out 0);
        match pa with
117
        | Valid | Invalid | Timeout | OutOfMemory -> pa
118 119 120
        | Unknown s -> Unknown (Str.replace_matched s out)
        | Failure s -> Failure (Str.replace_matched s out)
        | HighFailure -> assert false
121
      with Not_found -> grep out l end
122

123

124
let debug = Debug.register_info_flag "call_prover"
125
  ~desc:"About@ external@ prover@ calls@ and@ results."
126

127 128
type res_waitpid = int * Unix.process_status

129
type post_prover_call = unit -> prover_result
130 131 132
type prover_call =
  { call: ?res_waitpid:res_waitpid -> Unix.wait_flag list -> post_prover_call;
    pid: int}
Andrei Paskevich's avatar
Andrei Paskevich committed
133
type pre_prover_call = unit -> prover_call
134

135 136
let save f = f ^ ".save"

137 138
let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
                 ~regexps ~timeregexps ~exitcodes
139
                 ?(cleanup=false) ?(inplace=false) fin =
Andrei Paskevich's avatar
Andrei Paskevich committed
140 141 142

  let arglist = Cmdline.cmdline_split command in
  let command = List.hd arglist in
143
  let on_timelimit = ref false in
144
  let cmd_regexp = Str.regexp "%\\(.\\)" in
145
  let replace s = match Str.matched_group 1 s with
146
    | "%" -> "%"
147
    | "f" -> fin
148
    | "t" -> on_timelimit := true; string_of_int timelimit
149
    | "T" -> string_of_int (16 * succ timelimit)
150
    | "m" -> string_of_int memlimit
151 152 153
    (* FIXME: libdir and datadir can be changed in the configuration file
       Should we pass them as additional arguments? Or would it be better
       to prepare the command line in a separate function? *)
154
    | "l" -> Config.libdir
155 156
    | "d" -> Config.datadir
    | _ -> failwith "unknown specifier, use %%f, %%t, %%m, %%l, or %%d"
157
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
158
  let subst s =
159 160 161 162 163 164
    try
      Str.global_substitute cmd_regexp replace s
    with e ->
      if cleanup then Sys.remove fin;
      if inplace then Sys.rename (save fin) fin;
      raise e
165
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
166 167 168 169
  let arglist = List.map subst arglist 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
Andrei Paskevich's avatar
Andrei Paskevich committed
170

171
  fun () ->
Andrei Paskevich's avatar
Andrei Paskevich committed
172 173 174 175 176 177 178 179
    let fd_in = Unix.openfile fin [Unix.O_RDONLY] 0 in
    let fout,cout = Filename.open_temp_file (Filename.basename fin) ".out" in
    let fd_out = Unix.descr_of_out_channel cout in
    let time = Unix.gettimeofday () in
    let pid = Unix.create_process command argarray fd_in fd_out fd_out in
    Unix.close fd_in;
    close_out cout;

180
    let call = fun ?res_waitpid wait_flags ->
Andrei Paskevich's avatar
Andrei Paskevich committed
181
      (* TODO? check that we haven't given the result earlier *)
182 183 184 185
      let res,ret =
        match res_waitpid with
        | Some ((res,_) as res_waitpid) when pid = res -> res_waitpid
        | _ -> Unix.waitpid wait_flags pid in
Andrei Paskevich's avatar
Andrei Paskevich committed
186 187 188 189 190 191
      if res = 0 then raise Exit;
      let time = Unix.gettimeofday () -. time in
      let cout = open_in fout in
      let out = Sysutil.channel_contents cout in
      close_in cout;

Andrei Paskevich's avatar
Andrei Paskevich committed
192 193
      fun () ->
        if Debug.nottest_flag debug then begin
194
          if cleanup then Sys.remove fin;
195
          if inplace then Sys.rename (save fin) fin;
196
          Sys.remove fout
Andrei Paskevich's avatar
Andrei Paskevich committed
197 198 199 200
        end;
        let ans = match ret with
          | Unix.WSTOPPED n ->
              Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
201
              grep out regexps
Andrei Paskevich's avatar
Andrei Paskevich committed
202 203
          | Unix.WSIGNALED n ->
              Debug.dprintf debug "Call_provers: killed by signal %d@." n;
204
              grep out regexps
Andrei Paskevich's avatar
Andrei Paskevich committed
205 206 207 208 209
          | Unix.WEXITED n ->
              Debug.dprintf debug "Call_provers: exited with status %d@." n;
              (try List.assoc n exitcodes with Not_found -> grep out regexps)
        in
        Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
210
        let time = Util.def_option time (grep_time out timeregexps) in
Andrei Paskevich's avatar
Andrei Paskevich committed
211 212 213 214 215 216
        let ans = match ans with
          | HighFailure when !on_timelimit && timelimit > 0
            && time >= (0.9 *. float timelimit) -> Timeout
          | _ -> ans
        in
        { pr_answer = ans;
217
          pr_status = ret;
Andrei Paskevich's avatar
Andrei Paskevich committed
218
          pr_output = out;
219 220
          pr_time   = time } in
    {call = call; pid = pid}
221

222
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
223 224 225 226 227 228 229 230 231
                   ~regexps ~timeregexps ~exitcodes ~filename
                   ?(inplace=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
232 233
  Buffer.output_buffer cin buffer; close_out cin;
  call_on_file ~command ~timelimit ~memlimit
234
               ~regexps ~timeregexps ~exitcodes ~cleanup:true ~inplace fin
235

236 237 238 239 240 241 242 243 244
let query_call ?res_waitpid call =
  try Some (call.call ?res_waitpid [Unix.WNOHANG]) with Exit -> None

let wait_on_call ?res_waitpid call = call.call ?res_waitpid []

let query_wait_all wait_flags =
  let res,_ as res_waitpid = Unix.waitpid wait_flags 0 in
  if res = 0 then raise Exit;
  res_waitpid
Andrei Paskevich's avatar
Andrei Paskevich committed
245

246 247
let query_all () = try Some (query_wait_all [Unix.WNOHANG]) with Exit -> None
let wait_all ()  = query_wait_all []
Andrei Paskevich's avatar
Andrei Paskevich committed
248

249
let prover_call_pid pc = pc.pid