call_provers.ml 9.18 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 21
open Format

22 23 24 25 26 27 28 29
type prover_answer = 
  | Valid
  | Invalid
  | Unknown of string  
  | Failure of string      
  | Timeout
  | HighFailure

30 31 32 33 34 35 36 37
let print_prover_answer fmt = function
  | Valid -> fprintf fmt "Valid"
  | Invalid -> fprintf fmt "Invalid"
  | Unknown s -> pp_print_string fmt s
  | Failure s -> pp_print_string fmt s
  | Timeout -> fprintf fmt "Timeout"
  | HighFailure -> fprintf fmt "HighFailure"

38 39 40 41 42 43
type prover_result =
    { pr_time   : float;
      pr_answer : prover_answer;
      pr_stderr : string;
      pr_stdout : string}

44
let print_prover_result fmt pr = 
45 46 47
  fprintf fmt "%a (%.2fs)" print_prover_answer pr.pr_answer pr.pr_time;
  if pr.pr_answer == HighFailure 
  then fprintf fmt "@\nstdout-stderr : \"%s\"" pr.pr_stdout;
48

49 50 51
type prover =
    { pr_call_stdin : string option; (* %f pour le nom du fichier *)
      pr_call_file  : string option;
52 53
      pr_regexps    : (Str.regexp * prover_answer) list; 
      (* \1,... sont remplacés *)
54 55 56 57 58 59
    }
      

exception CommandError
exception NoCommandlineProvided      

60
let is_true_cygwin = Sys.os_type = "Cygwin"
61

MARCHE Claude's avatar
MARCHE Claude committed
62
(* this should be replaced by a proper use of fork/waitpid() *)
Francois Bobot's avatar
Francois Bobot committed
63 64
let dirname = Filename.dirname Sys.argv.(0)
let cpulimit_local = Filename.concat dirname "why-cpulimit"
65 66
let cpulimit_commands = ["why-cpulimit"; cpulimit_local ; "timeout"]
let cpulimit = (
MARCHE Claude's avatar
MARCHE Claude committed
67 68 69 70
  let tmp = ref "" in
  try
    List.iter
      (fun s ->
71 72 73 74 75 76 77 78
         (*let r = Sys.command (s^" 1 echo") in
         if r=0 then (tmp:=s; raise Exit)*)
         let pid = Unix.create_process s [|s;"1";"true"|] 
           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
79
    cpulimit_commands;
80 81 82
    failwith ("need shell command among: "^
                (String.concat " ," cpulimit_commands))
  with Exit -> tmp)
MARCHE Claude's avatar
MARCHE Claude committed
83 84
     
    
85 86 87 88 89 90 91 92

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

95
let timed_sys_command ?formatter ?buffer ?(debug=false) ?timeout cmd =
96 97 98
  let t0 = Unix.times () in
  let cmd = match timeout with
    | None -> Format.sprintf "%s 2>&1" cmd
99
    | Some timeout -> Format.sprintf "%s %d %s 2>&1" !cpulimit timeout cmd in
Francois Bobot's avatar
Francois Bobot committed
100
  if debug then Format.eprintf "command line: %s@." cmd;
101
  let (cin,cout) as p = Unix.open_process cmd in
102
  (* Write the formatter to the stdin of the prover *)
Francois Bobot's avatar
Francois Bobot committed
103 104 105 106 107 108 109 110 111
  begin try
    (match formatter with
       | None -> ()
       | Some formatter -> 
           let fmt = formatter_of_out_channel cout in
           formatter fmt);
  with Sys_error s -> 
    if debug then Format.eprintf "Sys_error : %s@." s
  end;
112 113 114 115 116 117 118 119 120 121
  (* Write the buffer to the stdin of the prover *)
  begin try
    (match buffer with
       | None -> ()
       | Some buffer -> 
           Buffer.output_buffer cout buffer);
  with Sys_error s -> 
    if debug then Format.eprintf "Sys_error : %s@." s
  end;
  close_out cout;
122 123 124 125
  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
126
  if debug then Format.eprintf "Call_provers : Command output : %s@." out;
127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
  (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  *)
155 156
  (*         "Calldp.gen_prover_call : filename must be given if the prover 
             can't use stdin."  *)
157 158 159 160 161 162 163 164 165
  (* in *)


let treat_result pr (t,c,outerr) = 
  let answer = 
    match c with
      | Unix.WSTOPPED 24 | Unix.WSIGNALED 24 | Unix.WEXITED 124 
      | Unix.WEXITED 152 -> 
          (* (*128 +*) SIGXCPU signal (i.e. 24, /usr/include/bits/signum.h) *) 
166 167 168 169 170 171
          (* 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 *)
172 173
          Timeout
      | Unix.WSTOPPED _ | Unix.WSIGNALED _ -> HighFailure
174
      | Unix.WEXITED _ ->
175 176 177
          let rec greps res = function
            | [] -> HighFailure
            | (r,pa)::l ->
178 179 180 181 182 183 184
                if grep r res 
                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
185 186 187 188 189 190 191 192 193 194 195 196
          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...*)
  (* *)


let check_prover prover = 
  if prover.pr_call_file = None && prover.pr_call_stdin = None then
    raise NoCommandlineProvided

Francois Bobot's avatar
Francois Bobot committed
197
let regexp_call_file = Str.regexp "%\\([a-z]\\)"
198 199 200 201 202

let rec on_file ?debug ?timeout pr filename = 
  check_prover pr;
  match pr.pr_call_file with
    | Some cmd -> 
203 204 205 206 207 208 209
        let filename = if is_true_cygwin 
        then 
          let cin = Unix.open_process_in 
            (sprintf "cygpath -am \"%s\"" filename) in
          let f = input_line cin in
          close_in cin; f
        else filename in
210 211 212
        let cmd = 
          let repl_fun s = 
            match Str.matched_group 1 s with
Francois Bobot's avatar
Francois Bobot committed
213
              | "s" -> filename
214 215 216 217 218
              | _ -> 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
    | None -> 
219 220
        let formatter = Sysutil.file_contents_fmt filename in
        on_formatter ?timeout ?debug pr formatter
221

222
and on_formatter ?debug ?timeout ?filename pr formatter =
223
  check_prover pr;
Francois Bobot's avatar
Francois Bobot committed
224
  match pr.pr_call_stdin with
225
    | Some cmd -> 
226
        let res = timed_sys_command ?debug ?timeout ~formatter cmd in
227 228 229 230
        treat_result pr res
    | None -> 
        match filename with
          | None -> raise NoCommandlineProvided
Francois Bobot's avatar
Francois Bobot committed
231
          | Some filename -> Sysutil.open_temp_file ?debug filename
232
              (fun file cout ->
233 234 235
                 let fmt = formatter_of_out_channel cout in
                 formatter fmt;
                 pp_print_flush fmt ();
236
                 on_file ?timeout ?debug pr file)
237 238 239 240 241 242 243 244 245 246 247 248 249 250 251


let on_buffer ?debug ?timeout ?filename pr buffer =
  check_prover pr;
  match pr.pr_call_stdin with
    | Some cmd -> 
        let res = timed_sys_command ?debug ?timeout ~buffer cmd in
        treat_result pr res
    | None -> 
        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)