12 Mar
2020
12 Mar
'20
12:24 p.m.
Hello,
I would like to use the sel4.xml API description files to generate custom bindings for a
prototype language to interact directly with seL4 without going through libsel4 C API.
I assume that the structure of these files could change, which I'm willing to
accept, but wanted to know if these files are here to stay in the future?
I understand also that I will still have to parse libsel4 C headers to recover the full
API which I'm fine with too.
Do you see any trouble following this approach or would you recommend something else?
Hi, (sorry for the laggy response).
There is a wish to represent the libsel4 API in a language agnostic format to make
generating bindings for other languages easier but at the moment it isn't being
actively worked on.
Currently the parts of the API that are generated from language agnostic formats are the
invocation and syscall bindings from the *.xml files and some data type definitions that
are generated from *.bf (bitfield) files. The bitfield language is used to generate
bitfield struct access methods in C as well as automatically generating some of the
Isabelle theory scripts relating to the C methods.
In the future, the .xml files could get replaced with a more domain specific interface
language format but it is likely that that transition would happen after more of the C
definitions get converted to either .xml or .bf formats first.
I'm not sure whether you would want to manually translate all of the non-xml
definitions or also try and generate them. The definitions that change the most across
build configurations are already likely to be in a .xml representation as that was the
motivation for adding the .xml representation in the first place.
As for staying up to date with any changes, this discussion page
(https://sel4.discourse.group/t/procedural-generation-of-the-sel4-api/24) will likely get
updated with any changes. Also feel free to weigh in on the discussion there too.