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

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

let call_on_buffer ?(debug=false) ~command ~timelimit ~memlimit
                                  ~regexps ~exitcodes ~filename buffer () =
74
  let on_stdin = ref true in
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
  let cmd_regexp = Str.regexp "%\\(.\\)" in
  let replace file s = match Str.matched_group 1 s with
    | "%" -> "%"
    | "f" -> on_stdin := false; file
    | "t" -> string_of_int timelimit
    | "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
98 99
  let ans = match ret with
    | Unix.WSTOPPED n ->
100
        if debug then eprintf "Call_provers: stopped by signal %d@." n;
101 102
        HighFailure
    | Unix.WSIGNALED n ->
103
        if debug then eprintf "Call_provers: killed by signal %d@." n;
104 105
        HighFailure
    | Unix.WEXITED n ->
106 107 108 109
        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
110
    | HighFailure
111
      when timelimit > 0 && time >= (0.9 *. float timelimit) -> Timeout
112
    | _ -> ans
113 114 115
  in
  { pr_answer = ans;
    pr_output = out;
116
    pr_time   = time }
117

118
(*
119
let is_true_cygwin = Sys.os_type = "Cygwin"
120

MARCHE Claude's avatar
MARCHE Claude committed
121
(* this should be replaced by a proper use of fork/waitpid() *)
Francois Bobot's avatar
Francois Bobot committed
122 123
let dirname = Filename.dirname Sys.argv.(0)
let cpulimit_local = Filename.concat dirname "why-cpulimit"
124 125
let cpulimit_commands = ["why-cpulimit"; cpulimit_local ; "timeout"]
let cpulimit = (
MARCHE Claude's avatar
MARCHE Claude committed
126 127 128 129
  let tmp = ref "" in
  try
    List.iter
      (fun s ->
130 131
         (*let r = Sys.command (s^" 1 echo") in
         if r=0 then (tmp:=s; raise Exit)*)
132
         let pid = Unix.create_process s [|s;"1";"true"|]
133 134 135 136 137
           Unix.stdin Unix.stdout Unix.stderr in
         match Unix.waitpid [] pid with
           | _,Unix.WEXITED 0 -> (tmp:=s; raise Exit)
           | _ -> ()
      )
MARCHE Claude's avatar
MARCHE Claude committed
138
    cpulimit_commands;
139 140 141
    failwith ("need shell command among: "^
                (String.concat " ," cpulimit_commands))
  with Exit -> tmp)
142 143


144 145 146 147 148 149 150 151

(* Utils *)

let remove_file ?(debug=false) f =
  if not debug then try Sys.remove f with _ -> ()

(*let environment = Unix.environment ()*)

Francois Bobot's avatar
Francois Bobot committed
152 153
let () = Sys.set_signal Sys.sigpipe Sys.Signal_ignore

154
let timed_sys_command ?formatter ?buffer ?(debug=false) ?timeout cmd =
155 156
  let t0 = Unix.times () in
  let cmd = match timeout with
157 158 159
    | None -> sprintf "%s 2>&1" cmd
    | Some timeout -> sprintf "%s %d %s 2>&1" !cpulimit timeout cmd in
  if debug then eprintf "command line: %s@." cmd;
160
  let (cin,cout) as p = Unix.open_process cmd in
161
  (* Write the formatter to the stdin of the prover *)
Francois Bobot's avatar
Francois Bobot committed
162 163 164
  begin try
    (match formatter with
       | None -> ()
165
       | Some formatter ->
Francois Bobot's avatar
Francois Bobot committed
166 167
           let fmt = formatter_of_out_channel cout in
           formatter fmt);
168
  with Sys_error s ->
169
    if debug then eprintf "Sys_error : %s@." s
Francois Bobot's avatar
Francois Bobot committed
170
  end;
171 172 173 174
  (* Write the buffer to the stdin of the prover *)
  begin try
    (match buffer with
       | None -> ()
175
       | Some buffer ->
176
           Buffer.output_buffer cout buffer);
177
  with Sys_error s ->
178
    if debug then eprintf "Sys_error : %s@." s
179 180
  end;
  close_out cout;
181 182 183 184
  let out = Sysutil.channel_contents cin in
  let ret = Unix.close_process p in
  let t1 = Unix.times () in
  let cpu_time = t1.Unix.tms_cutime -. t0.Unix.tms_cutime in
185
  if debug then eprintf "Call_provers : Command output : %s@." out;
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213
  (cpu_time,ret,out)

let grep re str =
  try
    let _ = Str.search_forward re str 0 in true
  with Not_found -> false

  (*   match buffers,p.DpConfig.stdin_switch,filename with *)
  (*     | None,_, Some f -> *)
  (*         let cmd = sprintf "%s %s %s %s"  *)
  (*           p.DpConfig.command p.DpConfig.command_switches switch f  *)
  (*         in *)
  (*         cmd,timed_sys_command ~debug timeout cmd *)
  (*     | Some buffers, Some stdin_s, _ -> *)
  (*         let cmd = sprintf "%s %s %s %s"  *)
  (*           p.DpConfig.command p.DpConfig.command_switches switch stdin_s *)
  (*         in *)
  (*         cmd,timed_sys_command ~stdin:buffers ~debug timeout cmd *)
  (*     | Some buffers, None, Some f -> *)
  (*         let f = Filename.temp_file "" f in *)
  (*         let cout = open_out f in *)
  (*         List.iter (Buffer.output_buffer cout) buffers; *)
  (*         close_out cout; *)
  (*         let cmd = sprintf "%s %s %s %s"  *)
  (*           p.DpConfig.command p.DpConfig.command_switches switch f *)
  (*         in *)
  (*         cmd,timed_sys_command ~debug timeout cmd *)
  (*     | _ -> invalid_arg  *)
214
  (*         "Calldp.gen_prover_call : filename must be given if the prover
215
             can't use stdin."  *)
216 217 218
  (* in *)


219 220
let treat_result pr (t,c,outerr) =
  let answer =
221
    match c with
222 223 224
      | Unix.WSTOPPED 24 | Unix.WSIGNALED 24 | Unix.WEXITED 124
      | Unix.WEXITED 152 ->
          (* (*128 +*) SIGXCPU signal (i.e. 24, /usr/include/bits/signum.h) *)
225 226 227 228 229 230
          (* TODO : if somebody use why_cpulimit to call "why -timeout
             0", Why will think that he called why_cpulimit (WEXITED
             152) and will return Timeout instead of exit 152. In fact
             in this case Why will receive a SIGXCPU in less than 1
             sec (soft limit) (ie man setrlimit ). The problem can be
             here or in the use of why_cpulimit *)
231 232
          Timeout
      | Unix.WSTOPPED _ | Unix.WSIGNALED _ -> HighFailure
233
      | Unix.WEXITED _ ->
234 235 236
          let rec greps res = function
            | [] -> HighFailure
            | (r,pa)::l ->
237
                if grep r res
238 239 240 241 242 243
                then match pa with
                  | Valid | Invalid -> pa
                  | Unknown s -> Unknown (Str.replace_matched s res)
                  | Failure s -> Failure (Str.replace_matched s res)
                  | Timeout | HighFailure -> assert false
                else greps outerr l in
244 245 246 247 248 249 250 251
          greps outerr pr.pr_regexps in
  { pr_time = t;
    pr_answer = answer;
    pr_stderr = ""; (*Fill it with something real*)
    pr_stdout = outerr} (* Split it in two...*)
  (* *)


252
let check_prover prover =
253 254 255
  if prover.pr_call_file = None && prover.pr_call_stdin = None then
    raise NoCommandlineProvided

Francois Bobot's avatar
Francois Bobot committed
256
let regexp_call_file = Str.regexp "%\\([a-z]\\)"
257

258
let rec on_file ?debug ?timeout pr filename =
259 260
  check_prover pr;
  match pr.pr_call_file with
261 262 263 264
    | Some cmd ->
        let filename = if is_true_cygwin
        then
          let cin = Unix.open_process_in
265 266 267 268
            (sprintf "cygpath -am \"%s\"" filename) in
          let f = input_line cin in
          close_in cin; f
        else filename in
269 270
        let cmd =
          let repl_fun s =
271
            match Str.matched_group 1 s with
Francois Bobot's avatar
Francois Bobot committed
272
              | "s" -> filename
273 274 275 276
              | _ -> assert false in (*TODO mettre une belle exception*)
          Str.global_substitute regexp_call_file repl_fun cmd in
        let res = timed_sys_command ?debug ?timeout cmd in
        treat_result pr res
277
    | None ->
278 279
        let formatter = Sysutil.file_contents_fmt filename in
        on_formatter ?timeout ?debug pr formatter
280

281
and on_formatter ?debug ?timeout ?filename pr formatter =
282
  check_prover pr;
Francois Bobot's avatar
Francois Bobot committed
283
  match pr.pr_call_stdin with
284
    | Some cmd ->
285
        let res = timed_sys_command ?debug ?timeout ~formatter cmd in
286
        treat_result pr res
287
    | None ->
288 289
        match filename with
          | None -> raise NoCommandlineProvided
Francois Bobot's avatar
Francois Bobot committed
290
          | Some filename -> Sysutil.open_temp_file ?debug filename
291
              (fun file cout ->
292 293 294
                 let fmt = formatter_of_out_channel cout in
                 formatter fmt;
                 pp_print_flush fmt ();
295
                 on_file ?timeout ?debug pr file)
296 297 298 299 300


let on_buffer ?debug ?timeout ?filename pr buffer =
  check_prover pr;
  match pr.pr_call_stdin with
301
    | Some cmd ->
302 303
        let res = timed_sys_command ?debug ?timeout ~buffer cmd in
        treat_result pr res
304
    | None ->
305 306 307 308 309 310
        match filename with
          | None -> raise NoCommandlineProvided
          | Some filename -> Sysutil.open_temp_file ?debug filename
              (fun file cout ->
                 Buffer.output_buffer cout buffer;
                 on_file ?timeout ?debug pr file)
311
*)