From 40b684627df4a8da45924ee9c77fc34b46c93109 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 5 Jan 2023 17:30:19 +0100
Subject: [PATCH] [Eva] Add a module to compute and export stats
---
src/plugins/eva/utils/statistics.ml | 184 +++++++++++++++++++++++++++
src/plugins/eva/utils/statistics.mli | 40 ++++++
2 files changed, 224 insertions(+)
create mode 100644 src/plugins/eva/utils/statistics.ml
create mode 100644 src/plugins/eva/utils/statistics.mli
diff --git a/src/plugins/eva/utils/statistics.ml b/src/plugins/eva/utils/statistics.ml
new file mode 100644
index 00000000000..8c7dad25f98
--- /dev/null
+++ b/src/plugins/eva/utils/statistics.ml
@@ -0,0 +1,184 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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 dictonary, implemented as an hashtable from
+ keys to integers.
+
+ [Key] is the representation of the dictionnary keys: a registered
+ ['a t] statistic accompagnied by the function or the statement the stat is
+ about
+
+ 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
+
+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
+ let Registered stat = Hashtbl.find registry name in
+ match stat.kind, kind with
+ | 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 ->
+ 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.Make_with_collections (
+ 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 = []
+ let equal (Key (s1,x1)) (Key (s2,x2)) =
+ match s1.kind, s2.kind with
+ | Global, Global -> true
+ | Function, Function -> Kernel_function.equal x1 x2
+ | Statement, Statement -> Cil_datatype.Stmt.equal x1 x2
+ | _, _ -> false
+ 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 ->
+ Format.fprintf fmt "%s:%a" s.name Cil_datatype.Stmt.pretty 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)
+
+
+(* -- 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 (k,v) =
+ Format.fprintf fmt "%a\t%d\n" Key.pretty k v
+ in
+ List.iter (pp_stat fmt) l
+
+let export_as_csv ?filename () =
+ let filename = (filename : Filepath.Normalized.t option :> string option) in
+ let filename = Option.value ~default:"stats.json" filename in
+ let out_channel = open_out (filename :> string) in
+ export_as_csv_to_channel out_channel
diff --git a/src/plugins/eva/utils/statistics.mli b/src/plugins/eva/utils/statistics.mli
new file mode 100644
index 00000000000..038a57bb0e9
--- /dev/null
+++ b/src/plugins/eva/utils/statistics.mli
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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
+
+(* Export the computed statistics as CSV *)
+val export_as_csv : ?filename:Filepath.Normalized.t -> unit -> unit
--
GitLab