From a67f91271633a2455e1aa802b469ae6377bdef1d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 10 Dec 2021 16:38:45 +0100
Subject: [PATCH] [server] added server-socket transport protocol
---
headers/header_spec.txt | 2 +
src/plugins/server/Makefile.in | 3 +-
src/plugins/server/server_socket.ml | 223 ++++++++++++++++++++++
src/plugins/server/server_socket.mli | 23 +++
src/plugins/server/share/server_socket.md | 63 ++++++
5 files changed, 313 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/server/server_socket.ml
create mode 100644 src/plugins/server/server_socket.mli
create mode 100644 src/plugins/server/share/server_socket.md
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 194a94cddf0..c77ac35916f 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1227,6 +1227,8 @@ src/plugins/server/server_parameters.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_batch.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_batch.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/server_socket.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/server_socket.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_zmq.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_zmq.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/states.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/server/Makefile.in b/src/plugins/server/Makefile.in
index 0736b25b9d0..e2428ee5cfb 100644
--- a/src/plugins/server/Makefile.in
+++ b/src/plugins/server/Makefile.in
@@ -43,6 +43,7 @@ PLUGIN_CMO:= \
data main request states \
server_doc \
server_batch \
+ server_socket \
kernel_ast \
kernel_main \
kernel_project \
@@ -54,7 +55,7 @@ PLUGIN_TESTS_DIRS := batch
PLUGIN_REQUIRES:= yojson
-PLUGIN_UNDOC:= server_batch.ml server_zmq.ml
+PLUGIN_UNDOC:= server_batch.ml server_zmq.ml server_socket.ml
PLUGIN_GENERATED:= $(PLUGIN_DIR)/Server.mli
diff --git a/src/plugins/server/server_socket.ml b/src/plugins/server/server_socket.ml
new file mode 100644
index 00000000000..3c1a4020631
--- /dev/null
+++ b/src/plugins/server/server_socket.ml
@@ -0,0 +1,223 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Socket Server Options --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Senv = Server_parameters
+
+let socket_group = Senv.add_group "Protocol Unix Sockets"
+
+let () = Parameter_customize.set_group socket_group
+module Socket = Senv.String
+ (struct
+ let option_name = "-server-socket"
+ let arg_name = "url"
+ let default = ""
+ let help =
+ "Launch the UnixSocket 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 _ = Server_doc.protocole
+ ~title:"Unix Socket Protocol"
+ ~readme:"server_socket.md"
+
+(* -------------------------------------------------------------------------- *)
+(* --- Low-level Messages --- *)
+(* -------------------------------------------------------------------------- *)
+
+let buffer_size = 65536
+
+type channel = {
+ mutable eof : bool ;
+ inc : in_channel ;
+ out : out_channel ;
+ buffer : Buffer.t ;
+}
+
+let feed q =
+ if not q.eof then
+ try Buffer.add_channel q.buffer q.inc buffer_size
+ with End_of_file -> q.eof <- true
+
+let read q =
+ try
+ let h = match Buffer.nth q.buffer 0 with
+ | 'S' -> 3
+ | 'L' -> 7
+ | 'W' -> 15
+ | _ -> raise (Invalid_argument "Server_socket.read")
+ in
+ let hex = Buffer.sub q.buffer 1 h in
+ let len = int_of_string ("0x" ^ hex) in
+ let data = Buffer.sub q.buffer (1+h) len in
+ let p = 1 + h + len in
+ let n = Buffer.length q.buffer - p in
+ let rest = Buffer.sub q.buffer p n in
+ Buffer.reset q.buffer ;
+ Buffer.add_string q.buffer rest ;
+ Some data
+ with Invalid_argument _ ->
+ None
+
+let write q data =
+ begin
+ let len = String.length data in
+ let hex =
+ if len < 0xFFF then Printf.sprintf "S%03x" len else
+ if len < 0xFFFFFFF then Printf.sprintf "L%07x" len else
+ Printf.sprintf "W%015x" len
+ in
+ output_string q.out hex ;
+ output_string q.out data ;
+ flush q.out ;
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Request Encoding --- *)
+(* -------------------------------------------------------------------------- *)
+
+let jfield fd js = Json.field fd js |> Json.string
+
+let decode (data : string) : string Main.request =
+ match data with
+ | "POLL" -> `Poll
+ | "SHUTDOWN" -> `Shutdown
+ | _ ->
+ let js = Yojson.Basic.from_string data in
+ match jfield "cmd" js with
+ | "GET" | "SET" | "EXEC" ->
+ let id = jfield "id" js in
+ let request = jfield "request" js in
+ let data = Json.field "data" js in
+ `Request(id,request,data)
+ | "SIGON" -> `SigOn (jfield "id" js)
+ | "SIGOFF" -> `SigOff (jfield "id" js)
+ | "KILL" -> `Kill (jfield "id" js)
+ | _ -> raise Not_found
+
+let encode (resp : string Main.response) : string =
+ let js =
+ match resp with
+ | `Data(id,data) -> `Assoc [
+ "res", `String "DATA" ;
+ "id", `String id ;
+ "data", data ]
+ | `Error(id,msg) -> `Assoc [
+ "res", `String "ERROR" ;
+ "id", `String id ;
+ "msg", `String msg ]
+ | `Killed id -> `Assoc [
+ "res", `String "KILLED" ;
+ "id", `String id ]
+ | `Rejected id -> `Assoc [
+ "res", `String "REJECTED" ;
+ "id", `String id ]
+ | `Signal id -> `Assoc [
+ "res", `String "SIGNAL" ;
+ "id", `String id ]
+ in Yojson.Basic.to_string ~std:false js
+
+let commands q =
+ begin
+ feed q ;
+ let rec scan cmds q =
+ match read q with
+ | None -> List.rev cmds
+ | Some data ->
+ match decode data with
+ | cmd -> scan (cmd::cmds) q
+ | exception _ -> scan cmds q
+ in scan [] q
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Socket Messages --- *)
+(* -------------------------------------------------------------------------- *)
+
+let callback q rs =
+ List.iter
+ (fun r ->
+ match encode r with
+ | data -> write q data
+ | exception _ -> ()
+ ) rs
+
+let fetch q () =
+ if q.eof then None else
+ match commands q with
+ | [] -> None
+ | requests -> Some Main.{ requests ; callback = callback q }
+
+(* -------------------------------------------------------------------------- *)
+(* --- Establish the Server --- *)
+(* -------------------------------------------------------------------------- *)
+
+let pretty = Format.pp_print_string
+let server = ref None
+
+let bind inc out =
+ try
+ Senv.debug "Client connected" ;
+ let channel = {
+ eof = false ; inc ; out ;
+ buffer = Buffer.create buffer_size ;
+ } in
+ let srv = Main.create ~pretty ~fetch:(fetch channel) () in
+ Extlib.safe_at_exit begin fun () ->
+ Main.stop srv ;
+ close_in inc ;
+ close_out out ;
+ end ;
+ Main.start srv ;
+ Cmdline.at_normal_exit (fun () -> Main.run srv) ;
+ with exn ->
+ close_in inc ;
+ close_out out ;
+ raise exn
+
+let cmdline () =
+ let url = Socket.get () in
+ match !server with
+ | Some url0 ->
+ if url = url0 then
+ Senv.feedback "Socket server already running"
+ else
+ Senv.warning "Socket server already running on [%s]" url0
+ | None ->
+ if url <> "" then
+ try
+ server := Some url ;
+ if Sys.file_exists url then Unix.unlink url ;
+ Senv.feedback "Socket server running on [%s]" url ;
+ Unix.establish_server bind (ADDR_UNIX url) ;
+ with exn ->
+ Senv.fatal "Server socket failed@\nError: %s@"
+ (Printexc.to_string exn)
+
+let () = Db.Main.extend cmdline
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/server_socket.mli b/src/plugins/server/server_socket.mli
new file mode 100644
index 00000000000..e472344b807
--- /dev/null
+++ b/src/plugins/server/server_socket.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* No interface, registered via side-effects *)
diff --git a/src/plugins/server/share/server_socket.md b/src/plugins/server/share/server_socket.md
new file mode 100644
index 00000000000..c43990c8cea
--- /dev/null
+++ b/src/plugins/server/share/server_socket.md
@@ -0,0 +1,63 @@
+# Unix Sockets Protocol
+
+This section presents entry point for Frama-C Server based on standard Unix
+Sockets. It is activated by option `-server-socket <URL>` option of the Server
+plug-in, which is compiled when the OCaml package `zmq` is detected at Frama-C
+configure time.
+
+The protocol builds a pair of Unix sockets from the OCaml unix standard library.
+
+```shell
+$ frama-c [options...] -then -server-socket /tmp/my-server.io
+```
+
+## Messages Chunk Format
+
+Messages are exchanged through non-blocking I/O on sockets input and output streams.
+Each individual message is formatted into _chunks_ with any of the following formats:
+
+ | 'S' | 3-HEX | n-DATA | -- with n = 0xHHH
+ | 'L' | 7-HEX | n-DATA | -- with n = 0xHHH,HHHH
+ | 'W' | 15-HEX | n-DATA | -- with n = 0xHHH,HHHH,HHHH,HHHH
+
+The first byte of a message chunk is one ASCII character encoding the data-length format:
+- `'S'` (short) : the length consists of 3 hex-digits in ASCII format;
+- `'L'` (long) : the length consists of 7 hex-digits in ASCII format;
+- `'W'` (wide) : the length consists of 15 hex-digits in ASCII format.
+
+The last part of the message consists of `0xHEX` bytes of data, which is an `UTF-8`
+encoded JSON data.
+
+## Input Message Format
+
+An input message chunk consists of a single command encoded as follows:
+
+| Commands | JSON Message |
+|:--------|:--------------|
+| `POLL` | `"POLL"` |
+| `SHUTDOWN` | `"SHUTDOWN"` |
+| `GET(id,request,data)` | `{ cmd = 'GET', id, request, data }` |
+| `SET(id,request,data)` | `{ cmd = 'SET', id, request, data }` |
+| `EXEC(id,request,data)` | `{ cmd = 'EXEC', id, request, data }` |
+| `SIGON(id)` | `{ cmd = 'SIGON', id }` |
+| `SIGOFF(id)` | `{ cmd = 'SIGOFF', id }` |
+| `KILL(id)` | `{ cmd = 'KILL', id }` |
+
+## Output Message Format
+
+An output message chunk consists of a single response encoded as follows:
+
+| Response | JSON Message |
+|:--------|:--------------|
+| `DATA(id,data)` | `{ res = 'DATA', id, data }` |
+| `ERROR(id,msg)` | `{ res = 'ERROR', id, msg }` |
+| `KILLED(id)` | `{ res = 'KILLED', id }` |
+| `REJECTED(id)` | `{ res = 'REJECTED', id }` |
+| `SIGNAL(id)` | `{ res = 'SIGNAL', id }` |
+
+The special last case is used when the server is busy or died or some low-level
+error occurs.
+
+## Data Format
+
+Request identifiers can be any JSON string and data are in JSON format.
--
GitLab