From d28e64dcb4eaa557287989d2363e7dc03f0c0d2f Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 21 Apr 2023 20:13:07 +0200
Subject: [PATCH] [Eva] server api: use the new state building when possible
---
src/plugins/eva/api/general_requests.ml | 17 +++++++----------
src/plugins/eva/engine/analysis.ml | 12 +++++++++---
src/plugins/eva/engine/compute_functions.ml | 6 +++---
src/plugins/eva/self.ml | 16 ----------------
src/plugins/eva/self.mli | 13 ++-----------
src/plugins/eva/utils/eva_results.ml | 2 +-
src/plugins/eva/utils/summary.ml | 11 +----------
src/plugins/eva/utils/summary.mli | 12 ++++++++----
8 files changed, 31 insertions(+), 58 deletions(-)
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index d3085ad822c..f4de3ff5552 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -31,7 +31,7 @@ let package =
()
module ComputationState = struct
- type t = Analysis.computation_state
+ type t = Self.computation_state
let jtype =
Data.declare ~package
~name:"computationStateType"
@@ -42,20 +42,18 @@ module ComputationState = struct
Jtag "computed" ;
Jtag "aborted" ])
let to_json = function
- | Analysis.NotComputed -> `String "not_computed"
+ | Self.NotComputed -> `String "not_computed"
| Computing -> `String "computing"
| Computed -> `String "computed"
| Aborted -> `String "aborted"
end
let computation_signal =
- States.register_value ~package
+ States.register_framac_value ~package
~name:"computationState"
~descr:(Markdown.plain "The current computation state of the analysis.")
~output:(module ComputationState)
- ~get:Analysis.current_computation_state
- ~add_hook:Analysis.register_computation_hook
- ()
+ (module Self.ComputationState)
(* ----- Callsites ---------------------------------------------------------- *)
@@ -747,16 +745,15 @@ let _array =
~data:(module Statuses)
~get:(fun (_kf,stats) -> stats.fun_alarm_statuses);
- States.register_array
+ States.register_framac_array
~package
~name:"functionStats"
~descr:(Markdown.plain
"Statistics about the last Eva analysis for each function")
- ~key:(fun (fundec,_stats) -> fundec.svar.vname)
+ ~key:(fun fundec -> fundec.svar.vname)
~keyType:Kernel_ast.Fundec.jtype
- ~iter:(fun f -> FunctionStats.iter (fun fundec s -> f (fundec,s)))
- ~add_update_hook:FunctionStats.register_hook
model
+ (module FunctionStats)
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index ddc557787c5..a93c6903e27 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -25,8 +25,14 @@ open Eval
type computation_state = Self.computation_state =
| NotComputed | Computing | Computed | Aborted
-let current_computation_state = Self.current_computation_state
-let register_computation_hook = Self.register_computation_hook
+let current_computation_state = Self.ComputationState.get
+let register_computation_hook ?on f =
+ let f' = match on with
+ | None -> f
+ | Some s -> fun s' -> if s = s' then f s
+ in
+ Self.ComputationState.add_hook_on_change f'
+
let is_computed = Self.is_computed
let self = Self.state
let emitter = Eva_utils.emitter
@@ -210,7 +216,7 @@ let force_compute () =
let kf, lib_entry = Globals.entry_point () in
reset_analyzer ();
(* The new analyzer can be accesed through hooks *)
- Self.set_computation_state Computing;
+ Self.ComputationState.set Computing;
let module Analyzer = (val snd !ref_analyzer) in
Analyzer.compute_from_entry_point ~lib_entry kf
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 58c9b2173fc..fcc29b34251 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -361,7 +361,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
Eva_utils.clear_call_stack ();
Self.feedback "done for function %a" Kernel_function.pretty kf;
Abstract.Dom.Store.mark_as_computed ();
- Self.(set_computation_state Computed);
+ Self.(ComputationState.set Computed);
post_analysis ();
Abstract.Dom.post_analysis final_state;
Summary.print_summary ();
@@ -370,7 +370,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
in
let cleanup () =
Abstract.Dom.Store.mark_as_computed ();
- Self.(set_computation_state Aborted);
+ Self.(ComputationState.set Aborted);
post_analysis_cleanup ~aborted:true
in
Eva_utils.protect compute ~cleanup
@@ -388,7 +388,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
match initial_state with
| `Bottom ->
Abstract.Dom.Store.mark_as_computed ();
- Self.(set_computation_state Aborted);
+ Self.(ComputationState.set Aborted);
Self.result "Eva not started because globals \
initialization is not computable.";
Eval_annots.mark_invalid_initializers ()
diff --git a/src/plugins/eva/self.ml b/src/plugins/eva/self.ml
index eeceead1daa..072213e1a68 100644
--- a/src/plugins/eva/self.ml
+++ b/src/plugins/eva/self.ml
@@ -69,11 +69,7 @@ struct
end
module Datatype' = Datatype.Make (Prototype)
- module Hook = Hook.Build (Prototype)
include (State_builder.Ref (Datatype') (Prototype))
-
- let set s = set s; Hook.apply s
- let () = add_hook_on_update (fun r -> Hook.apply !r)
end
let is_computed () =
@@ -81,18 +77,6 @@ let is_computed () =
| Computed | Aborted -> true
| NotComputed | Computing -> false
-let current_computation_state = ComputationState.get
-let set_computation_state = ComputationState.set
-
-(* Register a hook on current computation state *)
-let register_computation_hook ?on f =
- let f' = match on with
- | None -> f
- | Some s -> fun s' -> if s = s' then f s
- in
- ComputationState.Hook.extend f'
-
-
(* Debug categories. *)
let dkey_initial_state = register_category "initial-state"
let dkey_final_states = register_category "final-states"
diff --git a/src/plugins/eva/self.mli b/src/plugins/eva/self.mli
index fef6d68746d..3171cb73572 100644
--- a/src/plugins/eva/self.mli
+++ b/src/plugins/eva/self.mli
@@ -31,18 +31,9 @@ val is_computed: unit -> bool
(** Computation state of the analysis. *)
type computation_state = NotComputed | Computing | Computed | Aborted
-(** Get the current computation state of the analysis, updated by
+(** The current computation state of the analysis, updated by
[force_compute] and states updates. *)
-val current_computation_state : unit -> computation_state
-
-(** Set the current computation state. *)
-val set_computation_state: computation_state -> unit
-
-(** Registers a hook that will be called each time the analysis starts or
- finishes. If [on] is given, the hook will only be called when the
- analysis switches to this specific state. *)
-val register_computation_hook: ?on:computation_state ->
- (computation_state -> unit) -> unit
+module ComputationState : State_builder.Ref with type data = computation_state
(** Debug categories responsible for printing initial and final states of Value.
Enabled by default, but can be disabled via the command-line:
diff --git a/src/plugins/eva/utils/eva_results.ml b/src/plugins/eva/utils/eva_results.ml
index 7b7d2b98ddf..6d905282146 100644
--- a/src/plugins/eva/utils/eva_results.ml
+++ b/src/plugins/eva/utils/eva_results.ml
@@ -171,7 +171,7 @@ let set_results results =
let b = Parameters.ResultsAll.get () in
Cvalue_domain.State.Store.register_global_state b
(`Value Cvalue_domain.State.top);
- Self.set_computation_state Computed;
+ Self.ComputationState.set Computed;
Db.Value.mark_as_computed ();
;;
diff --git a/src/plugins/eva/utils/summary.ml b/src/plugins/eva/utils/summary.ml
index 6b2dd8e93b0..5462206ea9e 100644
--- a/src/plugins/eva/utils/summary.ml
+++ b/src/plugins/eva/utils/summary.ml
@@ -211,19 +211,10 @@ module FunctionStats = struct
let size = 17
end)
- module Hook = Hook.Build (struct
- type t = Cil_types.fundec * fun_stats
- end)
-
- let compute kf =
- let stats = compute_fun_stats kf in
- Hook.apply (kf,stats);
- stats
let get kf =
try Some (find kf)
with Not_found -> None
- let recompute kf = replace kf (compute kf)
- let register_hook = Hook.extend
+ let recompute kf = replace kf (compute_fun_stats kf)
end
diff --git a/src/plugins/eva/utils/summary.mli b/src/plugins/eva/utils/summary.mli
index c9bd45a364d..eea1b0df3d3 100644
--- a/src/plugins/eva/utils/summary.mli
+++ b/src/plugins/eva/utils/summary.mli
@@ -65,17 +65,21 @@ type program_stats =
preconds_statuses: statuses; }
module FunctionStats : sig
+ type key = Cil_types.fundec
+ type data = fun_stats
+
(** Get the current analysis statistics for a function *)
- val get: Cil_types.fundec -> fun_stats option
+ val get: key -> data option
(** Iterate on every function statistics *)
- val iter: (Cil_types.fundec -> fun_stats -> unit) -> unit
+ val iter: (key -> data -> unit) -> unit
(** Trigger the recomputation of function stats *)
- val recompute: Cil_types.fundec -> unit
+ val recompute: key -> unit
(** Set a hook on function statistics computation *)
- val register_hook: (Cil_types.fundec * fun_stats -> unit) -> unit
+ val add_hook_on_change:
+ ((key, data) State_builder.hashtbl_event -> unit) -> unit
end
(** Compute analysis statistics. *)
--
GitLab