call_provers.ml 11.6 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 45 46
  | Unknown s -> pp_print_string fmt s
  | Failure s -> pp_print_string fmt s
  | 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 50
  if pr.pr_answer == HighFailure then
    fprintf fmt "@\n@stdout-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 75 76 77 78 79 80 81 82 83 84 85 86
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 ->
        if debug then Format.eprintf "Call_provers: stopped on signal %d" n;
        HighFailure
    | Unix.WSIGNALED n ->
        if debug then Format.eprintf "Call_provers: killed by signal %d" n;
        HighFailure
    | Unix.WEXITED n ->
        if debug then Format.eprintf "Call_provers: exited with status %d" n;
        grep out regexps
  in
  { pr_answer = ans;
    pr_output = out;
    pr_time   = t1 -. t0 }
87

88 89 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
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

(*
126
let is_true_cygwin = Sys.os_type = "Cygwin"
127

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


151 152 153 154 155 156 157 158

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

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


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


259
let check_prover prover =
260 261 262
  if prover.pr_call_file = None && prover.pr_call_stdin = None then
    raise NoCommandlineProvided

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

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

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


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