1/* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 */ 12 13#pragma once 14 15#include <autoconf.h> 16#include <sel4/types.h> 17#include <allocman/cspace/cspace.h> 18#include <vka/vka.h> 19 20/* This is a proxy allocator that just passes any allocs/frees to a vka interface */ 21static inline cspacepath_t _cspace_vka_make_path(void *_cspace, seL4_CPtr slot) 22{ 23 vka_t *vka = (vka_t*)_cspace; 24 cspacepath_t path; 25 vka_cspace_make_path(vka, slot, &path); 26 return path; 27} 28 29static int _cspace_vka_alloc(struct allocman *alloc, void *_cspace, cspacepath_t *slot) 30{ 31 vka_t *vka = (vka_t*)_cspace; 32 (void)alloc; 33 return vka_cspace_alloc_path(vka, slot); 34} 35static void _cspace_vka_free(struct allocman *alloc, void *_cspace, const cspacepath_t *slot) 36{ 37 vka_t *vka = (vka_t*)_cspace; 38 (void)alloc; 39 vka_cspace_free(vka, slot->capPtr); 40} 41 42/** 43 * Make a cspace interface from a VKA. It is the responsibility of the caller to ensure 44 * that this pointer remains valid for as long as this cspace is used 45 * 46 * @param vka Allocator to proxy cspace calls to 47 * @return cspace_interface that can be given to allocman 48 */ 49static inline struct cspace_interface cspace_vka_make_interface(vka_t *vka) { 50 return (struct cspace_interface){ 51 .alloc = _cspace_vka_alloc, 52 .free = _cspace_vka_free, 53 .make_path = _cspace_vka_make_path, 54 /* VKA is not guaranteed to recurse */ 55 .properties = ALLOCMAN_DEFAULT_PROPERTIES, 56 .cspace = vka 57 }; 58} 59 60