call_provers.ml 4.61 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Format
21
open Sysutil
22

23
type prover_answer =
24 25 26
  | Valid
  | Invalid
  | Timeout
27 28
  | Unknown of string
  | Failure of string
29 30
  | HighFailure

31 32 33 34 35 36
type prover_result = {
  pr_answer : prover_answer;
  pr_output : string;
  pr_time   : float;
}

37 38 39
let print_prover_answer fmt = function
  | Valid -> fprintf fmt "Valid"
  | Invalid -> fprintf fmt "Invalid"
40
  | Timeout -> fprintf fmt "Timeout"
41 42
  | Unknown s -> fprintf fmt "Unknown: %s" s
  | Failure s -> fprintf fmt "Failure: %s" s
43 44
  | HighFailure -> fprintf fmt "HighFailure"

45 46 47
let print_prover_result fmt {pr_answer=ans; pr_output=out; pr_time=t} =
  fprintf fmt "%a (%.2fs)" print_prover_answer ans t;
  if ans == HighFailure then fprintf fmt "@\nProver output:@\n%s@." out
48

49
let rec grep out l = match l with
50 51 52
  | [] -> 
      HighFailure
  | (re,pa) :: l ->
53 54 55
      begin try
        ignore (Str.search_forward re out 0);
        match pa with
56 57 58 59
        | Valid | Invalid | Timeout -> pa
        | Unknown s -> Unknown (Str.replace_matched s out)
        | Failure s -> Failure (Str.replace_matched s out)
        | HighFailure -> assert false
60
      with Not_found -> grep out l end
61

62
let call_prover debug command opt_cout buffer =
63
  let time = Unix.gettimeofday () in
64
  let (cin,cout) as p = Unix.open_process command in
65
  let cout = match opt_cout with Some c -> close_out cout; c | _ -> cout in
66 67 68
  Buffer.output_buffer cout buffer; close_out cout;
  let out = channel_contents cin in
  let ret = Unix.close_process p in
69
  let time = Unix.gettimeofday () -. time in
70 71 72
  if debug then eprintf "Call_provers: prover output:@\n%s@." out;
  ret, out, time

73
let call_on_buffer ?(debug=false) ~command ?(timelimit=0) ?(memlimit=0)
74
                                  ~regexps ~exitcodes ~filename buffer () =
75
  let on_stdin = ref true in
76
  let on_timelimit = ref false in
77 78 79 80
  let cmd_regexp = Str.regexp "%\\(.\\)" in
  let replace file s = match Str.matched_group 1 s with
    | "%" -> "%"
    | "f" -> on_stdin := false; file
81
    | "t" -> on_timelimit := true; string_of_int timelimit
82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
    | "m" -> string_of_int memlimit
    | _ -> failwith "unknown format specifier, use %%f, %%t or %%m"
  in
  let cmd = Str.global_substitute cmd_regexp (replace "") command in
  let ret, out, time =
    if !on_stdin then call_prover debug cmd None buffer else begin
      let fout,cout = Filename.open_temp_file "why_" ("_" ^ filename) in
      try
        let cmd = Str.global_substitute cmd_regexp (replace fout) command in
        let res = call_prover debug cmd (Some cout) buffer in
        if not debug then Sys.remove fout;
        res
      with e ->
        close_out cout;
        if not debug then Sys.remove fout;
        raise e
    end
  in
100 101
  let ans = match ret with
    | Unix.WSTOPPED n ->
102
        if debug then eprintf "Call_provers: stopped by signal %d@." n;
103 104
        HighFailure
    | Unix.WSIGNALED n ->
105
        if debug then eprintf "Call_provers: killed by signal %d@." n;
106 107
        HighFailure
    | Unix.WEXITED n ->
108 109 110 111
        if debug then eprintf "Call_provers: exited with status %d@." n;
        (try List.assoc n exitcodes with Not_found -> grep out regexps)
  in
  let ans = match ans with
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
112
    | HighFailure when !on_timelimit && timelimit > 0
113
      && time >= (0.9 *. float timelimit) -> Timeout
114
    | _ -> ans
115 116 117
  in
  { pr_answer = ans;
    pr_output = out;
118
    pr_time   = time }
119