Commit 1b919e57 authored by Jean-Christophe's avatar Jean-Christophe
parents abdfa014 d284bb83
......@@ -622,22 +622,18 @@ clean::
# tools
#######
TOOLS = bin/why3-cpulimit bin/why3-cpulimit_time
TOOLS = bin/why3-cpulimit
byte opt: $(TOOLS)
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
$(CC) -Wall -o $@ $^
bin/why3-cpulimit_time: src/tools/@CPULIMIT@_time.c
$(CC) -Wall -o $@ $^
clean::
rm -f bin/why3-cpulimit src/tools/*~
install_no_local::
cp -f bin/why3-cpulimit $(BINDIR)
cp -f bin/why3-cpulimit_time $(BINDIR)
########
# bench
......
......@@ -4,27 +4,29 @@
== Documentation ==
1 Introduction (TODO: a finir)
2 getting started (TODO: finir why3 batch)
2 getting started (Claude: done, to be read by others)
3 Syntax, tutorial (TODO: JCF + Andrei)
4 tutorial for API:
** build a task (done)
** call a prover (done)
** build a task (Claude: done, to be read by others)
** call a prover (Claude: done, to be read by others)
** apply a transformation (TODO ?)
** develop a new transformation (TODO ?)
5 syntax reference (TODO)
6 Standard lib of theories: done, although quite sparse
6 Standard lib of theories:
(Claude: done, although quite sparse, to be read by others)
7 Manpages
7.1 Compilation, Installation done
7.2 external provers done
7.1 Compilation, Installation (done)
7.2 external provers (done)
7.3 why3config (TODO Francois)
7.4 why3 (todo François)
7.5 whyml todo ?
7.4 why3 (TODO François)
7.5 whyml (TODO ?)
7.6 IDE (TODO, Claude)
7.7 whybench (TODO Francois)
7.8 why.conf (TODO Francois)
7.9 drivers (TODO Francois)
7.10 transformations (TODO)
8 API: Andrei + Francois
(should we really add that in the doc ?)
== IDE ==
......@@ -37,10 +39,9 @@
* add "context" options (partially done)
** semantics not clear, should be clarified, documented and
implemented accordingly
* add transf "inline goal" (TODO)
** not urgent
* add transf "inline goal" (TODO, not urgent)
* add button "remove" (TODO: implement)
* add button "replay" (TODO: implement)
* add button "replay" (TODO, not urgent)
** semantics: replay obsolete proofs
== Misc ==
......@@ -57,7 +58,7 @@
* make install (done)
* make export (TODO: JCF)
* "make -j" (done)
* META for ocamlfind (Done)
* META for ocamlfind (done)
* headers (done)
......
......@@ -13,3 +13,10 @@ theory Test
goal SquareNonNeg : forall x : int. 0 <= x * x
goal ZeroLessOne : 0 <= 1
end
theory MinMax
use import int.MinMax
goal G : min 1 (min 3 2) = 1
end
theory Prop
logic a
logic b
goal G : a and b -> a
goal G2 : G -> true
end
\ No newline at end of file
......@@ -51,7 +51,11 @@ The Why3 executables are then available in subdirectory \texttt{bin/}.
\subsection{Installation of the Why3 library}
\label{sec:installlib}
TODO
By default, the Why3 library is not installed. It can be installed using
\begin{verbatim}
make byte opt
make install_lib
\end{verbatim}
\section{Installation of external provers}
......@@ -170,9 +174,15 @@ used to provide other informations :
% TODO (pour plus tard)
% \section{The \texttt{why3ml} tool}
\section{The \texttt{why3ide} tool}
[TO BE COMPLETED]
\section{The \texttt{why3ide} GUI}
\label{sec:ideref}
The basic usage of the GUI is described by the tutorial of
Section~\ref{sec:gui}. We describe here the command-line options and
the actions of the various menus and buttons of the interface.
\subsection{Command-line options}
\begin{description}
......
......@@ -210,7 +210,8 @@ hello_proof.why HelloProof G3 : Valid (0.01s)
\end{verbatim}
Finally, a transformation to apply to goals before proving them can be
specified. To know the unique identifier associated to transformations, do as follows.
specified. To know the unique identifier associated to
transformations, do as follows.
\begin{verbatim}
> why3 --list-transforms
Known non-splitting transformations:
......
......@@ -9,7 +9,8 @@ valid "Valid"
invalid "Invalid"
unknown "I don't know" "Unknown"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
time "Valid (\\(.*\\))" "0:0:\\1"
time "Valid (%s)"
time "cpulimit_time : %s s"
(* À discuter *)
transformation "simplify_recursive_definition"
......
......@@ -7,7 +7,7 @@ filename "%f-%t-%g.smt"
valid "unsat"
unknown "\\bunknown\\b\\|\\bsat\\b" "Unknown"
time "cpulimit_time : \\([0-9]+.[0-9]*\\) s" "0:0:\\1"
time "cpulimit_time : %s s"
(* À discuter *)
transformation "simplify_recursive_definition"
......
......@@ -8,6 +8,7 @@ filename "%f-%t-%g.gappa"
valid 0
unknown "no contradiction was found\\|some enclosures were not satisfied" "Unknown"
time "cpulimit_time : %s s"
transformation "simplify_recursive_definition"
transformation "inline_trivial"
......
......@@ -7,7 +7,7 @@ filename "%f-%t-%g.sx"
valid "\\bValid\\b"
unknown "\\bInvalid\\b" "Unknown"
time "cpulimit_time : \\([0-9]+.[0-9]*\\) s" "0:0:\\1"
time "cpulimit_time : %s s"
transformation "simplify_recursive_definition"
transformation "inline_trivial"
......
......@@ -10,8 +10,9 @@ timeout "Resource limit exceeded"
timeout "CPU time limit exceeded"
unknown "No Proof Found" "Unknown"
fail "Failure.*" "\"\\0\""
time "\\([0-9]+:[0-9]+:[0-9]+.[0-9]*\\) on the problem" "\\1"
time "Total time[ ]*: \\([0-9]+.[0-9]*\\) s" "0:0:\\1"
time "cpulimit_time : %s s"
(* time "%h:%m:%s on the problem" *)
(* time "Total time[ ]*: %s s" *)
(* to be improved *)
......
......@@ -7,6 +7,7 @@ filename "%f-%t-%g.smt"
valid "^unsat"
unknown "^\\(unknown\\|sat\\)" "Unknown"
time "cpulimit_time : %s s"
(* À discuter *)
transformation "simplify_recursive_definition"
......
......@@ -7,6 +7,7 @@ filename "%f-%t-%g.smt"
valid "\\bunsat\\b"
unknown "\\bunknown\\b\\|\\bsat\\b\\|feature not supported: non linear problem" "Unknown"
time "cpulimit_time : %s s"
(* À discuter *)
transformation "simplify_recursive_definition"
......
......@@ -7,7 +7,8 @@ filename "%f-%t-%g.smt"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
time "cpulimit_time : \\([0-9]+.[0-9]*\\) s" "0:0:\\1"
time "cpulimit_time : %s s"
(* À discuter *)
transformation "simplify_recursive_definition"
......@@ -133,8 +134,11 @@ theory int.EuclideanDivision
end
theory transform.array.Array
syntax logic get "(select %1 %2)"
syntax logic get "(store %1 %2)"
syntax logic get "(select %1 %2)"
syntax logic set "(store %1 %2)"
remove prop Select_eq
remove prop Select_neq
end
(*
......
......@@ -11,7 +11,7 @@ version_ok = "0.92"
version_ok = "0.91"
version_old = "0.9"
version_old = "0.8"
command = "why3-cpulimit %t %m %e %f"
command = "why3-cpulimit %t %m yes %e %f"
driver = "drivers/alt_ergo.drv"
[ATP cvc3]
......@@ -21,7 +21,7 @@ version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
version_ok = "2.2"
version_old = "2.1"
command = "why3-cpulimit_time 0 %m %e -timeout %t -lang smt %f 2>&1"
command = "why3-cpulimit 0 %m yes %e -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3.drv"
[ATP yices]
......@@ -32,7 +32,7 @@ version_regexp = "[Yices ]*\\([^ \n]+\\)"
version_ok = "1.0.27"
version_old = "1.0.17"
version_old = "1.0.24"
command = "why3-cpulimit %t %m %e -smt 2>&1"
command = "why3-cpulimit %t %m yes %e -smt 2>&1"
driver = "drivers/yices.drv"
[ATP eprover]
......@@ -40,7 +40,7 @@ name = "Eprover"
exec = "eprover"
version_switch = "--version"
version_regexp = "E \\([^\n]+\\)"
command = "why3-cpulimit 0 %m %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
command = "why3-cpulimit 0 %m yes %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
driver = "drivers/tptp.drv"
[ATP gappa]
......@@ -54,7 +54,7 @@ version_old = "0.12.2"
version_old = "0.12.1"
version_old = "0.12.0"
version_old = "0.11.2"
command = "why3-cpulimit %t %m %e %f 2>&1"
command = "why3-cpulimit %t %m yes %e %f 2>&1"
driver = "drivers/gappa.drv"
[ATP simplify]
......@@ -67,7 +67,7 @@ version_switch = "-version"
version_regexp = "Simplify version \\([^ \n,]+\\)"
version_ok = "1.5.5"
version_ok = "1.5.4"
command = "why3-cpulimit_time %t %m %e %f 2>&1"
command = "why3-cpulimit %t %m yes %e %f 2>&1"
driver = "drivers/simplify.drv"
[ATP spass]
......@@ -75,7 +75,7 @@ name = "Spass"
exec = "SPASS"
version_switch = "-TPTP || true"
version_regexp = "SPASS V \\([^ \n\t]+\\)"
command = "why3-cpulimit 0 %m %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f 2>&1"
command = "why3-cpulimit 0 %m yes %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f 2>&1"
driver = "drivers/tptp.drv"
[ATP verit]
......@@ -84,7 +84,7 @@ exec = "veriT"
exec = "verit"
version_switch = "--help"
version_regexp = "Version: \\([^ \n\r]+\\)"
command = "why3-cpulimit %t %m %e %f 2>&1"
command = "why3-cpulimit %t %m yes %e %f 2>&1"
driver = "drivers/verit.drv"
[ATP z3]
......@@ -96,7 +96,7 @@ version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "2.2"
version_old = "2.1"
version_old = "1.3"
command = "why3-cpulimit_time %t %m %e -smt %f 2>&1"
command = "why3-cpulimit %t %m yes %e -smt %f 2>&1"
driver = "drivers/z3.drv"
[ITP coq]
......
......@@ -20,6 +20,54 @@
open Format
open Sysutil
(** time regexp "%h:%m:%s" *)
type timeunit =
| Hour
| Min
| Sec
| Msec
type regexptime = {
re : Str.regexp;
group : timeunit array; (*ieme corresponds to the group i + 1*)
}
let regexptime s =
let cmd_regexp = Str.regexp "%\\(.\\)" in
let nb = ref 0 in
let l = ref [] in
let add_unit x = l := (!nb,x) :: !l; incr nb; "\\([0-9]+.?[0-9]*\\)" in
let replace s = match Str.matched_group 1 s with
| "%" -> "%"
| "h" -> add_unit Hour
| "m" -> add_unit Min
| "s" -> add_unit Sec
| "i" -> add_unit Msec
| _ -> failwith "unknown format specifier, use %%h, %%m, %%s, %%i"
in
let s = Str.global_substitute cmd_regexp replace s in
let group = Array.make !nb Hour in
List.iter (fun (i,u) -> group.(i) <- u) !l;
{ re = Str.regexp s; group = group}
let rec grep_time out = function
| [] -> None
| re :: l ->
begin try
ignore (Str.search_forward re.re out 0);
let t = ref 0. in
Array.iteri (fun i u ->
let v = float_of_string (Str.matched_group (succ i) out) in
match u with
| Hour -> t := !t +. v *. 3600.
| Min -> t := !t +. v *. 60.
| Sec -> t := !t +. v
| Msec -> t := !t +. v /. 1000.) re.group;
Some !t
with _ -> grep_time out l end
(** *)
type prover_answer =
| Valid
| Invalid
......@@ -59,16 +107,6 @@ let rec grep out l = match l with
| HighFailure -> assert false
with Not_found -> grep out l end
let rec grep_time out = function
| [] -> None
| (re,pa) :: l ->
begin try
ignore (Str.search_forward re out 0);
let stime = (Str.replace_matched pa out) in
Some (Scanf.sscanf stime "%f:%f:%f"
(fun h m s -> h *. 3600. +. m *. 60. +. s))
with _ -> grep_time out l end
let debug = Debug.register_flag "call_prover"
......@@ -103,7 +141,8 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
| "f" -> on_stdin := false; file
| "t" -> on_timelimit := true; string_of_int timelimit
| "m" -> string_of_int memlimit
| _ -> failwith "unknown format specifier, use %%f, %%t or %%m"
| "b" -> string_of_int (memlimit * 1024)
| _ -> failwith "unknown format specifier, use %%f, %%t, %%m or %%b"
in
let cmd = Str.global_substitute cmd_regexp (replace "") command in
let on_stdin = !on_stdin in
......@@ -133,7 +172,7 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
let time = Util.default_option time (grep_time out regexpstime) in
let ans = match ans with
| HighFailure when !on_timelimit && timelimit > 0
&& time >= (float timelimit -. 0.1) -> Timeout
&& time >= (0.9 *. float timelimit) -> Timeout
| _ -> ans
in
{ pr_answer = ans;
......
......@@ -56,6 +56,11 @@ val debug : Debug.flag
If set [call_on_buffer] prints on stderr the commandline called
and the output of the prover. *)
(** time parser *)
type regexptime
val regexptime : string -> regexptime
(** *)
type post_prover_call = unit -> prover_result
(** Thread-unsafe closure that processes a prover's output
and returns the final result. Once again: this closure
......@@ -70,7 +75,7 @@ val call_on_buffer :
?timelimit : int ->
?memlimit : int ->
regexps : (Str.regexp * prover_answer) list ->
regexpstime : (Str.regexp * string) list ->
regexpstime : regexptime list ->
exitcodes : (int * prover_answer) list ->
filename : string ->
Buffer.t -> bare_prover_call
......
......@@ -42,7 +42,7 @@ type driver = {
drv_meta : (theory * Stdecl.t) Mid.t;
drv_meta_cl : (theory * Stdecl.t) Mid.t;
drv_regexps : (Str.regexp * prover_answer) list;
drv_regexpstime : (Str.regexp * string) list;
drv_regexpstime : Call_provers.regexptime list;
drv_exitcodes : (int * prover_answer) list;
}
......@@ -90,7 +90,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
| RegexpTimeout s -> add_to_list regexps (Str.regexp s, Timeout)
| RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown t)
| RegexpFailure (s,t) -> add_to_list regexps (Str.regexp s, Failure t)
| RegexpTime (r,s) -> add_to_list regexpstime (Str.regexp r,s)
| RegexpTime r -> add_to_list regexpstime (Call_provers.regexptime r)
| ExitCodeValid s -> add_to_list exitcodes (s, Valid)
| ExitCodeInvalid s -> add_to_list exitcodes (s, Invalid)
| ExitCodeTimeout s -> add_to_list exitcodes (s, Timeout)
......
......@@ -50,7 +50,7 @@ type global =
| RegexpTimeout of string
| RegexpUnknown of string * string
| RegexpFailure of string * string
| RegexpTime of string * string
| RegexpTime of string
| ExitCodeValid of int
| ExitCodeInvalid of int
| ExitCodeTimeout of int
......
......@@ -57,7 +57,7 @@ global:
| VALID STRING { RegexpValid $2 }
| INVALID STRING { RegexpInvalid $2 }
| TIMEOUT STRING { RegexpTimeout $2 }
| TIME STRING STRING { RegexpTime ($2,$3) }
| TIME STRING { RegexpTime ($2) }
| UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
| FAIL STRING STRING { RegexpFailure ($2, $3) }
| VALID INTEGER { ExitCodeValid $2 }
......
......@@ -65,15 +65,16 @@ type info = {
let rec print_type info fmt ty = match ty.ty_node with
| Tyvar _ -> unsupported "smt : you must encode the polymorphism"
| Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with
| Some s -> syntax_arguments s (print_type info) fmt tl
| None -> fprintf fmt "%a%a" (print_tyapp info) tl print_ident ts.ts_name
end
| Tyapp (ts, []) -> begin match query_syntax info.info_syn ts.ts_name with
| Some s -> syntax_arguments s (print_type info) fmt []
| None -> fprintf fmt "%a" print_ident ts.ts_name
end
| Tyapp (_, _) -> unsupported "smt : you must encode the complexe type"
and print_tyapp info fmt = function
| [] -> ()
| [ty] -> fprintf fmt "%a " (print_type info) ty
| tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl
(* and print_tyapp info fmt = function *)
(* | [] -> () *)
(* | [ty] -> fprintf fmt "%a " (print_type info) ty *)
(* | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl *)
let print_type info fmt = catch_unsupportedType (print_type info fmt)
......@@ -223,15 +224,15 @@ let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
let barrays task =
let fold barrays =
function
| [MAts tst;MAts tsk;MAts tse] ->
let extract_ty ts =
if ts.ts_args <> [] then
unsupported "smtv1 : type with argument are not supported";
match ts.ts_def with
| Some ty -> ty
| None -> ty_app ts [] in
Mts.add tst (extract_ty tsk,extract_ty tse) barrays
| _ -> barrays in
| [MAts tst;MAty tyk;MAty tye] ->
(* let extract_ty ts = *)
(* if ts.ts_args <> [] then *)
(* unsupported "smtv1 : type with argument are not supported"; *)
(* match ts.ts_def with *)
(* | Some ty -> ty *)
(* | None -> ty_app ts [] in *)
Mts.add tst (tyk,tye) barrays
| _ -> assert false in
Task.on_meta Encoding_arrays.meta_mono_array fold Mts.empty task
let print_task pr thpr fmt task =
......
......@@ -27,22 +27,46 @@
#include <sys/types.h>
#include <sys/time.h>
#include <time.h>
#include <sys/times.h>
#include <sys/resource.h>
#include <stdio.h>
#include <stdlib.h>
#include <unistd.h>
#include <errno.h>
#include <string.h>
#include <sys/wait.h>
int main(int argc, char *argv[]) {
int timelimit, memlimit;
struct rlimit res;
if (argc < 4) {
if (argc < 5) {
fprintf(stderr, "usage: %s <time limit in seconds> \
<virtual memory limit in MiB> <command>\n\
<virtual memory limit in MiB> <print time yes|no> <command>\n\
a null value sets no limit (keeps the actual limit)\n", argv[0]);
return 1;
return EXIT_FAILURE;
}
/* Fork if requested */
if(strcmp("yes",argv[3]) == 0){
int pid = fork ();
if (pid == -1){
perror("fork");
exit(EXIT_FAILURE);
} else if (pid == 0){
/* The child continue to execute the program */
} else {
/* The parent will not exit this condition */
int status;
waitpid(pid, &status, 0);
struct tms tms;
times(&tms);
double time = (double)((tms.tms_cutime + tms.tms_cstime + 0.0)
/ sysconf(_SC_CLK_TCK));
fprintf(stdout, "cpulimit_time : %f s\n",time);
return status;
}
}
/* get time limit in seconds from command line */
......@@ -66,8 +90,10 @@ a null value sets no limit (keeps the actual limit)\n", argv[0]);
}
/* execute the command */
execvp(argv[3],argv+3);
fprintf(stderr, "%s: exec of '%s' failed (%s)\n",argv[0],argv[3],strerror(errno));
return 1;
execvp(argv[4],argv+4);
fprintf(stderr, "%s: exec of '%s' failed (%s)\n",
argv[0],argv[4],strerror(errno));
return EXIT_FAILURE;
}
......@@ -219,12 +219,19 @@ let gen_tvar su =
Ssubst.fold fold su su in
Ssubst.fold aux su (Ssubst.singleton (Mtv.empty))
(* find all the possible instantiation which can give a type of env.keep *)
let ty_quant env =
let rec add_vs s ty =
let s = ty_fold add_vs s ty in
match ty.ty_node with
| Tyapp(app,_) when ts_equal app env.poly_ts ->
Mty.fold (fun uty _ s -> Ssubst.add (ty_match Mtv.empty ty uty) s)
Mty.fold (fun uty _ s ->
try
Ssubst.add (ty_match Mtv.empty ty uty) s
with Ty.TypeMismatch _ ->
(* No instantiation possible *)
s
)
env.keep s
| _ -> s in
f_ty_fold add_vs Ssubst.empty
......@@ -320,7 +327,7 @@ let collect_arrays poly_ts tds =
Sts.fold extract tds Mty.empty
let meta_mono_array = register_meta "encoding_arrays : mono_arrays"
[MTtysymbol;MTtysymbol;MTtysymbol]
[MTtysymbol;MTty;MTty]
(* Some general env creation function *)
let create_env env task thpoly tds =
......
......@@ -150,7 +150,7 @@ let fold tenv taskpre task =
| ls, None -> conv_ls tenv ud ls, None
| _ -> Printer.unsupportedDecl d "use eliminate_definition"
in
decl_ud ud (add_logic_decl task (List.map conv ll))
add_logic_decl (decl_ud ud task) (List.map conv ll)
| Dind _ ->
Printer.unsupportedDecl d "use eliminate_inductive"
| Dprop _ ->
......@@ -165,12 +165,13 @@ let fold tenv taskpre task =
| MAty ty -> MAty (conv_ty tenv ud ty)
| MAts {ts_name = name; ts_args = []; ts_def = Some ty} ->
MAts (conv_ts tenv ud name ty)
| MAts {ts_args = []; ts_def = None} as x -> x
| MAts _ -> raise Exit
| MAls ls -> MAls (conv_ls tenv ud ls)
| MApr _ -> raise Exit
| MAstr _ as s -> s
| MAint _ as i -> i in
decl_ud ud (add_meta task meta (List.map map ml))
add_meta (decl_ud ud task) meta (List.map map ml)
with
| Printer.UnsupportedType _
| Exit -> add_tdecl task taskpre.task_decl
......
......@@ -40,10 +40,16 @@ theory MinMax
lemma Min_sym: forall x y:t. ge x y -> min x y = min y x
(*
logic min (x y : t) : t
axiom Min_def : if ge x y then min x y = y else min x y = x
logic min (x y : t) : t
axiom Min_def : if ge x y then min x y = y else min x y = x
logic max (x y : t) : t
axiom Max_def : if ge x y then max x y = x else max x y = y
axiom Max_def : if ge x y then max x y = x else max x y = y
*)
(*
logic min (x y : t) : t = if ge x y then y else x
logic max (x y : t) : t = if ge x y then x else y
*)
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