Commit e470f34e authored by Francois Bobot's avatar Francois Bobot

ajout de quoi faire l'appel au prouveur, pas encore connecte a driver.ml

parent decf673c
......@@ -55,9 +55,9 @@ PDFVIEWER = @PDFVIEWER@
INCLUDES = -I src/core -I src/util -I src/parser -I src/output \
-I src/transform -I src/programs -I src
BFLAGS = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cma
BFLAGS = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cma unix.cma
# no -warn-error because some do not compile all files (e.g. those linked to APRON)
OFLAGS = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cmxa
OFLAGS = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cmxa unix.cmxa
COQC7 = @COQC7@
COQC8 = @COQC8@
......@@ -110,7 +110,7 @@ doc/version.tex src/version.ml: Version version.sh config.status
CORE_CMO := ident.cmo ty.cmo term.cmo theory.cmo pretty.cmo
CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
UTIL_CMO := pp.cmo loc.cmo util.cmo hashcons.cmo
UTIL_CMO := pp.cmo loc.cmo util.cmo hashcons.cmo sysutil.cmo
UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))
PARSER_CMO := parser.cmo lexer.cmo typing.cmo
......@@ -120,7 +120,7 @@ TRANSFORM_CMO := transform.cmo simplify_recursive_definition.cmo \
inlining.cmo
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
OUTPUT_CMO := driver_parser.cmo driver_lexer.cmo driver.cmo \
OUTPUT_CMO := call_provers.cmo driver_parser.cmo driver_lexer.cmo driver.cmo \
print_real.cmo alt_ergo.cmo why3.cmo
OUTPUT_CMO := $(addprefix src/output/,$(OUTPUT_CMO))
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
type prover_answer =
| Valid
| Invalid
| Unknown of string
| Failure of string
| Timeout
| HighFailure
type prover_result =
{ pr_time : float;
pr_answer : prover_answer;
pr_stderr : string;
pr_stdout : string}
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 *)
}
exception CommandError
exception NoCommandlineProvided
let cpulimit = ref "timeout" (*"why-cpulimit"*)
(* Utils *)
let remove_file ?(debug=false) f =
if not debug then try Sys.remove f with _ -> ()
(*let environment = Unix.environment ()*)
let timed_sys_command ?stdin ?(debug=false) ?timeout cmd =
let t0 = Unix.times () in
if debug then Format.eprintf "command line: %s@." cmd;
let cmd = match timeout with
| None -> Format.sprintf "%s 2>&1" cmd
| Some timeout -> Format.sprintf "%s %d %s 2>&1" !cpulimit timeout cmd in
let (cin,cout) as p = Unix.open_process cmd in
(match stdin with
| None -> ()
| Some stdin -> Buffer.output_buffer cout stdin);
close_out cout;
let out = Sysutil.channel_contents cin in
let ret = Unix.close_process p in
let t1 = Unix.times () in
let cpu_time = t1.Unix.tms_cutime -. t0.Unix.tms_cutime in
if debug then Format.eprintf "Calldp : Command output : %s@." out;
(cpu_time,ret,out)
let grep re str =
try
let _ = Str.search_forward re str 0 in true
with Not_found -> false
(* match buffers,p.DpConfig.stdin_switch,filename with *)
(* | None,_, Some f -> *)
(* let cmd = sprintf "%s %s %s %s" *)
(* p.DpConfig.command p.DpConfig.command_switches switch f *)
(* in *)
(* cmd,timed_sys_command ~debug timeout cmd *)
(* | Some buffers, Some stdin_s, _ -> *)
(* let cmd = sprintf "%s %s %s %s" *)
(* p.DpConfig.command p.DpConfig.command_switches switch stdin_s *)
(* in *)
(* cmd,timed_sys_command ~stdin:buffers ~debug timeout cmd *)
(* | Some buffers, None, Some f -> *)
(* let f = Filename.temp_file "" f in *)
(* let cout = open_out f in *)
(* List.iter (Buffer.output_buffer cout) buffers; *)
(* close_out cout; *)
(* let cmd = sprintf "%s %s %s %s" *)
(* p.DpConfig.command p.DpConfig.command_switches switch f *)
(* in *)
(* cmd,timed_sys_command ~debug timeout cmd *)
(* | _ -> invalid_arg *)
(* "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 =
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) *)
Timeout
| Unix.WSTOPPED _ | Unix.WSIGNALED _ -> HighFailure
| Unix.WEXITED c ->
let rec greps res = function
| [] -> HighFailure
| (r,pa)::l ->
if grep r res
then match pa with
| Valid | Invalid -> pa
| Unknown s -> Unknown (Str.replace_matched s res)
| Failure s -> Failure (Str.replace_matched s res)
| Timeout | HighFailure -> assert false
else greps outerr l in
greps outerr pr.pr_regexps in
{ pr_time = t;
pr_answer = answer;
pr_stderr = ""; (*Fill it with something real*)
pr_stdout = outerr} (* Split it in two...*)
(* *)
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-f]\\)"
let rec on_file ?debug ?timeout pr filename =
check_prover pr;
match pr.pr_call_file with
| Some cmd ->
let cmd =
let repl_fun s =
match Str.matched_group 1 s with
| "f" -> 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 ->
let buf = Sysutil.file_contents_buf filename in
on_buffer ?timeout ?debug pr buf
and on_buffer ?debug ?timeout ?filename pr buf =
check_prover pr;
match pr.pr_call_file with
| Some cmd ->
let res = timed_sys_command ?debug ?timeout ~stdin:buf cmd in
treat_result pr res
| None ->
match filename with
| None -> raise NoCommandlineProvided
| Some filename -> Sysutil.open_temp_file filename
(fun file cout ->
Buffer.output_buffer cout buf;
on_file ?timeout ?debug pr file)
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
type prover_answer =
| Valid
| Invalid
| Unknown of string
| Failure of string
| Timeout
| HighFailure
type prover_result =
{ pr_time : float;
pr_answer : prover_answer;
pr_stderr : string;
pr_stdout : string}
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 *)
}
exception CommandError
exception NoCommandlineProvided
val cpulimit : string ref
val on_file :
?debug:bool ->
?timeout:int ->
prover ->
string ->
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
......@@ -86,12 +86,14 @@ let errorm ?loc f =
(** creating drivers *)
type prover_answer =
type prover_answer =
Call_provers.prover_answer =
| Valid
| Invalid
| Unknown of string
| Failure of string
| Timeout
| HighFailure
type theory_driver = {
thd_prelude : string option;
......
......@@ -53,11 +53,13 @@ val filename_of_goal : driver -> Ident.ident_printer ->
(* filename_of_goal printer file_ident theory_ident ctxt *)
type prover_answer =
Call_provers.prover_answer =
| Valid
| Invalid
| Unknown of string
| Failure of string
| Timeout
| HighFailure
val call_prover : driver -> context -> prover_answer
val call_prover_on_file : driver -> string -> prover_answer
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
let channel_contents_buf cin =
let buf = Buffer.create 1024
and buff = String.make 1024 ' ' in
let n = ref 0 in
while n := input cin buff 0 1024; !n <> 0 do
Buffer.add_substring buf buff 0 !n
done;
buf
let channel_contents cin = Buffer.contents (channel_contents_buf cin)
let file_contents_buf f =
try
let cin = open_in f in
let buf = channel_contents_buf cin in
close_in cin;
buf
with _ ->
invalid_arg (Printf.sprintf "(cannot open %s)" f)
let file_contents f = Buffer.contents (file_contents_buf f)
let open_temp_file filesuffix usefile =
let file,cout = Filename.open_temp_file "why" filesuffix in
try
let res = usefile file cout in
Sys.remove file;
close_out cout;
res
with
| e ->
Sys.remove file;
close_out cout;
raise e
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
(* return the content of an in-channel *)
val channel_contents : in_channel -> string
(* return the content of a file *)
val file_contents : string -> string
(* return the content of a file *)
val file_contents_buf : string -> Buffer.t
val open_temp_file : string -> (string -> out_channel -> 'a) -> 'a
(* open_temp_file suffix usefile
Create a temporary file with suffix suffix,
and call usefile on this file (filename and open_out).
usefile can close the file *)
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