call_provers.ml 6.34 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 30 31 32 33 34 35 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
(** time regexp "%h:%m:%s" *)
type timeunit =
  | Hour
  | Min
  | Sec
  | Msec

type regexptime = {
  re : Str.regexp;
  group : timeunit array; (*ieme corresponds to the group i + 1*)
}

let regexptime s =
  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 ~regexpstime ~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 regexpstime) 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