call_provers.ml 18.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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."

Guillaume Melquiond's avatar
Guillaume Melquiond committed
19 20
let debug_attrs = Debug.register_info_flag "print_attrs"
  ~desc:"Print@ attrs@ of@ identifiers@ and@ expressions."
21

22
(* BEGIN{proveranswer} anchor for automatic documentation, do not remove *)
23 24 25 26 27 28
type prover_answer =
  | Valid
  | Invalid
  | Timeout
  | OutOfMemory
  | StepLimitExceeded
29
  | Unknown of string
30 31
  | Failure of string
  | HighFailure
32
(* END{proveranswer} anchor for automatic documentation, do not remove *)
33

34
(* BEGIN{proverresult} anchor for automatic documentation, do not remove *)
35 36 37 38 39 40 41 42
type prover_result = {
  pr_answer : prover_answer;
  pr_status : Unix.process_status;
  pr_output : string;
  pr_time   : float;
  pr_steps  : int;		(* -1 if unknown *)
  pr_model  : model;
}
43
(* END{proverresult} anchor for automatic documentation, do not remove *)
44

45
(* BEGIN{resourcelimit} anchor for automatic documentation, do not remove *)
46 47 48 49 50
type resource_limit = {
  limit_time  : int;
  limit_mem   : int;
  limit_steps : int;
}
51
(* END{resourcelimit} anchor for automatic documentation, do not remove *)
52

53
let empty_limit = { limit_time = 0 ; limit_mem = 0; limit_steps = 0 }
54

55 56 57 58 59 60
let limit_max =
  let single_limit_max a b = if a = 0 || b = 0 then 0 else max a b in
  fun a b ->
    { limit_time = single_limit_max a.limit_time b.limit_time;
      limit_steps = single_limit_max a.limit_steps b.limit_steps;
      limit_mem = single_limit_max a.limit_mem b.limit_mem; }
61

62 63 64 65 66 67
type timeunit =
  | Hour
  | Min
  | Sec
  | Msec

68 69 70
type timeregexp = {
  re    : Str.regexp;
  group : timeunit array; (* i-th corresponds to the group i+1 *)
71 72
}

73
type stepregexp = {
74
  steps_re        : Str.regexp;
75 76
  steps_group_num : int;
  (* the number of matched group which corresponds to the number of steps *)
77 78
}

79
let timeregexp s =
80 81 82 83 84 85 86 87 88 89
  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
90 91
    | x -> failwith ("unknown time format specifier: %%" ^
            x ^ " (should be either %%h, %%m, %%s or %%i")
92 93 94 95
  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;
96
  { re = Str.regexp s; group = group }
97 98 99 100

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

114
let stepregexp s_re s_group_num =
115 116 117 118 119
  {steps_re = (Str.regexp s_re); steps_group_num = s_group_num}

let rec grep_steps out = function
  | [] -> None
  | re :: l ->
120 121 122 123 124
      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
125

126
(*
127 128
let grep_reason_unknown out =
  try
129
    (* TODO: this is SMTLIB specific, should be done in drivers instead *)
130 131
    let re = Str.regexp "^(:reason-unknown \\([^)]*\\)" in
    ignore (Str.search_forward re out 0);
132
    match (Str.matched_group 1 out) with
133 134 135 136
    | "resourceout" -> Resourceout
    | _ -> Other
  with Not_found ->
    Other
137
 *)
138

139
type prover_result_parser = {
140
  prp_regexps     : (string * prover_answer) list;
141
  prp_timeregexps : timeregexp list;
142
  prp_stepregexps : stepregexp list;
143
  prp_exitcodes   : (int * prover_answer) list;
144
  prp_model_parser : Model_parser.model_parser;
145 146
}

147 148 149
let print_prover_answer fmt = function
  | Valid -> fprintf fmt "Valid"
  | Invalid -> fprintf fmt "Invalid"
150
  | Timeout -> fprintf fmt "Timeout"
151
  | OutOfMemory -> fprintf fmt "Ouf Of Memory"
152
  | StepLimitExceeded -> fprintf fmt "Step limit exceeded"
153
  | Unknown s -> fprintf fmt "Unknown (%s)" s
154
  | Failure s -> fprintf fmt "Failure (%s)" s
155 156
  | HighFailure -> fprintf fmt "HighFailure"

157 158 159 160 161
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

162
let print_steps fmt s =
163
  if s >= 0 then fprintf fmt ", %d steps" s
164

