why3replay.ml 12.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
11

François Bobot's avatar
François Bobot committed
12
open Format
13
open Why3
14 15 16 17 18 19 20 21 22 23 24 25 26 27

(** {2 Warnings} *)

(* warnings are shown on standard output instead of standard error:
   they are not an error but should be present in the reporting of the
   replay *)

let display_warning ?loc msg =
  match loc with
    | None -> printf "%s@." msg
    | Some l -> printf "%a: %s@." Loc.gen_report_position l msg

let () = Warning.set_hook display_warning

28 29 30 31 32 33
let debug = Debug.register_info_flag
    ~desc:"of@ the@ progression@ of@ a@ replay"
    "replay"

let () = Debug.set_flag debug

34
let opt_file = ref None
35
(*
36
let opt_stats = ref true
37
*)
38
let opt_force = ref false
39
let opt_obsolete_only = ref false
40
let opt_use_steps = ref false
41
(*
42
let opt_bench = ref false
43
*)
44
let opt_provers = ref []
45 46 47



François Bobot's avatar
François Bobot committed
48 49
(** {2 Smoke detector} *)

50
(*
François Bobot's avatar
François Bobot committed
51 52 53 54 55 56 57 58
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
59 60

let set_opt_smoke = function
François Bobot's avatar
François Bobot committed
61 62 63
  | "none" -> opt_smoke := SD_None
  | "top" ->  opt_smoke := SD_Top
  | "deep" ->  opt_smoke := SD_Deep
64
  | _ -> assert false
65
 *)
MARCHE Claude's avatar
MARCHE Claude committed
66

67
let usage_msg = Format.sprintf
68
  "Usage: %s [options] [<file.why>|<project directory>]"
69 70 71
  (Filename.basename Sys.argv.(0))

let option_list = [
Andrei Paskevich's avatar
Andrei Paskevich committed
72 73 74
  ("-f",
   Arg.Set opt_force,
   " enforce saving the session after replay");
75
  ("--force",
76
   Arg.Set opt_force,
Andrei Paskevich's avatar
Andrei Paskevich committed
77
   " same as -f");
78 79 80
  ("--use-steps",
   Arg.Set opt_use_steps,
   " replay using recorded number of proof steps (when possible)");
81
  ("--obsolete-only",
82 83
   Arg.Set opt_obsolete_only,
   " replay only if session is obsolete") ;
Andrei Paskevich's avatar
Andrei Paskevich committed
84 85 86 87 88 89 90 91
  ("-P",
   Arg.String (fun s ->
     opt_provers := Whyconf.parse_filter_prover s :: !opt_provers),
   "<prover> restrict replay to given prover");
  ("--prover",
   Arg.String (fun s ->
     opt_provers := Whyconf.parse_filter_prover s :: !opt_provers),
   " same as -P");
92
(*
93
  ("--smoke-detector",
94 95
   Arg.Symbol (["none";"top";"deep"],set_opt_smoke),
   " try to detect if the context is self-contradicting") ;
96
  ("--bench",
97
   Arg.Set opt_bench, " run as bench (experimental)");
Andrei Paskevich's avatar
Andrei Paskevich committed
98
  ("--no-stats",
99 100
   Arg.Clear opt_stats,
   " do not print statistics") ;
101
*)
102
  ("-q",
103
   Arg.Unit (fun () -> Debug.unset_flag debug),
Andrei Paskevich's avatar
Andrei Paskevich committed
104 105 106 107
   " run quietly");
  ("--quiet",
   Arg.Unit (fun () -> Debug.unset_flag debug),
   " same as -q") ]
MARCHE Claude's avatar
MARCHE Claude committed
108

109
let add_opt_file f = match !opt_file with
MARCHE Claude's avatar
MARCHE Claude committed
110 111 112
  | Some _ ->
      raise (Arg.Bad "only one parameter")
  | None ->
113
      opt_file := Some f
MARCHE Claude's avatar
MARCHE Claude committed
114

115
let config, _, env =
Andrei Paskevich's avatar
Andrei Paskevich committed
116
  Whyconf.Args.initialize option_list add_opt_file usage_msg
