replay.ml 22.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


François Bobot's avatar
François Bobot committed
21
open Format
22
open Why3
François Bobot's avatar
François Bobot committed
23
module S = Session
24
module C = Whyconf
MARCHE Claude's avatar
MARCHE Claude committed
25 26 27 28

let includes = ref []
let file = ref None
let opt_version = ref false
29
let opt_stats = ref true
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
30 31
let opt_latex = ref ""
let opt_latex2 = ref ""
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
32
let opt_longtable = ref false
33
let opt_force = ref false
François Bobot's avatar
François Bobot committed
34
let opt_convert_unknown_provers = ref false
35
let opt_remove_converted = ref false
François Bobot's avatar
François Bobot committed
36 37 38 39 40 41 42 43 44 45
(** {2 Smoke detector} *)

type smoke_detector =
  | SD_None (** No smoke detector *)
  | SD_Top  (** Negation added at the top of the goals *)
  | SD_Deep
(** Negation added under implication and universal quantification *)


let opt_smoke = ref SD_None
46 47

let set_opt_smoke = function
François Bobot's avatar
François Bobot committed
48 49 50
  | "none" -> opt_smoke := SD_None
  | "top" ->  opt_smoke := SD_Top
  | "deep" ->  opt_smoke := SD_Deep
51
  | _ -> assert false
MARCHE Claude's avatar
MARCHE Claude committed
52 53 54 55 56

let spec = Arg.align [
  ("-I",
   Arg.String (fun s -> includes := s :: !includes),
   "<s> add s to loadpath") ;
57 58
  ("-force",
   Arg.Set opt_force,
Asma Tafat's avatar
Asma Tafat committed
59
   " enforce saving of session even if replay failed") ;
60 61 62
  ("-smoke-detector",
   Arg.Symbol (["none";"top";"deep"],set_opt_smoke),
   " try to detect if the context is self-contradicting") ;
63 64 65
  ("-s",
   Arg.Clear opt_stats,
   " do not print statistics") ;
MARCHE Claude's avatar
MARCHE Claude committed
66 67 68
  ("-v",
   Arg.Set opt_version,
   " print version information") ;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
69
  ("-latex",
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
70
   Arg.Set_string opt_latex,
Asma Tafat's avatar
Asma Tafat committed
71
   " [Dir_output] produce latex statistics") ;
Asma Tafat's avatar
Asma Tafat committed
72
  ("-latex2",
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
73
   Arg.Set_string opt_latex2,
Asma Tafat's avatar
Asma Tafat committed
74
   " [Dir_output] produce latex statistics") ;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
75 76 77
  ("-longtable",
   Arg.Set opt_longtable,
   " produce latex statistics using longtable package") ;
François Bobot's avatar
François Bobot committed
78
  "--convert-unknown-provers", Arg.Set opt_convert_unknown_provers,
79 80 81
  " try to find compatible provers for all unknown provers.";
  "--remove-converted", Arg.Set opt_remove_converted,
  " The external proof which have been converted are removed";
82 83 84 85 86 87 88
  Debug.Opt.desc_debug_list;
  Debug.Opt.desc_shortcut "parse_only" "--parse-only" " Stop after parsing";
  Debug.Opt.desc_shortcut
    "type_only" "--type-only" " Stop after type checking";
  Debug.Opt.desc_debug_all;
  Debug.Opt.desc_debug;

MARCHE Claude's avatar
MARCHE Claude committed
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111
]

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

François Bobot's avatar
François Bobot committed
112 113 114 115 116
(* let () = *)
(*   if !opt_smoke <> Session.SD_None && !opt_force then begin *)
(*     Format.printf "You can't force when detecting smoke@."; *)
(*     exit 1 *)
(*   end *)
117

118

MARCHE Claude's avatar
MARCHE Claude committed
119 120 121 122 123 124 125 126 127 128
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
129
  @ List.rev !includes
MARCHE Claude's avatar
MARCHE Claude committed
130

131
let env = Env.create_env loadpath
MARCHE Claude's avatar
MARCHE Claude committed
132

