Merge branch 'feature/eva/api-hook' into 'master'

[Eva] API: exports analysis computation state and hook.

See merge request frama-c/frama-c!3712

src/plugins/impact/pdg_aux.ml

@@ -104,7 +104,7 @@ module NS = struct
     fold (fun n z -> f (n, z))
 
 
-  let () = Db.Value.Table_By_Callstack.add_hook_on_update (fun _ -> clear_caches ())
+  let () = Eva.Analysis.register_computation_hook (fun _ -> clear_caches ())
 end
 
 type call_interface = (PdgTypes.Node.t * NS.t) list

src/plugins/metrics/register_gui.ml

@@ -272,7 +272,7 @@ module ValueCoverageGUI = struct
     update_filetree := refresh
 
   let () =
-    Db.Value.Table_By_Callstack.add_hook_on_update
+    Eva.Analysis.register_computation_hook
       (fun _ ->
          Metrics_coverage.clear_coverage_by_fun ();
          !update_filetree `Visibility)

src/plugins/users/users_register.ml

@@ -47,28 +47,30 @@ module Users =
       let dependencies = [ Eva.Analysis.self; ForceUsers.self ]
     end)
 
-let call_for_users (_state, call_stack) =
-  match call_stack with
-  | [] -> assert false
-  | (current_function, _call_site) :: tail ->
-    if tail = [] then begin
-      (* End of Value analysis, we record that Users has run. We should not
-         do this after the explicit call to Eva.Analysis.compute later in this
-         file, as Value can run on its own and execute Users while doing so.*)
-      Users.mark_as_computed ()
-    end;
-    let treat_element (user, _call_site) =
-      ignore
-        (Users.memo
-           ~change:(Kernel_function.Hptset.add current_function)
-           (fun _ -> Kernel_function.Hptset.singleton current_function)
-           user)
-    in
-    List.iter treat_element tail
+let compute_users _ =
+  let process kf =
+    if Eva.Results.is_called kf
+    then
+      let callstacks = Eva.Results.(at_start_of kf |> callstacks) in
+      let process_callstack list =
+        let process_element (user, _call_site) =
+          ignore
+            (Users.memo
+               ~change:(Kernel_function.Hptset.add kf)
+               (fun _ -> Kernel_function.Hptset.singleton kf)
+               user)
+        in
+        List.iter process_element (List.tl list)
+      in
+      List.iter process_callstack callstacks
+  in
+  Globals.Functions.iter process;
+  Users.mark_as_computed ()
 
-let add_value_hook () = Db.Value.Call_Value_Callbacks.extend_once call_for_users
+let add_eva_hook () =
+  Eva.Analysis.(register_computation_hook ~on:Computed compute_users)
 
-let init () = if ForceUsers.get () then add_value_hook ()
+let init () = if ForceUsers.get () then add_eva_hook ()
 let () = Cmdline.run_after_configuring_stage init
 
 let get kf =
@@ -86,8 +88,8 @@ let get kf =
         ()
     end else
       feedback ~level:2 "requiring the computation of the value analysis";
-    add_value_hook ();
     Eva.Analysis.compute ();
+    compute_users ();
     find kf
   end
 

src/plugins/value/engine/analysis.mli

@@ -74,19 +74,6 @@ 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. *)
 
-type computation_state = NotComputed | Computing | Computed | Aborted
-(** 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. *)
 
@@ -106,6 +93,18 @@ val is_computed : unit -> bool
 val self : State.t
 (** Internal state of Eva analysis from projects viewpoint. *)
 
+type computation_state = NotComputed | Computing | Computed | Aborted
+(** 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. *)
 
 (** Kind of results for the analysis of a function body. *)
 type results =

src/plugins/value/engine/compute_functions.ml

@@ -360,16 +360,16 @@ module Make (Abstract: Abstractions.Eva) = struct
       let final_state = PowersetDomain.(final_states |> of_list |> join) in
       Eva_utils.pop_call_stack ();
       Self.feedback "done for function %a" Kernel_function.pretty kf;
-      Self.(set_computation_state Computed);
       Abstract.Dom.Store.mark_as_computed ();
+      Self.(set_computation_state Computed);
       post_analysis ();
       Abstract.Dom.post_analysis final_state;
       Summary.print_summary ();
       restore_signals ()
     in
     let cleanup () =
-      Self.(set_computation_state Aborted);
       Abstract.Dom.Store.mark_as_computed ();
+      Self.(set_computation_state Aborted);
       post_analysis_cleanup ~aborted:true
     in
     Eva_utils.protect compute ~cleanup
@@ -386,8 +386,8 @@ module Make (Abstract: Abstractions.Eva) = struct
     in
     match initial_state with
     | `Bottom ->
-      Self.(set_computation_state Aborted);
       Abstract.Dom.Store.mark_as_computed ();
+      Self.(set_computation_state Aborted);
       Self.result "Eva not started because globals \
                    initialization is not computable.";
       Eval_annots.mark_invalid_initializers ()