Merge branch 'feature/eva/analysis-stats' into 'master'

[Eva] Analysis stats

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

src/libraries/project/state_builder.ml

@@ -490,9 +490,11 @@ module type Hashtbl = sig
     ?cmp:(key -> key -> int) -> (key -> data -> 'a -> 'a) -> 'a -> 'a
   val memo: ?change:(data -> data) -> (key -> data) -> key -> data
   val find: key -> data
+  val find_opt: key -> data option
   val find_all: key -> data list
   val mem: key -> bool
   val remove: key -> unit
+  val to_seq: unit -> (key * data) Seq.t
 end
 
 module Hashtbl
@@ -548,6 +550,7 @@ struct
   let replace key v = H.replace !state key v
   let add key v = H.add !state key v
   let find key = H.find !state key
+  let find_opt key = H.find_opt !state key
   let find_all key = H.find_all !state key
   let mem key = H.mem !state key
   let remove key = H.remove !state key
@@ -555,6 +558,7 @@ struct
   let iter_sorted ?cmp f = H.iter_sorted ?cmp f !state
   let fold f acc = H.fold f !state acc
   let fold_sorted ?cmp f acc = H.fold_sorted ?cmp f !state acc
+  let to_seq () = H.to_seq !state
 
   let memo ?change f key =
     try

src/libraries/project/state_builder.mli

@@ -351,11 +351,20 @@ module type Hashtbl = sig
   (** Return the current binding of the given key.
       @raise Not_found if the key is not in the table. *)
 
+  val find_opt: key -> data option
+  (** Return the current binding of the given key, or None if no such binding
+      exists.
+      @since Frama-C+dev *)
+
   val find_all: key -> data list
   (** Return the list of all data associated with the given key. *)
 
   val mem: key -> bool
   val remove: key -> unit
+
+  val to_seq: unit -> (key * data) Seq.t
+  (** Iterate on the whole table.
+      @since Frama-C+dev *)
 end
 
 (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide

src/plugins/eva/engine/compute_functions.ml

@@ -85,6 +85,7 @@ let pre_analysis () =
   Widen.precompute_widen_hints ();
   Builtins.prepare_builtins ();
   Eva_perf.reset ();
+  Statistics.reset_all ();
   (* We may be resuming Value from a previously crashed analysis. Clear
      degeneration states *)
   Eva_utils.DegenerationPoints.clear ();
@@ -363,6 +364,7 @@ module Make (Abstract: Abstractions.Eva) = struct
       post_analysis ();
       Abstract.Dom.post_analysis final_state;
       Summary.print_summary ();
+      Statistics.export_as_csv ();
       restore_signals ()
     in
     let cleanup () =

src/plugins/eva/engine/iterator.ml

@@ -36,6 +36,7 @@ let check_signals, signal_abort =
 
 let dkey = Self.dkey_iterator
 let dkey_callbacks = Self.dkey_callbacks
+let stat_iterations = Statistics.register_statement_stat "iterations"
 
 let blocks_share_locals b1 b2 =
   match b1.blocals, b2.blocals with
@@ -562,6 +563,7 @@ module Make_Dataflow
         not (process_vertex ~widening:true v) || !iteration_count = 0
       do
         Self.debug ~dkey "iteration %d" !iteration_count;
+        Option.iter (Statistics.incr stat_iterations) v.vertex_start_of;
         iterate_list w;
         incr iteration_count;
       done;

src/plugins/eva/engine/mem_exec.ml

@@ -20,6 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+let stat_hits = Statistics.register_function_stat "memexec-hits"
+let stat_misses = Statistics.register_function_stat "memexec-misses"
 
 module SaveCounter =
   State_builder.SharedCounter(struct let name = "Mem_exec.save_counter" end)
@@ -263,10 +265,14 @@ module Make
       let args = List.map (function `Bottom -> None | `Value v -> Some v) args in
       let previous = ActualArgs.Map.find args previous_kf in
       find_match_in_previous kf previous state;
+      Statistics.incr stat_misses kf;
       None
     with
-    | Not_found -> None
+    | Not_found ->
+      Statistics.incr stat_misses kf;
+      None
     | Result_found (outputs, i) ->
+      Statistics.incr stat_hits kf;
       let call_result = outputs in
       Some (call_result, i)
 

src/plugins/eva/parameters.ml

@@ -1091,6 +1091,18 @@ module NumerorsLogFile =
                   function in the given file"
     end)
 