Andrei Paskevich's avatar
Andrei Paskevich committed
133 134
let () = Whyconf.load_plugins (Whyconf.get_main config)

135 136 137 138
let () =
  Debug.Opt.set_flags_selected ();
  if Debug.Opt.option_list () then exit 0

MARCHE Claude's avatar
MARCHE Claude committed
139 140 141 142 143 144
let usleep t = ignore (Unix.select [] [] [] t)


let idle_handler = ref None
let timeout_handler = ref None

François Bobot's avatar
François Bobot committed
145
module O =
MARCHE Claude's avatar
MARCHE Claude committed
146 147 148
  (struct
     type key = int

MARCHE Claude's avatar
MARCHE Claude committed
149
     let create ?parent () =
MARCHE Claude's avatar
MARCHE Claude committed
150 151 152 153 154 155
       match parent with
         | None -> 0
         | Some  n -> n+1

     let remove _row = ()

MARCHE Claude's avatar
MARCHE Claude committed
156 157
     let reset () = ()

MARCHE Claude's avatar
MARCHE Claude committed
158 159 160 161 162 163 164 165 166 167
     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"

168
     let notify_timer_state w s r =
169
       Printf.eprintf "Progress: %d/%d/%d                       \r%!" w s r
170

François Bobot's avatar
François Bobot committed
171 172 173 174 175

let init =
(*
  let cpt = ref 0 in
*)
176
  fun _row _any ->
François Bobot's avatar
François Bobot committed
177 178 179
(*
    incr cpt;
    Hashtbl.add model_index !cpt any;
180

François Bobot's avatar
François Bobot committed
181 182 183 184 185 186 187
    let _name =
      match any with
        | S.Goal g -> S.goal_expl g
        | S.Theory th -> th.S.theory_name.Ident.id_string
        | S.File f -> Filename.basename f.S.file_name
        | S.Proof_attempt a ->
          let p = a.S.proof_prover in
188
          p.C.prover_name ^ " " ^ p.C.prover_version
François Bobot's avatar
François Bobot committed
189 190
        | S.Transf tr -> tr.S.transf_name
    in
191
*)
François Bobot's avatar
François Bobot committed
192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215
    (* eprintf "Item '%s' loaded@." name *)
    ()


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
        printf "Proof with '%s %s' gives %a@."
          p.Session.prover_name p.Session.prover_version
          print_result a.M.proof_state
    | M.Transformation tr ->
        printf "Transformation '%s' proved: %b@."
          (Session.transformation_id tr.M.transf) tr.M.transf_proved
*)

216 217 218
let unknown_prover _ _ = None

let replace_prover _ _ = false
François Bobot's avatar
François Bobot committed
219

MARCHE Claude's avatar
MARCHE Claude committed
220 221
   end)

François Bobot's avatar
François Bobot committed
222 223 224 225 226 227 228 229 230 231 232
module M = Session_scheduler.Make(O)

let print_result fmt
    {Call_provers.pr_answer=ans; Call_provers.pr_output=out;
     Call_provers.pr_time=_t} =
(*
  fprintf fmt "%a (%.1fs)" Call_provers.print_prover_answer ans t;
*)
  fprintf fmt "%a" Call_provers.print_prover_answer ans;
  if ans == Call_provers.HighFailure then
    fprintf fmt "@\nProver output:@\n%s@." out
MARCHE Claude's avatar
MARCHE Claude committed
233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256

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
257 258 259
        | None ->
            begin
              let ms =
MARCHE Claude's avatar
MARCHE Claude committed
260
                match !timeout_handler with
261
                  | None -> 100.0 (* raise Exit *)
MARCHE Claude's avatar
MARCHE Claude committed
262 263 264 265
                  | Some(ms,_) -> ms
              in
              usleep (ms -. time)
            end
MARCHE Claude's avatar
MARCHE Claude committed
266
        | Some f ->
MARCHE Claude's avatar
MARCHE Claude committed
267 268 269 270 271 272 273
            let b = f () in
            if b then () else
              begin
                idle_handler := None;
              end
  done

