1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6 7#pragma once 8 9 10#include <arch/kernel/vspace.h> 11 12static inline pte_t x86_make_device_pte(paddr_t phys) 13{ 14 return pte_new( 15 phys, /* page_base_address */ 16 0, /* avl */ 17 1, /* global */ 18 0, /* pat */ 19 0, /* dirty */ 20 0, /* accessed */ 21 1, /* cache_disabled */ 22 1, /* write_through */ 23 0, /* super_user */ 24 1, /* read_write */ 25 1 /* present */ 26 ); 27} 28 29static inline CONST pte_t x86_make_empty_pte(void) 30{ 31 return makeUserPTEInvalid(); 32} 33 34static inline CONST pde_t x86_make_empty_root_mapping(void) 35{ 36 return makeUserPDEInvalid(); 37} 38 39