diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml index 54ae0cddc8d06b921dcba983059f675b46df9a09..3ec95cd8ca8ce4bd76a267ceab94d7c6b53a088f 100644 --- a/src/plugins/value/api/general_requests.ml +++ b/src/plugins/value/api/general_requests.ml @@ -45,6 +45,7 @@ module ComputationState = struct | Analysis.NotComputed -> `String "not_computed" | Computing -> `String "computing" | Computed -> `String "computed" + | Aborted -> `String "aborted" end let _computation_signal = diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml index 122e2c5ca6c2656f4da3339c1b80fc101dfcae1c..0b609958aeb1091140665d5b0982a83d9e2279ab 100644 --- a/src/plugins/value/engine/analysis.ml +++ b/src/plugins/value/engine/analysis.ml @@ -23,6 +23,11 @@ open Cil_types open Eval +type computation_state = Self.computation_state = + | NotComputed | Computing | Computed | Aborted +let current_computation_state = Self.current_computation_state +let register_computation_hook = Self.register_computation_hook + module type Results = sig type state type value @@ -116,36 +121,6 @@ module Default = else (module Make (Abstractions.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 = [ Self.state ] - 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. *) @@ -168,18 +143,6 @@ 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 @@ -214,10 +177,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 *) + (* The new analyzer can be accesed through hooks *) + Self.set_computation_state Computing; let module Analyzer = (val snd !ref_analyzer) in - Analyzer.compute_from_entry_point ~lib_entry kf ; - ComputationState.set Computed + Analyzer.compute_from_entry_point ~lib_entry kf let is_computed = Db.Value.is_computed diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli index 7eb2d53ef9b03bc1ace961ebf8be08ed5cd75564..98d61c3fc42aff8890a05eabcb32b8c82fa18e5d 100644 --- a/src/plugins/value/engine/analysis.mli +++ b/src/plugins/value/engine/analysis.mli @@ -72,7 +72,7 @@ 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 +type computation_state = NotComputed | Computing | Computed | Aborted (** Computation state of the analysis. *) val current_computation_state : unit -> computation_state diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml index a22d04bfebf60217422f34a2890cf1b84362ba42..b0dd26b84ba0822d7fc896839b6a00a5dca3d8dd 100644 --- a/src/plugins/value/engine/compute_functions.ml +++ b/src/plugins/value/engine/compute_functions.ml @@ -356,6 +356,7 @@ 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 (); post_analysis (); Abstract.Dom.post_analysis final_state; @@ -363,6 +364,7 @@ module Make (Abstract: Abstractions.Eva) = struct restore_signals () in let cleanup () = + Self.(set_computation_state Aborted); Abstract.Dom.Store.mark_as_computed (); post_analysis_cleanup ~aborted:true in @@ -380,6 +382,7 @@ module Make (Abstract: Abstractions.Eva) = struct in match initial_state with | `Bottom -> + Self.(set_computation_state Aborted); Abstract.Dom.Store.mark_as_computed (); Self.result "Eva not started because globals \ initialization is not computable."; diff --git a/src/plugins/value/self.ml b/src/plugins/value/self.ml index 660ac61d9a5f179f2174c4e36ef8592439c07101..f0596f76bbcd557dbff1f07eca5e8f5a38cf4b8a 100644 --- a/src/plugins/value/self.ml +++ b/src/plugins/value/self.ml @@ -28,6 +28,9 @@ include Plugin.Register "automatically computes variation domains for the variables of the program" end) +let () = Help.add_aliases ~visible:false [ "-value-h"; "-val-h" ] +let () = add_plugin_output_aliases ~visible:false ~deprecated:true [ "value" ] + (* Do not add dependencies to Kernel parameters here, but at the top of Parameters. *) let kernel_dependencies = @@ -42,8 +45,53 @@ let state = State_builder.Proxy.get proxy let () = State_builder.Proxy.extend [state] Db.Value.proxy -let () = Help.add_aliases ~visible:false [ "-value-h"; "-val-h" ] -let () = add_plugin_output_aliases ~visible:false ~deprecated:true [ "value" ] + +(* Current state of the analysis *) +type computation_state = NotComputed | Computing | Computed | Aborted + +module ComputationState = +struct + let to_string = function + | NotComputed -> "NotComputed" + | Computing -> "Computing" + | Computed -> "Computed" + | Aborted -> "Aborted" + + 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 ; Aborted ] + let dependencies = [ state ] + 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 + +let is_computed () = + match ComputationState.get () with + | Computed | Aborted -> true + | NotComputed | Computing -> false + +let current_computation_state = ComputationState.get +let set_computation_state = ComputationState.set + +(* 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' + (* Debug categories. *) let dkey_initial_state = register_category "initial-state" diff --git a/src/plugins/value/self.mli b/src/plugins/value/self.mli index cd4de22ea767957d005d1cba9f703b5ed73eb4ab..a710b296982494a2ebefc8ff8f20739db657d612 100644 --- a/src/plugins/value/self.mli +++ b/src/plugins/value/self.mli @@ -25,6 +25,25 @@ include Plugin.General_services val proxy: State_builder.Proxy.t val state: State.t +(** Return [true] iff the value analysis has been done. *) +val is_computed: unit -> bool + +(** Computation state of the analysis. *) +type computation_state = NotComputed | Computing | Computed | Aborted + +(** Get the current computation state of the analysis, updated by + [force_compute] and states updates. *) +val current_computation_state : unit -> computation_state + +(** Set the current computation state. *) +val set_computation_state: computation_state -> 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 register_computation_hook: ?on:computation_state -> + (computation_state -> unit) -> unit + (** 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" *)