117

118 119
let fname =
  match !opt_file with
Andrei Paskevich's avatar
Andrei Paskevich committed
120
  | None -> Whyconf.Args.exit_with_usage option_list usage_msg
121
  | Some f -> f
122

123 124
let found_upgraded_prover = ref false

125
module C = Controller_itp.Make(Unix_scheduler.Unix_scheduler)
MARCHE Claude's avatar
MARCHE Claude committed
126

127 128 129 130 131 132
let () =
  C.set_max_tasks (Whyconf.running_provers_max (Whyconf.get_main config));
  C.register_observer
    (fun w s r ->
      if Debug.test_flag debug then
        Printf.eprintf "Progress: %d/%d/%d                       \r%!" w s r)
François Bobot's avatar
François Bobot committed
133

134
let print_result = Call_provers.print_prover_result
MARCHE Claude's avatar
MARCHE Claude committed
135

136
module S = Session_itp
MARCHE Claude's avatar
MARCHE Claude committed
137 138

let project_dir =
139 140 141
  try
    Session.get_project_dir fname
  with Not_found -> failwith "file does not exist"
MARCHE Claude's avatar
MARCHE Claude committed
142

143 144
let goal_statistics cont (goals,n,m) g =
  if Controller_itp.pn_proved cont g then (goals,n+1,m+1) else (g::goals,n,m+1)
145

146
let theory_statistics cont (ths,n,m) th =
François Bobot's avatar
François Bobot committed
147
  let goals,n1,m1 =
148
    List.fold_left (goal_statistics cont) ([],0,0) (Session_itp.theory_goals th) in
149
  ((th,goals,n1,m1)::ths,n+n1,m+m1)
150

151
let file_statistics cont _ f (files,n,m) =
François Bobot's avatar
François Bobot committed
152
  let ths,n1,m1 =
153
    List.fold_left (theory_statistics cont) ([],0,0) f.Session_itp.file_theories in
154
  ((f,ths,n1,m1)::files,n+n1,m+m1)
155

156
let print_statistics cont files =
François Bobot's avatar
François Bobot committed
157
  let print_goal g =
158 159
    printf "         +--goal %s not proved@."
           (Session_itp.get_proof_name cont.Controller_itp.controller_session g).Ident.id_string
François Bobot's avatar
François Bobot committed
160 161 162
  in
  let print_theory (th,goals,n,m) =
    if n<m then begin
François Bobot's avatar
François Bobot committed
163
      printf "      +--theory %s: %d/%d@."
164
        (Session_itp.theory_name th).Ident.id_string n m;
François Bobot's avatar
François Bobot committed
165 166 167 168 169
      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
170
      printf "   +--file %s: %d/%d@." f.S.file_name n m;
François Bobot's avatar
François Bobot committed
171 172 173 174
      List.iter print_theory (List.rev ths)
    end
  in
  List.iter print_file (List.rev files)
MARCHE Claude's avatar
MARCHE Claude committed
175

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

177 178
let print_report ses (id,p,l,r) =
  let g = S.get_proof_name ses id in
179
  printf "   goal '%s', prover '%a': " g.Ident.id_string Whyconf.print_prover p;
180
  match r with
181
  | C.Result(new_res,old_res) ->
182
        printf "%a instead of %a (timelimit=%d, memlimit=%d, steplimit=%d)@."
183 184 185 186
          print_result new_res print_result old_res
          l.Call_provers.limit_time
          l.Call_provers.limit_mem
          l.Call_provers.limit_steps
187
  | C.No_former_result new_res ->
188 189
      printf "no former result available, new result is: %a@."
        print_result new_res
190
  | C.CallFailed msg ->
191
      printf "internal failure '%a'@." Exn_printer.exn_printer msg;
192 193 194
  | C.Replay_interrupted ->
      printf "replay interrupted@."
  | C.Edited_file_absent f ->
195
      printf "proof script absent (%s)@." f
196 197
  | C.Prover_not_installed ->
     printf "not installed@."
198

