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#pragma once 13 14#include <autoconf.h> 15#include <stddef.h> 16#include <utils/attribute.h> 17#include <sel4/sel4.h> 18 19/* ordered list of page sizes for this architecture */ 20static const UNUSED size_t sel4_page_sizes[] = { 21 seL4_PageBits, 22 seL4_LargePageBits, 23#ifdef CONFIG_HUGE_PAGE 24 seL4_HugePageBits, 25#endif 26}; 27 28#define seL4_ARCH_Page_Map seL4_X86_Page_Map 29#define seL4_ARCH_Page_MapIO seL4_X86_Page_MapIO 30#define seL4_ARCH_Page_Unmap seL4_X86_Page_Unmap 31#define seL4_ARCH_Page_GetAddress seL4_X86_Page_GetAddress 32#define seL4_ARCH_Page_GetAddress_t seL4_X86_Page_GetAddress_t 33#define seL4_ARCH_PageTable_Map seL4_X86_PageTable_Map 34#define seL4_ARCH_IOPageTable_Map seL4_X86_IOPageTable_Map 35#define seL4_ARCH_PageTable_Unmap seL4_X86_PageTable_Unmap 36#define seL4_ARCH_ASIDPool_Assign seL4_X86_ASIDPool_Assign 37#define seL4_ARCH_ASIDControl_MakePool seL4_X86_ASIDControl_MakePool 38#define seL4_ARCH_PageTableObject seL4_X86_PageTableObject 39#define seL4_ARCH_PageDirectoryObject seL4_X86_PageDirectoryObject 40#define seL4_ARCH_Default_VMAttributes seL4_X86_Default_VMAttributes 41#define seL4_ARCH_VMAttributes seL4_X86_VMAttributes 42#define seL4_ARCH_4KPage seL4_X86_4K 43#define seL4_ARCH_Uncached_VMAttributes seL4_X86_CacheDisabled 44#define seL4_ARCH_LargePageObject seL4_X86_LargePageObject 45/* for size of a large page object use seL4_LargePageBits */ 46#define ARCHPageGetAddress X86PageGetAddress 47 48