call_provers.ml 6.35 KB
Newer Older
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
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 113

let debug = Debug.register_flag "call_prover"

let call_prover command opt_cout buffer =
114
  let time = Unix.gettimeofday () in
115 116 117 118 119 120 121 122 123
  let (cin,_) as p = match opt_cout with
    | Some cout ->
        Buffer.output_buffer cout buffer; close_out cout;
        Unix.open_process command
    | None ->
        let (_,cout) as p = Unix.open_process command in
        Buffer.output_buffer cout buffer; close_out cout;
        p
  in
124 125
  let out = channel_contents cin in
  let ret = Unix.close_process p in
126
  let time = Unix.gettimeofday () -. time in
127
  Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
128 129
  ret, out, time

130 131 132 133
type post_prover_call = unit -> prover_result

type bare_prover_call = unit -> post_prover_call

134
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
135
                   ~regexps ~timeregexps ~exitcodes ~filename buffer =
136
  let on_stdin = ref true in
137
  let on_timelimit = ref false in
138 139 140 141
  let cmd_regexp = Str.regexp "%\\(.\\)" in
  let replace file s = match Str.matched_group 1 s with
    | "%" -> "%"
    | "f" -> on_stdin := false; file
142
    | "t" -> on_timelimit := true; string_of_int timelimit
143
    | "m" -> string_of_int memlimit
144 145
    | "b" -> string_of_int (memlimit * 1024)
    | _ -> failwith "unknown format specifier, use %%f, %%t, %%m or %%b"
146 147
  in
  let cmd = Str.global_substitute cmd_regexp (replace "") command in
148 149 150 151 152 153 154 155
  let on_stdin = !on_stdin in
  let cmd,fout,cout = if on_stdin then cmd, "", None else
    let fout,cout = Filename.open_temp_file "why_" ("_" ^ filename) in
    let cmd =
      try Str.global_substitute cmd_regexp (replace fout) command
      with e -> close_out cout; Sys.remove fout; raise e
    in
    cmd, fout, Some cout
156
  in
157
  fun () ->
158
    let ret,out,time = call_prover cmd cout buffer in
159
    fun () ->
160 161 162 163 164 165 166 167 168 169 170 171
      if not on_stdin && Debug.nottest_flag debug then Sys.remove fout;
      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
172
      let time = Util.default_option time (grep_time out timeregexps) in
173 174
      let ans = match ans with
        | HighFailure when !on_timelimit && timelimit > 0
175
          && time >= (0.9 *. float timelimit) -> Timeout
176 177 178 179 180
        | _ -> ans
      in
      { pr_answer = ans;
        pr_output = out;
        pr_time   = time }
181