274
(*
MARCHE Claude's avatar
MARCHE Claude committed
275
let model_index = Hashtbl.create 257
276
*)
MARCHE Claude's avatar
MARCHE Claude committed
277 278

let project_dir =
279 280 281
  try
    Session.get_project_dir fname
  with Not_found -> failwith "file does not exist"
MARCHE Claude's avatar
MARCHE Claude committed
282

283
let goal_statistics (goals,n,m) g =
François Bobot's avatar
François Bobot committed
284
  if g.S.goal_verified then (goals,n+1,m+1) else (g::goals,n,m+1)
285 286

let theory_statistics (ths,n,m) th =
François Bobot's avatar
François Bobot committed
287 288
  let goals,n1,m1 =
    List.fold_left goal_statistics ([],0,0) th.S.theory_goals in
289
  ((th,goals,n1,m1)::ths,n+n1,m+m1)
290

François Bobot's avatar
François Bobot committed
291 292 293
let file_statistics _ f (files,n,m) =
  let ths,n1,m1 =
    List.fold_left theory_statistics ([],0,0) f.S.file_theories in
294
  ((f,ths,n1,m1)::files,n+n1,m+m1)
295 296

let print_statistics files =
François Bobot's avatar
François Bobot committed
297
  let print_goal g =
François Bobot's avatar
François Bobot committed
298
      printf "         +--goal %s not proved@." g.S.goal_name.Ident.id_string
François Bobot's avatar
François Bobot committed
299 300 301
  in
  let print_theory (th,goals,n,m) =
    if n<m then begin
François Bobot's avatar
François Bobot committed
302 303
      printf "      +--theory %s: %d/%d@."
        th.S.theory_name.Ident.id_string n m;
François Bobot's avatar
François Bobot committed
304 305 306 307 308
      List.iter print_goal (List.rev goals)
    end
  in
  let print_file (f,ths,n,m) =
    if n<m then begin
François Bobot's avatar
François Bobot committed
309
      printf "   +--file %s: %d/%d@." f.S.file_name n m;
François Bobot's avatar
François Bobot committed
310 311 312 313
      List.iter print_theory (List.rev ths)
    end
  in
  List.iter print_file (List.rev files)
MARCHE Claude's avatar
MARCHE Claude committed
314

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
315
(* Statistics in LaTeX*)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
316

Asma Tafat's avatar
Asma Tafat committed
317
let rec transf_depth tr =
François Bobot's avatar
François Bobot committed
318
  List.fold_left (fun depth g -> max depth (goal_depth g)) 0 tr.S.transf_goals
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
319
and goal_depth g =
François Bobot's avatar
François Bobot committed
320
  S.PHstr.fold
François Bobot's avatar
François Bobot committed
321
    (fun _st tr depth -> max depth (1 + transf_depth tr))
François Bobot's avatar
François Bobot committed
322
    g.S.goal_transformations 0
Asma Tafat's avatar
Asma Tafat committed
323 324

let theory_depth t =
François Bobot's avatar
François Bobot committed
325 326 327 328 329 330
  List.fold_left (fun depth g -> max depth (goal_depth g)) 0 t.S.theory_goals

let rec provers_latex_stats provers theory =
  S.theory_iter_proof_attempt (fun a ->
    Hashtbl.replace provers a.S.proof_prover a.S.proof_prover) theory

Asma Tafat's avatar
Asma Tafat committed
331 332 333 334
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
335 336 337 338 339
	'_' -> Buffer.add_string b "\\_"
      | c -> Buffer.add_char b c
  done;
  Buffer.contents b

Asma Tafat's avatar
Asma Tafat committed
340 341

let column n depth provers =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
342
  if n == 1 then
Asma Tafat's avatar
Asma Tafat committed
343 344 345 346
    if depth > 1 then
      (List.length provers) + depth
    else
      (List.length provers) + depth + 1
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
347
  else
Asma Tafat's avatar
Asma Tafat committed
348 349 350
    (List.length provers) +  1


