replay.ml 6.09 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58


open Why


let includes = ref []
let file = ref None
let opt_version = ref false

let spec = Arg.align [
  ("-I",
   Arg.String (fun s -> includes := s :: !includes),
   "<s> add s to loadpath") ;
(*
  ("-f",
   Arg.String (fun s -> input_files := s :: !input_files),
   "<f> add file f to the project (ignored if it is already there)") ;
*)
  ("-v",
   Arg.Set opt_version,
   " print version information") ;
]

let version_msg = Format.sprintf "Why3 replayer, version %s (build date: %s)"
  Config.version Config.builddate

let usage_str = Format.sprintf
  "Usage: %s [options] [<file.why>|<project directory>]"
  (Filename.basename Sys.argv.(0))

let set_file f = match !file with
  | Some _ ->
      raise (Arg.Bad "only one parameter")
  | None ->
      file := Some f

let () = Arg.parse spec set_file usage_str

let () =
  if !opt_version then begin
    Format.printf "%s@." version_msg;
    exit 0
  end

let fname = match !file with
  | None ->
      Arg.usage spec usage_str;
      exit 1
  | Some f ->
      f

let config = Whyconf.read_config None

let loadpath = (Whyconf.loadpath (Whyconf.get_main config))
  (* @ List.rev !includes *)

let env = Lexer.create_env loadpath

MARCHE Claude's avatar
MARCHE Claude committed
59
let provers = Whyconf.get_provers config
MARCHE Claude's avatar
MARCHE Claude committed
60 61 62 63 64 65 66 67 68 69 70 71 72 73

let provers =
  Util.Mstr.fold (Session.get_prover_data env) provers Util.Mstr.empty

let usleep t = ignore (Unix.select [] [] [] t)


let idle_handler = ref None
let timeout_handler = ref None

module M = Session.Make
  (struct
     type key = int

MARCHE Claude's avatar
MARCHE Claude committed
74
     let create ?parent () =
MARCHE Claude's avatar
MARCHE Claude committed
75 76 77 78 79 80
       match parent with
         | None -> 0
         | Some  n -> n+1

     let remove _row = ()

MARCHE Claude's avatar
MARCHE Claude committed
81 82
     let reset () = ()

MARCHE Claude's avatar
MARCHE Claude committed
83 84 85 86 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
     let idle f =
       match !idle_handler with
         | None -> idle_handler := Some f;
         | Some _ -> failwith "Replay.idle: already one handler installed"

     let timeout ~ms f =
       match !timeout_handler with
         | None -> timeout_handler := Some(float ms /. 1000.0 ,f);
         | Some _ -> failwith "Replay.timeout: already one handler installed"

   end)



let main_loop () =
  let last = ref (Unix.gettimeofday ()) in
  while true do
    let time = Unix.gettimeofday () -. !last in
    (* attempt to run timeout handler *)
    let timeout =
      match !timeout_handler with
        | None -> false
        | Some(ms,f) ->
            if time > ms then
              let b = f () in
              if b then true else
                begin
                  timeout_handler := None;
                  true
                end
            else false
    in
    if timeout then
      last := Unix.gettimeofday ()
    else
      (* attempt to run the idle handler *)
      match !idle_handler with
MARCHE Claude's avatar
MARCHE Claude committed
120 121 122
        | None ->
            begin
              let ms =
MARCHE Claude's avatar
MARCHE Claude committed
123
                match !timeout_handler with
124
                  | None -> raise Exit
MARCHE Claude's avatar
MARCHE Claude committed
125 126 127 128
                  | Some(ms,_) -> ms
              in
              usleep (ms -. time)
            end
MARCHE Claude's avatar
MARCHE Claude committed
129
        | Some f ->
MARCHE Claude's avatar
MARCHE Claude committed
130 131 132 133 134 135 136 137 138 139 140
            let b = f () in
            if b then () else
              begin
                idle_handler := None;
              end
  done

open Format

let model_index = Hashtbl.create 257

MARCHE Claude's avatar
MARCHE Claude committed
141 142
let init =
  let cpt = ref 0 in
