main.ml 19.1 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
1
2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4
5
6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
7
(*    Andrei Paskevich                                                    *)
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
8
9
10
11
12
13
14
15
16
17
18
19
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Format
21
open Why
22
23
open Util
open Whyconf
24
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
25
open Task
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
26
open Driver
27
open Trans
28

29
30
let usage_msg = sprintf
  "Usage: %s [options] [[file|-] [-T <theory> [-G <goal>]...]...]..."
31
  (Filename.basename Sys.argv.(0))
32

33
34
35
let version_msg = sprintf "Why3 platform, version %s (build date: %s)"
  Config.version Config.builddate

36
let opt_queue = Queue.create ()
37

38
39
let opt_input = ref None
let opt_theory = ref None
40
let opt_trans = ref []
41
let opt_metas = ref []
42
let opt_debug = ref []
43

44
45
let add_opt_file x =
  let tlist = Queue.create () in
46
  Queue.push (Some x, tlist) opt_queue;
47
  opt_input := Some tlist
48

49
50
51
let add_opt_theory =
  let rdot = (Str.regexp "\\.") in fun x ->
  let l = Str.split rdot x in
52
53
54
55
56
57
  let p, t = match List.rev l with
    | t::p -> List.rev p, t
    | _ -> assert false
  in
  match !opt_input, p with
  | None, [] ->
58
      eprintf "Option '-T'/'--theory' with a non-qualified \
59
60
61
62
        argument requires an input file.@.";
      exit 1
  | Some tlist, [] ->
      let glist = Queue.create () in
63
      Queue.push (x, p, t, glist) tlist;
64
65
66
      opt_theory := Some glist
  | _ ->
      let tlist = Queue.create () in
67
      Queue.push (None, tlist) opt_queue;
68
69
      opt_input := None;
      let glist = Queue.create () in
70
      Queue.push (x, p, t, glist) tlist;
71
72
73
74
      opt_theory := Some glist

let add_opt_goal x = match !opt_theory with
  | None ->
75
      eprintf "Option '-G'/'--goal' requires a theory.@.";
76
77
78
      exit 1
  | Some glist ->
      let l = Str.split (Str.regexp "\\.") x in
79
      Queue.push (x, l) glist
80
81

let add_opt_trans x = opt_trans := x::!opt_trans
82

83
84
let add_opt_debug x = opt_debug := x::!opt_debug

85
let add_opt_meta meta =
86
  let meta_name, meta_arg =
87
88
89
    let index = String.index meta '=' in
    (String.sub meta 0 index),
    (String.sub meta (index+1) (String.length meta - (index + 1))) in
90
91
  opt_metas := (meta_name,meta_arg)::!opt_metas

92
let opt_config = ref None
93
let opt_parser = ref None
94
let opt_prover = ref None
95
let opt_coq_realization = ref None
96
let opt_loadpath = ref []
97
98
let opt_driver = ref None
let opt_output = ref None
99
100
let opt_timelimit = ref None
let opt_memlimit = ref None
101
let opt_command = ref None
102
let opt_task = ref None
103
let opt_bisect = ref false
104

105
106
107
let opt_print_libdir = ref false
let opt_print_datadir = ref false

108
109
110
111
let opt_print_theory = ref false
let opt_print_namespace = ref false
let opt_list_transforms = ref false
let opt_list_printers = ref false
112
let opt_list_provers = ref false
113
let opt_list_formats = ref false
114
let opt_list_metas = ref false
115
let opt_list_flags = ref false
116
117
118

let opt_parse_only = ref false
let opt_type_only = ref false
119
let opt_debug_all = ref false
120
let opt_version = ref false
121
122
123
124

