replay.ml 19.3 KB
Newer Older
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7 8 9 10 11 12 13 14 15 16 17 18
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
19 20


21
open Why3
MARCHE Claude's avatar
MARCHE Claude committed
22 23 24 25 26


let includes = ref []
let file = ref None
let opt_version = ref false
27
let opt_stats = ref true
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
28 29
let opt_latex = ref ""
let opt_latex2 = ref ""
Asma Tafat's avatar
Asma Tafat committed
30
let opt_html = ref ""
31
let opt_force = ref false
32 33 34 35 36 37 38
let opt_smoke = ref Session.SD_None

let set_opt_smoke = function
  | "none" -> opt_smoke := Session.SD_None
  | "top" ->  opt_smoke := Session.SD_Top
  | "deep" ->  opt_smoke := Session.SD_Deep
  | _ -> assert false
MARCHE Claude's avatar
MARCHE Claude committed
39 40 41 42 43

let spec = Arg.align [
  ("-I",
   Arg.String (fun s -> includes := s :: !includes),
   "<s> add s to loadpath") ;
44 45
  ("-force",
   Arg.Set opt_force,
Asma Tafat's avatar
Asma Tafat committed
46
   " enforce saving of session even if replay failed") ;
47 48 49
  ("-smoke-detector",
   Arg.Symbol (["none";"top";"deep"],set_opt_smoke),
   " try to detect if the context is self-contradicting") ;
50 51 52
  ("-s",
   Arg.Clear opt_stats,
   " do not print statistics") ;
MARCHE Claude's avatar
MARCHE Claude committed
53 54 55
  ("-v",
   Arg.Set opt_version,
   " print version information") ;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
56
  ("-latex",
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
57
   Arg.Set_string opt_latex,
Asma Tafat's avatar
Asma Tafat committed
58
   " [Dir_output] produce latex statistics") ;
Asma Tafat's avatar
Asma Tafat committed
59
  ("-latex2",
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
60
   Arg.Set_string opt_latex2,
Asma Tafat's avatar
Asma Tafat committed
61
   " [Dir_output] produce latex statistics") ;
Asma Tafat's avatar
Asma Tafat committed
62 63
  ("-html",
   Arg.Set_string opt_html,
Asma Tafat's avatar
Asma Tafat committed
64
   " [Dir_output] produce html statistics") ;
MARCHE Claude's avatar
MARCHE Claude committed
65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
]

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

88 89 90 91 92 93
let () =
  if !opt_smoke <> Session.SD_None && !opt_force then begin
    Format.printf "You can't force when detecting smoke@.";
    exit 1
  end

MARCHE Claude's avatar
MARCHE Claude committed
94 95 96 97 98 99 100 101 102 103
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))
MARCHE Claude's avatar
MARCHE Claude committed
104
  @ List.rev !includes
MARCHE Claude's avatar
MARCHE Claude committed
105

106
let env = Env.create_env loadpath
MARCHE Claude's avatar
MARCHE Claude committed
107

MARCHE Claude's avatar
MARCHE Claude committed
108
let provers = Whyconf.get_provers config
MARCHE Claude's avatar
MARCHE Claude committed
109 110 111 112 113 114 115 116 117 118 119 120 121 122

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
123
     let create ?parent () =
MARCHE Claude's avatar
MARCHE Claude committed
124 125 126 127 128 129
       match parent with
         | None -> 0
         | Some  n -> n+1

     let remove _row = ()

MARCHE Claude's avatar
MARCHE Claude committed
130 131
     let reset () = ()

MARCHE Claude's avatar
MARCHE Claude committed
132 133 134 135 136 137 138 139 140 141
     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"

142
     let notify_timer_state w s r =
Asma Tafat's avatar
Asma Tafat committed
143
       Printf.eprintf "Progress: %d/%d/%d   \r%!" w s r
144

MARCHE Claude's avatar
MARCHE Claude committed
145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
   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
171 172 173
        | None ->
            begin
              let ms =
MARCHE Claude's avatar
MARCHE Claude committed
174
                match !timeout_handler with
175
                  | None -> 100.0 (* raise Exit *)
MARCHE Claude's avatar
MARCHE Claude committed
176 177 178 179
                  | Some(ms,_) -> ms
              in
              usleep (ms -. time)
            end
MARCHE Claude's avatar
MARCHE Claude committed
180
        | Some f ->
