main.ml 15.7 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
4
5
6
7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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
let opt_queue = Queue.create ()
34

35
36
let opt_input = ref None
let opt_theory = ref None
37
let opt_trans = ref []
38
let opt_metas = ref []
39
let opt_debug = ref []
40

41
42
let add_opt_file x =
  let tlist = Queue.create () in
43
  Queue.push (Some x, tlist) opt_queue;
44
  opt_input := Some tlist
45

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

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

let add_opt_trans x = opt_trans := x::!opt_trans
79

80
81
let add_opt_debug x = opt_debug := x::!opt_debug

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

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

let opt_print_theory = ref false
let opt_print_namespace = ref false
let opt_list_transforms = ref false
let opt_list_printers = ref false
104
let opt_list_provers = ref false
105
let opt_list_formats = ref false
106
let opt_list_metas = ref false
107
let opt_list_flags = ref false
108
109
110

let opt_parse_only = ref false
let opt_type_only = ref false
111
let opt_debug_all = ref false
112
113
114
115

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

191
let () =
192
  try
193
194
  Arg.parse option_list add_opt_file usage_msg;

François Bobot's avatar
François Bobot committed
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
  (** 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*)

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

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

280
281
282
  if !opt_prover <> None && !opt_driver <> None then begin
    eprintf "Options '-P'/'--prover' and \
      '-D'/'--driver' cannot be used together.@.";
283
284
    exit 1
  end;
285
286
287
288
289
290
291

  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
292
      eprintf "Option '-t'/'--timelimit' requires a prover.@.";
293
294
295
      exit 1
    end;
    if !opt_memlimit <> None then begin
296
      eprintf "Option '-m'/'--memlimit' requires a prover.@.";
297
298
299
300
      exit 1
    end;
    if !opt_driver = None && not !opt_print_namespace then
      opt_print_theory := true
301
302
  end;

303
304
305
  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);
306
  begin match !opt_prover with
307
  | Some s ->
308
      let prover = try Mstr.find s (get_provers config) with
309
        | Not_found -> eprintf "Driver %s not found.@." s; exit 1
310
      in
311
      opt_command := Some prover.command;
312
313
      opt_driver := Some prover.driver
  | None ->
314
315
      ()
  end;
316
  let add_meta task (meta,s) =
317
    let meta = lookup_meta meta in
318
319
    add_meta task meta [MAstr s]
  in
320
  opt_task := List.fold_left add_meta !opt_task !opt_metas
321
322
323
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
324
325

let timelimit = match !opt_timelimit with
326
327
328
  | None -> 10
  | Some i when i <= 0 -> 0
  | Some i -> i
329

330
let memlimit = match !opt_memlimit with
331
332
333
334
  | None -> 0
  | Some i when i <= 0 -> 0
  | Some i -> i

335
let print_th_namespace fmt th =
336
  Pretty.print_namespace fmt th.th_name.Ident.id_string th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
337

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

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

366
let do_tasks env drv fname tname th task =
367
  let lookup acc t =
368
369
    (try t, Trans.singleton (Trans.lookup_transform t env) with
       Trans.UnknownTrans _ -> t, Trans.lookup_transform_l t env) :: acc
370
  in
371
  let trans = List.fold_left lookup [] !opt_trans in
372
  let apply tasks (s, tr) =
373
374
    List.rev (List.fold_left (fun acc task ->
      List.rev_append (Trans.apply_named s tr task) acc) [] tasks)
375
  in
376
  let tasks = List.fold_left apply [task] trans in
377
  List.iter (do_task drv fname tname th) tasks
378

379
let do_theory env drv fname tname th glist =
380
381
382
383
384
  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
385
    let add acc (x,l) =
386
387
388
389
      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
390
      Decl.Spr.add pr acc
391
392
    in
    let drv = Util.of_option drv in
393
394
395
396
    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
397
  end
MARCHE Claude's avatar
MARCHE Claude committed
398

399
let do_global_theory env drv (tname,p,t,glist) =
400
401
402
  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
403
  in
404
  do_theory env drv "lib" tname th glist
MARCHE Claude's avatar
MARCHE Claude committed
405

406
let do_local_theory env drv fname m (tname,_,t,glist) =
407
408
409
  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
410
  in
411
  do_theory env drv fname tname th glist
412
413

let do_input env drv = function
414
  | None, _ when !opt_parse_only || !opt_type_only ->
415
      ()
416
  | None, tlist ->
417
      Queue.iter (do_global_theory env drv) tlist
418
  | Some f, tlist ->
419
420
421
422
      let fname, cin = match f with
        | "-" -> "stdin", stdin
        | f   -> f, open_in f
      in
423
      let m = Env.read_channel ?format:!opt_parser env fname cin in
424
425
426
427
428
429
      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
430
        let do_th _ (t,th) = do_theory env drv fname t th glist in
431
432
433
        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
434

435
436
let () =
  try
437
    let env = Env.create_env (Lexer.retrieve !opt_loadpath) in
438
    let drv = Util.option_map (load_driver env) !opt_driver in
439
    Queue.iter (do_input env drv) opt_queue
440
  with e when not (Debug.test_flag Debug.stack_trace) ->
441
    eprintf "%a@." Exn_printer.exn_printer e;
442
    exit 1
443

444
(*
445
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
446
compile-command: "unset LANG; make -C .. byte"
447
End:
448
*)