From c3243f75ccc78aab32ae2734a977ac57d74a2cf1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 8 Jun 2023 14:18:21 +0200
Subject: [PATCH] [wp] refactor prover stats
---
src/plugins/wp/Cache.ml | 2 +-
src/plugins/wp/ProofEngine.ml | 22 ++-
src/plugins/wp/ProofScript.ml | 2 -
src/plugins/wp/ProverWhy3.ml | 3 +-
src/plugins/wp/Stats.ml | 180 ++++++------------
src/plugins/wp/Stats.mli | 18 +-
src/plugins/wp/VCS.ml | 72 +++----
src/plugins/wp/VCS.mli | 17 +-
src/plugins/wp/gui/GuiList.ml | 12 +-
src/plugins/wp/gui/GuiProver.ml | 2 +-
src/plugins/wp/register.ml | 54 +++---
.../oracle_qualif/bsearch.res.oracle | 1 +
.../oracle_qualif/euclid.res.oracle | 1 +
.../wp_plugin/oracle_qualif/doomed.res.oracle | 4 +-
.../oracle_qualif/doomed_axioms.res.oracle | 4 +-
.../oracle_qualif/doomed_call.1.res.oracle | 4 +-
.../oracle_qualif/doomed_call.2.res.oracle | 4 +-
.../oracle_qualif/doomed_dead.0.res.oracle | 4 +-
.../oracle_qualif/doomed_dead.1.res.oracle | 4 +-
.../oracle_qualif/doomed_localinit.res.oracle | 3 +-
.../oracle_qualif/doomed_loop.res.oracle | 4 +-
.../oracle_qualif/doomed_pre.res.oracle | 3 +-
.../oracle_qualif/doomed_report_ko.res.oracle | 4 +-
.../oracle_qualif/doomed_report_ok.res.oracle | 1 +
.../oracle_qualif/doomed_unreach.res.oracle | 1 +
.../oracle_qualif/doomed_unroll.res.oracle | 1 +
.../oracle_qualif/no_step_limit.res.oracle | 2 +-
.../oracle_qualif/nosession.res.oracle | 4 +-
.../oracle_qualif/unsigned.res.oracle | 2 +-
.../wp/tests/wp_tip/oracle/clear.res.oracle | 4 +-
.../wp_tip/oracle/induction_typing.res.oracle | 2 +-
.../wp/tests/wp_tip/oracle/split.res.oracle | 46 ++---
.../tac_split_quantifiers.res.oracle | 10 +-
src/plugins/wp/wpReport.ml | 8 +-
src/plugins/wp/wpo.ml | 2 +-
35 files changed, 220 insertions(+), 287 deletions(-)
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index f5867c9db28..2751c487e98 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -157,7 +157,7 @@ let steps_seized steps steplimit =
let promote ?timeout ?steplimit (res : VCS.result) =
match res.verdict with
| VCS.NoResult | VCS.Computing _ | VCS.Failed -> VCS.no_result
- | VCS.Invalid | VCS.Valid | VCS.Unknown ->
+ | VCS.Valid | VCS.Unknown ->
if not (steps_fits res.prover_steps steplimit) then
{ res with verdict = Stepout }
else
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index 89a4bbb2c96..0c4b341c4fe 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -155,21 +155,21 @@ let pending n =
let is_prover_result (p,_) = p <> VCS.Tactical
-let prover_stats goal =
- Stats.results ~smoke:(Wpo.is_smoke_test goal) @@
+let prover_stats ~smoke goal =
+ Stats.results ~smoke @@
List.filter is_prover_result @@
Wpo.get_results goal
-let rec consolidate n =
+let rec consolidate ~smoke n =
let s =
if Wpo.is_valid n.goal then
- prover_stats n.goal
+ prover_stats ~smoke n.goal
else
match n.script with
- | Opened | Script _ -> prover_stats n.goal
+ | Opened | Script _ -> prover_stats ~smoke n.goal
| Tactic(_,children) ->
let qed = Wpo.qed_time n.goal in
- let results = List.map (fun (_,n) -> consolidate n) children in
+ let results = List.map (fun (_,n) -> consolidate ~smoke n) children in
Stats.tactical ~qed results
in n.stats <- s ; s
@@ -177,17 +177,19 @@ let validate tree =
match tree.root with
| None -> ()
| Some root ->
- if not (Wpo.is_valid tree.main) then
- let stats = consolidate root in
+ let main = tree.main in
+ if not (Wpo.is_valid main) then
+ let stats = consolidate ~smoke:(Wpo.is_smoke_test main) root in
Wpo.set_result tree.main Tactical (Stats.script stats)
let consolidated wpo =
+ let smoke = Wpo.is_smoke_test wpo in
try
- if Wpo.is_smoke_test wpo || not (PROOFS.mem wpo) then raise Not_found ;
+ if smoke || 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 -> prover_stats wpo
+ with Not_found -> prover_stats ~smoke wpo
(* -------------------------------------------------------------------------- *)
(* --- Accessors --- *)
diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index a654b1f4212..c8d5ede112b 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -336,7 +336,6 @@ let json_of_verdict = function
| VCS.Unknown -> `String "unknown"
| VCS.Timeout -> `String "timeout"
| VCS.Stepout -> `String "stepout"
- | VCS.Invalid -> `String "invalid"
| VCS.Failed -> `String "failed"
let verdict_of_json = function
@@ -344,7 +343,6 @@ let verdict_of_json = function
| `String "unknown" -> VCS.Unknown
| `String "timeout" -> VCS.Timeout
| `String "stepout" -> VCS.Stepout
- | `String "invalid" -> VCS.Invalid
| `String "failed" -> VCS.Failed
| _ -> VCS.NoResult
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 7a9bd2fa1a7..8a81cbafb47 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1188,10 +1188,9 @@ let ping_prover_call ~config p =
match pr.pr_answer with
| Timeout -> VCS.timeout pr.pr_time
| Valid -> VCS.result ~time:pr.pr_time ~steps:pr.pr_steps VCS.Valid
- | Invalid -> VCS.result ~time:pr.pr_time ~steps:pr.pr_steps VCS.Invalid
| OutOfMemory -> VCS.failed "out of memory"
| StepLimitExceeded -> VCS.result ?steps:p.steps VCS.Stepout
- | Unknown _ -> VCS.unknown
+ | Unknown _ | Invalid -> VCS.unknown
| _ when p.interrupted -> VCS.timeout p.timeout
| Failure s -> VCS.failed s
| HighFailure ->
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index 4b24c8f82fb..fcdee85cb04 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -36,16 +36,16 @@ type pstats = {
}
type stats = {
- verdict : VCS.verdict ;
+ best : VCS.verdict ;
provers : (VCS.prover * pstats) list ;
tactics : int ;
proved : int ;
- trivial : int ;
timeout : int ;
unknown : int ;
noresult : int ;
failed : int ;
cached : int ;
+ cachemiss : int ;
}
(* -------------------------------------------------------------------------- *)
@@ -86,17 +86,19 @@ 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 psolver r = ptime r.solver_time false
let pqed r = if VCS.is_valid r then ptime r.solver_time true else pzero
let presult r = if VCS.is_valid r then ptime r.prover_time true else pzero
-let psolver r = ptime r.solver_time false
-let psmoked = { pzero with success = 1.0 }
+let qsmoked r = if VCS.is_valid r then ptime r.solver_time false else ptime 0.0 true
+let psmoked r = if VCS.is_valid r then ptime r.prover_time false else ptime 0.0 true
+let vsmoked v = if VCS.is_proved ~smoke:true v then VCS.Valid else VCS.Failed
(* -------------------------------------------------------------------------- *)
(* --- Global Stats --- *)
(* -------------------------------------------------------------------------- *)
let empty = {
- verdict = NoResult;
+ best = NoResult;
provers = [];
tactics = 0;
proved = 0;
@@ -104,103 +106,40 @@ let empty = {
unknown = 0 ;
noresult = 0 ;
failed = 0 ;
- trivial = 0 ;
cached = 0 ;
+ cachemiss = 0 ;
}
-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 is_trivial (p,r) =
- p = Qed || VCS.is_trivial r
-
-let is_cached ((_,r) as pr) =
- r.VCS.cached || not (VCS.is_verdict r) || is_trivial pr
-
-type consolidated = {
- cs_verdict : VCS.verdict ;
- cs_cached : int ;
- cs_trivial : int ;
- cs_provers : (prover * pstats) list ;
-}
-
-let consolidated = function
- | [] ->
- { cs_verdict = NoResult ;
- cs_trivial = 0 ;
- cs_cached = 0 ;
- cs_provers = [] }
- | (u::w) as results ->
- let (p,r) as pr = List.fold_left choose_best u w in
- let trivial = is_trivial pr in
- let cached = not trivial && List.for_all is_cached results in
- let provers =
- if p = Qed then [Qed,pqed r]
- else pmerge [Qed,psolver r] [p,presult r]
- in
- {
- cs_verdict = r.VCS.verdict ;
- cs_trivial = (if trivial then 1 else 0) ;
- cs_cached = (if cached then 1 else 0) ;
- cs_provers = provers ;
- }
-
-let stats prs =
- let { cs_verdict = verdict ;
- cs_trivial = trivial ;
- cs_cached = cached ;
- cs_provers = provers ;
- } = consolidated prs in
- match verdict with
- | Valid ->
- { empty with verdict ; provers ; trivial ; cached ; proved = 1 }
- | Timeout | Stepout ->
- { empty with verdict ; provers ; trivial ; cached ; timeout = 1 }
- | Unknown ->
- { empty with verdict ; provers ; trivial ; cached ; unknown = 1 }
- | NoResult | Computing _ ->
- { empty with verdict ; provers ; trivial ; cached ; noresult = 1 }
- | Failed | Invalid ->
- { empty with verdict ; provers ; trivial ; cached ; failed = 1 }
-
-let results ~smoke prs =
- if not smoke then 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
- stats doomed
- else
- let trivial = List.fold_left
- (fun c (p,r) -> if p = Qed || VCS.is_trivial r then succ c else c)
- 0 passed in
- let cached = List.fold_left
- (fun c (_,r) -> if r.VCS.cached then succ c else c)
- 0 passed in
- let stucked = List.map (fun (p,_) -> p,psmoked) passed in
- let solver = List.fold_left
- (fun t (_,r) -> t +. r.solver_time)
- 0.0 passed 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 in
- { empty with verdict ; provers ; trivial ; cached ; proved ; failed }
+let cacheable p r = p <> Qed && not @@ VCS.is_trivial r
+let add_cached n (p,r) = if cacheable p r && r.cached then succ n else n
+let add_cachemiss n (p,r) = if cacheable p r && not r.cached then succ n else n
+
+let results ~smoke results =
+ let (p,r) = VCS.best results in
+ let verdict = if smoke then vsmoked r.verdict else r.verdict in
+ let is v = if verdict == v then 1 else 0 in
+ let proved = is Valid in
+ let timeout = is Timeout + is Stepout in
+ let failed = is Failed in
+ let unknown = is Unknown in
+ let noresult = 1 - proved - timeout - failed - unknown in
+ (* ENSURES: noresult <= 0 && subgoals result == 1 *)
+ { (* returns verdict of provers, not verdict for the (smoked) goal *)
+ best = r.verdict ; tactics = 0 ;
+ proved ; timeout ; unknown ; failed ; noresult ;
+ cached = List.fold_left add_cached 0 results ;
+ cachemiss = List.fold_left add_cachemiss 0 results ;
+ provers =
+ if p = Qed then [Qed,if smoke then qsmoked r else pqed r]
+ else
+ pmerge [Qed,psolver r] [p,if smoke then psmoked r else presult r] ;
+ }
let add a b =
if a == empty then b else
if b == empty then a else
{
- verdict = VCS.combine a.verdict b.verdict ;
+ best = VCS.conjunction a.best b.best ;
provers = pmerge a.provers b.provers ;
tactics = a.tactics + b.tactics ;
proved = a.proved + b.proved ;
@@ -208,31 +147,31 @@ let add a b =
unknown = a.unknown + b.unknown ;
noresult = a.noresult + b.noresult ;
failed = a.failed + b.failed ;
- trivial = a.trivial + b.trivial ;
cached = a.cached + b.cached ;
+ cachemiss = a.cachemiss + b.cachemiss ;
}
let tactical ~qed children =
- let valid = List.for_all (fun c -> c.verdict = Valid) children in
+ let valid = List.for_all (fun c -> c.best = Valid) children in
let qed_only = children = [] in
- let verdict = if valid then Valid else Unknown in
+ let best = 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
+ List.fold_left add { empty with best ; provers ; tactics = 1 } children
let script stats =
- let cached = (stats.trivial + stats.cached = stats.proved) in
+ let cached = stats.cachemiss = 0 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
+ VCS.result ~cached ~solver ~time stats.best
(* -------------------------------------------------------------------------- *)
(* --- Utils --- *)
(* -------------------------------------------------------------------------- *)
-let proofs s = s.proved + s.timeout + s.unknown + s.noresult + s.failed
-let complete s = s.proved = proofs s
+let subgoals s = s.proved + s.timeout + s.unknown + s.noresult + s.failed
+let complete s = s.proved = subgoals s
let pp_pstats fmt p =
if p.tnbr > 0.0 &&
@@ -257,30 +196,21 @@ let pp_pstats fmt p =
Rformat.pp_time p.tmax
let pp_stats ~shell ~cache fmt s =
- let total = proofs s in
- let cacheable = total - s.trivial in
+ let total = subgoals s in
if s.tactics > 1 then
Format.fprintf fmt " (Tactics %d)" s.tactics
else if s.tactics = 1 then
Format.fprintf fmt " (Tactic)" ;
let updating = Cache.is_updating cache in
- let cache_miss =
- Cache.is_active cache && not updating && s.cached < cacheable in
- let qed_only =
- match s.provers with [Qed,_] -> s.proved = total | _ -> false in
- let print_cache =
- not qed_only && Cache.is_active cache &&
- (updating || 0 < s.trivial || 0 < s.cached)
- in
+ let qed_only = match s.provers with [Qed,_] -> true | _ -> false in
+ let print_cache = not qed_only && Cache.is_active cache in
List.iter
(fun (p,pr) ->
let success = truncate pr.success in
- let print_perfo =
- pr.time > Rformat.epsilon &&
- (not shell || cache_miss) in
let print_proofs = success > 0 && total > 1 in
- let print_qed = qed_only && s.verdict = Valid && s.proved = total in
- if p != Qed || print_qed || print_perfo || print_proofs
+ let print_perfo =
+ pr.time > Rformat.epsilon && (not shell || s.cachemiss > 0) in
+ if p != Qed || qed_only || print_perfo || print_proofs
then
begin
let title = VCS.title_of_prover ~version:false p in
@@ -292,15 +222,19 @@ let pp_stats ~shell ~cache fmt s =
Format.fprintf fmt ")"
end
) s.provers ;
- if shell && cache_miss then
- Format.fprintf fmt " (Cache miss %d)" (cacheable - s.cached)
+ if shell && s.cachemiss > 0 && not updating then
+ Format.fprintf fmt " (Cache miss %d)" s.cachemiss
else
if print_cache then
- if s.trivial = total then
- Format.fprintf fmt " (Trivial)"
+ let cacheable = s.cachemiss + s.cached in
+ if cacheable = 0 then
+ if s.best = Valid then
+ Format.pp_print_string fmt " (Trivial)"
+ else
+ Format.pp_print_string fmt " (No Cache)"
else
- if updating || s.cached = cacheable then
- Format.fprintf fmt " (Cached)"
+ if updating || s.cachemiss = 0 then
+ Format.pp_print_string fmt " (Cached)"
else
Format.fprintf fmt " (Cached %d/%d)" s.cached cacheable
diff --git a/src/plugins/wp/Stats.mli b/src/plugins/wp/Stats.mli
index 419fdfc1b81..5ac456b19ae 100644
--- a/src/plugins/wp/Stats.mli
+++ b/src/plugins/wp/Stats.mli
@@ -38,16 +38,16 @@ type pstats = {
Remark: for each sub-goal, only the _best_ prover result is kept *)
type stats = {
- verdict : VCS.verdict ; (** global verdict *)
+ best : VCS.verdict ; (** provers best verdict (not verdict of the goal) *)
provers : (VCS.prover * pstats) list ; (** meaningfull provers *)
tactics : int ; (** number of tactics *)
proved : int ; (** number of proved sub-goals *)
- trivial : int ; (** number of proved sub-goals with Qed or No-prover time *)
- timeout : int ; (** number of resulting timeouts and stepouts *)
- unknown : int ; (** number of resulting unknown *)
- noresult : int ; (** number of no-result *)
- failed : int ; (** number of resulting failures *)
- cached : int ; (** number of cached (non-trivial) results *)
+ timeout : int ; (** number of timeouts and stepouts sub-goals *)
+ unknown : int ; (** number of unknown sub-goals *)
+ noresult : int ; (** number of no-result sub-goals *)
+ failed : int ; (** number of failed sub-goals *)
+ cached : int ; (** number of cached prover results *)
+ cachemiss : int ; (** number of non-cached prover results *)
}
val pp_pstats : Format.formatter -> pstats -> unit
@@ -65,7 +65,9 @@ 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 subgoals : stats -> int
+(* sum of proved + timeout + unit + noresult + failed *)
+
val complete : stats -> bool
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index e4b0d5f91ee..1b8b67db730 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -192,7 +192,6 @@ let get_stepout = function
type verdict =
| NoResult
- | Invalid
| Unknown
| Timeout
| Stepout
@@ -211,7 +210,7 @@ type result = {
}
let is_result = function
- | Valid | Unknown | Invalid | Timeout | Stepout | Failed -> true
+ | Valid | Unknown | Timeout | Stepout | Failed -> true
| NoResult | Computing _ -> false
let is_verdict r = is_result r.verdict
@@ -219,15 +218,10 @@ let is_valid = function { verdict = Valid } -> true | _ -> false
let is_trivial r = is_valid r && r.prover_time = 0.0
let is_not_valid r = is_verdict r && not (is_valid r)
let is_computing = function { verdict=Computing _ } -> true | _ -> false
-
-let smoked = function
- | (Failed | NoResult | Computing _) as r -> r
- | Valid -> Invalid
- | Invalid | Unknown | Timeout | Stepout -> Valid
-
-let verdict ~smoke r = if smoke then smoked r.verdict else r.verdict
-
-let is_proved ~smoke r = (verdict ~smoke r = Valid)
+let is_proved ~smoke = function
+ | NoResult | Computing _ | Failed -> false
+ | Valid -> not smoke
+ | Unknown | Timeout | Stepout -> smoke
let configure r =
let valid = (r.verdict = Valid) in
@@ -280,7 +274,6 @@ let result ?(cached=false) ?(solver=0.0) ?(time=0.0) ?(steps=0) verdict =
let no_result = result NoResult
let valid = result Valid
-let invalid = result Invalid
let unknown = result Unknown
let timeout t = result ~time:t Timeout
let stepout n = result ~steps:n Stepout
@@ -320,7 +313,6 @@ let pp_perf_shell fmt r =
let name_of_verdict = function
| NoResult | Computing _ -> "none"
- | Invalid -> "invalid"
| Valid -> "valid"
| Failed -> "failed"
| Unknown -> "unknown"
@@ -331,7 +323,6 @@ let pp_result fmt r =
match r.verdict with
| NoResult -> Format.pp_print_string fmt "No Result"
| Computing _ -> Format.pp_print_string fmt "Computing"
- | Invalid -> Format.pp_print_string fmt "Invalid"
| Failed -> Format.fprintf fmt "Failed@ %s" r.prover_errmsg
| Valid -> Format.fprintf fmt "Valid%a" pp_perf_shell r
| Unknown -> Format.fprintf fmt "Unknown%a" pp_perf_shell r
@@ -358,7 +349,6 @@ let pp_result_qualif ?(updating=true) prover result fmt =
match result.verdict with
| NoResult -> Format.pp_print_string fmt "No Result"
| Computing _ -> Format.pp_print_string fmt "Computing"
- | Invalid -> Format.pp_print_string fmt "Invalid"
| Failed -> Format.fprintf fmt "Failed@ %s" result.prover_errmsg
| Valid -> pp_cache_miss fmt "Valid" updating prover result
| Unknown -> pp_cache_miss fmt "Unsuccess" updating prover result
@@ -367,13 +357,22 @@ let pp_result_qualif ?(updating=true) prover result fmt =
else
pp_result fmt result
+(* highest is best *)
let vrank = function
- | NoResult | Computing _ -> 0
- | Failed -> 1
- | Unknown -> 2
- | Timeout | Stepout -> 3
- | Valid -> 4
- | Invalid -> 5
+ | Computing _ -> 0
+ | NoResult -> 1
+ | Failed -> 2
+ | Unknown -> 3
+ | Timeout -> 4
+ | Stepout -> 5
+ | Valid -> 6
+
+let conjunction a b =
+ match a,b with
+ | Valid,Valid -> Valid
+ | Valid, r -> r
+ | r , Valid -> r
+ | _ -> if vrank b > vrank a then b else a
let compare p q =
let r = vrank q.verdict - vrank p.verdict in
@@ -384,32 +383,5 @@ let compare p q =
if t <> 0 then t else
Stdlib.compare p.solver_time q.solver_time
-let combine v1 v2 =
- match v1 , v2 with
- | Valid , Valid -> Valid
- | Failed , _ | _ , Failed -> Failed
- | Invalid , _ | _ , Invalid -> Invalid
- | Timeout , _ | _ , Timeout -> Timeout
- | Stepout , _ | _ , Stepout -> Stepout
- | _ -> Unknown
-
-let merge r1 r2 =
- let err = if r1.prover_errmsg <> "" then r1 else r2 in
- {
- verdict = combine r1.verdict r2.verdict ;
- cached = r1.cached && r2.cached ;
- solver_time = max r1.solver_time r2.solver_time ;
- prover_time = max r1.prover_time r2.prover_time ;
- prover_steps = max r1.prover_steps r2.prover_steps ;
- prover_errpos = err.prover_errpos ;
- prover_errmsg = err.prover_errmsg ;
- }
-
-let leq r1 r2 =
- match is_valid r1 , is_valid r2 with
- | true , false -> true
- | false , true -> false
- | _ -> compare r1 r2 <= 0
-
-let choose r1 r2 = if leq r1 r2 then r1 else r2
-let best = List.fold_left choose no_result
+let bestp pr1 pr2 = if compare (snd pr1) (snd pr2) <= 0 then pr1 else pr2
+let best = List.fold_left bestp (Qed,no_result)
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index f5ecae0ad98..00b754c18e6 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -82,7 +82,6 @@ val get_stepout : config -> int (** 0 means no-stepout *)
type verdict =
| NoResult
- | Invalid
| Unknown
| Timeout
| Stepout
@@ -102,7 +101,6 @@ type result = {
val no_result : result
val valid : result
-val invalid : result
val unknown : result
val stepout : int -> result
val timeout : float -> result
@@ -120,10 +118,7 @@ val is_valid: result -> bool
val is_trivial: result -> bool
val is_not_valid: result -> bool
val is_computing: result -> bool
-val is_proved: smoke:bool -> result -> bool
-
-val smoked : verdict -> verdict
-val verdict: smoke:bool -> result -> verdict
+val is_proved: smoke:bool -> verdict -> bool
val configure : result -> config
val autofit : result -> bool (** Result that fits the default configuration *)
@@ -134,12 +129,8 @@ val pp_result : Format.formatter -> result -> unit
val pp_result_qualif : ?updating:bool -> prover -> result ->
Format.formatter -> unit
-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
-val best : result list -> result
+val conjunction : verdict -> verdict -> verdict (* for tactic children *)
+val compare : result -> result -> int (* minimal is best *)
+val best : (prover * result) list -> prover * result
val dkey_shell: Wp_parameters.category
diff --git a/src/plugins/wp/gui/GuiList.ml b/src/plugins/wp/gui/GuiList.ml
index 9e83c9070ca..149c4edbef0 100644
--- a/src/plugins/wp/gui/GuiList.ml
+++ b/src/plugins/wp/gui/GuiList.ml
@@ -51,13 +51,12 @@ let render_prover_result p =
let icn_cut = icn_stock "gtk-cut" in
let icn_running = icn_stock "gtk-execute" in
let open VCS in
- let icon_of_verdict = function
+ let icon_of_verdict ~smoke = function
| NoResult -> icn_none
- | Valid -> icn_valid
- | Invalid -> icn_invalid
- | Unknown -> icn_unknown
+ | Valid -> if smoke then icn_invalid else icn_valid
+ | Unknown -> if smoke then icn_valid else icn_unknown
+ | Timeout | Stepout -> if smoke then icn_valid else icn_cut
| Failed -> icn_failed
- | Timeout | Stepout -> icn_cut
| Computing _ -> icn_running
in fun w ->
match Wpo.get_result w p , p with
@@ -71,8 +70,7 @@ let render_prover_result p =
| `Saved -> icn_stock "gtk-file"
end
| result , _ ->
- let smoke = Wpo.is_smoke_test w in
- icon_of_verdict (VCS.verdict ~smoke result)
+ icon_of_verdict ~smoke:(Wpo.is_smoke_test w) result.verdict
class pane (gprovers:GuiConfig.provers) =
let model = new model in
diff --git a/src/plugins/wp/gui/GuiProver.ml b/src/plugins/wp/gui/GuiProver.ml
index 7f02b9f6fa7..4a373fbc8b7 100644
--- a/src/plugins/wp/gui/GuiProver.ml
+++ b/src/plugins/wp/gui/GuiProver.ml
@@ -132,7 +132,7 @@ class prover ~(console:Wtext.text) ~prover =
self#set_action ~tooltip:"Run Prover" ~icon:`MEDIA_PLAY ~callback () ;
Pretty_utils.ksfprintf self#set_label "%a (%a)" VCS.pp_prover prover
Rformat.pp_time res.VCS.prover_time ;
- | VCS.Invalid | VCS.Unknown | VCS.Timeout | VCS.Stepout ->
+ | VCS.Unknown | VCS.Timeout | VCS.Stepout ->
let callback () = self#run wpo in
self#set_status ko_status ;
self#set_action ~tooltip:"Run Prover" ~icon:`MEDIA_PLAY ~callback () ;
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 88e7725affd..6938108da2e 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -187,16 +187,19 @@ module GOALS = Wpo.S.Set
let scheduled = ref 0
let exercised = ref 0
let session = ref GOALS.empty
-let global_stats = ref Stats.empty
-let script_stats = ref Stats.empty
+let prover_stats = ref Stats.empty
+let tactic_stats = ref Stats.empty
+let smoked_passed = ref 0
+let smoked_failed = ref 0
+let add_stats r s = r := Stats.add !r s
let clear_scheduled () =
begin
scheduled := 0 ;
exercised := 0 ;
session := GOALS.empty ;
- global_stats := Stats.empty ;
- script_stats := Stats.empty ;
+ prover_stats := Stats.empty ;
+ tactic_stats := Stats.empty ;
CfgInfos.trivial_terminates := 0 ;
WpReached.unreachable_proved := 0 ;
WpReached.unreachable_failed := 0 ;
@@ -304,8 +307,8 @@ let stats_to_json g (s : Stats.stats) : Json.t =
"function", `String (Kernel_function.get_name kf);
"behavior", `String bhv ;
] in
- let proofs = Stats.proofs s in
- let subgoals = if proofs > 1 then ["subgoals", `Int proofs] else [] in
+ let subgoals = Stats.subgoals s in
+ let subgoals = if subgoals > 1 then ["subgoals", `Int subgoals] else [] in
`Assoc
([
"goal", `String g.po_gid ;
@@ -315,7 +318,7 @@ let stats_to_json g (s : Stats.stats) : Json.t =
] @ index @ [
"smoke", `Bool smoke ;
"passed", `Bool (Wpo.is_passed g) ;
- "verdict", `String (VCS.name_of_verdict s.verdict) ;
+ "verdict", `String (VCS.name_of_verdict s.best) ;
] @ script @ [
"provers", `List (List.map pstats_to_json s.provers) ;
] @ subgoals @
@@ -351,7 +354,7 @@ let do_wpo_result goal prover res =
let do_report_stats ~shell ~cache ~smoke goal (stats : Stats.stats) =
let status =
if smoke then
- match stats.verdict with
+ match stats.best with
| Valid -> "[Failed] (Doomed)"
| Failed -> "[Failure] (Solver Error)"
| NoResult | Computing _ -> "[Unknown] (Incomplete)"
@@ -359,13 +362,11 @@ let do_report_stats ~shell ~cache ~smoke goal (stats : Stats.stats) =
| Unknown -> "[Passed] (Unknown)"
| Timeout -> "[Passed] (Timeout)"
| Stepout -> "[Passed] (Stepout)"
- | Invalid -> "[Passed] (Invalid)"
else
- match stats.verdict with
+ match stats.best with
| NoResult when shell -> "[CacheMiss]"
| NoResult | Computing _ -> ""
| Valid -> "[Valid]"
- | Invalid -> "[Invalid]"
| Failed -> "[Failure]"
| (Unknown | Timeout | Stepout) when shell -> "[Unsuccess]"
| Unknown -> "[Unknown]"
@@ -386,13 +387,16 @@ let do_wpo_success ~shell ~cache goal success =
else
let gui = Frama_c_very_first.Gui_init.is_gui in
let smoke = Wpo.is_smoke_test goal in
- let gstats = Stats.results ~smoke @@ Wpo.get_results goal in
+ let pstats = Stats.results ~smoke @@ Wpo.get_results goal in
let cstats = ProofEngine.consolidated goal in
let success = Wpo.is_passed goal in
begin
- global_stats := Stats.add !global_stats gstats ;
- if cstats.tactics > 0 then
- script_stats := Stats.add !script_stats cstats ;
+ add_stats prover_stats pstats ;
+ if smoke then
+ (if Wpo.is_passed goal
+ then incr smoked_passed
+ else incr smoked_failed) ;
+ if cstats.tactics > 0 then add_stats tactic_stats cstats ;
if gui || shell || not success then
do_report_stats ~shell ~cache goal ~smoke cstats ;
if smoke then
@@ -416,7 +420,7 @@ let do_report_scheduled () =
!CfgInfos.trivial_terminates in
if total > 0 then
begin
- let gstats = !global_stats in
+ let proofs = !prover_stats in
let unreachable = !WpReached.unreachable_proved in
let terminating = !CfgInfos.trivial_terminates in
let passed = GOALS.fold
@@ -439,22 +443,28 @@ let do_report_scheduled () =
if success > 0 || (not shell && p = Qed) then
add_line name success (fun fmt ->
if p = Tactical then
- Stats.pp_stats ~shell ~cache fmt !script_stats
+ Stats.pp_stats ~shell ~cache fmt !tactic_stats
else
if not shell then Stats.pp_pstats fmt s
)
- ) gstats.provers ;
- if gstats.failed > 0 then add_line "Failed" gstats.failed none ;
+ ) proofs.provers ;
+ let failed = proofs.failed in
+ if failed > 0 then add_line "Failed" failed none ;
if shell then
begin
- let n = gstats.timeout + gstats.unknown in
+ let n = Stats.subgoals proofs - proofs.proved - proofs.failed in
if n > 0 then add_line "Unsuccess" n none
end
else
begin
- if gstats.timeout > 0 then add_line "Timeout" gstats.timeout none ;
- if gstats.unknown > 0 then add_line "Unknown" gstats.unknown none ;
+ if proofs.timeout > 0 then add_line "Timeout" proofs.timeout none ;
+ if proofs.unknown > 0 then add_line "Unknown" proofs.unknown none ;
end ;
+ let smoked = !smoked_failed + !smoked_passed in
+ if smoked > 0 then
+ add_line "Smoke Tests" !smoked_passed
+ (fun fmt -> Format.fprintf fmt " / %d" smoked) ;
+ if proofs.noresult > 0 then add_line "Missing" proofs.noresult none ;
let iter f = List.iter f (List.rev !lines) in
let title (p,_,_) = p in
let pp_title fmt p = Format.fprintf fmt "%s:" p in
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
index c75c338b4d4..941e0fbf7df 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
@@ -34,6 +34,7 @@
[wp] Proved goals: 28 / 28
Qed: 8
Alt-Ergo: 20
+ Smoke Tests: 7 / 7
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
binary_search 8 20 28 100%
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
index 878ff5856b1..ff7e6a81f3c 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
@@ -22,6 +22,7 @@
[wp] Proved goals: 16 / 16
Qed: 7
Alt-Ergo: 9
+ Smoke Tests: 5 / 5
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
euclid_gcd 7 9 16 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
index be42e319576..fcd999d2765 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
@@ -13,8 +13,10 @@
[wp] doomed.i:41: Warning: Failed smoke-test
[wp] [Valid] typed_buzz_ensures (Qed)
[wp] Proved goals: 5 / 7
- Qed: 4
+ Qed: 2
Alt-Ergo: 3
+ Failed: 2
+ Smoke Tests: 3 / 5
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo - 2 3 66.7%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
index 156fa5567f5..290311caf6a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
@@ -18,7 +18,9 @@
[wp] [Valid] typed_foo_loop_assigns (Qed)
[wp] Proved goals: 7 / 10
Qed: 1
- Alt-Ergo: 9
+ Alt-Ergo: 6
+ Failed: 3
+ Smoke Tests: 0 / 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo 1 6 10 70.0%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
index 053984aed19..c344cd19769 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
@@ -41,8 +41,10 @@
[wp] [Failed] (Doomed) typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
[wp] [Valid] typed_f5_ko_ensures (Qed)
[wp] Proved goals: 28 / 33
- Qed: 15
+ Qed: 10
Alt-Ergo: 18
+ Failed: 5
+ Smoke Tests: 18 / 23
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f1_ok 2 3 5 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
index b14c7877833..82a6a29f489 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
@@ -44,8 +44,10 @@
[wp] [Failed] (Doomed) typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
[wp] [Valid] typed_f5_ko_ensures (Qed)
[wp] Proved goals: 31 / 36
- Qed: 18
+ Qed: 13
Alt-Ergo: 18
+ Failed: 5
+ Smoke Tests: 18 / 23
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f1_ok 3 3 6 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
index b4ed26cadbc..e4957a6be52 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
@@ -52,8 +52,10 @@
[wp] [Valid] typed_f5_ko_assigns_part3 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part4 (Qed)
[wp] Proved goals: 44 / 46
- Qed: 25
+ Qed: 23
Alt-Ergo: 21
+ Failed: 2
+ Smoke Tests: 21 / 23
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f1_ok 2 3 5 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
index 7af31c3fade..f48bd8b1443 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
@@ -54,8 +54,10 @@
[wp] [Valid] typed_f5_ko_assigns_part3 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part4 (Qed)
[wp] Proved goals: 46 / 48
- Qed: 27
+ Qed: 25
Alt-Ergo: 21
+ Failed: 2
+ Smoke Tests: 21 / 23
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f1_ok 3 3 6 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle
index 95c235146e5..51dbf06fb40 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle
@@ -9,9 +9,10 @@
[wp] [Unsuccess] typed_access_assert_rte_mem_access (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_access_assert_rte_mem_access_2 (Alt-Ergo) (Cached)
[wp] Proved goals: 1 / 4
- Qed: 1
Alt-Ergo: 1
+ Failed: 1
Unsuccess: 2
+ Smoke Tests: 1 / 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
access - 1 4 25.0%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
index 795cba15889..afce87cbbb7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
@@ -15,8 +15,10 @@
[wp] [Unsuccess] typed_foo_loop_invariant_B_established (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_assigns (Qed)
[wp] Proved goals: 3 / 8
- Qed: 6
+ Qed: 3
+ Failed: 3
Unsuccess: 2
+ Smoke Tests: 0 / 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo 3 - 8 37.5%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
index 01424e5495b..491593a5157 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
@@ -24,8 +24,9 @@
[wp] doomed_pre.i:56: Warning: Failed smoke-test
[wp] [Failed] (Doomed) typed_reqs_massumes_wp_smoke_B2_assumes (Qed)
[wp] Proved goals: 5 / 13
- Qed: 8
Alt-Ergo: 5
+ Failed: 8
+ Smoke Tests: 5 / 13
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
requires - - 1 0.0%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
index 69ed4be30c1..45d3c52ddf2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
@@ -18,7 +18,9 @@
[wp] [Valid] typed_foo_loop_assigns (Qed)
[wp] Proved goals: 7 / 10
Qed: 1
- Alt-Ergo: 9
+ Alt-Ergo: 6
+ Failed: 3
+ Smoke Tests: 0 / 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo 1 6 10 70.0%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
index 55cd0694206..fff595a824c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
@@ -16,6 +16,7 @@
[wp] Proved goals: 10 / 10
Qed: 1
Alt-Ergo: 9
+ Smoke Tests: 3 / 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo 1 9 10 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle
index 7038457d7b2..f951ad709d1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle
@@ -15,6 +15,7 @@
[wp] Proved goals: 6 / 9
Qed: 3
Alt-Ergo: 3
+ Smoke Tests: 3 / 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job 3 3 6 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
index cf04c0de469..122ab2295f2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
@@ -13,6 +13,7 @@
[wp] Proved goals: 5 / 5
Qed: 2
Alt-Ergo: 3
+ Smoke Tests: 3 / 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo 2 3 5 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle
index 0ad955337d7..ff42726ec4f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle
@@ -3,6 +3,6 @@
[wp] Running WP plugin...
[wp] 1 goal scheduled
[wp] Warning: no-steps does not support steps limit (ignored option)
-[wp] [Unsuccess] typed_lemma_truc (no-steps)
+[wp] [Unsuccess] typed_lemma_truc (no-steps) (Cache miss 1)
[wp] Proved goals: 0 / 1
Unsuccess: 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle
index a4605ebc81e..6f1edb60029 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle
@@ -3,5 +3,7 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
-[wp] [CacheMiss] typed_f_ensures (Cache miss 1)
+[wp] [CacheMiss] typed_f_ensures (Qed)
[wp] Proved goals: 0 / 1
+ Unsuccess: 1
+ Missing: 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
index 43ce8fab823..234a6e8800c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing unsigned.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
-[wp] [Unsuccess] typed_lemma_U32 (Tactic) (Qed 1/2) (Cache miss 1)
+[wp] [Unsuccess] typed_lemma_U32 (Tactic) (Qed 1/2)
[wp] Proved goals: 0 / 1
Unsuccess: 1
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
index df8ab558675..e390eec7786 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
@@ -105,7 +105,7 @@
Prove: P_S(42).
------------------------------------------------------------
-[wp] [Unsuccess] typed_clear_in_step_check (Tactics 3) (Cached)
+[wp] [Unsuccess] typed_clear_in_step_check (Tactics 3) (Qed)
[wp:script:allgoals]
typed_clear_ensures subgoal:
@@ -143,6 +143,6 @@
Prove: P_S(a + b).
------------------------------------------------------------
-[wp] [Unsuccess] typed_clear_ensures (Tactics 7) (Cached)
+[wp] [Unsuccess] typed_clear_ensures (Tactics 7) (Qed)
[wp] Proved goals: 0 / 2
Unsuccess: 2
diff --git a/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
index 8ac7d4b65c8..01698843ed0 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
@@ -114,7 +114,7 @@
Prove: ([ 1 ] *^ n) = a_1.
------------------------------------------------------------
-[wp] [Unsuccess] typed_function_loop_invariant_X_preserved (Tactic) (Cached)
+[wp] [Unsuccess] typed_function_loop_invariant_X_preserved (Tactic) (Qed)
[wp] Proved goals: 1 / 2
Qed: 1
Unsuccess: 1
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
index 8ce73ffc5be..25c7911f7d1 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
@@ -215,7 +215,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_branch_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_step_branch_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_or_ensures subgoal:
@@ -240,7 +240,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_or_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_step_or_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_and_ensures subgoal:
@@ -256,7 +256,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_and_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_step_and_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_peq_ensures subgoal:
@@ -273,7 +273,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_peq_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_step_peq_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_pneq_ensures subgoal:
@@ -290,7 +290,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_pneq_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_step_pneq_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_neq_ensures subgoal:
@@ -315,7 +315,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_neq_ensures (Tactic) (Qed 1/3) (Cached)
+[wp] [Unsuccess] typed_test_step_neq_ensures (Tactic) (Qed 1/3)
[wp:script:allgoals]
typed_test_step_leq_ensures subgoal:
@@ -339,7 +339,7 @@
Prover Qed returns Valid
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_leq_ensures (Tactic) (Qed 1/3) (Cached)
+[wp] [Unsuccess] typed_test_step_leq_ensures (Tactic) (Qed 1/3)
[wp:script:allgoals]
typed_test_step_lt_ensures subgoal:
@@ -369,7 +369,7 @@
Prover Qed returns Valid
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_lt_ensures (Tactic) (Qed 1/3) (Cached)
+[wp] [Unsuccess] typed_test_step_lt_ensures (Tactic) (Qed 1/3)
[wp:script:allgoals]
typed_test_step_if_ensures subgoal:
@@ -391,7 +391,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_if_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_step_if_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_fa_if_ensures subgoal:
@@ -418,7 +418,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_fa_if_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_step_fa_if_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_fa_or_ensures subgoal:
@@ -435,7 +435,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_fa_or_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_step_fa_or_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_fa_and_ensures subgoal:
@@ -448,7 +448,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_fa_and_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_step_fa_and_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_inside_leq_ensures subgoal:
@@ -479,7 +479,7 @@
Prover Qed returns Valid
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_inside_leq_ensures (Tactic) (Qed 1/3) (Cached)
+[wp] [Unsuccess] typed_test_inside_leq_ensures (Tactic) (Qed 1/3)
[wp:script:allgoals]
typed_test_inside_lt_ensures subgoal:
@@ -510,7 +510,7 @@
Prover Qed returns Valid
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_inside_lt_ensures (Tactic) (Qed 1/3) (Cached)
+[wp] [Unsuccess] typed_test_inside_lt_ensures (Tactic) (Qed 1/3)
[wp:script:allgoals]
typed_test_inside_neq_ensures subgoal:
@@ -547,7 +547,7 @@
Prove: P_Q.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_inside_neq_ensures (Tactic) (Qed 1/3) (Cached)
+[wp] [Unsuccess] typed_test_inside_neq_ensures (Tactic) (Qed 1/3)
[wp:script:allgoals]
typed_test_goal_and_ensures subgoal:
@@ -572,7 +572,7 @@
Prove: P_R.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_and_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_goal_and_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_goal_eq_ensures subgoal:
@@ -589,7 +589,7 @@
Prove: (L_LQ=true).
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_eq_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_goal_eq_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_goal_neq_ensures subgoal:
@@ -606,7 +606,7 @@
Prove: (L_LQ=false).
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_neq_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_goal_neq_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_goal_if_ensures subgoal:
@@ -633,7 +633,7 @@
Prove: P_Q.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_if_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_goal_if_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_goal_ex_and_ensures subgoal:
@@ -650,7 +650,7 @@
Prove: P_P /\ P_Q.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_ex_and_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_goal_ex_and_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_goal_ex_or_ensures subgoal:
@@ -659,7 +659,7 @@
Prove: P_P \/ P_Q \/ (exists i : Z. P_Pi(i)) \/ (exists i : Z. P_Qi(i)).
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_ex_or_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_goal_ex_or_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_goal_ex_if_ensures subgoal:
@@ -688,7 +688,7 @@
Prove: P_P /\ P_Q.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_ex_if_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_goal_ex_if_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_goal_ex_imply_ensures subgoal:
@@ -702,6 +702,6 @@
Prove: exists i : Z. P_Qi(i).
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_ex_imply_ensures (Tactic) (Cached)
+[wp] [Unsuccess] typed_test_goal_ex_imply_ensures (Tactic) (Qed)
[wp] Proved goals: 0 / 23
Unsuccess: 23
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
index 612e769d605..70c32d4d2f1 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
-[wp] [Unsuccess] typed_split_ensures_Goal_Exist_Or (Tactic) (Cache miss 1)
-[wp] [Unsuccess] typed_split_ensures_Goal_Exist_And (Tactic) (Cache miss 2)
-[wp] [Unsuccess] typed_split_ensures_Goal_Exist_And_bis (Tactic) (Cache miss 3)
-[wp] [Unsuccess] typed_split_ensures_Hyp_Forall_And (Tactic) (Cache miss 1)
-[wp] [Unsuccess] typed_split_ensures_Hyp_Forall_Or_bis (Tactic) (Cache miss 3)
+[wp] [Unsuccess] typed_split_ensures_Goal_Exist_Or (Tactic) (Qed)
+[wp] [Unsuccess] typed_split_ensures_Goal_Exist_And (Tactic) (Qed)
+[wp] [Unsuccess] typed_split_ensures_Goal_Exist_And_bis (Tactic) (Qed)
+[wp] [Unsuccess] typed_split_ensures_Hyp_Forall_And (Tactic) (Qed)
+[wp] [Unsuccess] typed_split_ensures_Hyp_Forall_Or_bis (Tactic) (Qed)
[wp] Proved goals: 0 / 5
Unsuccess: 5
------------------------------------------------------------
diff --git a/src/plugins/wp/wpReport.ml b/src/plugins/wp/wpReport.ml
index 4c95715e8b6..6e09d4fd1ab 100644
--- a/src/plugins/wp/wpReport.ml
+++ b/src/plugins/wp/wpReport.ml
@@ -94,11 +94,13 @@ let result ~status ~smoke (r:VCS.result) =
match status with
| `Passed when smoke -> VALID
| _ ->
- match VCS.verdict ~smoke r with
+ match r.VCS.verdict with
| VCS.NoResult | VCS.Computing _ -> NORESULT
| VCS.Failed -> INCONCLUSIVE
- | VCS.Invalid | VCS.Unknown | VCS.Timeout | VCS.Stepout -> UNSUCCESS
- | VCS.Valid -> VALID
+ | VCS.Unknown | VCS.Timeout | VCS.Stepout ->
+ if smoke then VALID else UNSUCCESS
+ | VCS.Valid ->
+ if smoke then UNSUCCESS else VALID
let best_result a b = match a,b with
| NORESULT,c | c,NORESULT -> c
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 2566ccb7842..c397261fd93 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -495,7 +495,7 @@ module ResultType =
let name = "Wpo.result"
let reprs =
List.map VCS.result
- [ Valid ; Invalid ; Unknown ; Timeout ; Failed ]
+ [ Valid ; Unknown ; Timeout ; Failed ]
end)
(* to get a "reasonable" API doc *)
let () = Type.set_ml_name ResultType.ty (Some "Wpo.result")
--
GitLab