MARCHE Claude's avatar
MARCHE Claude committed
181 182 183 184 185 186 187 188 189
            let b = f () in
            if b then () else
              begin
                idle_handler := None;
              end
  done

open Format

190
(*
MARCHE Claude's avatar
MARCHE Claude committed
191
let model_index = Hashtbl.create 257
192
*)
MARCHE Claude's avatar
MARCHE Claude committed
193

MARCHE Claude's avatar
MARCHE Claude committed
194
let init =
195
(*
MARCHE Claude's avatar
MARCHE Claude committed
196
  let cpt = ref 0 in
197
*)
MARCHE Claude's avatar
MARCHE Claude committed
198
  fun _row any ->
199
(*
MARCHE Claude's avatar
MARCHE Claude committed
200 201
    incr cpt;
    Hashtbl.add model_index !cpt any;
202
*)
203
    let _name =
MARCHE Claude's avatar
MARCHE Claude committed
204 205 206 207
      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
MARCHE Claude's avatar
MARCHE Claude committed
208
        | M.Proof_attempt a ->
209 210 211
            begin
              match a.M.prover with
                | M.Detected_prover p ->
212
                    p.Session.prover_name ^ " " ^ p.Session.prover_version
213 214
                | M.Undetected_prover s -> s
            end
MARCHE Claude's avatar
MARCHE Claude committed
215 216
        | M.Transformation tr -> Session.transformation_id tr.M.transf
    in
MARCHE Claude's avatar
MARCHE Claude committed
217 218
    (* eprintf "Item '%s' loaded@." name *)
    ()
MARCHE Claude's avatar
MARCHE Claude committed
219

MARCHE Claude's avatar
MARCHE Claude committed
220
(*
MARCHE Claude's avatar
MARCHE Claude committed
221
let string_of_result result =
MARCHE Claude's avatar
MARCHE Claude committed
222 223 224 225 226 227
  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
228 229 230 231 232 233
        | 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
234

MARCHE Claude's avatar
MARCHE Claude committed
235
let print_result fmt res =
MARCHE Claude's avatar
MARCHE Claude committed
236 237
  let t = match res with
    | Session.Done { Call_provers.pr_time = time } ->
238
        Format.sprintf "(%.1f)" time
MARCHE Claude's avatar
MARCHE Claude committed
239 240 241
    | _ -> ""
  in
  fprintf fmt "%s%s" (string_of_result res) t
MARCHE Claude's avatar
MARCHE Claude committed
242 243
*)

MARCHE Claude's avatar
MARCHE Claude committed
244

MARCHE Claude's avatar
MARCHE Claude committed
245 246
let print_result fmt
    {Call_provers.pr_answer=ans; Call_provers.pr_output=out;
247 248
     Call_provers.pr_time=_t} =
(*
MARCHE Claude's avatar
MARCHE Claude committed
249
  fprintf fmt "%a (%.1fs)" Call_provers.print_prover_answer ans t;
250 251
*)
  fprintf fmt "%a" Call_provers.print_prover_answer ans;
MARCHE Claude's avatar
MARCHE Claude committed
252 253
  if ans == Call_provers.HighFailure then
    fprintf fmt "@\nProver output:@\n%s@." out
MARCHE Claude's avatar
MARCHE Claude committed
254

255 256
let notify _any = ()
(*
MARCHE Claude's avatar
MARCHE Claude committed
257 258
  match any with
    | M.Goal g ->
259
        printf "Goal '%s' proved: %b@." (M.goal_expl g) (M.goal_proved g)
MARCHE Claude's avatar
MARCHE Claude committed
260
    | M.Theory th ->
261
        printf "Theory '%s' verified: %b@." (M.theory_name th) (M.verified th)
MARCHE Claude's avatar
MARCHE Claude committed
262
    | M.File file ->
263
        printf "File '%s' verified: %b@." (Filename.basename file.M.file_name)
MARCHE Claude's avatar
MARCHE Claude committed
264 265 266
          file.M.file_verified
    | M.Proof_attempt a ->
        let p = a.M.prover in
267 268
        printf "Proof with '%s %s' gives %a@."
          p.Session.prover_name p.Session.prover_version
MARCHE Claude's avatar
MARCHE Claude committed
269 270
          print_result a.M.proof_state
    | M.Transformation tr ->
271
        printf "Transformation '%s' proved: %b@."
MARCHE Claude's avatar
MARCHE Claude committed
272
          (Session.transformation_id tr.M.transf) tr.M.transf_proved
273
*)
MARCHE Claude's avatar
MARCHE Claude committed
274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296

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"