let option_list = Arg.align [
  "-", Arg.Unit (fun () -> add_opt_file "-"),
      " Read the input file from stdin";
125
  "-T", Arg.String add_opt_theory,
126
127
      "<theory> Select <theory> in the input file or in the library";
  "--theory", Arg.String add_opt_theory,
128
129
      " same as -T";
  "-G", Arg.String add_opt_goal,
130
131
      "<goal> Select <goal> in the last selected theory";
  "--goal", Arg.String add_opt_goal,
132
      " same as -G";
133
134
135
136
137
  "-C", Arg.String (fun s -> opt_config := Some s),
      "<file> Read configuration from <file>";
  "--config", Arg.String (fun s -> opt_config := Some s),
      " same as -C";
  "-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
138
      "<dir> Add <dir> to the library search path";
139
140
141
142
143
144
145
146
  "--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
      " same as -L";
  "-I", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
      " same as -L (obsolete)";
  "-P", Arg.String (fun s -> opt_prover := Some s),
      "<prover> Prove or print (with -o) the selected goals";
  "--prover", Arg.String (fun s -> opt_prover := Some s),
      " same as -P";
147
  "--coq-realize", Arg.String (fun s -> opt_coq_realization := Some s),
148
149
      " produce, in given file, a Coq realization of the theory given \
        using -T";
150
  "-F", Arg.String (fun s -> opt_parser := Some s),
151
      "<format> Select input format (default: \"why\")";
152
153
  "--format", Arg.String (fun s -> opt_parser := Some s),
      " same as -F";
154
  "-t", Arg.Int (fun i -> opt_timelimit := Some i),
155
156
      "<sec> Set the prover's time limit (default=10, no limit=0)";
  "--timelimit", Arg.Int (fun i -> opt_timelimit := Some i),
157
158
      " same as -t";
  "-m", Arg.Int (fun i -> opt_memlimit := Some i),
159
160
      "<MiB> Set the prover's memory limit (default: no limit)";
  "--memlimit", Arg.Int (fun i -> opt_timelimit := Some i),
161
      " same as -m";
162
163
164
165
  "-a", Arg.String add_opt_trans,
      "<transformation> Apply a transformation to every task";
  "--apply-transform", Arg.String add_opt_trans,
      " same as -a";
166
  "-M", Arg.String add_opt_meta,
167
      "<meta_name>=<string> Add a string meta to every task";
168
169
  "--meta", Arg.String add_opt_meta,
      " same as -M";
170
  "-D", Arg.String (fun s -> opt_driver := Some s),
171
      "<file> Specify a prover's driver (conflicts with -P)";
172
173
174
175
176
177
  "--driver", Arg.String (fun s -> opt_driver := Some s),
      " same as -D";
  "-o", Arg.String (fun s -> opt_output := Some s),
      "<dir> Print the selected goals to separate files in <dir>";
  "--output", Arg.String (fun s -> opt_output := Some s),
      " same as -o";
178
179
180
  "--bisect", Arg.Set opt_bisect,
  " Reduce the set of needed axioms which prove a goal, \
    and output the resulting task";
181
  "--print-theory", Arg.Set opt_print_theory,
182
      " Print selected theories";
183
  "--print-namespace", Arg.Set opt_print_namespace,
184
      " Print namespaces of selected theories";
185
  "--list-transforms", Arg.Set opt_list_transforms,
186
      " List known transformations";
187
  "--list-printers", Arg.Set opt_list_printers,
188
      " List known printers";
189
  "--list-provers", Arg.Set opt_list_provers,
190
      " List known provers";
191
  "--list-formats", Arg.Set opt_list_formats,
192
      " List known input formats";
193
  "--list-metas", Arg.Set opt_list_metas,
194
      " List known metas";
195
196
  "--list-debug-flags", Arg.Set opt_list_flags,
      " List known debug flags";
197
  "--parse-only", Arg.Set opt_parse_only,
198
      " Stop after parsing (same as --debug parse_only)";
199
  "--type-only", Arg.Set opt_type_only,
200
201
      " Stop after type checking (same as --debug type_only)";
  "--debug-all", Arg.Set opt_debug_all,
202
      " Set all debug flags (except parse_only and type_only)";
203
  "--debug", Arg.String add_opt_debug,
204
      "<flag> Set a debug flag";
205
206
207
208
  "--print-libdir", Arg.Set opt_print_libdir,
      " Print location of binary components (plugins, etc)";
  "--print-datadir", Arg.Set opt_print_datadir,
      " Print location of non-binary data (theories, modules, etc)";
209
210
  "--version", Arg.Set opt_version,
      " Print version information" ]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
211

212
let () = try
213
214
  Arg.parse option_list add_opt_file usage_msg;

215
216
217
218
  if !opt_version then begin
    printf "%s@." version_msg;
    exit 0
  end;
219
220
221
222
223
224
225
226
  if !opt_print_libdir then begin
    printf "%s@." Config.libdir;
    exit 0
  end;
  if !opt_print_datadir then begin
    printf "%s@." Config.datadir;
    exit 0
  end;
227