MARCHE Claude's avatar
MARCHE Claude committed
143 144 145 146 147 148 149 150 151 152 153 154 155 156
  fun _row any ->
    incr cpt;
    Hashtbl.add model_index !cpt any;
    let name =
      match any with
        | M.Goal g -> M.goal_expl g
        | M.Theory th -> M.theory_name th
        | M.File f -> Filename.basename f.M.file_name
        | M.Proof_attempt a -> let p = a.M.prover in
	  p.Session.prover_name ^ " " ^ p.Session.prover_version
        | M.Transformation tr -> Session.transformation_id tr.M.transf
    in
    printf "Item '%s' loaded@." name

MARCHE Claude's avatar
MARCHE Claude committed
157
let string_of_result result =
MARCHE Claude's avatar
MARCHE Claude committed
158 159 160 161 162 163 164 165 166 167 168 169 170
  match result with
    | Session.Undone -> "undone"
    | Session.Scheduled -> "scheduled"
    | Session.Running -> "running"
    | Session.InternalFailure _ -> "internal failure"
    | Session.Done r -> match r.Call_provers.pr_answer with
	| Call_provers.Valid -> "valid"
	| Call_provers.Invalid -> "invalid"
	| Call_provers.Timeout -> "timeout"
	| Call_provers.Unknown _ -> "unknown"
	| Call_provers.Failure _ -> "failure"
	| Call_provers.HighFailure -> "high failure"

MARCHE Claude's avatar
MARCHE Claude committed
171
let print_result fmt res =
MARCHE Claude's avatar
MARCHE Claude committed
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190
  let t = match res with
    | Session.Done { Call_provers.pr_time = time } ->
	Format.sprintf "(%.2f)" time
    | _ -> ""
  in
  fprintf fmt "%s%s" (string_of_result res) t


let notify any =
  match any with
    | M.Goal g ->
	printf "Goal '%s' proved: %b@." (M.goal_expl g) (M.goal_proved g)
    | M.Theory th ->
	printf "Theory '%s' verified: %b@." (M.theory_name th) (M.verified th)
    | M.File file ->
	printf "File '%s' verified: %b@." (Filename.basename file.M.file_name)
          file.M.file_verified
    | M.Proof_attempt a ->
        let p = a.M.prover in
MARCHE Claude's avatar
MARCHE Claude committed
191 192
	printf "Proof with '%s %s' gives %a@."
	  p.Session.prover_name p.Session.prover_version
MARCHE Claude's avatar
MARCHE Claude committed
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 221 222 223 224
          print_result a.M.proof_state
    | M.Transformation tr ->
	printf "Transformation '%s' proved: %b@."
          (Session.transformation_id tr.M.transf) tr.M.transf_proved


let project_dir =
  if Sys.file_exists fname then
    begin
      if Sys.is_directory fname then
        begin
          eprintf "Info: found directory '%s' for the project@." fname;
          fname
        end
      else
        begin
          eprintf "Info: found regular file '%s'@." fname;
          let d =
            try Filename.chop_extension fname
            with Invalid_argument _ -> fname
          in
          eprintf "Info: using '%s' as directory for the project@." d;
          d
        end
    end
  else
    failwith "file does not exist"

let main () =
  try
    eprintf "Opening session...@?";
    M.open_session ~env ~provers ~init ~notify project_dir;
MARCHE Claude's avatar
MARCHE Claude committed
225
    M.maximum_running_proofs :=
MARCHE Claude's avatar
MARCHE Claude committed
226 227
      Whyconf.running_provers_max (Whyconf.get_main config);
    eprintf " done@.";
228
    let files = M.get_all_files () in
MARCHE Claude's avatar
MARCHE Claude committed
229 230
    List.iter
      (fun f ->
231 232 233 234 235
         eprintf "Replaying file '%s'@." f.M.file_name;
         M.replay ~obsolete_only:false
           ~context_unproved_goals_only:false (M.File f)) files;
    try main_loop ()
    with Exit -> eprintf "Everything done@."
MARCHE Claude's avatar
MARCHE Claude committed
236 237 238 239 240 241 242
  with e ->
    eprintf "Error while opening session with database '%s'@." project_dir;
    eprintf "Aborting...@.";
    raise e


let () = Printexc.catch main ()