Asma Tafat's avatar
Asma Tafat committed
351
let print_result_prov proofs prov fmt=
François Bobot's avatar
François Bobot committed
352
  List.iter (fun p ->
Asma Tafat's avatar
Asma Tafat committed
353
  try
François Bobot's avatar
François Bobot committed
354 355
    let pr = S.PHprover.find proofs p in
    let s = pr.S.proof_state in
Asma Tafat's avatar
Asma Tafat committed
356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371
      match s with
	  Session.Done res ->
	    begin
	      match res.Call_provers.pr_answer with
		  Call_provers.Valid ->
                    fprintf fmt "& \\valid{%.2f} " res.Call_provers.pr_time
		| Call_provers.Invalid -> fprintf fmt "& \\invalid "
		| Call_provers.Timeout -> fprintf fmt "& \\timeout "
		| Call_provers.Unknown _s -> fprintf fmt "& \\unknown "
		| _ -> fprintf fmt "& \\failure "
	    end
	| _ -> fprintf fmt "& Undone"
  with Not_found -> fprintf fmt "& \\noresult") prov;
  fprintf fmt "\\\\ @."


Asma Tafat's avatar
Asma Tafat committed
372 373 374 375 376 377 378 379 380 381 382 383 384 385 386
let rec goal_latex_stat fmt prov depth depth_max subgoal g =
  let column = column 1 depth prov
  in
    if depth > 0 then
      if subgoal > 0 then
	fprintf fmt "\\cline{%d-%d} @." (depth + 1) column
      else ()
    else
      fprintf fmt "\\hline @.";
    if depth_max > 1 then
      begin
	if subgoal > 0 then
	  begin
	    if(depth < depth_max)  then
	      for i = 1 to depth do
François Bobot's avatar
François Bobot committed
387
                fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
Asma Tafat's avatar
Asma Tafat committed
388 389 390 391 392 393 394 395
              done
	    else
	      for i = 1 to depth - 1 do
                fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
              done
	  end
	else
	  if(depth < depth_max) then
François Bobot's avatar
François Bobot committed
396 397
	    if depth > 0 then
              fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
Asma Tafat's avatar
Asma Tafat committed
398 399 400 401 402 403 404 405 406 407 408
      end
    else
      begin
	if subgoal > 0  then
	  for i = 1 to depth  do
	    fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " done
	else
	  if depth > 0 then
	    fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
      end;
    if (depth <= 1) then
François Bobot's avatar
François Bobot committed
409
      fprintf fmt "\\explanation{%s} " (protect (S.goal_expl g))
Asma Tafat's avatar
Asma Tafat committed
410 411
    else
      fprintf fmt "\\explanation{%s}"  " ";
François Bobot's avatar
François Bobot committed
412 413
    let proofs = g.S.goal_external_proofs in
      if (S.PHprover.length proofs) > 0 then
Asma Tafat's avatar
Asma Tafat committed
414 415 416 417 418 419 420 421 422 423 424
	begin
	  if depth_max <= 1 then
	    begin
	      if depth > 0 then
		for i = depth to (depth_max - depth) do
                  fprintf fmt "& \\explanation{%s}" " " done
	      else
		for i = depth to (depth_max - depth - 1) do
                  fprintf fmt "& \\explanation{%s}" " " done
	    end
	  else
Asma Tafat's avatar
Asma Tafat committed
425 426
	    if depth > 0 then
	      for i = depth to (depth_max - depth - 1) do
Asma Tafat's avatar
Asma Tafat committed
427 428 429 430 431
		fprintf fmt "& \\explanation{%s}" " " done
	    else
	      for i = depth to (depth_max - depth - 2) do
		fprintf fmt "& \\explanation{%s}" " " done;
	  print_result_prov proofs prov fmt;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
432
	end;
François Bobot's avatar
François Bobot committed
433 434 435
      let tr = g.S.goal_transformations in
	if S.PHstr.length tr > 0 then
	  if S.PHprover.length proofs > 0 then
Asma Tafat's avatar
Asma Tafat committed
436
	    fprintf fmt "\\cline{%d-%d} @." (depth + 2) column;