François Bobot's avatar
François Bobot committed
228
229
230
231
232
233
234
235
236
237
238
239
240
  (** Debug flag *)
  if !opt_debug_all then begin
    List.iter (fun (_,f,_) -> Debug.set_flag f) (Debug.list_flags ());
    Debug.unset_flag Typing.debug_parse_only;
    Debug.unset_flag Typing.debug_type_only
  end;

  List.iter (fun s -> Debug.set_flag (Debug.lookup_flag s)) !opt_debug;

  if !opt_parse_only then Debug.set_flag Typing.debug_parse_only;
  if !opt_type_only then Debug.set_flag Typing.debug_type_only;

  (** Configuration *)
241
  let config = read_config !opt_config in
François Bobot's avatar
François Bobot committed
242
243
244
245
246
  let main = get_main config in
  Whyconf.load_plugins main;

  (** listings*)

247
  let opt_list = ref false in
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
248
  if !opt_list_transforms then begin
249
250
    opt_list := true;
    printf "@[<hov 2>Known non-splitting transformations:@\n%a@]@\n@."
251
      (Pp.print_list Pp.newline Pp.string)
252
      (List.sort String.compare (Trans.list_transforms ()));
253
    printf "@[<hov 2>Known splitting transformations:@\n%a@]@\n@."
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
254
      (Pp.print_list Pp.newline Pp.string)
255
      (List.sort String.compare (Trans.list_transforms_l ()))
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
256
  end;
257
  if !opt_list_printers then begin
258
259
    opt_list := true;
    printf "@[<hov 2>Known printers:@\n%a@]@\n@."
260
      (Pp.print_list Pp.newline Pp.string)
261
      (List.sort String.compare (Printer.list_printers ()))
262
263
  end;
  if !opt_list_formats then begin
264
    opt_list := true;
265
    let print1 fmt s = fprintf fmt "%S" s in
266
    let print fmt (p, l) =
267
268
      fprintf fmt "%s [%a]" p (Pp.print_list Pp.comma print1) l
    in
269
    printf "@[<hov 2>Known input formats:@\n%a@]@."
270
271
272
      (Pp.print_list Pp.newline print)
      (List.sort Pervasives.compare (Env.list_formats ()))
  end;
273
  if !opt_list_provers then begin
274
    opt_list := true;
275
276
277
    let config = read_config !opt_config in
    let print fmt s prover = fprintf fmt "%s (%s)@\n" s prover.name in
    let print fmt m = Mstr.iter (print fmt) m in
278
279
    let provers = get_provers config in
    printf "@[<hov 2>Known provers:@\n%a@]@." print provers
280
  end;
281
  if !opt_list_metas then begin
282
    opt_list := true;
283
284
285
    let print fmt m = fprintf fmt "@[%s %s%a@]"
      (let s = m.meta_name in
        if String.contains s ' ' then "\"" ^ s ^ "\"" else s)
François Bobot's avatar
François Bobot committed
286
      (if m.meta_excl then "(flag) " else "")
287
      (Pp.print_list Pp.space Pretty.print_meta_arg_type) m.meta_type
288
    in
289
290
291
    let cmp m1 m2 = Pervasives.compare m1.meta_name m2.meta_name in
    printf "@[<hov 2>Known metas:@\n%a@]@\n@."
      (Pp.print_list Pp.newline print) (List.sort cmp (Theory.list_metas ()))
292
  end;
293
294
295
296
297
298
299
300
  if !opt_list_flags then begin
    opt_list := true;
    let print fmt (p,_,_) = fprintf fmt "%s" p in
    printf "@[<hov 2>Known debug flags:@\n%a@]@."
      (Pp.print_list Pp.newline print)
      (List.sort Pervasives.compare (Debug.list_flags ()))
  end;
  if !opt_list then exit 0;
301
302
303
304
305
306

  if Queue.is_empty opt_queue then begin
    Arg.usage option_list usage_msg;
    exit 1
  end;

307
308
309
  if !opt_prover <> None && !opt_driver <> None then begin
    eprintf "Options '-P'/'--prover' and \
      '-D'/'--driver' cannot be used together.@.";
310
311
    exit 1
  end;
312
313
314
315
316
317
318

  if !opt_prover = None then begin
    if !opt_driver = None && !opt_output <> None then begin
      eprintf "Option '-o'/'--output' requires a prover or a driver.@.";
      exit 1
    end;
    if !opt_timelimit <> None then begin
319
      eprintf "Option '-t'/'--timelimit' requires a prover.@.";
320
321
322
      exit 1
    end;
    if !opt_memlimit <> None then begin
323
      eprintf "Option '-m'/'--memlimit' requires a prover.@.";
324
325
      exit 1
    end;
326
327
328
329
    if !opt_bisect then begin
      eprintf "Option '--bisect' requires a prover.@.";
      exit 1
    end;
