From 7ea29bd2f9c10a12df9337efb2ecf1fe92373135 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 5 Oct 2021 14:53:27 +0200
Subject: [PATCH] [Eva] Aborts the analysis cleanly on user interruption sigint
(Ctrl-C).
Cleans up and saves partial results on sigint signal.
Signal handlers are now registered at the start of an analysis, and previous
signal handlers are restored at the end.
New function [protect f ~cleanup] in value_util, that runs [f] and applies
[cleanup] in case of a user interruption or a Frama-C error, only if option
-save is set.
---
src/plugins/value/engine/compute_functions.ml | 50 +++++++++++--------
src/plugins/value/engine/iterator.ml | 13 ++---
src/plugins/value/engine/transfer_stmt.ml | 9 ++--
src/plugins/value/utils/value_util.ml | 16 ++++++
src/plugins/value/utils/value_util.mli | 5 ++
tests/fc_script/oracle/make-wrapper.res | 1 +
6 files changed, 62 insertions(+), 32 deletions(-)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 09d04639e82..a932d0eebdc 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -113,20 +113,25 @@ let post_analysis () =
(* Remove redundant alarms *)
if Value_parameters.RmAssert.get () then !Db.Value.rm_asserts ()
-(* Register a signal handler for SIGUSR1, that will be used to abort Value *)
-let () =
- let prev = ref (fun _ -> ()) in
- let handler (_signal: int) =
- !prev Sys.sigusr1; (* Call previous signal handler *)
- Value_parameters.warning "Stopping analysis at user request@.";
- Iterator.signal_abort ()
+(* Registers signal handlers for SIGUSR1 and SIGINT to cleanly abort the Eva
+ analysis. Returns a function that restores previous signal behaviors after
+ the analysis. *)
+let register_signal_handler () =
+ let warn () =
+ Value_parameters.warning ~once:true "Stopping analysis at user request@."
in
- try
- match Sys.signal Sys.sigusr1 (Sys.Signal_handle handler) with
- | Sys.Signal_default | Sys.Signal_ignore -> ()
- | Sys.Signal_handle f -> prev := f
- with Invalid_argument _ -> () (* Ignore: SIGURSR1 is not available on Windows,
- and possibly on other platforms. *)
+ let stop _ = warn (); Iterator.signal_abort () in
+ let interrupt _ = warn (); raise Sys.Break in
+ let register_handler signal handler =
+ match Sys.signal signal (Sys.Signal_handle handler) with
+ | previous_behavior -> fun () -> Sys.set_signal signal previous_behavior
+ | exception Invalid_argument _ -> fun () -> ()
+ (* Ignore: SIGURSR1 is not available on Windows,
+ and possibly on other platforms. *)
+ in
+ let restore_sigusr1 = register_handler Sys.sigusr1 stop in
+ let restore_sigint = register_handler Sys.sigint interrupt in
+ fun () -> restore_sigusr1 (); restore_sigint ()
module Make (Abstract: Abstractions.Eva) = struct
@@ -327,7 +332,8 @@ module Make (Abstract: Abstractions.Eva) = struct
Db.Value.Call_Value_Callbacks.apply (cvalue_state, [kf, Kglobal])
let compute kf init_state =
- try
+ let restore_signals = register_signal_handler () in
+ let compute () =
Value_util.push_call_stack kf Kglobal;
store_initial_state kf init_state;
let call =
@@ -344,10 +350,13 @@ module Make (Abstract: Abstractions.Eva) = struct
post_analysis ();
Abstract.Dom.post_analysis final_state;
Value_results.print_summary ();
- with Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _ as e ->
+ restore_signals ()
+ in
+ let cleanup () =
Abstract.Dom.Store.mark_as_computed ();
- post_analysis_cleanup ~aborted:true;
- raise e
+ post_analysis_cleanup ~aborted:true
+ in
+ Value_util.protect compute ~cleanup
let compute_from_entry_point kf ~lib_entry =
pre_analysis ();
@@ -355,10 +364,9 @@ module Make (Abstract: Abstractions.Eva) = struct
(if lib_entry then "n in" else " ")
Kernel_function.pretty kf;
let initial_state =
- try Init.initial_state_with_formals ~lib_entry kf
- with Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _ as e ->
- post_analysis_cleanup ~aborted:true;
- raise e
+ Value_util.protect
+ (fun () -> Init.initial_state_with_formals ~lib_entry kf)
+ ~cleanup:(fun () -> post_analysis_cleanup ~aborted:true)
in
match initial_state with
| `Bottom ->
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 6f1f546680a..933035419a6 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -29,7 +29,7 @@ let check_signals, signal_abort =
(fun () ->
if !signal_emitted then begin
signal_emitted := false;
- raise (Log.AbortError "eva")
+ raise Sys.Break
end),
(fun () -> signal_emitted := true)
@@ -765,7 +765,7 @@ module Computer
end)
()
in
- try
+ let compute () =
let results = Dataflow.compute () in
if Value_parameters.ValShowProgress.get () then
Value_parameters.feedback "Recording results for %a"
@@ -779,11 +779,12 @@ module Computer
Kernel_function.pretty kf;
| _ -> ());
results, !Dataflow.cacheable
- with Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _ as e ->
- (* analysis was aborted: pop the call stack and inform the caller *)
+ in
+ let cleanup () =
Dataflow.mark_degeneration ();
- Dataflow.merge_results ();
- raise e
+ Dataflow.merge_results ()
+ in
+ Value_util.protect compute ~cleanup
end
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 874b2b65af0..f18e4c385e8 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -319,7 +319,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Changed by compute_call_ref, called from process_call *)
Cil.CurrentLoc.set (Cil_datatype.Stmt.loc stmt);
in
- try
+ let process () =
let domain_valuation = Eval.to_domain_valuation valuation in
let res =
(* Process the call according to the domain decision. *)
@@ -332,10 +332,9 @@ module Make (Abstract: Abstractions.Eva) = struct
in
cleanup ();
res
- with Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _ as e ->
- InOutCallback.clear ();
- cleanup ();
- raise e
+ in
+ Value_util.protect process
+ ~cleanup:(fun () -> InOutCallback.clear (); cleanup ())
(* ------------------- Retro propagation on formals ----------------------- *)
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index 13a005dd2af..9f7ddc3f461 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -107,6 +107,22 @@ module DegenerationPoints =
let dependencies = [ Db.Value.self ]
end)
+let protect_only_once = ref true
+
+let protect f ~cleanup =
+ let catch () = !protect_only_once && not (Kernel.SaveState.is_empty ()) in
+ try f ();
+ with
+ | Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _
+ | Sys.Break as e when catch () ->
+ try
+ Value_parameters.feedback ~once:true "Clean up and save partial results.";
+ cleanup ();
+ raise e;
+ with e ->
+ protect_only_once := false;
+ raise e
+
let register_new_var v typ =
if Cil.isFunctionType typ then
Globals.Functions.replace_by_declaration (Cil.empty_funspec()) v v.vdecl
diff --git a/src/plugins/value/utils/value_util.mli b/src/plugins/value/utils/value_util.mli
index 0bfe89cbe91..c99393d8885 100644
--- a/src/plugins/value/utils/value_util.mli
+++ b/src/plugins/value/utils/value_util.mli
@@ -51,6 +51,11 @@ val warning_once_current : ('a, Format.formatter, unit) format -> 'a
status associated to {!Value_parameters.wkey_alarm} *)
val alarm_report: 'a Log.pretty_printer
+(** [protect f ~cleanup] runs [f]. On a user interruption or a Frama-C error,
+ if option -save is set, applies [cleanup]. This is used to clean up and
+ save partial results when the analysis is aborted. *)
+val protect: (unit -> 'a) -> cleanup:(unit -> unit) -> 'a
+
(* Statements for which the analysis has degenerated. [true] means that this is
the statement on which the degeneration occurred, or a statement above in
the callstack *)
diff --git a/tests/fc_script/oracle/make-wrapper.res b/tests/fc_script/oracle/make-wrapper.res
index 09358673bd0..8370fe5e494 100644
--- a/tests/fc_script/oracle/make-wrapper.res
+++ b/tests/fc_script/oracle/make-wrapper.res
@@ -25,6 +25,7 @@ Command: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-war
[kernel:annot:missing-spec] make-wrapper.c:13: Warning:
Neither code nor specification for function large_name_to_force_line_break_in_stack_msg, generating default assigns from the prototype
[kernel] User Error: warning annot:missing-spec treated as fatal error.
+[eva] Clean up and save partial results.
[kernel] Frama-C aborted: invalid user input.
[kernel] Warning: attempting to save on non-zero exit code: modifying filename into `PWD/make-for-make-wrapper.eva/framac.sav.error'.
--
GitLab