Skip to main content

sel4/
lib.rs

1//
2// Copyright 2023, Colias Group, LLC
3//
4// SPDX-License-Identifier: MIT
5//
6
7//! This crate provides straightforward, pure-Rust bindings to the [seL4
8//! API](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf).
9//!
10//! Most items in this crate correspond to types, constants, and functions in `libsel4`. See the
11//! [seL4 manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf) for more information about
12//! the seL4 concepts and `libsel4` items references in this crate's documentation.
13//!
14//! This crate's implementation is based on the lower-level [`sel4-sys`](::sel4_sys) crate, which is
15//! generated from the libsel4 headers and interface definition files.
16//!
17//! ### Features
18//!
19//! #### `"state"`
20//!
21//! Functions in the C libsel4 use the thread-local variable `__sel4_ipc_buffer` to obtain a pointer
22//! to the current thread's IPC buffer:
23//!
24//! ```C
25//! extern __thread seL4_IPCBuffer *__sel4_ipc_buffer;
26//! ```
27//!
28//! [libmicrokit](https://github.com/seL4/microkit/tree/main/libmicrokit), which does not support
29//! thread-local storage uses the following snippet to force `__sel4_ipc_buffer` to global rather
30//! than thread-local:
31//!
32//! ```C
33//! #define __thread
34//! #include <sel4/sel4.h>
35//! ```
36//!
37//! For the sake of flexibility and applicability, this crate can be configured to use no state at
38//! all. Users can opt out of state and explicitly pass around references to the active IPC buffer
39//! instead of relying on the implementation to obtain such a reference using thread-local or global
40//! state. Such a paradigm is useful in certain uncommon circumstances, but most users will benefit
41//! from the convenience of an implicit IPC buffer. The `"state"` feature, enabled by default, uses
42//! state to allow one to make seL4 API calls without having to explicitly specify an IPC buffer.
43//!
44//! For the sake of interoperability with C, the state looks something like: `static mut
45//! __sel4_ipc_buffer: *mut IpcBuffer`. If the `"state-exposed"` feature is enabled, it is exposed
46//! with `#![no_mangle]`. If the `"state-extern"` feature is enabled, it is wrapped in an `extern
47//! "C"` block. Whether it is thread-local is determined by the following pseudocode:
48//!
49//! ```rust
50//! cfg_if! {
51//!     if #[cfg(all(any(target_thread_local, feature = "tls"), not(feature = "non-thread-local-state")))] {
52//!         // thread-local
53//!     } else if #[cfg(not(feature = "thread-local-state"))] {
54//!         // not thread-local
55//!     } else {
56//!         compile_error!(r#"invalid configuration"#);
57//!     }
58//! }
59//! ```
60//!
61//! The non-thread-local configuration should only be used in cases where the language runtime does
62//! not support thread-local storage. In those cases without thread-local storage where this crate
63//! will only ever run in a single thread, use the `"single-threaded"` feature to enable a more
64//! efficient implementation. Note that enabling the `"single-threaded"` feature in a case where
65//! this crate runs in more than one thread is unsafe.
66//!
67//! At the API level, the `"state"` feature causes [`NoExplicitInvocationContext`] to be an alias
68//! for [`ImplicitInvocationContext`], which implements [`InvocationContext`] by accessing the
69//! thread-local pointer to an IPC buffer. When the `"state"` feature is not enabled,
70//! [`NoExplicitInvocationContext`] is an alias for [`NoInvocationContext`], which does not
71//! implement [`InvocationContext`]. The thread-local IPC buffer pointer is modified and accessed by
72//! [`set_ipc_buffer`], [`with_ipc_buffer`], and [`with_ipc_buffer_mut`]. The lower-level
73//! [`try_with_ipc_buffer_slot`] and [`try_with_ipc_buffer_slot_mut`] are provided as well.
74//!
75//! ### Building
76//!
77//! This crate and its dependencies depend, at build time, on the libsel4 headers. The location of
78//! these headers is provided to this crate at build time by environment variables. If
79//! `SEL4_INCLUDE_DIRS` is set, then its value is interpreted as a colon-separated list of include
80//! paths for the libsel4 headers. Otherwise, if `SEL4_PREFIX` is set, then
81//! `$SEL4_PREFIX/libsel4/include` is used.
82
83#![no_std]
84#![feature(cfg_target_thread_local)]
85#![feature(thread_local)]
86#![allow(unused_features)]
87#![allow(clippy::unit_arg)]
88
89pub use sel4_config::{
90    self as config, sel4_cfg, sel4_cfg_attr, sel4_cfg_bool, sel4_cfg_enum, sel4_cfg_if,
91    sel4_cfg_match, sel4_cfg_str, sel4_cfg_struct, sel4_cfg_usize, sel4_cfg_word,
92    sel4_cfg_wrap_match,
93};
94
95pub use sel4_sys as sys;
96
97mod arch;
98mod bootinfo;
99mod cap_rights;
100mod cnode_cap_data;
101mod const_helpers;
102mod cptr;
103mod error;
104mod fault;
105mod helper_macros;
106mod invocation_context;
107mod invocations;
108mod ipc_buffer;
109mod message_info;
110mod object;
111mod reply_authority;
112mod syscalls;
113mod vspace;
114
115pub mod init_thread;
116
117pub use bootinfo::{
118    BootInfo, BootInfoExtra, BootInfoExtraId, BootInfoExtraIter, BootInfoPtr, UntypedDesc,
119};
120pub use cap_rights::{CapRights, CapRightsBuilder};
121pub use cnode_cap_data::CNodeCapData;
122pub use cptr::{
123    AbsoluteCPtr, CPtr, CPtrBits, CPtrWithDepth, Cap, CapType, HasCPtrWithDepth, cap, cap_type,
124};
125pub use error::{Error, Result};
126pub use fault::*;
127pub use invocation_context::{InvocationContext, NoExplicitInvocationContext, NoInvocationContext};
128pub use invocations::TcbFlagsBuilder;
129pub use ipc_buffer::IpcBuffer;
130pub use message_info::{MessageInfo, MessageInfoBuilder};
131pub use object::{
132    CapTypeForObject, CapTypeForObjectOfFixedSize, CapTypeForObjectOfVariableSize, ObjectBlueprint,
133    ObjectType,
134};
135pub use reply_authority::{ConveysReplyAuthority, ReplyAuthority};
136pub use syscalls::{
137    Badge, CallWithMRs, FastMessages, IpcCapType, NUM_MESSAGE_REGISTERS, RecvWithMRs, r#yield,
138};
139pub use vspace::{
140    CapTypeForFrameObject, CapTypeForFrameObjectOfFixedSize, CapTypeForTranslationTableObject,
141    vspace_levels,
142};
143
144sel4_cfg_if! {
145    if #[sel4_cfg(KERNEL_MCS)] {
146        pub use invocations::Time;
147    } else {
148        pub use syscalls::reply;
149        pub use reply_authority::ImplicitReplyAuthority;
150    }
151}
152
153#[sel4_cfg(SET_TLS_BASE_SELF)]
154pub use syscalls::set_tls_base;
155
156pub use arch::top_level::*;
157
158pub(crate) use helper_macros::{
159    declare_cap_alias, declare_cap_type, declare_cap_type_for_object,
160    declare_cap_type_for_object_of_fixed_size, declare_cap_type_for_object_of_variable_size,
161    declare_fault_newtype, newtype_methods,
162};
163
164sel4_cfg_if! {
165    if #[sel4_cfg(PRINTING)] {
166        mod printing;
167
168        pub use printing::{DebugWrite, debug_put_char};
169    }
170}
171
172sel4_cfg_if! {
173    if #[sel4_cfg(DEBUG_BUILD)] {
174        mod debug;
175
176        pub use debug::{debug_snapshot, debug_halt};
177    }
178}
179
180sel4_cfg_if! {
181    if #[sel4_cfg(ENABLE_BENCHMARKS)] {
182        mod benchmark;
183
184        pub use benchmark::{
185            benchmark_reset_log,
186            benchmark_finalize_log,
187            benchmark_set_log_buffer,
188        };
189
190        sel4_cfg_if! {
191            if #[sel4_cfg(BENCHMARK_TRACK_UTILISATION)] {
192                pub use benchmark::{
193                    benchmark_get_thread_utilisation,
194                    benchmark_reset_thread_utilisation,
195                };
196
197                #[sel4_cfg(DEBUG_BUILD)]
198                pub use benchmark::{
199                    benchmark_dump_all_thread_utilisation,
200                    benchmark_reset_all_thread_utilisation,
201                };
202            }
203        }
204    }
205}
206
207#[cfg(feature = "state")]
208mod state;
209
210#[cfg(feature = "state")]
211pub use state::{
212    ImplicitInvocationContext, ipc_buffer_is_thread_local, set_ipc_buffer,
213    try_with_ipc_buffer_slot, try_with_ipc_buffer_slot_mut, with_ipc_buffer, with_ipc_buffer_mut,
214};
215
216/// Corresponds to `seL4_Word`.
217pub type Word = sys::seL4_Word;
218
219/// The size of [`Word`] in bits.
220pub const WORD_SIZE: usize = sel4_cfg_usize!(WORD_SIZE);
221
222#[doc(hidden)]
223pub mod _private {
224    #[sel4_config::sel4_cfg(PRINTING)]
225    pub use super::printing::_private as printing;
226}