main.c

#include <allocman/allocman.h>
#include <allocman/bootstrap.h>
#include <allocman/vka.h>
#include <cpio/cpio.h>
#include <sel4platsupport/bootinfo.h>
#include <sel4utils/process.h>
#include <sel4utils/vspace.h>
#include <simple-default/simple-default.h>
#include <simple/simple.h>
#include <stdio.h>

#define ALLOCATOR_STATIC_POOL_SIZE (BIT(seL4_PageBits) * 10)
#define ALLOCATOR_VIRTUAL_POOL_SIZE (BIT(seL4_PageBits) * 100)


/* global state */
allocman_t *allocman;
vka_object_t endpoint;
simple_t simple;
vka_t vka;
vspace_t vspace;
cspacepath_t IPCCapRecv;

UNUSED static char allocman_mem[ALLOCATOR_STATIC_POOL_SIZE];
UNUSED static sel4utils_alloc_data_t data;

#define APP_BADGE 1
sel4utils_process_t app_pcb;
vka_object_t app_ep;

void init(void)
{
    UNUSED int err = 0;

    NAME_THREAD(seL4_CapInitThreadTCB, "root");

    // get boot info
    seL4_BootInfo *info = platsupport_get_bootinfo();
    ZF_LOGF_IF(info == NULL, "failed to get bootinfo\n");

    // init simple
    simple_default_init_bootinfo(&simple, info);

    // initialise the allocator
    allocman = bootstrap_use_bootinfo(info, ALLOCATOR_STATIC_POOL_SIZE, allocman_mem);
    ZF_LOGF_IF(allocman == NULL, "failed to initialize allocator\n");

    // create a vka (interface for interacting with the kernel allocator)
    allocman_make_vka(&vka, allocman);

    // manage our own root server VSpace using this newly created allocator.
    err =
        sel4utils_bootstrap_vspace_with_bootinfo_leaky(&vspace, &data, seL4_CapInitThreadPD, &vka, info);
    ZF_LOGF_IFERR(err, "failed to bootstrap root vspace\n");

    /* fill the allocator with virtual memory */
    void *vaddr;
    UNUSED reservation_t virtual_reservation;

    virtual_reservation = vspace_reserve_range(&vspace, ALLOCATOR_VIRTUAL_POOL_SIZE, seL4_AllRights, 1, &vaddr);
    ZF_LOGF_IF(virtual_reservation.res == NULL, "failed to provide virtual memory");
    bootstrap_configure_virtual_pool(allocman, vaddr, ALLOCATOR_VIRTUAL_POOL_SIZE, seL4_CapInitThreadPD);

    err = vka_alloc_endpoint(&vka, &endpoint);
    ZF_LOGF_IFERR(err, "failed to allocate endpoint\n");

    printf("root initialised\n");
}

void spawn(simple_t *simple, sel4utils_process_t *pcb, seL4_Word badge, char *name)
{
    ZF_LOGF_IF(name == NULL, "invalid name, refuse to create new process");

    // configure process
    sel4utils_process_config_t config = process_config_default_simple(simple, name, seL4_MaxPrio);
    int error = sel4utils_configure_process_custom(pcb, &vka, &vspace, config);
    ZF_LOGF_IFERR(error, "failed to setup new process\n");

    // mint ep cap
    cspacepath_t re_path;
    vka_cspace_make_path(&vka, endpoint.cptr, &re_path);
    seL4_CPtr ep = sel4utils_mint_cap_to_process(pcb, re_path, seL4_AllRights, badge);

    // prepare args, and spawn the process
    char string_args[1][WORD_STRING_SIZE];
    char *argv[1];
    sel4utils_create_word_args(string_args, argv, 1, ep);

    printf("starting %s\n", name);
    error = sel4utils_spawn_process_v(pcb, &vka, &vspace, 1, argv, 1);
    ZF_LOGF_IFERR(error, "failed to spawn process %s\n", name);

    return 0;
}

sel4utils_process_t *pcb_from_badge(seL4_Word badge)
{
    return badge == APP_BADGE ? &app_pcb : NULL /* ... */;
}

void handle_req_ep(sel4utils_process_t *pcb)
{
    printf("app requested new endpoint from root\n");

    // allocate new endpoint, and track it
    vka_alloc_endpoint(&vka, &app_ep);

    cspacepath_t ep_cap_path;
    vka_cspace_make_path(&vka, app_ep.cptr, &ep_cap_path);

    // seL4_CPtr c = sel4utils_copy_cap_to_process(pcb, &vka, app_ep.cptr);
    seL4_CPtr new_ep_cap = sel4utils_mint_cap_to_process(pcb, ep_cap_path,
                                               seL4_AllRights, APP_BADGE);

    seL4_MessageInfo_t info = seL4_MessageInfo_new(0, 0, 1, 1);
    seL4_SetCap(0, new_ep_cap);
    seL4_SetMR(0, 0x2E2E2E2E);
    seL4_Reply(info);

    printf("root send to ep\n");
    seL4_MessageInfo_t msg = seL4_MessageInfo_new(0, 0, 0, 1);
    seL4_SetMR(0, 0xEFEFEFEF);
    seL4_Send(app_ep.cptr, msg);
}

int main(void)
{
    printf("==========================================================\n");
    printf("==                     main started                     ==\n");
    printf("==========================================================\n");

    // initialise root task
    init();

    printf("root ep: 0x%x\n", endpoint.cptr);

    // spawn processes
    spawn(&simple, &app_pcb, APP_BADGE, "app");

    // wait for IPC request
    seL4_Word badge;
    seL4_MessageInfo_t msg = seL4_Recv(endpoint.cptr, &badge);

    handle_req_ep(pcb_from_badge(badge));

    while (true) ;

    return 0;
}