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