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

12
open Format
13
open Model_parser
14

15 16 17 18
let debug = Debug.register_info_flag "call_prover"
  ~desc:"Print@ debugging@ messages@ about@ prover@ calls@ \
         and@ keep@ temporary@ files."

19 20 21 22 23 24 25
(** time regexp "%h:%m:%s" *)
type timeunit =
  | Hour
  | Min
  | Sec
  | Msec

26 27 28
type timeregexp = {
  re    : Str.regexp;
  group : timeunit array; (* i-th corresponds to the group i+1 *)
29 30
}

31
type stepregexp = {
32
  steps_re        : Str.regexp;
33 34
  steps_group_num : int;
  (* the number of matched group which corresponds to the number of steps *)
35 36
}

37
let timeregexp s =
38 39 40 41 42 43 44 45 46 47
  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
48 49
    | x -> failwith ("unknown time format specifier: %%" ^
            x ^ " (should be either %%h, %%m, %%s or %%i")
50 51 52 53 54 55 56 57 58 59 60 61 62
  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 ->
63
              let v = Str.matched_group (succ i) out in
64
              match u with
65 66 67
                | Hour -> t := !t +. float_of_string v *. 3600.
                | Min  -> t := !t +. float_of_string v *. 60.
                | Sec  -> t := !t +. float_of_string v
68 69 70 71 72
                | Msec -> t := !t +. float_of_string v /. 1000. ) re.group;
            Some( !t )
      with _ -> grep_time out l
    end

73
let stepregexp s_re s_group_num =
74 75 76 77 78 79 80 81 82 83 84
  {steps_re = (Str.regexp s_re); steps_group_num = s_group_num}

let rec grep_steps out = function
  | [] -> None
  | re :: l ->
    begin try
	    ignore (Str.search_forward re.steps_re out 0);
	    let v = Str.matched_group (re.steps_group_num) out in
	    Some(int_of_string v)
      with _ -> grep_steps out l
    end
85 86 87

(** *)

88
type prover_answer =
89 90 91
  | Valid
  | Invalid
  | Timeout
92
  | OutOfMemory
93
  | StepLimitExceeded
94 95
  | Unknown of string
  | Failure of string
96 97
  | HighFailure

98 99
type prover_result = {
  pr_answer : prover_answer;
100
  pr_status : Unix.process_status;
101 102
  pr_output : string;
  pr_time   : float;
103
  pr_steps  : int;		(* -1 if unknown *)
104
  pr_model  : model;
105 106
}

107 108 109
type prover_result_parser = {
  prp_regexps     : (Str.regexp * prover_answer) list;
  prp_timeregexps : timeregexp list;
110
  prp_stepregexps : stepregexp list;
111
  prp_exitcodes   : (int * prover_answer) list;
112
  prp_model_parser : Model_parser.model_parser;
113 114
}

115 116 117
let print_prover_answer fmt = function
  | Valid -> fprintf fmt "Valid"
  | Invalid -> fprintf fmt "Invalid"
118
  | Timeout -> fprintf fmt "Timeout"
119
  | OutOfMemory -> fprintf fmt "Ouf Of Memory"
120
  | StepLimitExceeded -> fprintf fmt "Step limit exceeded"
121 122
  | Unknown "" -> fprintf fmt "Unknown"
  | Failure "" -> fprintf fmt "Failure"
123 124
  | Unknown s -> fprintf fmt "Unknown (%s)" s
  | Failure s -> fprintf fmt "Failure (%s)" s
125 126
  | HighFailure -> fprintf fmt "HighFailure"

127 128 129 130 131
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

132 133 134
let print_steps fmt s =
  if s >= 0 then fprintf fmt ", %d steps)" s

135
let print_prover_result fmt
136
  {pr_answer=ans; pr_status=status; pr_output=out; pr_time=t; pr_steps=s; pr_model=m} =
137
  fprintf fmt "%a (%.2fs%a)" print_prover_answer ans t print_steps s;
