[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

@@ -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 ->

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
 
 

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 ----------------------- *)
 

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

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 *)

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'.