main.ml 18.5 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
1
2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
MARCHE Claude's avatar
MARCHE Claude committed
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
108

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

let opt_parse_only = ref false
let opt_type_only = ref false
116
let opt_debug_all = ref false
117
let opt_version = ref false
118
119
120
121

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

205
let () =
206
  try
207
208
  Arg.parse option_list add_opt_file usage_msg;

209
210
211
212
213
  if !opt_version then begin
    printf "%s@." version_msg;
    exit 0
  end;

François Bobot's avatar
François Bobot committed
214
215
216
217
218
219
220
221
222
223
224
225
226
  (** 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 *)
227
  let config = read_config !opt_config in
François Bobot's avatar
François Bobot committed
228
229
230
231
232
  let main = get_main config in
  Whyconf.load_plugins main;

  (** listings*)

233
  let opt_list = ref false in
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
234
  if !opt_list_transforms then begin
235
236
    opt_list := true;
    printf "@[<hov 2>Known non-splitting transformations:@\n%a@]@\n@."
237
      (Pp.print_list Pp.newline Pp.string)
238
      (List.sort String.compare (Trans.list_transforms ()));
239
    printf "@[<hov 2>Known splitting transformations:@\n%a@]@\n@."
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
240
      (Pp.print_list Pp.newline Pp.string)
241
      (List.sort String.compare (Trans.list_transforms_l ()))
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
242
  end;
243
  if !opt_list_printers then begin
244
245
    opt_list := true;
    printf "@[<hov 2>Known printers:@\n%a@]@\n@."
246
      (Pp.print_list Pp.newline Pp.string)
247
      (List.sort String.compare (Printer.list_printers ()))
248
249
  end;
  if !opt_list_formats then begin
250
    opt_list := true;
251
    let print1 fmt s = fprintf fmt "%S" s in
252
    let print fmt (p, l) =
253
254
      fprintf fmt "%s [%a]" p (Pp.print_list Pp.comma print1) l
    in
255
    printf "@[<hov 2>Known input formats:@\n%a@]@."
256
257
258
      (Pp.print_list Pp.newline print)
      (List.sort Pervasives.compare (Env.list_formats ()))
  end;
259
  if !opt_list_provers then begin
260
    opt_list := true;
261
262
263
    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
264
265
    let provers = get_provers config in
    printf "@[<hov 2>Known provers:@\n%a@]@." print provers
266
  end;
267
  if !opt_list_metas then begin
268
    opt_list := true;
269
270
271
    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
272
      (if m.meta_excl then "(flag) " else "")
273
      (Pp.print_list Pp.space Pretty.print_meta_arg_type) m.meta_type
274
    in
275
276
277
    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 ()))
278
  end;
279
280
281
282
283
284
285
286
  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;
287
288
289
290
291
292

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

293
294
295
  if !opt_prover <> None && !opt_driver <> None then begin
    eprintf "Options '-P'/'--prover' and \
      '-D'/'--driver' cannot be used together.@.";
296
297
    exit 1
  end;
298
299
300
301
302
303
304

  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
305
      eprintf "Option '-t'/'--timelimit' requires a prover.@.";
306
307
308
      exit 1
    end;
    if !opt_memlimit <> None then begin
309
      eprintf "Option '-m'/'--memlimit' requires a prover.@.";
310
311
      exit 1
    end;
312
313
314
315
    if !opt_bisect then begin
      eprintf "Option '--bisect' requires a prover.@.";
      exit 1
    end;
316
317
    if !opt_driver = None && not !opt_print_namespace then
      opt_print_theory := true
318
319
  end;

320
321
322
323
324
325
  if !opt_bisect && !opt_output = None then begin
    eprintf "Option '--bisect' require a directory to output the result.@.";
    exit 1
  end;


326
327
328
  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);
329
  begin match !opt_prover with
330
  | Some s ->
331
      let prover = try Mstr.find s (get_provers config) with
332
        | Not_found -> eprintf "Driver %s not found.@." s; exit 1
333
      in
334
      opt_command := Some prover.command;
335
336
      opt_driver := Some prover.driver
  | None ->
337
338
      ()
  end;
339
  let add_meta task (meta,s) =
340
    let meta = lookup_meta meta in
341
342
    add_meta task meta [MAstr s]
  in