138
  if m <> Model_parser.empty_model then begin
139 140 141
    fprintf fmt "\nCounter-example model:";
    Model_parser.print_model fmt m
  end;
142 143 144
  if ans == HighFailure then
    fprintf fmt "@\nProver exit status: %a@\nProver output:@\n%s@."
      print_prover_status status out
145

146
let rec grep out l = match l with
147
  | [] ->
148 149
      HighFailure
  | (re,pa) :: l ->
150 151 152
      begin try
        ignore (Str.search_forward re out 0);
        match pa with
153
        | Valid | Invalid | Timeout | OutOfMemory | StepLimitExceeded -> pa
154 155 156
        | Unknown s -> Unknown (Str.replace_matched s out)
        | Failure s -> Failure (Str.replace_matched s out)
        | HighFailure -> assert false
157
      with Not_found -> grep out l end
158

159
type post_prover_call = unit -> prover_result
160 161 162 163 164 165

type prover_call = {
  call : Unix.process_status -> post_prover_call;
  pid  : int
}

Andrei Paskevich's avatar
Andrei Paskevich committed
166
type pre_prover_call = unit -> prover_call
167

168 169
let save f = f ^ ".save"

170 171 172
let debug_print_model model =
  Debug.dprintf debug "Call_provers: %s@." (Model_parser.model_to_string model)
  
173

174
let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_mapping =
175 176 177 178 179 180 181 182 183 184 185 186 187
  let ans = match ret with
    | Unix.WSTOPPED n ->
        Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
        grep out res_parser.prp_regexps
    | Unix.WSIGNALED n ->
        Debug.dprintf debug "Call_provers: killed by signal %d@." n;
        grep out res_parser.prp_regexps
    | Unix.WEXITED n ->
        Debug.dprintf debug "Call_provers: exited with status %d@." n;
        (try List.assoc n res_parser.prp_exitcodes
         with Not_found -> grep out res_parser.prp_regexps)
  in
  Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
188
  let time = Opt.get_def (time) (grep_time out res_parser.prp_timeregexps) in
189
  let steps = Opt.get_def (-1) (grep_steps out res_parser.prp_stepregexps) in
190
  let ans = match ans with
191
    | Unknown _ | HighFailure when on_timelimit && timelimit > 0
192 193 194
      && time >= (0.9 *. float timelimit) -> Timeout
    | _ -> ans
  in
195
  let model = res_parser.prp_model_parser out printer_mapping in
196
  Debug.dprintf debug "Call_provers: model:@.";
197
  debug_print_model model;
198 199
  { pr_answer = ans;
    pr_status = ret;
200
    pr_output = out;
201 202
    pr_time   = time;
    pr_steps  = steps;
203
    pr_model  = model;
204
  }
205

206
let actualcommand command timelimit memlimit steplimit file =
Andrei Paskevich's avatar
Andrei Paskevich committed
207
  let arglist = Cmdline.cmdline_split command in
208
  let use_stdin = ref true in
209
  (* FIXME: use_stdin is never modified below ?? *)
210
  let on_timelimit = ref false in
211
  let cmd_regexp = Str.regexp "%\\(.\\)" in
212
  let replace s = match Str.matched_group 1 s with
213
    | "%" -> "%"
Johannes Kanig's avatar
Johannes Kanig committed
214
    | "f" -> file
215
    | "t" -> on_timelimit := true; string_of_int timelimit
216
    | "T" -> string_of_int (succ timelimit)
217
    | "U" -> string_of_int (2 * timelimit + 1)
218
    | "m" -> string_of_int memlimit
219 220 221
    (* 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? *)
222
    | "l" -> Config.libdir
223
    | "d" -> Config.datadir
224
    | "S" -> string_of_int steplimit
225
    | _ -> failwith "unknown specifier, use %%, %f, %t, %T, %U, %m, %l, %d or %S"
226
  in
