diff --git a/ivette/src/frama-c/client.ts b/ivette/src/frama-c/client.ts
index 0398a92fcb28ac2ca8b61d8ff00a00d0141e059c..ae1acb242e98e7f18c14e371fdb9aeebf8bf1794 100644
--- a/ivette/src/frama-c/client.ts
+++ b/ivette/src/frama-c/client.ts
@@ -44,7 +44,7 @@ export abstract class Client {
/** Signal ON */
abstract sigOn(id: string): void;
- /** Signal ON */
+ /** Signal OFF */
abstract sigOff(id: string): void;
/** Kill Request */
@@ -143,6 +143,20 @@ export abstract class Client {
this.events.emit('CONNECT', err);
}
+ // --------------------------------------------------------------------------
+ // --- CMDLINE Event
+ // --------------------------------------------------------------------------
+
+ /** Signal callback */
+ onCmdLine(callback: (cmd: boolean) => void): void {
+ this.events.on('CMDLINE', callback);
+ }
+
+ /** @internal */
+ emitCmdLine(cmd: boolean): void {
+ this.events.emit('CMDLINE', cmd);
+ }
+
}
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/client_socket.ts b/ivette/src/frama-c/client_socket.ts
index d8360cf31fda671bd4522387ff558273f71d1e35..4f6d62223cc1c431cc6019c41bde1bdf6719ebae 100644
--- a/ivette/src/frama-c/client_socket.ts
+++ b/ivette/src/frama-c/client_socket.ts
@@ -27,7 +27,7 @@ import { Client } from './client';
const D = new Debug('SocketServer');
-const RETRIES = 10;
+const RETRIES = 30;
const TIMEOUT = 200;
// --------------------------------------------------------------------------
@@ -193,8 +193,14 @@ class SocketClient extends Client {
default:
D.warn('Unknown command', cmd);
}
- } else
- D.warn('Misformed data', data);
+ } else {
+ switch (cmd) {
+ case 'CMDLINEON': this.emitCmdLine(true); break;
+ case 'CMDLINEOFF': this.emitCmdLine(false); break;
+ default:
+ D.warn('Misformed data', data);
+ }
+ }
} catch (err) {
D.warn('Misformed JSON', data, err);
}
diff --git a/ivette/src/frama-c/client_zmq.ts b/ivette/src/frama-c/client_zmq.ts
index 45be4a2c04832c2079a0973c19bee13c8e0d8793..e66610de46cc555c1c555555398bd747303a7ad6 100644
--- a/ivette/src/frama-c/client_zmq.ts
+++ b/ivette/src/frama-c/client_zmq.ts
@@ -190,6 +190,12 @@ class ZmqClient extends Client {
D.error(`ZMQ Protocol Error: ${err}`);
}
break;
+ case 'CMDLINEON':
+ this.emitCmdLine(true);
+ break;
+ case 'CMDLINEOFF':
+ this.emitCmdLine(false);
+ break;
default:
D.error(`Unknown Response: ${cmd}`);
return;
diff --git a/ivette/src/frama-c/server.ts b/ivette/src/frama-c/server.ts
index 8906457a68102a451c932b45eb023dad1c1cc71d..a621798462c09a889bdb455af074f4205445c2bb 100644
--- a/ivette/src/frama-c/server.ts
+++ b/ivette/src/frama-c/server.ts
@@ -50,8 +50,10 @@ export enum Status {
OFF = 'OFF',
/** Server is starting, but not on yet. */
STARTING = 'STARTING',
- /** Server is on. */
+ /** Server is running. */
ON = 'ON',
+ /** Server is running command line. */
+ CMD = 'CMD',
/** Server is halting, but not off yet. */
HALTING = 'HALTING',
/** Server is restarting. */
@@ -76,7 +78,7 @@ const STATUS = new Dome.Event<Status>('frama-c.server.status');
/**
* Server is actually started and running.
- * This event is emitted when ther server _enters_ the `ON` state.
+ * This event is emitted when ther server _enters_ the `ON` or `CMD` state.
* The server is now ready to handle requests.
*/
const READY = new Dome.Event('frama-c.server.ready');
@@ -84,7 +86,7 @@ const READY = new Dome.Event('frama-c.server.ready');
/**
* Server Status Notification Event
- * This event is emitted when ther server _leaves_ the `ON` state.
+ * This event is emitted when ther server _leaves_ the `ON` or `CMD` state.
* The server is no more able to handle requests until restart.
*/
const SHUTDOWN = new Dome.Event('frama-c.server.shutdown');
@@ -121,7 +123,7 @@ const pending = new Map<string, PendingRequest>();
let process: ChildProcess | undefined;
/** Polling timeout when server is busy. */
-const pollingTimeout = 200;
+const pollingTimeout = 50;
let pollingTimer: NodeJS.Timeout | undefined;
/** Killing timeout and timer for server process hard kill. */
@@ -154,11 +156,17 @@ export function useStatus(): Status {
return status;
}
+const running = (st: Status): boolean =>
+ (st === Status.ON || st === Status.CMD);
+
/**
* Whether the server is running and ready to handle requests.
- * @return {boolean} Whether server stage is [[ON]].
+ * @return {boolean} Whether server is in running stage,
+ * defined by status `ON` or `CMD`.
*/
-export function isRunning(): boolean { return status === Status.ON; }
+export function isRunning(): boolean {
+ return running(status);
+}
/**
* Number of requests still pending.
@@ -170,7 +178,7 @@ export function getPending(): number {
/**
* Register callback on `READY` event.
- * @param {function} callback Invoked when the server enters [[ON]] stage.
+ * @param {function} callback Invoked when the server enters running stage.
*/
export function onReady(callback: () => void): void {
READY.on(callback);
@@ -178,7 +186,7 @@ export function onReady(callback: () => void): void {
/**
* Register callback on `SHUTDOWN` event.
- * @param {function} callback Invoked when the server leaves [[ON]] stage.
+ * @param {function} callback Invoked when the server leaves running stage.
*/
export function onShutdown(callback: () => void): void {
SHUTDOWN.on(callback);
@@ -193,11 +201,15 @@ function _status(newStatus: Status): void {
const oldStatus = status;
status = newStatus;
STATUS.emit(newStatus);
- if (oldStatus === Status.ON) SHUTDOWN.emit();
- if (newStatus === Status.ON) READY.emit();
+ const oldRun = running(oldStatus);
+ const newRun = running(newStatus);
+ if (oldRun && !newRun) SHUTDOWN.emit();
+ if (!oldRun && newRun) READY.emit();
}
}
+const _update: () => void = debounce(() => STATUS.emit(status), 100);
+
// --------------------------------------------------------------------------
// --- Server Control (Start)
// --------------------------------------------------------------------------
@@ -226,6 +238,7 @@ export async function start(): Promise<void> {
_status(Status.RESTARTING);
return;
case Status.ON:
+ case Status.CMD:
case Status.STARTING:
return;
default:
@@ -252,6 +265,7 @@ export function stop(): void {
_kill();
return;
case Status.ON:
+ case Status.CMD:
case Status.HALTING:
_status(Status.HALTING);
_shutdown();
@@ -283,6 +297,7 @@ export function stop(): void {
export function kill(): void {
switch (status) {
case Status.ON:
+ case Status.CMD:
case Status.HALTING:
case Status.STARTING:
case Status.RESTARTING:
@@ -318,6 +333,7 @@ export function restart(): void {
start();
return;
case Status.ON:
+ case Status.CMD:
_status(Status.RESTARTING);
_shutdown();
return;
@@ -477,6 +493,26 @@ async function _launch(): Promise<void> {
client.connect(sockaddr);
}
+// --------------------------------------------------------------------------
+// --- Polling Management
+// --------------------------------------------------------------------------
+
+function _startPolling(): void {
+ if (!pollingTimer) {
+ const polling = (config && config.polling) || pollingTimeout;
+ pollingTimer = setInterval(() => {
+ client.poll();
+ }, polling);
+ }
+}
+
+function _stopPolling(): void {
+ if (pollingTimer) {
+ clearInterval(pollingTimer);
+ pollingTimer = undefined;
+ }
+}
+
// --------------------------------------------------------------------------
// --- Low-level Killing
// --------------------------------------------------------------------------
@@ -485,10 +521,7 @@ function _clear(): void {
rqCount = 0;
pending.forEach((p: PendingRequest) => p.reject('clear'));
pending.clear();
- if (pollingTimer) {
- clearTimeout(pollingTimer);
- pollingTimer = undefined;
- }
+ _stopPolling();
if (killingTimer) {
clearTimeout(killingTimer);
killingTimer = undefined;
@@ -732,12 +765,8 @@ export function send<In, Out>(
});
response.kill = () => pending.get(rid)?.reject('kill');
client.send(request.kind, rid, request.name, param as unknown as Json.json);
- if (!pollingTimer) {
- const polling = (config && config.polling) || pollingTimeout;
- pollingTimer = setInterval(() => {
- client.poll();
- }, polling);
- }
+ _startPolling();
+ _update();
return response;
}
@@ -747,20 +776,20 @@ export function send<In, Out>(
function _resolved(id: string): void {
pending.delete(id);
- if (pending.size === 0) {
+ if (pending.size === 0 && status === Status.ON) {
rqCount = 0;
- if (pollingTimer) {
- clearInterval(pollingTimer);
- pollingTimer = undefined;
- }
+ _stopPolling();
+ _update();
}
}
client.onConnect((err?: Error) => {
if (err) {
_status(Status.FAILURE);
+ _clear();
} else {
- _status(Status.ON);
+ _status(Status.CMD);
+ _startPolling();
}
});
@@ -800,4 +829,14 @@ client.onSignal((id: string) => {
_signal(id).emit();
});
+client.onCmdLine((cmd: boolean) => {
+ _status(cmd ? Status.CMD : Status.ON);
+ if (cmd)
+ _startPolling();
+ else {
+ if (pending.size === 0)
+ _stopPolling();
+ }
+});
+
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index 8c62b47cb54da7b22daf6334d739063e3ab3574a..ff7b0310ffc622958094a9f668b70a6edcf18bbb 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -304,6 +304,7 @@ class SyncState<A> {
`Fail to set value of SyncState '${this.handler.name}'.`,
`${error}`,
);
+ this.UPDATE.emit();
}
}
@@ -311,16 +312,18 @@ class SyncState<A> {
try {
this.upToDate = true;
this.value = undefined;
+ this.UPDATE.emit();
if (Server.isRunning()) {
const v = await Server.send(this.handler.getter, null);
this.value = v;
+ this.UPDATE.emit();
}
- this.UPDATE.emit();
} catch (error) {
D.error(
`Fail to update SyncState '${this.handler.name}'.`,
`${error}`,
);
+ this.UPDATE.emit();
}
}
}
diff --git a/ivette/src/renderer/Controller.tsx b/ivette/src/renderer/Controller.tsx
index 3cd1379e16540683b05593d2c40404040e45e1db..996c3c0878b8d1b8ae46831698fb6e446c77c0ce 100644
--- a/ivette/src/renderer/Controller.tsx
+++ b/ivette/src/renderer/Controller.tsx
@@ -160,6 +160,7 @@ export const Control = () => {
play = { enabled: true, onClick: Server.start };
break;
case Server.Status.ON:
+ case Server.Status.CMD:
case Server.Status.FAILURE:
stop = { enabled: true, onClick: Server.stop };
reload = { enabled: true, onClick: Server.restart };
@@ -372,36 +373,50 @@ export const Status = () => {
const status = Server.useStatus();
const pending = Server.getPending();
let led: LEDstatus = 'inactive';
+ let title = undefined;
let icon = undefined;
let running = 'OFF';
let blink = false;
switch (status) {
case Server.Status.OFF:
+ title = 'Server is off';
break;
case Server.Status.STARTING:
led = 'active';
blink = true;
running = 'BOOT';
+ title = 'Server is starting';
break;
case Server.Status.ON:
- led = pending > 0 ? 'positive' : 'active';
+ led = 'active';
+ blink = pending > 0;
running = 'ON';
+ title = 'Server is running';
+ break;
+ case Server.Status.CMD:
+ led = 'positive';
+ blink = true;
+ running = 'CMD';
+ title = 'Command-line processing';
break;
case Server.Status.HALTING:
led = 'negative';
blink = true;
running = 'HALT';
+ title = 'Server is halting';
break;
case Server.Status.RESTARTING:
led = 'warning';
blink = true;
running = 'REBOOT';
+ title = 'Server is restarting';
break;
case Server.Status.FAILURE:
led = 'negative';
blink = true;
running = 'ERR';
+ title = 'Server halted because of failure';
icon = 'WARNING';
break;
}
@@ -409,7 +424,7 @@ export const Status = () => {
return (
<>
<LED status={led} blink={blink} />
- <Code icon={icon} label={running} />
+ <Code icon={icon} label={running} title={title} />
<Toolbars.Separator />
</>
);
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index 29aac7f954eabee8cbecf1fbe404d82fe3d93239..006d4b9d15221f5cc3013df7bbb3e0edc4d647a3 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -25,6 +25,7 @@
(* -------------------------------------------------------------------------- *)
module Senv = Server_parameters
+module Signals = Set.Make(String)
(* -------------------------------------------------------------------------- *)
(* --- Registry --- *)
@@ -69,6 +70,8 @@ type 'a response = [
| `Killed of 'a
| `Signal of string
| `Rejected of 'a
+ | `CmdLineOn
+ | `CmdLineOff
]
type 'a message = {
@@ -87,7 +90,10 @@ type 'a process = {
mutable killed : bool ;
}
-module Sigs = Set.Make(String)
+type 'a running =
+ | Idle (* Server is waiting for requests *)
+ | CmdLine (* Frama-C command line is running *)
+ | ExecRequest of 'a process (* Running EXEC process *)
(* Server with request identifier (RqId) of type ['a] *)
type 'a server = {
@@ -95,13 +101,14 @@ type 'a server = {
equal : 'a -> 'a -> bool ; (* RqId equality *)
polling : int ; (* server polling, in milliseconds *)
fetch : unit -> 'a message option ; (* fetch some client message *)
- q_in : 'a process Queue.t ; (* queue of pending jobs *)
+ q_in : 'a process 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 s_active : Sigs.t ; (* signals the client is listening to *)
- mutable s_signal : Sigs.t ; (* emitted signals since last synchro *)
+ mutable s_active : Signals.t ; (* signals the client is listening to *)
+ mutable s_signal : Signals.t ; (* emitted signals since last synchro *)
mutable shutdown : bool ; (* server has been asked to shut down *)
- mutable running : 'a process option ; (* currently running EXEC request *)
+ mutable running : 'a running ; (* server running state *)
+ mutable cmdline : bool option ; (* cmdline signal management *)
}
exception Killed
@@ -133,8 +140,18 @@ let pp_response pp fmt (r : _ response) =
| `Rejected id -> Format.fprintf fmt "Rejected %a" pp id
| `Killed id -> Format.fprintf fmt "Killed %a" pp id
| `Signal sg -> Format.fprintf fmt "Signal %S" sg
+ | `CmdLineOn -> Format.pp_print_string fmt "CmdLine On"
+ | `CmdLineOff -> Format.pp_print_string fmt "CmdLine Off"
| `Data(id,data) ->
- Format.fprintf fmt "@[<hov 2>Replies [%a]@ %a@]" pp id Data.pretty data
+ if Senv.debug_atleast 3 then
+ Format.fprintf fmt "@[<hov 2>Response %a:@ %a@]" pp id Data.pretty data
+ else
+ Format.fprintf fmt "Replied %a" pp id
+
+let pp_running pp fmt = function
+ | Idle -> Format.pp_print_string fmt "Idle"
+ | CmdLine -> Format.pp_print_string fmt "CmdLine"
+ | ExecRequest { id } -> Format.fprintf fmt "ExectRequest [%a]" pp id
(* -------------------------------------------------------------------------- *)
(* --- Request Handling --- *)
@@ -167,9 +184,7 @@ let execute server ?yield proc =
?on_delayed:(delayed proc.request)
yield run proc
| _ -> run proc
- in
- Senv.debug ~level:2 "%a" (pp_response server.pretty) resp ;
- Queue.push resp server.q_out
+ in Queue.push resp server.q_out
(* -------------------------------------------------------------------------- *)
(* --- Signals --- *)
@@ -203,37 +218,49 @@ let emit s = !emitter s
(* --- Processing Requests --- *)
(* -------------------------------------------------------------------------- *)
-let raise_if_killed = function { killed } -> if killed then raise Killed
-let kill_exec e = e.killed <- true
-let kill_request eq id e = if eq id e.id then e.killed <- true
+let raise_if_killed = function
+ | Idle -> ()
+ | CmdLine -> ()
+ | ExecRequest { killed } -> if killed then raise Killed
+
+let kill_running ?id s =
+ match s.running with
+ | Idle -> ()
+ | CmdLine -> if id = None then Db.cancel ()
+ | ExecRequest p ->
+ match id with
+ | None -> p.killed <- true
+ | Some id -> if s.equal id p.id then p.killed <- true
+
+let kill_request eq id p = if eq id p.id then p.killed <- true
let process_request (server : 'a server) (request : 'a request) : unit =
- if Senv.debug_atleast 1 && (Senv.debug_atleast 3 || request <> `Poll) then
+ if Senv.debug_atleast 1 && (Senv.debug_atleast 2 || request <> `Poll) then
Senv.debug "%a" (pp_request server.pretty) request ;
match request with
| `Poll -> ()
| `Shutdown ->
begin
- Option.iter kill_exec server.running ;
+ kill_running server ;
Queue.clear server.q_in ;
Queue.clear server.q_out ;
server.shutdown <- true ;
end
| `SigOn sg ->
begin
- server.s_active <- Sigs.add sg server.s_active ;
+ server.s_active <- Signals.add sg server.s_active ;
notify sg true ;
end
| `SigOff sg ->
begin
- server.s_active <- Sigs.remove sg server.s_active ;
+ server.s_active <- Signals.remove sg server.s_active ;
notify sg false ;
end
| `Kill id ->
begin
+ kill_running ~id server ;
let set_killed = kill_request server.equal id in
Queue.iter set_killed server.q_in ;
- Option.iter set_killed server.running ;
end
| `Request(id,request,data) ->
begin
@@ -260,16 +287,27 @@ let process_request (server : 'a server) (request : 'a request) : unit =
(* -------------------------------------------------------------------------- *)
let communicate server =
+ Senv.debug ~level:3 "fetch" ;
match server.fetch () with
| None -> false
| Some message ->
+ Senv.debug ~level:2 "message(s) received" ;
let error =
try List.iter (process_request server) message.requests ; None
with exn -> Some exn in (* re-raised after message reply *)
let pool = ref [] in
Queue.iter (fun r -> pool := r :: !pool) server.q_out ;
+ Option.iter
+ (fun cmd ->
+ pool := (if cmd then `CmdLineOn else `CmdLineOff) :: !pool ;
+ ) server.cmdline ;
+ pool := List.rev !pool ;
Queue.clear server.q_out ;
- server.s_signal <- Sigs.empty ;
+ server.cmdline <- None ;
+ server.s_signal <- Signals.empty ;
+ Senv.debug ~level:2 "response(s) callback" ;
+ if Senv.debug_atleast 2 then
+ List.iter (Senv.debug "%a" (pp_response server.pretty)) !pool ;
message.callback !pool ;
Option.iter raise error ;
true
@@ -279,13 +317,13 @@ let communicate server =
(* -------------------------------------------------------------------------- *)
let do_yield server () =
- Option.iter raise_if_killed server.running ;
+ raise_if_killed server.running ;
ignore ( communicate server )
let do_signal server s =
- if Sigs.mem s server.s_active && not (Sigs.mem s server.s_signal) then
+ if Signals.mem s server.s_active && not (Signals.mem s server.s_signal) then
begin
- server.s_signal <- Sigs.add s server.s_signal ;
+ server.s_signal <- Signals.add s server.s_signal ;
Queue.push (`Signal s) server.q_out ;
end
@@ -302,14 +340,14 @@ let rec fetch_exec q =
let process server =
match fetch_exec server.q_in with
| None -> communicate server
- | Some proc ->
- server.running <- Some proc ;
+ | Some exec ->
+ server.running <- ExecRequest exec ;
try
- execute server ~yield:(do_yield server) proc ;
- server.running <- None ;
+ execute server ~yield:(do_yield server) exec ;
+ server.running <- Idle ;
true
with exn ->
- server.running <- None ;
+ server.running <- Idle ;
raise exn
(* -------------------------------------------------------------------------- *)
@@ -331,10 +369,11 @@ let create ~pretty ?(equal=(=)) ~fetch () =
fetch ; polling ; equal ; pretty ;
q_in = Queue.create () ;
q_out = Queue.create () ;
- s_active = Sigs.empty ;
- s_signal = Sigs.empty ;
+ s_active = Signals.empty ;
+ s_signal = Signals.empty ;
daemon = None ;
- running = None ;
+ running = Idle ;
+ cmdline = None ;
shutdown = false ;
}
@@ -342,49 +381,72 @@ let create ~pretty ?(equal=(=)) ~fetch () =
(* --- Start / Stop --- *)
(* -------------------------------------------------------------------------- *)
+(* public API ; shall be scheduled at command line main stage *)
let start server =
- emitter := do_signal 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 ;
- set_active true ;
- end
-
+ begin
+ Senv.debug ~level:2 "Server started (was %a)"
+ (pp_running server.pretty) server.running ;
+ server.running <- CmdLine ;
+ server.cmdline <- Some true ;
+ emitter := do_signal 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 ;
+ set_active true ;
+ end
+ end
+
+(* public API ; can be invoked to force server shutdown *)
let stop server =
- emitter := nop ;
- match server.daemon with
- | None -> ()
- | Some daemon ->
- begin
- Senv.feedback "Server disabled." ;
- server.daemon <- None ;
- Db.off_progress daemon ;
- set_active false ;
- end
-
+ begin
+ Senv.debug ~level:2 "Server stopped (was %a)"
+ (pp_running server.pretty) server.running ;
+ kill_running server ;
+ emitter := nop ;
+ match server.daemon with
+ | None -> ()
+ | Some daemon ->
+ begin
+ Senv.feedback "Server disabled." ;
+ server.daemon <- None ;
+ server.running <- Idle ;
+ server.cmdline <- None ;
+ Db.off_progress daemon ;
+ set_active false ;
+ end
+ end
+
+(* internal only ; invoked by run when command line is finished *)
let foreground server =
- emitter := do_signal server ;
- match server.daemon with
- | None -> ()
- | Some daemon ->
- begin
- server.daemon <- None ;
- Db.off_progress daemon ;
- end
+ begin
+ Senv.debug ~level:2 "Server foreground (was %a)"
+ (pp_running server.pretty) server.running ;
+ server.running <- Idle ;
+ server.cmdline <- Some false ;
+ emitter := do_signal server ;
+ match server.daemon with
+ | None -> ()
+ | Some daemon ->
+ begin
+ server.daemon <- None ;
+ Db.off_progress daemon ;
+ end
+ end
(* -------------------------------------------------------------------------- *)
(* --- Main Loop --- *)
(* -------------------------------------------------------------------------- *)
+(* public API ; shall be invoked at command line normal exit *)
let run server =
try
( (* TODO: catch-break to be removed once Why3 signal handler is fixed *)
diff --git a/src/plugins/server/main.mli b/src/plugins/server/main.mli
index 167692bbafdef2279b32f3594f1091de5771d413..9b649da2166f9c06ffd33a6bec2a75261f80c7f0 100644
--- a/src/plugins/server/main.mli
+++ b/src/plugins/server/main.mli
@@ -68,6 +68,8 @@ type 'a response = [
| `Killed of 'a
| `Rejected of 'a
| `Signal of string
+ | `CmdLineOn
+ | `CmdLineOff
]
(** A paired request-response message.
@@ -89,19 +91,38 @@ val create :
fetch:(unit -> 'a message option) ->
unit -> 'a server
-(** Run the server forever.
- The function will {i not} return until the server is actually 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()]. *)
+ The function returns immediately after installing a daemon that (only)
+ accepts GET requests received by the server on calls to [Db.yield()].
+
+ Shall be scheduled at command line main stage {i via}
+ [Db.Main.extend] extension point.
+*)
val start : 'a server -> unit
-(** Stop the server if it is running in background. *)
+(** Stop the server if it is running in background.
+
+ Can be invoked to force server shutdown at any time.
+
+ It shall be typically scheduled {i via} [Extlib.safe_at_exit] along with
+ other system cleanup operations to make sure the server is property
+ shutdown before Frama-C main process exits.
+*)
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()]
+ at every [server.polling] time interval.
+
+ The function will {i not} return until the server is actually shutdown.
+
+ Shall be scheduled at normal command line termination {i via}
+ [Cmdline.at_normal_exit] extension point. *)
+val run : 'a server -> unit
+
(** Kill the currently running request by raising an exception. *)
val kill : unit -> 'a
diff --git a/src/plugins/server/server_socket.ml b/src/plugins/server/server_socket.ml
index 13453b4fb283d1556e6192b922c024795d6251a7..b0f2e5b03fa47ea1dbd7bad43e8a5b960e564a90 100644
--- a/src/plugins/server/server_socket.ml
+++ b/src/plugins/server/server_socket.ml
@@ -41,6 +41,15 @@ module Socket = Senv.String
Finally, the server is executed until shutdown."
end)
+let () = Parameter_customize.set_group socket_group
+module SocketSize = Senv.Int
+ (struct
+ let option_name = "-server-socket-size"
+ let arg_name = "n"
+ let default = 256
+ let help = "Control the size of socket buffers (in ko, default 256)."
+ end)
+
let _ = Server_doc.protocole
~title:"Unix Socket Protocol"
~readme:"server_socket.md"
@@ -57,29 +66,42 @@ type channel = {
bsnd : Buffer.t ; (* SND data buffer, accumulated *)
}
-let feed_bytes { sock ; rcv ; brcv } =
- try
- (* rcv buffer is only used locally *)
- let s = Bytes.length rcv in
- let n = Unix.read sock rcv 0 s in
- Buffer.add_subbytes brcv rcv 0 n ;
- with Unix.Unix_error((EAGAIN|EWOULDBLOCK),_,_) -> ()
+let read_bytes { sock ; rcv ; brcv } =
+ (* rcv buffer is only used locally *)
+ let s = Bytes.length rcv in
+ let rec scan p =
+ (* try to fill RCV buffer *)
+ let n =
+ try Unix.read sock rcv p (s-p)
+ with Unix.Unix_error((EAGAIN|EWOULDBLOCK),_,_) -> 0
+ in
+ let p = p + n in
+ if n > 0 && p < s then scan p else p
+ in
+ let n = scan 0 in
+ if n > 0 then Buffer.add_subbytes brcv rcv 0 n
let send_bytes { sock ; snd ; bsnd } =
- try
- (* snd buffer is only used locally *)
- let n = Buffer.length bsnd in
- if n > 0 then
- let s = Bytes.length snd in
- let w = min n s in
- Buffer.blit bsnd 0 snd 0 w ;
- let r = Unix.single_write sock snd 0 w in
- if r > 0 then
- (* TODO[LC]: inefficient move. Requires a ring-buffer. *)
- let rest = Buffer.sub bsnd r (n-r) in
- Buffer.reset bsnd ;
- Buffer.add_string bsnd rest
- with Unix.Unix_error((EAGAIN|EWOULDBLOCK),_,_) -> ()
+ (* snd buffer is only used locally *)
+ let n = Buffer.length bsnd in
+ if n > 0 then
+ let s = Bytes.length snd in
+ let rec send p =
+ (* try to flush BSND buffer *)
+ let w = min (n-p) s in
+ Buffer.blit bsnd p snd 0 w ;
+ let r =
+ try Unix.single_write sock snd 0 w
+ with Unix.Unix_error((EAGAIN|EWOULDBLOCK),_,_) -> 0
+ in
+ let p = p + r in
+ if r > 0 && p < n then send p else p
+ in
+ let p = send 0 in
+ if p > 0 then
+ let tail = Buffer.sub bsnd p (n-p) in
+ Buffer.reset bsnd ;
+ Buffer.add_string bsnd tail
(* -------------------------------------------------------------------------- *)
(* --- Data Chunks Encoding --- *)
@@ -118,7 +140,6 @@ let write_data ch data =
in
Buffer.add_string ch.bsnd hex ;
Buffer.add_string ch.bsnd data ;
- send_bytes ch ;
end
(* -------------------------------------------------------------------------- *)
@@ -167,6 +188,8 @@ let encode (resp : string Main.response) : string =
| `Signal id -> `Assoc [
"res", `String "SIGNAL" ;
"id", `String id ]
+ | `CmdLineOn -> `String "CMDLINEON"
+ | `CmdLineOff -> `String "CMDLINEOFF"
in Yojson.Basic.to_string ~std:false js
let parse ch =
@@ -190,13 +213,14 @@ let callback ch rs =
| data -> write_data ch data
| exception err ->
Senv.debug "Socket: encoding error %S@." (Printexc.to_string err)
- ) rs
+ ) rs ;
+ send_bytes ch
let commands ch =
begin
- feed_bytes ch ;
+ read_bytes ch ;
match parse ch with
- | [] -> None
+ | [] -> send_bytes ch ; None
| requests -> Some Main.{ requests ; callback = callback ch }
end
@@ -214,14 +238,28 @@ let close (s: socket) =
s.channel <- None ;
Unix.close ch.sock
+let set_socket_size sock opt s =
+ begin
+ let nbytes = s * 1024 in
+ (try Unix.setsockopt_int sock opt nbytes
+ with Unix.Unix_error(err,_,_) ->
+ let msg = Unix.error_message err in
+ Senv.warning ~once:true
+ "Invalid socket size (%d: %s)" nbytes msg) ;
+ Unix.getsockopt_int sock opt
+ end
+
let channel (s: socket) =
match s.channel with
| Some _ as chan -> chan
| None ->
try
let sock,_ = Unix.accept ~cloexec:true s.socket in
- let snd = Unix.getsockopt_int sock SO_SNDBUF in
- let rcv = Unix.getsockopt_int sock SO_RCVBUF in
+ Unix.set_nonblock sock ;
+ let size = SocketSize.get () in
+ let rcv = set_socket_size sock SO_RCVBUF size in
+ let snd = set_socket_size sock SO_SNDBUF size in
+ Senv.debug ~level:2 "Socket size in:%d out:%d@." rcv snd ;
Senv.debug "Client connected" ;
let ch = Some {
sock ;
@@ -245,12 +283,10 @@ let fetch (s:socket) () =
Senv.warning "Socket: exn %s" (Printexc.to_string exn) ;
close s ; None
-let bind fd =
+let establish_server fd =
let socket = { socket = fd ; channel = None } in
try
- Unix.set_nonblock fd ;
Unix.listen fd 1 ;
- Unix.set_nonblock fd ;
ignore (Sys.signal Sys.sigpipe Signal_ignore) ;
let pretty = Format.pp_print_string in
let server = Main.create ~pretty ~fetch:(fetch socket) () in
@@ -276,17 +312,16 @@ let bind fd =
let server = ref None
let cmdline () =
- let addr = Socket.get () in
- match !server with
- | Some addr0 ->
- if Senv.debug_atleast 1 && addr <> addr0 then
+ let option = match Socket.get () with "" -> None | a -> Some a in
+ match !server, option with
+ | _ , None -> ()
+ | Some addr0, Some addr ->
+ if addr0 <> addr then
Senv.warning "Socket server already running on [%s]." addr0
- else
- Senv.feedback "Socket server already running."
- | None ->
- if addr <> "" then
+ | None, Some addr ->
+ begin
try
- server := Some addr ;
+ server := option ;
if Sys.file_exists addr then Unix.unlink addr ;
let fd = Unix.socket PF_UNIX SOCK_STREAM 0 in
Unix.bind fd (ADDR_UNIX addr) ;
@@ -294,10 +329,11 @@ let cmdline () =
Senv.feedback "Socket server running on [%s]." addr
else
Senv.feedback "Socket server running." ;
- bind fd
+ establish_server fd ;
with exn ->
Senv.fatal "Server socket failed.@\nError: %s@"
(Printexc.to_string exn)
+ end
let () = Db.Main.extend cmdline
diff --git a/src/plugins/server/server_zmq.ml b/src/plugins/server/server_zmq.ml
index d6c4ad728f20218cd05d1f26f2cd802ac3fcfc02..d19dd35c8d7ee38d02a3eda1147331b929221ae3 100644
--- a/src/plugins/server/server_zmq.ml
+++ b/src/plugins/server/server_zmq.ml
@@ -111,6 +111,8 @@ let rec encode = function
| `Killed id :: w -> "KILLED" :: id :: encode w
| `Rejected id :: w -> "REJECTED" :: id :: encode w
| `Signal sg :: w -> "SIGNAL" :: sg :: encode w
+ | `CmdLineOn :: w -> "CMDLINEON" :: encode w
+ | `CmdLineOff :: w -> "CMDLINEOFF" :: encode w
| [] -> []
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/share/server.md b/src/plugins/server/share/server.md
index 8d308a85a4d36f59e3c33607d981eec88fc2bd41..92163ccf852d3e68516ba74f438640d50f84416e 100644
--- a/src/plugins/server/share/server.md
+++ b/src/plugins/server/share/server.md
@@ -38,7 +38,7 @@ asynchronous entry points, requests are classified into three kinds:
- `EXEC` to starts a resource intensive analysis in Frama-C
During an `EXEC` requests, the implementation of the all resource demanding
-computations shall repeatedly call the yielding routine `!Db.progress()` of the
+computations shall repeatedly call the yielding routine `Db.yield()` of the
Frama-C kernel to ensures a smooth asynchronous behavior of the Server. During a
_yield_ call, the Server would be allowed to handle few `GET` pending requests,
since they shall be fast without any modification. When the server is idled, any
@@ -59,19 +59,25 @@ to the client. However, since a lot of signals might be emitted, the server
must be aware of which signals the client is listening to.
Signal are identified by unique strings.
-The server and client can exchange two special commands to manage signals:
+The server and client can exchange other special commands to manage signals:
| Command | Issued by | Effect |
|:--------|:---------:|:----------------------------|
| `SIGON s` | client | start listening to signal `<s>` |
| `SIGOFF s` | client | stop listening to signal `<s>` |
| `SIGNAL s` | server | signal `<s>` has been emitted |
+| `CMDLINEON` | server | execution of the Frama-C command line |
+| `CMDLINEOFF` | server | termination of the Frama-C command line |
When one or many requests emit some signal `<s>` several times,
the client would be notified only once per cycle of data exchange.
Signals will be notified in addition to responses or logical requests
or server polling.
+During the execution of the Frama-C command line, the server behaves just like
+during an `EXEC` request: only `GET` requests are processed at `Db.yield()` calls
+until the (normal) termination of the command line.
+
## Transport Messages
From the entry points layer, the asynchronous behavior of the Server makes
@@ -89,7 +95,7 @@ paired _intput messages_ and _output messages_. Each single input message consis
a list of _commands_:
| Commands | Parameters | Description |
-|:--------:|:----------:|:------------|
+|:---------|:-----------|:------------|
| `POLL` | - | Ask for pending responses and signals, if any |
| `GET` | `id,request,data` | En-queue the given GET request |
| `SET` | `id,request,data` | En-queue the given SET request |
@@ -103,12 +109,14 @@ Similarly, a single output message consists of a list
of _replies_, listed in table below:
| Replies | Parameters | Description |
-|:--------:|:----------:|:------------|
+|:---------|:-----------|:------------|
| `DATA` | `id,data` | Response data from the identified request |
| `ERROR` | `id,message` | Error message from the identified request |
| `SIGNAL` | `id` | The identified signal has been emitted since last exchange |
| `KILLED` | `id` | The identified request has been killed or interrupted |
| `REJECTED` | `id` | The identified request was not registered on the Server |
+| `CMDLINEON` | - | The command line has started |
+| `CMDLINEOFF` | - | The command line is terminated |
The logic layer makes no usage of _identifiers_ and simply pass them unchanged into
output messages in response to received requests.
@@ -131,9 +139,21 @@ function that possibly returns a list of commands, associated with a
callback for emitting the paired list of replies. The Server main
loop is guaranteed to invoke the callback exactly once.
-The Server plug-in implements two entry-points, however, other Frama-C plugins might
-implement their own entry-points and call the `Server.Main.run ~fetch ()` function
-to make the server starting and exchanging messages with the external world.
+To integrate your own server into the Frama-C command-line framework, you need to
+provide an implementation of the non-blocking `fetch` function and create a server
+with `Server.create`. Then, you shall:
+
+- Schedule `Server.start myServer` during the main plug-in extension phase _via_
+ `Db.Main.extend`;
+
+- Schedule `Server.run myServer` at normal command line termination phase _via_
+ `Cmdline.at_normal_exit`;
+
+- Schedule `Server.stop myServer` with other cleaning operations at exit phase
+ _via_ `Extlib.at_exit_safe`.
+
+This way, your server will integrate well with the command line execution of
+Frama-C and the other plug-ins.
## Request Implementations
diff --git a/src/plugins/server/share/server_socket.md b/src/plugins/server/share/server_socket.md
index c43990c8cea51c2ee65bfd10ad0227af1038b038..04b580e658790f58fc0483928db8ad91dd1182e6 100644
--- a/src/plugins/server/share/server_socket.md
+++ b/src/plugins/server/share/server_socket.md
@@ -54,6 +54,8 @@ An output message chunk consists of a single response encoded as follows:
| `KILLED(id)` | `{ res = 'KILLED', id }` |
| `REJECTED(id)` | `{ res = 'REJECTED', id }` |
| `SIGNAL(id)` | `{ res = 'SIGNAL', id }` |
+| `CMDLINEON` | `"CMDLINEON"` |
+| `CMDLINEOFF` | `"CMDLINEOFF"` |
The special last case is used when the server is busy or died or some low-level
error occurs.
diff --git a/src/plugins/server/share/server_zmq.md b/src/plugins/server/share/server_zmq.md
index 67999c67a5900e251f1340f539d1c447dad6b0a7..63e1d7e830a658a2653b3871efacccebf73a3703 100644
--- a/src/plugins/server/share/server_zmq.md
+++ b/src/plugins/server/share/server_zmq.md
@@ -45,6 +45,8 @@ of each reply is a finel string identifying the reply:
| `KILLED(id)` | 2 | `"KILLED"` | id | |
| `REJECTED(id)` | 2 | `"REJECTED"` | id | |
| `SIGNAL(id)` | 2 | `"SIGNAL"` | id | |
+| `CMDLINEON` | 1 | `"CMDLINEON"` | | |
+| `CMDLINEOFF` | 1 | `"CMDLINEOFF"` | | |
| (special) | 2 | `"WRONG"` | message | |
| (special) | 1 | `"NONE"` | | |