Commit c38e1957 authored by Johannes Kanig's avatar Johannes Kanig Committed by MARCHE Claude
Browse files

N211-037 introduce a type "prover_parser"

This type groups three elements that are used to evaluate prover output.
Grouping this will allow easier reues of existing code for the VC server
facility.

* call_provers.ml:
new type prover_result_parser
(parse_prover_run) extract code to parse prover output in a function
(call_on_file, call_on_buffer) group three arguments into one, and adapt
   calls

* driver.ml:
modify type driver to group three fields into one
(parse_driver) modify according to change in type
(call_on_buffer) modify call

* session_scheduler.ml
adapt call
parent eeec93b5
......@@ -80,6 +80,12 @@ type prover_result = {
pr_steps : int; (* -1 if unknown *)
}
type prover_result_parser = {
prp_regexps : (Str.regexp * prover_answer) list;
prp_timeregexps : timeregexp list;
prp_exitcodes : (int * prover_answer) list;
}
let print_prover_answer fmt = function
| Valid -> fprintf fmt "Valid"
| Invalid -> fprintf fmt "Invalid"
......@@ -132,8 +138,33 @@ type pre_prover_call = unit -> prover_call
let save f = f ^ ".save"
let parse_prover_run res_parser time out ret on_timelimit timelimit =
let ans = match ret with
| Unix.WSTOPPED n ->
Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
grep out res_parser.prp_regexps
| Unix.WSIGNALED n ->
Debug.dprintf debug "Call_provers: killed by signal %d@." n;
grep out res_parser.prp_regexps
| Unix.WEXITED n ->
Debug.dprintf debug "Call_provers: exited with status %d@." n;
(try List.assoc n res_parser.prp_exitcodes
with Not_found -> grep out res_parser.prp_regexps)
in
Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
let time = Opt.get_def time (grep_time out res_parser.prp_timeregexps) in
let ans = match ans with
| HighFailure when on_timelimit && timelimit > 0
&& time >= (0.9 *. float timelimit) -> Timeout
| _ -> ans
in
{ pr_answer = ans;
pr_status = ret;
pr_output = out;
pr_time = time }
let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
~regexps ~timeregexps ~exitcodes
~res_parser
?(cleanup=false) ?(inplace=false) ?(redirect=true) fin =
let arglist = Cmdline.cmdline_split command in
......@@ -201,34 +232,12 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
if inplace then swallow (Sys.rename (save fin)) fin;
if redirect then swallow Sys.remove fout
end;
let ans = match ret with
| Unix.WSTOPPED n ->
Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
grep out regexps
| Unix.WSIGNALED n ->
Debug.dprintf debug "Call_provers: killed by signal %d@." n;
grep out regexps
| Unix.WEXITED n ->
Debug.dprintf debug "Call_provers: exited with status %d@." n;
(try List.assoc n exitcodes with Not_found -> grep out regexps)
in
Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
let time, step = Opt.get_def (time, -1) (grep_time out timeregexps) in
let ans = match ans with
| HighFailure when !on_timelimit && timelimit > 0
&& time >= (0.9 *. float timelimit) -> Timeout
| _ -> ans
in
{ pr_answer = ans;
pr_status = ret;
pr_output = out;
pr_time = time;
pr_steps = step}
parse_prover_run res_parser time out ret !on_timelimit timelimit
in
{ call = call; pid = pid }
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
~regexps ~timeregexps ~exitcodes ~filename
~res_parser ~filename
?(inplace=false) buffer =
let fin,cin =
......@@ -239,7 +248,7 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
Filename.open_temp_file "why_" ("_" ^ filename) in
Buffer.output_buffer cin buffer; close_out cin;
call_on_file ~command ~timelimit ~memlimit ~stepslimit
~regexps ~timeregexps ~exitcodes ~cleanup:true ~inplace fin
~res_parser ~cleanup:true ~inplace fin
let query_call pc =
let pid, ret = Unix.waitpid [Unix.WNOHANG] pc.pid in
......
......@@ -61,6 +61,12 @@ val timeregexp : string -> timeregexp
(** Converts a regular expression with special markers '%h','%m',
'%s','%i' (for milliseconds) into a value of type [timeregexp] *)
type prover_result_parser = {
prp_regexps : (Str.regexp * prover_answer) list;
prp_timeregexps : timeregexp list;
prp_exitcodes : (int * prover_answer) list;
}
type prover_call
(** Type that represents a single prover run *)
......@@ -75,9 +81,7 @@ val call_on_file :
?timelimit : int ->
?memlimit : int ->
?stepslimit : int ->
regexps : (Str.regexp * prover_answer) list ->
timeregexps : timeregexp list ->
exitcodes : (int * prover_answer) list ->
res_parser : prover_result_parser ->
?cleanup : bool ->
?inplace : bool ->
?redirect : bool ->
......@@ -88,9 +92,7 @@ val call_on_buffer :
?timelimit : int ->
?memlimit : int ->
?stepslimit : int ->
regexps : (Str.regexp * prover_answer) list ->
timeregexps : timeregexp list ->
exitcodes : (int * prover_answer) list ->
res_parser : prover_result_parser ->
filename : string ->
?inplace : bool ->
Buffer.t -> pre_prover_call
......
......@@ -32,9 +32,7 @@ type driver = {
drv_thprelude : prelude_map;
drv_blacklist : string list;
drv_meta : (theory * Stdecl.t) Mid.t;
drv_regexps : (Str.regexp * prover_answer) list;
drv_timeregexps : Call_provers.timeregexp list;
drv_exitcodes : (int * prover_answer) list;
drv_res_parser : prover_result_parser;
drv_tag : int
}
......@@ -192,9 +190,12 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
drv_thprelude = Mid.map List.rev !thprelude;
drv_blacklist = Queue.fold (fun l s -> s :: l) [] blacklist;
drv_meta = !meta;
drv_regexps = List.rev !regexps;
drv_timeregexps = List.rev !timeregexps;
drv_exitcodes = List.rev !exitcodes;
drv_res_parser =
{
prp_regexps = List.rev !regexps;
prp_timeregexps = List.rev !timeregexps;
prp_exitcodes = List.rev !exitcodes;
};
drv_tag = !driver_tag
}
......@@ -231,12 +232,10 @@ let file_of_theory drv input_file th =
get_filename drv input_file th.th_name.Ident.id_string "null"
let call_on_buffer ~command ?timelimit ?memlimit ?stepslimit ?inplace ~filename drv buffer =
let regexps = drv.drv_regexps in
let timeregexps = drv.drv_timeregexps in
let exitcodes = drv.drv_exitcodes in
Call_provers.call_on_buffer
~command ?timelimit ?memlimit ?stepslimit ~regexps ~timeregexps
~exitcodes ~filename ?inplace buffer
~command ?timelimit ?memlimit ?stepslimit ~res_parser:drv.drv_res_parser
~filename ?inplace buffer
(** print'n'prove *)
......
......@@ -289,10 +289,13 @@ let schedule_proof_attempt ~timelimit ~memlimit ~stepslimit ?old ~inplace
let schedule_edition t command filename callback =
Debug.dprintf debug "[Sched] Scheduling an edition@.";
let res_parser =
{ Call_provers.prp_exitcodes = [(0,Call_provers.Unknown "")];
Call_provers.prp_regexps = [];
Call_provers.prp_timeregexps = []
} in
let precall =
Call_provers.call_on_file ~command ~regexps:[] ~timeregexps:[]
~exitcodes:[(0,Call_provers.Unknown "")] ~redirect:false filename
in
Call_provers.call_on_file ~command ~res_parser ~redirect:false filename in
callback Running;
t.running_proofs <- (Check_prover(callback, precall ())) :: t.running_proofs;
run_timeout_handler t
......
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