330
331
    if !opt_driver = None && not !opt_print_namespace then
      opt_print_theory := true
332
333
  end;

334
335
336
337
338
  if !opt_bisect && !opt_output = None then begin
    eprintf "Option '--bisect' require a directory to output the result.@.";
    exit 1
  end;

339
340
341
  opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main);
  if !opt_timelimit = None then opt_timelimit := Some (Whyconf.timelimit main);
  if !opt_memlimit  = None then opt_memlimit  := Some (Whyconf.memlimit main);
342
  begin match !opt_prover with
343
  | Some s ->
344
      let prover = try Mstr.find s (get_provers config) with
345
        | Not_found -> eprintf "Driver %s not found.@." s; exit 1
346
      in
347
      opt_command := Some prover.command;
348
349
      opt_driver := Some prover.driver
  | None ->
350
351
      ()
  end;
352
  let add_meta task (meta,s) =
353
    let meta = lookup_meta meta in
354
355
    add_meta task meta [MAstr s]
  in
356
  opt_task := List.fold_left add_meta !opt_task !opt_metas
357

358
359
360
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
361
362

let timelimit = match !opt_timelimit with
363
364
365
  | None -> 10
  | Some i when i <= 0 -> 0
  | Some i -> i
366

367
let memlimit = match !opt_memlimit with
368
369
370
371
  | None -> 0
  | Some i when i <= 0 -> 0
  | Some i -> i

372
let print_th_namespace fmt th =
373
  Pretty.print_namespace fmt th.th_name.Ident.id_string th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
374

375
let fname_printer = ref (Ident.create_ident_printer [])
MARCHE Claude's avatar
MARCHE Claude committed
376

377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
let output_task drv fname _tname th task dir =
  let fname = Filename.basename fname in
  let fname =
    try Filename.chop_extension fname with _ -> fname
  in
  let tname = th.th_name.Ident.id_string in
  let dest = Driver.file_of_task drv fname tname task in
  (* Uniquify the filename before the extension if it exists*)
  let i = try String.rindex dest '.' with _ -> String.length dest in
  let name = Ident.string_unique !fname_printer (String.sub dest 0 i) in
  let ext = String.sub dest i (String.length dest - i) in
  let cout = open_out (Filename.concat dir (name ^ ext)) in
  Driver.print_task drv (formatter_of_out_channel cout) task;
  close_out cout


let output_task_prepared drv fname _tname th task dir =
  let fname = Filename.basename fname in
  let fname =
    try Filename.chop_extension fname with _ -> fname
  in
  let tname = th.th_name.Ident.id_string in
  let dest = Driver.file_of_task drv fname tname task in
  (* Uniquify the filename before the extension if it exists*)
  let i = try String.rindex dest '.' with _ -> String.length dest in
  let name = Ident.string_unique !fname_printer (String.sub dest 0 i) in
  let ext = String.sub dest i (String.length dest - i) in
  let cout = open_out (Filename.concat dir (name ^ ext)) in
  Driver.print_task_prepared drv (formatter_of_out_channel cout) task;
  close_out cout


409
let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
410
  match !opt_output, !opt_command with
411
412
413
414
415
416
417
418
419
420
    | Some dir, Some command when !opt_bisect ->
      let test task =
        let call = Driver.prove_task_prepared
          ~command ~timelimit ~memlimit drv task in
        let res = Call_provers.wait_on_call (call ()) () in
        printf "%s %s %s : %a@." fname tname
          (task_goal task).Decl.pr_name.Ident.id_string
          Call_provers.print_prover_result res;
        res.Call_provers.pr_answer = Call_provers.Valid in
      let prepared_task = Driver.prepare_task drv task in
421
422
423
424
425
426
      if not (test prepared_task)
      then printf "I can't bisect %s %s %s which is not valid@." fname tname
        (task_goal task).Decl.pr_name.Ident.id_string
      else
        let prepared_task = Task.bisect test prepared_task in
        output_task_prepared drv fname tname th prepared_task dir
427
    | None, Some command ->
Andrei Paskevich's avatar
Andrei Paskevich committed
428
429
        let call = Driver.prove_task ~command ~timelimit ~memlimit drv task in
        let res = Call_provers.wait_on_call (call ()) () in
430
        printf "%s %s %s : %a@." fname tname
431
          (task_goal task).Decl.pr_name.Ident.id_string
432
433
          Call_provers.print_prover_result res
    | None, None ->
434
        Driver.print_task drv std_formatter task
