From af775059c0ed742527a4a64a21c8ef7c97e39b01 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 24 Jun 2024 19:26:18 +0200
Subject: [PATCH] [Eva] Adds requests to run and abort the analysis.
New exception Self.Abort to cleanly abort the analysis without killing Frama-C.
---
.../frama-c/plugins/eva/api/general/index.ts | 22 +++++++++++++++++++
src/plugins/eva/api/general_requests.ml | 16 ++++++++++++++
src/plugins/eva/engine/analysis.ml | 9 +++++++-
src/plugins/eva/engine/analysis.mli | 4 ++++
src/plugins/eva/engine/compute_functions.ml | 3 ++-
src/plugins/eva/engine/iterator.ml | 18 ++++++++-------
src/plugins/eva/engine/iterator.mli | 7 ++++--
src/plugins/eva/self.ml | 2 ++
src/plugins/eva/self.mli | 3 +++
src/plugins/eva/utils/eva_utils.ml | 5 +++--
10 files changed, 75 insertions(+), 14 deletions(-)
diff --git a/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index 2e5a1eec5f8..c37d5121b0b 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -113,6 +113,28 @@ const computationState_internal: State.Value<computationStateType> = {
/** The current computation state of the analysis. */
export const computationState: State.Value<computationStateType> = computationState_internal;
+const compute_internal: Server.ExecRequest<null,null> = {
+ kind: Server.RqKind.EXEC,
+ name: 'plugins.eva.general.compute',
+ input: Json.jNull,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** run eva analysis */
+export const compute: Server.ExecRequest<null,null>= compute_internal;
+
+const abort_internal: Server.GetRequest<null,null> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.abort',
+ input: Json.jNull,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** abort eva analysis */
+export const abort: Server.GetRequest<null,null>= abort_internal;
+
/** Callee function and caller stmt */
export type CallSite = { call: decl, stmt: marker };
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index ec649515e95..c5cba410e23 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -55,6 +55,22 @@ let computation_signal =
~output:(module ComputationState)
(module Self.ComputationState)
+let () = Request.register ~package
+ ~kind:`EXEC
+ ~name:"compute"
+ ~descr:(Markdown.plain "run eva analysis")
+ ~input:(module Data.Junit)
+ ~output:(module Data.Junit)
+ Analysis.compute
+
+let () = Request.register ~package
+ ~kind:`GET (* able to interrupt the EXEC compute request *)
+ ~name:"abort"
+ ~descr:(Markdown.plain "abort eva analysis")
+ ~input:(module Data.Junit)
+ ~output:(module Data.Junit)
+ Analysis.abort
+
(* ----- Callers & Callees -------------------------------------------------- *)
module CallSite =
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index 35c262f48a1..c3b9861d3fd 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -217,7 +217,10 @@ let force_compute () =
(* The new analyzer can be accesed through hooks *)
Self.ComputationState.set Computing;
let module Analyzer = (val snd !ref_analyzer) in
- Analyzer.compute_from_entry_point ~lib_entry kf
+ try Analyzer.compute_from_entry_point ~lib_entry kf
+ with Self.Abort ->
+ Self.(ComputationState.set Aborted);
+ Self.error "The analysis has been aborted: results are incomplete."
let compute () =
(* Nothing to recompute when Eva has already been computed. This boolean
@@ -233,3 +236,7 @@ let () = Parameters.ForceValues.set_output_dependencies [Self.state]
let main () = if Parameters.ForceValues.get () then compute ()
let () = Boot.Main.extend main
+
+let abort () =
+ if Self.ComputationState.get () = Computing
+ then Iterator.signal_abort ~kill:false
diff --git a/src/plugins/eva/engine/analysis.mli b/src/plugins/eva/engine/analysis.mli
index 736b503e7fa..436a53aa7c6 100644
--- a/src/plugins/eva/engine/analysis.mli
+++ b/src/plugins/eva/engine/analysis.mli
@@ -77,6 +77,10 @@ val register_hook: ((module S) -> unit) -> unit
val force_compute : unit -> unit
(** Perform a full analysis, starting from the [main] function. *)
+val abort : unit -> unit
+(** Cleanly abort the analysis at the next safe point: partial results will be
+ saved and Frama-C is not killed. *)
+
[@@@ api_start]
val compute : unit -> unit
(** Computes the Eva analysis, if not already computed, using the entry point
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index e853b106bab..a3bd81ebe62 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -88,6 +88,7 @@ let generate_specs () =
Parameters.UsePrototype.iter aux
let pre_analysis () =
+ Iterator.signal_reset ();
floats_ok ();
options_ok ();
plugins_ok ();
@@ -139,7 +140,7 @@ let register_signal_handler () =
let warn () =
Self.warning ~once:true "Stopping analysis at user request@."
in
- let stop _ = warn (); Iterator.signal_abort () in
+ let stop _ = warn (); Iterator.signal_abort ~kill:true in
let interrupt _ = warn (); raise Sys.Break in
let register_handler signal handler =
match Sys.signal signal (Sys.Signal_handle handler) with
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index f4d84b5a63e..35f3fda11c2 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -26,14 +26,16 @@ open Eva_automata
open Lattice_bounds
open Bottom.Operators
-let check_signals, signal_abort =
- let signal_emitted = ref false in
- (fun () ->
- if !signal_emitted then begin
- signal_emitted := false;
- raise Sys.Break
- end),
- (fun () -> signal_emitted := true)
+type signal = Abort | Kill
+
+let signal_emitted = ref None
+let signal_abort ~kill = signal_emitted := Some (if kill then Kill else Abort)
+let signal_reset () = signal_emitted := None
+
+let check_signals () =
+ Option.iter
+ (fun signal -> raise (if signal = Kill then Sys.Break else Self.Abort))
+ !signal_emitted
let dkey = Self.dkey_iterator
let stat_iterations = Statistics.register_statement_stat "iterations"
diff --git a/src/plugins/eva/engine/iterator.mli b/src/plugins/eva/engine/iterator.mli
index a1b632ba703..b898e9e8663 100644
--- a/src/plugins/eva/engine/iterator.mli
+++ b/src/plugins/eva/engine/iterator.mli
@@ -22,8 +22,11 @@
open Cil_types
-(** Mark the analysis as aborted. It will be stopped at the next safe point *)
-val signal_abort: unit -> unit
+(** Mark the analysis as aborted: it will be stopped at the next safe point. *)
+val signal_abort: kill:bool -> unit
+
+(** Reset the signal sent by [signal_abort], if any. *)
+val signal_reset: unit -> unit
(** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
(resp. snd) is true if and only if the condition of the 'if' has been
diff --git a/src/plugins/eva/self.ml b/src/plugins/eva/self.ml
index d2e1e284de6..590a2a4da92 100644
--- a/src/plugins/eva/self.ml
+++ b/src/plugins/eva/self.ml
@@ -67,6 +67,8 @@ struct
include (State_builder.Ref (Datatype') (Prototype))
end
+exception Abort
+
let is_computed () =
match ComputationState.get () with
| Computed | Aborted -> true
diff --git a/src/plugins/eva/self.mli b/src/plugins/eva/self.mli
index ab724f59bbc..4872dcfaa89 100644
--- a/src/plugins/eva/self.mli
+++ b/src/plugins/eva/self.mli
@@ -35,6 +35,9 @@ type computation_state = NotComputed | Computing | Computed | Aborted
[force_compute] and states updates. *)
module ComputationState : State_builder.Ref with type data = computation_state
+(** Exception used to cleanly abort the analysis (without killing Frama-C). *)
+exception Abort
+
(** Debug categories responsible for printing initial and final states of Value.
Enabled by default, but can be disabled via the command-line:
-value-msg-key="-initial_state,-final_state" *)
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index ad3e6bec741..f8da531466c 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -138,8 +138,9 @@ let protect f ~cleanup =
with
| Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _
| Sys.Break as e when catch () ->
- cleanup ();
- raise e
+ cleanup (); raise e
+ | Self.Abort as e ->
+ cleanup (); raise e
let register_new_var v typ =
if Cil.isFunctionType typ then
--
GitLab