François Bobot's avatar
François Bobot committed
437 438
	S.PHstr.iter (fun _st tr ->
          let goals = tr.S.transf_goals in
Asma Tafat's avatar
Asma Tafat committed
439 440 441 442
	  let _ = List.fold_left (fun subgoal g ->
              goal_latex_stat fmt prov (depth + 1) depth_max (subgoal) g;
               subgoal + 1) 0 goals in
	    () ) tr
Asma Tafat's avatar
Asma Tafat committed
443 444 445 446 447 448 449 450 451 452 453


let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
  let column = column 2 depth prov
  in
    if depth > 0 then
      fprintf fmt "\\cline{%d-%d} @." 2 column
    else
      fprintf fmt "\\hline @.";
    for i = 1 to depth do fprintf fmt "\\quad" done;
    if (depth <= 1) then
François Bobot's avatar
François Bobot committed
454
      fprintf fmt "\\explanation{%s} " (protect (S.goal_expl g))
Asma Tafat's avatar
Asma Tafat committed
455 456
    else
      fprintf fmt "\\explanation{%d} " (subgoal + 1);
François Bobot's avatar
François Bobot committed
457 458
    let proofs = g.S.goal_external_proofs in
      if (S.PHprover.length proofs) > 0 then
Asma Tafat's avatar
Asma Tafat committed
459
	print_result_prov proofs prov fmt;
François Bobot's avatar
François Bobot committed
460 461
      let tr = g.S.goal_transformations in
	if S.PHstr.length tr > 0 then
Asma Tafat's avatar
Asma Tafat committed
462
	  begin
François Bobot's avatar
François Bobot committed
463 464 465 466 467
	    if (S.PHprover.length proofs == 0) then
	      fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
                (List.length prov);
	    S.PHstr.iter (fun _st tr ->
		let goals = tr.S.transf_goals in
Asma Tafat's avatar
Asma Tafat committed
468
		let _ = List.fold_left (fun subgoal g ->
François Bobot's avatar
François Bobot committed
469
		  goal_latex2_stat fmt prov (depth + 1) depth_max (subgoal) g;
Asma Tafat's avatar
Asma Tafat committed
470 471 472 473
				subgoal + 1) 0 goals in
		  () ) tr
	  end
	else
François Bobot's avatar
François Bobot committed
474
	  if (S.PHprover.length proofs) == 0 then
Asma Tafat's avatar
Asma Tafat committed
475 476 477 478 479 480 481 482 483 484 485
	    fprintf fmt "\\\\ @."


let print_head n depth provers fmt =
  if n == 1 then
    if (depth > 1) then
      fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
        depth
    else
      fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
        (depth + 1)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
486
  else
Asma Tafat's avatar
Asma Tafat committed
487
    fprintf fmt "\\hline Proof obligations ";
488
  List.iter (fun a -> fprintf fmt "& \\provername{%a} " C.print_prover a)
François Bobot's avatar
François Bobot committed
489
    provers;
Asma Tafat's avatar
Asma Tafat committed
490
  fprintf fmt "\\\\ @."
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
491

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

Asma Tafat's avatar
Asma Tafat committed
493 494 495 496 497 498 499
let latex_tabular n fmt depth provers t =
fprintf fmt "\\begin{tabular}";
fprintf fmt "{| l |";
  for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
  fprintf fmt "}@.";
  print_head n depth provers fmt;
  if n == 1 then
François Bobot's avatar
François Bobot committed
500
    List.iter (goal_latex_stat fmt provers 0 depth 0) t.S.theory_goals
Asma Tafat's avatar
Asma Tafat committed
501
  else
François Bobot's avatar
François Bobot committed
502
    List.iter (goal_latex2_stat fmt provers 0 depth  0) t.S.theory_goals;
Asma Tafat's avatar
Asma Tafat committed
503 504 505 506 507
  fprintf fmt "\\hline \\end{tabular}@."


let latex_longtable n fmt depth name provers t=
  fprintf fmt "\\begin{longtable}";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
508 509
  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
510
  fprintf fmt "}@.";
511
  (** First head *)
Asma Tafat's avatar
Asma Tafat committed
512
  print_head n depth provers fmt;
Asma Tafat's avatar
Asma Tafat committed
513
  fprintf fmt "\\hline \\endfirsthead @.";
