call_provers.ml 7.04 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    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 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 76
  | Unknown of string
  | Failure of string
77 78
  | HighFailure

79 80 81 82 83 84
type prover_result = {
  pr_answer : prover_answer;
  pr_output : string;
  pr_time   : float;
}

85 86 87
let print_prover_answer fmt = function
  | Valid -> fprintf fmt "Valid"
  | Invalid -> fprintf fmt "Invalid"
88
  | Timeout -> fprintf fmt "Timeout"
89 90
  | Unknown s -> fprintf fmt "Unknown: %s" s
  | Failure s -> fprintf fmt "Failure: %s" s
91 92
  | HighFailure -> fprintf fmt "HighFailure"

93 94 95
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
96

97
let rec grep out l = match l with
98
  | [] ->
99 100
      HighFailure
  | (re,pa) :: l ->
101 102 103
      begin try
        ignore (Str.search_forward re out 0);
        match pa with
104 105 106 107
        | Valid | Invalid | Timeout -> pa
        | Unknown s -> Unknown (Str.replace_matched s out)
        | Failure s -> Failure (Str.replace_matched s out)
        | HighFailure -> assert false
108
      with Not_found -> grep out l end
109

110 111 112

let debug = Debug.register_flag "call_prover"

113
type post_prover_call = unit -> prover_result
Andrei Paskevich's avatar
Andrei Paskevich committed
114 115
type prover_call = Unix.wait_flag list -> post_prover_call
type pre_prover_call = unit -> prover_call
116

117 118 119
let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
                 ~regexps ~timeregexps ~exitcodes
                 ?(cleanup=false) fin =
Andrei Paskevich's avatar
Andrei Paskevich committed
120 121 122

  let arglist = Cmdline.cmdline_split command in
  let command = List.hd arglist in
123
  let on_timelimit = ref false in
124
  let on_filename = ref false in
125
  let cmd_regexp = Str.regexp "%\\(.\\)" in
126
  let replace s = match Str.matched_group 1 s with
127
    | "%" -> "%"
128
    | "f" -> on_filename := true; fin
129
    | "t" -> on_timelimit := true; string_of_int timelimit
130
    | "m" -> string_of_int memlimit
131
    | "b" -> string_of_int (memlimit * 1024)
132
    | "l" -> Config.libdir
133
    | _ -> failwith "unknown format specifier, use %%f, %%t, %%m or %%b"
134
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
135
  let subst s =
136 137
    try Str.global_substitute cmd_regexp replace s
    with e -> if cleanup then Sys.remove fin; raise e
138
  in
139 140 141
  let arglist = List.map subst arglist in
  let argarray = Array.of_list
    (if !on_filename then arglist else arglist @ [fin]) in
Andrei Paskevich's avatar
Andrei Paskevich committed
142

143
  fun () ->
Andrei Paskevich's avatar
Andrei Paskevich committed
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160
    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;

    fun wait_flags ->
      (* TODO? check that we haven't given the result earlier *)
      let res,ret = Unix.waitpid wait_flags pid in
      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
161 162
      fun () ->
        if Debug.nottest_flag debug then begin
163 164
          if cleanup then Sys.remove fin;
          Sys.remove fout
Andrei Paskevich's avatar
Andrei Paskevich committed
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186
        end;
        let ans = match ret with
          | Unix.WSTOPPED n ->
              Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
              HighFailure
          | Unix.WSIGNALED n ->
              Debug.dprintf debug "Call_provers: killed by signal %d@." n;
              HighFailure
          | 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;
        let time = Util.default_option time (grep_time out timeregexps) in
        let ans = match ans with
          | HighFailure when !on_timelimit && timelimit > 0
            && time >= (0.9 *. float timelimit) -> Timeout
          | _ -> ans
        in
        { pr_answer = ans;
          pr_output = out;
          pr_time   = time }
187

188 189 190 191 192 193 194 195
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
                   ~regexps ~timeregexps ~exitcodes ~filename buffer =

  let fin,cin = Filename.open_temp_file "why_" ("_" ^ filename) in
  Buffer.output_buffer cin buffer; close_out cin;
  call_on_file ~command ~timelimit ~memlimit
               ~regexps ~timeregexps ~exitcodes ~cleanup:true fin

Andrei Paskevich's avatar
Andrei Paskevich committed
196 197 198 199
let query_call call = try Some (call [Unix.WNOHANG]) with Exit -> None

let wait_on_call call = call []