Commit 4582aecd authored by MARCHE Claude's avatar MARCHE Claude

Ressurect 'smoke detection' feature of why3replay

parent 9e28eb01
......@@ -670,24 +670,24 @@ let file_proved s f =
Hstr.add s.file_state f.file_name b;
b
let pa_proved s paid =
let pa = get_proof_attempt_node s paid in
match pa.proof_state with
| None -> false
| Some pa ->
begin
match pa.Call_provers.pr_answer with
| Call_provers.Valid -> true
| _ -> false
end
let any_proved s any : bool =
match any with
| AFile file -> file_proved s file
| ATh th -> th_proved s th
| ATn tn -> tn_proved s tn
| APn pn -> pn_proved s pn
| APa pa ->
begin
let pa = get_proof_attempt_node s pa in
match pa.proof_state with
| None -> false
| Some pa ->
begin
match pa.Call_provers.pr_answer with
| Call_provers.Valid -> true
| _ -> false
end
end
| APa pa -> pa_proved s pa
......
......@@ -251,6 +251,7 @@ val remove_subtree: notification:notifier -> removed:notifier ->
(** {2 proved status} *)
val pa_proved : session -> proofAttemptID -> bool
val th_proved : session -> theory -> bool
val pn_proved : session -> proofNodeID -> bool
val tn_proved : session -> transID -> bool
......
......@@ -30,9 +30,7 @@ let debug = Debug.register_info_flag
"replay"
let files = Queue.create ()
(*
let opt_stats = ref true
*)
let opt_force = ref false
let opt_obsolete_only = ref false
let opt_use_steps = ref false
......@@ -46,7 +44,6 @@ let opt_verbose = ref true
(** {2 Smoke detector} *)
(*
type smoke_detector =
| SD_None (** No smoke detector *)
| SD_Top (** Negation added at the top of the goals *)
......@@ -61,7 +58,6 @@ let set_opt_smoke = function
| "top" -> opt_smoke := SD_Top
| "deep" -> opt_smoke := SD_Deep
| _ -> assert false
*)
let usage_msg = Format.sprintf
"Usage: %s [options] <project directory>"
......@@ -91,16 +87,16 @@ let option_list = [
Arg.String (fun s ->
opt_provers := Whyconf.parse_filter_prover s :: !opt_provers),
" same as -P");
(*
("--smoke-detector",
Arg.Symbol (["none";"top";"deep"],set_opt_smoke),
" try to detect if the context is self-contradicting") ;
(*
("--bench",
Arg.Set opt_bench, " run as bench (experimental)");
*)
("--no-stats",
Arg.Clear opt_stats,
" do not print statistics") ;
*)
("-q",
Arg.Clear opt_verbose,
" run quietly");
......@@ -163,6 +159,11 @@ let print_statistics ses files =
let print_report ses (id,p,l,r) =
let g = S.get_proof_name ses id in
printf " goal '%s', prover '%a': " g.Ident.id_string Whyconf.print_prover p;
begin
match !opt_smoke with
| SD_None -> ()
| _ -> printf "Smoke detected!:@ "
end;
match r with
| C.Result(new_res,old_res) ->
printf "%a instead of %a (timelimit=%d, memlimit=%d, steplimit=%d)@."
......@@ -193,7 +194,7 @@ let same_result r1 r2 =
| Call_provers.Failure _, Call_provers.Failure _-> true
| _ -> false
let add_to_check_no_smoke some_merge_miss found_obs cont =
let run_replay some_merge_miss found_obs cont =
let session = cont.Controller_itp.controller_session in
let final_callback found_upgraded_prover report =
Debug.dprintf debug "@.";
......@@ -202,12 +203,23 @@ let add_to_check_no_smoke some_merge_miss found_obs cont =
(S.get_files session) ([],0,0)
in
let report =
List.filter
(function
| (_,_,_,C.Result(new_res,old_res)) ->
not (same_result new_res old_res)
| _ -> true)
report
match !opt_smoke with
| SD_None ->
List.filter
(function
| (_,_,_,C.Result(new_res,old_res)) ->
not (same_result new_res old_res)
| _ -> true)
report
| _ ->
List.filter
(function
| (_,_,_,C.Result({Call_provers.pr_answer = Call_provers.Valid} ,_))
-> true
| (_,_,_,C.No_former_result({Call_provers.pr_answer = Call_provers.Valid}))
-> true
| _ -> false)
report
in
let save () =
Debug.dprintf debug "Saving session...@?";
......@@ -216,13 +228,18 @@ let add_to_check_no_smoke some_merge_miss found_obs cont =
printf " %d/%d " n m;
if report = [] && not some_merge_miss then
begin
printf "(replay OK%s%s)@."
(if found_obs then ", obsolete session" else "")
(if found_upgraded_prover then ", upgraded prover" else "");
if true (* !opt_stats *) && n<m then print_statistics session files;
Debug.dprintf debug "Everything replayed OK.@.";
if !opt_force || found_obs || found_upgraded_prover then save ();
exit 0
match !opt_smoke with
| SD_None ->
printf "(replay OK%s%s)@."
(if found_obs then ", obsolete session" else "")
(if found_upgraded_prover then ", upgraded prover" else "");
if !opt_stats && n<m then print_statistics session files;
Debug.dprintf debug "Everything replayed OK.@.";
if !opt_force || found_obs || found_upgraded_prover then save ();
exit 0
| _ ->
printf "No smoke detected@.";
exit 0
end
else
let report = List.rev report in
......@@ -260,53 +277,61 @@ let add_to_check_no_smoke some_merge_miss found_obs cont =
C.replay ~valid_only:false ~obsolete_only:!opt_obsolete_only ~use_steps:!opt_use_steps
~filter ~callback ~notification ~final_callback cont ~any:None
(*
let add_to_check_smoke env_session sched =
let callback report =
Debug.dprintf debug "@.";
let report =
List.filter
(function
| (_,_,_,M.Result({Call_provers.pr_answer = Call_provers.Valid} ,_))
-> true
| (_,_,_,M.No_former_result({Call_provers.pr_answer = Call_provers.Valid}))
-> true
| _ -> false) report
in
if report = [] then begin
Debug.dprintf debug "No smoke detected.@.";
exit 0
end
else begin
List.iter print_report report;
eprintf "Smoke detected.@.";
exit 1
end
in
M.check_all ~release:true ~use_steps:!opt_use_steps
~callback env_session sched
let add_to_check config some_merge_miss found_obs =
match !opt_smoke with
| SD_None -> add_to_check_no_smoke config some_merge_miss found_obs;
| _ ->
assert (not some_merge_miss);
assert (not found_obs);
add_to_check_smoke
let transform_smoke env_session =
let trans tr_name s =
Session_tools.filter_proof_attempt
(fun p -> Opt.inhabited (S.proof_verified p)) s.S.session;
Session_tools.transform_proof_attempt ~keygen:O.create s tr_name
let transform_smoke cont tr_name =
let session = cont.Controller_itp.controller_session in
(* filter the proof attempts *)
let (to_remove,to_transform) =
Session_itp.fold_all_session
session
(fun ((to_remove,to_transform) as acc) any ->
match any with
| Session_itp.APn pnid ->
let valid,other =
Whyconf.Hprover.fold
(fun _pr paid (valid,other) ->
if Session_itp.pa_proved session paid then
(paid::valid,other)
else (valid,paid::other))
(Session_itp.get_proof_attempt_ids session pnid)
([],[])
in
let to_transform =
match valid with
| [] -> to_transform
| _ -> (pnid,valid)::to_transform
in (List.rev_append other to_remove,to_transform)
| _ -> acc)
([],[])
in
match !opt_smoke with
| SD_None -> ()
| SD_Top -> trans "smoke_detector_top" env_session
| SD_Deep -> trans "smoke_detector_deep" env_session
*)
List.iter
(fun paid ->
let pa = Session_itp.get_proof_attempt_node session paid in
Session_itp.remove_proof_attempt
session pa.Session_itp.parent pa.Session_itp.prover)
to_remove;
List.iter
(fun (pn,paids) ->
let tasks =
Session_itp.apply_trans_to_goal
~allow_no_effect:true session cont.Controller_itp.controller_env
tr_name [] pn
in
let tid = Session_itp.graft_transf session pn tr_name [] tasks in
match Session_itp.get_sub_tasks session tid with
| [new_pn] ->
List.iter
(fun paid ->
let pa = Session_itp.get_proof_attempt_node session paid in
Session_itp.remove_proof_attempt
session pa.Session_itp.parent pa.Session_itp.prover;
let _new_paid =
Session_itp.graft_proof_attempt
session new_pn pa.Session_itp.prover
~limit:pa.Session_itp.limit in
())
paids
| _ -> assert false)
to_transform
(*
let run_as_bench env_session =
......@@ -370,18 +395,27 @@ let () =
printf "@.";
exit 0
end;
(*
if !opt_bench then run_as_bench env_session;
let () = transform_smoke env_session in
let sched =
M.init (Whyconf.running_provers_max (Whyconf.get_main config))
in
*)
if found_obs then eprintf "[Warning] session is obsolete@.";
if found_detached then eprintf "[Warning] found detached goals or theories or transformations@.";
if !opt_merging_only then
exit (if found_detached then 1 else 0);
add_to_check_no_smoke found_detached found_obs cont;
(*
if !opt_bench then run_as_bench env_session;
*)
let tr =
match !opt_smoke with
| SD_None -> None
| SD_Top -> Some "smoke_detector_top"
| SD_Deep -> Some "smoke_detector_deep"
in
begin match tr with
| Some _ when found_obs || found_detached ->
eprintf "Cannot run smoke detection in presence of obsolete proofs or detached goals@.";
exit 1
| Some tr -> transform_smoke cont tr
| None -> ()
end;
run_replay found_detached found_obs cont;
Debug.dprintf debug "[Replay] starting scheduler@.";
Unix_scheduler.Unix_scheduler.main_loop ~prompt:"" (fun _ -> ());
eprintf "main replayer loop exited unexpectedly@.";
......
module M
lemma a : false
let f (x:int)
ensures {result = 0}
= x
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../test_smoke.mlw">
<theory name="M">
<goal name="a">
</goal>
<goal name="VC f" expl="VC for f" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
</theory>
</file>
</why3session>
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