227
  (* FIXME: are we sure that tuples are evaluated from left to right ? *)
Johannes Kanig's avatar
Johannes Kanig committed
228 229 230
  List.map (Str.global_substitute cmd_regexp replace) arglist,
  !use_stdin, !on_timelimit

231
let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(steplimit=(-1))
Johannes Kanig's avatar
Johannes Kanig committed
232
                 ~res_parser
233
		 ~printer_mapping
Johannes Kanig's avatar
Johannes Kanig committed
234 235 236
                 ?(cleanup=false) ?(inplace=false) ?(redirect=true) fin =

  let command, use_stdin, on_timelimit =
237
    try actualcommand command timelimit memlimit steplimit fin
238 239 240
    with e ->
      if cleanup then Sys.remove fin;
      if inplace then Sys.rename (save fin) fin;
Johannes Kanig's avatar
Johannes Kanig committed
241 242
      raise e in
  let exec = List.hd command in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
243
  Debug.dprintf debug "@[<hov 2>Call_provers: command is: %a@]@."
Johannes Kanig's avatar
Johannes Kanig committed
244 245
    (Pp.print_list Pp.space pp_print_string) command;
  let argarray = Array.of_list command in
Andrei Paskevich's avatar
Andrei Paskevich committed
246

247
  fun () ->
248 249
    let fd_in = if use_stdin then
      Unix.openfile fin [Unix.O_RDONLY] 0 else Unix.stdin in
250 251
    let fout,cout,fd_out,fd_err =
      if redirect then
252 253
        let fout,cout =
          Filename.open_temp_file (Filename.basename fin) ".out" in
254 255 256 257
        let fd_out = Unix.descr_of_out_channel cout in
        fout, cout, fd_out, fd_out
      else
        "", stdout, Unix.stdout, Unix.stderr in
Andrei Paskevich's avatar
Andrei Paskevich committed
258
    let time = Unix.gettimeofday () in
Johannes Kanig's avatar
Johannes Kanig committed
259 260
    let pid = Unix.create_process exec argarray fd_in fd_out fd_err in
    if use_stdin then Unix.close fd_in;
261
    if redirect then close_out cout;
Andrei Paskevich's avatar
Andrei Paskevich committed
262

263
    let call = fun ret ->
Andrei Paskevich's avatar
Andrei Paskevich committed
264
      let time = Unix.gettimeofday () -. time in
265 266 267 268 269 270 271
      let out =
        if redirect then
          let cout = open_in fout in
          let out = Sysutil.channel_contents cout in
          close_in cout;
          out
        else "" in
Andrei Paskevich's avatar
Andrei Paskevich committed
272

Andrei Paskevich's avatar
Andrei Paskevich committed
273
      fun () ->
274
        if Debug.test_noflag debug then begin
275 276 277 278 279
          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
Andrei Paskevich's avatar
Andrei Paskevich committed
280
        end;
281
        parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_mapping
282 283
    in
    { call = call; pid = pid }
284

285
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0) ?(steplimit=(-1))
286
                   ~res_parser ~filename
287
		   ~printer_mapping
288 289 290 291 292 293 294 295
                   ?(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
296
  Buffer.output_buffer cin buffer; close_out cin;
297
  call_on_file ~command ~timelimit ~memlimit ~steplimit
298
               ~res_parser ~printer_mapping ~cleanup:true ~inplace fin
299

300 301 302
let query_call pc =
  let pid, ret = Unix.waitpid [Unix.WNOHANG] pc.pid in
  if pid = 0 then None else Some (pc.call ret)
303

304 305
let wait_on_call pc =
  let _, ret = Unix.waitpid [] pc.pid in pc.call ret
Andrei Paskevich's avatar
Andrei Paskevich committed
306

307
let post_wait_call pc ret = pc.call ret
Andrei Paskevich's avatar
Andrei Paskevich committed
308

309
let prover_call_pid pc = pc.pid