diff --git a/src/libraries/project/state_builder.ml b/src/libraries/project/state_builder.ml
index cb369ad1045dee8526dbab6490b672807fed3683..c93f9c167b30cdc49e3c100f6542147c4a548e67 100644
--- a/src/libraries/project/state_builder.ml
+++ b/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
diff --git a/src/libraries/project/state_builder.mli b/src/libraries/project/state_builder.mli
index 22ca6683820b4526024778cd2c3fef2a661fdc28..4c331d24135cc26af3d21985e0c28281cfc2a188 100644
--- a/src/libraries/project/state_builder.mli
+++ b/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
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index cfb195799f725002717bd4354080abf90cfa08fd..5e913a57d2c6738e82bcb20c861fa11a0cbc8177 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/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 () =
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index c05c4a2f10b16094f37ca59e57c63161cf4f5389..2ccf27969ed46fad6a08704b096a9ecf824fc026 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/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;
diff --git a/src/plugins/eva/engine/mem_exec.ml b/src/plugins/eva/engine/mem_exec.ml
index 71a68968d66278547885435ca8aae20ffc1e569b..a4a530a9741beeddfabb84ce64c3b793ee629878 100644
--- a/src/plugins/eva/engine/mem_exec.ml
+++ b/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)
diff --git a/src/plugins/eva/parameters.ml b/src/plugins/eva/parameters.ml
index a8a1b273ecc4111d11114502ac711dbd8902ef92..dca2f98df5726fbd57b4aacb43f2e598e21ace42 100644
--- a/src/plugins/eva/parameters.ml
+++ b/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 --- *)
(* ------------------------------------------------------------------------- *)
diff --git a/src/plugins/eva/parameters.mli b/src/plugins/eva/parameters.mli
index 4d8288faaa60f03efafc777f3859fa4e41fea8f5..61daa88642517dc801a2a65b73d7b82e80ce6210 100644
--- a/src/plugins/eva/parameters.mli
+++ b/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
diff --git a/src/plugins/eva/partitioning/partitioning_index.ml b/src/plugins/eva/partitioning/partitioning_index.ml
index 8379820d3bff92866607ee46d8f34b1065d6541d..422d29c424b36cfd050c73f464ae880d6c6cbf62 100644
--- a/src/plugins/eva/partitioning/partitioning_index.ml
+++ b/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
diff --git a/src/plugins/eva/partitioning/trace_partitioning.ml b/src/plugins/eva/partitioning/trace_partitioning.ml
index ea47c4aa9a23114915f126f9062413b27b10fc41..6e0868ccf242c011ba4763e2f0a5649a59eaae2f 100644
--- a/src/plugins/eva/partitioning/trace_partitioning.ml
+++ b/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;
diff --git a/src/plugins/eva/utils/statistics.ml b/src/plugins/eva/utils/statistics.ml
new file mode 100644
index 0000000000000000000000000000000000000000..508a68db4ad07966275613466a6fd24c6ce5b10a
--- /dev/null
+++ b/src/plugins/eva/utils/statistics.ml
@@ -0,0 +1,212 @@
+(**************************************************************************)
+(* *)
+(* 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
diff --git a/src/plugins/eva/utils/statistics.mli b/src/plugins/eva/utils/statistics.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ca402e73218f526d265cf2b19a624bc27910b93a
--- /dev/null
+++ b/src/plugins/eva/utils/statistics.mli
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(* *)
+(* 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
diff --git a/tests/value/oracle/statistics.csv b/tests/value/oracle/statistics.csv
new file mode 100644
index 0000000000000000000000000000000000000000..f844aeb8ca15700b2e9b58fd5303876925a37bae
--- /dev/null
+++ b/tests/value/oracle/statistics.csv
@@ -0,0 +1,7 @@
+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
diff --git a/tests/value/oracle/statistics.res.oracle b/tests/value/oracle/statistics.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9d6258ee598876f6071ef856f29e7393a2de4ab0
--- /dev/null
+++ b/tests/value/oracle/statistics.res.oracle
@@ -0,0 +1,76 @@
+[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
diff --git a/tests/value/oracle_apron/statistics.res.oracle b/tests/value/oracle_apron/statistics.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9a97de5637c3ca83fe4c2b5547eb7e2616f9bf94
--- /dev/null
+++ b/tests/value/oracle_apron/statistics.res.oracle
@@ -0,0 +1,17 @@
+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
diff --git a/tests/value/statistics.i b/tests/value/statistics.i
new file mode 100644
index 0000000000000000000000000000000000000000..329dbef213c9393b226943744f7d24d1694273d6
--- /dev/null
+++ b/tests/value/statistics.i
@@ -0,0 +1,20 @@
+/* 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);
+}