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 ipc_buffer::IpcBuffer;
129pub use message_info::{MessageInfo, MessageInfoBuilder};
130pub use object::{
131    CapTypeForObject, CapTypeForObjectOfFixedSize, CapTypeForObjectOfVariableSize, ObjectBlueprint,
132    ObjectType,
133};
134pub use reply_authority::{ConveysReplyAuthority, ReplyAuthority};
135pub use syscalls::{
136    Badge, CallWithMRs, FastMessages, IpcCapType, NUM_MESSAGE_REGISTERS, RecvWithMRs, r#yield,
137};
138pub use vspace::{
139    CapTypeForFrameObject, CapTypeForFrameObjectOfFixedSize, CapTypeForTranslationTableObject,
140    vspace_levels,
141};
142
143sel4_cfg_if! {
144    if #[sel4_cfg(KERNEL_MCS)] {
145        pub use invocations::Time;
146    } else {
147        pub use syscalls::reply;
148        pub use reply_authority::ImplicitReplyAuthority;
149    }
150}
151
152#[sel4_cfg(SET_TLS_BASE_SELF)]
153pub use syscalls::set_tls_base;
154
155pub use arch::top_level::*;
156
157pub(crate) use helper_macros::{
158    declare_cap_alias, declare_cap_type, declare_cap_type_for_object,
159    declare_cap_type_for_object_of_fixed_size, declare_cap_type_for_object_of_variable_size,
160    declare_fault_newtype, newtype_methods,
161};
162
163sel4_cfg_if! {
164    if #[sel4_cfg(PRINTING)] {
165        mod printing;
166
167        pub use printing::{DebugWrite, debug_put_char};
168    }
169}
170
171sel4_cfg_if! {
172    if #[sel4_cfg(DEBUG_BUILD)] {
173        mod debug;
174
175        pub use debug::{debug_snapshot, debug_halt};
176    }
177}
178
179sel4_cfg_if! {
180    if #[sel4_cfg(ENABLE_BENCHMARKS)] {
181        mod benchmark;
182
183        pub use benchmark::{
184            benchmark_reset_log,
185            benchmark_finalize_log,
186            benchmark_set_log_buffer,
187        };
188
189        sel4_cfg_if! {
190            if #[sel4_cfg(BENCHMARK_TRACK_UTILISATION)] {
191                pub use benchmark::{
192                    benchmark_get_thread_utilisation,
193                    benchmark_reset_thread_utilisation,
194                };
195
196                #[sel4_cfg(DEBUG_BUILD)]
197                pub use benchmark::{
198                    benchmark_dump_all_thread_utilisation,
199                    benchmark_reset_all_thread_utilisation,
200                };
201            }
202        }
203    }
204}
205
206#[cfg(feature = "state")]
207mod state;
208
209#[cfg(feature = "state")]
210pub use state::{
211    ImplicitInvocationContext, ipc_buffer_is_thread_local, set_ipc_buffer,
212    try_with_ipc_buffer_slot, try_with_ipc_buffer_slot_mut, with_ipc_buffer, with_ipc_buffer_mut,
213};
214
215/// Corresponds to `seL4_Word`.
216pub type Word = sys::seL4_Word;
217
218/// The size of [`Word`] in bits.
219pub const WORD_SIZE: usize = sel4_cfg_usize!(WORD_SIZE);
220
221#[doc(hidden)]
222pub mod _private {
223    #[sel4_config::sel4_cfg(PRINTING)]
224    pub use super::printing::_private as printing;
225}