Skip to content

Instantly share code, notes, and snippets.

@nuta
Created April 22, 2023 12:30
Show Gist options
  • Save nuta/61b1461798609eb1ef14e5e50b67c207 to your computer and use it in GitHub Desktop.
Save nuta/61b1461798609eb1ef14e5e50b67c207 to your computer and use it in GitHub Desktop.
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#define _assert_fail(msg, ...) do { puts(msg); exit(1); } while (0)
#define CONST __attribute__((__const__))
#define seL4_Null ((void*)0)
#define LIBSEL4_INLINE_FUNC static inline
typedef uint32_t seL4_CPtr;
typedef uint32_t seL4_Word;
typedef uint32_t seL4_MessageInfo_t;
typedef enum {
seL4_SysSend = -3,
} seL4_Syscall_ID;
typedef struct seL4_IPCBuffer_ {
seL4_Word msg[32];
} seL4_IPCBuffer __attribute__((__aligned__(sizeof(struct seL4_IPCBuffer_))));
__thread seL4_IPCBuffer *__sel4_ipc_buffer;
LIBSEL4_INLINE_FUNC seL4_IPCBuffer *seL4_GetIPCBuffer(void)
{
return __sel4_ipc_buffer;
}
LIBSEL4_INLINE_FUNC seL4_Word seL4_GetMR(int i)
{
return seL4_GetIPCBuffer()->msg[i];
}
LIBSEL4_INLINE_FUNC void seL4_SetMR(int i, seL4_Word mr)
{
seL4_GetIPCBuffer()->msg[i] = mr;
}
static inline void riscv_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1,
seL4_Word mr2, seL4_Word mr3)
{
register seL4_Word destptr asm("a0") = dest;
register seL4_Word info asm("a1") = info_arg;
/* Load beginning of the message into registers. */
register seL4_Word msg0 asm("a2") = mr0;
register seL4_Word msg1 asm("a3") = mr1;
register seL4_Word msg2 asm("a4") = mr2;
register seL4_Word msg3 asm("a5") = mr3;
/* Perform the system call. */
register seL4_Word scno asm("a7") = sys;
asm volatile(
"ecall"
: "+r"(destptr), "+r"(msg0), "+r"(msg1), "+r"(msg2),
"+r"(msg3), "+r"(info)
: "r"(scno)
);
}
static inline seL4_MessageInfo_t __attribute__((__const__))
seL4_MessageInfo_new(uint32_t label, uint32_t capsUnwrapped, uint32_t extraCaps, uint32_t length) {
seL4_MessageInfo_t seL4_MessageInfo;
/* fail if user has passed bits that we will override */
if(!((label & ~0xfffffu) == ((0 && (label & (1u << 31))) ? 0x0 : 0))) _assert_fail("(label & ~0xfffffu) == ((0 && (label & (1u << 31))) ? 0x0 : 0)", "/home/seiya/NeptuneOS/build-i386-debug/elf/kernel/generated/sel4/shared_types_gen.h", 94, __FUNCTION__);
if(!((capsUnwrapped & ~0x7u) == ((0 && (capsUnwrapped & (1u << 31))) ? 0x0 : 0))) _assert_fail("(capsUnwrapped & ~0x7u) == ((0 && (capsUnwrapped & (1u << 31))) ? 0x0 : 0)", "/home/seiya/NeptuneOS/build-i386-debug/elf/kernel/generated/sel4/shared_types_gen.h", 95, __FUNCTION__);
if(!((extraCaps & ~0x3u) == ((0 && (extraCaps & (1u << 31))) ? 0x0 : 0))) _assert_fail("(extraCaps & ~0x3u) == ((0 && (extraCaps & (1u << 31))) ? 0x0 : 0)", "/home/seiya/NeptuneOS/build-i386-debug/elf/kernel/generated/sel4/shared_types_gen.h", 96, __FUNCTION__);
if(!((length & ~0x7fu) == ((0 && (length & (1u << 31))) ? 0x0 : 0))) _assert_fail("(length & ~0x7fu) == ((0 && (length & (1u << 31))) ? 0x0 : 0)", "/home/seiya/NeptuneOS/build-i386-debug/elf/kernel/generated/sel4/shared_types_gen.h", 97, __FUNCTION__);
seL4_MessageInfo = 0
| (label & 0xfffffu) << 12
| (capsUnwrapped & 0x7u) << 9
| (extraCaps & 0x3u) << 7
| (length & 0x7fu) << 0;
return seL4_MessageInfo;
}
static inline uint32_t CONST
seL4_MessageInfo_get_length(seL4_MessageInfo_t seL4_MessageInfo) {
uint32_t ret;
ret = (seL4_MessageInfo & 0x7fu) >> 0;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1u << (31)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
riscv_sys_send(seL4_SysSend, dest, msgInfo,
mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
);
}
LIBSEL4_INLINE_FUNC void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
riscv_sys_send(seL4_SysSend, dest, msgInfo, seL4_GetMR(0), seL4_GetMR(1),
seL4_GetMR(2), seL4_GetMR(3));
}
// 本書で紹介したメッセージ送信ロジック
int main(void) {
seL4_CPtr dest = 123 /* 適当な値 */;
seL4_MessageInfo_t msgInfo = seL4_MessageInfo_new(0, 0, 0, 4);
seL4_SetMR(0, 1000);
seL4_SetMR(1, 1001);
seL4_SetMR(2, 1002);
seL4_SetMR(3, 1003);
seL4_Send(dest, msgInfo);
return 0;
}
// seL4_SendWithMRs を使ったメッセージ送信ロジック
int main_with_seL4_SendWithMRs(void) {
seL4_CPtr dest = 123 /* 適当な値 */;
seL4_MessageInfo_t msgInfo = seL4_MessageInfo_new(0, 0, 0, 4);
seL4_Word mr0 = 1000;
seL4_Word mr1 = 1001;
seL4_Word mr2 = 1002;
seL4_Word mr3 = 1003;
seL4_SendWithMRs(dest, msgInfo, &mr0, &mr1, &mr2, &mr3);
return 0;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment