src/tools/why3prove.ml

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2023 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 open Format
  13 open Why3
  14 open Wstdlib
  15 open Whyconf
  16 open Theory
  17 open Task
  18
  19 module Main : functor () -> sig end
  20  = functor () -> struct
  21
  22 let usage_msg =
  23   "[[<file>|-] [-T <theory> [-G <goal>]...]...]...\n\
  24    Run some transformation or prover on the given goals."
  25
  26 let opt_queue = Queue.create ()
  27
  28 let opt_input = ref None
  29 let opt_theory = ref None
  30 let opt_trans = ref []
  31 let opt_metas = ref []
  32 (* Option for printing counterexamples with JSON formatting *)
  33 let opt_json = ref false
  34 let opt_check_ce_model = ref false
  35 let opt_rac_prover = ref None
  36 let opt_rac_timelimit = ref None
  37 let opt_rac_memlimit = ref None
  38 let opt_rac_steplimit = ref None
  39 let opt_ce_log_verbosity = ref None
  40 let opt_sub_goals = ref []
  41
  42 let debug_print_original_model = Debug.register_info_flag "print-original-model"
  43     ~desc:"Print original counterexample model when --check-ce"
  44
  45 let debug_print_derived_model = Debug.register_info_flag "print-derived-model"
  46     ~desc:"Print derived counterexample model when --check-ce"
  47
  48 let add_opt_file x =
  49   let tlist = Queue.create () in
  50   Queue.push (Some x, tlist) opt_queue;
  51   opt_input := Some tlist
  52
  53 let add_opt_theory x =
  54   let l = Strings.split '.' x in
  55   let p, t = match List.rev l with
  56     | t::p -> List.rev p, t
  57     | _ -> assert false
  58   in
  59   match !opt_input, p with
  60   | None, [] ->
  61       let msg = "Option '-T'/'--theory' with a non-qualified \
  62                  argument requires an input file." in
  63       raise (Getopt.GetoptFailure msg)
  64   | Some tlist, [] ->
  65       let glist = Queue.create () in
  66       let elist = Queue.create () in
  67       Queue.push (x, p, t, glist, elist) tlist;
  68       opt_theory := Some glist
  69   | _ ->
  70       let tlist = Queue.create () in
  71       Queue.push (None, tlist) opt_queue;
  72       opt_input := None;
  73       let glist = Queue.create () in
  74       let elist = Queue.create () in
  75       Queue.push (x, p, t, glist,elist) tlist;
  76       opt_theory := Some glist
  77
  78 let add_opt_goal x =
  79   let glist = match !opt_theory, !opt_input with
  80     | None, None ->
  81         let msg = "Option '-G'/'--goal' requires an input file or a library \
  82                    theory." in
  83         raise (Getopt.GetoptFailure msg)
  84     | None, Some _ ->
  85         add_opt_theory "Top";
  86         Option.get !opt_theory
  87     | Some glist, _ -> glist in
  88   let l = Strings.split '.' x in
  89   Queue.push (x, l) glist
  90
  91 let add_opt_trans x =
  92   match String.split_on_char ' ' x with
  93   | [] -> assert false
  94   | name :: args ->
  95       opt_trans := (name, args) :: !opt_trans
  96
  97 let add_opt_meta meta =
  98   let meta_name, meta_arg =
  99     try
 100       let index = String.index meta '=' in
 101       (String.sub meta 0 index),
 102       Some (String.sub meta (index+1) (String.length meta - (index + 1)))
 103     with Not_found ->
 104       meta, None
 105   in
 106   opt_metas := (meta_name,meta_arg)::!opt_metas
 107
 108 let subgoal_re = Re.Str.regexp "^\\([^:@]+\\)?\\(:[^@]+\\)?\\(@.+\\)?$"
 109
 110 let add_sub_goal s =
 111   let failure str =
 112     let msg = str ^ " for option --sub-goal" in
 113     raise (Getopt.GetoptFailure msg) in
 114   if Re.Str.string_match subgoal_re s 0 then (
 115     let f =
 116       try Re.Str.matched_group 1 s
 117       with Not_found ->
 118       try Option.get (fst (Queue.peek opt_queue))
 119       with _ -> failure "Missing file" in
 120     let l =
 121       try
 122         let s = Strings.remove_prefix ":" (Re.Str.matched_group 2 s) in
 123         Some (int_of_string s)
 124       with Not_found -> None | Failure _ -> failure "Invalid line number" in
 125     let e =
 126       try Some (Strings.remove_prefix "@" (Re.Str.matched_group 3 s))
 127       with Not_found -> None in
 128     opt_sub_goals := (f,l,e) :: !opt_sub_goals )
 129   else
 130     failure "Invalid argument"
 131
 132 let opt_driver : string list ref = ref []
 133 let opt_parser = ref None
 134 let opt_prover = ref None
 135 let opt_output = ref None
 136 let opt_timelimit = ref None
 137 let opt_stepslimit = ref None
 138 let opt_memlimit = ref None
 139 let opt_command = ref None
 140 let opt_task = ref None
 141
 142 let opt_print_theory = ref false
 143 let opt_print_namespace = ref false
 144 let opt_color = ref false
 145
 146 let option_list =
 147   let open Getopt in
 148   [ Key ('T', "theory"), Hnd1 (AString, add_opt_theory),
 149     "<theory> select <theory> in the input file or in the library";
 150     Key ('G', "goal"), Hnd1 (AString, add_opt_goal),
 151     "<goal> select <goal> in the last selected theory";
 152     Key ('a', "apply-transform"), Hnd1 (AString, add_opt_trans),
 153     "<transf> apply a transformation to every task";
 154     Key ('g', "sub-goal"), Hnd1 (AString, add_sub_goal),
 155     "[<file>][:<line>][@<expl>] select sub-goals at the given\n\
 156      position and with the given explanation after applying\n\
 157      the transformations (<file> defaults to the input file)";
 158     Key ('P', "prover"), Hnd1 (AString, fun s -> opt_prover := Some s),
 159     "<prover> prove or print (with -o) the selected goals";
 160     Key ('F', "format"), Hnd1 (AString, fun s -> opt_parser := Some s),
 161     "<format> select input format (default: \"why\")";
 162     Key ('t', "timelimit"), Hnd1 (AFloat, fun i -> opt_timelimit := Some i),
 163     "<sec> set the prover's time limit (default=10, no limit=0)";
 164     Key ('s', "stepslimit"), Hnd1 (AInt, fun i -> opt_stepslimit := Some i),
 165     "<steps> set the prover's step limit (default: no limit)";
 166     Key ('m', "memlimit"), Hnd1 (AInt, fun i -> opt_memlimit := Some i),
 167     "<MiB> set the prover's memory limit (default: no limit)";
 168     Key ('M', "meta"), Hnd1 (AString, add_opt_meta),
 169     "<meta>[=<string>] add a meta to every task";
 170     Key ('D', "driver"), Hnd1 (AString, fun s -> opt_driver := s::!opt_driver),
 171     "<file> specify a prover's driver (conflicts with -P)";
 172     Key ('o', "output"), Hnd1 (AString, fun s -> opt_output := Some s),
 173     "<dir> print the selected goals to separate files in <dir>";
 174     KLong "print-theory", Hnd0 (fun () -> opt_print_theory := true),
 175     " print selected theories";
 176     KLong "print-namespace", Hnd0 (fun () -> opt_print_namespace := true),
 177     " print namespaces of selected theories";
 178     Debug.Args.desc_shortcut
 179       "parse_only" (KLong "parse-only") " stop after parsing";
 180     Debug.Args.desc_shortcut
 181       "type_only" (KLong "type-only") " stop after type checking";
 182     Termcode.opt_extra_expl_prefix;
 183     KLong "check-ce", Hnd0 (fun () -> opt_check_ce_model := true),
 184     " check counterexamples using runtime assertion checking\n\
 185      (RAC)";
 186     KLong "rac-prover", Hnd1 (AString, fun s -> opt_rac_prover := Some s),
 187     "<prover> use <prover> to check assertions in RAC when term\n\
 188      reduction is insufficient, with optional, space-\n\
 189      separated time and memory limit (e.g. 'cvc4 2 1000')";
 190     KLong "rac-timelimit", Hnd1 (AFloat, fun i -> opt_rac_timelimit := Some i),
 191     "<sec> set the time limit for RAC (with --check-ce)";
 192     KLong "rac-memlimit", Hnd1 (AInt, fun i -> opt_rac_memlimit := Some i),
 193     "<steps> set the memory limit for RAC (with --check-ce)";
 194     KLong "rac-steplimit", Hnd1 (AInt, fun i -> opt_rac_steplimit := Some i),
 195     "<steps> set the step limit for RAC (with --check-ce)";
 196     KLong "ce-log-verbosity", Hnd1(AInt, fun i -> opt_ce_log_verbosity := Some i),
 197     "<lvl> verbosity level for interpretation log of\n\
 198     counterexample solver model";
 199     KLong "json", Hnd0 (fun () -> opt_json := true),
 200     " print output in JSON format";
 201     KLong "color", Hnd0 (fun () -> opt_color := true),
 202     " print output with colors";
 203   ]
 204
 205 let config, env =
 206   Whyconf.Args.initialize option_list add_opt_file usage_msg
 207
 208 let opt_driver = ref (match !opt_driver with
 209   | f::ef -> Some (None,f,["",ef])
 210   | [] -> None)
 211
 212 let () = try
 213   if Queue.is_empty opt_queue then
 214     Whyconf.Args.exit_with_usage usage_msg;
 215
 216   if !opt_prover <> None && !opt_driver <> None then begin
 217     eprintf "Options '-P'/'--prover' and \
 218       '-D'/'--driver' cannot be used together.@.";
 219     exit 1
 220   end;
 221
 222   if !opt_output <> None && !opt_driver = None && !opt_prover = None then begin
 223     eprintf
 224       "Option '-o'/'--output' requires either a prover or a driver.@.";
 225     exit 1
 226   end;
 227
 228   if !opt_prover = None then begin
 229     if !opt_timelimit <> None then begin
 230       eprintf "Option '-t'/'--timelimit' requires a prover.@.";
 231       exit 1
 232     end;
 233     if !opt_stepslimit <> None then begin
 234       eprintf "Option '-t'/'--stepslimit' requires a prover.@.";
 235       exit 1
 236     end;
 237     if !opt_memlimit <> None then begin
 238       eprintf "Option '-m'/'--memlimit' requires a prover.@.";
 239       exit 1
 240     end;
 241     if !opt_driver = None && not !opt_print_namespace then
 242       opt_print_theory := true
 243   end;
 244
 245   let main = Whyconf.get_main config in
 246
 247   if !opt_timelimit = None then opt_timelimit := Some (Whyconf.timelimit main);
 248   if !opt_memlimit  = None then opt_memlimit  := Some (Whyconf.memlimit main);
 249   begin match !opt_prover with
 250   | Some s ->
 251     let filter_prover = Whyconf.parse_filter_prover s in
 252     let prover = Whyconf.filter_one_prover config filter_prover in
 253     let with_steps = !opt_stepslimit <> None in
 254     opt_command := Some (Whyconf.get_complete_command prover ~with_steps);
 255     let (d,f) = prover.driver in
 256     opt_driver := Some(d,f,prover.extra_drivers)
 257   | None ->
 258       ()
 259   end;
 260   let add_meta task (meta,s) =
 261     let meta = lookup_meta meta in
 262     let args = match meta.meta_type, s with
 263       | [MTstring], Some s -> [MAstr s]
 264       | [MTint], Some s -> [MAint (int_of_string s)]
 265       | [], None -> []
 266       | _ -> failwith "meta argument not implemented"
 267     in
 268     Task.add_meta task meta args
 269   in
 270   opt_task := List.fold_left add_meta !opt_task !opt_metas
 271
 272   with e when not (Debug.test_flag Debug.stack_trace) ->
 273     eprintf "%a@." Exn_printer.exn_printer e;
 274     exit 1
 275
 276 let timelimit = match !opt_timelimit with
 277   | None -> 10.
 278   | Some i when i <= 0. -> 0.
 279   | Some i -> i
 280
 281 let stepslimit = Option.value ~default:0 !opt_stepslimit
 282
 283 let memlimit = match !opt_memlimit with
 284   | None -> 0
 285   | Some i when i <= 0 -> 0
 286   | Some i -> i
 287
 288 let print_th_namespace fmt th =
 289   Pretty.print_namespace th.th_name.Ident.id_string fmt th
 290
 291 let really_do_task (task: task) =
 292   let t = task_goal_fmla task in
 293   let aux (f,l,e) =
 294     match t.Term.t_loc with
 295     | None -> false
 296     | Some loc ->
 297         let goal_f, goal_l, _, _, _ = Loc.get loc in
 298         goal_f = f &&
 299         (match l with None -> true | Some l -> l = goal_l) &&
 300         (match e with None -> true | Some e ->
 301          let expls = String.concat " " (Termcode.get_expls_fmla t) in
 302          String.(equal (lowercase_ascii e) (lowercase_ascii expls))) in
 303   !opt_sub_goals = [] || List.exists aux !opt_sub_goals
 304
 305 let fname_printer = ref (Ident.create_ident_printer [])
 306
 307 let output_task drv fname _tname th task dir =
 308   let fname = Filename.basename fname in
 309   let fname =
 310     try Filename.chop_extension fname with _ -> fname in
 311   let tname = th.th_name.Ident.id_string in
 312   let dest = Driver.file_of_task drv fname tname task in
 313   (* Uniquify the filename before the extension if it exists*)
 314   let i = try String.rindex dest '.' with _ -> String.length dest in
 315   let name = Ident.string_unique !fname_printer (String.sub dest 0 i) in
 316   let ext = String.sub dest i (String.length dest - i) in
 317   let cout = open_out (Filename.concat dir (name ^ ext)) in
 318   Driver.print_task drv (formatter_of_out_channel cout) task;
 319   close_out cout
 320
 321 let print_result json fmt (fname, loc, goal_name, expls, res, ce) =
 322   if json then
 323     begin
 324       let open Json_base in
 325       let loc =
 326         match loc with
 327         | None -> Record ["file-name", String fname]
 328         | Some loc ->
 329             let f, bl, bc, el, ec = Loc.get loc in
 330             Record [
 331                 "file-name", String f;
 332                 "start-line", Int bl;
 333                 "start-char", Int bc;
 334                 "end-line", Int el;
 335                 "end-char", Int ec
 336               ] in
 337       let term =
 338         Record [
 339             "loc", loc;
 340             "goal_name", String goal_name;
 341             "explanations", List (List.map (fun s -> String s) expls)
 342           ] in
 343       print_json fmt
 344         (Record [
 345              "term", term;
 346              "prover-result", Call_provers.json_prover_result res
 347            ])
 348     end
 349   else
 350     begin
 351       ( match loc with
 352         | None -> fprintf fmt "File %s:@\n" fname
 353         | Some loc -> fprintf fmt "File %a:@\n" Loc.pp_position loc );
 354       ( if expls = [] then
 355           fprintf fmt "@[<hov>Goal@ @{<bold>%s@}.@]" goal_name
 356         else
 357           let expls = String.capitalize_ascii (String.concat ", " expls) in
 358           fprintf fmt
 359             "@[<hov>Sub-goal@ @{<bold>%s@}@ of@ goal@ @{<bold>%s@}.@]"
 360             expls goal_name );
 361       fprintf fmt "@\n@[<hov2>Prover result is: %a.@]"
 362         (Call_provers.print_prover_result ~json:false) res;
 363       Option.iter
 364         (Check_ce.print_model_classification ~json
 365            ?verb_lvl:!opt_ce_log_verbosity ~check_ce:!opt_check_ce_model env fmt)
 366         ce;
 367       fprintf fmt "@\n"
 368     end
 369
 370 let unproved = ref false
 371
 372 let select_ce env th models =
 373   if models <> [] then
 374     match Pmodule.restore_module th with
 375     | pm ->
 376         let main = Whyconf.get_main config in
 377         let limit_time = Whyconf.timelimit main in
 378         let limit_time = Opt.fold (fun _ s -> s) limit_time !opt_rac_timelimit in
 379         let limit_mem = Whyconf.memlimit main in
 380         let limit_mem = Opt.fold (fun _ s -> s) limit_mem !opt_rac_memlimit in
 381         let limit_steps = Opt.fold (fun _ s -> s) 0 !opt_rac_steplimit in
 382         let limits = Call_provers.{ limit_time ; limit_mem ; limit_steps } in
 383         let why_prover =
 384           match !opt_rac_prover with
 385           | None -> None
 386           | Some p -> Some(p,limits)
 387         in
 388         let rac = Pinterp.mk_rac ~ignore_incomplete:false
 389             (Rac.Why.mk_check_term_lit config env ~why_prover ()) in
 390         Check_ce.select_model ~limits ?verb_lvl:!opt_ce_log_verbosity
 391           ~check_ce:!opt_check_ce_model rac env pm models
 392     | exception Not_found -> None
 393   else None
 394
 395 let debug_print_model_attrs = Debug.lookup_flag "print_model_attrs"
 396
 397 let print_other_models (m, (c, log)) =
 398   let print_model fmt m =
 399     let print_attrs = Debug.test_flag debug_print_model_attrs in
 400     Model_parser.print_model fmt m ~print_attrs
 401   in
 402   ( match c with
 403     | Check_ce.(NC | SW | NC_SW | BAD_CE _) ->
 404         if Debug.test_flag debug_print_original_model then
 405           printf "@[<v>Original model:@\n%a@]@\n@." print_model m;
 406     | _ -> () );
 407   ( match c with
 408     | Check_ce.(NC | SW | NC_SW) ->
 409         if Debug.test_flag debug_print_derived_model then
 410           printf "@[<v>Derived model:@\n%a@]@\n@." print_model
 411             (Check_ce.model_of_exec_log ~original_model:m log)
 412     | _ -> () )
 413
 414 let do_task config env drv fname tname (th : Theory.theory) (task : Task.task) =
 415   if really_do_task task then
 416   let open Call_provers in
 417   let limits =
 418     { limit_time = timelimit;
 419       limit_mem = memlimit;
 420       limit_steps = stepslimit } in
 421   match !opt_output, !opt_command with
 422     | None, Some command ->
 423         let call =
 424           Driver.prove_task ~command ~config ~limits drv task
 425         in
 426         let res = wait_on_call call in
 427         let ce = select_ce env th res.pr_models in
 428         let t = task_goal_fmla task in
 429         let expls = Termcode.get_expls_fmla t in
 430         let goal_name = (task_goal task).Decl.pr_name.Ident.id_string in
 431         printf "%a@." (print_result !opt_json)
 432           (fname, t.Term.t_loc, goal_name, expls, res, ce);
 433         Option.iter print_other_models ce;
 434         if res.pr_answer <> Valid then unproved := true
 435     | None, None ->
 436         Driver.print_task drv std_formatter task
 437     | Some dir, _ -> output_task drv fname tname th task dir
 438
 439 let do_tasks config env drv fname tname th task =
 440   let table = Args_wrapper.build_naming_tables task in
 441   let rec apply tasks = function
 442     | [] -> tasks
 443     | (name, args) :: trans ->
 444         let apply_trans =
 445           if args = [] then
 446             Trans.apply_transform name env
 447           else
 448             let ffmt = Env.get_format ?format:!opt_parser fname in
 449             Trans.apply_transform_args name env args table ffmt in
 450         apply (List.concat (List.map apply_trans tasks)) trans in
 451   let tasks = apply [task] !opt_trans in
 452   List.iter (do_task config env drv fname tname th) tasks
 453
 454 let do_theory config env drv fname tname th glist elist =
 455   if !opt_print_theory then
 456     printf "%a@." Pretty.print_theory th
 457   else if !opt_print_namespace then
 458     printf "%a@." print_th_namespace th
 459   else begin
 460     let add acc (x,l) =
 461       let pr = try ns_find_pr th.th_export l with Not_found ->
 462         eprintf "Goal '%s' not found in theory '%s'.@." x tname;
 463         exit 1
 464       in
 465       Decl.Spr.add pr acc
 466     in
 467     let drv = Option.get drv in
 468     let prs = Queue.fold add Decl.Spr.empty glist in
 469     let sel = if Decl.Spr.is_empty prs then None else Some prs in
 470     let tasks = Task.split_theory th sel !opt_task in
 471     List.iter (do_tasks config env drv fname tname th) tasks;
 472     let eval (x,l) =
 473       let ls = try ns_find_ls th.th_export l with Not_found ->
 474         eprintf "Declaration '%s' not found in theory '%s'.@." x tname;
 475         exit 1
 476       in
 477       match Decl.find_logic_definition th.th_known ls with
 478       | None -> eprintf "Symbol '%s' has no definition in theory '%s'.@." x tname;
 479         exit 1
 480       | Some d ->
 481         let l,_t = Decl.open_ls_defn d in
 482         match l with
 483         | [] ->
 484 (* TODO
 485           let t = Mlw_interp.eval_global_term env th.th_known t in
 486           printf "@[<hov 2>Evaluation of %s:@ %a@]@." x Mlw_interp.print_value t
 487 *) ()
 488         | _ ->
 489           eprintf "Symbol '%s' is not a constant in theory '%s'.@." x tname;
 490           exit 1
 491     in
 492     Queue.iter eval elist
 493   end
 494
 495 let do_global_theory config env drv (tname,p,t,glist,elist) =
 496   let th = Env.read_theory env p t in
 497   do_theory config env drv "lib" tname th glist elist
 498
 499 let do_local_theory config env drv fname m (tname,_,t,glist,elist) =
 500   let th = try Mstr.find t m with Not_found ->
 501     eprintf "Theory '%s' not found in file '%s'.@." tname fname;
 502     exit 1
 503   in
 504   do_theory config env drv fname tname th glist elist
 505
 506 let do_input config env drv = function
 507   | None, _ when Debug.test_flag Typing.debug_type_only ||
 508                  Debug.test_flag Typing.debug_parse_only ->
 509       ()
 510   | None, tlist ->
 511       Queue.iter (do_global_theory config env drv) tlist
 512   | Some f, tlist ->
 513       let format = !opt_parser in
 514       let fname, m = match f with
 515         | "-" -> "stdin",
 516             Env.read_channel Env.base_language ?format env "stdin" stdin
 517         | fname ->
 518             let (mlw_files, _) =
 519               Env.read_file Env.base_language ?format env fname in
 520             (fname, mlw_files)
 521       in
 522       if Debug.test_flag Typing.debug_type_only then ()
 523       else
 524         if Queue.is_empty tlist then
 525           let glist = Queue.create () in
 526           let elist = Queue.create () in
 527           let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
 528           let do_th _ (t,th) =
 529             do_theory config env drv fname t th glist elist
 530           in
 531           Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
 532         else
 533           Queue.iter (do_local_theory config env drv fname m) tlist
 534
 535 let () =
 536   try
 537     if (Util.terminal_has_color && !opt_color) then (
 538       Format.set_formatter_stag_functions Util.ansi_color_tags;
 539       set_mark_tags true );
 540     let main = Whyconf.get_main config in
 541     let load (d,f,ef) = Driver.load_driver_file_and_extras main env ~extra_dir:d f ef in
 542     let drv = Option.map load !opt_driver in
 543     Queue.iter (do_input main env drv) opt_queue;
 544     if !unproved then exit 2
 545   with e when not (Debug.test_flag Debug.stack_trace) ->
 546     eprintf "%a@." Exn_printer.exn_printer e;
 547     exit 1
 548
 549 end
 550
 551 let () = Whyconf.Args.register_main (module Main)
 552
 553
 554 (*
 555 Local Variables:
 556 compile-command: "unset LANG; make -C ../.. byte"
 557 End:
 558 *)