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#include <config.h>
10#include <util.h>
11
12/*
13 *          2^64 +-------------------+
14 *               | Kernel Page PDPT  | --+
15 *   2^64 - 2^39 +-------------------+ PPTR_BASE
16 *               |    TLB Bitmaps    |   |
17 *               +-------------------+   |
18 *               |                   |   |
19 *               |     Unmapped      |   |
20 *               |                   |   |
21 *   2^64 - 2^47 +-------------------+   |
22 *               |                   |   |
23 *               |   Unaddressable   |   |
24 *               |                   |   |
25 *          2^47 +-------------------+ USER_TOP
26 *               |                   |   |
27 *               |       User        |   |
28 *               |                   |   |
29 *           0x0 +-------------------+   |
30 *                                       |
31 *                         +-------------+
32 *                         |
33 *                         v
34 *          2^64 +-------------------+
35 *               |                   |
36 *               |                   |     +------+      +------+
37 *               |                   | --> |  PD  | -+-> |  PT  |
38 *               |  Kernel Devices   |     +------+  |   +------+
39 *               |                   |               |
40 *               |                   |               +-> Log Buffer
41 *               |                   |
42 *   2^64 - 2^30 +-------------------+ KDEV_BASE
43 *               |                   |
44 *               |                   |     +------+
45 *               |    Kernel ELF     | --> |  PD  |
46 *               |                   |     +------+
47 *               |                   |
48 *   2^64 - 2^29 +-------------------+ PPTR_TOP / KERNEL_ELF_BASE
49 *               |                   |
50 *               |  Physical Memory  |
51 *               |       Window      |
52 *               |                   |
53 *   2^64 - 2^39 +-------------------+ PPTR_BASE
54 */
55
56/* WARNING: some of these constants are also defined in linker.lds
57 * These constants are written out in full instead of using bit arithmetic
58 * because they need to defined like this in linker.lds
59 */
60
61/* Define USER_TOP to be 1 before the last address before sign extension occurs.
62 * This ensures that
63 *  1. user addresses never needed to be sign extended to be valid canonical addresses
64 *  2. the user cannot map the last page before addresses need sign extension. This prevents
65 *     the user doing a syscall as the very last instruction and the CPU calculated PC + 2
66 *     from being an invalid (non sign extended) address
67 */
68#define USER_TOP UL_CONST(0x7FFFFFFFFFFF)
69
70/* The first physical address to map into the kernel's physical memory
71 * window */
72#define PADDR_BASE UL_CONST(0x00000000)
73
74/* The base address in virtual memory to use for the 1:1 physical memory
75 * mapping. Our kernel window is 2^39 bits (2^9 * 1gb) and the virtual
76 * address range is 48 bits. Therefore our base is 2^48 - 2^39 */
77#define PPTR_BASE UL_CONST(0xffffff8000000000)
78
79/* Below the main kernel window we have any slots for the TLB bitmap */
80#define TLBBITMAP_PML4_RESERVED (TLBBITMAP_ROOT_ENTRIES * BIT(PML4_INDEX_OFFSET))
81#define TLBBITMAP_PPTR (PPTR_BASE - TLBBITMAP_PML4_RESERVED)
82
83/* The kernel binary itself is placed in the bottom 1gb of the top
84 * 2gb of virtual address space. This is so we can use the 'kernel'
85 * memory model of GCC, which requires all symbols to be linked
86 * within the top 2GiB of memory. This is (2^48 - 2 ^ 31) */
87#define PPTR_TOP UL_CONST(0xffffffff80000000)
88
89/* The physical memory address to use for mapping the kernel ELF */
90#define KERNEL_ELF_PADDR_BASE UL_CONST(0x00100000)
91
92/* Kernel mapping starts directly after the physical memory window */
93#define KERNEL_ELF_BASE (PPTR_TOP + KERNEL_ELF_PADDR_BASE)
94
95/* Put the kernel devices at the very beginning of the top
96 * 1GB. This means they are precisely after the kernel binary
97 * region. This is 2^48 - 2^30 */
98#define KDEV_BASE UL_CONST(0xffffffffc0000000)
99
100/* The kernel log buffer is a large page mapped into the second index
101 * of the page directory that is only otherwise used for the kernel
102 * device page table. */
103#ifdef CONFIG_KERNEL_LOG_BUFFER
104#define KS_LOG_PPTR (KDEV_BASE + BIT(seL4_LargePageBits))
105#endif
106
107#ifndef __ASSEMBLER__
108
109#include <basic_types.h>
110#include <plat/machine.h>
111#include <plat_mode/machine/hardware_gen.h>
112#include <arch/kernel/tlb_bitmap_defs.h>
113
114/* ensure the user top and tlb bitmap do not overlap if multicore */
115#ifdef ENABLE_SMP_SUPPORT
116compile_assert(user_top_tlbbitmap_no_overlap, GET_PML4_INDEX(USER_TOP) != GET_PML4_INDEX(TLBBITMAP_PPTR))
117#endif
118
119/* since we have two kernel VM windows, we have two pptr to paddr
120 * conversion functions.
121 * paddr_to_kpptr converts physical address to the second small kernel
122 * window which locates at the top 2GiB.
123 */
124static inline void *CONST
125paddr_to_kpptr(paddr_t paddr)
126{
127    assert(paddr < KERNEL_ELF_PADDR_TOP);
128    return (void *)(paddr + KERNEL_ELF_BASE_OFFSET);
129}
130
131static inline paddr_t CONST kpptr_to_paddr(void *pptr)
132{
133    assert((word_t)pptr >= KERNEL_ELF_BASE);
134    return (paddr_t)pptr - KERNEL_ELF_BASE_OFFSET;
135}
136
137#endif /* __ASSEMBLER__ */
138
139