Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

main.ml 19.1 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
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
let opt_print_libdir = ref false
let opt_print_datadir = ref false

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

let opt_parse_only = ref false
let opt_type_only = ref false
119
let opt_debug_all = ref false
120
let opt_version = ref false
121 122 123 124

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

212
let () = try
213 214
  Arg.parse option_list add_opt_file usage_msg;

215 216 217 218
  if !opt_version then begin
    printf "%s@." version_msg;
    exit 0
  end;
219 220 221 222 223 224 225 226
  if !opt_print_libdir then begin
    printf "%s@." Config.libdir;
    exit 0
  end;
  if !opt_print_datadir then begin
    printf "%s@." Config.datadir;
    exit 0
  end;
227

François Bobot's avatar
François Bobot committed
228 229 230 231 232 233 234 235 236 237 238 239 240
  (** 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 *)
241
  let config = read_config !opt_config in
François Bobot's avatar
François Bobot committed
242 243 244 245 246
  let main = get_main config in
  Whyconf.load_plugins main;

  (** listings*)

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

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

307 308 309
  if !opt_prover <> None && !opt_driver <> None then begin
    eprintf "Options '-P'/'--prover' and \
      '-D'/'--driver' cannot be used together.@.";
310 311
    exit 1
  end;
312 313 314 315 316 317 318

  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
319
      eprintf "Option '-t'/'--timelimit' requires a prover.@.";
320 321 322
      exit 1
    end;
    if !opt_memlimit <> None then begin
323
      eprintf "Option '-m'/'--memlimit' requires a prover.@.";
324 325
      exit 1
    end;
326 327 328 329
    if !opt_bisect then begin
      eprintf "Option '--bisect' requires a prover.@.";
      exit 1
    end;
330 331
    if !opt_driver = None && not !opt_print_namespace then
      opt_print_theory := true
332 333
  end;

334 335 336 337 338
  if !opt_bisect && !opt_output = None then begin
    eprintf "Option '--bisect' require a directory to output the result.@.";
    exit 1
  end;

339 340 341
  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);
342
  begin match !opt_prover with
343
  | Some s ->
344
      let prover = try Mstr.find s (get_provers config) with
345
        | Not_found -> eprintf "Driver %s not found.@." s; exit 1
346
      in
347
      opt_command := Some prover.command;
348 349
      opt_driver := Some prover.driver
  | None ->
350 351
      ()
  end;
352
  let add_meta task (meta,s) =
353
    let meta = lookup_meta meta in
354 355
    add_meta task meta [MAstr s]
  in
356
  opt_task := List.fold_left add_meta !opt_task !opt_metas
357

358 359 360
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
361 362

let timelimit = match !opt_timelimit with
363 364 365
  | None -> 10
  | Some i when i <= 0 -> 0
  | Some i -> i
366

367
let memlimit = match !opt_memlimit with
368 369 370 371
  | None -> 0
  | Some i when i <= 0 -> 0
  | Some i -> i

372
let print_th_namespace fmt th =
373
  Pretty.print_namespace fmt th.th_name.Ident.id_string th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
374

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

377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408
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


409
let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
410
  match !opt_output, !opt_command with
411 412 413 414 415 416 417 418 419 420
    | 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
421 422 423 424 425 426
      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
427
    | None, Some command ->
Andrei Paskevich's avatar
Andrei Paskevich committed
428 429
        let call = Driver.prove_task ~command ~timelimit ~memlimit drv task in
        let res = Call_provers.wait_on_call (call ()) () in
430
        printf "%s %s %s : %a@." fname tname
431
          (task_goal task).Decl.pr_name.Ident.id_string
432 433
          Call_provers.print_prover_result res
    | None, None ->
434
        Driver.print_task drv std_formatter task
435
    | Some dir, _ -> output_task drv fname tname th task dir
436

437
let do_tasks env drv fname tname th task =
438
  let lookup acc t =
439 440
    (try Trans.singleton (Trans.lookup_transform t env) with
       Trans.UnknownTrans _ -> Trans.lookup_transform_l t env) :: acc
441
  in
442
  let trans = List.fold_left lookup [] !opt_trans in
443
  let apply tasks tr =
444
    List.rev (List.fold_left (fun acc task ->
445
      List.rev_append (Trans.apply tr task) acc) [] tasks)
446
  in
447
  let tasks = List.fold_left apply [task] trans in
448
  List.iter (do_task drv fname tname th) tasks
449

450
let do_theory env drv fname tname th glist =
451 452 453 454 455
  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
456
    let add acc (x,l) =
457 458 459 460
      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
461
      Decl.Spr.add pr acc
462 463
    in
    let drv = Util.of_option drv in
464 465 466 467
    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
468
  end
MARCHE Claude's avatar
MARCHE Claude committed
469

470
let do_global_theory env drv (tname,p,t,glist) =
471 472 473
  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
474
  in
475
  do_theory env drv "lib" tname th glist
MARCHE Claude's avatar
MARCHE Claude committed
476

477
let do_local_theory env drv fname m (tname,_,t,glist) =
478
  let th = try Mstr.find t m with Not_found ->
479 480
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
481
  in
482
  do_theory env drv fname tname th glist
483

484
let do_coq_realize_theory env _drv oldf fname m (tname,_,t,_glist) =
485
  let th = try Mstr.find t m with Not_found ->
MARCHE Claude's avatar
MARCHE Claude committed
486 487 488
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
  in
489 490 491 492
  let old =
    if Sys.file_exists oldf
    then
      begin
493
        let backup = oldf ^ ".bak" in
494 495 496 497 498 499 500
        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
501
  Coq.print_theory ?old env [] Ident.Mid.empty fmt th
MARCHE Claude's avatar
MARCHE Claude committed
502

503
let do_input env drv = function
504
  | None, _ when !opt_parse_only || !opt_type_only ->
505
      ()
506
  | None, tlist ->
507
      Queue.iter (do_global_theory env drv) tlist
508
  | Some f, tlist ->
509 510 511 512
      let fname, cin = match f with
        | "-" -> "stdin", stdin
        | f   -> f, open_in f
      in
513
      let m = Env.read_channel ?format:!opt_parser env fname cin in
514 515 516
      close_in cin;
      if !opt_type_only then
        ()
517
      else
518 519 520 521 522 523 524 525 526 527 528
        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 (Mstr.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
529

530 531
let () =
  try
Andrei Paskevich's avatar
Andrei Paskevich committed
532
    let env = Env.create_env_of_loadpath !opt_loadpath in
533
    let drv = Util.option_map (load_driver env) !opt_driver in
534
    Queue.iter (do_input env drv) opt_queue
535
  with e when not (Debug.test_flag Debug.stack_trace) ->
536
    eprintf "%a@." Exn_printer.exn_printer e;
537
    exit 1
538

539
(*
540
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
541
compile-command: "unset LANG; make -C .. byte"
542
End:
543
*)