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 <sel4/types.h> 16#include <assert.h> 17#include <autoconf.h> 18#include <sel4vka/gen_config.h> 19#include <utils/util.h> 20#include <vka/sel4_arch/kobject_t.h> 21 22enum _x86_kobject_type { 23 KOBJECT_IO_PAGETABLE = KOBJECT_MODE_NUM_TYPES, 24 KOBJECT_PAGE_DIRECTORY, 25 KOBJECT_PAGE_TABLE, 26 KOBJECT_ARCH_NUM_TYPES, 27}; 28 29/* 30 * Get the size (in bits) of the untyped memory required to 31 * create an object of the given size. 32 */ 33static inline seL4_Word arch_kobject_get_size(kobject_t type, seL4_Word objectSize) 34{ 35 switch (type) { 36 case KOBJECT_IO_PAGETABLE: 37 return seL4_IOPageTableBits; 38 case KOBJECT_FRAME: 39 switch (objectSize) { 40 case seL4_PageBits: 41 case seL4_LargePageBits: 42 return objectSize; 43 } 44 /* If frame size was unknown fall through to default case as it 45 * might be a mode specific frame size */ 46 default: 47 return x86_mode_kobject_get_size(type, objectSize); 48 } 49} 50 51static inline seL4_Word arch_kobject_get_type(int type, seL4_Word objectSize) 52{ 53 switch (type) { 54 case KOBJECT_PAGE_DIRECTORY: 55 return seL4_X86_PageDirectoryObject; 56 case KOBJECT_PAGE_TABLE: 57 return seL4_X86_PageTableObject; 58 case KOBJECT_FRAME: 59 switch (objectSize) { 60 case seL4_PageBits: 61 return seL4_X86_4K; 62 case seL4_LargePageBits: 63 return seL4_X86_LargePageObject; 64 default: 65 return x86_mode_kobject_get_type(type, objectSize); 66 } 67 case KOBJECT_IO_PAGETABLE: 68 return seL4_X86_IOPageTableObject; 69 default: 70 return x86_mode_kobject_get_type(type, objectSize); 71 } 72} 73 74