François Bobot's avatar
François Bobot committed
199 200 201 202 203 204

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
205
    | Call_provers.OutOfMemory, Call_provers.OutOfMemory -> true
François Bobot's avatar
François Bobot committed
206 207 208 209
    | Call_provers.Unknown _, Call_provers.Unknown _-> true
    | Call_provers.Failure _, Call_provers.Failure _-> true
    | _ -> false

210 211 212
let add_to_check_no_smoke some_merge_miss found_obs cont =
  let session = cont.Controller_itp.controller_session in
  let final_callback report =
213
    Debug.dprintf debug "@.";
214
    let files,n,m =
215 216
      Stdlib.Hstr.fold (file_statistics cont)
        (S.get_files session) ([],0,0)
217 218 219 220
    in
    let report =
      List.filter
        (function
221
          | (_,_,_,C.Result(new_res,old_res)) ->
222 223 224 225
            not (same_result new_res old_res)
          | _ -> true)
        report
    in
226
    let save () =
227
      Debug.dprintf debug "Saving session...@?";
228
      S.save_session session;
229
      Debug.dprintf debug " done@." in
230
    printf " %d/%d " n m;
231
    if report = [] && not some_merge_miss then
232
      begin
233 234 235
        printf "(replay OK%s%s)@."
          (if found_obs then ", obsolete session" else "")
          (if !found_upgraded_prover then ", upgraded prover" else "");
236
        if true (* !opt_stats *) && n<m then print_statistics cont files;
237
        Debug.dprintf debug "Everything replayed OK.@.";
238
        if !opt_force || found_obs || !found_upgraded_prover then save ();
239 240 241 242 243
        exit 0
      end
    else
      let report = List.rev report in
      begin
244 245
        printf "(replay failed%s)@."
          (if some_merge_miss then ", with some merge miss" else "");
246
        List.iter (print_report cont.Controller_itp.controller_session) report;
247
        eprintf "Replay failed.@.";
248
        if !opt_force then save ();
249 250 251
        exit 1
      end
  in
252 253
  let callback _paid _pastatus = () in
  let notification _any _bool = () in
254
  if !opt_provers = [] then
255 256 257
    let () =
      C.replay ~obsolete_only:false ~use_steps:!opt_use_steps ~callback ~notification ~final_callback cont
    in ()
258
  else
259 260
    failwith "option -P not yet supported"
(*
261 262 263 264
    let filter a =
      List.exists
        (fun p -> Whyconf.filter_prover p a.Session.proof_prover)
        !opt_provers in
265 266
    M.check_all ~release:true ~use_steps:!opt_use_steps
      ~filter ~callback env_session sched
267 268 269
 *)

(*
270

François Bobot's avatar
François Bobot committed
271
let add_to_check_smoke env_session sched =
272
  let callback report =
273
    Debug.dprintf debug "@.";
274 275 276 277 278 279 280 281 282
    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
François Bobot's avatar
François Bobot committed
283
    if report = [] then begin
284
      Debug.dprintf debug "No smoke detected.@.";
285
      exit 0
François Bobot's avatar
François Bobot committed
286 287
    end
    else begin
288 289 290
      List.iter print_report report;
      eprintf "Smoke detected.@.";
      exit 1
François Bobot's avatar
François Bobot committed
291
    end
292
  in
293 294
  M.check_all ~release:true ~use_steps:!opt_use_steps
    ~callback env_session sched
295

296
let add_to_check config some_merge_miss found_obs =
297
  match !opt_smoke with
298
    | SD_None -> add_to_check_no_smoke config some_merge_miss found_obs;
Andrei Paskevich's avatar
Andrei Paskevich committed
299
    | _ ->
300
      assert (not some_merge_miss);
Andrei Paskevich's avatar
Andrei Paskevich committed
301
      assert (not found_obs);
302
      add_to_check_smoke
François Bobot's avatar
François Bobot committed
303 304 305

let transform_smoke env_session =
  let trans tr_name s =
306
    Session_tools.filter_proof_attempt
307 308 309
      (fun p -> Opt.inhabited (S.proof_verified p)) s.S.session;
    Session_tools.transform_proof_attempt ~keygen:O.create s tr_name
  in
François Bobot's avatar
François Bobot committed
310 311 312 313
  match !opt_smoke with
    | SD_None -> ()
    | SD_Top -> trans "smoke_detector_top" env_session
    | SD_Deep -> trans "smoke_detector_deep" env_session
314
 *)
