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

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

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


145 146 147 148 149 150 151 152

(* 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
153 154
let () = Sys.set_signal Sys.sigpipe Sys.Signal_ignore

155
let timed_sys_command ?formatter ?buffer ?(debug=false) ?timeout cmd =
156 157
  let t0 = Unix.times () in
  let cmd = match timeout with
158 159 160
    | 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;
161
  let (cin,cout) as p = Unix.open_process cmd in
162
  (* Write the formatter to the stdin of the prover *)
Francois Bobot's avatar
Francois Bobot committed
163 164 165
  begin try
    (match formatter with
       | None -> ()
166
       | Some formatter ->
Francois Bobot's avatar
Francois Bobot committed
167 168
           let fmt = formatter_of_out_channel cout in
           formatter fmt);
169
  with Sys_error s ->
170
    if debug then eprintf "Sys_error : %s@." s
Francois Bobot's avatar
Francois Bobot committed
171
  end;
172 173 174 175
  (* Write the buffer to the stdin of the prover *)
  begin try
    (match buffer with
       | None -> ()
176
       | Some buffer ->
177
           Buffer.output_buffer cout buffer);
178
  with Sys_error s ->
179
    if debug then eprintf "Sys_error : %s@." s
180 181
  end;
  close_out cout;
182 183 184 185
  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
186
  if debug then eprintf "Call_provers : Command output : %s@." out;
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 214
  (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  *)
215
  (*         "Calldp.gen_prover_call : filename must be given if the prover
216
             can't use stdin."  *)
217 218 219
  (* in *)


220 221
let treat_result pr (t,c,outerr) =
  let answer =
222
    match c with
223 224 225
      | Unix.WSTOPPED 24 | Unix.WSIGNALED 24 | Unix.WEXITED 124
      | Unix.WEXITED 152 ->
          (* (*128 +*) SIGXCPU signal (i.e. 24, /usr/include/bits/signum.h) *)
226 227 228 229 230 231
          (* 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 *)
232 233
          Timeout
      | Unix.WSTOPPED _ | Unix.WSIGNALED _ -> HighFailure
234
      | Unix.WEXITED _ ->
235 236 237
          let rec greps res = function
            | [] -> HighFailure
            | (r,pa)::l ->
238
                if grep r res
239 240 241 242 243 244
                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
245 246 247 248 249 250 251 252
          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...*)
  (* *)


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

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

259
let rec on_file ?debug ?timeout pr filename =
260 261
  check_prover pr;
  match pr.pr_call_file with
262 263 264 265
    | Some cmd ->
        let filename = if is_true_cygwin
        then
          let cin = Unix.open_process_in
266 267 268 269
            (sprintf "cygpath -am \"%s\"" filename) in
          let f = input_line cin in
          close_in cin; f
        else filename in
270 271
        let cmd =
          let repl_fun s =
272
            match Str.matched_group 1 s with
Francois Bobot's avatar
Francois Bobot committed
273
              | "s" -> filename
274 275 276 277
              | _ -> 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
278
    | None ->
279 280
        let formatter = Sysutil.file_contents_fmt filename in
        on_formatter ?timeout ?debug pr formatter
281

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


let on_buffer ?debug ?timeout ?filename pr buffer =
  check_prover pr;
  match pr.pr_call_stdin with
302
    | Some cmd ->
303 304
        let res = timed_sys_command ?debug ?timeout ~buffer cmd in
        treat_result pr res
305
    | None ->
306 307 308 309 310 311
        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)
312
*)