Appendix
Command Line Options
The following command line options are available for the rflx command:
usage: rflx [-h] [-q] [--version] [--no-caching] [--no-verification]
[--max-errors NUM] [--workers NUM] [--unsafe] [--legacy-errors]
{check,generate,optimize,graph,validate,install,convert,run_ls,doc}
...
positional arguments:
{check,generate,optimize,graph,validate,install,convert,run_ls,doc}
check check specification
generate generate code
optimize optimize generated state machine code
graph generate graphs
validate validate specification against a set of known valid or
invalid messages
install set up RecordFlux IDE integration
convert convert foreign specifications into RecordFlux
specifications
run_ls run language server
doc open documentation
options:
-h, --help show this help message and exit
-q, --quiet disable logging to standard output
--version
--no-caching ignore verification cache
--no-verification skip time-consuming verification of model
--max-errors NUM exit after at most NUM errors
--workers NUM parallelize proofs among NUM workers (default: NPROC)
--unsafe allow unsafe options (WARNING: may lead to erronous
behavior)
--legacy-errors use old error message format
The rflx check subcommand has the following options:
usage: rflx check [-h] SPECIFICATION_FILE [SPECIFICATION_FILE ...]
positional arguments:
SPECIFICATION_FILE specification file
options:
-h, --help show this help message and exit
The rflx generate subcommand has the following options:
usage: rflx generate [-h] [-p PREFIX] [-n] [-d OUTPUT_DIRECTORY]
[--debug {built-in,external}]
[--ignore-unsupported-checksum]
[--integration-files-dir INTEGRATION_FILES_DIR]
[--reproducible]
[SPECIFICATION_FILE ...]
positional arguments:
SPECIFICATION_FILE specification file
options:
-h, --help show this help message and exit
-p PREFIX, --prefix PREFIX
add prefix to generated packages (default: RFLX)
-n, --no-library omit generating library files
-d OUTPUT_DIRECTORY output directory
--debug {built-in,external}
enable adding of debug output to generated code
--ignore-unsupported-checksum
ignore checksum aspects during code generation
--integration-files-dir INTEGRATION_FILES_DIR
directory for the .rfi files
--reproducible ensure reproducible output
The rflx graph subcommand has the following options:
usage: rflx graph [-h] [-f {dot,jpg,pdf,png,raw,svg}] [-i REGEX]
[-d OUTPUT_DIRECTORY]
SPECIFICATION_FILE [SPECIFICATION_FILE ...]
positional arguments:
SPECIFICATION_FILE specification file
options:
-h, --help show this help message and exit
-f {dot,jpg,pdf,png,raw,svg}, --format {dot,jpg,pdf,png,raw,svg}
output format (default: svg)
-i REGEX, --ignore REGEX
ignore states with names matching regular expression
-d OUTPUT_DIRECTORY output directory
The rflx validate subcommand has the following options:
usage: rflx validate [-h] [--split-disjunctions] [-v VALID_SAMPLE_PATH]
[-i INVALID_SAMPLE_PATH] [-c CHECKSUM_MODULE]
[-o OUTPUT_FILE] [--abort-on-error] [--coverage]
[--target-coverage PERCENTAGE]
SPECIFICATION_FILE MESSAGE_IDENTIFIER
positional arguments:
SPECIFICATION_FILE specification file
MESSAGE_IDENTIFIER identifier of the top-level message (e.g.,
Package::Message)
options:
-h, --help show this help message and exit
--split-disjunctions split disjunctions before model validation (may have
severe performance impact)
-v VALID_SAMPLE_PATH known valid sample file or directory
-i INVALID_SAMPLE_PATH
known invalid sample file or directory
-c CHECKSUM_MODULE name of the module containing the checksum functions
-o OUTPUT_FILE path to output file for validation report in JSON
format (file must not exist)
--abort-on-error abort with exitcode 1 if a message is classified as a
false positive or false negative
--coverage enable coverage calculation and print the combined
link coverage of all provided messages
--target-coverage PERCENTAGE
abort with exitcode 1 if the coverage threshold is not
reached
The rflx install subcommand has the following options:
usage: rflx install [-h] [--gnat-studio-dir GNAT_STUDIO_DIR]
{gnatstudio,vscode,nvim,vim}
positional arguments:
{gnatstudio,vscode,nvim,vim}
options:
-h, --help show this help message and exit
--gnat-studio-dir GNAT_STUDIO_DIR
path to the GNAT Studio settings directory (default:
$HOME/.gnatstudio)
The rflx convert subcommand has the following options:
usage: rflx convert [-h] [--reproducible] {iana} ...
positional arguments:
{iana}
iana convert IANA registry into RecordFlux specifications
options:
-h, --help show this help message and exit
--reproducible ensure reproducible output
The rflx run_ls subcommand has the following options:
usage: rflx run_ls [-h]
options:
-h, --help show this help message and exit
The rflx doc subcommand has the following options:
usage: rflx doc [-h] {lrm,ug}
positional arguments:
{lrm,ug} documentation to open: Language Reference Manual (lrm), User's
Guide (ug)
options:
-h, --help show this help message and exit
Specification Files
Style Checks
By default, the style of specification files is checked. Error messages about style violations have a style check identifier appended to the message in the following form "[style:<identifier>]". For example: "[style:line-length]". Style checks can be disabled for individual files by adding a pragma to the first line of the file.
Example
-- style: disable = line-length, blank-lines
package P is
end P;
It is also possible to disable all style checks by using the identifier all.
Example
-- style: disable = all
package P is
end P;
Integration Files
For each RecordFlux specification file with the .rflx file extension, users may provide a file with the same name but the .rfi file extension.
This is useful to specify buffer sizes for state machines.
This file is in the YAML data format.
Buffer sizes are provided in bytes.
If no such file is provided, RecordFlux uses a default buffer size of 4096 bytes.
Integration file structure
The following example of an integration file defines, for the state machine My_State_Machine, a default buffer size of 4096 bytes, a buffer size of 2048 bytes for the global variable My_Global_Var, and a buffer size of 1024 bytes for the variable My_State_Variable defined in the state My_State.
Machine:
My_State_Machine:
Buffer_Size:
Default: 4096
Global:
My_Global_Var: 2048
Local:
My_State:
My_State_Variable: 1024
External IO Buffers
By default, all message buffers of a state machine are stored inside the state machine's Context type.
The Read and Write primitives give access to a message buffer when the state machine reaches an IO state.
An alternative is to use externally defined buffers.
This approach can save memory and prevent copy operations, but it removes some safety guarantees (see the notes at the end of the section).
External IO buffers can be enabled for a state machine by setting the External_IO_Buffers option in the integration file.
Machine:
My_State_Machine:
External_IO_Buffers: True
If external IO buffers are enabled, the buffer for all messages that are accessed in any IO state must be allocated externally and provided during the initialization of the state machine context as arguments to the Initialize procedure.
When an IO state is reached, the corresponding buffer of the accessed message can be removed from the state machine context.
The buffer must be added again before the state machine can be continued.
if Buffer_Accessible (Next_State (Ctx), B_Request) then
Remove_Buffer (Ctx, B_Request, Request_Buffer);
...
Add_Buffer (Ctx, B_Request, Request_Buffer, Written_Last (Ctx, B_Request));
end if;
Run (Ctx);
Before a buffer can be removed or added, it must be checked that the buffer is accessible.
The buffer is accessible if the next state of the state machine will perform either a read or write operation on the given buffer.
The function Buffer_Accessible can be used to check this condition.
If all read or write operations on a given channel are used with a single message buffer, then the function Needs_Data or Has_Data, respectively, is sufficient to determine this condition.
Each external buffer is uniquely identified by an enumeration literal of the External_Buffer type.
In the example shown above, B_Request identifies the buffer of a message called Request.
When adding a buffer, the index of the last written byte has to be provided.
If the buffer has not been changed, Written_Last can be used to set it to the same value as before.
CAUTION:
The message buffer must only be modified if the state machine expects data, i.e., Needs_Data is true.
Changing the contents of the buffer at other times may cause the state machine to behave unexpectedly.
This property cannot be guaranteed by the generated SPARK contracts.
Reporting Errors
Please report issues on GitHub:
https://github.com/AdaCore/RecordFlux/issues/new?labels=bug
If a tool invocation produces a bug box, please include its complete content and all input files in the report.
As an AdaCore customer, please open a ticket in GNAT Tracker.
Background
More information about the theoretical background of RecordFlux can be found in our paper:
Reiher T., Senier A., Castrillon J., Strufe T. (2020) RecordFlux: Formal Message Specification and Generation of Verifiable Binary Parsers. In: Arbab F., Jongmans SS. (eds) Formal Aspects of Component Software. FACS 2019. Lecture Notes in Computer Science, vol 12018. Springer, Cham (paper, preprint)