165 166 167
let print_prover_result fmt {pr_answer = ans; pr_status = status;
                             pr_output = out; pr_time   = t;
                             pr_steps  = s;   pr_model  = m} =
Guillaume Melquiond's avatar
Guillaume Melquiond committed
168
  let print_attrs = Debug.test_flag debug_attrs in
169
  fprintf fmt "%a (%.2fs%a)" print_prover_answer ans t print_steps s;
170
  if not (Model_parser.is_model_empty m) then begin
171
    fprintf fmt "\nCounter-example model:";
Guillaume Melquiond's avatar
Guillaume Melquiond committed
172
    Model_parser.print_model ~print_attrs fmt m
173
  end;
174 175 176
  if ans == HighFailure then
    fprintf fmt "@\nProver exit status: %a@\nProver output:@\n%s@."
      print_prover_status status out
177

178
let rec grep out l = match l with
179
  | [] ->
180 181
      HighFailure
  | (re,pa) :: l ->
182 183 184
      begin try
        ignore (Str.search_forward re out 0);
        match pa with
185
        | Valid | Invalid | Timeout | OutOfMemory | StepLimitExceeded -> pa
186
        | Unknown s -> Unknown (Str.replace_matched s out)
187 188
        | Failure s -> Failure (Str.replace_matched s out)
        | HighFailure -> assert false
189
      with Not_found -> grep out l end
190

191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
(*
let rec grep out l = match l with
  | [] ->
      HighFailure
  | (re,pa) :: l ->
      begin try
        ignore (Str.search_forward re out 0);
        match pa with
        | Valid | Invalid | Timeout | OutOfMemory | StepLimitExceeded -> pa
        | Unknown (s, ru) -> Unknown ((Str.replace_matched s out), ru)
        | Failure s -> Failure (Str.replace_matched s out)
        | HighFailure -> assert false
      with Not_found -> grep out l end
*)

Sylvain Dailler's avatar
Sylvain Dailler committed
206
(* Create a regexp matching the same as the union of all regexp of the list. *)
207 208 209 210 211 212
let craft_efficient_re l =
  let s = Format.asprintf "%a"
    (Pp.print_list_delim
       ~start:(fun fmt () -> Format.fprintf fmt "\\(")
       ~stop:(fun fmt () -> Format.fprintf fmt "\\)")
       ~sep:(fun fmt () -> Format.fprintf fmt "\\|")
213
       (fun fmt (a, _b) -> Format.fprintf fmt "%s" a)) l
214 215
  in
  Str.regexp s
216