435
    | Some dir, _ -> output_task drv fname tname th task dir
436

437
let do_tasks env drv fname tname th task =
438
  let lookup acc t =
439
440
    (try Trans.singleton (Trans.lookup_transform t env) with
       Trans.UnknownTrans _ -> Trans.lookup_transform_l t env) :: acc
441
  in
442
  let trans = List.fold_left lookup [] !opt_trans in
443
  let apply tasks tr =
444
    List.rev (List.fold_left (fun acc task ->
445
      List.rev_append (Trans.apply tr task) acc) [] tasks)
446
  in
447
  let tasks = List.fold_left apply [task] trans in
448
  List.iter (do_task drv fname tname th) tasks
449

450
let do_theory env drv fname tname th glist =
451
452
453
454
455
  if !opt_print_theory then
    printf "%a@." Pretty.print_theory th
  else if !opt_print_namespace then
    printf "%a@." print_th_namespace th
  else begin
456
    let add acc (x,l) =
457
458
459
460
      let pr = try ns_find_pr th.th_export l with Not_found ->
        eprintf "Goal '%s' not found in theory '%s'.@." x tname;
        exit 1
      in
461
      Decl.Spr.add pr acc
462
463
    in
    let drv = Util.of_option drv in
464
465
466
467
    let prs = Queue.fold add Decl.Spr.empty glist in
    let sel = if Decl.Spr.is_empty prs then None else Some prs in
    let tasks = List.rev (split_theory th sel !opt_task) in
    List.iter (do_tasks env drv fname tname th) tasks
468
  end
MARCHE Claude's avatar
MARCHE Claude committed
469

470
let do_global_theory env drv (tname,p,t,glist) =
471
472
473
  let th = try Env.find_theory env p t with Env.TheoryNotFound _ ->
    eprintf "Theory '%s' not found.@." tname;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
474
  in
475
  do_theory env drv "lib" tname th glist
MARCHE Claude's avatar
MARCHE Claude committed
476

477
let do_local_theory env drv fname m (tname,_,t,glist) =
478
  let th = try Mstr.find t m with Not_found ->
479
480
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
481
  in
482
  do_theory env drv fname tname th glist
483

484
let do_coq_realize_theory env _drv oldf fname m (tname,_,t,_glist) =
485
  let th = try Mstr.find t m with Not_found ->
MARCHE Claude's avatar
MARCHE Claude committed
486
487
488
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
  in
489
490
491
492
  let old =
    if Sys.file_exists oldf
    then
      begin
493
        let backup = oldf ^ ".bak" in
494
495
496
497
498
499
500
        Sys.rename oldf backup;
        Some(open_in backup)
      end
    else None
  in
  let ch = open_out oldf in
  let fmt = formatter_of_out_channel ch in
501
  Coq.print_theory ?old env [] Ident.Mid.empty fmt th
MARCHE Claude's avatar
MARCHE Claude committed
502

503
let do_input env drv = function
504
  | None, _ when !opt_parse_only || !opt_type_only ->
505
      ()
506
  | None, tlist ->
507
      Queue.iter (do_global_theory env drv) tlist
508
  | Some f, tlist ->
509
510
511
512
      let fname, cin = match f with
        | "-" -> "stdin", stdin
        | f   -> f, open_in f
      in
513
      let m = Env.read_channel ?format:!opt_parser env fname cin in
514
515
516
      close_in cin;
      if !opt_type_only then
        ()
517
      else
518
519
520
521
522
523
524
525
526
527
528
        match !opt_coq_realization with
          | Some f ->
              Queue.iter (do_coq_realize_theory env drv f fname m) tlist
          | None ->
              if Queue.is_empty tlist then
                let glist = Queue.create () in
                let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
                let do_th _ (t,th) = do_theory env drv fname t th glist in
                Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
              else
                Queue.iter (do_local_theory env drv fname m) tlist
MARCHE Claude's avatar
MARCHE Claude committed
529

530
531
let () =
  try
Andrei Paskevich's avatar
Andrei Paskevich committed
532
    let env = Env.create_env_of_loadpath !opt_loadpath in
533
    let drv = Util.option_map (load_driver env) !opt_driver in
534
    Queue.iter (do_input env drv) opt_queue
535
  with e when not (Debug.test_flag Debug.stack_trace) ->
536
    eprintf "%a@." Exn_printer.exn_printer e;
537
    exit 1
538

539
(*
540
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
541
compile-command: "unset LANG; make -C .. byte"
542
End:
543
*)