Commit 74e9e7b3 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Add a "prove" subcommand.

parent eedc2f21
......@@ -66,6 +66,9 @@ why3.conf
/bin/why3doc.byte
/bin/why3doc.opt
/bin/why3doc
/bin/why3prove.byte
/bin/why3prove.opt
/bin/why3prove
/bin/why3replayer.byte
/bin/why3replayer.opt
/bin/why3replayer
......
......@@ -429,8 +429,11 @@ src/tools/main.cmx: lib/why3/why3.cmxa
src/tools/why3contraption.cmo: lib/why3/why3.cma
src/tools/why3contraption.cmx: lib/why3/why3.cmxa
byte: bin/why3.byte bin/why3contraption.byte
opt: bin/why3.opt bin/why3contraption.opt
src/tools/why3prove.cmo: lib/why3/why3.cma
src/tools/why3prove.cmx: lib/why3/why3.cmxa
byte: bin/why3.byte bin/why3contraption.byte bin/why3prove.byte
opt: bin/why3.opt bin/why3contraption.opt bin/why3prove.opt
bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
......@@ -454,27 +457,42 @@ bin/why3contraption.byte: lib/why3/why3.cma src/tools/why3contraption.cmo
bin/why3contraption: bin/why3contraption.@OCAMLBEST@
ln -sf why3contraption.@OCAMLBEST@ $@
bin/why3prove.opt: lib/why3/why3.cmxa src/tools/why3prove.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3prove.byte: lib/why3/why3.cma src/tools/why3prove.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3prove: bin/why3prove.@OCAMLBEST@
ln -sf why3prove.@OCAMLBEST@ $@
clean_old_install::
rm -f $(BINDIR)/why3$(EXE) $(BINDIR)/why3contraption$(EXE)
rm -f $(BINDIR)/why3$(EXE) $(BINDIR)/why3contraption$(EXE) $(BINDIR)/why3prove$(EXE)
install_no_local::
cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
cp -f bin/why3contraption.@OCAMLBEST@ $(BINDIR)/why3contraption$(EXE)
cp -f bin/why3prove.@OCAMLBEST@ $(TOOLDIR)/why3prove$(EXE)
install_local: bin/why3 bin/why3contraption
install_local: bin/why3 bin/why3contraption bin/why3prove
ifneq "$(MAKECMDGOALS)" "clean"
include src/tools/main.dep
include src/tools/why3contraption.dep
include src/tools/why3prove.dep
endif
depend: src/tools/main.dep src/tools/why3contraption.dep
depend: src/tools/main.dep src/tools/why3contraption.dep src/tools/why3prove.dep
clean::
rm -f src/tools/main.cm[iox] src/tools/main.annot src/tools/main.o src/tools/main.dep
rm -f src/tools/why3contraption.cm[iox] src/tools/why3contraption.annot src/tools/why3contraption.o src/tools/why3contraption.dep
rm -f src/tools/why3prove.cm[iox] src/tools/why3prove.annot src/tools/why3prove.o src/tools/why3prove.dep
rm -f bin/why3.byte bin/why3.opt bin/why3
rm -f bin/why3contraption.byte bin/why3contraption.opt bin/why3contraption
rm -f bin/why3prove.byte bin/why3prove.opt bin/why3prove
##############
# test targets
......
......@@ -15,7 +15,7 @@ open Whyconf
open Theory
let usage_msg = sprintf
"Usage: %s [options] [[file|-] [-T <theory> [-G <goal>]...]...]..."
"Usage: %s [options] command [options]"
(Filename.basename Sys.argv.(0))
let version_msg = sprintf "Why3 platform, version %s (build date: %s)"
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2014 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open Format
open Why3
open Stdlib
open Whyconf
open Theory
open Task
open Driver
let usage_msg = sprintf
"Usage: %s [options] [[file|-] [-T <theory> [-G <goal>]...]...]..."
(Filename.basename Sys.argv.(0))
let opt_queue = Queue.create ()
let opt_input = ref None
let opt_theory = ref None
let opt_trans = ref []
let opt_metas = ref []
let add_opt_file x =
let tlist = Queue.create () in
Queue.push (Some x, tlist) opt_queue;
opt_input := Some tlist
let add_opt_theory =
let rdot = (Str.regexp "\\.") in fun x ->
let l = Str.split rdot x in
let p, t = match List.rev l with
| t::p -> List.rev p, t
| _ -> assert false
in
match !opt_input, p with
| None, [] ->
eprintf "Option '-T'/'--theory' with a non-qualified \
argument requires an input file.@.";
exit 1
| Some tlist, [] ->
let glist = Queue.create () in
let elist = Queue.create () in
Queue.push (x, p, t, glist, elist) tlist;
opt_theory := Some glist
| _ ->
let tlist = Queue.create () in
Queue.push (None, tlist) opt_queue;
opt_input := None;
let glist = Queue.create () in
let elist = Queue.create () in
Queue.push (x, p, t, glist,elist) tlist;
opt_theory := Some glist
let add_opt_goal x = match !opt_theory with
| None ->
eprintf "Option '-G'/'--goal' requires a theory.@.";
exit 1
| Some glist ->
let l = Str.split (Str.regexp "\\.") x in
Queue.push (x, l) glist
let add_opt_trans x = opt_trans := x::!opt_trans
let add_opt_meta meta =
let meta_name, meta_arg =
try
let index = String.index meta '=' in
(String.sub meta 0 index),
Some (String.sub meta (index+1) (String.length meta - (index + 1)))
with Not_found ->
meta, None
in
opt_metas := (meta_name,meta_arg)::!opt_metas
let opt_config = ref None
let opt_extra = ref []
let opt_parser = ref None
let opt_prover = ref None
let opt_loadpath = ref []
let opt_driver = ref None
let opt_output = ref None
let opt_timelimit = ref None
let opt_memlimit = ref None
let opt_command = ref None
let opt_task = ref None
let opt_print_theory = ref false
let opt_print_namespace = ref false
let opt_version = ref false
let option_list = Arg.align [
"-", Arg.Unit (fun () -> add_opt_file "-"),
" Read the input file from stdin";
"-T", Arg.String add_opt_theory,
"<theory> Select <theory> in the input file or in the library";
"--theory", Arg.String add_opt_theory,
" same as -T";
"-G", Arg.String add_opt_goal,
"<goal> Select <goal> in the last selected theory";
"--goal", Arg.String add_opt_goal,
" same as -G";
"-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";
"--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]),
"<file> Read additional configuration from <file>";
"-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
"<dir> Add <dir> to the library search path";
"--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
" same as -L";
"-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";
"-F", Arg.String (fun s -> opt_parser := Some s),
"<format> Select input format (default: \"why\")";
"--format", Arg.String (fun s -> opt_parser := Some s),
" same as -F";
"-t", Arg.Int (fun i -> opt_timelimit := Some i),
"<sec> Set the prover's time limit (default=10, no limit=0)";
"--timelimit", Arg.Int (fun i -> opt_timelimit := Some i),
" same as -t";
"-m", Arg.Int (fun i -> opt_memlimit := Some i),
"<MiB> Set the prover's memory limit (default: no limit)";
"--memlimit", Arg.Int (fun i -> opt_timelimit := Some i),
" same as -m";
"-a", Arg.String add_opt_trans,
"<transformation> Apply a transformation to every task";
"--apply-transform", Arg.String add_opt_trans,
" same as -a";
"-M", Arg.String add_opt_meta,
"<meta_name>[=<string>] Add a meta to every task";
"--meta", Arg.String add_opt_meta,
" same as -M";
"-D", Arg.String (fun s -> opt_driver := Some (s, [])),
"<file> Specify a prover's driver (conflicts with -P)";
"--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,
" Print selected theories";
"--print-namespace", Arg.Set opt_print_namespace,
" Print namespaces of selected theories";
Debug.Args.desc_debug_list;
Debug.Args.desc_shortcut "parse_only" "--parse-only" " Stop after parsing";
Debug.Args.desc_shortcut
"type_only" "--type-only" " Stop after type checking";
Debug.Args.desc_debug_all;
Debug.Args.desc_debug ]
let () = try
Arg.parse option_list add_opt_file usage_msg;
(** Configuration *)
let config = read_config !opt_config in
let config = List.fold_left merge_config config !opt_extra in
let main = get_main config in
Whyconf.load_plugins main;
Debug.Args.set_flags_selected ();
if Queue.is_empty opt_queue then begin
Arg.usage option_list usage_msg;
exit 1
end;
if !opt_prover <> None && !opt_driver <> None then begin
eprintf "Options '-P'/'--prover' and \
'-D'/'--driver' cannot be used together.@.";
exit 1
end;
if !opt_output <> None && !opt_driver = None && !opt_prover = None then begin
eprintf
"Option '-o'/'--output' requires either a prover or a driver.@.";
exit 1
end;
if !opt_prover = None then begin
if !opt_timelimit <> None then begin
eprintf "Option '-t'/'--timelimit' requires a prover.@.";
exit 1
end;
if !opt_memlimit <> None then begin
eprintf "Option '-m'/'--memlimit' requires a prover.@.";
exit 1
end;
if !opt_driver = None && not !opt_print_namespace then
opt_print_theory := true
end;
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);
begin match !opt_prover with
| Some s ->
let filter_prover = Whyconf.parse_filter_prover s in
let prover = Whyconf.filter_one_prover config filter_prover in
opt_command :=
Some (String.concat " " (prover.command :: prover.extra_options));
opt_driver := Some (prover.driver, prover.extra_drivers)
| None ->
()
end;
let add_meta task (meta,s) =
let meta = lookup_meta meta in
let args = match s with
| Some s -> [MAstr s]
| None -> []
in
Task.add_meta task meta args
in
opt_task := List.fold_left add_meta !opt_task !opt_metas
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
let timelimit = match !opt_timelimit with
| None -> 10
| Some i when i <= 0 -> 0
| Some i -> i
let memlimit = match !opt_memlimit with
| None -> 0
| Some i when i <= 0 -> 0
| Some i -> i
let print_th_namespace fmt th =
Pretty.print_namespace fmt th.th_name.Ident.id_string th
let fname_printer = ref (Ident.create_ident_printer [])
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
let output_theory drv fname _tname th task dir =
let fname = Filename.basename fname in
let fname =
try Filename.chop_extension fname with _ -> fname in
let dest = Driver.file_of_theory drv fname th in
let file = Filename.concat dir dest in
let old =
if Sys.file_exists file then begin
let backup = file ^ ".bak" in
Sys.rename file backup;
Some (open_in backup)
end else None in
let cout = open_out file in
Driver.print_task ?old drv (formatter_of_out_channel cout) task;
close_out cout
let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
match !opt_output, !opt_command with
| None, Some command ->
let call = Driver.prove_task ~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
| None, None ->
Driver.print_task drv std_formatter task
| Some dir, _ -> output_task drv fname tname th task dir
let do_tasks env drv fname tname th task =
let lookup acc t =
(try Trans.singleton (Trans.lookup_transform t env) with
Trans.UnknownTrans _ -> Trans.lookup_transform_l t env) :: acc
in
let trans = List.fold_left lookup [] !opt_trans in
let apply tasks tr =
List.rev (List.fold_left (fun acc task ->
List.rev_append (Trans.apply tr task) acc) [] tasks)
in
let tasks = List.fold_left apply [task] trans in
List.iter (do_task drv fname tname th) tasks
let do_theory env drv fname tname th glist elist =
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
let add acc (x,l) =
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
Decl.Spr.add pr acc
in
let drv = Opt.get drv in
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;
let eval (x,l) =
let ls = try ns_find_ls th.th_export l with Not_found ->
eprintf "Declaration '%s' not found in theory '%s'.@." x tname;
exit 1
in
match Decl.find_logic_definition th.th_known ls with
| None -> eprintf "Symbol '%s' has no definition in theory '%s'.@." x tname;
exit 1
| Some d ->
let l,t = Decl.open_ls_defn d in
match l with
| [] ->
let t = Mlw_interp.eval_global_term env th.th_known t in
printf "@[<hov 2>Evaluation of %s:@ %a@]@." x Mlw_interp.print_value t
| _ ->
eprintf "Symbol '%s' is not a constant in theory '%s'.@." x tname;
exit 1
in
Queue.iter eval elist
end
let do_global_theory env drv (tname,p,t,glist,elist) =
let format = Opt.get_def "why" !opt_parser in
let th = try Env.read_theory ~format env p t with Env.TheoryNotFound _ ->
eprintf "Theory '%s' not found.@." tname;
exit 1
in
do_theory env drv "lib" tname th glist elist
let do_local_theory env drv fname m (tname,_,t,glist,elist) =
let th = try Mstr.find t m with Not_found ->
eprintf "Theory '%s' not found in file '%s'.@." tname fname;
exit 1
in
do_theory env drv fname tname th glist elist
let do_input env drv = function
| None, _ when Debug.test_flag Typing.debug_type_only ||
Debug.test_flag Typing.debug_parse_only ->
()
| None, tlist ->
Queue.iter (do_global_theory env drv) tlist
| Some f, tlist ->
let fname, cin = match f with
| "-" -> "stdin", stdin
| f -> f, open_in f
in
let m = Env.read_channel ?format:!opt_parser env fname cin in
close_in cin;
if Debug.test_flag Typing.debug_type_only then
()
else
if Queue.is_empty tlist then
let glist = Queue.create () in
let elist = 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 elist
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
let driver_file s =
if Sys.file_exists s || String.contains s '/' || String.contains s '.' then
s
else
Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv"))
let load_driver env (s,ef) =
let file = driver_file s in
load_driver env file ef
let load_driver_extract env s =
let file = driver_file s in
let lib = Mlw_main.library_of_env env in
Mlw_driver.load_driver lib file []
let () =
try
let env = Env.create_env !opt_loadpath in
let drv = Opt.map (load_driver env) !opt_driver in
Queue.iter (do_input env drv) opt_queue
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. byte"
End:
*)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment