diff --git a/repos/base-sel4/doc/ipc_and_virt_mem.txt b/repos/base-sel4/doc/ipc_and_virt_mem.txt index b379c2165..d29d35567 100644 --- a/repos/base-sel4/doc/ipc_and_virt_mem.txt +++ b/repos/base-sel4/doc/ipc_and_virt_mem.txt @@ -184,6 +184,13 @@ single RPC call. That said, the simple capability-delegation test works as expected. +When repeatedly performing an IPC call with a delegated capability, the +RECV_CAP index will be populated by the first call. Subsequent attempts to +override the RECV_CAP capability do not work (the 'extraCaps' field of the +received message info remains 0). The receiver has to make sure that the +specified 'CapReceivePath' is an empty capability slot. I.e., by calling +'seL4_CNode_Delete' prior 'seL4_Wait'. + Translation of capabilities aka "unwrapping" ============================================ diff --git a/repos/base-sel4/src/test/sel4/main.cc b/repos/base-sel4/src/test/sel4/main.cc index 2e87bfc9f..27d4d4d38 100644 --- a/repos/base-sel4/src/test/sel4/main.cc +++ b/repos/base-sel4/src/test/sel4/main.cc @@ -100,6 +100,9 @@ void second_thread_entry() for (;;) { seL4_SetCapReceivePath(seL4_CapInitThreadCNode, RECV_CAP, 32); + seL4_CNode_Delete(seL4_CapInitThreadCNode, RECV_CAP, 32); + + PDBG("call seL4_Wait"); seL4_MessageInfo_t msg_info = seL4_Wait(EP_CAP, nullptr); PDBG("returned from seL4_Wait, call seL4_Reply"); @@ -241,6 +244,17 @@ int main() PDBG("returned from seL4_Call"); } + PDBG("seL4_Call, delegating a TCB capability"); + { + seL4_MessageInfo_t msg_info = seL4_MessageInfo_new(13, 0, 1, 0); + + seL4_SetCap(0, SECOND_THREAD_CAP); + + seL4_Call(EP_CAP, msg_info); + + PDBG("returned from seL4_Call"); + } + PDBG("seL4_Call, delegating a minted endpoint capability"); { /* mint EP_CAP into EP_MINTED_CAP */