297 298 299 300 301
let goal_statistics (goals,n,m) g =
  if M.goal_proved g then (goals,n+1,m+1) else (g::goals,n,m+1)

let theory_statistics (ths,n,m) th =
  let goals,n1,m1 = List.fold_left goal_statistics ([],0,0) (M.goals th) in
302
  ((th,goals,n1,m1)::ths,n+n1,m+m1)
303 304 305

let file_statistics (files,n,m) f =
  let ths,n1,m1 = List.fold_left theory_statistics ([],0,0) f.M.theories in
306
  ((f,ths,n1,m1)::files,n+n1,m+m1)
307 308

let print_statistics files =
François Bobot's avatar
François Bobot committed
309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324
  let print_goal g =
      printf "         +--goal %s not proved@." (M.goal_name g)
  in
  let print_theory (th,goals,n,m) =
    if n<m then begin
      printf "      +--theory %s: %d/%d@." (M.theory_name th) n m;
      List.iter print_goal (List.rev goals)
    end
  in
  let print_file (f,ths,n,m) =
    if n<m then begin
      printf "   +--file %s: %d/%d@." f.M.file_name n m;
      List.iter print_theory (List.rev ths)
    end
  in
  List.iter print_file (List.rev files)
MARCHE Claude's avatar
MARCHE Claude committed
325

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
326
(* Statistics in LaTeX*)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
327

Asma Tafat's avatar
Asma Tafat committed
328
let rec transf_depth tr =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
329 330
  List.fold_left (fun depth g -> max depth (goal_depth g)) 0 (tr.M.subgoals)
and goal_depth g =
Asma Tafat's avatar
Asma Tafat committed
331
  Hashtbl.fold
François Bobot's avatar
François Bobot committed
332 333
    (fun _st tr depth -> max depth (1 + transf_depth tr))
    (M.transformations g) 0
Asma Tafat's avatar
Asma Tafat committed
334 335

let theory_depth t =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
336
  List.fold_left (fun depth g -> max depth (goal_depth g)) 0 (M.goals t)
Asma Tafat's avatar
Asma Tafat committed
337 338

let rec provers_latex_stats provers g =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
339
  let proofs = M.external_proofs g in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
340
  Hashtbl.iter (fun p a-> Hashtbl.replace provers p a.M.prover) proofs;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
341
  let tr = M.transformations g in
Asma Tafat's avatar
Asma Tafat committed
342
  Hashtbl.iter (fun _st tr ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
343
    let goals = tr.M.subgoals in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
344
    List.iter (provers_latex_stats provers) goals) tr
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
345

Asma Tafat's avatar
Asma Tafat committed
346
let prover_name a =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
347
  match a with
François Bobot's avatar
François Bobot committed
348 349
      M.Detected_prover d ->
        d.Session.prover_name ^ " " ^ d.Session.prover_version
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
350
    | M.Undetected_prover s -> s
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
351

Asma Tafat's avatar
Asma Tafat committed
352 353 354 355
let protect s =
  let b = Buffer.create 7 in
  for i = 0 to String.length s - 1 do
    match s.[i] with
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
356 357 358 359 360
	'_' -> Buffer.add_string b "\\_"
      | c -> Buffer.add_char b c
  done;
  Buffer.contents b

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
361
let rec goal_latex_stat n fmt prov depth depth_max column subgoal g =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
362 363
  if n == 1 then
    begin
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
364 365 366 367 368 369
      if depth > 0 then
	if subgoal > 0 then
	  fprintf fmt "\\cline{%d-%d} @." (depth + 1) column
	else ()
      else
	fprintf fmt "\\hline @.";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
370 371 372
    end
  else
    begin
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
373 374 375 376
      if depth > 0 then
	fprintf fmt "\\cline{%d-%d} @." 2 column
      else
	fprintf fmt "\\hline @."
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
377
    end;
Asma Tafat's avatar
Asma Tafat committed
378
  if(n ==1) then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
379
    begin
Asma Tafat's avatar
Asma Tafat committed
380
      if depth_max > 1 then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
381
	begin
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
382
	  if subgoal > 0 then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
383 384
	    begin
	      if(depth < depth_max)  then