+let () = Parameter_customize.set_group messages
+module StatisticsFile =
+  Filepath
+    (struct
+      let option_name = "-eva-statistics-file"
+      let arg_name = "file.csv"
+      let file_kind = "CSV"
+      let existence = Fc_Filepath.Indifferent
+      let help = "Dump some internal statistics about the analysis"
+    end)
+
+
 (* ------------------------------------------------------------------------- *)
 (* --- Interpreter mode                                                  --- *)
 (* ------------------------------------------------------------------------- *)

src/plugins/eva/parameters.mli

@@ -125,6 +125,7 @@ module ShowSlevel: Parameter_sig.Int
 module PrintCallstacks: Parameter_sig.Bool
 module ReportRedStatuses: Parameter_sig.Filepath
 module NumerorsLogFile: Parameter_sig.Filepath
+module StatisticsFile: Parameter_sig.Filepath
 
 module MemExecAll: Parameter_sig.Bool
 

src/plugins/eva/partitioning/partitioning_index.ml

@@ -20,6 +20,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+let stat_hits = Statistics.register_global_stat "partitioning-index-hits"
+let stat_misses = Statistics.register_global_stat "partitioning-index-misses"
+
+
 (** Partition of the abstract states, computed for each node by the
     dataflow analysis. *)
 module Make (Domain : Abstract.Domain.External)
@@ -86,6 +90,11 @@ module Make (Domain : Abstract.Domain.External)
         then false
         else (Index.add states prefix state; true)
 
+  let add state partition =
+    let r = add state partition in
+    Statistics.incr (if r then stat_misses else stat_hits) ();
+    r
+
   let iter f { states; others } =
     Index.iter (fun _k v -> f v) states;
     List.iter f others

src/plugins/eva/partitioning/trace_partitioning.ml

@@ -23,6 +23,8 @@
 open Cil_types
 open Partition
 
+let stat_max_widenings = Statistics.register_statement_stat "max-widenings"
+
 module Make
     (Abstract: Abstractions.Eva)
     (Kf : sig val kf: kernel_function end) =
@@ -59,6 +61,7 @@ struct
     mutable widened_state : state option;
     mutable previous_state : state;
     mutable widening_counter : int;
+    mutable widening_steps : int; (* count the number of successive widenings *)
   }
 
   type widening = {
@@ -336,6 +339,8 @@ struct
           w.previous_state <- next;
           w.widened_state <- Some next;
           w.widening_counter <- widening_period - 1;
+          w.widening_steps <- w.widening_steps + 1;
+          Statistics.grow stat_max_widenings stmt w.widening_steps;
           Some next
         end
       with Not_found ->
@@ -345,7 +350,9 @@ struct
           let ws =
             { widened_state = None;
               previous_state = curr;
-              widening_counter = widening_delay - 1; }
+              widening_counter = widening_delay - 1;
+              widening_steps = 0
+            }
           in
           w.widening_partition <- Partition.replace key ws w.widening_partition
         end;