315 316


317
(*
318 319 320 321
let run_as_bench env_session =
  let sched =
    M.init (Whyconf.running_provers_max (Whyconf.get_main config))
  in
322
  eprintf "Provers:@ ";
323
  let provers =
324
    Whyconf.Mprover.fold
325
      (fun _ p acc ->
326 327 328 329 330
        if p.Whyconf.interactive then acc else
          begin
            eprintf "%a@ " Whyconf.print_prover p.Whyconf.prover;
            p.Whyconf.prover :: acc
          end)
331
      (Whyconf.get_provers env_session.Session.whyconf) []
332
  in
333
  eprintf "@.";
334
  let callback () =
335 336 337
    eprintf "Saving session...@?";
    Session.save_session config env_session.Session.session;
    eprintf " done.@.";
338 339
    exit 0
  in
340
  let limit = { Call_provers.empty_limit with Call_provers.limit_time = 2} in
341
  M.play_all env_session sched ~callback ~limit provers;
342 343
  main_loop ();
  eprintf "main replayer (in bench mode) exited unexpectedly@.";
344
  exit 1
345
 *)
346

347

348 349
let () =
  try
350
    Debug.dprintf debug "Opening session...@?";
351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374
    let cont = Controller_itp.create_controller env in
    let provers = Whyconf.get_provers config in
    Whyconf.Mprover.iter
      (fun _ p ->
       try
         let d = Driver.load_driver cont.Controller_itp.controller_env p.Whyconf.driver [] in
         Whyconf.Hprover.add cont.Controller_itp.controller_provers p.Whyconf.prover (p,d)
       with e ->
         Format.eprintf
           "error loading driver for prover %a: %a@."
           Whyconf.print_prover p.Whyconf.prover
           Exn_printer.exn_printer e)
      provers;
    let ses,use_shapes = S.load_session project_dir in
    Controller_itp.init_controller ses cont;
    (* update the session *)
    let found_obs, some_merge_miss =
      try
        Controller_itp.reload_files cont ~use_shapes;
        true, false (* TODO *)
      with
      | e ->
         Format.eprintf "%a@." Exn_printer.exn_printer e;
         exit 1
375
    in
376
    Debug.dprintf debug " done.@.";
Andrei Paskevich's avatar
Andrei Paskevich committed
377
    if !opt_obsolete_only && not found_obs
378
    then
379
      begin
380
        eprintf "Session is not obsolete, hence not replayed@.";
381 382 383
        printf "@.";
        exit 0
      end;
384
(*
385
    if !opt_bench then run_as_bench env_session;
386
    let () = transform_smoke env_session in
François Bobot's avatar
François Bobot committed
387
    let sched =
388 389
      M.init (Whyconf.running_provers_max (Whyconf.get_main config))
    in
390
 *)
391
    if found_obs then eprintf "[Warning] session is obsolete@.";
392
    if some_merge_miss then eprintf "[Warning] some goals were missed during merge@.";
393
    add_to_check_no_smoke some_merge_miss found_obs cont;
394
    Unix_scheduler.Unix_scheduler.main_loop ~prompt:"" (fun _ -> ());
395
    eprintf "main replayer loop exited unexpectedly@.";
396
    exit 1
397 398
  with
    | e when not (Debug.test_flag Debug.stack_trace) ->
399 400 401 402 403
      eprintf "Error while opening session with database '%s' : %a@."
        project_dir
        Exn_printer.exn_printer e;
      eprintf "Aborting...@.";
      exit 1
MARCHE Claude's avatar
MARCHE Claude committed
404 405


406 407
(*
Local Variables:
408
compile-command: "unset LANG; make -C ../.. bin/why3newreplay.byte"
409 410
End:
*)