From 4bb641ffe9ff7849a6821ff4b6caff88bad6bc04 Mon Sep 17 00:00:00 2001 From: Mark Old Date: Mon, 30 Mar 2026 12:18:40 -0700 Subject: [PATCH] Add remaining WithMRs variants and wrappers Add WithMRs variants at the sys level for: NBRecv, ReplyRecv, and (MCS-only) NBSendRecv, NBSendWait, NBWait. Add high-level wrappers for every IPC syscall that was missing one: - Endpoint: nb_send_with_mrs, nb_recv_with_mrs, reply_recv_with_mrs - Notification: wait_with_mrs, nb_wait, nb_wait_with_mrs, poll - Cap: nb_send_recv_with_mrs, nb_send_wait, nb_send_wait_with_mrs - Standalone: reply_with_mrs Signed-off-by: Mark Old --- crates/sel4/src/syscalls.rs | 212 ++++++++++++++++++++++++ crates/sel4/sys/src/syscalls/calls.rs | 228 ++++++++++++++++++++++++++ 2 files changed, 440 insertions(+) diff --git a/crates/sel4/src/syscalls.rs b/crates/sel4/src/syscalls.rs index 1a95bcad7..573735881 100644 --- a/crates/sel4/src/syscalls.rs +++ b/crates/sel4/src/syscalls.rs @@ -67,6 +67,20 @@ impl cap::Endpoint { }) } + pub fn nb_send_with_mrs(self, info: MessageInfo, messages: T) { + let [msg0, msg1, msg2, msg3] = messages.prepare_in(); + self.invoke(|cptr, ipc_buffer| { + ipc_buffer.inner_mut().seL4_NBSendWithMRs( + cptr.bits(), + info.into_inner(), + msg0, + msg1, + msg2, + msg3, + ) + }) + } + /// Corresponds to `seL4_Recv`. pub fn recv(self, reply_authority: impl ConveysReplyAuthority) -> (MessageInfo, Badge) { let (raw_msg_info, badge) = self.invoke(|cptr, ipc_buffer| { @@ -134,6 +148,28 @@ impl cap::Endpoint { }) } + pub fn nb_recv_with_mrs(self, reply_authority: impl ConveysReplyAuthority) -> RecvWithMRs { + let mut msg = [0; NUM_FAST_MESSAGE_REGISTERS]; + let [mr0, mr1, mr2, mr3] = &mut msg; + let (raw_msg_info, badge) = self.invoke(|cptr, ipc_buffer| { + ipc_buffer.inner_mut().seL4_NBRecvWithMRs( + cptr.bits(), + Some(mr0), + Some(mr1), + Some(mr2), + Some(mr3), + reply_authority + .into_reply_authority() + .into_sys_reply_authority(), + ) + }); + RecvWithMRs { + info: MessageInfo::from_inner(raw_msg_info), + badge, + msg, + } + } + pub fn recv_with_mrs(self, reply_authority: impl ConveysReplyAuthority) -> RecvWithMRs { let mut msg = [0; NUM_FAST_MESSAGE_REGISTERS]; let [mr0, mr1, mr2, mr3] = &mut msg; @@ -156,6 +192,34 @@ impl cap::Endpoint { } } + pub fn reply_recv_with_mrs( + self, + info: MessageInfo, + messages: T, + reply_authority: impl ConveysReplyAuthority, + ) -> RecvWithMRs { + let mut msg = messages.prepare_in_out(); + let [mr0, mr1, mr2, mr3] = &mut msg; + let (raw_msg_info, badge) = self.invoke(|cptr, ipc_buffer| { + ipc_buffer.inner_mut().seL4_ReplyRecvWithMRs( + cptr.bits(), + info.into_inner(), + Some(mr0), + Some(mr1), + Some(mr2), + Some(mr3), + reply_authority + .into_reply_authority() + .into_sys_reply_authority(), + ) + }); + RecvWithMRs { + info: MessageInfo::from_inner(raw_msg_info), + badge, + msg, + } + } + pub fn call_with_mrs(self, info: MessageInfo, messages: T) -> CallWithMRs { let mut msg = messages.prepare_in_out(); let [mr0, mr1, mr2, mr3] = &mut msg; @@ -188,6 +252,61 @@ impl cap::Notification { self.invoke(|cptr, ipc_buffer| ipc_buffer.inner_mut().seL4_Wait(cptr.bits())); (wait_message_info_from_sys(info), badge) } + + #[sel4_cfg(KERNEL_MCS)] + pub fn wait_with_mrs(self) -> WaitWithMRs { + let mut msg = [0; NUM_FAST_MESSAGE_REGISTERS]; + let [mr0, mr1, mr2, mr3] = &mut msg; + let (raw_msg_info, badge) = self.invoke(|cptr, ipc_buffer| { + ipc_buffer.inner_mut().seL4_WaitWithMRs( + cptr.bits(), + Some(mr0), + Some(mr1), + Some(mr2), + Some(mr3), + ) + }); + WaitWithMRs { + info: wait_message_info_from_sys(raw_msg_info), + badge, + msg, + } + } + + /// Corresponds to `seL4_NBWait`. + #[sel4_cfg(KERNEL_MCS)] + pub fn nb_wait(self) -> (WaitMessageInfo, Badge) { + let (info, badge) = + self.invoke(|cptr, ipc_buffer| ipc_buffer.inner_mut().seL4_NBWait(cptr.bits())); + (wait_message_info_from_sys(info), badge) + } + + #[sel4_cfg(KERNEL_MCS)] + pub fn nb_wait_with_mrs(self) -> WaitWithMRs { + let mut msg = [0; NUM_FAST_MESSAGE_REGISTERS]; + let [mr0, mr1, mr2, mr3] = &mut msg; + let (raw_msg_info, badge) = self.invoke(|cptr, ipc_buffer| { + ipc_buffer.inner_mut().seL4_NBWaitWithMRs( + cptr.bits(), + Some(mr0), + Some(mr1), + Some(mr2), + Some(mr3), + ) + }); + WaitWithMRs { + info: wait_message_info_from_sys(raw_msg_info), + badge, + msg, + } + } + + /// Corresponds to `seL4_Poll`. + pub fn poll(self) -> (MessageInfo, Badge) { + let (raw_msg_info, badge) = + self.invoke(|cptr, ipc_buffer| ipc_buffer.inner_mut().seL4_Poll(cptr.bits())); + (MessageInfo::from_inner(raw_msg_info), badge) + } } #[sel4_cfg(KERNEL_MCS)] @@ -224,6 +343,81 @@ impl Cap { }); (MessageInfo::from_inner(raw_msg_info), badge) } + + /// Corresponds to `seL4_NBSendRecvWithMRs`. + #[sel4_cfg(KERNEL_MCS)] + pub fn nb_send_recv_with_mrs( + self, + info: MessageInfo, + messages: M, + src: Cap, + reply_authority: impl ConveysReplyAuthority, + ) -> RecvWithMRs { + let mut msg = messages.prepare_in_out(); + let [mr0, mr1, mr2, mr3] = &mut msg; + let (raw_msg_info, badge) = self.invoke(|cptr, ipc_buffer| { + ipc_buffer.inner_mut().seL4_NBSendRecvWithMRs( + cptr.bits(), + info.into_inner(), + src.bits(), + Some(mr0), + Some(mr1), + Some(mr2), + Some(mr3), + reply_authority + .into_reply_authority() + .into_sys_reply_authority(), + ) + }); + RecvWithMRs { + info: MessageInfo::from_inner(raw_msg_info), + badge, + msg, + } + } + + /// Corresponds to `seL4_NBSendWait`. + #[sel4_cfg(KERNEL_MCS)] + pub fn nb_send_wait( + self, + info: MessageInfo, + src: Cap, + ) -> (MessageInfo, Badge) { + let (raw_msg_info, badge) = self.invoke(|cptr, ipc_buffer| { + ipc_buffer + .inner_mut() + .seL4_NBSendWait(cptr.bits(), info.into_inner(), src.bits()) + }); + (MessageInfo::from_inner(raw_msg_info), badge) + } + + /// Corresponds to `seL4_NBSendWaitWithMRs`. + #[sel4_cfg(KERNEL_MCS)] + pub fn nb_send_wait_with_mrs( + self, + info: MessageInfo, + messages: M, + src: Cap, + ) -> RecvWithMRs { + let mut msg = messages.prepare_in_out(); + let [mr0, mr1, mr2, mr3] = &mut msg; + let (raw_msg_info, badge) = self.invoke(|cptr, ipc_buffer| { + ipc_buffer.inner_mut().seL4_NBSendWaitWithMRs( + cptr.bits(), + info.into_inner(), + src.bits(), + Some(mr0), + Some(mr1), + Some(mr2), + Some(mr3), + ) + }); + RecvWithMRs { + info: MessageInfo::from_inner(raw_msg_info), + badge, + msg, + } + } } /// Corresponds to `seL4_Reply`. @@ -232,6 +426,16 @@ pub fn reply(ipc_buffer: &mut IpcBuffer, info: MessageInfo) { ipc_buffer.inner_mut().seL4_Reply(info.into_inner()) } +/// Corresponds to `seL4_ReplyWithMRs`. +#[sel4_cfg(not(KERNEL_MCS))] +#[allow(dead_code)] +pub fn reply_with_mrs(ipc_buffer: &mut IpcBuffer, info: MessageInfo, messages: T) { + let [msg0, msg1, msg2, msg3] = messages.prepare_in(); + ipc_buffer + .inner_mut() + .seL4_ReplyWithMRs(info.into_inner(), msg0, msg1, msg2, msg3) +} + /// Corresponds to `seL4_Yield`. pub fn r#yield() { sys::seL4_Yield() @@ -260,6 +464,14 @@ pub struct CallWithMRs { pub msg: [Word; NUM_FAST_MESSAGE_REGISTERS], } +/// The result of [`cap::Notification::wait_with_mrs`]. +#[sel4_cfg(KERNEL_MCS)] +pub struct WaitWithMRs { + pub info: WaitMessageInfo, + pub badge: Badge, + pub msg: [Word; NUM_FAST_MESSAGE_REGISTERS], +} + type ConcreteFastMessagesForIn = [Option; NUM_FAST_MESSAGE_REGISTERS]; type ConcreteFastMessagesForInOut = [Word; NUM_FAST_MESSAGE_REGISTERS]; diff --git a/crates/sel4/sys/src/syscalls/calls.rs b/crates/sel4/sys/src/syscalls/calls.rs index 35e3423ac..65f7cc1e8 100644 --- a/crates/sel4/sys/src/syscalls/calls.rs +++ b/crates/sel4/sys/src/syscalls/calls.rs @@ -279,6 +279,18 @@ impl seL4_IPCBuffer { ret } + pub fn seL4_NBRecvWithMRs( + &mut self, + src: seL4_CPtr, + msg0: Option<&mut seL4_Word>, + msg1: Option<&mut seL4_Word>, + msg2: Option<&mut seL4_Word>, + msg3: Option<&mut seL4_Word>, + reply_authority: ReplyAuthority, + ) -> (seL4_MessageInfo, seL4_Word) { + seL4_NBRecvWithMRsWithoutIPCBuffer(src, msg0, msg1, msg2, msg3, reply_authority) + } + pub fn seL4_Call(&mut self, dest: seL4_CPtr, msg_info: seL4_MessageInfo) -> seL4_MessageInfo { let mut mr0; let mut mr1; @@ -344,6 +356,27 @@ impl seL4_IPCBuffer { ret } + pub fn seL4_ReplyRecvWithMRs( + &mut self, + src: seL4_CPtr, + msg_info: seL4_MessageInfo, + msg0: Option<&mut seL4_Word>, + msg1: Option<&mut seL4_Word>, + msg2: Option<&mut seL4_Word>, + msg3: Option<&mut seL4_Word>, + reply_authority: ReplyAuthority, + ) -> (seL4_MessageInfo, seL4_Word) { + seL4_ReplyRecvWithMRsWithoutIPCBuffer( + src, + msg_info, + msg0, + msg1, + msg2, + msg3, + reply_authority, + ) + } + sel4_cfg_if! { if #[sel4_cfg(KERNEL_MCS)] { pub fn seL4_NBSendRecv( @@ -377,6 +410,20 @@ impl seL4_IPCBuffer { ret } + pub fn seL4_NBSendRecvWithMRs( + &mut self, + dest: seL4_CPtr, + msg_info: seL4_MessageInfo, + src: seL4_CPtr, + msg0: Option<&mut seL4_Word>, + msg1: Option<&mut seL4_Word>, + msg2: Option<&mut seL4_Word>, + msg3: Option<&mut seL4_Word>, + reply_authority: ReplyAuthority, + ) -> (seL4_MessageInfo, seL4_Word) { + seL4_NBSendRecvWithMRsWithoutIPCBuffer(dest, msg_info, src, msg0, msg1, msg2, msg3, reply_authority) + } + pub fn seL4_NBSendWait( &mut self, dest: seL4_CPtr, @@ -407,6 +454,19 @@ impl seL4_IPCBuffer { ret } + pub fn seL4_NBSendWaitWithMRs( + &mut self, + dest: seL4_CPtr, + msg_info: seL4_MessageInfo, + src: seL4_CPtr, + msg0: Option<&mut seL4_Word>, + msg1: Option<&mut seL4_Word>, + msg2: Option<&mut seL4_Word>, + msg3: Option<&mut seL4_Word>, + ) -> (seL4_MessageInfo, seL4_Word) { + seL4_NBSendWaitWithMRsWithoutIPCBuffer(dest, msg_info, src, msg0, msg1, msg2, msg3) + } + pub fn seL4_Wait(&mut self, src: seL4_CPtr) -> (WaitMessageInfo, seL4_Word) { let mut mr0 = 0; let mut mr1 = 0; @@ -460,6 +520,17 @@ impl seL4_IPCBuffer { ret } + + pub fn seL4_NBWaitWithMRs( + &mut self, + src: seL4_CPtr, + msg0: Option<&mut seL4_Word>, + msg1: Option<&mut seL4_Word>, + msg2: Option<&mut seL4_Word>, + msg3: Option<&mut seL4_Word>, + ) -> (WaitMessageInfo, seL4_Word) { + seL4_NBWaitWithMRsWithoutIPCBuffer(src, msg0, msg1, msg2, msg3) + } } else { pub fn seL4_Wait(&mut self, src: seL4_CPtr) -> (WaitMessageInfo, seL4_Word) { @@ -563,6 +634,66 @@ pub fn seL4_RecvWithMRsWithoutIPCBuffer( ret } +pub fn seL4_NBRecvWithMRsWithoutIPCBuffer( + src: seL4_CPtr, + msg0: Option<&mut seL4_Word>, + msg1: Option<&mut seL4_Word>, + msg2: Option<&mut seL4_Word>, + msg3: Option<&mut seL4_Word>, + reply_authority: ReplyAuthority, +) -> (seL4_MessageInfo, seL4_Word) { + let mut mr0 = 0; + let mut mr1 = 0; + let mut mr2 = 0; + let mut mr3 = 0; + + let ret = sys_recv( + syscall_id::NBRecv, + src, + &mut mr0, + &mut mr1, + &mut mr2, + &mut mr3, + reply_authority_to_sys_arg(reply_authority), + ); + + empty_mrs_to_args!(mr0, mr1, mr2, mr3, msg0, msg1, msg2, msg3,); + + ret +} + +pub fn seL4_ReplyRecvWithMRsWithoutIPCBuffer( + src: seL4_CPtr, + msg_info: seL4_MessageInfo, + msg0: Option<&mut seL4_Word>, + msg1: Option<&mut seL4_Word>, + msg2: Option<&mut seL4_Word>, + msg3: Option<&mut seL4_Word>, + reply_authority: ReplyAuthority, +) -> (seL4_MessageInfo, seL4_Word) { + let mut mr0; + let mut mr1; + let mut mr2; + let mut mr3; + + fill_mrs_from_args!(msg_info, mr0, mr1, mr2, mr3, msg0, msg1, msg2, msg3,); + + let ret = sys_send_recv( + syscall_id::ReplyRecv, + src, + msg_info, + &mut mr0, + &mut mr1, + &mut mr2, + &mut mr3, + reply_authority_to_sys_arg(reply_authority), + ); + + empty_mrs_to_args!(mr0, mr1, mr2, mr3, msg0, msg1, msg2, msg3,); + + ret +} + pub fn seL4_CallWithMRsWithoutIPCBuffer( dest: seL4_CPtr, msg_info: seL4_MessageInfo, @@ -622,6 +753,103 @@ pub fn seL4_WaitWithMRsWithoutIPCBuffer( ret } +#[sel4_cfg(KERNEL_MCS)] +pub fn seL4_NBSendRecvWithMRsWithoutIPCBuffer( + dest: seL4_CPtr, + msg_info: seL4_MessageInfo, + src: seL4_CPtr, + msg0: Option<&mut seL4_Word>, + msg1: Option<&mut seL4_Word>, + msg2: Option<&mut seL4_Word>, + msg3: Option<&mut seL4_Word>, + reply_authority: ReplyAuthority, +) -> (seL4_MessageInfo, seL4_Word) { + let mut mr0; + let mut mr1; + let mut mr2; + let mut mr3; + + fill_mrs_from_args!(msg_info, mr0, mr1, mr2, mr3, msg0, msg1, msg2, msg3,); + + let ret = sys_nb_send_recv( + syscall_id::NBSendRecv, + dest, + src, + msg_info, + &mut mr0, + &mut mr1, + &mut mr2, + &mut mr3, + reply_authority_to_sys_arg(reply_authority), + ); + + empty_mrs_to_args!(mr0, mr1, mr2, mr3, msg0, msg1, msg2, msg3,); + + ret +} + +#[sel4_cfg(KERNEL_MCS)] +pub fn seL4_NBSendWaitWithMRsWithoutIPCBuffer( + dest: seL4_CPtr, + msg_info: seL4_MessageInfo, + src: seL4_CPtr, + msg0: Option<&mut seL4_Word>, + msg1: Option<&mut seL4_Word>, + msg2: Option<&mut seL4_Word>, + msg3: Option<&mut seL4_Word>, +) -> (seL4_MessageInfo, seL4_Word) { + let mut mr0; + let mut mr1; + let mut mr2; + let mut mr3; + + fill_mrs_from_args!(msg_info, mr0, mr1, mr2, mr3, msg0, msg1, msg2, msg3,); + + let ret = sys_nb_send_recv( + syscall_id::NBSendWait, + 0, + src, + msg_info, + &mut mr0, + &mut mr1, + &mut mr2, + &mut mr3, + dest, + ); + + empty_mrs_to_args!(mr0, mr1, mr2, mr3, msg0, msg1, msg2, msg3,); + + ret +} + +#[sel4_cfg(KERNEL_MCS)] +pub fn seL4_NBWaitWithMRsWithoutIPCBuffer( + src: seL4_CPtr, + msg0: Option<&mut seL4_Word>, + msg1: Option<&mut seL4_Word>, + msg2: Option<&mut seL4_Word>, + msg3: Option<&mut seL4_Word>, +) -> (WaitMessageInfo, seL4_Word) { + let mut mr0 = 0; + let mut mr1 = 0; + let mut mr2 = 0; + let mut mr3 = 0; + + let ret = sys_recv( + syscall_id::NBWait, + src, + &mut mr0, + &mut mr1, + &mut mr2, + &mut mr3, + UNUSED_REPLY_ARG, + ); + + empty_mrs_to_args!(mr0, mr1, mr2, mr3, msg0, msg1, msg2, msg3,); + + ret +} + pub fn seL4_Yield() { sys_null(syscall_id::Yield); fence!();