From 7fd662420dc63a6c472958e57febaa7adf5ec87a Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 25 Jan 2024 14:57:36 +0100
Subject: [PATCH] [kernel] move Db functions to Async
---
.../plugin_entry_points/async.ml | 157 ++++++++++++++++++
.../plugin_entry_points/async.mli | 81 +++++++++
src/kernel_services/plugin_entry_points/db.ml | 148 -----------------
.../plugin_entry_points/db.mli | 93 -----------
src/libraries/utils/command.ml | 8 +-
src/libraries/utils/command.mli | 2 +-
src/libraries/utils/task.ml | 10 +-
src/plugins/eva/engine/iterator.ml | 2 +-
src/plugins/from/from_compute.ml | 8 +-
src/plugins/gui/analyses_manager.ml | 2 +-
src/plugins/gui/design.ml | 2 +-
src/plugins/gui/gtk_helper.ml | 2 +-
src/plugins/impact/compute_impact.ml | 2 +-
src/plugins/occurrence/register.ml | 2 +-
src/plugins/pdg/build.ml | 6 +-
src/plugins/postdominators/compute.ml | 2 +-
src/plugins/server/main.ml | 20 +--
src/plugins/server/main.mli | 6 +-
src/plugins/wp/Conditions.ml | 4 +-
src/plugins/wp/wp_parameters.ml | 2 +-
src/plugins/wp/wpo.ml | 2 +-
21 files changed, 279 insertions(+), 282 deletions(-)
create mode 100644 src/kernel_services/plugin_entry_points/async.ml
create mode 100644 src/kernel_services/plugin_entry_points/async.mli
diff --git a/src/kernel_services/plugin_entry_points/async.ml b/src/kernel_services/plugin_entry_points/async.ml
new file mode 100644
index 00000000000..62b272ad710
--- /dev/null
+++ b/src/kernel_services/plugin_entry_points/async.ml
@@ -0,0 +1,157 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+type daemon = {
+ trigger : unit -> unit ;
+ on_delayed : (int -> unit) option ;
+ on_finished : (unit -> unit) option ;
+ debounced : float ; (* in ms *)
+ mutable next_at : float ; (* next trigger time *)
+ mutable last_yield_at : float ; (* last yield time *)
+}
+
+(* ---- Registry ---- *)
+
+let daemons = ref []
+
+let on_progress ?(debounced=0) ?on_delayed ?on_finished trigger =
+ let d = {
+ trigger ;
+ debounced = float debounced *. 0.001 ;
+ on_delayed ;
+ on_finished ;
+ last_yield_at = 0.0 ;
+ next_at = 0.0 ;
+ } in
+ daemons := List.append !daemons [d] ; d
+
+let off_progress d =
+ daemons := List.filter (fun d0 -> d != d0) !daemons ;
+ match d.on_finished with
+ | None -> ()
+ | Some f -> f ()
+
+let while_progress ?debounced ?on_delayed ?on_finished progress =
+ let d : daemon option ref = ref None in
+ let trigger () =
+ if not @@ progress () then
+ Option.iter off_progress !d
+ in
+ d := Some (on_progress ?debounced ?on_delayed ?on_finished trigger)
+
+let with_progress ?debounced ?on_delayed ?on_finished trigger job data =
+ let d = on_progress ?debounced ?on_delayed ?on_finished trigger in
+ let result =
+ try job data
+ with exn ->
+ off_progress d ;
+ raise exn
+ in
+ off_progress d ; result
+
+(* ---- Canceling ---- *)
+
+exception Cancel
+
+(* ---- Triggering ---- *)
+
+let canceled = ref false
+let cancel () = canceled := true
+
+let warn_error exn =
+ Kernel.failure
+ "Unexpected Async.daemon exception:@\n%s"
+ (Printexc.to_string exn)
+
+let fire ~warn_on_delayed ~forced ~time d =
+ if forced || time > d.next_at then
+ begin
+ try
+ d.next_at <- time +. d.debounced ;
+ d.trigger () ;
+ with
+ | Cancel -> canceled := true
+ | exn -> warn_error exn ; raise exn
+ end ;
+ match d.on_delayed with
+ | None -> ()
+ | Some warn ->
+ if warn_on_delayed && 0.0 < d.last_yield_at then
+ begin
+ let time_since_last_yield = time -. d.last_yield_at in
+ let delay = if d.debounced > 0.0 then d.debounced else 0.1 in
+ if time_since_last_yield > delay then
+ warn (int_of_float (time_since_last_yield *. 1000.0)) ;
+ end ;
+ d.last_yield_at <- time
+
+let raise_if_canceled () =
+ if !canceled then ( canceled := false ; raise Cancel )
+
+(* ---- Yielding ---- *)
+
+let do_yield ~warn_on_delayed ~forced () =
+ match !daemons with
+ | [] -> ()
+ | ds ->
+ begin
+ let time = Unix.gettimeofday () in
+ List.iter (fire ~warn_on_delayed ~forced ~time) ds ;
+ raise_if_canceled () ;
+ end
+
+let yield = do_yield ~warn_on_delayed:true ~forced:false
+let flush = do_yield ~warn_on_delayed:false ~forced:true
+
+(* ---- Sleeping ---- *)
+
+let rec gcd a b = if b = 0 then a else gcd b (a mod b)
+
+(* n=0 means no periodic daemons (yet) *)
+let merge_period n { debounced = p } =
+ if p > 0.0 then gcd (int_of_float (p *. 1000.0)) n else n
+
+let sleep ms =
+ if ms > 0 then
+ let delta = float ms *. 0.001 in
+ let period = List.fold_left merge_period 0 !daemons in
+ if period = 0 then
+ begin
+ Unix.sleepf delta ;
+ do_yield ~warn_on_delayed:false ~forced:false ()
+ end
+ else
+ let delay = float period *. 0.001 in
+ let finished_at = Unix.gettimeofday () +. delta in
+ let rec wait_and_trigger () =
+ Unix.sleepf delay ;
+ let time = Unix.gettimeofday () in
+ List.iter
+ (fire ~warn_on_delayed:false ~forced:false ~time)
+ !daemons ;
+ raise_if_canceled () ;
+ if time < finished_at then
+ if time +. delay > finished_at then
+ Unix.sleepf (finished_at -. time)
+ else wait_and_trigger ()
+ in
+ wait_and_trigger ()
diff --git a/src/kernel_services/plugin_entry_points/async.mli b/src/kernel_services/plugin_entry_points/async.mli
new file mode 100644
index 00000000000..669045664fb
--- /dev/null
+++ b/src/kernel_services/plugin_entry_points/async.mli
@@ -0,0 +1,81 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Registered daemon on progress. *)
+type daemon
+
+(**
+ [on_progress ?debounced ?on_delayed trigger] registers [trigger] as new
+ daemon to be executed on each {!yield}.
+ @param debounced the least amount of time between two successive calls to the
+ daemon, in milliseconds (default is 0ms).
+ @param on_delayed callback is invoked as soon as the time since the last
+ {!yield} is greater than [debounced] milliseconds (or 100ms at least).
+ @param on_finished callback is invoked when the callback is unregistered.
+*)
+val on_progress :
+ ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
+ (unit -> unit) -> daemon
+
+(** Unregister the [daemon]. *)
+val off_progress : daemon -> unit
+
+(** [while_progress ?debounced ?on_delayed ?on_finished trigger] is similar to
+ [on_progress] but the daemon is automatically unregistered
+ as soon as [trigger] returns [false].
+ Same optional parameters than [on_progress].
+*)
+val while_progress :
+ ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
+ (unit -> bool) -> unit
+
+(**
+ [with_progress ?debounced ?on_delayed trigger job data] executes the given
+ [job] on [data] while registering [trigger] as temporary (debounced) daemon.
+ The daemon is finally unregistered at the end of the computation.
+ Same optional parameters than [on_progress].
+*)
+val with_progress :
+ ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
+ (unit -> unit) -> ('a -> 'b) -> 'a -> 'b
+
+(** Trigger all daemons immediately. *)
+val flush : unit -> unit
+
+(** Trigger all registered daemons (debounced).
+ This function should be called from time to time by all analysers taking
+ time. In GUI or Server mode, this will make the clients responsive. *)
+val yield : unit -> unit
+
+(** Interrupt the currently running job: the next call to {!yield}
+ will raise a [Cancel] exception. *)
+val cancel : unit -> unit
+
+(**
+ Pauses the currently running process for the specified time, in milliseconds.
+ Registered daemons, if any, will be regularly triggered during this waiting
+ time at a reasonable period with respect to their debouncing constraints.
+*)
+val sleep : int -> unit
+
+(** This exception may be raised by {!yield} to interrupt computations. *)
+exception Cancel
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 94925cd9905..e1d0d1816d5 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -23,151 +23,3 @@
module Main = struct
let extend = Boot.Main.extend
end
-
-(* ************************************************************************* *)
-(** {2 GUI} *)
-(* ************************************************************************* *)
-
-type daemon = {
- trigger : unit -> unit ;
- on_delayed : (int -> unit) option ;
- on_finished : (unit -> unit) option ;
- debounced : float ; (* in ms *)
- mutable next_at : float ; (* next trigger time *)
- mutable last_yield_at : float ; (* last yield time *)
-}
-
-(* ---- Registry ---- *)
-
-let daemons = ref []
-
-let on_progress ?(debounced=0) ?on_delayed ?on_finished trigger =
- let d = {
- trigger ;
- debounced = float debounced *. 0.001 ;
- on_delayed ;
- on_finished ;
- last_yield_at = 0.0 ;
- next_at = 0.0 ;
- } in
- daemons := List.append !daemons [d] ; d
-
-let off_progress d =
- daemons := List.filter (fun d0 -> d != d0) !daemons ;
- match d.on_finished with
- | None -> ()
- | Some f -> f ()
-
-let while_progress ?debounced ?on_delayed ?on_finished progress =
- let d : daemon option ref = ref None in
- let trigger () =
- if not @@ progress () then
- Option.iter off_progress !d
- in
- d := Some (on_progress ?debounced ?on_delayed ?on_finished trigger)
-
-let with_progress ?debounced ?on_delayed ?on_finished trigger job data =
- let d = on_progress ?debounced ?on_delayed ?on_finished trigger in
- let result =
- try job data
- with exn ->
- off_progress d ;
- raise exn
- in
- off_progress d ; result
-
-(* ---- Canceling ---- *)
-
-exception Cancel
-
-(* ---- Triggering ---- *)
-
-let canceled = ref false
-let cancel () = canceled := true
-
-let warn_error exn =
- Kernel.failure
- "Unexpected Db.daemon exception:@\n%s"
- (Printexc.to_string exn)
-
-let fire ~warn_on_delayed ~forced ~time d =
- if forced || time > d.next_at then
- begin
- try
- d.next_at <- time +. d.debounced ;
- d.trigger () ;
- with
- | Cancel -> canceled := true
- | exn -> warn_error exn ; raise exn
- end ;
- match d.on_delayed with
- | None -> ()
- | Some warn ->
- if warn_on_delayed && 0.0 < d.last_yield_at then
- begin
- let time_since_last_yield = time -. d.last_yield_at in
- let delay = if d.debounced > 0.0 then d.debounced else 0.1 in
- if time_since_last_yield > delay then
- warn (int_of_float (time_since_last_yield *. 1000.0)) ;
- end ;
- d.last_yield_at <- time
-
-let raise_if_canceled () =
- if !canceled then ( canceled := false ; raise Cancel )
-
-(* ---- Yielding ---- *)
-
-let do_yield ~warn_on_delayed ~forced () =
- match !daemons with
- | [] -> ()
- | ds ->
- begin
- let time = Unix.gettimeofday () in
- List.iter (fire ~warn_on_delayed ~forced ~time) ds ;
- raise_if_canceled () ;
- end
-
-let yield = do_yield ~warn_on_delayed:true ~forced:false
-let flush = do_yield ~warn_on_delayed:false ~forced:true
-
-(* ---- Sleeping ---- *)
-
-let rec gcd a b = if b = 0 then a else gcd b (a mod b)
-
-(* n=0 means no periodic daemons (yet) *)
-let merge_period n { debounced = p } =
- if p > 0.0 then gcd (int_of_float (p *. 1000.0)) n else n
-
-let sleep ms =
- if ms > 0 then
- let delta = float ms *. 0.001 in
- let period = List.fold_left merge_period 0 !daemons in
- if period = 0 then
- begin
- Unix.sleepf delta ;
- do_yield ~warn_on_delayed:false ~forced:false ()
- end
- else
- let delay = float period *. 0.001 in
- let finished_at = Unix.gettimeofday () +. delta in
- let rec wait_and_trigger () =
- Unix.sleepf delay ;
- let time = Unix.gettimeofday () in
- List.iter
- (fire ~warn_on_delayed:false ~forced:false ~time)
- !daemons ;
- raise_if_canceled () ;
- if time < finished_at then
- if time +. delay > finished_at then
- Unix.sleepf (finished_at -. time)
- else wait_and_trigger ()
- in
- wait_and_trigger ()
-
-(* ************************************************************************* *)
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index e119a4018c2..f30706002fe 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -20,31 +20,6 @@
(* *)
(**************************************************************************)
-(** Database in which static plugins are registered.
- @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
-
-(**
- Modules providing general services:
- - {!Dynamic}: API for plug-ins linked dynamically
- - {!Log}: message outputs and printers
- - {!Plugin}: general services for plug-ins
- - {!Project} and associated files: {!Datatype} and {!State_builder}.
-
- Other main kernel modules:
- - {!Ast}: the cil AST
- - {!Ast_info}: syntactic value directly computed from the Cil Ast
- - {!File}: Cil file initialization
- - {!Globals}: global variables, functions and annotations
- - {!Annotations}: annotations associated with a statement
- - {!Property_status}: status of annotations
- - {!Kernel_function}: C functions as seen by Frama-C
- - {!Stmts_graph}: the statement graph
- - {!Loop}: (natural) loops
- - {!Visitor}: frama-c visitors
- - {!Kernel}: general parameters of Frama-C (mostly set from the command
- line)
-*)
-
(** DEPRECATED Frama-C main interface.
@since Lithium-20081201
@deprecated Frama-C+dev Use module {!Boot.Main} *)
@@ -54,71 +29,3 @@ module Main: sig
(** Register a function to be called by the Frama-C main entry point.
@deprecated Frama-C+dev Use module {!Boot.Main} *)
end
-
-(** {3 GUI} *)
-
-(** Registered daemon on progress. *)
-type daemon
-
-(**
- [on_progress ?debounced ?on_delayed trigger] registers [trigger] as new
- daemon to be executed on each {!yield}.
- @param debounced the least amount of time between two successive calls to the
- daemon, in milliseconds (default is 0ms).
- @param on_delayed callback is invoked as soon as the time since the last
- {!yield} is greater than [debounced] milliseconds (or 100ms at least).
- @param on_finished callback is invoked when the callback is unregistered.
-*)
-val on_progress :
- ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
- (unit -> unit) -> daemon
-
-(** Unregister the [daemon]. *)
-val off_progress : daemon -> unit
-
-(** [while_progress ?debounced ?on_delayed ?on_finished trigger] is similar to
- [on_progress] but the daemon is automatically unregistered
- as soon as [trigger] returns [false].
- Same optional parameters than [on_progress].
-*)
-val while_progress :
- ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
- (unit -> bool) -> unit
-
-(**
- [with_progress ?debounced ?on_delayed trigger job data] executes the given
- [job] on [data] while registering [trigger] as temporary (debounced) daemon.
- The daemon is finally unregistered at the end of the computation.
- Same optional parameters than [on_progress].
-*)
-val with_progress :
- ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
- (unit -> unit) -> ('a -> 'b) -> 'a -> 'b
-
-(** Trigger all daemons immediately. *)
-val flush : unit -> unit
-
-(** Trigger all registered daemons (debounced).
- This function should be called from time to time by all analysers taking
- time. In GUI or Server mode, this will make the clients responsive. *)
-val yield : unit -> unit
-
-(** Interrupt the currently running job: the next call to {!yield}
- will raise a [Cancel] exception. *)
-val cancel : unit -> unit
-
-(**
- Pauses the currently running process for the specified time, in milliseconds.
- Registered daemons, if any, will be regularly triggered during this waiting
- time at a reasonable period with respect to their debouncing constraints.
-*)
-val sleep : int -> unit
-
-(** This exception may be raised by {!yield} to interrupt computations. *)
-exception Cancel
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/libraries/utils/command.ml b/src/libraries/utils/command.ml
index c0ef15d6202..f2211d8a389 100644
--- a/src/libraries/utils/command.ml
+++ b/src/libraries/utils/command.ml
@@ -43,7 +43,7 @@ let pp_from_file fmt (file: Filepath.Normalized.t) =
let cin = open_in (file :> string) in
try
while true do
- Db.yield () ;
+ Async.yield () ;
let line = input_line cin in
Format.pp_print_string fmt line ;
Format.pp_print_newline fmt () ;
@@ -248,11 +248,11 @@ let command ?(timeout=0) ?stdout ?stderr cmd args =
| Not_ready terminate ->
begin
try
- Db.yield () ;
+ Async.yield () ;
if timeout > 0 && Unix.gettimeofday () -. !start > ftimeout then
- raise Db.Cancel ;
+ raise Async.Cancel ;
true
- with Db.Cancel as e ->
+ with Async.Cancel as e ->
terminate ();
raise e
end
diff --git a/src/libraries/utils/command.mli b/src/libraries/utils/command.mli
index bdf1f030c40..6422211b226 100644
--- a/src/libraries/utils/command.mli
+++ b/src/libraries/utils/command.mli
@@ -125,7 +125,7 @@ val command :
When this function returns, the stdout and stderr of the child
process will be filled into the arguments buffer.
@raise Sys_error when a system error occurs
- @raise Db.Cancel when the computation is interrupted or on timeout *)
+ @raise Async.Cancel when the computation is interrupted or on timeout *)
(*
Local Variables:
diff --git a/src/libraries/utils/task.ml b/src/libraries/utils/task.ml
index 557953250f4..86beb2188dc 100644
--- a/src/libraries/utils/task.ml
+++ b/src/libraries/utils/task.ml
@@ -108,9 +108,9 @@ struct
let rec wait = function
| UNIT a -> a
- | YIELD f -> Db.yield() ; wait (f Coin)
+ | YIELD f -> Async.yield() ; wait (f Coin)
| WAIT(ms,f) ->
- Db.yield() ; Unix.sleepf (float_of_int ms /. 1_000_000.); wait (f Coin)
+ Async.yield() ; Unix.sleepf (float_of_int ms /. 1_000_000.); wait (f Coin)
let finished = function UNIT a -> Some a | YIELD _ | WAIT _ -> None
@@ -342,7 +342,7 @@ let share sh = todo
let on_idle = ref
(fun f -> try
while f () do Unix.sleepf 0.05 (* wait for 50ms *) done
- with Db.Cancel -> ())
+ with Async.Cancel -> ())
(* -------------------------------------------------------------------------- *)
(* --- Task thread --- *)
@@ -484,8 +484,8 @@ let server_progress server () =
) server.running ;
Array.iter (schedule server) server.queue ;
let () =
- try Db.yield ()
- with Db.Cancel -> cancel_all server
+ try Async.yield ()
+ with Async.Cancel -> cancel_all server
in
fire server.activity ;
if server.running <> [] then
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index f17c7e4f86e..de1a942094d 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -438,7 +438,7 @@ module Make_Dataflow
let {edge_transition=transition; edge_kinstr=kinstr} = e in
let tank = get_edge_data e in
let flow = Partitioning.drain tank in
- Db.yield ();
+ Async.yield ();
check_signals ();
current_ki := kinstr;
Cil.CurrentLoc.set e.edge_loc;
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index af8c23cbca5..4060d0d5183 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -323,7 +323,7 @@ struct
~exact access state.deps_table loc deps }
let transfer_call stmt dest f args _loc state =
- Db.yield ();
+ Async.yield ();
let request = To_Use.stmt_request stmt in
let called_vinfos = Eva.Results.(eval_callee f request |> default []) in
let f_deps = Eva.Results.expr_deps f request in
@@ -424,7 +424,7 @@ struct
result
let transfer_instr stmt (i: instr) (state: t) =
- Db.yield ();
+ Async.yield ();
match i with
| Set (lv, exp, _) ->
let comp_vars = find stmt state.deps_table exp in
@@ -643,7 +643,7 @@ struct
s := !s^" <-"^(Format.asprintf "%a" Kernel_function.pretty kf))
call_stack;
!s);
- Db.yield ();
+ Async.yield ();
let result =
if Eva.Analysis.use_spec_instead_of_definition kf
then compute_using_prototype kf
@@ -652,7 +652,7 @@ struct
let result = To_Use.cleanup_and_save kf result in
From_parameters.feedback
"Done for function %a" Kernel_function.pretty kf;
- Db.yield ();
+ Async.yield ();
CurrentLoc.set call_site_loc;
result
diff --git a/src/plugins/gui/analyses_manager.ml b/src/plugins/gui/analyses_manager.ml
index df4382b5254..6bfc77e2fc3 100644
--- a/src/plugins/gui/analyses_manager.ml
+++ b/src/plugins/gui/analyses_manager.ml
@@ -68,7 +68,7 @@ let insert (main_ui: Design.main_window_extension_points) =
(Menu_manager.Unit_callback (fun () -> run_module main_ui));
Menu_manager.toolbar ~sensitive:(fun () -> !stop_sensitive) ~icon:`STOP
~label:"Stop" ~tooltip:"Stop currently running analyses"
- (Menu_manager.Unit_callback Db.cancel)
+ (Menu_manager.Unit_callback Async.cancel)
]
in
default_analyses_items.(0)#add_accelerator `CONTROL 'r';
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 588d8f05465..a86b95b86ce 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1885,7 +1885,7 @@ let make_splash () =
let toplevel play =
Gtk_helper.Configuration.load ();
- ignore (Db.on_progress Gtk_helper.refresh_gui) ;
+ ignore (Async.on_progress Gtk_helper.refresh_gui) ;
let in_idle () =
let tid, splash_out, splash_w, reparent_console, force_s= make_splash () in
let error_manager =
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 20df4ae9601..fac1f1725dc 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -788,7 +788,7 @@ class error_manager ?reset (o_parent:GWindow.window_skel) : host =
| Cmdline.Exit ->
if cancelable then Project.Undo.clear_breakpoint ();
None
- | Sys.Break | Db.Cancel ->
+ | Sys.Break | Async.Cancel ->
if cancelable then Project.Undo.restore ();
self#error ?parent ~reset:true
"Stopping current computation on user request.";
diff --git a/src/plugins/impact/compute_impact.ml b/src/plugins/impact/compute_impact.ml
index 6f78536af6a..e92cbe6a932 100644
--- a/src/plugins/impact/compute_impact.ml
+++ b/src/plugins/impact/compute_impact.ml
@@ -581,7 +581,7 @@ let rec intraprocedural wl = match pick wl with
| Some (pnode, { kf; pdg; init; zone }) ->
let node = pnode, zone in
add_to_result wl node kf init;
- Db.yield ();
+ Async.yield ();
Options.debug ~level:2 "considering new node %a in %a:@ <%a>%t"
PdgTypes.Node.pretty pnode Kernel_function.pretty kf
Pdg_aux.pretty_node node
diff --git a/src/plugins/occurrence/register.ml b/src/plugins/occurrence/register.ml
index 2f8ae1cc9d5..de26bd8c7fa 100644
--- a/src/plugins/occurrence/register.ml
+++ b/src/plugins/occurrence/register.ml
@@ -132,7 +132,7 @@ class occurrence = object (self)
DoChildren
method! vstmt_aux s =
- Db.yield ();
+ Async.yield ();
super#vstmt_aux s
initializer Eva.Analysis.compute ()
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 51196e16434..6db271d345e 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -875,7 +875,7 @@ module Computer
(** Compute the new state after 'instr' starting from state before 'state'.
*)
let doInstr stmt instr state =
- Db.yield ();
+ Async.yield ();
pdg_debug "doInstr sid:%d : %a" stmt.sid Printer.pp_instr instr;
match instr with
| _ when not (Eva.Results.is_reachable stmt) ->
@@ -884,12 +884,12 @@ module Computer
| Local_init (v, AssignInit i, _) ->
process_init current_pdg state stmt (Cil.var v) i
| Local_init (v, ConsInit (f, args, kind), loc) ->
- Db.yield ();
+ Async.yield ();
Cil.treat_constructor_as_func
(process_call current_pdg state stmt) v f args kind loc
| Set (lv, exp, _) -> process_asgn current_pdg state stmt lv exp
| Call (lvaloption,funcexp,argl,loc) ->
- Db.yield ();
+ Async.yield ();
process_call current_pdg state stmt lvaloption funcexp argl loc
| Code_annot _
| Skip _ -> process_skip current_pdg state stmt
diff --git a/src/plugins/postdominators/compute.ml b/src/plugins/postdominators/compute.ml
index c2e20b2ea2e..ab96a7e7419 100644
--- a/src/plugins/postdominators/compute.ml
+++ b/src/plugins/postdominators/compute.ml
@@ -120,7 +120,7 @@ struct
let combineSuccessors = DomSet.inter
let doStmt stmt =
- Db.yield ();
+ Async.yield ();
Postdominators_parameters.debug ~level:2 "doStmt: %d" stmt.sid;
match stmt.skind with
| Return _ -> Dataflow2.Done (DomSet.Value (Stmt.Hptset.singleton stmt))
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index 06d8471f772..9363447b71e 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -107,7 +107,7 @@ type 'a server = {
fetch : unit -> 'a message option ; (* fetch some client message *)
q_in : 'a pending Queue.t ; (* queue of pending `EXEC and `GET jobs *)
q_out : 'a response Queue.t ; (* queue of pending responses *)
- mutable daemon : Db.daemon option ; (* Db.yield daemon *)
+ mutable daemon : Async.daemon option ; (* Async.yield daemon *)
mutable s_listen : Signals.t ; (* signals the client is listening to *)
mutable s_emitted : Signals.t ; (* emitted signals enqueued *)
mutable s_pending : Signals.t ; (* emitted signals not enqueued yet *)
@@ -184,7 +184,7 @@ let execute_process server ?yield proc =
Senv.debug ~level:2 "%a" (pp_process server.pretty) proc ;
let resp = match yield with
| Some yield when proc.yield ->
- Db.with_progress
+ Async.with_progress
~debounced:server.polling
?on_delayed:(delayed proc.request)
yield run proc
@@ -231,7 +231,7 @@ let raise_if_killed = function
let kill_running ?id s =
match s.running with
| Idle -> ()
- | CmdLine -> if id = None then Db.cancel ()
+ | CmdLine -> if id = None then Async.cancel ()
| ExecRequest p ->
match id with
| None -> p.killed <- true
@@ -362,7 +362,7 @@ let rec process server =
execute_process server ~yield p
| Command cmd ->
server.running <- CmdLine ;
- Db.with_progress
+ Async.with_progress
~debounced:server.polling
?on_delayed:(delayed "<async>")
yield cmd ()
@@ -414,7 +414,7 @@ let schedule server job data =
let st =
try Task.Result (job data)
with
- | Db.Cancel -> Task.Canceled
+ | Async.Cancel -> Task.Canceled
| exn -> Task.Failed exn
in status := Task.Return st
in
@@ -455,7 +455,7 @@ let start server =
begin
Senv.feedback "Server enabled." ;
let daemon =
- Db.on_progress
+ Async.on_progress
~debounced:server.polling
?on_delayed:(delayed "command line")
(do_yield server)
@@ -480,7 +480,7 @@ let stop server =
server.daemon <- None ;
server.running <- Idle ;
server.cmdline <- None ;
- Db.off_progress daemon ;
+ Async.off_progress daemon ;
set_active false ;
end
end
@@ -493,14 +493,14 @@ let foreground server =
server.running <- Idle ;
server.cmdline <- Some false ;
emitter := do_signal server ;
- Task.on_idle := Db.while_progress ~debounced:50 ;
+ Task.on_idle := Async.while_progress ~debounced:50 ;
scheduler := Server server ;
match server.daemon with
| None -> ()
| Some daemon ->
begin
server.daemon <- None ;
- Db.off_progress daemon ;
+ Async.off_progress daemon ;
end
end
@@ -521,7 +521,7 @@ let run server =
try
while not server.shutdown do
let activity = process server in
- if not activity then Db.sleep server.polling
+ if not activity then Async.sleep server.polling
done ;
with Sys.Break -> () (* Ctr+C, just leave the loop normally *)
end;
diff --git a/src/plugins/server/main.mli b/src/plugins/server/main.mli
index 4868d732093..9215a456db5 100644
--- a/src/plugins/server/main.mli
+++ b/src/plugins/server/main.mli
@@ -94,10 +94,10 @@ val create :
(** Start the server in background.
The function returns immediately after installing a daemon that (only)
- accepts GET requests received by the server on calls to [Db.yield()].
+ accepts GET requests received by the server on calls to [Async.yield()].
Shall be scheduled at command line main stage {i via}
- [Db.Main.extend] extension point.
+ [Boot.Main.extend] extension point.
*)
val start : 'a server -> unit
@@ -114,7 +114,7 @@ val stop : 'a server -> unit
(** Run the server forever.
The server would now accept any kind of requests and start handling them.
While executing an [`EXEC] request, the server would
- continue to handle (only) [`GET] pending requests on [Db.yield()]
+ continue to handle (only) [`GET] pending requests on [Async.yield()]
at every [server.polling] time interval.
The function will {i not} return until the server is actually shutdown.
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index bb251b1e178..461d4303122 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -1164,7 +1164,7 @@ end
let rec fixpoint limit solvers sigma s0 =
if limit > 0 then compute limit solvers sigma s0 else s0
and compute limit solvers sigma s0 =
- Db.yield ();
+ Async.yield ();
let s1 =
if Wp_parameters.Ground.get () then ground s0
else s0 in
@@ -1227,7 +1227,7 @@ let tc = ref 0
let rec test_cases (s : hsp) = function
| [] -> s
| (p,_) :: tail ->
- Db.yield () ;
+ Async.yield () ;
match test_case p s , test_case (p_not p) s with
| None , None -> incr tc ; [],F.p_true
| Some w , None -> incr tc ; test_cases w tail
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index aa558367890..8eab81d8496 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1300,7 +1300,7 @@ let print_generated ?header file =
let protect e =
if debug_atleast 1 then false else
match e with
- | Sys.Break | Db.Cancel | Log.AbortError _ | Log.AbortFatal _ -> false
+ | Sys.Break | Async.Cancel | Log.AbortError _ | Log.AbortFatal _ -> false
| _ -> true
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 94995e8bb72..7dc808882fd 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -150,7 +150,7 @@ struct
let apply option phi g =
try
- Db.yield () ;
+ Async.yield () ;
Wp_parameters.debug ~dkey "Apply %s" option ;
g.sequent <- phi g.sequent ;
with exn when Wp_parameters.protect exn ->
--
GitLab