François Bobot's avatar
François Bobot committed
385 386 387
		for i = 1 to depth do
                  fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
                done
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
388
	      else
François Bobot's avatar
François Bobot committed
389 390 391
		for i = 1 to depth - 1 do
                  fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
                done
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
392
	    end
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
393
	  else
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
394
	    if(depth < depth_max) then
François Bobot's avatar
François Bobot committed
395 396
	      if depth > 0 then
                fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
397 398 399
	end
      else
	begin
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
400
	  if subgoal > 0  then
François Bobot's avatar
François Bobot committed
401 402
	    for i = 1 to depth  do
              fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " done
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
403
	  else
François Bobot's avatar
François Bobot committed
404 405
	    if depth > 0 then
              fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
406 407
	end
    end
Asma Tafat's avatar
Asma Tafat committed
408
  else
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
409
    for i = 1 to depth do fprintf fmt "\\quad" done;
Asma Tafat's avatar
Asma Tafat committed
410
  if (depth <= 1) then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
411
    fprintf fmt "\\explanation{%s} " (protect (M.goal_expl g))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
412 413
  else
    if n == 2 then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
414
      fprintf fmt "\\explanation{%d} " (subgoal + 1)
Asma Tafat's avatar
Asma Tafat committed
415 416
    else
      fprintf fmt "\\explanation{%s}"  " ";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
417
  let proofs = M.external_proofs g in
Asma Tafat's avatar
Asma Tafat committed
418
  if (Hashtbl.length proofs) > 0 then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
419
    begin
Asma Tafat's avatar
Asma Tafat committed
420 421
      if (n == 1) then
	begin
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
422
	  if depth_max <= 1 then
Asma Tafat's avatar
Asma Tafat committed
423
	    begin
Asma Tafat's avatar
Asma Tafat committed
424
	      if depth > 0 then
François Bobot's avatar
François Bobot committed
425 426
		for i = depth to (depth_max - depth) do
                  fprintf fmt "& \\explanation{%s}" " " done
Asma Tafat's avatar
Asma Tafat committed
427
	      else
François Bobot's avatar
François Bobot committed
428 429
		for i = depth to (depth_max - depth - 1) do
                  fprintf fmt "& \\explanation{%s}" " " done
Asma Tafat's avatar
Asma Tafat committed
430
	    end
Asma Tafat's avatar
Asma Tafat committed
431
	  else
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
432
	      if depth > 0 then
François Bobot's avatar
François Bobot committed
433 434
		for i = depth to (depth_max - depth - 1) do
                  fprintf fmt "& \\explanation{%s}" " " done
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
435
	      else
François Bobot's avatar
François Bobot committed
436 437
		for i = depth to (depth_max - depth - 2) do
                  fprintf fmt "& \\explanation{%s}" " " done
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
438
	end;
Asma Tafat's avatar
Asma Tafat committed
439 440
      List.iter (fun (p, _pr) ->
	try
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
441 442 443
	  let pr = Hashtbl.find proofs p in
	  let s = pr.M.proof_state in
	  match s with
Asma Tafat's avatar
Asma Tafat committed
444
	      Session.Done res ->
Asma Tafat's avatar
Asma Tafat committed
445 446
		begin
		  match res.Call_provers.pr_answer with
François Bobot's avatar
François Bobot committed
447 448
		      Call_provers.Valid ->
                        fprintf fmt "& \\valid{%.2f} " res.Call_provers.pr_time
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
449 450 451 452
		    | Call_provers.Invalid -> fprintf fmt "& \\invalid "
		    | Call_provers.Timeout -> fprintf fmt "& \\timeout "
		    | Call_provers.Unknown _s -> fprintf fmt "& \\unknown "
		    | _ -> fprintf fmt "& \\failure "
Asma Tafat's avatar
Asma Tafat committed
453
		end
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
454 455
	    | _ -> fprintf fmt "& Undone"
	with Not_found -> fprintf fmt "& \\noresult") prov;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
456
    fprintf fmt "\\\\ @."
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
457 458 459
    end;
  let tr = M.transformations g in
  if Hashtbl.length tr > 0 then
François Bobot's avatar
François Bobot committed
460
  if n == 2 then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
461
    begin
François Bobot's avatar
François Bobot committed
462
      if (Hashtbl.length proofs == 0) then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
463
	fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @." (List.length prov)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
464
    end
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
465
  else
