From f073186af51fc52993a0d9f059f3189a8a81672c Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 22 Sep 2021 15:13:44 +0200
Subject: [PATCH] [Eva] export computation state through server API
---
.../generated/plugins/eva/general/index.ts | 50 ++++++++++++++++--
ivette/src/frama-c/kernel/Globals.tsx | 4 +-
ivette/src/frama-c/plugins/eva/Summary.tsx | 46 +++++++++++------
ivette/src/frama-c/plugins/eva/summary.css | 9 ++++
src/plugins/value/api/general_requests.ml | 47 ++++++++++++-----
src/plugins/value/api/values_request.ml | 3 +-
src/plugins/value/engine/analysis.ml | 51 ++++++++++++++++---
src/plugins/value/engine/analysis.mli | 15 ++++--
8 files changed, 177 insertions(+), 48 deletions(-)
diff --git a/ivette/src/frama-c/api/generated/plugins/eva/general/index.ts b/ivette/src/frama-c/api/generated/plugins/eva/general/index.ts
index 05370709479..86688a25b9d 100644
--- a/ivette/src/frama-c/api/generated/plugins/eva/general/index.ts
+++ b/ivette/src/frama-c/api/generated/plugins/eva/general/index.ts
@@ -54,15 +54,53 @@ import { jTagSafe } from 'frama-c/api/kernel/data';
//@ts-ignore
import { tag } from 'frama-c/api/kernel/data';
-const isComputed_internal: Server.GetRequest<null,boolean> = {
+/** State of the computation of Eva Analysis. */
+export type computationStateType = "not_computed" | "computing" | "computed";
+
+/** Loose decoder for `computationStateType` */
+export const jComputationStateType: Json.Loose<computationStateType> =
+ Json.jUnion<"not_computed" | "computing" | "computed">(
+ Json.jTag("not_computed"),
+ Json.jTag("computing"),
+ Json.jTag("computed"),
+ );
+
+/** Safe decoder for `computationStateType` */
+export const jComputationStateTypeSafe: Json.Safe<computationStateType> =
+ Json.jFail(jComputationStateType,'ComputationStateType expected');
+
+/** Natural order for `computationStateType` */
+export const byComputationStateType: Compare.Order<computationStateType> =
+ Compare.structural;
+
+/** Signal for state [`computationState`](#computationstate) */
+export const signalComputationState: Server.Signal = {
+ name: 'plugins.eva.general.signalComputationState',
+};
+
+const getComputationState_internal: Server.GetRequest<
+ null,
+ computationStateType
+ > = {
kind: Server.RqKind.GET,
- name: 'plugins.eva.general.isComputed',
+ name: 'plugins.eva.general.getComputationState',
input: Json.jNull,
- output: Json.jBoolean,
+ output: jComputationStateType,
signals: [],
};
-/** True if the Eva analysis has been done */
-export const isComputed: Server.GetRequest<null,boolean>= isComputed_internal;
+/** Getter for state [`computationState`](#computationstate) */
+export const getComputationState: Server.GetRequest<
+ null,
+ computationStateType
+ >= getComputationState_internal;
+
+const computationState_internal: State.Value<computationStateType> = {
+ name: 'plugins.eva.general.computationState',
+ signal: signalComputationState,
+ getter: getComputationState,
+};
+/** The current computation state of the analysis. */
+export const computationState: State.Value<computationStateType> = computationState_internal;
const getCallers_internal: Server.GetRequest<
Json.key<'#fct'>,
@@ -286,6 +324,7 @@ const alarmCategoryTags_internal: Server.GetRequest<null,tag[]> = {
name: 'plugins.eva.general.alarmCategoryTags',
input: Json.jNull,
output: Json.jList(jTag),
+ signals: [],
};
/** Registered tags for the above type. */
export const alarmCategoryTags: Server.GetRequest<null,tag[]>= alarmCategoryTags_internal;
@@ -435,6 +474,7 @@ const getStats_internal: Server.GetRequest<null,statistics> = {
name: 'plugins.eva.general.getStats',
input: Json.jNull,
output: jStatistics,
+ signals: [],
};
/** Getter for state [`stats`](#stats) */
export const getStats: Server.GetRequest<null,statistics>= getStats_internal;
diff --git a/ivette/src/frama-c/kernel/Globals.tsx b/ivette/src/frama-c/kernel/Globals.tsx
index 7705b8ee816..6c94aedd859 100644
--- a/ivette/src/frama-c/kernel/Globals.tsx
+++ b/ivette/src/frama-c/kernel/Globals.tsx
@@ -33,7 +33,7 @@ import * as Ivette from 'ivette';
import * as States from 'frama-c/states';
import { functions, functionsData } from 'frama-c/api/kernel/ast';
-import { isComputed } from 'frama-c/api/plugins/eva/general';
+import { computationState } from 'frama-c/api/plugins/eva/general';
// --------------------------------------------------------------------------
// --- Global Search Hints
@@ -115,7 +115,7 @@ export default () => {
useFlipSettings('ivette.globals.evaonly', false);
const multipleSelection = selection?.multiple;
const multipleSelectionActive = multipleSelection?.allSelections.length > 0;
- const evaComputed = States.useRequest(isComputed, null);
+ const evaComputed = States.useSyncValue(computationState) === 'computed';
function isSelected(fct: functionsData) {
return multipleSelection?.allSelections.some(
diff --git a/ivette/src/frama-c/plugins/eva/Summary.tsx b/ivette/src/frama-c/plugins/eva/Summary.tsx
index 9aea5f55144..f9beeefda29 100644
--- a/ivette/src/frama-c/plugins/eva/Summary.tsx
+++ b/ivette/src/frama-c/plugins/eva/Summary.tsx
@@ -27,6 +27,8 @@ import { Vfill } from 'dome/layout/boxes';
import * as States from 'frama-c/states';
import * as Eva from 'frama-c/api/plugins/eva/general';
+import { LED } from 'dome/controls/buttons';
+
import './summary.css';
function percent(reachable: number, total: number): string {
@@ -200,22 +202,36 @@ function Statuses(data: Eva.statistics): JSX.Element {
export function EvaSummary(): JSX.Element {
const alarmCategories = States.useTags(Eva.alarmCategoryTags);
const data = States.useSyncValue(Eva.stats);
+ const state = States.useSyncValue(Eva.computationState);
- return (data && alarmCategories ? (
- <div className="eva-summary">
- <h1>Analysis Summary</h1>
- <h2>Coverage</h2>
- {CoverageTable(data)}
- <h2>Errors</h2>
- {Errors(data)}
- <h2>Alarms</h2>
- {Alarms(data, alarmCategories)}
- <h2>Statuses</h2>
- {Statuses(data)}
- </div>
- ) :
- <></>
- );
+ if (state === 'not_computed')
+ return (
+ <div className="eva-summary-status">
+ Eva analysis not run yet.
+ </div>);
+
+ if (state === 'computing')
+ return (
+ <div className="eva-summary-status">
+ Eva analysis running.
+ <LED status="active" blink />
+ </div>);
+
+ if (state === 'computed' && data && alarmCategories)
+ return (
+ <div className="eva-summary computed">
+ <h1>Analysis Summary</h1>
+ <h2>Coverage</h2>
+ {CoverageTable(data)}
+ <h2>Errors</h2>
+ {Errors(data)}
+ <h2>Alarms</h2>
+ {Alarms(data, alarmCategories)}
+ <h2>Statuses</h2>
+ {Statuses(data)}
+ </div>);
+
+ return (<></>);
}
function EvaSummaryComponent(): JSX.Element {
diff --git a/ivette/src/frama-c/plugins/eva/summary.css b/ivette/src/frama-c/plugins/eva/summary.css
index 82aca9ded08..1b67fd4d29d 100644
--- a/ivette/src/frama-c/plugins/eva/summary.css
+++ b/ivette/src/frama-c/plugins/eva/summary.css
@@ -1,3 +1,12 @@
+.eva-summary-status {
+ margin: 6px;
+}
+
+.eva-summary-status .dome-xButton-led {
+ display: inline-block;
+ vertical-align: baseline;
+}
+
.eva-summary {
padding: 10px;
background-color: white;
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 78a7ba5c09f..789a5b7494a 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -31,11 +31,31 @@ let package =
~readme:"eva.md"
()
-let () = Request.register ~package
- ~kind:`GET ~name:"isComputed"
- ~descr:(Markdown.plain "True if the Eva analysis has been done")
- ~input:(module Data.Junit) ~output:(module Data.Jbool)
- Db.Value.is_computed
+module ComputationState = struct
+ open Analysis
+ type t = computation_state
+ let jtype =
+ Data.declare ~package
+ ~name:"computationStateType"
+ ~descr:(Markdown.plain "State of the computation of Eva Analysis.")
+ Package.(Junion [
+ Jtag "not_computed" ;
+ Jtag "computing" ;
+ Jtag "computed"])
+ let to_json = function
+ | Analysis.NotComputed -> `String "not_computed"
+ | Computing -> `String "computing"
+ | Computed -> `String "computed"
+end
+
+let _computation_signal =
+ States.register_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
+ ()
let is_computed kf =
Db.Value.is_computed () &&
@@ -380,15 +400,14 @@ module Statistics = struct
"count", `Int c ]) (AlarmsStats.bindings x.alarms))]
end
-let () =
- let signal = States.register_value ~package
- ~name:"stats"
- ~descr:(Markdown.plain "Statistics about the last Eva analysis")
- ~output:(module Statistics)
- ~get:Value_results.compute_stats
- ()
- in
- Analysis.register_computed_hook (fun () -> Request.emit signal)
+let _computed_signal =
+ States.register_value ~package
+ ~name:"stats"
+ ~descr:(Markdown.plain "Statistics about the last Eva analysis")
+ ~output:(module Statistics)
+ ~get:Value_results.compute_stats
+ ~add_hook:(Analysis.register_computation_hook ~on:Computed)
+ ()
(**************************************************************************)
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index 5255b073cb6..1aae152c818 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -60,7 +60,8 @@ type domain = {
let signal = Request.signal ~package ~name:"changed"
~descr:(Md.plain "Emitted when EVA results has changed")
-let () = Analysis.register_computed_hook (fun () -> Request.emit signal)
+let () = Analysis.register_computation_hook ~on:Computed
+ (fun _ -> Request.emit signal)
(* -------------------------------------------------------------------------- *)
(* --- Marker Utilities --- *)
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 278bc97910d..7fde8c2e3dd 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -114,6 +114,35 @@ module Default =
: Analyzer)
+(* Current state of the analysis *)
+type computation_state = NotComputed | Computing | Computed
+
+module ComputationState =
+struct
+ let to_string = function
+ | NotComputed -> "NotComputed"
+ | Computing -> "Computing"
+ | Computed -> "Computed"
+
+ module Prototype =
+ struct
+ include Datatype.Serializable_undefined
+ type t = computation_state
+ let name = "Eva.Analysis.ComputationState"
+ let pretty fmt s = Format.pp_print_string fmt (to_string s)
+ let reprs = [ NotComputed ; Computing ; Computed ]
+ let dependencies = [ Db.Value.self ]
+ let default () = NotComputed
+ 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
+
(* Reference to the current configuration (built by Abstractions.configure from
the parameters of Eva regarding the abstractions used in the analysis) and
the current Analyzer module. *)
@@ -127,22 +156,27 @@ let current_analyzer () = (module (val (snd !ref_analyzer)): S)
Useful for the GUI parts that depend on it. *)
module Analyzer_Hook = Hook.Build (struct type t = (module S) end)
-(* Set of hooks called whenever the current Analyzer is computed.
- Useful for the GUI parts that depend on it. *)
-module Computed_Hook = Hook.Build (struct type t = unit end)
-
(* Register a new hook. *)
let register_hook = Analyzer_Hook.extend
-(* Register a new computed hook. *)
-let register_computed_hook = Computed_Hook.extend
-
(* Sets the current Analyzer module for a given configuration.
Calls the hooks above. *)
let set_current_analyzer config (analyzer: (module Analyzer)) =
Analyzer_Hook.apply (module (val analyzer): S);
ref_analyzer := (config, analyzer)
+(* Get the current computation state. *)
+let current_computation_state () =
+ ComputationState.get ()
+
+(* 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'
+
let cvalue_initial_state () =
let module A = (val snd !ref_analyzer) in
let _, lib_entry = Globals.entry_point () in
@@ -177,9 +211,10 @@ let force_compute () =
Eva_audit.check_configuration (Kernel.AuditCheck.get ());
let kf, lib_entry = Globals.entry_point () in
reset_analyzer ();
+ ComputationState.set Computing; (* The new analyzer can be accesed through hooks *)
let module Analyzer = (val snd !ref_analyzer) in
Analyzer.compute_from_entry_point ~lib_entry kf ;
- Computed_Hook.apply ()
+ ComputationState.set Computed
(* Resets the Analyzer when the current project is changed. *)
let () =
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index 732d307bd55..055917d6cd4 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -70,9 +70,18 @@ val register_hook: ((module S) -> unit) -> unit
is changed. This happens when a new analysis is run with different
abstractions than before, or when the current project is changed. *)
-val register_computed_hook: (unit -> unit) -> unit
-(** Registers a hook that will be called each time the [current] analyzer
- has been computed. *)
+type computation_state = NotComputed | Computing | Computed
+(** Computation state of the analysis. *)
+
+val current_computation_state : unit -> computation_state
+(** Get the current computation state of the analysis, updated by
+ [force_compute] and states updates. *)
+
+val register_computation_hook: ?on:computation_state ->
+ (computation_state -> unit) -> 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 force_compute : unit -> unit
(** Perform a full analysis, starting from the [main] function. *)
--
GitLab