Repository files navigation

A generated thin wrapper around libsel4.a, with supporting subcrates.

• selfe-config is a build dependency library that defines a seL4 configuration format (sel4.toml) and utilities for building seL4 with that config
  • Also includes a binary tool,selfe for building seL4 applications with the help of a sel4.toml config file
• example_application is a Rust seL4 application that depends onselfe-sys for access to syscalls. It can be built/run independently or withselfe.
• selfe-start is a library that defines Rust lang-items required forno_std Rust-based root tasks on seL4.
• selfe-runtime is a tiny runtime library, required for any process which uses libsel4.a.

See the READMEs of the subdirectories for more detailed explanations.

Add a dependency to this library in your Cargo.toml manifest:

[dependencies]selfe-sys ="0.1"

And then in your Rust project:

externcrate selfe_sys;use selfe_sys::{seL4_CapInitThreadTCB, seL4_TCB_Suspend};fnmain(){let _suspend_error =unsafe{seL4_TCB_Suspend(seL4_CapInitThreadTCBasusize)};}

Furthermore, your library may require the following rustflags set in your.cargo/config filein order to link successfully.

[build]rustflags = ["-C","link-args=-no-pie"]

Note that the Rust-available library name isselfe_sys

selfe_sys contains the syscalls, constants, API functions, and type definitionsfromlibsel4.

The majority of these bindings are generated withbindgenfrom the seL4 kernel source specified in the project's relevant sel4.toml, as managed byselfe-config. The exact contents of thesel4-sys packagewill depend on the configuration flags set in that sel4.toml file, as they affectthe headers in seL4 used as input to the binding generation.

The goal here is to be able to track against changes to seL4 with as little manualeffort as reasonable.

Because these bindings are intended to be zero-overhead, the output is not particularlyRust-idiomatic. A notable no-cost ergonomics addition is thatseL4_Word andseL4_CPtr have been defined to be the same as regular Rustusize.

Starting from a regular Rust toolchain, install the build tools.

cargo install cargo-xbuildcargo install selfe-config --bin selfe --features bin --force

Note that Python, CMake, Ninja, QEMU, and others are lurking as indirect dependencies for seL4.

Default configuration is provided such that a regularcargo build will workeven without supplying a specificSEL4_CONFIG_PATH environment variable pointing at a sel4.toml file.

cargo build

Cross-compilation is also possible withcargo-xbuild orxargo. Specify your Rust target triple as an argument explicitly,and use the environment variableSEL4_CONFIG_PATH to point to your sel4.toml configuration fileand theSEL4_PLATFORM env-var to select your desired platform target.

SEL4_CONFIG_PATH=/home/other/sel4.toml SEL4_PLATFORM=pc99 cargo xbuild --target=x86_64-unknown-linux-gnu

The embedded default configuration file minimally supports thesabre andpc99 platforms

SEL4_PLATFORM=sabre cargo xbuild --target armv7-unknown-linux-gnueabihf

SEL4_PLATFORM=pc99 cargo xbuild --target x86_64-unknown-linux-gnu

This library contains three kinds of tests:

• Compile time tests that assert and confirm the expected structure of the bindgen output
• Runtime unit tests produced by bindgen itself that check layout details
• Runtime property based tests which ensure that some non-kernel interacting functionsbehave reasonably. These target the "bitfield" based structures which are generated behind inside seL4's build systemwith a combination of custom parsing and Python-template-based code creation.

Run them all on anx86_64 type host dev machine withcargo test

SeeLICENSE for more details.

Copyright 2021Auxon Corporation

Licensed under the Apache License, Version 2.0 (the "License");you may not use this file except in compliance with the License.You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, softwaredistributed under the License is distributed on an "AS IS" BASIS,WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.See the License for the specific language governing permissions andlimitations under the License.