From 9e97fdd6f27c544aba103d8930a38c9c79a72a17 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 5 Jan 2023 18:11:11 +0100
Subject: [PATCH] [Eva] Compute some statistics
---
src/plugins/eva/engine/compute_functions.ml | 1 +
src/plugins/eva/engine/iterator.ml | 2 ++
src/plugins/eva/engine/mem_exec.ml | 8 +++++++-
src/plugins/eva/partitioning/partitioning_index.ml | 9 +++++++++
src/plugins/eva/partitioning/trace_partitioning.ml | 9 ++++++++-
5 files changed, 27 insertions(+), 2 deletions(-)
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index cfb195799f7..1e79de5680e 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -363,6 +363,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 c05c4a2f10b..2ccf27969ed 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 71a68968d66..a4a530a9741 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/partitioning/partitioning_index.ml b/src/plugins/eva/partitioning/partitioning_index.ml
index 8379820d3bf..422d29c424b 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 ea47c4aa9a2..6e0868ccf24 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;
--
GitLab