Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 643936c5 authored by Johannes Kanig's avatar Johannes Kanig
Browse files

group all limits into a single object

makes API of Call_provers and Driver a bit simpler
parent a164de08
......@@ -92,9 +92,9 @@ let add_proofs_attempts g =
~keygen:dummy_keygen
~obsolete:true
~archived:false
~timelimit:5
~steplimit:(-1)
~memlimit:1000
~limit:{Call_provers.limit_time = Some 5;
limit_steps = None;
limit_mem = Some 1000 }
~edit:None
g p.Whyconf.prover Session.Scheduled
in ())
......
......@@ -94,7 +94,8 @@ let alt_ergo_driver : Driver.driver =
(* calls Alt-Ergo *)
let result1 : Call_provers.prover_result =
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver task1 ()) ()
(* prints Alt-Ergo answer *)
......@@ -104,7 +105,9 @@ let () = printf "@[On task 1, alt-ergo answers %a@."
let result2 : Call_provers.prover_result =
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
~timelimit:10
~limit:{Call_provers.limit_time = Some 10;
limit_mem = None ;
limit_steps = None}
alt_ergo_driver task2 ()) ()
let () = printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
......@@ -141,7 +144,8 @@ let () = printf "@[task 3 created@]@."
let result3 =
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver task3 ()) ()
let () = printf "@[On task 3, alt-ergo answers %a@."
......@@ -170,7 +174,8 @@ let task4 = Task.add_prop_decl task4 Decl.Pgoal goal_id4 fmla4
let result4 =
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver task4 ()) ()
let () = printf "@[On task 4, alt-ergo answers %a@."
......
......@@ -39,7 +39,31 @@ type prover_result = {
pr_model : model;
}
(** time regexp "%h:%m:%s" *)
type resource_limit =
{
limit_time : int option;
limit_mem : int option;
limit_steps : int option;
}
let empty_limit =
{ limit_time = None ; limit_mem = None; limit_steps = None }
let get_time x = Opt.get_def 0 x.limit_time
let get_mem x = Opt.get_def 0 x.limit_mem
let get_steps x = Opt.get_def (-1) x.limit_steps
let mk_limit t m s =
{ limit_time = if t = 0 then None else Some t;
limit_mem = if m = 0 then None else Some m;
limit_steps = if s = -1 then None else Some s
}
let limit_max a b =
mk_limit (max (get_time a) (get_time b))
(max (get_mem a) (get_mem b))
(max (get_steps a) (get_steps b))
type timeunit =
| Hour
| Min
......@@ -189,7 +213,7 @@ let debug_print_model model =
Debug.dprintf debug "Call_provers: %s@." model_str
let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_mapping =
let parse_prover_run res_parser time out ret on_timelimit limit ~printer_mapping =
let ans = match ret with
| Unix.WSTOPPED n ->
Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
......@@ -209,9 +233,9 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_map
let ans = match ans with
| Unknown (s, _) -> Unknown (s, Some reason_unknown)
| _ -> ans in
let ans = match ans with
| Unknown _ | HighFailure when on_timelimit && timelimit > 0
&& time >= (0.9 *. float timelimit) -> Timeout
let ans = match ans, limit with
| (Unknown _ | HighFailure), { limit_time = Some tlimit }
when on_timelimit && time >= (0.9 *. float tlimit) -> Timeout
| _ -> ans
in
let model = res_parser.prp_model_parser out printer_mapping in
......@@ -225,7 +249,10 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_map
pr_model = model;
}
let actualcommand command timelimit memlimit steplimit file =
let actualcommand command limit file =
let timelimit = get_time limit in
let memlimit = get_mem limit in
let steplimit = get_steps limit in
let arglist = Cmdline.cmdline_split command in
let use_stdin = ref true in
let on_timelimit = ref false in
......@@ -250,13 +277,14 @@ let actualcommand command timelimit memlimit steplimit file =
in
args, !use_stdin, !on_timelimit
let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(steplimit=(-1))
let call_on_file ~command
~limit
~res_parser
~printer_mapping
?(cleanup=false) ?(inplace=false) ?(redirect=true) fin =
let command, use_stdin, on_timelimit =
try actualcommand command timelimit memlimit steplimit fin
try actualcommand command limit fin
with e ->
if cleanup then Sys.remove fin;
if inplace then Sys.rename (save fin) fin;
......@@ -300,12 +328,12 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(steplimit=(-1))
if inplace then swallow (Sys.rename (save fin)) fin;
if redirect then swallow Sys.remove fout
end;
parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_mapping
parse_prover_run res_parser time out ret on_timelimit limit
~printer_mapping
in
{ call = call; pid = pid }
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0) ?(steplimit=(-1))
~res_parser ~filename
let call_on_buffer ~command ~limit ~res_parser ~filename
~printer_mapping
?(inplace=false) buffer =
......@@ -316,7 +344,7 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0) ?(steplimit=(-1))
end else
Filename.open_temp_file "why_" ("_" ^ filename) in
Buffer.output_buffer cin buffer; close_out cin;
call_on_file ~command ~timelimit ~memlimit ~steplimit
call_on_file ~command ~limit
~res_parser ~printer_mapping ~cleanup:true ~inplace fin
let query_call pc =
......
......@@ -102,11 +102,36 @@ type pre_prover_call = unit -> prover_call
type post_prover_call = unit -> prover_result
(** Thread-unsafe closure that interprets the prover's results *)
type resource_limit =
{
limit_time : int option;
limit_mem : int option;
limit_steps : int option;
}
(* represents the three ways a prover run can be limited: in time, memory
and/or steps *)
val empty_limit : resource_limit
(* the limit object which imposes no limits *)
val limit_max : resource_limit -> resource_limit -> resource_limit
(* return the limit object whose components represent the maximum of the
corresponding components of the arguments *)
val get_time : resource_limit -> int
(* return time, return default value 0 if not set *)
val get_mem : resource_limit -> int
(* return time, return default value 0 if not set *)
val get_steps : resource_limit -> int
(* return time, return default value (-1) if not set *)
val mk_limit : int -> int -> int -> resource_limit
(* build a limit object, transforming the default values into None on the fly
*)
val call_on_file :
command : string ->
?timelimit : int ->
?memlimit : int ->
?steplimit : int ->
limit : resource_limit ->
res_parser : prover_result_parser ->
printer_mapping : Printer.printer_mapping ->
?cleanup : bool ->
......@@ -116,9 +141,7 @@ val call_on_file :
val call_on_buffer :
command : string ->
?timelimit : int ->
?memlimit : int ->
?steplimit : int ->
limit : resource_limit ->
res_parser : prover_result_parser ->
filename : string ->
printer_mapping : Printer.printer_mapping ->
......
......@@ -251,10 +251,10 @@ let file_of_task drv input_file theory_name task =
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 ?steplimit
let call_on_buffer ~command ~limit
?inplace ~filename ~printer_mapping drv buffer =
Call_provers.call_on_buffer
~command ?timelimit ?memlimit ?steplimit ~res_parser:drv.drv_res_parser
~command ~limit ~res_parser:drv.drv_res_parser
~filename ~printer_mapping ?inplace buffer
......@@ -324,7 +324,7 @@ let print_theory ?old drv fmt th =
print_task ?old drv fmt task
let prove_task_prepared
~command ?timelimit ?memlimit ?steplimit ?old ?inplace drv task =
~command ~limit ?old ?inplace drv task =
let buf = Buffer.create 1024 in
let fmt = formatter_of_buffer buf in
let old_channel = Opt.map open_in old in
......@@ -342,15 +342,14 @@ let prove_task_prepared
get_filename drv fn "T" pr.pr_name.id_string
in
let res =
call_on_buffer ~command ?timelimit ?memlimit ?steplimit
call_on_buffer ~command ~limit
?inplace ~filename ~printer_mapping drv buf in
Buffer.reset buf;
res
let prove_task ~command ?(cntexample=false) ?timelimit ?memlimit ?steplimit ?old ?inplace drv task =
let prove_task ~command ~limit ?(cntexample=false) ?old ?inplace drv task =
let task = prepare_task ~cntexample drv task in
prove_task_prepared ~command ?timelimit ?memlimit
?steplimit ?old ?inplace drv task
prove_task_prepared ~command ~limit ?old ?inplace drv task
(* exception report *)
......
......@@ -36,9 +36,7 @@ val file_of_theory : driver -> string -> Theory.theory -> string
val call_on_buffer :
command : string ->
?timelimit : int ->
?memlimit : int ->
?steplimit : int ->
limit : Call_provers.resource_limit ->
?inplace : bool ->
filename : string ->
printer_mapping : Printer.printer_mapping ->
......@@ -57,10 +55,8 @@ val print_theory :
val prove_task :
command : string ->
limit : Call_provers.resource_limit ->
?cntexample : bool ->
?timelimit : int ->
?memlimit : int ->
?steplimit : int ->
?old : string ->
?inplace : bool ->
driver -> Task.task -> Call_provers.pre_prover_call
......@@ -74,9 +70,7 @@ val print_task_prepared :
val prove_task_prepared :
command : string ->
?timelimit : int ->
?memlimit : int ->
?steplimit : int ->
limit : Call_provers.resource_limit ->
?old : string ->
?inplace : bool ->
driver -> Task.task -> Call_provers.pre_prover_call
......
......@@ -209,8 +209,8 @@ let cntexample m = m.cntexample
exception StepsCommandNotSpecified of string
let get_complete_command pc steplimit =
let comm = if steplimit < 0 then pc.command
let get_complete_command pc ~with_steps =
let comm = if with_steps then pc.command
else
match pc.command_steps with
| None -> raise (StepsCommandNotSpecified
......
......@@ -120,7 +120,7 @@ type config_prover = {
extra_drivers: string list;
}
val get_complete_command : config_prover -> int -> string
val get_complete_command : config_prover -> with_steps:bool -> string
(** add the extra_options to the command *)
val get_provers : config -> config_prover Mprover.t
......
......@@ -489,7 +489,8 @@ let set_proof_state a =
| S.Done { Call_provers.pr_time = time; Call_provers.pr_steps = steps } ->
let s =
if gconfig.show_time_limit then
Format.sprintf "%.2f [%d.0]" time a.S.proof_timelimit
Format.sprintf "%.2f [%d.0]" time
(Call_provers.get_time a.S.proof_limit)
else
Format.sprintf "%.2f" time
in
......@@ -503,7 +504,8 @@ let set_proof_state a =
| S.Interrupted -> "(interrupted)"
| S.Scheduled | S.Running ->
Format.sprintf "[limit=%d sec., %d M]"
a.S.proof_timelimit a.S.proof_memlimit
(Call_provers.get_time a.S.proof_limit)
(Call_provers.get_mem a.S.proof_limit)
in
let t = if obsolete then t ^ " (obsolete)" else t in
(* TODO find a better way to signal archived row *)
......@@ -1016,7 +1018,10 @@ let prover_on_selected_goals pr =
M.run_prover
(env_session()) sched
~context_unproved_goals_only:!context_unproved_goals_only
~cntexample ~timelimit ~steplimit:(-1) ~memlimit
~cntexample
~limit:{Call_provers.limit_time = Some timelimit;
limit_mem = Some memlimit;
limit_steps = None}
pr a
with e ->
eprintf "@[Exception raised while running a prover:@ %a@.@]"
......@@ -1131,13 +1136,13 @@ let bisect_proof_attempt pa =
assert (not lp.S.prover_config.C.in_place); (* TODO do this case *)
M.schedule_proof_attempt
~cntexample
~timelimit:!timelimit
~memlimit:pa.S.proof_memlimit
~steplimit:(-1)
~limit:{Call_provers.limit_time = Some !timelimit;
limit_mem = pa.S.proof_limit.Call_provers.limit_mem;
limit_steps = None}
?old:(S.get_edited_as_abs eS.S.session pa)
(* It is dangerous, isn't it? to be in place for bisecting? *)
~inplace:lp.S.prover_config.C.in_place
~command:(C.get_complete_command lp.S.prover_config (-1))
~command:(C.get_complete_command lp.S.prover_config ~with_steps:false)
~driver:lp.S.prover_driver
~callback:(callback lp pa c) sched t
in
......@@ -1170,12 +1175,13 @@ let bisect_proof_attempt pa =
| Some lp ->
M.schedule_proof_attempt
~cntexample
~timelimit:!timelimit
~memlimit:pa.S.proof_memlimit
~steplimit:(-1)
~limit:{pa.S.proof_limit with
Call_provers.limit_steps = None;
limit_time = Some !timelimit}
?old:(S.get_edited_as_abs eS.S.session pa)
~inplace:lp.S.prover_config.C.in_place
~command:(C.get_complete_command lp.S.prover_config (-1))
~command:(C.get_complete_command lp.S.prover_config
~with_steps:false)
~driver:lp.S.prover_driver
~callback:(callback lp pa c) sched t in
dprintf debug "Bisecting with %a started.@."
......
......@@ -157,9 +157,7 @@ and 'a proof_attempt =
mutable proof_prover : Whyconf.prover;
proof_parent : 'a goal;
mutable proof_state : proof_attempt_status;
mutable proof_timelimit : int;
mutable proof_steplimit : int;
mutable proof_memlimit : int;
mutable proof_limit : Call_provers.resource_limit;
mutable proof_obsolete : bool;
mutable proof_archived : bool;
mutable proof_edited_as : string option;
......@@ -498,21 +496,15 @@ let get_used_provers_with_stats session =
PHprover.add prover_table prover x;
x
in
let tf =
try Hashtbl.find timelimits pa.proof_timelimit
with Not_found -> 0
in
let sf =
try Hashtbl.find steplimits pa.proof_steplimit
with Not_found -> 0
in
let mf =
try Hashtbl.find memlimits pa.proof_timelimit
with Not_found -> 0
in
Hashtbl.replace timelimits pa.proof_timelimit (tf+1);
Hashtbl.replace steplimits pa.proof_steplimit (sf+1);
Hashtbl.replace memlimits pa.proof_memlimit (mf+1))
let lim_time = Call_provers.get_time pa.proof_limit in
let lim_mem = Call_provers.get_mem pa.proof_limit in
let lim_steps = Call_provers.get_steps pa.proof_limit in
let tf = try Hashtbl.find timelimits lim_time with Not_found -> 0 in
let sf = try Hashtbl.find steplimits lim_steps with Not_found -> 0 in
let mf = try Hashtbl.find memlimits lim_mem with Not_found -> 0 in
Hashtbl.replace timelimits lim_time (tf+1);
Hashtbl.replace steplimits lim_mem (sf+1);
Hashtbl.replace memlimits lim_steps (mf+1))
session;
prover_table
......@@ -588,9 +580,9 @@ let save_proof_attempt fmt ((id,tl,sl,ml),a) =
fprintf fmt
"@\n@[<h><proof@ prover=\"%i\"%a%a%a%a%a%a>"
id
(save_int_def "timelimit" tl) a.proof_timelimit
(save_int_def "steplimit" sl) a.proof_steplimit
(save_int_def "memlimit" ml) a.proof_memlimit
(save_int_def "timelimit" tl) (Call_provers.get_time a.proof_limit)
(save_int_def "steplimit" sl) (Call_provers.get_steps a.proof_limit)
(save_int_def "memlimit" ml) (Call_provers.get_mem a.proof_limit)
(opt_string "edited") a.proof_edited_as
(save_bool_def "obsolete" false) a.proof_obsolete
(save_bool_def "archived" false) a.proof_archived;
......@@ -954,7 +946,7 @@ type 'a keygen = ?parent:'a -> unit -> 'a
let add_external_proof
?(notify=notify)
~(keygen:'a keygen) ~obsolete
~archived ~timelimit ~steplimit ~memlimit ~edit (g:'a goal) p result =
~archived ~limit ~edit (g:'a goal) p result =
assert (edit <> Some "");
let key = keygen ~parent:g.goal_key () in
let a = { proof_prover = p;
......@@ -963,9 +955,7 @@ let add_external_proof
proof_obsolete = obsolete;
proof_archived = archived;
proof_state = result;
proof_timelimit = timelimit;
proof_steplimit = steplimit;
proof_memlimit = memlimit;
proof_limit = limit;
proof_edited_as = edit;
}
in
......@@ -995,8 +985,12 @@ let change_prover a p =
let set_edited_as edited_as a = a.proof_edited_as <- edited_as
let set_timelimit timelimit a = a.proof_timelimit <- timelimit
let set_memlimit memlimit a = a.proof_memlimit <- memlimit
let set_timelimit timelimit a =
a.proof_limit <-
{ a.proof_limit with Call_provers.limit_time = Some timelimit}
let set_memlimit memlimit a =
a.proof_limit <-
{ a.proof_limit with Call_provers.limit_mem = Some memlimit}
let set_obsolete ?(notify=notify) a =
a.proof_obsolete <- true;
......@@ -1299,6 +1293,7 @@ and load_proof_or_transf ctxt mg a =
let timelimit = int_attribute_def "timelimit" a timelimit in
let steplimit = int_attribute_def "steplimit" a steplimit in
let memlimit = int_attribute_def "memlimit" a memlimit in
let limit = Call_provers.mk_limit timelimit memlimit steplimit in
(*
if timelimit < 0 then begin
eprintf "[Error] incorrect or unspecified timelimit '%i'@."
......@@ -1309,7 +1304,7 @@ and load_proof_or_transf ctxt mg a =
*)
let (_ : 'a proof_attempt) =
add_external_proof ~keygen:ctxt.keygen ~archived ~obsolete
~timelimit ~steplimit ~memlimit ~edit mg p res
~limit ~edit mg p res
in
()
with Failure _ | Not_found ->
......@@ -1930,16 +1925,14 @@ let ft_of_pa a =
But since it will be perhaps removed...
*)
let copy_external_proof
?notify ~keygen ?obsolete ?archived ?timelimit ?steplimit ?memlimit ?edit
?notify ~keygen ?obsolete ?archived ?limit ?edit
?goal ?prover ?attempt_status ?env_session ?session a =
let session = match env_session with
| Some eS -> Some eS.session
| _ -> session in
let obsolete = Opt.get_def a.proof_obsolete obsolete in
let archived = Opt.get_def a.proof_archived archived in
let timelimit = Opt.get_def a.proof_timelimit timelimit in
let steplimit = Opt.get_def a.proof_steplimit steplimit in
let memlimit = Opt.get_def a.proof_memlimit memlimit in
let limit = Opt.get_def a.proof_limit limit in
let pas = Opt.get_def a.proof_state attempt_status in
let ngoal = Opt.get_def a.proof_parent goal in
let nprover = match prover with
......@@ -1986,7 +1979,7 @@ let copy_external_proof
Some (dst_file)
in
add_external_proof ?notify ~keygen
~obsolete ~archived ~timelimit ~steplimit ~memlimit ~edit ngoal nprover pas
~obsolete ~archived ~limit ~edit ngoal nprover pas
exception UnloadableProver of Whyconf.prover
......@@ -2046,7 +2039,9 @@ let print_external_proof fmt p =
fprintf fmt "%a - %a (%i, %i, %i)%s%s%s"
Whyconf.print_prover p.proof_prover
print_attempt_status p.proof_state
p.proof_timelimit p.proof_steplimit p.proof_memlimit
(Call_provers.get_time p.proof_limit)
(Call_provers.get_steps p.proof_limit)
(Call_provers.get_mem p.proof_limit)
(if p.proof_obsolete then " obsolete" else "")
(if p.proof_archived then " archived" else "")
(if p.proof_edited_as <> None then " edited" else "")
......@@ -2081,9 +2076,7 @@ let merge_proof ~keygen obsolete to_goal _ from_proof =
(add_external_proof ~keygen
~obsolete
~archived:from_proof.proof_archived
~timelimit:from_proof.proof_timelimit
~steplimit:from_proof.proof_steplimit
~memlimit:from_proof.proof_memlimit
~limit:from_proof.proof_limit
~edit:from_proof.proof_edited_as
to_goal
from_proof.proof_prover
......
......@@ -95,9 +95,7 @@ and 'a proof_attempt = private
mutable proof_prover : Whyconf.prover;
proof_parent : 'a goal;
mutable proof_state : proof_attempt_status;
mutable proof_timelimit : int;
mutable proof_steplimit : int;
mutable proof_memlimit : int;
mutable proof_limit : Call_provers.resource_limit;
mutable proof_obsolete : bool;
mutable proof_archived : bool;
mutable proof_edited_as : string option;
......@@ -346,9 +344,7 @@ val add_external_proof :
keygen:'key keygen ->
obsolete:bool ->
archived:bool ->
timelimit:int ->
steplimit:int ->
memlimit:int ->
limit: Call_provers.resource_limit ->
edit:string option ->
'key goal ->
Whyconf.prover ->
......@@ -389,9 +385,7 @@ val copy_external_proof :
keygen:'key keygen ->
?obsolete:bool ->
?archived:bool ->
?timelimit:int ->
?steplimit:int ->
?memlimit:int ->
?limit:Call_provers.resource_limit ->
?edit:string option ->
?goal:'key goal ->
?prover:Whyconf.prover ->
......
......@@ -79,7 +79,8 @@ module Make(O : OBSERVER) = struct
(*************************)
type action =
| Action_proof_attempt of bool * int * int * int * string option * bool * string *
| Action_proof_attempt of
bool * Call_provers.resource_limit * string option * bool * string *
Driver.driver * (proof_attempt_status -> unit) * Task.task
| Action_delayed of (unit -> unit)
......@@ -209,13 +210,13 @@ let idle_handler t =
if Queue.length t.proof_attempts_queue < 3 * t.maximum_running_proofs then
begin
match Queue.pop t.actions_queue with
| Action_proof_attempt(cntexample,timelimit,memlimit,steplimit,
| Action_proof_attempt(cntexample,limit,
old,inplace,command,driver,callback,goal) ->
begin
try
let pre_call =
Driver.prove_task ?old ~cntexample ~inplace ~command
~timelimit ~steplimit ~memlimit driver goal
~limit driver goal
in
Queue.push (callback,pre_call) t.proof_attempts_queue;
run_timeout_handler t
......@@ -257,7 +258,7 @@ let cancel_scheduled_proofs t =
try
while true do
match Queue.pop t.actions_queue with
| Action_proof_attempt(_cntexample,_timelimit,_memlimit,_steplimit,
| Action_proof_attempt(_cntexample,_limit,
_old,_inplace,_command,_driver,callback,_goal) ->
callback Interrupted
| Action_delayed _ as a->
......@@ -275,14 +276,14 @@ let cancel_scheduled_proofs t =
O.notify_timer_state 0 0 (List.length t.running_proofs)
let schedule_proof_attempt ~cntexample ~timelimit ~memlimit ~steplimit ?old ~inplace
let schedule_proof_attempt ~cntexample ~limit ?old ~inplace
~command ~driver ~callback t goal =
Debug.dprintf