From c3ee29acea9455bee0713fb8d96b6a6d3eb98d1a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 11 Jul 2022 20:52:12 +0200
Subject: [PATCH] [wp] improved consolidation for smoke tests
---
src/plugins/wp/ProofEngine.ml | 58 ++++++++--------
src/plugins/wp/ProofEngine.mli | 9 ++-
src/plugins/wp/ProverScript.ml | 4 +-
src/plugins/wp/Stats.ml | 108 +++++++++++++++++++----------
src/plugins/wp/Stats.mli | 6 +-
src/plugins/wp/VC.ml | 2 +-
src/plugins/wp/VC.mli | 6 +-
src/plugins/wp/VCS.ml | 20 +++---
src/plugins/wp/VCS.mli | 2 +
src/plugins/wp/gui/GuiNavigator.ml | 2 +-
src/plugins/wp/register.ml | 21 +++---
src/plugins/wp/wpo.ml | 16 +++--
src/plugins/wp/wpo.mli | 9 ++-
13 files changed, 161 insertions(+), 102 deletions(-)
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index cccb5817a93..093befdcd5f 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -29,6 +29,7 @@ type node = {
goal : Wpo.t ; (* only GoalAnnot of a sequent *)
parent : node option ;
mutable script : script ;
+ mutable stats : Stats.stats ;
mutable search_index : int ;
mutable search_space : Strategy.t array ; (* sorted by priority *)
}
@@ -128,13 +129,6 @@ let rec walk f node =
| Tactic (_,children) -> iter_all (walk f) children
| Opened | Script _ -> f node
-let rec witer f node =
- let proved = Wpo.is_valid node.goal in
- if proved then f ~proved node else
- match node.script with
- | Tactic (_,children) -> iter_all (witer f) children
- | Opened | Script _ -> f ~proved node
-
let iteri f tree =
match tree.root with
| None -> ()
@@ -152,30 +146,37 @@ let pending n =
let k = ref 0 in
walk (fun _ -> incr k) n ; !k
-let has_pending n =
- try walk (fun _ -> raise Exit) n ; false
- with Exit -> true
-
-let consolidate root =
- let result = ref VCS.valid in
- witer
- (fun ~proved:_ node ->
- let rs = List.map snd (Wpo.get_results node.goal) in
- result := VCS.merge !result (VCS.best rs) ;
- ) root ;
- !result
-
-let validate ?(incomplete=false) tree =
+let rec consolidate n =
+ let s =
+ if Wpo.is_valid n.goal then
+ Stats.results ~smoke:false (Wpo.get_results n.goal)
+ else
+ match n.script with
+ | Opened | Script _ -> Stats.empty
+ | Tactic(_,children) ->
+ let qed = Wpo.qed_time n.goal in
+ let results = List.map (fun (_,n) -> consolidate n) children in
+ Stats.tactical ~qed results
+ in n.stats <- s ; s
+
+let validate tree =
match tree.root with
| None -> ()
| Some root ->
if not (Wpo.is_valid tree.main) then
- if incomplete then
- let result = consolidate root in
- Wpo.set_result tree.main VCS.Tactical result
- else
- if not (has_pending root) then
- Wpo.set_result tree.main VCS.Tactical VCS.valid
+ let stats = consolidate root in
+ Wpo.set_result tree.main Tactical (Stats.script stats)
+
+let consolidated wpo =
+ let smoke = Wpo.is_smoke_test wpo in
+ let prs = Wpo.get_results wpo in
+ try
+ if Wpo.is_smoke_test wpo || not (PROOFS.mem wpo) then raise Not_found ;
+ match PROOFS.get wpo with
+ | { root = Some { stats ; script = Tactic _ } } -> stats
+ | _ -> raise Not_found
+ with Not_found ->
+ Stats.results ~smoke prs
(* -------------------------------------------------------------------------- *)
(* --- Accessors --- *)
@@ -186,6 +187,7 @@ let head t = match t.head with
| None -> t.main
| Some n -> n.goal
let goal n = n.goal
+let stats n = n.stats
let tree_context t = Wpo.get_context t.main
let node_context n = Wpo.get_context n.goal
let parent n = n.parent
@@ -320,6 +322,7 @@ let mk_tree_node ~tree ~anchor goal = {
tree = tree.main ; goal ;
parent = Some anchor ;
script = Opened ;
+ stats = Stats.empty ;
search_index = 0 ;
search_space = [| |] ;
}
@@ -328,6 +331,7 @@ let mk_root_node goal = {
tree = goal ; goal ;
parent = None ;
script = Opened ;
+ stats = Stats.empty ;
search_index = 0 ;
search_space = [| |] ;
}
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index 55dde001ca1..03c14eb81ee 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -34,10 +34,14 @@ val get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]
val proof : main:Wpo.t -> tree
val reset : tree -> unit
val remove : Wpo.t -> unit
-val validate : ?incomplete:bool -> tree -> unit
-(** Leaves are numbered from 0 to n-1 *)
+(** Re-compute stats & set status of the entire script *)
+val validate : tree -> unit
+
+(** Consolidate statistics wrt current script or prover results *)
+val consolidated : Wpo.t -> Stats.stats
+(** Leaves are numbered from 0 to n-1 *)
type status = [
| `Unproved (** proof obligation not proved *)
@@ -67,6 +71,7 @@ val node_context : node -> WpContext.t
val title : node -> string
val proved : node -> bool
val pending : node -> int
+val stats : node -> Stats.stats
val parent : node -> node option
val children : node -> (string * node) list
val tactical : node -> ProofScript.jtactic option
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 652b0220a88..ea335f1aecb 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -141,13 +141,13 @@ struct
let stuck env =
if not env.signaled then
begin
- ProofEngine.validate ~incomplete:true env.tree ;
+ ProofEngine.validate env.tree ;
env.success (ProofEngine.main env.tree) None ;
env.signaled <- true ;
end
let validate ?(finalize=false) env =
- ProofEngine.validate ~incomplete:true env.tree ;
+ ProofEngine.validate env.tree ;
if not env.signaled then
let wpo = ProofEngine.main env.tree in
let proved = Wpo.is_valid wpo in
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index ebd9a175550..cd724a5c7eb 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -36,6 +36,7 @@ type pstats = {
}
type stats = {
+ verdict : VCS.verdict ;
provers : (VCS.prover * pstats) list ;
tactics : int ;
proved : int ;
@@ -84,11 +85,6 @@ let ptime t valid =
{ tmin = t ; tval = t ; tmax = t ; time = t ; tnbr = 1.0 ;
success = if valid then 1.0 else 0.0 }
-let psmoke r =
- { pzero with
- time = r.prover_time ;
- success = if VCS.is_valid valid then 1.0 else 0.0 }
-
let pqed r = ptime r.solver_time (VCS.is_valid r)
let presult r = ptime r.prover_time (VCS.is_valid r)
let psolver r = ptime r.solver_time false
@@ -97,7 +93,8 @@ let psolver r = ptime r.solver_time false
(* --- Global Stats --- *)
(* -------------------------------------------------------------------------- *)
-let zero = {
+let empty = {
+ verdict = NoResult;
provers = [];
tactics = 0;
proved = 0;
@@ -108,46 +105,75 @@ let zero = {
cached = 0 ;
}
-let choose (p,rp) (q,rq) =
- if VCS.leq rp rq then (p,rp) else (q,rq)
+let choose_best a b =
+ if VCS.leq (snd a) (snd b) then a else b
+
+let choose_worst a b =
+ if VCS.leq (snd b) (snd a) then a else b
-let consolidated ~smoke = function
+let consolidated_valid = function
| [] -> NoResult, 0, []
| u::w as results ->
- let p,r = List.fold_left choose u w in
+ let p,r = List.fold_left choose_best u w in
let cached =
p = Qed ||
if VCS.is_valid r then r.cached else
List.for_all
(fun (_,r) -> r.VCS.cached || not (VCS.is_verdict r))
results in
- r.verdict,
+ r.VCS.verdict,
(if cached then 1 else 0),
if p = Qed then [Qed,pqed r]
- else pmerge [Qed,psolver r] [p,if smoke then psmoke r else presult r]
-
-let smoked_result (p,r) = p, { r with verdict = VCS.smoked r.verdict }
+ else pmerge [Qed,psolver r] [p,presult r]
-let results ~smoke prs =
- let prs = if smoke then List.map smoked_result prs else prs in
- let verdict, cached, provers = consolidated ~smoke prs in
- verdict,
+let valid_stats prs =
+ let verdict, cached, provers = consolidated_valid prs in
match verdict with
| Valid ->
- { zero with provers ; cached ; proved = 1 }
+ { empty with verdict ; provers ; cached ; proved = 1 }
| Timeout | Stepout ->
- { zero with provers ; cached ; timeout = 1 }
+ { empty with verdict ; provers ; cached ; timeout = 1 }
| Unknown ->
- { zero with provers ; cached ; unknown = 1 }
+ { empty with verdict ; provers ; cached ; unknown = 1 }
| NoResult | Computing _ ->
- { zero with provers ; cached ; noresult = 1 }
+ { empty with verdict ; provers ; cached ; noresult = 1 }
| Failed | Invalid ->
- { zero with provers ; cached ; failed = 1 }
+ { empty with verdict ; provers ; cached ; failed = 1 }
+
+let results ~smoke prs =
+ if not smoke then valid_stats prs
+ else
+ let verdict, missing =
+ List.partition (fun (_,r) -> VCS.is_verdict r) prs in
+ let doomed, passed =
+ List.partition (fun (_,r) -> VCS.is_valid r) verdict in
+ if doomed <> [] then
+ valid_stats doomed
+ else
+ let cached = List.fold_left
+ (fun c (_,r) -> if r.VCS.cached then succ c else c)
+ 0 doomed in
+ let stucked = List.map
+ (fun (p,r) -> p, ptime r.prover_time true)
+ doomed in
+ let solver = List.fold_left
+ (fun t (_,r) -> t +. r.solver_time)
+ 0.0 doomed in
+ let provers = pmerge [Qed,ptime solver false] stucked in
+ let verdict =
+ if missing <> [] then NoResult else
+ match passed with
+ | [] -> NoResult
+ | u::w -> (snd @@ List.fold_left choose_worst u w).verdict in
+ let proved = List.length passed in
+ let failed = List.length missing + List.length doomed in
+ { empty with verdict ; provers ; cached ; proved ; failed }
let add a b =
- if a == zero then b else
- if b == zero then a else
+ if a == empty then b else
+ if b == empty then a else
{
+ verdict = VCS.combine a.verdict b.verdict ;
provers = pmerge a.provers b.provers ;
tactics = a.tactics + b.tactics ;
proved = a.proved + b.proved ;
@@ -159,9 +185,19 @@ let add a b =
}
let tactical ~qed children =
- let valid = children = [] in
- let provers = [Qed,ptime qed valid] in
- List.fold_left add { zero with provers ; tactics = 1 } children
+ let valid = List.for_all (fun c -> c.verdict = Valid) children in
+ let qed_only = children = [] in
+ let verdict = if valid then Valid else Unknown in
+ let provers = [Qed,ptime qed qed_only] in
+ List.fold_left add { empty with verdict ; provers ; tactics = 1 } children
+
+let script stats =
+ let cached = stats.cached = stats.proved in
+ let solver = List.fold_left
+ (fun t (p,s) -> if p = Qed then t +. s.time else t) 0.0 stats.provers in
+ let time = List.fold_left
+ (fun t (p,s) -> if p <> Qed then t +. s.time else t) 0.0 stats.provers in
+ VCS.result ~cached ~solver ~time stats.verdict
(* -------------------------------------------------------------------------- *)
(* --- Utils --- *)
@@ -195,20 +231,20 @@ let pp_pstats fmt p =
let pp_stats ~shell ~updating fmt s =
let vp = s.proved in
let np = proofs s in
- if vp < np && np > 1 then
- Format.fprintf fmt " (Proofs %d/%d)" vp np ;
if s.tactics > 1 then
- Format.fprintf fmt " (Tactics %d)" s.tactics
- else if np <= 1 && s.tactics = 1 then
- Format.fprintf fmt " (Tactic)" ;
+ Format.fprintf fmt " (Script %d)" s.tactics
+ else if s.tactics = 1 then
+ Format.fprintf fmt " (Script)" ;
let perfo = not shell || (not updating && s.cached < vp) in
- let only_qed = match s.provers with [Qed,_] -> true | _ -> false in
+ let qed_only =
+ match s.provers with [Qed,_] -> vp = np | _ -> false in
List.iter
(fun (p,pr) ->
let success = truncate pr.success in
let print_perfo = perfo && pr.time > Rformat.epsilon in
let print_proofs = success > 0 && np > 1 in
- if p != Qed || only_qed || print_perfo || print_proofs then
+ let print_qed = qed_only && s.verdict = Valid && vp = np in
+ if p != Qed || print_qed || print_perfo || print_proofs then
begin
let title = VCS.title_of_prover ~version:false p in
Format.fprintf fmt " (%s" title ;
@@ -229,6 +265,8 @@ let pp_stats ~shell ~updating fmt s =
else
Format.fprintf fmt " (Cached %d/%d)" s.cached np
+let pretty = pp_stats ~shell:false ~updating:false
+
(* -------------------------------------------------------------------------- *)
(* --- Yojson --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Stats.mli b/src/plugins/wp/Stats.mli
index c1ced421667..cf83426f8f3 100644
--- a/src/plugins/wp/Stats.mli
+++ b/src/plugins/wp/Stats.mli
@@ -36,6 +36,7 @@ type pstats = {
(** Cumulated Stats *)
type stats = {
+ verdict : VCS.verdict ;
provers : (VCS.prover * pstats) list ;
tactics : int ;
proved : int ;
@@ -48,9 +49,12 @@ type stats = {
val pp_pstats : Format.formatter -> pstats -> unit
val pp_stats : shell:bool -> updating:bool -> Format.formatter -> stats -> unit
+val pretty : Format.formatter -> stats -> unit
-val results : smoke:bool -> (VCS.prover * VCS.result) list -> VCS.verdict * stats
+val empty : stats
+val results : smoke:bool -> (VCS.prover * VCS.result) list -> stats
val tactical : qed:float -> stats list -> stats
+val script : stats -> VCS.result
val proofs : stats -> int
val complete : stats -> bool
diff --git a/src/plugins/wp/VC.ml b/src/plugins/wp/VC.ml
index cf8ebc3518c..8a033bbc2ce 100644
--- a/src/plugins/wp/VC.ml
+++ b/src/plugins/wp/VC.ml
@@ -41,8 +41,8 @@ let get_logout = Wpo.get_file_logout
let get_logerr = Wpo.get_file_logerr
let is_trivial = Wpo.is_trivial
let is_valid = Wpo.is_valid
-let is_unknown = Wpo.is_unknown
let is_passed = Wpo.is_passed
+let has_unknown = Wpo.has_unknown
let get_formula po =
match po.po_formula with
diff --git a/src/plugins/wp/VC.mli b/src/plugins/wp/VC.mli
index ac4abf38e2a..fc3724a2b36 100644
--- a/src/plugins/wp/VC.mli
+++ b/src/plugins/wp/VC.mli
@@ -48,11 +48,11 @@ val get_sequent : t -> Conditions.sequent
val get_formula: t -> Lang.F.pred
val is_trivial : t -> bool
-(** One prover at least returns Valid verdict. *)
+(** One prover at least returns a valid verdict. *)
val is_valid : t -> bool
-(** No prover with Valid verdict, and at least one non-Valid verdict. *)
-val is_unknown : t -> bool
+(** At least one non-valid verdict. *)
+val has_unknown : t -> bool
(** Same as [is_valid] for non-smoke tests. For smoke-tests,
same as [is_unknown]. *)
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 7e56f3caa29..b4d955ed251 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -209,6 +209,7 @@ let is_result = function
let is_verdict r = is_result r.verdict
let is_valid = function { verdict = Valid } -> true | _ -> false
+let is_not_valid r = is_verdict r && not (is_valid r)
let is_computing = function { verdict=Computing _ } -> true | _ -> false
let smoked = function
@@ -349,16 +350,16 @@ let pp_result_qualif ?(updating=true) prover result fmt =
else
pp_result fmt result
+let vrank = function
+ | NoResult | Computing _ -> 0
+ | Failed -> 1
+ | Unknown -> 2
+ | Timeout | Stepout -> 3
+ | Valid -> 4
+ | Invalid -> 5
+
let compare p q =
- let rank = function
- | NoResult | Computing _ -> 0
- | Failed -> 1
- | Unknown -> 2
- | Timeout | Stepout -> 3
- | Valid -> 4
- | Invalid -> 5
- in
- let r = rank q.verdict - rank p.verdict in
+ let r = vrank q.verdict - vrank p.verdict in
if r <> 0 then r else
let s = Stdlib.compare p.prover_steps q.prover_steps in
if s <> 0 then s else
@@ -394,5 +395,4 @@ let leq r1 r2 =
| _ -> compare r1 r2 <= 0
let choose r1 r2 = if leq r1 r2 then r1 else r2
-
let best = List.fold_left choose no_result
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 1f384006307..818fb7667f5 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -114,6 +114,7 @@ val is_auto : prover -> bool
val is_result : verdict -> bool
val is_verdict : result -> bool
val is_valid: result -> bool
+val is_not_valid: result -> bool
val is_computing: result -> bool
val is_proved: smoke:bool -> result -> bool
@@ -129,6 +130,7 @@ val pp_result_qualif : ?updating:bool -> prover -> result ->
val compare : result -> result -> int (* best is minimal *)
+val combine : verdict -> verdict -> verdict
val merge : result -> result -> result
val leq : result -> result -> bool
val choose : result -> result -> result
diff --git a/src/plugins/wp/gui/GuiNavigator.ml b/src/plugins/wp/gui/GuiNavigator.ml
index c99c230f647..8928431f449 100644
--- a/src/plugins/wp/gui/GuiNavigator.ml
+++ b/src/plugins/wp/gui/GuiNavigator.ml
@@ -139,7 +139,7 @@ class behavior
| `All -> true
| `Smoke -> Wpo.is_smoke_test g
| `Scripts -> has_proof g
- | `ToProve -> to_prove g && (Wpo.is_unknown g || has_proof g)
+ | `ToProve -> to_prove g && (Wpo.has_unknown g || has_proof g)
in if ok then list#add g
in
begin
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index aa8d04a8b6a..bdd6e296559 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -295,20 +295,20 @@ let do_wpo_result goal prover res =
do_wpo_stat goal prover res ;
end
-let do_report_stats ~shell ~updating ~smoke goal (verdict,stats) =
+let do_report_stats ~shell ~updating ~smoke goal (stats : Stats.stats) =
let status =
if smoke then
- match verdict with
- | VCS.NoResult | Computing _ -> ""
+ match stats.verdict with
| Valid -> "Failed (Doomed)"
| Failed -> "Unknown (Failure)"
- | Invalid -> "Passed (Invalid)"
+ | NoResult | Computing _ -> "Unknown (Incomplete)"
| Unknown -> "Passed (Unknown)"
| Timeout -> "Passed (Timeout)"
| Stepout -> "Passed (Stepout)"
+ | Invalid -> "Passed (Invalid)"
else
- match verdict with
- | VCS.NoResult | Computing _ -> ""
+ match stats.verdict with
+ | NoResult | Computing _ -> ""
| Valid -> "Valid"
| Invalid -> "Invalid"
| Failed -> "Failure"
@@ -329,12 +329,11 @@ let do_wpo_success ~shell ~updating goal success =
"[Generated] Goal %s (%a)" (Wpo.get_gid goal) VCS.pp_prover prover
else
let smoke = Wpo.is_smoke_test goal in
- let prs = Wpo.get_results goal in
- let (verdict,_) as vstats = Stats.results ~smoke prs in
+ let stats = ProofEngine.consolidated goal in
begin
- if shell || verdict <> Valid then
- do_report_stats ~shell ~updating goal ~smoke vstats ;
- if smoke && verdict <> Valid then
+ if shell || stats.verdict <> Valid then
+ do_report_stats ~shell ~updating goal ~smoke stats ;
+ if smoke && stats.verdict <> Valid then
begin
let target = Wpo.get_target goal in
let source = fst (Property.location target) in
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 852c10d1bdd..361ef48ee20 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -830,18 +830,22 @@ let compute g =
let is_valid g =
is_trivial g || List.exists (fun (_,r) -> VCS.is_valid r) (get_results g)
-let is_unknown g =
- not (is_valid g) &&
- List.exists
- (fun (_,r) -> VCS.is_verdict r && not (VCS.is_valid r))
- (get_results g)
+let all_not_valid g =
+ not (is_trivial g) &&
+ List.for_all (fun (_,r) -> VCS.is_not_valid r) (get_results g)
let is_passed g =
if is_smoke_test g then
- is_unknown g
+ all_not_valid g
else
is_valid g
+let has_unknown g =
+ not (is_valid g) &&
+ List.exists
+ (fun (_,r) -> VCS.is_verdict r && not (VCS.is_valid r))
+ (get_results g)
+
(* -------------------------------------------------------------------------- *)
(* --- Proof Obligations : Pretty-printing --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index 4023e885a48..e5f8c3313b8 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -199,11 +199,14 @@ val is_trivial : t -> bool
val is_valid : t -> bool
(** Checks for some prover with valid verdict (no forced simplification) *)
-val is_unknown : t -> bool
-(** Checks that all provers has a non-valid verdict *)
+val all_not_valid : t -> bool
+(** Checks for all provers to give a non-valid, computed verdict *)
val is_passed : t -> bool
-(** valid, or unknown for smoke tests *)
+(** valid, or all-not-valid for smoke tests *)
+
+val has_unknown : t -> bool
+(** Checks there is some provers with a non-valid verdict *)
val warnings : t -> Warning.t list
--
GitLab