call_provers.ml 11.8 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 37 38
type prover_result = {
  pr_answer : prover_answer;
  pr_output : string;
  pr_time   : float;
}

type prover_regexp = Str.regexp * prover_answer

39 40 41
let print_prover_answer fmt = function
  | Valid -> fprintf fmt "Valid"
  | Invalid -> fprintf fmt "Invalid"
42
  | Timeout -> fprintf fmt "Timeout"
43 44
  | Unknown s -> fprintf fmt "Unknown: %s" s
  | Failure s -> fprintf fmt "Failure: %s" s
45 46
  | HighFailure -> fprintf fmt "HighFailure"

47
let print_prover_result fmt pr =
48
  fprintf fmt "%a (%.2fs)" print_prover_answer pr.pr_answer pr.pr_time;
49
  if pr.pr_answer == HighFailure then
50
    fprintf fmt "@\nstdout-stderr:@\n%s@." pr.pr_output
51

52 53 54 55 56 57 58 59 60 61 62
let rec grep out l = match l with
  | [] -> HighFailure
  | (re,pa)::l ->
      begin try
        ignore (Str.search_forward re out 0);
        match pa with
          | Valid | Invalid | Timeout -> pa
          | Unknown s -> Unknown (Str.replace_matched s out)
          | Failure s -> Failure (Str.replace_matched s out)
          | HighFailure -> assert false
      with Not_found -> grep out l end
63

64 65 66 67 68 69 70 71 72 73 74
let call_prover debug command regexps opt_cout buffer =
  let t0 = Unix.time () in
  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
  let t1 = Unix.time () in
  if debug then Format.eprintf "Call_provers: Command output:@\n%s@." out;
  let ans = match ret with
    | Unix.WSTOPPED n ->
75
        if debug then Format.eprintf "Call_provers: stopped on signal %d@." n;
76
        HighFailure
77 78 79
    | Unix.WSIGNALED 24 (* SIGXCPU signal cf. /usr/include/bits/signum.h *) ->
        if debug then Format.eprintf "Call_provers: killed by signal SIGXCPU@.";
        Timeout
80
    | Unix.WSIGNALED n ->
81
        if debug then Format.eprintf "Call_provers: killed by signal %d@." n;
82 83
        HighFailure
    | Unix.WEXITED n ->
84
        if debug then Format.eprintf "Call_provers: exited with status %d@." n;
85 86 87 88 89
        grep out regexps
  in
  { pr_answer = ans;
    pr_output = out;
    pr_time   = t1 -. t0 }
90

91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
let call_on_buffer ?(debug=false) ?(suffix=".dump")
      ~command ~timelimit ~memlimit ~regexps buffer () =
  let on_stdin = ref false in
  let cmd_regexp = Str.regexp "%\\(.\\)" in
  let replace filename s = match Str.matched_group 1 s with
    | "%" -> "%"
    | "f" -> on_stdin := false; filename
    | "t" -> string_of_int timelimit
    | "m" -> string_of_int memlimit
    | _ -> failwith "unknown format specifier, use %%f, %%t or %%m"
  in
  let cmd_stdin = Str.global_substitute cmd_regexp (replace "") command in
  if !on_stdin then call_prover debug cmd_stdin regexps None buffer
  else
    let fout,cout = Filename.open_temp_file "why" suffix in
    try
      let cmd = Str.global_substitute cmd_regexp (replace fout) command in
      let res = call_prover debug cmd regexps (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

let call_on_formatter ?debug ?suffix
      ~command ~timelimit ~memlimit ~regexps formatter =
  let buffer = Buffer.create 1024 in
  let fmt = formatter_of_buffer buffer in
  formatter fmt; pp_print_flush fmt ();
  call_on_buffer ?debug ?suffix ~command ~timelimit ~memlimit ~regexps buffer

let call_on_file ?debug ?suffix
      ~command ~timelimit ~memlimit ~regexps filename =
  let buffer = file_contents_buf filename in
  call_on_buffer ?debug ?suffix ~command ~timelimit ~memlimit ~regexps buffer

(*
129
let is_true_cygwin = Sys.os_type = "Cygwin"
130

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


154 155 156 157 158 159 160 161

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

164
let timed_sys_command ?formatter ?buffer ?(debug=false) ?timeout cmd =
165 166 167
  let t0 = Unix.times () in
  let cmd = match timeout with
    | None -> Format.sprintf "%s 2>&1" cmd
168
    | Some timeout -> Format.sprintf "%s %d %s 2>&1" !cpulimit timeout cmd in
Francois Bobot's avatar
Francois Bobot committed
169
  if debug then Format.eprintf "command line: %s@." cmd;
170
  let (cin,cout) as p = Unix.open_process cmd in
171
  (* Write the formatter to the stdin of the prover *)
Francois Bobot's avatar
Francois Bobot committed
172 173 174
  begin try
    (match formatter with
       | None -> ()
175
       | Some formatter ->
Francois Bobot's avatar
Francois Bobot committed
176 177
           let fmt = formatter_of_out_channel cout in
           formatter fmt);
178
  with Sys_error s ->
Francois Bobot's avatar
Francois Bobot committed
179 180
    if debug then Format.eprintf "Sys_error : %s@." s
  end;
181 182 183 184
  (* Write the buffer to the stdin of the prover *)
  begin try
    (match buffer with
       | None -> ()
185
       | Some buffer ->
186
           Buffer.output_buffer cout buffer);
187
  with Sys_error s ->
188 189 190
    if debug then Format.eprintf "Sys_error : %s@." s
  end;
  close_out cout;
191 192 193 194
  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
195
  if debug then Format.eprintf "Call_provers : Command output : %s@." out;
196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223
  (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  *)
224
  (*         "Calldp.gen_prover_call : filename must be given if the prover
225
             can't use stdin."  *)
226 227 228
  (* in *)


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


262
let check_prover prover =
263 264 265
  if prover.pr_call_file = None && prover.pr_call_stdin = None then
    raise NoCommandlineProvided

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

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

291
and on_formatter ?debug ?timeout ?filename pr formatter =
292
  check_prover pr;
Francois Bobot's avatar
Francois Bobot committed
293
  match pr.pr_call_stdin with
294
    | Some cmd ->
295
        let res = timed_sys_command ?debug ?timeout ~formatter cmd in
296
        treat_result pr res
297
    | None ->
298 299
        match filename with
          | None -> raise NoCommandlineProvided
Francois Bobot's avatar
Francois Bobot committed
300
          | Some filename -> Sysutil.open_temp_file ?debug filename
301
              (fun file cout ->
302 303 304
                 let fmt = formatter_of_out_channel cout in
                 formatter fmt;
                 pp_print_flush fmt ();
305
                 on_file ?timeout ?debug pr file)
306 307 308 309 310


let on_buffer ?debug ?timeout ?filename pr buffer =
  check_prover pr;
  match pr.pr_call_stdin with
311
    | Some cmd ->
312 313
        let res = timed_sys_command ?debug ?timeout ~buffer cmd in
        treat_result pr res
314
    | None ->
315 316 317 318 319 320
        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)
321
*)