514
  (** Other heads : "Continued... " added *)
François Bobot's avatar
François Bobot committed
515 516
  fprintf fmt "\\multicolumn{%d}{r}{\\textit{Continued from previous page}} \
\\\\ @." (List.length provers + 1) ;
Asma Tafat's avatar
Asma Tafat committed
517
  fprintf fmt "\\hline @.";
Asma Tafat's avatar
Asma Tafat committed
518
  print_head n depth provers fmt;
Asma Tafat's avatar
Asma Tafat committed
519
  fprintf fmt "\\hline \\endhead @.";
520
  (** Other foots : "Continued..." added *)
François Bobot's avatar
François Bobot committed
521 522
  fprintf fmt "\\hline \\multicolumn{%d}{r}{\\textit{Continued on next page}} \
\\\\ @." (List.length provers);
523
  (** Last foot : nothing *)
Asma Tafat's avatar
Asma Tafat committed
524
  fprintf fmt "\\endfoot \\endlastfoot @.";
Asma Tafat's avatar
Asma Tafat committed
525
  if n == 1 then
François Bobot's avatar
François Bobot committed
526
    List.iter (goal_latex_stat fmt provers 0 depth 0) t.S.theory_goals
Asma Tafat's avatar
Asma Tafat committed
527
  else
François Bobot's avatar
François Bobot committed
528
    List.iter (goal_latex2_stat fmt provers 0 depth  0) t.S.theory_goals;
Asma Tafat's avatar
Asma Tafat committed
529 530
  fprintf fmt "\\hline \\caption{%s statistics} @." (protect name);
  fprintf fmt "\\label{%s} \\end{longtable}@." (protect name)
Asma Tafat's avatar
Asma Tafat committed
531

Asma Tafat's avatar
Asma Tafat committed
532 533 534

let theory_latex_stat n table dir t =
  let provers = Hashtbl.create 9 in
François Bobot's avatar
François Bobot committed
535 536
  provers_latex_stats provers t;
  let provers = Hashtbl.fold (fun _ pr acc -> pr :: acc)
Asma Tafat's avatar
Asma Tafat committed
537
    provers [] in
538
  let provers = List.sort C.Prover.compare provers in
Asma Tafat's avatar
Asma Tafat committed
539
  let depth = theory_depth  t in
François Bobot's avatar
François Bobot committed
540
  let name = t.S.theory_name.Ident.id_string in
Asma Tafat's avatar
Asma Tafat committed
541 542 543
  let ch = open_out (Filename.concat dir(name^".tex")) in
  let fmt = formatter_of_out_channel ch in
    if table = "tabular" then
Asma Tafat's avatar
Asma Tafat committed
544
      begin
Asma Tafat's avatar
Asma Tafat committed
545
      latex_tabular n fmt depth provers t
Asma Tafat's avatar
Asma Tafat committed
546
      end
Asma Tafat's avatar
Asma Tafat committed
547
    else
Asma Tafat's avatar
Asma Tafat committed
548 549
      latex_longtable n fmt depth name provers t;
    close_out ch
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
550

Asma Tafat's avatar
Asma Tafat committed
551
let file_latex_stat n table  dir f =
François Bobot's avatar
François Bobot committed
552
   List.iter (theory_latex_stat n table dir) f.S.file_theories
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
553

François Bobot's avatar
François Bobot committed
554 555 556
let print_latex_statistics n table dir session =
  let files = session.S.session_files in
  S.PHstr.iter (fun _ f -> file_latex_stat n table dir f) files
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
557

MARCHE Claude's avatar
MARCHE Claude committed
558
let print_report (g,p,r) =
559
  printf "   goal '%s', prover '%a': " g.Ident.id_string C.print_prover p;
560
  match r with
François Bobot's avatar
François Bobot committed
561 562 563
  | M.Result(new_res,old_res) ->
    (* begin match !opt_smoke with *)
    (*   | Session.SD_None -> *)
564 565
        printf "%a instead of %a@."
          print_result new_res print_result old_res
