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 [Filename.concat Whyconf.datadir "theories"]
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
187
188
189
      " Stop after type checking (same as --debug type_only)";
  "--debug-all", Arg.Set opt_debug_all,
      " Set every known debug flag";
  "--debug", Arg.String add_opt_debug,
      "<flag> Set a debug flag" ]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
190

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

194
  (* TODO? : Since drivers can dynlink ml code they can add printer,
195
     transformations, ... So drivers should be loaded before listing *)
196
  let opt_list = ref false in
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
197
  if !opt_list_transforms then begin
198
199
    opt_list := true;
    printf "@[<hov 2>Known non-splitting transformations:@\n%a@]@\n@."
200
      (Pp.print_list Pp.newline Pp.string)
201
      (List.sort String.compare (Trans.list_transforms ()));
202
    printf "@[<hov 2>Known splitting transformations:@\n%a@]@\n@."
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
203
      (Pp.print_list Pp.newline Pp.string)
204
      (List.sort String.compare (Trans.list_transforms_l ()));
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
205
  end;
206
  if !opt_list_printers then begin
207
208
    opt_list := true;
    printf "@[<hov 2>Known printers:@\n%a@]@\n@."
209
      (Pp.print_list Pp.newline Pp.string)
210
      (List.sort String.compare (Printer.list_printers ()))
211
212
  end;
  if !opt_list_formats then begin
213
    opt_list := true;
214
    let print1 fmt s = fprintf fmt "%S" s in
215
    let print fmt (p, l) =
216
217
      fprintf fmt "%s [%a]" p (Pp.print_list Pp.comma print1) l
    in
218
    printf "@[<hov 2>Known input formats:@\n%a@]@."
219
220
221
      (Pp.print_list Pp.newline print)
      (List.sort Pervasives.compare (Env.list_formats ()))
  end;
222
  if !opt_list_provers then begin
223
    opt_list := true;
224
225
226
227
228
    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
    printf "@[<hov 2>Known provers:@\n%a@]@." print config.provers
  end;
229
  if !opt_list_metas then begin
230
    opt_list := true;
231
232
233
234
235
    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
236
    in
237
238
239
    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 ()))
240
  end;
241
242
243
244
245
246
247
248
  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;
249
250
251
252
253
254

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

255
256
257
  if !opt_prover <> None && !opt_driver <> None then begin
    eprintf "Options '-P'/'--prover' and \
      '-D'/'--driver' cannot be used together.@.";
258
259
    exit 1
  end;
260
261
262
263
264
265
266

  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
267
      eprintf "Option '-t'/'--timelimit' requires a prover.@.";
268
269
270
      exit 1
    end;
    if !opt_memlimit <> None then begin
271
      eprintf "Option '-m'/'--memlimit' requires a prover.@.";
272
273
274
275
      exit 1
    end;
    if !opt_driver = None && not !opt_print_namespace then
      opt_print_theory := true
276
277
  end;

278
279
280
281
282
283
284
285
  if !opt_debug_all then
    List.iter (fun (_,f,_) -> Debug.set_flag f) (Debug.list_flags ());

  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;

286
287
288
289
290
291
  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;
    if !opt_config <> None || !opt_prover <> None then exit 1;
    { conf_file = "";
292
(*
293
      loadpath  = [];
294
*)
295
296
      timelimit = None;
      memlimit  = None;
297
      running_provers_max = None;
298
299
300
      provers   = Mstr.empty }
  in

301
(*
302
  opt_loadpath := List.rev_append !opt_loadpath config.loadpath;
303
*)
304
305
  if !opt_timelimit = None then opt_timelimit := config.timelimit;
  if !opt_memlimit  = None then opt_memlimit  := config.memlimit;
306
  begin match !opt_prover with
307
308
  | Some s ->
      let prover = try Mstr.find s config.provers 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
    () end;
315
  let add_meta task (meta,s) =
316
317
    let meta = lookup_meta meta in
    add_meta task meta [MAstr s] in
318
  opt_task := List.fold_left add_meta !opt_task !opt_metas
319
320

let timelimit = match !opt_timelimit with
321
322
323
  | None -> 10
  | Some i when i <= 0 -> 0
  | Some i -> i
324

325
let memlimit = match !opt_memlimit with
326
327
328
329
  | None -> 0
  | Some i when i <= 0 -> 0
  | Some i -> i

330
let print_th_namespace fmt th =
331
  Pretty.print_namespace fmt th.th_name.Ident.id_string th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
332

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

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

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

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

394
let do_global_theory env drv (tname,p,t,glist) =
395
396
397
  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
398
  in
399
  do_theory env drv "lib" tname th glist
MARCHE Claude's avatar
MARCHE Claude committed
400

401
let do_local_theory env drv fname m (tname,_,t,glist) =
402
403
404
  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
405
  in
406
  do_theory env drv fname tname th glist
407
408

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

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

439
(*
440
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
441
compile-command: "unset LANG; make -C .. byte"
442
End:
443
*)