From b237c7eecd221ddbd25c80eee9aaa0a5feb2c7f8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 27 Jan 2020 14:22:28 +0100
Subject: [PATCH] [kernel] deprecates Db.progress
---
src/kernel_services/plugin_entry_points/db.ml | 4 ---
src/libraries/utils/command.ml | 4 +--
src/libraries/utils/task.ml | 6 ++--
src/plugins/from/from_compute.ml | 8 ++---
src/plugins/gui/analyses_manager.ml | 13 ++------
src/plugins/gui/design.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 | 33 +------------------
src/plugins/server/main.mli | 4 ---
src/plugins/value/engine/iterator.ml | 2 +-
src/plugins/wp/Conditions.ml | 4 +--
src/plugins/wp/calculus.ml | 2 +-
src/plugins/wp/cil2cfg.ml | 8 ++---
16 files changed, 27 insertions(+), 75 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 9c2d3d155bb..bf1eb6ce502 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -1109,11 +1109,7 @@ let flush () =
List.iter (fun d -> d.next_at <- 0.0) !daemons ;
yield ()
-(*
let progress = ref (Kernel.deprecated "!Db.progress()" ~now:"Db.yield()" yield)
-*)
-
-let progress = ref yield
exception Cancel
let cancel () = raise Cancel
diff --git a/src/libraries/utils/command.ml b/src/libraries/utils/command.ml
index f11b1065d5e..14bedfcb05c 100644
--- a/src/libraries/utils/command.ml
+++ b/src/libraries/utils/command.ml
@@ -45,7 +45,7 @@ let pp_from_file fmt file =
let cin = open_in file in
try
while true do
- !Db.progress () ;
+ Db.yield () ;
let line = input_line cin in
Format.pp_print_string fmt line ;
Format.pp_print_newline fmt () ;
@@ -248,7 +248,7 @@ let command ?(timeout=0) ?stdout ?stderr cmd args =
| Not_ready terminate ->
begin
try
- !Db.progress () ;
+ Db.yield () ;
if timeout > 0 && Unix.gettimeofday () -. !start > ftimeout then
raise Db.Cancel ;
true
diff --git a/src/libraries/utils/task.ml b/src/libraries/utils/task.ml
index 7750a6c5c9a..be822879c38 100644
--- a/src/libraries/utils/task.ml
+++ b/src/libraries/utils/task.ml
@@ -108,8 +108,8 @@ struct
let rec wait = function
| UNIT a -> a
- | YIELD f -> !Db.progress() ; wait (f Coin)
- | WAIT(ms,f) -> !Db.progress() ; Extlib.usleep ms ; wait (f Coin)
+ | YIELD f -> Db.yield() ; wait (f Coin)
+ | WAIT(ms,f) -> Db.yield() ; Extlib.usleep ms ; wait (f Coin)
let finished = function UNIT a -> Some a | YIELD _ | WAIT _ -> None
@@ -479,7 +479,7 @@ let rec run_server server () =
) server.running ;
Array.iter (schedule server) server.queue ;
try
- !Db.progress () ;
+ Db.yield ();
fire server.activity ;
if server.running <> [] then
begin
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index ea103a92baa..87c04563112 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -353,7 +353,7 @@ struct
~exact access state.deps_table loc deps }
let transfer_call stmt dest f args _loc state =
- !Db.progress ();
+ Db.yield ();
let value_state = To_Use.get_value_state stmt in
let f_deps, called_vinfos =
!Db.Value.expr_to_kernel_function_state
@@ -456,7 +456,7 @@ struct
result
let transfer_instr stmt (i: instr) (state: t) =
- !Db.progress ();
+ Db.yield ();
match i with
| Set (lv, exp, _) ->
let comp_vars = find stmt state.deps_table exp in
@@ -688,7 +688,7 @@ struct
s := !s^" <-"^(Format.asprintf "%a" Kernel_function.pretty kf))
call_stack;
!s);
- !Db.progress ();
+ Db.yield ();
let result =
if !Db.Value.use_spec_instead_of_definition kf
then compute_using_prototype kf
@@ -697,7 +697,7 @@ struct
let result = To_Use.cleanup_and_save kf result in
From_parameters.feedback
"Done for function %a" Kernel_function.pretty kf;
- !Db.progress ();
+ Db.yield ();
CurrentLoc.set call_site_loc;
result
diff --git a/src/plugins/gui/analyses_manager.ml b/src/plugins/gui/analyses_manager.ml
index 787a26083c2..87b43c2355f 100644
--- a/src/plugins/gui/analyses_manager.ml
+++ b/src/plugins/gui/analyses_manager.ml
@@ -57,7 +57,7 @@ let run_module =
let insert (main_ui: Design.main_window_extension_points) =
let menu_manager = main_ui#menu_manager () in
- let stop = ref (fun () -> assert false) (* delayed *) in
+ let stop () = Db.once Db.cancel in
let stop_sensitive = ref false (* can the stop button be clicked? *) in
let default_analyses_items =
menu_manager#add_plugin
@@ -69,31 +69,22 @@ 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 (fun () -> !stop ()));
+ (Menu_manager.Unit_callback stop)
]
in
default_analyses_items.(0)#add_accelerator `CONTROL 'r';
let stop_button = Extlib.the default_analyses_items.(2)#tool_button in
- let old_progress = ref !Db.progress in
- stop :=
- (fun () ->
- Db.progress :=
- (fun () ->
- Db.progress := !old_progress;
- raise Db.Cancel));
Gtk_helper.register_locking_machinery
~lock_last:true
~lock:(fun cancelable ->
if !stop_sensitive then Gui_parameters.warning
"Inconsistent state for stop button. Ignoring.";
- old_progress := !Db.progress;
menu_manager#set_sensitive false;
if cancelable then (stop_button#misc#set_sensitive true;
stop_sensitive := true);
)
~unlock:(fun () ->
- Db.progress := !old_progress;
menu_manager#set_sensitive true;
stop_button#misc#set_sensitive false;
stop_sensitive := false;
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 4cf526308c2..4b926e21ca0 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1845,7 +1845,7 @@ let make_splash () =
let toplevel play =
Gtk_helper.Configuration.load ();
- Db.progress := Gtk_helper.refresh_gui;
+ ignore (Db.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/impact/compute_impact.ml b/src/plugins/impact/compute_impact.ml
index 9755c2489b7..9bb6b38920a 100644
--- a/src/plugins/impact/compute_impact.ml
+++ b/src/plugins/impact/compute_impact.ml
@@ -577,7 +577,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.progress ();
+ Db.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 2842ba46739..d2aca0a1c8e 100644
--- a/src/plugins/occurrence/register.ml
+++ b/src/plugins/occurrence/register.ml
@@ -135,7 +135,7 @@ class occurrence = object (self)
DoChildren
method! vstmt_aux s =
- !Db.progress ();
+ Db.yield ();
super#vstmt_aux s
initializer !Db.Value.compute ()
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 8d0c5ba63a3..8fbfb29d894 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -863,7 +863,7 @@ module Computer
(** Compute the new state after 'instr' starting from state before 'state'.
*)
let doInstr stmt instr state =
- !Db.progress ();
+ Db.yield ();
pdg_debug "doInstr sid:%d : %a" stmt.sid Printer.pp_instr instr;
match instr with
| _ when not (Db.Value.is_reachable_stmt stmt) ->
@@ -872,12 +872,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.progress ();
+ Db.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.progress ();
+ Db.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 f766ae37ba1..1e65b7b9b83 100644
--- a/src/plugins/postdominators/compute.ml
+++ b/src/plugins/postdominators/compute.ml
@@ -118,7 +118,7 @@ struct
let combineSuccessors = DomSet.inter
let doStmt stmt =
- !Db.progress ();
+ Db.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 9d0e1f4dff6..c66c94f455a 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -132,8 +132,6 @@ let pp_response pp fmt (r : _ response) =
(* --- Request Handling --- *)
(* -------------------------------------------------------------------------- *)
-let no_yield () = ()
-
let execute exec : _ response =
try
let data = exec.handler exec.data in
@@ -147,38 +145,10 @@ let execute exec : _ response =
exec.request (Cmdline.protect exn) ;
`Error(exec.id,Printexc.to_string exn)
-let acceptable_between_yield = 0.25 (* seconds *)
-
-let execute_with_yield yield exec =
- let db = !Db.progress in
- let yield, check =
- if Senv.debug_atleast 1 then
- let time = ref (Unix.gettimeofday ()) in
- let check () =
- let time' = Unix.gettimeofday () in
- let diff = time' -. !time in
- if diff > acceptable_between_yield
- then
- Senv.debug
- "Db.progress missing during %s request (spent %fs between calls)"
- exec.request
- diff
- in
- (fun () ->
- check ();
- yield ();
- time := Unix.gettimeofday ()),
- check
- else
- yield, ignore
- in
- Db.progress := if exec.yield then yield else no_yield;
- Extlib.try_finally ~finally:(fun () -> Db.progress := db; check ()) execute exec
-
let execute_debug pp yield exec =
if Senv.debug_atleast 1 then
Senv.debug "Trigger %s:%a" exec.request pp exec.id ;
- execute_with_yield yield exec
+ Db.with_progress yield execute exec
let reply_debug server resp =
if Senv.debug_atleast 1 then
@@ -290,7 +260,6 @@ let process server =
let in_range ~min:a ~max:b v = min (max a v) b
let kill () = raise Killed
-let yield () = !Db.progress ()
let demons = ref []
let on callback = demons := !demons @ [ callback ]
diff --git a/src/plugins/server/main.mli b/src/plugins/server/main.mli
index 721291d96e9..75d51a0d17a 100644
--- a/src/plugins/server/main.mli
+++ b/src/plugins/server/main.mli
@@ -81,10 +81,6 @@ val run :
fetch:(unit -> 'a message option) ->
unit -> unit
-(** Yield the server during the currently running request.
- Actually, calls [!Db.progress()]. *)
-val yield : unit -> unit
-
(** Kills the currently running request. Actually raises an exception. *)
val kill : unit -> 'a
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index b0ac5fda287..660b178d718 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -420,7 +420,7 @@ module Make_Dataflow
let {edge_transition=transition; edge_kinstr=kinstr} = e in
let tank,edge_info = get_edge_data e in
let flow = Partition.drain tank in
- !Db.progress ();
+ Db.yield ();
check_signals ();
current_ki := kinstr;
Cil.CurrentLoc.set e.edge_loc;
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index f203b8b5cd7..021ef13b877 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -1095,7 +1095,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.progress ();
+ Db.yield ();
let s1 =
if Wp_parameters.Ground.get () then ground s0
else s0 in
@@ -1158,7 +1158,7 @@ let tc = ref 0
let rec test_cases (s : hsp) = function
| [] -> s
| (p,_) :: tail ->
- !Db.progress () ;
+ Db.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/calculus.ml b/src/plugins/wp/calculus.ml
index 8f5b282c90d..e6d6bf8cdd9 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -500,7 +500,7 @@ module Cfg (W : Mcfg.S) = struct
(** @return the WP stored for edge [e]. Compute it if it is not already
* there and store it. Also handle the Acut annotations. *)
let rec get_wp_edge ((_kf, cfg, strategy, res, wenv) as env) e =
- !Db.progress ();
+ Db.yield ();
let v = Cil2cfg.edge_dst e in
debug "[get_wp_edge] get wp before %a@." Cil2cfg.pp_node v;
try
diff --git a/src/plugins/wp/cil2cfg.ml b/src/plugins/wp/cil2cfg.ml
index 3129f581006..e295b76eb7e 100644
--- a/src/plugins/wp/cil2cfg.ml
+++ b/src/plugins/wp/cil2cfg.ml
@@ -853,7 +853,7 @@ and cfg_switch env switch_stmt switch_exp blk case_stmts next =
n_switch
and cfg_stmt env s next =
- !Db.progress ();
+ Db.yield ();
match s.skind with
| Instr (Call (_, f, _, _)) ->
setup_preconditions_proxies f;
@@ -1220,11 +1220,11 @@ let cfg_from_definition kf f =
kf_name (CFG.nb_edges graph) (CFG.nb_vertex graph);
debug
"start removing unreachable in %s@." kf_name;
- !Db.progress ();
+ Db.yield ();
let cfg = clean_graph cfg in
debug "for function '%s': %d vertex - %d edges@."
kf_name (CFG.nb_edges graph) (CFG.nb_vertex graph);
- !Db.progress ();
+ Db.yield ();
debug
"start loop analysis for %s@." kf_name;
let cfg = mark_loops cfg in
@@ -1249,7 +1249,7 @@ let create kf =
with Kernel_function.No_Definition ->
cfg_from_proto kf
in debug "done for %s@." kf_name;
- !Db.progress ();
+ Db.yield ();
cfg
module KfCfg =
--
GitLab