François Bobot's avatar
François Bobot committed
566 567 568 569 570
    (*   | _ -> *)
    (*     printf "Smoke detected!!!@." *)
    (* end *)
  | M.No_former_result new_res ->
      printf "no former result available : %a@." print_result new_res
571 572 573 574 575
  | M.CallFailed msg ->
      printf "internal failure '%a'@." Exn_printer.exn_printer msg;
  | M.Prover_not_installed ->
      printf "not installed@."

François Bobot's avatar
François Bobot committed
576 577 578 579 580 581 582 583 584 585 586 587

let same_result r1 r2 =
  match r1.Call_provers.pr_answer, r2.Call_provers.pr_answer with
    | Call_provers.Valid, Call_provers.Valid -> true
    | Call_provers.Invalid, Call_provers.Invalid -> true
    | Call_provers.Timeout, Call_provers.Timeout -> true
    | Call_provers.Unknown _, Call_provers.Unknown _-> true
    | Call_provers.Failure _, Call_provers.Failure _-> true
    | _ -> false

let add_to_check_no_smoke found_obs env_session sched =
      let session = env_session.S.session in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
588
      let callback report =
589
        eprintf "@.";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
590
	let files,n,m =
François Bobot's avatar
François Bobot committed
591 592
          S.PHstr.fold file_statistics
            session.S.session_files ([],0,0)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
593
	in
François Bobot's avatar
François Bobot committed
594 595 596 597
        let report = List.filter (function
          | (_,_,M.Result(new_res,old_res)) ->not (same_result new_res old_res)
          | _ -> true) report in
        if report = [] then begin
598 599
            if found_obs then
              if n=m then
François Bobot's avatar
François Bobot committed
600 601
                printf " %d/%d (replay OK, all proved: obsolete session \
updated)@." n m
602
              else
603
                if !opt_force then
François Bobot's avatar
François Bobot committed
604 605
                  printf " %d/%d (replay OK, but not all proved: obsolete \
session updated since -force was given)@." n m
606
                else
François Bobot's avatar
François Bobot committed
607 608
                  printf " %d/%d (replay OK, but not all proved: obsolete \
session NOT updated)@." n m
609 610
            else
              printf " %d/%d@." n m ;
611
            if !opt_stats && n<m then print_statistics files;
612
            eprintf "Everything replayed OK.@.";
613 614
            if (!opt_convert_unknown_provers || found_obs)
              && (n=m || !opt_force) then
615
              begin
616 617 618
                eprintf "Updating %s%ssession...@?"
                (if !opt_convert_unknown_provers then "converted " else "")
                (if found_obs then "obsolete " else "");
François Bobot's avatar
François Bobot committed
619
                S.save_session session;
620 621
                eprintf " done@."
              end;
622
            exit 0
François Bobot's avatar
François Bobot committed
623 624 625
        end
        else
          begin
626
            printf " %d/%d (replay failed)@." n m ;
627
            List.iter print_report report;
628
            eprintf "Replay failed.@.";
629
            exit 1
François Bobot's avatar
François Bobot committed
630
          end
631
    in
François Bobot's avatar
François Bobot committed
632
    M.check_all ~callback env_session sched
633

François Bobot's avatar
François Bobot committed
634
let add_to_check_smoke env_session sched =
635 636
  let callback report =
    eprintf "@.";
François Bobot's avatar
François Bobot committed
637 638 639 640 641 642 643
    let report = List.filter (function
      | (_,_,M.Result({Call_provers.pr_answer = Call_provers.Valid} ,_))
        -> true
      | (_,_,M.No_former_result({Call_provers.pr_answer = Call_provers.Valid}))
        -> true
      | _ -> false) report in
    if report = [] then begin
644 645
        eprintf "No smoke detected.@.";
        exit 0
François Bobot's avatar
François Bobot committed
646 647
    end
    else begin
648 649 650
        List.iter print_report report;
        eprintf "Smoke detected.@.";
        exit 1
François Bobot's avatar
François Bobot committed
651
    end
652
  in
François Bobot's avatar
François Bobot committed
653
  M.check_all ~callback env_session sched
654 655 656

