diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 8824f51b8b9c3aaaf4878bce0334ccd62b0e5f47..3878bb45f6376a737ff3be5c3030744338358c4c 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -1077,7 +1077,7 @@ let daemons = ref []
let on_progress ?(debounced=0) ?on_delayed trigger =
let d = {
trigger ;
- debounced = float debounced /. 1000.0 ;
+ debounced = float debounced *. 0.001 ;
on_delayed ;
last_yield_at = 0.0 ;
next_at = 0.0 ;
@@ -1101,53 +1101,93 @@ let warn_error exn =
let with_progress ?debounced ?on_delayed trigger job data =
let d = on_progress ?debounced ?on_delayed trigger in
let result =
- try job data with e ->
+ try job data
+ with exn ->
off_progress d ;
- raise e
+ raise exn
in
off_progress d ; result
-(* ---- Yielding ---- *)
+(* ---- Triggering ---- *)
let canceled = ref false
let cancel () = canceled := true
-let yield () =
+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 t = Unix.gettimeofday () in
- List.iter
- (fun d ->
- if t > d.next_at then
- begin
- try
- d.next_at <- t +. d.debounced ;
- d.trigger () ;
- with
- | Cancel -> canceled := true
- | exn -> warn_error exn ; raise exn
- end ;
- match d.on_delayed with
- | None ->
- ()
- | Some _ when d.last_yield_at = 0. ->
- (* first yield *)
- d.last_yield_at <- t
- | Some warn ->
- let time_since_last_yield = t -. 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)) ;
- d.last_yield_at <- t)
- ds;
- if !canceled then ( canceled := false ; raise Cancel )
+ let time = Unix.gettimeofday () in
+ List.iter (fire ~warn_on_delayed ~forced ~time) ds ;
+ raise_if_canceled () ;
end
-let flush () =
- List.iter (fun d -> d.next_at <- 0.0) !daemons ;
- yield ()
+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 ()
+
+(* ---- Deprecated old API ---- *)
let progress = ref (Kernel.deprecated "!Db.progress()" ~now:"Db.yield()" yield)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 02f3e32ba3d2f081f9416489228b92ec387cb6e0..85362586ac31164101ffc05a44234e2ad8afab16 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -1339,18 +1339,18 @@ module Derefs : INOUT with type t = Locations.Zone.t
@plugin development guide
@deprecated Frama-C+dev *)
val progress: (unit -> unit) ref
+[@@ deprecated "Use Db.yield instead."]
(** 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, in milliseconds, between two
- successive calls to the daemon (default is 0ms).
+ 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 the callback invoked as soon as the time since the last
- [yield] is greater than [debounced] milliseconds (or 100ms at least).
+ {!yield} is greater than [debounced] milliseconds (or 100ms at least).
*)
val on_progress :
?debounced:int -> ?on_delayed:(int -> unit) -> (unit -> unit) -> daemon
@@ -1361,11 +1361,13 @@ val off_progress : daemon -> unit
(** Trigger all daemons immediately. *)
val flush : unit -> unit
-(** Trigger all registered daemons (debounced). *)
+(** Trigger all registered daemons (debounced).
+ This function should be called from time to time by all analysers taking
+ time. In GUI mode, this will make the interface reactive. *)
val yield : unit -> unit
-(** Interrupt the currently running job.
- The next call to [Db.yield()] will raise a [Cancel] exception. *)
+(** Interrupt the currently running job at the next call to {!yield} as a
+ [Cancel] exception is raised. *)
val cancel : unit -> unit
(**
@@ -1389,17 +1391,22 @@ val cancel : unit -> unit
notes : (1) (2) (3)
]}
- 1. First yield, normal trigger.
-
- 2. Debounced yields leads to this second trigger.
-
- 3. Delayed warning invoked since there was no yield for more than debounced period.
+ {ol {li First yield, normal trigger.}
+ {li Debounced yields leads to this second trigger.}
+ {li Delayed warning invoked since there was no yield for more than debounced period.}}
*)
val with_progress :
?debounced:int -> ?on_delayed:(int -> unit) ->
(unit -> unit) -> ('a -> 'b) -> 'a -> 'b
-(** This exception may be raised by {!progress} to interrupt computations. *)
+(**
+ 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/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index af05488f599dbeb746a800ba05315730341010c6..4161d4533e2c87ac43997725e716c37fbaccca77 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -185,27 +185,28 @@ let monitoring = ref false
let monitored = ref false
let events : Log.event Queue.t = Queue.create ()
-let monitor flag =
+let set_monitoring flag =
if flag != !monitoring then
- ( if flag then
- Senv.feedback "Start logs monitoring."
- else
- Senv.feedback "Stop logs monitoring." ) ;
- monitoring := flag ;
+ monitoring := flag ;
if !monitoring && not !monitored then
begin
monitored := true ;
Log.add_listener (fun evt -> if !monitoring then Queue.add evt events)
end
-let monitor_logs () = monitor (Senv.Log.get ())
-
let monitor_server activity =
- if activity then monitor true else monitor_logs ()
+ if not (Senv.AutoLog.get ()) then set_monitoring activity
+
+let monitor_autologs () =
+ if Senv.AutoLog.get () then
+ begin
+ Senv.feedback "Auto-log started." ;
+ set_monitoring true ;
+ end
let () =
Main.on monitor_server ;
- Cmdline.run_after_configuring_stage monitor_logs
+ Cmdline.run_after_configuring_stage monitor_autologs
(* -------------------------------------------------------------------------- *)
(* --- Log Requests --- *)
@@ -214,7 +215,8 @@ let () =
let () = Request.register
~page ~kind:`SET ~name:"kernel.setLogs"
~descr:(Md.plain "Turn logs monitoring on/off")
- ~input:(module Jbool) ~output:(module Junit) monitor
+ ~input:(module Jbool) ~output:(module Junit)
+ set_monitoring
let () = Request.register
~page ~kind:`GET ~name:"kernel.getLogs"
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index c628ffc4c34e7ec16a7d25382b15ac7660f02130..fc42c15e056be1317b6ed6add87a493eb60e691f 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -26,7 +26,6 @@
module Senv = Server_parameters
-let option f = function None -> () | Some x -> f x
(* -------------------------------------------------------------------------- *)
(* --- Registry --- *)
@@ -77,7 +76,7 @@ type 'a message = {
(* Private API: *)
-type 'a exec = {
+type 'a process = {
id : 'a ;
request : string ;
data : json ;
@@ -87,14 +86,15 @@ type 'a exec = {
}
type 'a server = {
- yield : int ;
+ polling : int ;
pretty : Format.formatter -> 'a -> unit ;
equal : 'a -> 'a -> bool ;
fetch : unit -> 'a message option ;
- q_in : 'a exec Queue.t ;
+ q_in : 'a process Queue.t ;
q_out : 'a response Stack.t ;
+ mutable daemon : Db.daemon option ;
mutable shutdown : bool ;
- mutable running : 'a exec option ;
+ mutable running : 'a process option ;
}
exception Killed
@@ -115,6 +115,9 @@ let pp_request pp fmt (r : _ request) =
else
Format.fprintf fmt "Request %s:%a" request pp id
+let pp_process pp fmt (p : _ process) =
+ Format.fprintf fmt "Execute %s:%a" p.request pp p.id
+
let pp_response pp fmt (r : _ response) =
match r with
| `Error(id,err) -> Format.fprintf fmt "Error %a: %s" pp id err
@@ -131,31 +134,35 @@ let pp_response pp fmt (r : _ response) =
(* --- Request Handling --- *)
(* -------------------------------------------------------------------------- *)
-let execute exec : _ response =
+let run proc : _ response =
try
- let data = exec.handler exec.data in
- `Data(exec.id,data)
+ let data = proc.handler proc.data in
+ `Data(proc.id,data)
with
- | Killed -> `Killed exec.id
- | Data.InputError msg -> `Error(exec.id,msg)
+ | Killed -> `Killed proc.id
+ | Data.InputError msg -> `Error(proc.id,msg)
| Sys.Break as exn -> raise exn (* Silently pass the exception *)
| exn when Cmdline.catch_at_toplevel exn ->
Senv.warning "[%s] Uncaught exception:@\n%s"
- exec.request (Cmdline.protect exn) ;
- `Error(exec.id,Printexc.to_string exn)
-
-let execute_debug server yield exec =
- let on_delayed =
- if Senv.debug_atleast 1 then
- (Senv.debug "Trigger %s:%a" exec.request server.pretty exec.id ;
- Some (fun delay -> Senv.debug
- "No yield since %dms during %s" delay exec.request))
- else None
- in Db.with_progress ~debounced:server.yield ?on_delayed yield execute exec
-
-let reply_debug server resp =
+ proc.request (Cmdline.protect exn) ;
+ `Error(proc.id,Printexc.to_string exn)
+
+let delayed process =
if Senv.debug_atleast 1 then
- Senv.debug "%a" (pp_response server.pretty) resp ;
+ Some (fun d -> Senv.debug "No yield since %dms during %s" d process)
+ else None
+
+let execute server ?yield proc =
+ Senv.debug "%a" (pp_process server.pretty) proc ;
+ let resp = match yield with
+ | Some yield when proc.yield ->
+ Db.with_progress
+ ~debounced:server.polling
+ ?on_delayed:(delayed proc.request)
+ yield run proc
+ | _ -> run proc
+ in
+ Senv.debug "%a" (pp_response server.pretty) resp ;
Stack.push resp server.q_out
(* -------------------------------------------------------------------------- *)
@@ -173,33 +180,35 @@ let process_request (server : 'a server) (request : 'a request) : unit =
| `Poll -> ()
| `Shutdown ->
begin
- option kill_exec server.running ;
+ Extlib.may kill_exec server.running ;
Queue.clear server.q_in ;
Stack.clear server.q_out ;
server.shutdown <- true ;
end
| `Kill id ->
begin
- let kill = kill_request server.equal id in
- Queue.iter kill server.q_in ;
- option kill server.running ;
+ let set_killed = kill_request server.equal id in
+ Queue.iter set_killed server.q_in ;
+ Extlib.may set_killed server.running ;
end
| `Request(id,request,data) ->
begin
match find request with
- | None -> reply_debug server (`Rejected id)
+ | None ->
+ Senv.debug "Rejected %a" server.pretty id ;
+ Stack.push (`Rejected id) server.q_out
| Some( `GET , handler ) ->
- let exec = { id ; request ; handler ; data ;
+ let proc = { id ; request ; handler ; data ;
yield = false ; killed = false } in
- reply_debug server (execute exec)
+ execute server proc ;
| Some( `SET , handler ) ->
- let exec = { id ; request ; handler ; data ;
+ let proc = { id ; request ; handler ; data ;
yield = false ; killed = false } in
- Queue.push exec server.q_in
+ Queue.push proc server.q_in
| Some( `EXEC , handler ) ->
- let exec = { id ; request ; handler ; data ;
+ let proc = { id ; request ; handler ; data ;
yield = true ; killed = false } in
- Queue.push exec server.q_in
+ Queue.push proc server.q_in
end
(* -------------------------------------------------------------------------- *)
@@ -217,35 +226,28 @@ let communicate server =
Stack.iter (fun r -> pool := r :: !pool) server.q_out ;
Stack.clear server.q_out ;
message.callback !pool ;
- option raise error ; true
+ Extlib.may raise error ; true
(* -------------------------------------------------------------------------- *)
(* --- Yielding --- *)
(* -------------------------------------------------------------------------- *)
let do_yield server () =
- begin
- option raise_if_killed server.running ;
- ignore ( communicate server );
- end
+ Extlib.may raise_if_killed server.running ;
+ ignore ( communicate server )
(* -------------------------------------------------------------------------- *)
(* --- One Step Process --- *)
(* -------------------------------------------------------------------------- *)
-let rec fetch_exec q =
- if Queue.is_empty q then None
- else
- let e = Queue.pop q in
- if e.killed then fetch_exec q else Some e
-
let process server =
- match fetch_exec server.q_in with
- | None -> communicate server
- | Some exec ->
- server.running <- Some exec ;
+ if Queue.is_empty server.q_in then
+ communicate server
+ else
+ let proc = Queue.pop server.q_in in
+ server.running <- Some proc ;
try
- reply_debug server (execute_debug server (do_yield server) exec) ;
+ execute server ~yield:(do_yield server) proc ;
server.running <- None ;
true
with exn ->
@@ -260,42 +262,89 @@ let in_range ~min:a ~max:b v = min (max a v) b
let kill () = raise Killed
-let demons = ref []
-let on callback = demons := !demons @ [ callback ]
+let daemons = ref []
+let on callback = daemons := !daemons @ [ callback ]
let signal activity =
- List.iter (fun f -> try f activity with _ -> ()) !demons
-
-let run ~pretty ?(equal=(=)) ~fetch () =
- begin
- let yield = in_range ~min:1 ~max:200 (Senv.Yield.get ()) in
- let idle_ms = in_range ~min:1 ~max:2000 (Senv.Idle.get ()) in
- let idle = float_of_int idle_ms /. 1000.0 in
- let server = {
- fetch ; yield ; equal ; pretty ;
- q_in = Queue.create () ;
- q_out = Stack.create () ;
- running = None ;
- shutdown = false ;
- } in
- try
- (* TODO: remove the following line once the Why3 signal handler is not
- used anymore. *)
- Sys.catch_break true;
+ List.iter (fun f -> try f activity with _ -> ()) !daemons
+
+let create ~pretty ?(equal=(=)) ~fetch () =
+ let polling = in_range ~min:1 ~max:200 (Senv.Polling.get ()) in
+ {
+ fetch ; polling ; equal ; pretty ;
+ q_in = Queue.create () ;
+ q_out = Stack.create () ;
+ daemon = None ;
+ running = None ;
+ shutdown = false ;
+ }
+
+(* -------------------------------------------------------------------------- *)
+(* --- Start / Stop --- *)
+(* -------------------------------------------------------------------------- *)
+
+let start server =
+ match server.daemon with
+ | Some _ -> ()
+ | None ->
+ begin
+ Senv.feedback "Server enabled." ;
+ let daemon =
+ Db.on_progress
+ ~debounced:server.polling
+ ?on_delayed:(delayed "command line")
+ (do_yield server)
+ in
+ server.daemon <- Some daemon ;
signal true ;
- Senv.feedback "Server running." ;
- begin try
- while not server.shutdown do
- let activity = process server in
- if not activity then Unix.sleepf idle ;
- done ;
- with Sys.Break -> () (* Ctr+C, just leave the loop normally *)
- end;
- Senv.feedback "Server shutdown." ;
- signal false ;
- with exn ->
- Senv.feedback "Server interruped (fatal error)." ;
+ end
+
+let stop server =
+ match server.daemon with
+ | None -> ()
+ | Some daemon ->
+ begin
+ Senv.feedback "Server disabled." ;
+ server.daemon <- None ;
+ Db.off_progress daemon ;
signal false ;
- raise exn
- end
+ end
+
+let foreground server =
+ match server.daemon with
+ | None -> ()
+ | Some daemon ->
+ begin
+ server.daemon <- None ;
+ Db.off_progress daemon ;
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Main Loop --- *)
+(* -------------------------------------------------------------------------- *)
+
+let run server =
+ try
+ ( (* TODO: catch-break to be removed once Why3 signal handler is fixed *)
+ Sys.catch_break true
+ ) ;
+ Senv.feedback "Server running." ;
+ foreground server ;
+ signal true ;
+ begin
+ try
+ while not server.shutdown do
+ let activity = process server in
+ if not activity then Db.sleep server.polling
+ done ;
+ with Sys.Break -> () (* Ctr+C, just leave the loop normally *)
+ end;
+ Senv.feedback "Server shutdown." ;
+ signal false ;
+ with
+ | Killed -> ()
+ | exn ->
+ Senv.feedback "Server interruped (fatal error)." ;
+ signal false ;
+ raise exn
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/main.mli b/src/plugins/server/main.mli
index 75d51a0d17af477241683a5ccdc2c5915210dfe3..acd7ef46c6b7030dc51c34cc2b0c187852f00768 100644
--- a/src/plugins/server/main.mli
+++ b/src/plugins/server/main.mli
@@ -66,6 +66,8 @@ type 'a message = {
callback : 'a response list -> unit ;
}
+type 'a server
+
(**
Run a server with the provided low-level network primitives to
actually exchange data.
@@ -75,11 +77,25 @@ type 'a message = {
Default equality is the standard `(=)` one.
*)
-val run :
+val create :
pretty:(Format.formatter -> 'a -> unit) ->
?equal:('a -> 'a -> bool) ->
fetch:(unit -> 'a message option) ->
- unit -> unit
+ unit -> 'a server
+
+(** Run the server forever.
+ The function will not return until the server is shut down. *)
+val run : 'a server -> unit
+
+(** Start the server in background.
+ The function returns immediately
+ after installing a daemon that accepts GET requests received by
+ the server on calls to `Db.yield()`.
+*)
+val start : 'a server -> unit
+
+(** Stop the server if it is running in background. *)
+val stop : 'a server -> unit
(** Kills the currently running request. Actually raises an exception. *)
val kill : unit -> 'a
diff --git a/src/plugins/server/server_parameters.ml b/src/plugins/server/server_parameters.ml
index 57dbdd133f9f088015fe82df6ea19932565b883f..5b9e0018622e06add5fcf012e2bdc76d0d0d92cc 100644
--- a/src/plugins/server/server_parameters.ml
+++ b/src/plugins/server/server_parameters.ml
@@ -33,22 +33,33 @@ module P = Plugin.Register
include P
-module Idle = P.Int
+(* -------------------------------------------------------------------------- *)
+(* --- Server General Options --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Polling = P.Int
(struct
- let option_name = "-server-idle"
+ let option_name = "-server-polling"
let arg_name = "ms"
- let default = 20
- let help = "Waiting time (in milliseconds) when idle"
+ let default = 50
+ let help = "Server polling time period, in milliseconds (default 50ms)"
end)
-module Yield = P.Int
+module AutoLog = P.False
(struct
- let option_name = "-server-yield"
- let arg_name = "ms"
- let default = 20
- let help = "Yielding time (in milliseconds) during computations"
+ let option_name = "-server-auto-log"
+ let help =
+ "Start monitoring logs before server is running (default is false)"
end)
+(* -------------------------------------------------------------------------- *)
+(* --- Doc Options --- *)
+(* -------------------------------------------------------------------------- *)
+
+let server_doc = add_group "Server Doc Generation"
+let () = Parameter_customize.set_group server_doc
+let () = Parameter_customize.do_not_save ()
+
module Doc = P.String
(struct
let option_name = "-server-doc"
@@ -57,12 +68,6 @@ module Doc = P.String
let help = "Output a markdown documentation of the server in <dir>"
end)
-module Log = P.False
- (struct
- let option_name = "-server-logs"
- let help = "Start (or stop) monitoring logs"
- end)
-
let wpage = register_warn_category "inconsistent-page"
let wkind = register_warn_category "inconsistent-kind"
let wname = register_warn_category "invalid-name"
diff --git a/src/plugins/server/server_parameters.mli b/src/plugins/server/server_parameters.mli
index 9bbd8a148fde84d797559b9675f44098c42e59c7..33406edeb1db315f587b0a26ec136b006c6af303 100644
--- a/src/plugins/server/server_parameters.mli
+++ b/src/plugins/server/server_parameters.mli
@@ -24,10 +24,9 @@
include Plugin.General_services
-module Idle : Parameter_sig.Int (** Idle waiting time (in ms) *)
-module Yield : Parameter_sig.Int (** Yield time (in ms) *)
module Doc : Parameter_sig.String (** Generate documentation *)
-module Log : Parameter_sig.Bool (** Monitor logs *)
+module Polling : Parameter_sig.Int (** Idle waiting time (in ms) *)
+module AutoLog : Parameter_sig.Bool (** Monitor logs *)
val wpage : warn_category (** Inconsistent page warning *)
val wkind : warn_category (** Inconsistent category warning *)
diff --git a/src/plugins/server/server_zmq.ml b/src/plugins/server/server_zmq.ml
index 82d2ce4316762eb1f638f499c928eb15000d2442..b9bc13013539919685dfac227d8039d37869180e 100644
--- a/src/plugins/server/server_zmq.ml
+++ b/src/plugins/server/server_zmq.ml
@@ -32,12 +32,30 @@ module Senv = Server_parameters
let zmq_group = Senv.add_group "Protocol ZeroMQ"
let () = Parameter_customize.set_group zmq_group
-module Enabled = Senv.String
+module Socket = Senv.String
(struct
let option_name = "-server-zmq"
let arg_name = "url"
let default = ""
- let help = "Establish a ZeroMQ server and listen for connections"
+ let help =
+ "Launch the ZeroMQ server (in background).\n\
+ The server can handle GET requests during the\n\
+ execution of the frama-c command line.\n\
+ Finally, the server is executed until shutdown."
+ end)
+
+let () = Parameter_customize.set_group zmq_group
+module Client = Senv.String
+ (struct
+ let option_name = "-server-gui"
+ let arg_name = "cmd"
+ let default = ""
+ let help =
+ "Launch the ZeroMQ client (as a child process).\n\
+ If not started by -server-zmq <url>, the ZeroMQ server\n\
+ is established with a local 'ipc://<tmp>' address.\n\
+ The specified <cmd> is passed the actual server <url>\n\
+ as first and unique argument."
end)
let _ = Doc.page `Protocol ~title:"ZeroMQ Protocol" ~filename:"server_zmq.md"
@@ -46,14 +64,14 @@ let _ = Doc.page `Protocol ~title:"ZeroMQ Protocol" ~filename:"server_zmq.md"
(* --- ZMQ Context --- *)
(* -------------------------------------------------------------------------- *)
-let context =
+let zmq_context =
let zmq = ref None in
fun () ->
match !zmq with
| Some ctxt -> ctxt
| None ->
let major,minor,patch = Zmq.version () in
- Senv.feedback "ZeroMQ %d.%d.%d" major minor patch ;
+ Senv.debug "ZeroMQ [v%d.%d.%d]" major minor patch ;
let ctxt = Zmq.Context.create () in
at_exit (fun () -> Zmq.Context.terminate ctxt) ;
zmq := Some ctxt ; ctxt
@@ -117,25 +135,78 @@ let fetch socket () =
(* --- Establish the Server --- *)
(* -------------------------------------------------------------------------- *)
-let establish url =
- if url <> "" then
- begin
- let context = context () in
- let socket = Zmq.Socket.(create context rep) in
- try
- Zmq.Socket.bind socket url ;
- Senv.feedback "ZeroMQ [%s]" url ;
- Main.run ~pretty:Format.pp_print_string ~fetch:(fetch socket) () ;
- Zmq.Socket.close socket ;
- with exn ->
+let pretty = Format.pp_print_string
+let server = ref None
+let client = ref None
+
+let ping () =
+ match !client with None -> None | Some process ->
+ try Some (process ())
+ with Unix.Unix_error _ -> None
+
+let launch_server url =
+ match !server with
+ | Some _ -> ()
+ | None ->
+ let context = zmq_context () in
+ let socket = Zmq.Socket.(create context rep) in
+ try
+ Zmq.Socket.bind socket url ;
+ Senv.debug "ZeroMQ [%s]" url ;
+ let srv = Main.create ~pretty ~fetch:(fetch socket) () in
+ server := Some(url,srv) ;
+ Extlib.safe_at_exit begin fun () ->
+ Main.stop srv ;
Zmq.Socket.close socket ;
- raise exn
+ server := None ;
+ end ;
+ Main.start srv ;
+ Cmdline.at_normal_exit (fun () -> Main.run srv) ;
+ with exn ->
+ Zmq.Socket.close socket ;
+ raise exn
+
+let temp_url () =
+ let socket = Filename.temp_file "frama-c.socket" ".io" in
+ Extlib.safe_at_exit (fun () -> Extlib.safe_remove socket) ;
+ "ipc://" ^ socket
+
+let start_server () =
+ match !server with
+ | None ->
+ let socket = Socket.get () in
+ let url = if socket = "" then temp_url () else socket in
+ launch_server url ; url
+ | Some (url,_) -> url
+
+let launch_client cmd =
+ match !client with
+ | Some _ -> ()
+ | None ->
+ begin
+ let url = start_server () in
+ let process = Command.command_async cmd [| url |] in
+ Senv.debug "%s --connect %s@." cmd url ;
+ Senv.feedback "Client launched." ;
+ client := Some process ;
+ Extlib.safe_at_exit
+ begin fun () ->
+ match ping () with
+ | Some (Not_ready kill) ->
+ Senv.feedback "Client interrupted." ;
+ kill ()
+ | _ -> ()
+ end ;
end
-(* -------------------------------------------------------------------------- *)
-(* --- Establish the Server from Command line --- *)
-(* -------------------------------------------------------------------------- *)
+let cmdline () =
+ begin
+ let url = Socket.get () in
+ if url <> "" then launch_server url ;
+ let cmd = Client.get () in
+ if cmd <> "" then launch_client cmd ;
+ end
-let () = Db.Main.extend (fun () -> establish (Enabled.get ()))
+let () = Db.Main.extend cmdline
(* -------------------------------------------------------------------------- *)