217 218 219 220 221 222
(*
let print_delim fmt d =
  match d with
  | Str.Delim s -> Format.fprintf fmt "Delim %s" s
  | Str.Text s -> Format.fprintf fmt "Text %s" s
 *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
223 224
let debug_print_model ~print_attrs model =
  let model_str = Model_parser.model_to_string ~print_attrs model in
225 226
  Debug.dprintf debug "Call_provers: %s@." model_str

227 228
type answer_or_model = Answer of prover_answer | Model of string

229 230
let analyse_result res_parser printer_mapping out =
  let list_re = res_parser.prp_regexps in
Sylvain Dailler's avatar
Sylvain Dailler committed
231 232 233
  let re = craft_efficient_re list_re in
  let list_re = List.map (fun (a, b) -> Str.regexp a, b) list_re in
  let result_list = Str.full_split re out in
234 235 236 237 238 239 240
  let result_list =
    List.map
      (function
        | Str.Delim r -> Answer (grep r list_re)
        | Str.Text t -> Model t)
      result_list
  in
241 242 243
(*  Format.eprintf "[incremental model parsing] results list is @[[%a]@]@."
                 (Pp.print_list Pp.semi print_delim) result_list;
*)
Sylvain Dailler's avatar
Sylvain Dailler committed
244 245 246
  let rec analyse saved_model saved_res l =
    match l with
    | [] ->
247 248 249 250
        if saved_res = None then
          (HighFailure, saved_model)
        else
          (Opt.get saved_res, saved_model)
251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269
    | Answer res1 :: (Answer res2 :: tl as tl1) ->
       Debug.dprintf debug "Call_provers: two consecutive answers: %a %a@."
          print_prover_answer res1 print_prover_answer res2;
       begin
         match res1,res2 with
         | Unknown _, Unknown "resourceout" ->
            analyse saved_model saved_res (Answer StepLimitExceeded :: tl)
         | Unknown _, Unknown "timeout" ->
            analyse saved_model saved_res (Answer Timeout :: tl)
         | Unknown "", Unknown _ ->
            analyse saved_model saved_res tl1
         | Unknown s1, Unknown "" ->
            analyse saved_model saved_res (Answer (Unknown s1) :: tl)
         | Unknown s1, Unknown s2 ->
            analyse saved_model saved_res (Answer (Unknown (s1 ^ " + " ^ s2)) :: tl)
         | _,_ ->
            analyse saved_model saved_res tl1
       end
    | Answer res :: Model model :: tl ->
Sylvain Dailler's avatar
Sylvain Dailler committed
270 271 272
        if res = Valid then
          (Valid, None)
        else
273 274 275
          (* get model if possible *)
          let m = res_parser.prp_model_parser model printer_mapping in
          Debug.dprintf debug "Call_provers: model:@.";
Guillaume Melquiond's avatar
Guillaume Melquiond committed
276
          debug_print_model ~print_attrs:false m;
277 278
          let m = if is_model_empty m then saved_model else (Some m) in
          analyse m (Some res) tl
279
    | Answer res :: tl ->
Sylvain Dailler's avatar
Sylvain Dailler committed
280 281 282 283
        if res = Valid then
          (Valid, None)
        else
          analyse saved_model (Some res) tl
284
    | Model _fail :: tl -> analyse saved_model saved_res tl
285
  in
Sylvain Dailler's avatar
Sylvain Dailler committed
286 287

  analyse None None result_list
288

289
let backup_file f = f ^ ".save"
290

291

292
let parse_prover_run res_parser signaled time out exitcode limit ~printer_mapping =
293 294 295 296 297 298
  Debug.dprintf debug "Call_provers: exited with status %Ld@." exitcode;
  (* the following conversion is incorrect (but does not fail) on 32bit, but if
     the incoming exitcode was really outside the bounds of [int], its exact
     value is meaningless for Why3 anyway (e.g. some windows status codes). If
     it becomes meaningful, we might want to change the conversion here *)
  let int_exitcode = Int64.to_int exitcode in
Sylvain Dailler's avatar
Sylvain Dailler committed
299
  let ans, model =
300
    if signaled then HighFailure, None else
Sylvain Dailler's avatar
Sylvain Dailler committed
301
    try List.assoc int_exitcode res_parser.prp_exitcodes, None
302
    with Not_found -> analyse_result res_parser printer_mapping out
303 304 305
      (* TODO let (n, m, t) = greps out res_parser.prp_regexps in
      t, None *)
  in
306
  let model = match model with Some s -> s | None -> default_model in
307
  Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
308
  let time = Opt.get_def (time) (grep_time out res_parser.prp_timeregexps) in
309
  let steps = Opt.get_def (-1) (grep_steps out res_parser.prp_stepregexps) in
310
  (* HighFailure or Unknown close to time limit are assumed to be timeouts *)
311 312
  let tlimit = float limit.limit_time in
  let ans, time =
313
    if tlimit > 0.0 && time >= 0.9 *. tlimit -. 0.1 then
314
    match ans with
315 316
    | HighFailure | Unknown _ | Timeout ->
       Debug.dprintf debug
317
         "[Call_provers.parse_prover_run] answer after %f >= 0.9 timelimit - 0.1 -> Timeout@." time;
318 319
       Timeout, tlimit
    | _ -> ans,time
320
    else ans, time
321
  in
322
  { pr_answer = ans;
323
    pr_status = if signaled then Unix.WSIGNALED int_exitcode else Unix.WEXITED int_exitcode;
324
    pr_output = out;
325 326
    pr_time   = time;
    pr_steps  = steps;
327
    pr_model  = model;
328
  }
329

330
let actualcommand command limit file =
331 332
  let stime = string_of_int limit.limit_time in
  let smem = string_of_int limit.limit_mem in
Andrei Paskevich's avatar
Andrei Paskevich committed
333
  let arglist = Cmdline.cmdline_split command in
334
  let use_stdin = ref true in
335
  let on_timelimit = ref false in
336
  let cmd_regexp = Str.regexp "%\\(.\\)" in
337
  let replace s = match Str.matched_group 1 s with
338
    | "%" -> "%"
339
    | "f" -> use_stdin := false; file
340
    | "t" -> on_timelimit := true; stime
341
    | "m" -> smem
342 343 344
    (* 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? *)
345
    | "l" -> Config.libdir
346
    | "d" -> Config.datadir
347
    | "S" -> string_of_int limit.limit_steps
348
    | _ -> failwith "unknown specifier, use %%, %f, %t, %m, %l, %d or %S"
349
  in
350 351 352 353
  let args =
    List.map (Str.global_substitute cmd_regexp replace) arglist
  in
  args, !use_stdin, !on_timelimit
Johannes Kanig's avatar
Johannes Kanig committed
354

355
let actualcommand ~cleanup ~inplace command limit file =
356 357 358 359 360 361 362
  try
    let (cmd, _,_) as x =
      actualcommand command limit file
    in
    Debug.dprintf debug "@[<hv 2>Call_provers: actual command is:@ @[%a@]@]@."
                  (Pp.print_list Pp.space pp_print_string) cmd;
    x
363
  with e ->
364 365 366 367
    Debug.dprintf
      debug
      "@[<hv 2>Call_provers: failed to build an actual corresponding to@ %s@]@."
      command;
368 369 370 371 372
    if cleanup then Sys.remove file;
    if inplace then Sys.rename (backup_file file) file;
    raise e

let adapt_limits limit on_timelimit =
373 374 375 376 377 378
  if limit.limit_time = empty_limit.limit_time then limit
  else
    { limit with limit_time =
      (* for steps limit use 2 * t + 1 time *)
      if limit.limit_steps <> empty_limit.limit_steps
      then (2 * limit.limit_time + 1)
MARCHE Claude's avatar
MARCHE Claude committed
379 380
      (* if prover implements time limit, use 4t + 1 *)
      else if on_timelimit then 4 * limit.limit_time + 1
381 382
      (* otherwise use t *)
      else limit.limit_time }
383

384
type server_id = int
385

386 387 388 389 390 391
let gen_id =
  let x = ref 0 in
  fun () ->
    incr x;
    !x

392 393 394 395 396 397 398
type save_data = {
  vc_file    : string;
  inplace    : bool;
  limit      : resource_limit;
  res_parser : prover_result_parser;
  printer_mapping : Printer.printer_mapping;
}
399

400
let saved_data : (int, save_data) Hashtbl.t = Hashtbl.create 17
401 402 403

let read_and_delete_file fn =
  let cin = open_in fn in
404 405 406 407
  let out = Sysutil.channel_contents cin in
  close_in cin;
  if Debug.test_noflag debug then Sys.remove fn;
  out
408

409 410
open Prove_client

411
let handle_answer answer =
412
  match answer with
413
  | Finished { id; time; timeout; out_file; exit_code } ->
414 415
      let save = Hashtbl.find saved_data id in
      Hashtbl.remove saved_data id;
416 417 418 419 420
      let keep_vcs =
        try let flag = Debug.lookup_flag "keep_vcs" in Debug.test_flag flag with
        | _ -> false
      in
      if Debug.test_noflag debug && not keep_vcs then begin
421 422
        Sys.remove save.vc_file;
        if save.inplace then Sys.rename (backup_file save.vc_file) save.vc_file
423
      end;
424 425
      let out = read_and_delete_file out_file in
      let ret = exit_code in
426 427
      let printer_mapping = save.printer_mapping in
      let ans = parse_prover_run save.res_parser
428
          timeout time out ret save.limit ~printer_mapping in
429
      id, Some ans
430
  | Started id ->
431
      id, None
432

433
let wait_for_server_result ~blocking =
434
  List.map handle_answer (read_answers ~blocking)
435

436 437
type prover_call =
  | ServerCall of server_id
Andrei Paskevich's avatar
Andrei Paskevich committed
438
  | EditorCall of int
439 440

let call_on_file ~command ~limit ~res_parser ~printer_mapping
Andrei Paskevich's avatar
Andrei Paskevich committed
441
                 ?(inplace=false) fin =
442
  let id = gen_id () in
443
  let cmd, use_stdin, on_timelimit =
444
    actualcommand ~cleanup:true ~inplace command limit fin in
445 446 447 448 449 450
  let save = {
    vc_file    = fin;
    inplace    = inplace;
    limit      = limit;
    res_parser = res_parser;
    printer_mapping = printer_mapping } in
451
  Hashtbl.add saved_data id save;
452
  let limit = adapt_limits limit on_timelimit in
453
  let use_stdin = if use_stdin then Some fin else None in
454 455 456 457 458
  Debug.dprintf
    debug
    "Request sent to prove_client:@ timelimit=%d@ memlimit=%d@ cmd=@[[%a]@]@."
    limit.limit_time limit.limit_mem
    (Pp.print_list Pp.comma Pp.string) cmd;
459
  send_request ~use_stdin ~id
460 461 462
                            ~timelimit:limit.limit_time
                            ~memlimit:limit.limit_mem
                            ~cmd;
463
  ServerCall id
464

Andrei Paskevich's avatar
Andrei Paskevich committed
465 466
type prover_update =
  | NoUpdates
467 468
  | ProverInterrupted
  | InternalFailure of exn
Andrei Paskevich's avatar
Andrei Paskevich committed
469 470 471 472 473
  | ProverStarted
  | ProverFinished of prover_result

let result_buffer : (server_id, prover_update) Hashtbl.t = Hashtbl.create 17

474
let fetch_new_results ~blocking = (* TODO: handle ProverStarted events *)
475 476 477 478 479
  List.iter (fun (id, r) ->
    let x = match r with
    | Some r -> ProverFinished r
    | None -> ProverStarted in
    Hashtbl.add result_buffer id x)
480 481
    (wait_for_server_result ~blocking)

482 483
let get_new_results ~blocking =
  fetch_new_results ~blocking;
484
  let q = ref [] in
485 486 487 488
  Hashtbl.iter (fun key element ->
    if element = ProverStarted && blocking then
      ()
    else
489
      q := (ServerCall key, element) :: !q) result_buffer;
490
  Hashtbl.clear result_buffer;
491
  !q
492

Andrei Paskevich's avatar
Andrei Paskevich committed
493 494 495 496 497 498
let query_result_buffer id =
  try let r = Hashtbl.find result_buffer id in
      Hashtbl.remove result_buffer id; r
  with Not_found -> NoUpdates

let editor_result ret = {
499
  pr_answer = Unknown "not yet edited";
Andrei Paskevich's avatar
Andrei Paskevich committed
500 501 502 503 504 505 506
  pr_status = ret;
  pr_output = "";
  pr_time   = 0.0;
  pr_steps  = 0;
  pr_model  = Model_parser.default_model;
}

507 508
let query_call = function
  | ServerCall id ->
509
      fetch_new_results ~blocking:false;
Andrei Paskevich's avatar
Andrei Paskevich committed
510 511
      query_result_buffer id
  | EditorCall pid ->
512
      let pid, ret = Unix.waitpid [Unix.WNOHANG] pid in
Andrei Paskevich's avatar
Andrei Paskevich committed
513 514
      if pid = 0 then NoUpdates else
      ProverFinished (editor_result ret)
515

516 517
let rec wait_on_call = function
  | ServerCall id as pc ->
Andrei Paskevich's avatar
Andrei Paskevich committed
518 519
      begin match query_result_buffer id with
        | ProverFinished r -> r
520
        | _ ->
521
            fetch_new_results ~blocking:true;
Andrei Paskevich's avatar
Andrei Paskevich committed
522
            wait_on_call pc
523
      end
Andrei Paskevich's avatar
Andrei Paskevich committed
524 525 526
  | EditorCall pid ->
      let _, ret = Unix.waitpid [] pid in
      editor_result ret
527 528

let call_on_buffer ~command ~limit ~res_parser ~filename ~printer_mapping
529
                   ~gen_new_file ?(inplace=false) buffer =
530
  let fin,cin =
531 532 533 534 535 536 537 538 539 540
    if gen_new_file then
      Filename.open_temp_file "why_" ("_" ^ filename)
    else
      begin
        let filename = Sysutil.absolutize_filename (Sys.getcwd ()) filename in
        if inplace then
          Sys.rename filename (backup_file filename);
        filename, open_out filename
      end
  in
541
  Buffer.output_buffer cin buffer; close_out cin;
542 543 544 545 546 547 548
  call_on_file ~command ~limit ~res_parser ~printer_mapping ~inplace fin

let call_editor ~command fin =
  let command, use_stdin, _ =
    actualcommand ~cleanup:false ~inplace:false command empty_limit fin in
  let exec = List.hd command in
  let argarray = Array.of_list command in
Andrei Paskevich's avatar
Andrei Paskevich committed
549 550 551 552 553
  let fd_in =
    if use_stdin then Unix.openfile fin [Unix.O_RDONLY] 0 else Unix.stdin in
  let pid = Unix.create_process exec argarray fd_in Unix.stdout Unix.stderr in
  if use_stdin then Unix.close fd_in;
  EditorCall pid