Skip to content

why3
why3
Commit fd402ea5 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

- rework Call_provers, remove calling primitives from Driver 

- accept timeout regexps in drivers
- do not take command line from drivers
parent a3f4f927
Hide whitespace changes
Inline Side-by-side
Showing with 260 additions and 316 deletions
drivers/alt_ergo.drv
View file @ fd402ea5
......@@ -4,8 +4,7 @@
prelude "(* this is a prelude for Alt-Ergo*)"
printer "alt-ergo"
filename "%f-%t-%s.why"
call_on_file "alt-ergo %s"
filename "%f-%t-%g.why"
valid "Valid"
invalid "Invalid"
......
drivers/coq.drv
View file @ fd402ea5
printer "coq"
filename "%f_%t_%s.v"
call_on_file "coqc %s"
filename "%f_%t_%g.v"
prelude "(* generated by Why3's Coq driver *)"
......
drivers/cvc3.drv
View file @ fd402ea5
......@@ -4,8 +4,7 @@
prelude "(* this is a prelude for smtlib*)"
printer "smtv1"
filename "%f-%t-%s.smt"
call_on_stdin "cvc3 -lang smt"
filename "%f-%t-%g.smt"
valid "unsat"
unknown "\\bunknown\\b\\|\\bsat\\b" "Unknown"
......
drivers/why3.drv
View file @ fd402ea5
printer "why3"
filename "%f-%t-%s.why"
filename "%f-%t-%g.why"
theory BuiltIn
syntax type int "int"
......
drivers/why3_encoding_decorate.drv
View file @ fd402ea5
printer "why3"
filename "%f-%t-%s.why"
filename "%f-%t-%g.why"
transformations
"remove_logic_definition"
......
drivers/why3_inline_all.drv
View file @ fd402ea5
printer "why3"
filename "%f-%t-%s.why"
filename "%f-%t-%g.why"
(* À discuter *)
transformations
......
drivers/why3_split_conjunction.drv
View file @ fd402ea5
printer "why3"
filename "%f-%t-%s.why"
filename "%f-%t-%g.why"
(* À discuter *)
transformations
......
drivers/why3_total_elimination.drv
View file @ fd402ea5
printer "why3"
filename "%f-%t-%s.why"
filename "%f-%t-%g.why"
transformations
"compile_match"
......
drivers/z3.drv
View file @ fd402ea5
......@@ -4,9 +4,7 @@
prelude "(* this is a prelude for smtlib*)"
printer "smtv1"
filename "%f-%t-%s.smt"
call_on_file "z3 -smt %s"
call_on_stdin "z3 -smt -in"
filename "%f-%t-%g.smt"
valid "unsat"
unknown "unknown\\|sat|Fail" "Unknown"
......
src/driver/call_provers.ml
View file @ fd402ea5
......@@ -18,45 +18,111 @@
(**************************************************************************)
open Format
open Sysutil
type prover_answer =
type prover_answer =
| Valid
| Invalid
| Unknown of string
| Failure of string
| Timeout
| Unknown of string
| Failure of string
| HighFailure
type prover_result = {
pr_answer : prover_answer;
pr_output : string;
pr_time : float;
}
type prover_regexp = Str.regexp * prover_answer
let print_prover_answer fmt = function
| Valid -> fprintf fmt "Valid"
| Invalid -> fprintf fmt "Invalid"
| Timeout -> fprintf fmt "Timeout"
| Unknown s -> pp_print_string fmt s
| Failure s -> pp_print_string fmt s
| Timeout -> fprintf fmt "Timeout"
| HighFailure -> fprintf fmt "HighFailure"
type prover_result =
{ pr_time : float;
pr_answer : prover_answer;
pr_stderr : string;
pr_stdout : string}
let print_prover_result fmt pr =
let print_prover_result fmt pr =
fprintf fmt "%a (%.2fs)" print_prover_answer pr.pr_answer pr.pr_time;
if pr.pr_answer == HighFailure
then fprintf fmt "@\nstdout-stderr : \"%s\"" pr.pr_stdout;
if pr.pr_answer == HighFailure then
fprintf fmt "@\n@stdout-stderr:@\n%s@." pr.pr_output
type prover =
{ pr_call_stdin : string option; (* %f pour le nom du fichier *)
pr_call_file : string option;
pr_regexps : (Str.regexp * prover_answer) list;
(* \1,... sont remplacés *)
}
let rec grep out l = match l with
| [] -> HighFailure
| (re,pa)::l ->
begin try
ignore (Str.search_forward re out 0);
match pa with
| Valid | Invalid | Timeout -> pa
| Unknown s -> Unknown (Str.replace_matched s out)
| Failure s -> Failure (Str.replace_matched s out)
| HighFailure -> assert false
with Not_found -> grep out l end
exception CommandError
exception NoCommandlineProvided
let call_prover debug command regexps opt_cout buffer =
let t0 = Unix.time () in
let (cin,cout) as p = Unix.open_process command in
let cout = match opt_cout with Some c -> c | _ -> cout in
Buffer.output_buffer cout buffer; close_out cout;
let out = channel_contents cin in
let ret = Unix.close_process p in
let t1 = Unix.time () in
if debug then Format.eprintf "Call_provers: Command output:@\n%s@." out;
let ans = match ret with
| Unix.WSTOPPED n ->
if debug then Format.eprintf "Call_provers: stopped on signal %d" n;
HighFailure
| Unix.WSIGNALED n ->
if debug then Format.eprintf "Call_provers: killed by signal %d" n;
HighFailure
| Unix.WEXITED n ->
if debug then Format.eprintf "Call_provers: exited with status %d" n;
grep out regexps
in
{ pr_answer = ans;
pr_output = out;
pr_time = t1 -. t0 }
let call_on_buffer ?(debug=false) ?(suffix=".dump")
~command ~timelimit ~memlimit ~regexps buffer () =
let on_stdin = ref false in
let cmd_regexp = Str.regexp "%\\(.\\)" in
let replace filename s = match Str.matched_group 1 s with
| "%" -> "%"
| "f" -> on_stdin := false; filename
| "t" -> string_of_int timelimit
| "m" -> string_of_int memlimit
| _ -> failwith "unknown format specifier, use %%f, %%t or %%m"
in
let cmd_stdin = Str.global_substitute cmd_regexp (replace "") command in
if !on_stdin then call_prover debug cmd_stdin regexps None buffer
else
let fout,cout = Filename.open_temp_file "why" suffix in
try
let cmd = Str.global_substitute cmd_regexp (replace fout) command in
let res = call_prover debug cmd regexps (Some cout) buffer in
if not debug then Sys.remove fout;
res
with e ->
close_out cout;
if not debug then Sys.remove fout;
raise e
let call_on_formatter ?debug ?suffix
~command ~timelimit ~memlimit ~regexps formatter =
let buffer = Buffer.create 1024 in
let fmt = formatter_of_buffer buffer in
formatter fmt; pp_print_flush fmt ();
call_on_buffer ?debug ?suffix ~command ~timelimit ~memlimit ~regexps buffer
let call_on_file ?debug ?suffix
~command ~timelimit ~memlimit ~regexps filename =
let buffer = file_contents_buf filename in
call_on_buffer ?debug ?suffix ~command ~timelimit ~memlimit ~regexps buffer
(*
let is_true_cygwin = Sys.os_type = "Cygwin"
(* this should be replaced by a proper use of fork/waitpid() *)
......@@ -70,7 +136,7 @@ let cpulimit = (
(fun s ->
(*let r = Sys.command (s^" 1 echo") in
if r=0 then (tmp:=s; raise Exit)*)
let pid = Unix.create_process s [|s;"1";"true"|]
let pid = Unix.create_process s [|s;"1";"true"|]
Unix.stdin Unix.stdout Unix.stderr in
match Unix.waitpid [] pid with
| _,Unix.WEXITED 0 -> (tmp:=s; raise Exit)
......@@ -80,8 +146,8 @@ let cpulimit = (
failwith ("need shell command among: "^
(String.concat " ," cpulimit_commands))
with Exit -> tmp)
(* Utils *)
......@@ -103,19 +169,19 @@ let timed_sys_command ?formatter ?buffer ?(debug=false) ?timeout cmd =
begin try
(match formatter with
| None -> ()
| Some formatter ->
| Some formatter ->
let fmt = formatter_of_out_channel cout in
formatter fmt);
with Sys_error s ->
with Sys_error s ->
if debug then Format.eprintf "Sys_error : %s@." s
end;
(* Write the buffer to the stdin of the prover *)
begin try
(match buffer with
| None -> ()
| Some buffer ->
| Some buffer ->
Buffer.output_buffer cout buffer);
with Sys_error s ->
with Sys_error s ->
if debug then Format.eprintf "Sys_error : %s@." s
end;
close_out cout;
......@@ -152,17 +218,17 @@ let grep re str =
(* in *)
(* cmd,timed_sys_command ~debug timeout cmd *)
(* | _ -> invalid_arg *)
(* "Calldp.gen_prover_call : filename must be given if the prover
(* "Calldp.gen_prover_call : filename must be given if the prover
can't use stdin." *)
(* in *)
let treat_result pr (t,c,outerr) =
let answer =
let treat_result pr (t,c,outerr) =
let answer =
match c with
| Unix.WSTOPPED 24 | Unix.WSIGNALED 24 | Unix.WEXITED 124
| Unix.WEXITED 152 ->
(* (*128 +*) SIGXCPU signal (i.e. 24, /usr/include/bits/signum.h) *)
| Unix.WSTOPPED 24 | Unix.WSIGNALED 24 | Unix.WEXITED 124
| Unix.WEXITED 152 ->
(* (*128 +*) SIGXCPU signal (i.e. 24, /usr/include/bits/signum.h) *)
(* TODO : if somebody use why_cpulimit to call "why -timeout
0", Why will think that he called why_cpulimit (WEXITED
152) and will return Timeout instead of exit 152. In fact
......@@ -175,7 +241,7 @@ let treat_result pr (t,c,outerr) =
let rec greps res = function
| [] -> HighFailure
| (r,pa)::l ->
if grep r res
if grep r res
then match pa with
| Valid | Invalid -> pa
| Unknown s -> Unknown (Str.replace_matched s res)
......@@ -190,42 +256,42 @@ let treat_result pr (t,c,outerr) =
(* *)
let check_prover prover =
let check_prover prover =
if prover.pr_call_file = None && prover.pr_call_stdin = None then
raise NoCommandlineProvided
let regexp_call_file = Str.regexp "%\\([a-z]\\)"
let rec on_file ?debug ?timeout pr filename =
let rec on_file ?debug ?timeout pr filename =
check_prover pr;
match pr.pr_call_file with
| Some cmd ->
let filename = if is_true_cygwin
then
let cin = Unix.open_process_in
| Some cmd ->
let filename = if is_true_cygwin
then
let cin = Unix.open_process_in
(sprintf "cygpath -am \"%s\"" filename) in
let f = input_line cin in
close_in cin; f
else filename in
let cmd =
let repl_fun s =
let cmd =
let repl_fun s =
match Str.matched_group 1 s with
| "s" -> filename
| _ -> assert false in (*TODO mettre une belle exception*)
Str.global_substitute regexp_call_file repl_fun cmd in
let res = timed_sys_command ?debug ?timeout cmd in
treat_result pr res
| None ->
| None ->
let formatter = Sysutil.file_contents_fmt filename in
on_formatter ?timeout ?debug pr formatter
and on_formatter ?debug ?timeout ?filename pr formatter =
check_prover pr;
match pr.pr_call_stdin with
| Some cmd ->
| Some cmd ->
let res = timed_sys_command ?debug ?timeout ~formatter cmd in
treat_result pr res
| None ->
| None ->
match filename with
| None -> raise NoCommandlineProvided
| Some filename -> Sysutil.open_temp_file ?debug filename
......@@ -239,13 +305,14 @@ and on_formatter ?debug ?timeout ?filename pr formatter =
let on_buffer ?debug ?timeout ?filename pr buffer =
check_prover pr;
match pr.pr_call_stdin with
| Some cmd ->
| Some cmd ->
let res = timed_sys_command ?debug ?timeout ~buffer cmd in
treat_result pr res
| None ->
| None ->
match filename with
| None -> raise NoCommandlineProvided
| Some filename -> Sysutil.open_temp_file ?debug filename
(fun file cout ->
Buffer.output_buffer cout buffer;
on_file ?timeout ?debug pr file)
*)
src/driver/call_provers.mli
View file @ fd402ea5
......@@ -17,59 +17,52 @@
(* *)
(**************************************************************************)
open Format
type prover_answer =
type prover_answer =
| Valid
| Invalid
| Unknown of string
| Failure of string
| Timeout
| Unknown of string
| Failure of string
| HighFailure
val print_prover_answer : formatter -> prover_answer -> unit
type prover_result =
{ pr_time : float;
pr_answer : prover_answer;
pr_stderr : string;
pr_stdout : string}
val print_prover_result : formatter -> prover_result -> unit
type prover_result = {
pr_answer : prover_answer;
pr_output : string;
pr_time : float;
}
type prover =
{ pr_call_stdin : string option; (* %f pour le nom du fichier *)
pr_call_file : string option;
pr_regexps : (Str.regexp * prover_answer) list;
(* \1,... sont remplacés *)
}
type prover_regexp = Str.regexp * prover_answer
exception CommandError
exception NoCommandlineProvided
val print_prover_answer : Format.formatter -> prover_answer -> unit
val print_prover_result : Format.formatter -> prover_result -> unit
val cpulimit : string ref
val call_on_buffer :
?debug : bool ->
?suffix : string ->
command : string ->
timelimit : int ->
memlimit : int ->
regexps : prover_regexp list ->
Buffer.t ->
(unit -> prover_result)
val on_file :
?debug:bool ->
?timeout:int ->
prover ->
string ->
prover_result
val call_on_formatter :
?debug : bool ->
?suffix : string ->
command : string ->
timelimit : int ->
memlimit : int ->
regexps : prover_regexp list ->
(Format.formatter -> unit) ->
(unit -> prover_result)
val on_formatter :
?debug:bool ->
?timeout:int ->
?filename:string -> (* used as the suffix of a tempfile if the prover can't
deal with stdin *)
prover ->
(formatter -> unit) ->
prover_result
val call_on_file :
?debug : bool ->
?suffix : string ->
command : string ->
timelimit : int ->
memlimit : int ->
regexps : prover_regexp list ->
string ->
(unit -> prover_result)
val on_buffer :
?debug:bool ->
?timeout:int ->
?filename:string -> (* used as the suffix of a tempfile if the prover can't
deal with stdin *)
prover ->
Buffer.t ->
prover_result
src/driver/driver.ml
View file @ fd402ea5
......@@ -28,6 +28,7 @@ open Task
open Register
open Env
open Driver_ast
open Call_provers
(* Utils from Str *)
......@@ -91,31 +92,20 @@ let errorm ?loc f =
(** creating drivers *)
type prover_answer =
Call_provers.prover_answer =
| Valid
| Invalid
| Unknown of string
| Failure of string
| Timeout
| HighFailure
type theory_driver = {
thd_prelude : string list;
thd_tsymbol : unit ;
}
type translation =
| Remove
| Syntax of string
| Tag of Sstr.t
let translation_union t1 t2 =
match t1, t2 with
| Remove, _ | _, Remove -> Remove
| ((Syntax _ as s), _) | (_,(Syntax _ as s)) -> s
| Tag s1, Tag s2 -> Tag (Sstr.union s1 s2)
let translation_union t1 t2 = match t1, t2 with
| Remove, _ | _, Remove -> Remove
| ((Syntax _ as s), _) | (_,(Syntax _ as s)) -> s
| Tag s1, Tag s2 -> Tag (Sstr.union s1 s2)
let print_translation fmt = function
| Remove -> fprintf fmt "remove"
......@@ -125,63 +115,30 @@ let print_translation fmt = function
type printer = (ident -> translation) -> formatter -> task -> unit
and driver = {
type driver = {
drv_env : env;
drv_printer : printer option;
drv_prover : Call_provers.prover;
drv_prelude : string list;
drv_filename : string option;
drv_transforms : task tlist_reg;
drv_thprelude : string list Mid.t;
drv_translations : (translation * translation) Mid.t
}
(*
and driver = {
drv_raw : raw_driver;
drv_clone : Theory.clone_map;
drv_used : Theory.use_map;
drv_env : env;
drv_thprelude : string list Hid.t;
(* the first is the translation only for this ident, the second is
also for representant *)
drv_theory : (translation * translation) Hid.t;
drv_with_task : translation Hid.t;
drv_translations : (translation * translation) Mid.t;
drv_regexps : Call_provers.prover_regexp list;
}
*)
(*
let print_driver fmt driver =
printf "drv_theory %a@\n"
(Pp.print_iter2 Hid.iter Pp.semi Pp.comma print_ident
(Pp.print_pair print_translation print_translation))
driver.drv_theory
*)
(** registering transformation *)
let (transforms : (string, task tlist_reg) Hashtbl.t)
= Hashtbl.create 17
let register_transform_l name transform =
Hashtbl.replace transforms name transform
let (transforms : (string, task tlist_reg) Hashtbl.t) = Hashtbl.create 17
let register_transform_l name trans = Hashtbl.replace transforms name trans
let register_transform name t = register_transform_l name (singleton t)
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []
(** registering printers *)
let (printers : (string, printer) Hashtbl.t) = Hashtbl.create 17
let register_printer name printer = Hashtbl.replace printers name printer
let list_printers () = Hashtbl.fold (fun k _ acc -> k::acc) printers []
(*
let () =
Dynlink.allow_only ["Theory";"Term";"Ident";"Transform";"Driver";
"Pervasives";"Format";"List";"Sys";"Unix"]
*)
let load_plugin dir (byte,nat) =
if not Config.why_plugins then errorm "Plugins not supported";
let file = if Config.Dynlink.is_native then nat else byte in
......@@ -220,7 +177,6 @@ let check_syntax loc s len =
"invalid indice of argument \"%%%i\" this logic has only %i argument"
i len) s
let load_rules env (premap,tmap) {thr_name = loc,qualid; thr_rules = trl} =
let id,qfile = qualid_to_slist qualid in
let th = try
......@@ -244,7 +200,7 @@ let load_rules env (premap,tmap) {thr_name = loc,qualid; thr_rules = trl} =
try
premap,add_htheory tmap c
(ns_find_pr th.th_export q).pr_name Remove
with Not_found -> errorm ~loc "Unknown axioms %s"
with Not_found -> errorm ~loc "Unknown proposition %s"
(string_of_qualid qualid q)
end
| Rsyntaxls ((loc,q),s) ->
......@@ -302,14 +258,13 @@ let load_driver file env =
let f = load_file file in
let prelude = ref [] in
let printer = ref None in
let call_stdin = ref None in
let call_file = ref None in
let filename = ref None in
let ltransforms = ref None in
let regexps = ref [] in
let set_or_raise loc r v error =
if !r <> None then errorm ~loc "duplicate %s" error
else r := Some v in
else r := Some v
in
let add (loc, g) = match g with
| Printer _ when !printer <> None ->
errorm ~loc "duplicate printer"
......@@ -318,10 +273,9 @@ let load_driver file env =
| Printer s ->
errorm ~loc "unknown printer %s" s
| Prelude s -> prelude := s :: !prelude
| CallStdin s -> set_or_raise loc call_stdin s "callstdin"
| CallFile s -> set_or_raise loc call_file s "callfile"
| RegexpValid s -> regexps:=(s,Valid)::!regexps
| RegexpInvalid s -> regexps:=(s,Invalid)::!regexps
| RegexpTimeout s -> regexps:=(s,Timeout)::!regexps
| RegexpUnknown (s1,s2) -> regexps:=(s1,Unknown s2)::!regexps
| RegexpFailure (s1,s2) -> regexps:=(s1,Failure s2)::!regexps
| Filename s -> set_or_raise loc filename s "filename"
......@@ -332,7 +286,9 @@ let load_driver file env =
let regexps = List.map (fun (s,a) -> (Str.regexp s,a)) !regexps in
let trans r =
let transformations = match !r with
| None -> [] | Some l -> l in
| Some l -> l
| None -> []
in
List.fold_left
(fun acc (loc,s) ->
let t =
......@@ -340,21 +296,21 @@ let load_driver file env =
with Not_found -> errorm ~loc "unknown transformation %s" s in
compose_l acc t
)
identity_l transformations in
let transforms = trans ltransforms in
let (premap,tmap) =
List.fold_left (load_rules env) (Mid.empty,Mid.empty) f.f_rules in
identity_l transformations
in
let transforms = trans ltransforms in
let (premap,tmap) =
List.fold_left (load_rules env) (Mid.empty,Mid.empty) f.f_rules
in
{
drv_env = env;
drv_printer = !printer;
drv_prover = {Call_provers.pr_call_stdin = !call_stdin;
pr_call_file = !call_file;
pr_regexps = regexps};
drv_prelude = !prelude;
drv_filename = !filename;
drv_transforms = transforms;
drv_thprelude = premap;
drv_translations = tmap
drv_translations = tmap;
drv_regexps = regexps;
}
(** querying drivers *)
......@@ -384,6 +340,8 @@ let syntax_arguments s print fmt l =
print fmt args.(i-1) in
global_substitute_fmt regexp_arg_pos repl_fun s fmt
let get_regexps drv = drv.drv_regexps
(** using drivers *)
let apply_transforms drv =
......@@ -409,60 +367,26 @@ let print_prelude drv used fmt =
fprintf fmt "@."
let print_task drv fmt task = match drv.drv_printer with
| None -> errorm "no printer"
| None ->
errorm "no printer"
| Some f ->
print_prelude drv (task_used task) fmt;
f (query_ident drv (task_clone task)) fmt task
let regexp_filename = Str.regexp "%\\([a-z]\\)"
let filename_of_goal drv filename theory_name task =
match drv.drv_filename with
| None -> errorm "no filename syntax given"
| Some f ->
let pr_name = (task_goal task).pr_name in
let repl_fun s =
let i = matched_group 1 s in
match i with
| "f" -> filename
| "t" -> theory_name
| "s" -> pr_name.id_short
| _ -> errorm "substitution variable are only %%f %%t and %%s" in
global_substitute regexp_filename repl_fun f
let file_printer =
create_ident_printer ~sanitizer:(sanitizer char_to_alnumus char_to_alnumus)
[]
let call_prover_on_file ?debug ?timeout drv filename =
Call_provers.on_file ?debug ?timeout drv.drv_prover filename
let call_prover_on_formatter ?debug ?timeout ?filename drv ib =
Call_provers.on_formatter ?debug ?timeout ?filename drv.drv_prover ib
let call_prover_on_buffer ?debug ?timeout ?filename drv ib =
Call_provers.on_buffer ?debug ?timeout ?filename drv.drv_prover ib
let call_prover ?debug ?timeout drv task =
let filename =
match drv.drv_filename with
| None -> None
| Some _ -> Some (filename_of_goal drv "why" "call_prover" task) in
let formatter fmt = print_task drv fmt task in
call_prover_on_formatter ?debug ?timeout ?filename drv formatter
let call_prover_ext ?debug ?timeout drv task =
let filename =
match drv.drv_filename with
| None -> None
| Some _ -> Some (filename_of_goal drv "why" "call_prover" task) in
let formatter fmt = print_task drv fmt task in
let buf = Buffer.create 64 in
let fmt = formatter_of_buffer buf in
formatter fmt;
(fun () -> call_prover_on_buffer ?debug ?timeout ?filename drv buf)
let file_of_task drv input_file theory_name task =
let filename_regexp = Str.regexp "%\\(.\\)" in