François Bobot's avatar
François Bobot committed
466
      if Hashtbl.length proofs > 0 then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
467 468 469 470
	  fprintf fmt "\\cline{%d-%d} @." (depth + 2) column;
  Hashtbl.iter (fun _st tr ->
    let goals = tr.M.subgoals in
    let _ = List.fold_left (fun subgoal g ->
François Bobot's avatar
François Bobot committed
471 472
      goal_latex_stat n fmt prov (depth + 1) depth_max column (subgoal) g;
      subgoal + 1) 0 goals in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
473
    () ) tr
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
474

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
475

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
476
let theory_latex_stat n dir t =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
477
  let provers = Hashtbl.create 9 in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
478
  List.iter (provers_latex_stats provers) (M.goals t);
François Bobot's avatar
François Bobot committed
479 480
  let provers = Hashtbl.fold (fun p pr acc -> (p, prover_name pr) :: acc)
    provers [] in
Asma Tafat's avatar
Asma Tafat committed
481 482
  let provers =
    List.sort (fun (_p1, n1) (_p2, n2) -> String.compare n1 n2) provers in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
483
  let depth = theory_depth  t in
Asma Tafat's avatar
Asma Tafat committed
484 485 486
  let name = M.theory_name t in
  let ch = open_out (Filename.concat dir(name^".tex")) in
  let fmt = formatter_of_out_channel ch in
Asma Tafat's avatar
Asma Tafat committed
487
      fprintf fmt "\\begin{longtable}";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
488 489
  fprintf fmt "{| l |";
  for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
490
  fprintf fmt "}@.";
Asma Tafat's avatar
Asma Tafat committed
491 492
  if (n == 1) then
    if (depth > 1) then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
493
      fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "  depth
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
494
      else
François Bobot's avatar
François Bobot committed
495 496
      fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
        (depth + 1)
Asma Tafat's avatar
Asma Tafat committed
497
  else
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
498
    fprintf fmt "\\hline Proof obligations ";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
499
  List.iter (fun (_, a) -> fprintf fmt "& \\provername{%s} " a) provers;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
500
  fprintf fmt "\\\\ @.";
Asma Tafat's avatar
Asma Tafat committed
501
  fprintf fmt "\\hline \\endfirsthead @.";
François Bobot's avatar
François Bobot committed
502 503
  fprintf fmt "\\multicolumn{%d}{r}{\\textit{Continued from previous page}} \
\\\\ @." (List.length provers + 1) ;
Asma Tafat's avatar
Asma Tafat committed
504 505 506 507
  fprintf fmt "\\hline @.";
  if (depth > 1) then
    fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "  depth
  else
François Bobot's avatar
François Bobot committed
508 509
    fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
      (depth + 1);
Asma Tafat's avatar
Asma Tafat committed
510 511 512
  List.iter (fun (_, a) -> fprintf fmt "& \\provername{%s} " a) provers;
  fprintf fmt "\\\\ @.";
  fprintf fmt "\\hline \\endhead @.";
François Bobot's avatar
François Bobot committed
513 514
  fprintf fmt "\\hline \\multicolumn{%d}{r}{\\textit{Continued on next page}} \
\\\\ @." (List.length provers);
Asma Tafat's avatar
Asma Tafat committed
515 516
  fprintf fmt "\\endfoot \\endlastfoot @.";

Asma Tafat's avatar
Asma Tafat committed
517 518
  let column =
    if n == 1 then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
519
    if depth > 1
Asma Tafat's avatar
Asma Tafat committed
520
    then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
521
      (List.length provers) + depth
Asma Tafat's avatar
Asma Tafat committed
522
    else
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
523
      (List.length provers) + depth + 1
Asma Tafat's avatar
Asma Tafat committed
524
    else
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
525
      (List.length provers) +  1
Asma Tafat's avatar
Asma Tafat committed
526
  in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
527
  List.iter (goal_latex_stat n fmt provers 0 depth column 0) (M.goals t);
Asma Tafat's avatar
Asma Tafat committed
528 529
  fprintf fmt "\\hline \\caption{%s statistics} @." (protect name);
  fprintf fmt "\\label{%s} \\end{longtable}@." (protect name);
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
530 531 532 533 534 535
  close_out ch

let file_latex_stat n dir f =
   List.iter (theory_latex_stat n dir) f.M.theories

let print_latex_statistics n dir =
536
  let files = M.get_all_files () in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
