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
*)