The Server plug-in provides a remote procedure call (RPC) interface to foreign applications. The protocol is organized in three logic layers, organized as follows:
The intermediate, logic layer, is responsible for adding a small bit of parallelism upon the intrinsically synchronous behavior of Frama-C. This makes Frama-C resembling an asynchronous RPC server.
The externally visible layer is only focused on transporting external requests to the logic layer, and transporting back the results to the caller. The only requirement for an entry point is to be able to transport a sequence of 1-input message for 1-output message over time.
The concrete layer is implemented by the Frama-C kernel and its plug-ins. All requests must be registered via the Frama-C Server OCaml API in order to be accessible from the entry-points. Some parts of this documentation are automatically generated from the registered requests.
From a functional point of view, requests are remote procedures with input data that reply with output data. Each request is identified by a unique name. Input and output parameters are encoded into JSON values.
To adapt the internal synchronous Frama-C implementation with the external asynchronous entry points, requests are classified into three kinds:
GET
to instantaneously return data from the
internal state of Frama-CSET
to instantaneously modifies the state or
configure Frama-C plug-insEXEC
to starts a resource intensive analysis in
Frama-CDuring an EXEC
requests, the implementation of the
all resource demanding 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 kind of
requests can be started.
To summarize:
Request | During Yields | Allowed to Yield | Computation |
---|---|---|---|
GET |
✓ | - | fast, pure |
SET |
- | - | fast, side-effects |
EXEC |
- | ✓ | resource demanding |
In response to a logical requests, the server might also emit signals 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 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.
From the entry points layer, the asynchronous behavior of the Server makes output data and input data to be dispatched into different messages. However, from the Client side, we still want to have one response message for each incoming message. However, answer messages might contains output data from potentially any previously received requests.
When the client has no more requests to send, but is simply waiting for pending requests responses, it must periodically send polling requests to simply get back the expected responses.
To implement those features, the Client-Server protocol consists of a sequence of paired intput messages and output messages. Each single input message consists of 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 |
EXEC |
id,request,data |
En-queue the given EXEC request |
SIGON |
id |
Start listening to the given signal |
SIGOFF |
id |
Stop listening to the given signal |
KILL |
id |
Cancel the given request or interrupt its execution |
SHUTDOWN |
- | Makes the server to stop running |
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.
At the transport message layer, input and output data are made
of a single JSON
encoded value. Requests are
identified by string, and request identifiers can be of any type
from the entry-points.
Remark the GET
, SET
or EXEC
behavior of a request is actually defined by
the request implementation, from the Frama-C internal side. The
Server will silently ignore the request kind from the incoming
messages and use the actual internal one instead. The distinction
still appears in the transport protocol only for a purpose of
information, as clients shall know what they are asking for.
Implementations of entry points layers shall provide a
non-blocking fetch
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.
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.
It is the responsibility of Frama-C plug-ins to implement and register requests into the Server to make them accessible via any entry point. Whereas data is encoded into JSON structures at the transport layer, requests are processes with well typed OCaml types from the internal side.
Hence, the requests implementations also requires data encoder
and decoders to be defined. Some predefined data types are
provided by the Server plug-in, but more complex types can be
defined and shared among plug-ins via the
Server.Data
module factory.
Registration of requests, data encoder and decoders always
comes with their markdown documentation thanks to the
Markdown
library provided by the Frama-C kernel.
Hence, a full documentation of all implemented requests with their
data formats can be generated consistently at any time. See option
-server-doc
of the Server plug-in for more
details.