537
  List.iter (file_latex_stat n dir) files
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
538

MARCHE Claude's avatar
MARCHE Claude committed
539
let print_report (g,p,r) =
540 541
  printf "   goal '%s', prover '%s': " g p;
  match r with
MARCHE Claude's avatar
MARCHE Claude committed
542
  | M.Wrong_result(new_res,old_res) ->
543 544 545 546 547 548 549
    begin match !opt_smoke with
      | Session.SD_None ->
        printf "%a instead of %a@."
          print_result new_res print_result old_res
      | _ ->
        printf "Smoke detected!!!@."
    end
550 551 552 553 554 555 556
  | M.No_former_result ->
      printf "no former result available@."
  | M.CallFailed msg ->
      printf "internal failure '%a'@." Exn_printer.exn_printer msg;
  | M.Prover_not_installed ->
      printf "not installed@."

557
let add_to_check_no_smoke found_obs =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
558
      let callback report =
559
        eprintf "@.";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
560 561 562
	let files,n,m =
          List.fold_left file_statistics ([],0,0) (M.get_all_files ())
	in
563
      match report with
564
        | [] ->
565 566
            if found_obs then
              if n=m then
François Bobot's avatar
François Bobot committed
567 568
                printf " %d/%d (replay OK, all proved: obsolete session \
updated)@." n m
569
              else
570
                if !opt_force then
François Bobot's avatar
François Bobot committed
571 572
                  printf " %d/%d (replay OK, but not all proved: obsolete \
session updated since -force was given)@." n m
573
                else
François Bobot's avatar
François Bobot committed
574 575
                  printf " %d/%d (replay OK, but not all proved: obsolete \
session NOT updated)@." n m
576 577
            else
              printf " %d/%d@." n m ;
578
            if !opt_stats && n<m then print_statistics files;
579
            eprintf "Everything replayed OK.@.";
MARCHE Claude's avatar
MARCHE Claude committed
580
            if found_obs && (n=m || !opt_force) then
581 582 583 584 585
              begin
                eprintf "Updating obsolete session...@?";
                M.save_session ();
                eprintf " done@."
              end;
586 587
            exit 0
        | _ ->
588
            printf " %d/%d (replay failed)@." n m ;
589
            List.iter print_report report;
590
            eprintf "Replay failed.@.";
591
            exit 1
592
    in
593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642
    M.check_all ~callback

let add_to_check_smoke () =
  let callback report =
    eprintf "@.";
    match report with
      | [] ->
        eprintf "No smoke detected.@.";
        exit 0
      | _ ->
        List.iter print_report report;
        eprintf "Smoke detected.@.";
        exit 1
  in
  M.check_all ~callback

let add_to_check found_obs =
  match !opt_smoke with
    | Session.SD_None -> add_to_check_no_smoke found_obs;
    | _ -> assert (not found_obs); add_to_check_smoke ()


let () =
  try
    eprintf "Opening session...@?";
    let found_obs =
      M.open_session ~allow_obsolete:true
        ~env ~config ~init ~notify project_dir
    in
    if found_obs then begin
      if !opt_smoke <> Session.SD_None then begin
        eprintf
          "[Error] I can't run the smoke detector if the session is obsolete";
        exit 1
      end;
      eprintf "[Warning] session is obsolete@.";
    end;
    M.maximum_running_proofs :=
      Whyconf.running_provers_max (Whyconf.get_main config);
    M.smoke_detector := !opt_smoke;
    eprintf " done@.";
    if !opt_latex <> "" then print_latex_statistics 1 !opt_latex
    else
    if !opt_latex2 <> "" then print_latex_statistics 2 !opt_latex2
    else
      begin
        add_to_check found_obs;
        try main_loop ()
        with Exit -> eprintf "main replayer exited unexpectedly@."
      end
643 644
  with
    | M.OutdatedSession ->
645
        eprintf "The session database '%s' is outdated, cannot replay@."
646 647 648 649
          project_dir;
        eprintf "Aborting...@.";
        exit 1
    | e when not (Debug.test_flag Debug.stack_trace) ->
650
        eprintf "Error while opening session with database '%s' : %a@."
651 652 653 654
          project_dir
          Exn_printer.exn_printer e;
        eprintf "Aborting...@.";
        exit 1
MARCHE Claude's avatar
MARCHE Claude committed
655 656


657 658 659 660 661
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3replayer.byte"
End:
*)