Skip to content
GitLab
Commit f0d149ac authored by Clément Fumex's avatar Clément Fumex
Browse files

Adding steps limit for replays

parent ef562661
Hide whitespace changes
Inline Side-by-side
drivers/alt_ergo_bare.drv
View file @ f0d149ac
......@@ -9,10 +9,11 @@ valid "Valid"
invalid "Invalid"
unknown "I don't know" ""
timeout "Timeout"
timeout "Steps limit reached"
outofmemory "Fatal error: out of memory"
outofmemory "Fatal error: exception Stack_overflow"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
time "Valid (%s)"
time "Valid (%s) (%S)"
time "why3cpulimit time : %s s"
(* À discuter *)
......
share/provers-detection-data.conf
View file @ f0d149ac
......@@ -5,7 +5,7 @@ exec = "alt-ergo-0.95.2"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
version_ok = "0.95.2"
command = "%l/why3-cpulimit %t %m -s %e -timelimit %t %f"
command = "%l/why3-cpulimit %t %m -s %e -timelimit %t -steps-bound %S %f"
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"
......@@ -18,7 +18,7 @@ version_switch = "-version"
version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
version_ok = "0.95.1"
version_old = "0.95"
command = "%l/why3-cpulimit %T %m -s %e -timelimit %t %f"
command = "%l/why3-cpulimit %T %m -s %e -timelimit %t -steps-bound %S %f"
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"
......
share/why3session.dtd
View file @ f0d149ac
......@@ -36,7 +36,7 @@
<!ATTLIST goal loccnumb CDATA #IMPLIED>
<!ATTLIST goal loccnume CDATA #IMPLIED>
<!ELEMENT proof (result|undone|internalfailure)>
<!ELEMENT proof (result|undone|internalfailure|unedited)>
<!ATTLIST proof prover CDATA #REQUIRED>
<!ATTLIST proof timelimit CDATA #IMPLIED>
<!ATTLIST proof memlimit CDATA #IMPLIED>
......@@ -47,8 +47,10 @@
<!ELEMENT result EMPTY>
<!ATTLIST result status (valid|invalid|unknown|timeout|outofmemory|failure|highfailure) #REQUIRED>
<!ATTLIST result time CDATA #IMPLIED>
<!ATTLIST result steps CDATA #IMPLIED>
<!ELEMENT undone EMPTY>
<!ELEMENT unedited EMPTY>
<!ELEMENT internalfailure EMPTY>
<!ATTLIST internalfailure reason CDATA #REQUIRED>
......
src/driver/call_provers.ml
View file @ f0d149ac
......@@ -17,6 +17,7 @@ type timeunit =
| Min
| Sec
| Msec
| Step
type timeregexp = {
re : Str.regexp;
......@@ -34,7 +35,8 @@ let timeregexp s =
| "m" -> add_unit Min
| "s" -> add_unit Sec
| "i" -> add_unit Msec
| _ -> failwith "unknown format specifier, use %%h, %%m, %%s, %%i"
| "S" -> add_unit Step
| _ -> failwith "unknown format specifier, use %%h, %%m, %%s, %%i, %%S"
in
let s = Str.global_substitute cmd_regexp replace s in
let group = Array.make !nb Hour in
......@@ -47,14 +49,16 @@ let rec grep_time out = function
begin try
ignore (Str.search_forward re.re out 0);
let t = ref 0. in
let s = ref (-1) in
Array.iteri (fun i u ->
let v = float_of_string (Str.matched_group (succ i) out) in
let v = 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
| Hour -> t := !t +. float_of_string v *. 3600.
| Min -> t := !t +. float_of_string v *. 60.
| Sec -> t := !t +. float_of_string v
| Msec -> t := !t +. float_of_string v /. 1000.
| Step -> s := int_of_string v ) re.group;
Some( !t, !s )
with _ -> grep_time out l end
(** *)
......@@ -73,6 +77,7 @@ type prover_result = {
pr_status : Unix.process_status;
pr_output : string;
pr_time : float;
pr_steps : int; (* -1 if unknown *)
}
let print_prover_answer fmt = function
......@@ -127,7 +132,7 @@ type pre_prover_call = unit -> prover_call
let save f = f ^ ".save"
let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
~regexps ~timeregexps ~exitcodes
?(cleanup=false) ?(inplace=false) ?(redirect=true) fin =
......@@ -147,6 +152,7 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
to prepare the command line in a separate function? *)
| "l" -> Config.libdir
| "d" -> Config.datadir
| "S" -> string_of_int stepslimit
| _ -> failwith "unknown specifier, use %%, %f, %t, %T, %U, %m, %l, or %d"
in
let subst s =
......@@ -207,7 +213,7 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
(try List.assoc n exitcodes with Not_found -> grep out regexps)
in
Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
let time = Opt.get_def time (grep_time out timeregexps) in
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
......@@ -216,11 +222,12 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
{ pr_answer = ans;
pr_status = ret;
pr_output = out;
pr_time = time }
pr_time = time;
pr_steps = step}
in
{ call = call; pid = pid }
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
~regexps ~timeregexps ~exitcodes ~filename
?(inplace=false) buffer =
......@@ -231,7 +238,7 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
end else
Filename.open_temp_file "why_" ("_" ^ filename) in
Buffer.output_buffer cin buffer; close_out cin;
call_on_file ~command ~timelimit ~memlimit
call_on_file ~command ~timelimit ~memlimit ~stepslimit
~regexps ~timeregexps ~exitcodes ~cleanup:true ~inplace fin
let query_call pc =
......
src/driver/call_provers.mli
View file @ f0d149ac
......@@ -37,6 +37,8 @@ type prover_result = {
(** The output of the prover currently stderr and stdout *)
pr_time : float;
(** The time taken by the prover *)
pr_steps : int;
(** The number of steps taken by the prover (-1 if not available) *)
}
val print_prover_answer : Format.formatter -> prover_answer -> unit
......@@ -72,6 +74,7 @@ val call_on_file :
command : string ->
?timelimit : int ->
?memlimit : int ->
?stepslimit : int ->
regexps : (Str.regexp * prover_answer) list ->
timeregexps : timeregexp list ->
exitcodes : (int * prover_answer) list ->
......@@ -84,6 +87,7 @@ val call_on_buffer :
command : string ->
?timelimit : int ->
?memlimit : int ->
?stepslimit : int ->
regexps : (Str.regexp * prover_answer) list ->
timeregexps : timeregexp list ->
exitcodes : (int * prover_answer) list ->
......
src/driver/driver.ml
View file @ f0d149ac
......@@ -230,12 +230,12 @@ 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 ?inplace ~filename drv buffer =
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 ~regexps ~timeregexps
~command ?timelimit ?memlimit ?stepslimit ~regexps ~timeregexps
~exitcodes ~filename ?inplace buffer
(** print'n'prove *)
......@@ -291,7 +291,7 @@ let print_theory ?old drv fmt th =
print_task ?old drv fmt task
let prove_task_prepared
~command ?timelimit ?memlimit ?old ?inplace drv task =
~command ?timelimit ?memlimit ?stepslimit ?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
......@@ -308,13 +308,13 @@ let prove_task_prepared
get_filename drv fn "T" pr.pr_name.id_string
in
let res =
call_on_buffer ~command ?timelimit ?memlimit ?inplace ~filename drv buf in
call_on_buffer ~command ?timelimit ?memlimit ?stepslimit ?inplace ~filename drv buf in
Buffer.reset buf;
res
let prove_task ~command ?timelimit ?memlimit ?old ?inplace drv task =
let prove_task ~command ?timelimit ?memlimit ?stepslimit ?old ?inplace drv task =
let task = prepare_task drv task in
prove_task_prepared ~command ?timelimit ?memlimit ?old ?inplace drv task
prove_task_prepared ~command ?timelimit ?memlimit ?stepslimit ?old ?inplace drv task
(* exception report *)
......
src/driver/driver.mli
View file @ f0d149ac
......@@ -38,6 +38,7 @@ val call_on_buffer :
command : string ->
?timelimit : int ->
?memlimit : int ->
?stepslimit : int ->
?inplace : bool ->
filename : string ->
driver -> Buffer.t -> Call_provers.pre_prover_call
......@@ -56,6 +57,7 @@ val prove_task :
command : string ->
?timelimit : int ->
?memlimit : int ->
?stepslimit : int ->
?old : string ->
?inplace : bool ->
driver -> Task.task -> Call_provers.pre_prover_call
......@@ -71,6 +73,7 @@ val prove_task_prepared :
command : string ->
?timelimit : int ->
?memlimit : int ->
?stepslimit : int ->
?old : string ->
?inplace : bool ->
driver -> Task.task -> Call_provers.pre_prover_call
......
src/ide/gmain.ml
View file @ f0d149ac
......@@ -420,11 +420,17 @@ let set_proof_state a =
goals_model#set ~row:row#iter ~column:status_column
(image_of_result ~obsolete res);
let t = match res with
| S.Done { Call_provers.pr_time = time } ->
| 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
else
Format.sprintf "%.2f" time
in
if steps >= 0 then
Format.sprintf "%s (steps: %d)" s steps
else
s
| S.Unedited -> "(not yet edited)"
| S.JustEdited -> "(edited)"
| S.InternalFailure _ -> "(internal failure)"
......@@ -991,6 +997,7 @@ let bisect_proof_attempt pa =
M.schedule_proof_attempt
~timelimit:!timelimit
~memlimit:pa.S.proof_memlimit
~stepslimit:(-1)
?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
......@@ -1028,6 +1035,7 @@ let bisect_proof_attempt pa =
M.schedule_proof_attempt
~timelimit:!timelimit
~memlimit:pa.S.proof_memlimit
~stepslimit:(-1)
?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)
......
src/session/session.ml
View file @ f0d149ac
......@@ -544,9 +544,17 @@ let save_string fmt s =
| c -> pp_print_char fmt c
done
let opt pr lab fmt = function
| None -> ()
| Some s -> fprintf fmt "@ %s=\"%a\"" lab pr s
let save_result fmt r =
fprintf fmt "<result@ status=\"%s\"@ time=\"%.2f\"/>"
let steps = if r.Call_provers.pr_steps >= 0 then
Some r.Call_provers.pr_steps
else
None
in
fprintf fmt "<result@ status=\"%s\"@ time=\"%.2f\"%a/>"
(match r.Call_provers.pr_answer with
| Call_provers.Valid -> "valid"
| Call_provers.Failure _ -> "failure"
......@@ -556,6 +564,7 @@ let save_result fmt r =
| Call_provers.OutOfMemory -> "outofmemory"
| Call_provers.Invalid -> "invalid")
r.Call_provers.pr_time
(opt pp_print_int "steps") steps
let save_status fmt s =
match s with
......@@ -575,10 +584,6 @@ let save_bool_def name def fmt b =
let save_int_def name def fmt n =
if n <> def then fprintf fmt "@ %s=\"%d\"" name n
let opt pr lab fmt = function
| None -> ()
| Some s -> fprintf fmt "@ %s=\"%a\"" lab pr s
let opt_string = opt save_string
let save_proof_attempt fmt ((id,tl,ml),a) =
......@@ -1181,11 +1186,16 @@ let load_result r =
try float_of_string (List.assoc "time" r.Xml.attributes)
with Not_found -> 0.0
in
let steps =
try int_of_string (List.assoc "steps" r.Xml.attributes)
with Not_found -> -1
in
Done {
Call_provers.pr_answer = answer;
Call_provers.pr_time = time;
Call_provers.pr_output = "";
Call_provers.pr_status = Unix.WEXITED 0
Call_provers.pr_status = Unix.WEXITED 0;
Call_provers.pr_steps = steps
}
| "undone" -> Interrupted
| "unedited" -> Unedited
......
src/session/session_scheduler.ml
View file @ f0d149ac
......@@ -79,7 +79,7 @@ module Make(O : OBSERVER) = struct
(*************************)
type action =
| Action_proof_attempt of int * int * string option * bool * string *
| Action_proof_attempt of int * int * int * string option * bool * string *
Driver.driver * (proof_attempt_status -> unit) * Task.task
| Action_delayed of (unit -> unit)
......@@ -209,13 +209,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(timelimit,memlimit,old,inplace,command,driver,
| Action_proof_attempt(timelimit,memlimit,stepslimit,old,inplace,command,driver,
callback,goal) ->
begin
try
let pre_call =
Driver.prove_task
?old ~inplace ~command ~timelimit ~memlimit driver goal
?old ~inplace ~command ~timelimit ~stepslimit ~memlimit driver goal
in
Queue.push (callback,pre_call) t.proof_attempts_queue;
run_timeout_handler t
......@@ -257,7 +257,7 @@ let cancel_scheduled_proofs t =
try
while true do
match Queue.pop t.actions_queue with
| Action_proof_attempt(_timelimit,_memlimit,_old,_inplace,_command,
| Action_proof_attempt(_timelimit,_memlimit,_stepslimit,_old,_inplace,_command,
_driver,callback,_goal) ->
callback Interrupted
| Action_delayed _ as a->
......@@ -275,14 +275,14 @@ let cancel_scheduled_proofs t =
O.notify_timer_state 0 0 (List.length t.running_proofs)
let schedule_proof_attempt ~timelimit ~memlimit ?old ~inplace
let schedule_proof_attempt ~timelimit ~memlimit ~stepslimit ?old ~inplace
~command ~driver ~callback t goal =
Debug.dprintf debug "[Sched] Scheduling a new proof attempt (goal : %a)@."
(fun fmt g -> Format.pp_print_string fmt
(Task.task_goal g).Decl.pr_name.Ident.id_string) goal;
callback Scheduled;
Queue.push
(Action_proof_attempt(timelimit,memlimit,old,inplace,command,driver,
(Action_proof_attempt(timelimit,memlimit,stepslimit,old,inplace,command,driver,
callback,goal))
t.actions_queue;
run_idle_handler t
......@@ -458,6 +458,12 @@ let run_external_proof_v3 eS eT a callback =
end else begin
let previous_result = a.proof_state in
let timelimit, memlimit = adapt_limits a in
let stepslimit =
match a with
| { proof_state = Done { pr_answer = Valid; pr_steps = s };
proof_obsolete = false }-> s
| _ -> -1
in
let inplace = npc.prover_config.Whyconf.in_place in
let command = Whyconf.get_complete_command npc.prover_config in
let cb result =
......@@ -473,7 +479,7 @@ let run_external_proof_v3 eS eT a callback =
if Sys.file_exists f then Some f
else raise (NoFile f) in
schedule_proof_attempt
~timelimit ~memlimit
~timelimit ~memlimit ~stepslimit
?old ~inplace ~command
~driver:npc.prover_driver
~callback:cb
......
src/session/session_scheduler.mli
View file @ f0d149ac
......@@ -286,6 +286,7 @@ module Make(O: OBSERVER) : sig
val schedule_proof_attempt:
timelimit:int ->
memlimit:int ->
stepslimit:int ->
?old:string ->
inplace:bool ->
command:string ->
......
Supports Markdown
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