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 <sel4vka/gen_config.h> 17 18#include <sel4/sel4.h> 19#include <sel4/types.h> 20#ifdef CONFIG_DEBUG_BUILD 21#include <sel4debug/debug.h> 22#endif 23#include <assert.h> 24#include <stdint.h> 25#include <utils/util.h> 26#include <vka/cspacepath_t.h> 27 28/** 29 * Allocate a slot in a cspace. 30 * 31 * @param data cookie for the underlying allocator 32 * @param res pointer to a cptr to store the allocated slot 33 * @return 0 on success 34 */ 35typedef int (*vka_cspace_alloc_fn)(void *data, seL4_CPtr *res); 36 37/** 38 * Convert an allocated cptr to a cspacepath, for use in 39 * operations such as Untyped_Retype 40 * 41 * @param data cookie for the underlying allocator 42 * @param slot a cslot allocated by the cspace alloc function 43 * @param res pointer to a cspacepath struct to fill out 44 */ 45typedef void (*vka_cspace_make_path_fn)(void *data, seL4_CPtr slot, cspacepath_t *res); 46 47/** 48 * Free an allocated cslot 49 * 50 * @param data cookie for the underlying allocator 51 * @param slot a cslot allocated by the cspace alloc function 52 */ 53typedef void (*vka_cspace_free_fn)(void *data, seL4_CPtr slot); 54 55/** 56 * Allocate a portion of an untyped into an object 57 * 58 * @param data cookie for the underlying allocator 59 * @param dest path to an empty cslot to place the cap to the allocated object 60 * @param type the seL4 object type to allocate (as passed to Untyped_Retype) 61 * @param size_bits the size of the object to allocate (as passed to Untyped_Retype) 62 * @param res pointer to a location to store the cookie representing this allocation 63 * @return 0 on success 64 */ 65typedef int (*vka_utspace_alloc_fn)(void *data, const cspacepath_t *dest, seL4_Word type, seL4_Word size_bits, 66 seL4_Word *res); 67 68/** 69 * Allocate a portion of an untyped into an object 70 * 71 * @param data cookie for the underlying allocator 72 * @param dest path to an empty cslot to place the cap to the allocated object 73 * @param type the seL4 object type to allocate (as passed to Untyped_Retype) 74 * @param size_bits the size of the object to allocate (as passed to Untyped_Retype) 75 * @param paddr The desired physical address that this object should start at 76 * @param cookie pointer to a location to store the cookie representing this allocation 77 * @return 0 on success 78 */ 79typedef int (*vka_utspace_alloc_at_fn)(void *data, const cspacepath_t *dest, seL4_Word type, seL4_Word size_bits, 80 uintptr_t paddr, seL4_Word *cookie); 81 82/** 83 * Allocate a portion of an untyped into an object 84 * 85 * @param data cookie for the underlying allocator 86 * @param dest path to an empty cslot to place the cap to the allocated object 87 * @param type the seL4 object type to allocate (as passed to Untyped_Retype) 88 * @param size_bits the size of the object to allocate (as passed to Untyped_Retype) 89 * @param can_use_dev whether the allocator can use device untyped instead of regular untyped 90 * @param res pointer to a location to store the cookie representing this allocation 91 * @return 0 on success 92 */ 93typedef int (*vka_utspace_alloc_maybe_device_fn)(void *data, const cspacepath_t *dest, seL4_Word type, 94 seL4_Word size_bits, bool can_use_dev, seL4_Word *res); 95 96/** 97 * Free a portion of an allocated untyped. Is the responsibility of the caller to 98 * have already deleted the object (by deleting all capabilities) first 99 * 100 * @param data cookie for the underlying allocator 101 * @param type the seL4 object type that was allocated (as passed to Untyped_Retype) 102 * @param size_bits the size of the object that was allocated (as passed to Untyped_Retype) 103 * @param target cookie to the allocation as given by the utspace alloc function 104 */ 105typedef void (*vka_utspace_free_fn)(void *data, seL4_Word type, seL4_Word size_bits, seL4_Word target); 106 107/** 108 * Request the physical address of an object. 109 * 110 * @param data cookie for the underlying allocator 111 * @param target cookie to the allocation as given by the utspace alloc function 112 * @param type the seL4 object type that was allocated (as passed to Untyped_Retype) 113 * @param size_bits the size of the object that was allocated (as passed to Untyped_Retype) 114 * @return paddr of object, or VKA_NO_PADDR on error 115 */ 116typedef uintptr_t (*vka_utspace_paddr_fn)(void *data, seL4_Word target, seL4_Word type, seL4_Word size_bits); 117 118#define VKA_NO_PADDR 1 119 120/* 121 * Generic Virtual Kernel Allocator (VKA) data structure. 122 * 123 * This is similar in concept to the Linux VFS structures, but for 124 * the seL4 kernel object allocator instead of the Linux file system. 125 * 126 * Alternatively, you can think of this as a abstract class in an 127 * OO hierarchy, of which has several implementations. 128 */ 129 130typedef struct vka { 131 void *data; 132 vka_cspace_alloc_fn cspace_alloc; 133 vka_cspace_make_path_fn cspace_make_path; 134 vka_utspace_alloc_fn utspace_alloc; 135 vka_utspace_alloc_maybe_device_fn utspace_alloc_maybe_device; 136 vka_utspace_alloc_at_fn utspace_alloc_at; 137 vka_cspace_free_fn cspace_free; 138 vka_utspace_free_fn utspace_free; 139 vka_utspace_paddr_fn utspace_paddr; 140} vka_t; 141 142static inline int vka_cspace_alloc(vka_t *vka, seL4_CPtr *res) 143{ 144 if (!vka) { 145 ZF_LOGE("vka is NULL"); 146 return -1; 147 } 148 149 if (!res) { 150 ZF_LOGE("res is NULL"); 151 return -1; 152 } 153 154 if (!vka->cspace_alloc) { 155 ZF_LOGE("Unimplemented"); 156 return -1; 157 } 158 159 return vka->cspace_alloc(vka->data, res); 160} 161 162static inline void vka_cspace_make_path(vka_t *vka, seL4_CPtr slot, cspacepath_t *res) 163{ 164 165 if (!res) { 166 ZF_LOGF("res is NULL"); 167 } 168 169 if (!vka) { 170 ZF_LOGF("vka is NULL"); 171 } 172 173 if (!vka->cspace_make_path) { 174 ZF_LOGF("Unimplmented"); 175 } 176 177 vka->cspace_make_path(vka->data, slot, res); 178} 179 180/* 181 * Wrapper functions to make calls more convenient 182 */ 183static inline int vka_cspace_alloc_path(vka_t *vka, cspacepath_t *res) 184{ 185 seL4_CPtr slot; 186 int error = vka_cspace_alloc(vka, &slot); 187 188 if (error == seL4_NoError) { 189 vka_cspace_make_path(vka, slot, res); 190 } 191 192 return error; 193} 194 195static inline void vka_cspace_free(vka_t *vka, seL4_CPtr slot) 196{ 197#ifdef CONFIG_DEBUG_BUILD 198 if (debug_cap_is_valid(slot)) { 199 ZF_LOGF("slot is not free: call vka_cnode_delete first"); 200 /* this terminates the system */ 201 } 202#endif 203 204 if (!vka->cspace_free) { 205 ZF_LOGE("Not implemented"); 206 return; 207 } 208 209 vka->cspace_free(vka->data, slot); 210} 211 212static inline void vka_cspace_free_path(vka_t *vka, cspacepath_t path) 213{ 214 vka_cspace_free(vka, path.capPtr); 215} 216 217static inline int vka_utspace_alloc(vka_t *vka, const cspacepath_t *dest, seL4_Word type, seL4_Word size_bits, 218 seL4_Word *res) 219{ 220 if (!vka) { 221 ZF_LOGE("vka is NULL"); 222 return -1; 223 } 224 225 if (!res) { 226 ZF_LOGE("res is NULL"); 227 return -1; 228 } 229 230 if (!vka->utspace_alloc) { 231 ZF_LOGE("Not implemented"); 232 return -1; 233 } 234 235 return vka->utspace_alloc(vka->data, dest, type, size_bits, res); 236} 237 238static inline int vka_utspace_alloc_maybe_device(vka_t *vka, const cspacepath_t *dest, seL4_Word type, 239 seL4_Word size_bits, bool can_use_dev, seL4_Word *res) 240{ 241 if (!vka) { 242 ZF_LOGE("vka is NULL"); 243 return -1; 244 } 245 246 if (!res) { 247 ZF_LOGE("res is NULL"); 248 return -1; 249 } 250 251 if (!vka->utspace_alloc_maybe_device) { 252 ZF_LOGE("Not implemented"); 253 return -1; 254 } 255 256 return vka->utspace_alloc_maybe_device(vka->data, dest, type, size_bits, can_use_dev, res); 257} 258 259static inline int vka_utspace_alloc_at(vka_t *vka, const cspacepath_t *dest, seL4_Word type, seL4_Word size_bits, 260 uintptr_t paddr, seL4_Word *cookie) 261{ 262 if (!vka) { 263 ZF_LOGE("vka is NULL"); 264 return -1; 265 } 266 if (!cookie) { 267 ZF_LOGE("cookie is NULL"); 268 return -1; 269 } 270 if (!vka->utspace_alloc_at) { 271 ZF_LOGE("Not implemented"); 272 return -1; 273 } 274 275 return vka->utspace_alloc_at(vka->data, dest, type, size_bits, paddr, cookie); 276} 277 278static inline void vka_utspace_free(vka_t *vka, seL4_Word type, seL4_Word size_bits, seL4_Word target) 279{ 280 if (!vka) { 281 ZF_LOGE("vka is NULL"); 282 return ; 283 } 284 285 if (!vka->utspace_free) { 286#ifndef CONFIG_LIB_VKA_ALLOW_MEMORY_LEAKS 287 ZF_LOGF("Not implemented"); 288 /* This terminates the system */ 289#endif 290 return; 291 } 292 293 vka->utspace_free(vka->data, type, size_bits, target); 294} 295 296static inline uintptr_t vka_utspace_paddr(vka_t *vka, seL4_Word target, seL4_Word type, seL4_Word size_bits) 297{ 298 299 if (!vka) { 300 ZF_LOGE("vka is NULL"); 301 return VKA_NO_PADDR; 302 } 303 304 if (!vka->utspace_paddr) { 305 ZF_LOGE("Not implemented"); 306 return VKA_NO_PADDR; 307 } 308 309 return vka->utspace_paddr(vka->data, target, type, size_bits); 310} 311 312