main.ml 16 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
1
2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
3
(*  Copyright (C) 2010-                                                   *)
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_loadpath = ref []
96
97
let opt_driver = ref None
let opt_output = ref None
98
99
let opt_timelimit = ref None
let opt_memlimit = ref None
100
let opt_command = ref None
101
let opt_task = ref None
102
103
104
105
106

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

let opt_parse_only = ref false
let opt_type_only = ref false
114
let opt_debug_all = ref false
115
let opt_version = ref false
116
117
118
119

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

197
let () =
198
  try
199
200
  Arg.parse option_list add_opt_file usage_msg;

François Bobot's avatar
François Bobot committed
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
  (** 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 *)
  let config = try read_config !opt_config with Not_found ->
    option_iter (eprintf "Config file '%s' not found.@.") !opt_config;
    option_iter
      (eprintf "No config file found (required by '-P %s').@.") !opt_prover;
    exit 1;
  in

  let main = get_main config in
  Whyconf.load_plugins main;

  (** listings*)

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

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

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

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

313
314
315
  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);
316
  begin match !opt_prover with
317
  | Some s ->
318
      let prover = try Mstr.find s (get_provers config) with
319
        | Not_found -> eprintf "Driver %s not found.@." s; exit 1
320
      in
321
      opt_command := Some prover.command;
322
323
      opt_driver := Some prover.driver
  | None ->
324
325
      ()
  end;
326
  let add_meta task (meta,s) =
327
    let meta = lookup_meta meta in
328
329
    add_meta task meta [MAstr s]
  in
330
  opt_task := List.fold_left add_meta !opt_task !opt_metas
331
332
333
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
334
335

let timelimit = match !opt_timelimit with
336
337
338
  | None -> 10
  | Some i when i <= 0 -> 0
  | Some i -> i
339

340
let memlimit = match !opt_memlimit with
341
342
343
344
  | None -> 0
  | Some i when i <= 0 -> 0
  | Some i -> i

345
let print_th_namespace fmt th =
346
  Pretty.print_namespace fmt th.th_name.Ident.id_string th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
347

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

350
let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
351
352
  match !opt_output, !opt_command with
    | None, Some command ->
353
        let res =
354
          Driver.prove_task ~command ~timelimit ~memlimit drv task () ()
355
        in
356
        printf "%s %s %s : %a@." fname tname
357
          (task_goal task).Decl.pr_name.Ident.id_string
358
359
          Call_provers.print_prover_result res
    | None, None ->
360
        Driver.print_task drv std_formatter task
361
    | Some dir, _ ->
362
363
364
365
        let fname = Filename.basename fname in
        let fname =
          try Filename.chop_extension fname with _ -> fname
        in
366
        let tname = th.th_name.Ident.id_string in
367
        let dest = Driver.file_of_task drv fname tname task in
368
369
370
371
372
        (* 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
373
        Driver.print_task drv (formatter_of_out_channel cout) task;
374
375
        close_out cout

376
let do_tasks env drv fname tname th task =
377
  let lookup acc t =
378
379
    (try t, Trans.singleton (Trans.lookup_transform t env) with
       Trans.UnknownTrans _ -> t, Trans.lookup_transform_l t env) :: acc
380
  in
381
  let trans = List.fold_left lookup [] !opt_trans in
382
  let apply tasks (s, tr) =
383
384
    List.rev (List.fold_left (fun acc task ->
      List.rev_append (Trans.apply_named s tr task) acc) [] tasks)
385
  in
386
  let tasks = List.fold_left apply [task] trans in
387
  List.iter (do_task drv fname tname th) tasks
388

389
let do_theory env drv fname tname th glist =
390
391
392
393
394
  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
395
    let add acc (x,l) =
396
397
398
399
      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
400
      Decl.Spr.add pr acc
401
402
    in
    let drv = Util.of_option drv in
403
404
405
406
    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
407
  end
MARCHE Claude's avatar
MARCHE Claude committed
408

409
let do_global_theory env drv (tname,p,t,glist) =
410
411
412
  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
413
  in
414
  do_theory env drv "lib" tname th glist
MARCHE Claude's avatar
MARCHE Claude committed
415

416
let do_local_theory env drv fname m (tname,_,t,glist) =
417
418
419
  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
420
  in
421
  do_theory env drv fname tname th glist
422
423

let do_input env drv = function
424
  | None, _ when !opt_parse_only || !opt_type_only ->
425
      ()
426
  | None, tlist ->
427
      Queue.iter (do_global_theory env drv) tlist
428
  | Some f, tlist ->
429
430
431
432
      let fname, cin = match f with
        | "-" -> "stdin", stdin
        | f   -> f, open_in f
      in
433
      let m = Env.read_channel ?format:!opt_parser env fname cin in
434
435
436
437
438
439
      close_in cin;
      if !opt_type_only then
        ()
      else 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
440
        let do_th _ (t,th) = do_theory env drv fname t th glist in
441
442
443
        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
444

445
446
let () =
  try
447
    let env = Env.create_env (Lexer.retrieve !opt_loadpath) in
448
    let drv = Util.option_map (load_driver env) !opt_driver in
449
    Queue.iter (do_input env drv) opt_queue
450
  with e when not (Debug.test_flag Debug.stack_trace) ->
451
    eprintf "%a@." Exn_printer.exn_printer e;
452
    exit 1
453

454
(*
455
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
456
compile-command: "unset LANG; make -C .. byte"
457
End:
458
*)