Merge branch 'feature/wp/stats' into 'master'

[wp] new solver stats

See merge request frama-c/frama-c!3840

src/kernel_services/plugin_entry_points/log.ml

@@ -804,6 +804,7 @@ sig
     ('a,formatter,unit) format -> 'a
 
   val result  : ?level:int -> ?dkey:category -> 'a pretty_printer
+  val has_tty : unit -> bool
   val feedback: ?ontty:ontty -> ?level:int -> ?dkey:category -> 'a pretty_printer
   val debug   : ?level:int -> ?dkey:category -> 'a pretty_printer
   val warning : ?wkey: warn_category -> 'a pretty_printer
@@ -1038,6 +1039,8 @@ struct
 
   let transient channel = channel.terminal.isatty && !tty ()
 
+  let has_tty () = transient channel
+
   let feedback
       ?(ontty=`Message)
       ?(level=1) ?dkey ?current ?source

src/kernel_services/plugin_entry_points/log.mli

@@ -158,6 +158,9 @@ module type Messages = sig
       @since Beryllium-20090601-beta1
       @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
 
+  val has_tty : unit -> bool
+  (** Returns [true] is this Log's channel is in console mode *)
+
   val feedback : ?ontty:ontty -> ?level:int -> ?dkey:category -> 'a pretty_printer
   (** Progress and feedback. Level is tested against the verbosity level.
       @since Beryllium-20090601-beta1

src/plugins/aorai/tests/Aorai_test.ml

@@ -58,7 +58,7 @@ let extend () =
         Wp.VC.command vcs;
         Bag.iter
           (fun vc ->
-             if not (Wp.VC.is_proved vc) then
+             if not (Wp.VC.is_passed vc) then
                P.warning "Could not prove %a in automaton function %a"
                  Property.pretty (Wp.VC.get_property vc)
                  Kernel_function.pretty kf)

src/plugins/report/tests/report/oracle/classify.0.res.oracle

@@ -5,8 +5,8 @@
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
-[wp] [Qed] Goal typed_f_assigns : Valid
-[wp] [Qed] Goal typed_f_ensures : Valid
+[wp] [Valid] typed_f_assigns (Qed)
+[wp] [Valid] typed_f_ensures (Qed)
 [wp] Proved goals:    2 / 2
   Qed:             2
 [report] Classification

src/plugins/report/tests/report/oracle/classify.1.res.oracle

@@ -6,8 +6,8 @@
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
-[wp] [Qed] Goal typed_f_assigns : Valid
-[wp] [Qed] Goal typed_f_ensures : Valid
+[wp] [Valid] typed_f_assigns (Qed)
+[wp] [Valid] typed_f_ensures (Qed)
 [wp] Proved goals:    2 / 2
   Qed:             2
 [report] Classification

src/plugins/report/tests/report/oracle/classify.2.res.oracle

@@ -6,8 +6,8 @@
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
-[wp] [Qed] Goal typed_f_assigns : Valid
-[wp] [Qed] Goal typed_f_ensures : Valid
+[wp] [Valid] typed_f_assigns (Qed)
+[wp] [Valid] typed_f_ensures (Qed)
 [wp] Proved goals:    2 / 2
   Qed:             2
 [report] Classification

src/plugins/report/tests/report/oracle/classify.3.res.oracle

@@ -7,8 +7,8 @@
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
-[wp] [Qed] Goal typed_f_assigns : Valid
-[wp] [Qed] Goal typed_f_ensures : Valid
+[wp] [Valid] typed_f_assigns (Qed)
+[wp] [Valid] typed_f_ensures (Qed)
 [wp] Proved goals:    2 / 2
   Qed:             2
 [report] Classification

src/plugins/report/tests/report/oracle/classify.4.res.oracle

@@ -7,8 +7,8 @@
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
-[wp] [Qed] Goal typed_f_assigns : Valid
-[wp] [Qed] Goal typed_f_ensures : Valid
+[wp] [Valid] typed_f_assigns (Qed)
+[wp] [Valid] typed_f_ensures (Qed)
 [wp] Proved goals:    2 / 2
   Qed:             2
 [report] Classification

src/plugins/wp/Cache.ml

@@ -136,8 +136,11 @@ module MODE = WpContext.StaticGenerator(Datatype.Unit)
 let get_mode = MODE.get
 let set_mode m = MODE.clear () ; Wp_parameters.Cache.set (mode_name m)
 
-let is_updating () =
-  match MODE.get () with
+let is_active = function
+  | NoCache -> false
+  | Replay | Offline | Update | Rebuild | Cleanup -> true
+
+let is_updating = function
   | NoCache | Replay | Offline -> false
   | Update | Rebuild | Cleanup -> true
 

src/plugins/wp/Cache.mli

@@ -30,7 +30,8 @@ val get_hits : unit -> int
 val get_miss : unit -> int
 val get_removed : unit -> int
 
-val is_updating : unit -> bool
+val is_active : mode -> bool
+val is_updating : mode -> bool
 
 val cleanup_cache : unit -> unit
 

src/plugins/wp/Changelog

@@ -24,6 +24,9 @@
 Plugin WP <next-release>
 ########################
 
+- Cmd         [2022-07-29] Improves the WP JSON report provided by
+                           -wp-report-json
+
 ##########################
 Plugin WP 25.0 (Manganese)
 ##########################

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 *)
 }
@@ -63,7 +64,8 @@ module PROOFS = WpContext.StaticGenerator(Wpo.S)
         }
     end)
 
-let () = Wpo.on_remove PROOFS.remove
+let () = Wpo.add_removed_hook PROOFS.remove
+let () = Wpo.add_cleared_hook PROOFS.clear
 
 let get wpo =
   try
@@ -122,18 +124,11 @@ let set_saved t s = t.saved <- s
 (* -------------------------------------------------------------------------- *)
 
 let rec walk f node =
-  if not (Wpo.is_proved node.goal) then
+  if not (Wpo.is_valid node.goal) then
     match node.script with
     | Tactic (_,children) -> iter_all (walk f) children
     | Opened | Script _ -> f node
 
-let rec witer f node =
-  let proved = Wpo.is_proved 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 -> ()
@@ -145,36 +140,43 @@ let iteri f tree =
 (* --- Consolidating                                                      --- *)
 (* -------------------------------------------------------------------------- *)
 
-let proved n = Wpo.is_proved n.goal
+let proved n = Wpo.is_valid n.goal
 
 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_proved 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
+    if not (Wpo.is_valid tree.main) then
+      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                                                          --- *)
@@ -185,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
@@ -217,7 +220,7 @@ type status = [
 let status t : status =
   match t.root with
   | None ->
-    if Wpo.is_proved t.main
+    if Wpo.is_valid t.main
     then if Wpo.is_smoke_test t.main then `Invalid else `Proved
     else if Wpo.is_smoke_test t.main then `Passed else `Unproved
   | Some root ->
@@ -319,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 = [| |] ;
 }
@@ -327,6 +331,7 @@ let mk_root_node goal = {
   tree = goal ; goal ;
   parent = None ;
   script = Opened ;
+  stats = Stats.empty ;
   search_index = 0 ;
   search_space = [| |] ;
 }

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,8 +71,7 @@ val node_context : node -> WpContext.t
 val title : node -> string
 val proved : node -> bool
 val pending : node -> int
-(** 0 means proved *)
-
+val stats : node -> Stats.stats
 val parent : node -> node option
 val children : node -> (string * node) list
 val tactical : node -> ProofScript.jtactic option

src/plugins/wp/ProverScript.ml

@@ -141,16 +141,16 @@ 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_proved wpo in
+      let proved = Wpo.is_valid wpo in
       if proved || finalize then
         begin
           env.signaled <- true ;

src/plugins/wp/ProverWhy3.ml

@@ -1247,7 +1247,7 @@ let digest wpo drv prover task =
   let _ = Command.print_file file
       begin fun fmt ->
         Format.fprintf fmt "(* WP Task for Prover %s *)@\n"
-          (Why3Provers.print_why3 prover) ;
+          (Why3Provers.ident_why3 prover) ;
         Why3.Driver.print_task_prepared drv fmt task ;
       end
   in Digest.file file |> Digest.to_hex

src/plugins/wp/Stats.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Performance Reporting                                              --- *)
+(* -------------------------------------------------------------------------- *)
+
+open VCS
+
+type pstats = {
+  tmin : float ;
+  tval : float ;
+  tmax : float ;
+  tnbr : float ;
+  time : float ;
+  success : float ;
+}
+
+type stats = {
+  verdict : VCS.verdict ;
+  provers : (VCS.prover * pstats) list ;
+  tactics : int ;
+  proved : int ;
+  trivial : int ;
+  timeout : int ;
+  unknown : int ;
+  noresult : int ;
+  failed : int ;
+  cached : int ;
+}
+
+(* -------------------------------------------------------------------------- *)
+(* --- Prover Stats                                                       --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Plist = Qed.Listmap.Make
+    (struct
+      type t = VCS.prover
+      let equal a b = a==b || (VCS.cmp_prover a b = 0)
+      let compare = VCS.cmp_prover
+    end)
+
+let pzero = {
+  tmin = max_float ;
+  tval = 0.0 ;
+  tmax = 0.0 ;
+  tnbr = 0.0 ;
+  time = 0.0 ;
+  success = 0.0 ;
+}
+
+let padd a b =
+  if a == pzero then b else
+  if b == pzero then a else
+    {
+      tmin = min a.tmin b.tmin ;
+      tmax = max a.tmax b.tmax ;
+      tval = a.tval +. b.tval ;
+      time = a.time +. b.time ;
+      tnbr = a.tnbr +. b.tnbr ;
+      success = a.success +. b.success ;
+    }
+
+let pmerge = Plist.union (fun _ a b -> padd a b)
+
+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 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
+
+(* -------------------------------------------------------------------------- *)
+(* --- Global Stats                                                       --- *)
+(* -------------------------------------------------------------------------- *)
+
+let empty = {
+  verdict = NoResult;
+  provers = [];
+  tactics = 0;
+  proved = 0;
+  timeout = 0;
+  unknown = 0 ;
+  noresult = 0 ;
+  failed = 0 ;
+  trivial = 0 ;
+  cached = 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,r) -> p, ptime r.prover_time true)
+          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 add a b =
+  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 ;
+      timeout = a.timeout + b.timeout ;
+      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 ;
+    }
+
+let tactical ~qed 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.trivial + 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                                                              --- *)
+(* -------------------------------------------------------------------------- *)
+
+let proofs s = s.proved + s.timeout + s.unknown + s.noresult + s.failed
+let complete s = s.proved = proofs s
+
+let pp_pstats fmt p =
+  if p.tnbr > 0.0 &&
+     p.tmin > Rformat.epsilon &&
+     not (Wp_parameters.has_dkey VCS.dkey_shell)
+  then
+    let mean = p.tval /. p.tnbr in
+    let epsilon = 0.05 *. mean in
+    let delta = p.tmax -. p.tmin in
+    if delta < epsilon then
+      Format.fprintf fmt " (%a)" Rformat.pp_time mean
+    else
+      let middle = (p.tmin +. p.tmax) *. 0.5 in
+      if abs_float (middle -. mean) < epsilon then
+        Format.fprintf fmt " (%a-%a)"
+          Rformat.pp_time p.tmin
+          Rformat.pp_time p.tmax
+      else
+        Format.fprintf fmt " (%a-%a-%a)"
+          Rformat.pp_time p.tmin
+          Rformat.pp_time mean
+          Rformat.pp_time p.tmax
+
+let pp_stats ~shell ~cache fmt s =
+  let total = proofs s in
+  let cacheable = total - s.trivial 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