343
  opt_task := List.fold_left add_meta !opt_task !opt_metas
344
345
346
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
347
348

let timelimit = match !opt_timelimit with
349
350
351
  | None -> 10
  | Some i when i <= 0 -> 0
  | Some i -> i
352

353
let memlimit = match !opt_memlimit with
354
355
356
357
  | None -> 0
  | Some i when i <= 0 -> 0
  | Some i -> i

358
let print_th_namespace fmt th =
359
  Pretty.print_namespace fmt th.th_name.Ident.id_string th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
360

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

363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
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


395
let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
396
  match !opt_output, !opt_command with
397
398
399
400
401
402
403
404
405
406
    | 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
407
408
409
410
411
412
      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
413
    | None, Some command ->
Andrei Paskevich's avatar
Andrei Paskevich committed
414
415
        let call = Driver.prove_task ~command ~timelimit ~memlimit drv task in
        let res = Call_provers.wait_on_call (call ()) () in
416
        printf "%s %s %s : %a@." fname tname
417
          (task_goal task).Decl.pr_name.Ident.id_string
418
419
          Call_provers.print_prover_result res
    | None, None ->
420
        Driver.print_task drv std_formatter task
421
    | Some dir, _ -> output_task drv fname tname th task dir
422

423
let do_tasks env drv fname tname th task =
424
  let lookup acc t =
425
426
    (try Trans.singleton (Trans.lookup_transform t env) with
       Trans.UnknownTrans _ -> Trans.lookup_transform_l t env) :: acc
427
  in
428
  let trans = List.fold_left lookup [] !opt_trans in
429
  let apply tasks tr =
430
    List.rev (List.fold_left (fun acc task ->
431
      List.rev_append (Trans.apply tr task) acc) [] tasks)
432
  in
433
  let tasks = List.fold_left apply [task] trans in
434
  List.iter (do_task drv fname tname th) tasks
435

436
let do_theory env drv fname tname th glist =
437
438
439
440
441
  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
442
    let add acc (x,l) =
443
444
445
446
      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
447
      Decl.Spr.add pr acc
448
449
    in
    let drv = Util.of_option drv in
450
451
452
453
    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
454
  end
MARCHE Claude's avatar
MARCHE Claude committed
455

456
let do_global_theory env drv (tname,p,t,glist) =
457
458
459
  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
460
  in
461
  do_theory env drv "lib" tname th glist
MARCHE Claude's avatar
MARCHE Claude committed
462

463
let do_local_theory env drv fname m (tname,_,t,glist) =
464
465
466
  let th = try Mnm.find t m with Not_found ->
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
467
  in
468
  do_theory env drv fname tname th glist
469

470
let do_coq_realize_theory env _drv oldf fname m (tname,_,t,_glist) =
MARCHE Claude's avatar
MARCHE Claude committed
471
472
473
474
  let th = try Mnm.find t m with Not_found ->
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
  in
475
476
477
478
479
480
481
482
483
484
485
486
487
  let old =
    if Sys.file_exists oldf
    then
      begin
	let backup = oldf ^ ".bak" in
        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
  Coq.print_theory ~old env [] Ident.Mid.empty fmt th
MARCHE Claude's avatar
MARCHE Claude committed
488

489
let do_input env drv = function
490
  | None, _ when !opt_parse_only || !opt_type_only ->
491
      ()
492
  | None, tlist ->
493
      Queue.iter (do_global_theory env drv) tlist
494
  | Some f, tlist ->
495
496
497
498
      let fname, cin = match f with
        | "-" -> "stdin", stdin
        | f   -> f, open_in f
      in
499
      let m = Env.read_channel ?format:!opt_parser env fname cin in
500
501
502
      close_in cin;
      if !opt_type_only then
        ()
503
504
505
506
507
508
509
510
511
512
513
514
      else 
	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 (Mnm.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
515

516
517
let () =
  try
518
    let env = Lexer.create_env !opt_loadpath in
519
    let drv = Util.option_map (load_driver env) !opt_driver in
520
    Queue.iter (do_input env drv) opt_queue
521
  with e when not (Debug.test_flag Debug.stack_trace) ->
522
    eprintf "%a@." Exn_printer.exn_printer e;
523
    exit 1
524

525
(*
526
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
527
compile-command: "unset LANG; make -C .. byte"
528
End:
529
*)