let add_to_check found_obs =
  match !opt_smoke with
François Bobot's avatar
François Bobot committed
657 658 659 660 661 662 663 664 665 666 667
    | SD_None -> add_to_check_no_smoke found_obs;
    | _ -> assert (not found_obs); add_to_check_smoke

let transform_smoke env_session =
  let trans tr_name s =
    Session_tools.filter_proof_attempt S.proof_verified s.S.session;
    Session_tools.transform_proof_attempt ~keygen:O.create s tr_name in
  match !opt_smoke with
    | SD_None -> ()
    | SD_Top -> trans "smoke_detector_top" env_session
    | SD_Deep -> trans "smoke_detector_deep" env_session
668 669 670 671 672


let () =
  try
    eprintf "Opening session...@?";
François Bobot's avatar
François Bobot committed
673
    let env_session,found_obs =
674
      let session = S.read_session project_dir in
François Bobot's avatar
François Bobot committed
675 676
      M.update_session ~allow_obsolete:true session env config in
    transform_smoke env_session;
677
    if !opt_convert_unknown_provers then
678 679
        M.convert_unknown_prover
          ~remove_converted:!opt_remove_converted env_session;
François Bobot's avatar
François Bobot committed
680 681
    let sched =
      M.init (Whyconf.running_provers_max (Whyconf.get_main config)) in
682
    if found_obs then begin
François Bobot's avatar
François Bobot committed
683
      if (* !opt_smoke <> Session.SD_None *) false then begin
684 685 686 687 688 689
        eprintf
          "[Error] I can't run the smoke detector if the session is obsolete";
        exit 1
      end;
      eprintf "[Warning] session is obsolete@.";
    end;
François Bobot's avatar
François Bobot committed
690
    (* M.smoke_detector := !opt_smoke; *)
Asma Tafat's avatar
Asma Tafat committed
691 692
    eprintf " done.";
    if !opt_longtable && !opt_latex == "" && !opt_latex2 == "" then
693
      begin
Asma Tafat's avatar
Asma Tafat committed
694 695 696
	eprintf
	  "[Error] I can't use option longtable without latex ou latex2@.";
	exit 1
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
697
      end;
Asma Tafat's avatar
Asma Tafat committed
698 699 700
    if !opt_latex <> "" then
      if !opt_longtable then
	print_latex_statistics 1 "longtable" !opt_latex
François Bobot's avatar
François Bobot committed
701
            env_session.S.session
Asma Tafat's avatar
Asma Tafat committed
702 703
      else
	print_latex_statistics 1 "tabular" !opt_latex
François Bobot's avatar
François Bobot committed
704
            env_session.S.session
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
705
    else
Asma Tafat's avatar
Asma Tafat committed
706 707 708
      if !opt_latex2 <> "" then
	if !opt_longtable then
	  print_latex_statistics 2 "longtable" !opt_latex2
François Bobot's avatar
François Bobot committed
709
            env_session.S.session
Asma Tafat's avatar
Asma Tafat committed
710
	else
Asma Tafat's avatar
Asma Tafat committed
711
	  print_latex_statistics 2 "tabular" !opt_latex2
François Bobot's avatar
François Bobot committed
712
            env_session.S.session
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
713 714
      else
	begin
François Bobot's avatar
François Bobot committed
715
          add_to_check found_obs env_session sched;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
716 717 718
          try main_loop ()
          with Exit -> eprintf "main replayer exited unexpectedly@."
	end
719
  with
François Bobot's avatar
François Bobot committed
720
    | S.OutdatedSession ->
721
        eprintf "The session database '%s' is outdated, cannot replay@."
722 723 724 725
          project_dir;
        eprintf "Aborting...@.";
        exit 1
    | e when not (Debug.test_flag Debug.stack_trace) ->
726
        eprintf "Error while opening session with database '%s' : %a@."
727 728 729 730
          project_dir
          Exn_printer.exn_printer e;
        eprintf "Aborting...@.";
        exit 1
MARCHE Claude's avatar
MARCHE Claude committed
731 732


733 734 735 736 737
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3replayer.byte"
End:
*)