src/plugins/eva/utils/statistics.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2023                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* Statistics are stored in a dictionary, implemented as an hashtable from
+   keys to integers.
+
+   [Key] is the representation of the dictionary keys: a couple of a registered
+   statistic (type ['a t]) accompanied by the function or the statement the stat
+   is about (type ['a]).
+
+   Statistics must be registered before usage. The registry keeps track of the
+   registered statistics and allow the reloading of projects by matching the
+   previous stats to the current ones.
+*)
+
+(* --- Type --- *)
+
+type _ kind =
+  | Global : unit kind
+  | Function : Cil_types.kernel_function kind
+  | Statement : Cil_types.stmt kind
+
+type 'a t = {
+  id: int;
+  name: string;
+  kind: 'a kind;
+}
+
+
+(* --- Registry --- *)
+
+type registered_stat = Registered : 'a t -> registered_stat [@@unboxed]
+
+let kind_to_string : type a. a kind -> string = function
+  | Global -> "global"
+  | Function  -> "function"
+  | Statement -> "statement"
+
+let registry = Hashtbl.create 13
+let last_id = ref 0
+
+let register (type a) (name : string) (kind : a kind) : a t =
+  try
+    (* If the stat is already registered, return the previous one *)
+    let Registered stat = Hashtbl.find registry name in
+    match stat.kind, kind with (* equality must be ensured to return the right type of stat *)
+    | Global, Global -> stat
+    | Function, Function -> stat
+    | Statement, Statement -> stat
+    | _ ->
+      Self.fatal
+        "%s statistic \"%s\" was already registered with as a %s statistic"
+        name (kind_to_string kind) (kind_to_string stat.kind)
+  with Not_found ->
+    (* Otherwise, create a new record for the stat *)
+    incr last_id;
+    let stat = { id = !last_id; name; kind } in
+    Hashtbl.add registry name (Registered stat);
+    stat
+
+let register_global_stat name =
+  register name Global
+
+let register_function_stat name =
+  register name Function
+
+let register_statement_stat name =
+  register name Statement
+
+
+(* --- Keys --- *)
+
+type key = Key : 'a t * 'a -> key
+
+module Key_Datatype = struct
+  include Datatype.Serializable_undefined
+
+  type t = key
+  let name = "Statistics.Key"
+  let rehash (Key (s, x)) =
+    (Key (register s.name s.kind, x))
+  let reprs = [Key ({ id = 0; name="dummy"; kind=Global }, ())]
+  let equal = Datatype.from_compare
+  let compare (Key (s1,x1)) (Key (s2,x2)) =
+    let c = s1.id - s2.id in
+    if c <> 0 then c else
+      match s1.kind, s2.kind with
+      | Global, Global -> 0
+      | Function, Function -> Kernel_function.compare x1 x2
+      | Statement, Statement -> Cil_datatype.Stmt.compare x1 x2
+      | Global, (Function | Statement) -> -1
+      | (Function | Statement), Global -> 1
+      | Function, Statement -> -1
+      | Statement, Function -> 1
+  let hash (Key (s,x)) =
+    let h = match s.kind with
+      | Global -> 0
+      | Function -> Kernel_function.hash x
+      | Statement -> Cil_datatype.Stmt.hash x
+    in
+    Hashtbl.hash (s.id, h)
+  let copy k = k
+  let pretty fmt (Key (s,x)) =
+    match s.kind with
+    | Global ->
+      Format.fprintf fmt "%s" s.name
+    | Function ->
+      Format.fprintf fmt "%s:%a" s.name Kernel_function.pretty x
+    | Statement ->
+      let loc = Cil_datatype.Stmt.loc x in
+      Format.fprintf fmt "%s:%a" s.name Cil_datatype.Location.pretty loc
+end
+
+module Key = struct
+  include Datatype.Make_with_collections (Key_Datatype)
+
+  let name (Key (s, _x)) = s.name
+
+  let pretty_kf fmt (Key (s, x)) =
+    match s.kind with
+    | Global -> ()
+    | Function -> Kernel_function.pretty fmt x
+    | Statement -> Kernel_function.(pretty fmt (find_englobing_kf x))
+
+  let pretty_stmt fmt (Key (s, x)) =
+    match s.kind with
+    | Global | Function -> ()
+    | Statement -> Cil_datatype.Location.pretty fmt (Cil_datatype.Stmt.loc x)
+end
+
+(* --- Projectified state --- *)
+
+module State =
+  State_builder.Hashtbl
+    (Key.Hashtbl)
+    (Datatype.Int)
+    (struct
+      let name = "Eva.Statistics.State"
+      let dependencies = [ Self.state ]
+      let size = 17
+    end)
+
+
+(* --- Statistics update --- *)
+
+let set (type a) (stat : a t) (x : a) value =
+  let k = Key (stat,x) in
+  State.replace k value
+
+let update (type a) (stat : a t) (x : a) (f : int -> int) =
+  let k = Key (stat,x) in
+  State.replace k (f (State.find_opt k |> Option.value ~default:0))
+
+let incr (type a) (stat : a t) (x : a) =
+  update stat x (fun v -> v + 1)
+
+let grow (type a) (stat : a t) (x : a) value =
+  update stat x (fun v -> max v value)
+
+let reset_all () =
+  State.clear ()
+
+
+(* -- Export --- *)
+
+let export_as_list () =
+  State.to_seq () |> List.of_seq |>
+  List.sort (fun (k1,_v1) (k2,_v2) -> Key.compare k1 k2)
+
+let export_as_csv_to_channel out_channel =
+  let fmt = Format.formatter_of_out_channel out_channel in
+  let l = export_as_list () in
+  let pp_stat fmt (key, value) =
+    Format.fprintf fmt "%s\t%a\t%a\t%d\n"
+      (Key.name key)
+      Key.pretty_kf key
+      Key.pretty_stmt key
+      value
+  in
+  List.iter (pp_stat fmt) l
+
+let export_as_csv_to_file filename =
+  let out_channel = open_out (filename : Filepath.Normalized.t :> string) in
+  export_as_csv_to_channel out_channel
+
+let export_as_csv ?filename () =
+  match filename with
+  | None ->
+    if not (Parameters.StatisticsFile.is_empty ()) then
+      let filename = Parameters.StatisticsFile.get () in
+      export_as_csv_to_file filename
+  | Some filename ->
+    export_as_csv_to_file filename

src/plugins/eva/utils/statistics.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2023                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+type 'a t
+
+(* Register a statistic class *)
+val register_global_stat : string -> unit t
+val register_function_stat : string -> Cil_types.kernel_function t
+val register_statement_stat : string -> Cil_types.stmt t
+
+(* Set the stat to the given value *)
+val set : 'a t -> 'a -> int -> unit
+
+(* Adds 1 to the stat or set it to 1 if undefined *)
+val incr : 'a t -> 'a -> unit
+
+(* Set the stat to the maximum between the current value and the given value *)
+val grow : 'a t -> 'a -> int -> unit
+
+(* Reset all statistics to zero *)
+val reset_all: unit -> unit
+
+(* Export the computed statistics as CSV *)
+val export_as_csv : ?filename:Filepath.Normalized.t -> unit -> unit

tests/value/oracle/statistics.csv

+memexec-hits	g		3
+memexec-misses	g		5
+memexec-misses	f		2
+memexec-misses	main		1
+partitioning-index-misses			57
+max-widenings	f	statistics.i:12	1
+iterations	f	statistics.i:12	8

tests/value/oracle/statistics.res.oracle

+[kernel] Parsing statistics.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva] computing for function f <- main.
+  Called from statistics.i:18.
+[eva] computing for function g <- f <- main.
+  Called from statistics.i:13.
+[eva] Recording results for g
+[eva] Done for function g
+[eva] statistics.i:12: starting to merge loop iterations
+[eva] computing for function g <- f <- main.
+  Called from statistics.i:13.
+[eva] Recording results for g
+[eva] Done for function g
+[eva] computing for function g <- f <- main.
+  Called from statistics.i:13.
+[eva] Recording results for g
+[eva] Done for function g
+[eva] computing for function g <- f <- main.
+  Called from statistics.i:13.
+[eva] Recording results for g
+[eva] Done for function g
+[eva] Recording results for f
+[eva] Done for function f
+[eva:alarm] statistics.i:19: Warning: 
+  signed overflow. assert -2147483648 ≤ n - 1;
+[eva] computing for function f <- main.
+  Called from statistics.i:19.
+[eva] statistics.i:13: Reusing old results for call to g
+[eva] statistics.i:13: Reusing old results for call to g
+[eva] statistics.i:13: Reusing old results for call to g
+[eva] computing for function g <- f <- main.
+  Called from statistics.i:13.
+[eva] Recording results for g
+[eva] Done for function g
+[eva] Recording results for f
+[eva] Done for function f
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function g:
+  
+[eva:final-states] Values at end of function f:
+  i ∈ [0..2147483647]
+[eva:final-states] Values at end of function main:
+  __retres ∈ {0}
+[from] Computing for function g
+[from] Done for function g
+[from] Computing for function f
+[from] Done for function f
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function g:
+  NO EFFECTS
+[from] Function f:
+  NO EFFECTS
+[from] Function main:
+  \result FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function g:
+    \nothing
+[inout] Inputs for function g:
+    \nothing
+[inout] Out (internal) for function f:
+    i
+[inout] Inputs for function f:
+    \nothing
+[inout] Out (internal) for function main:
+    __retres
+[inout] Inputs for function main:
+    \nothing

tests/value/oracle_apron/statistics.res.oracle

+32,34c32,43
+< [eva] statistics.i:13: Reusing old results for call to g
+< [eva] statistics.i:13: Reusing old results for call to g
+< [eva] statistics.i:13: Reusing old results for call to g
+---
+> [eva] computing for function g <- f <- main.
+>   Called from statistics.i:13.
+> [eva] Recording results for g
+> [eva] Done for function g
+> [eva] computing for function g <- f <- main.
+>   Called from statistics.i:13.
+> [eva] Recording results for g
+> [eva] Done for function g
+> [eva] computing for function g <- f <- main.
+>   Called from statistics.i:13.
+> [eva] Recording results for g
+> [eva] Done for function g

tests/value/statistics.i

+/* run.config
+   LOG: @PTEST_NAME@.csv
+   STDOPT: +" -eva-statistics-file ./@PTEST_NAME@.csv"
+*/
+
+/* This test only dump statistics in the default configuration
+   to avoid oracle duplication. */
+
+void g(int i) {}
+
+void f(int n) {
+  for (int i = 0 ; i < n ; i++) {
+    g(i);
+  }
+}
+
+int main(int n) {
+  f(n);
+  f(n-1);
+}