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 <autoconf.h> 16#include <sel4utils/gen_config.h> 17#include <vka/vka.h> 18#include <vspace/vspace.h> 19 20#include <sel4utils/util.h> 21#include <sel4utils/mapping.h> 22#include <sel4utils/vspace.h> 23 24#define RESERVED UINTPTR_MAX 25#define EMPTY 0 26 27#define TOP_LEVEL_BITS_OFFSET (VSPACE_LEVEL_BITS * (VSPACE_NUM_LEVELS - 1) + PAGE_BITS_4K) 28#define LEVEL_MASK MASK_UNSAFE(VSPACE_LEVEL_BITS) 29 30#define INDEX_FOR_LEVEL(addr, l) ( ( (addr) >> ((l) * VSPACE_LEVEL_BITS + PAGE_BITS_4K)) & MASK(VSPACE_LEVEL_BITS)) 31#define TOP_LEVEL_INDEX(x) INDEX_FOR_LEVEL(x, VSPACE_NUM_LEVELS - 1) 32 33#define BYTES_FOR_LEVEL(l) BIT(VSPACE_LEVEL_BITS * (l) + PAGE_BITS_4K) 34#define ALIGN_FOR_LEVEL(l) (~(MASK(VSPACE_LEVEL_BITS * (l) + PAGE_BITS_4K))) 35 36void *create_level(vspace_t *vspace, size_t size); 37void *bootstrap_create_level(vspace_t *vspace, size_t size); 38 39static inline void *create_mid_level(vspace_t *vspace, uintptr_t init) 40{ 41 vspace_mid_level_t *level = create_level(vspace, sizeof(vspace_mid_level_t)); 42 if (level) { 43 for (int i = 0; i < VSPACE_LEVEL_SIZE; i++) { 44 level->table[i] = init; 45 } 46 } 47 return level; 48} 49 50static inline void *create_bottom_level(vspace_t *vspace, uintptr_t init) 51{ 52 vspace_bottom_level_t *level = create_level(vspace, sizeof(vspace_bottom_level_t)); 53 if (level) { 54 for (int i = 0; i < VSPACE_LEVEL_SIZE; i++) { 55 level->cap[i] = init; 56 level->cookie[i] = 0; 57 } 58 } 59 return level; 60} 61 62static inline sel4utils_alloc_data_t *get_alloc_data(vspace_t *vspace) 63{ 64 return (sel4utils_alloc_data_t *) vspace->data; 65} 66 67static int reserve_entries_bottom(vspace_t *vspace, vspace_bottom_level_t *level, uintptr_t start, uintptr_t end, 68 bool preserve_frames) 69{ 70 while (start < end) { 71 int index = INDEX_FOR_LEVEL(start, 0); 72 uintptr_t cap = level->cap[index]; 73 if (cap == RESERVED) { 74 ZF_LOGE("Attempting to reserve already reserved region"); 75 return -1; 76 } 77 if (cap != EMPTY && preserve_frames) { 78 return -1; 79 } 80 level->cap[index] = RESERVED; 81 level->cookie[index] = 0; 82 start += BYTES_FOR_LEVEL(0); 83 } 84 return 0; 85} 86 87static int reserve_entries_mid(vspace_t *vspace, vspace_mid_level_t *level, int level_num, uintptr_t start, 88 uintptr_t end, bool preserve_frames) 89{ 90 /* walk entries at this level until we complete this range */ 91 while (start < end) { 92 int index = INDEX_FOR_LEVEL(start, level_num); 93 /* align the start so we can check for alignment later */ 94 uintptr_t aligned_start = start & ALIGN_FOR_LEVEL(level_num); 95 /* calculate the start of the next index */ 96 uintptr_t next_start = aligned_start + BYTES_FOR_LEVEL(level_num); 97 int must_recurse = 0; 98 if (next_start > end) { 99 next_start = end; 100 must_recurse = 1; 101 } else if (start != aligned_start) { 102 must_recurse = 1; 103 } 104 uintptr_t next_table = level->table[index]; 105 if (next_table == RESERVED) { 106 ZF_LOGE("Tried to reserve already reserved region"); 107 return -1; 108 } 109 if (next_table == EMPTY) { 110 if (must_recurse) { 111 /* allocate new level */ 112 if (level_num == 1) { 113 next_table = (uintptr_t)create_bottom_level(vspace, EMPTY); 114 } else { 115 next_table = (uintptr_t)create_mid_level(vspace, EMPTY); 116 } 117 if (next_table == EMPTY) { 118 ZF_LOGE("Failed to allocate and map book keeping frames during bootstrapping"); 119 return -1; 120 } 121 } else { 122 next_table = RESERVED; 123 } 124 level->table[index] = next_table; 125 } 126 /* at this point table is either RESERVED or needs recursion */ 127 if (next_table != RESERVED) { 128 int error; 129 if (level_num == 1) { 130 error = reserve_entries_bottom(vspace, (vspace_bottom_level_t *)next_table, start, next_start, preserve_frames); 131 } else { 132 error = reserve_entries_mid(vspace, (vspace_mid_level_t *)next_table, level_num - 1, start, next_start, 133 preserve_frames); 134 } 135 if (error) { 136 return error; 137 } 138 } 139 start = next_start; 140 } 141 return 0; 142} 143 144static int clear_entries_bottom(vspace_t *vspace, vspace_bottom_level_t *level, uintptr_t start, uintptr_t end, 145 bool only_reserved) 146{ 147 while (start < end) { 148 int index = INDEX_FOR_LEVEL(start, 0); 149 uintptr_t cap = level->cap[index]; 150 if (cap != RESERVED && only_reserved) { 151 return -1; 152 } 153 level->cap[index] = EMPTY; 154 level->cookie[index] = 0; 155 start += BYTES_FOR_LEVEL(0); 156 } 157 return 0; 158} 159 160static int clear_entries_mid(vspace_t *vspace, vspace_mid_level_t *level, int level_num, uintptr_t start, uintptr_t end, 161 bool only_reserved) 162{ 163 /* walk entries at this level until we complete this range */ 164 while (start < end) { 165 int index = INDEX_FOR_LEVEL(start, level_num); 166 /* align the start so we can check for alignment later */ 167 uintptr_t aligned_start = start & ALIGN_FOR_LEVEL(level_num); 168 /* calculate the start of the next index */ 169 uintptr_t next_start = aligned_start + BYTES_FOR_LEVEL(level_num); 170 if (next_start > end) { 171 next_start = end; 172 } 173 uintptr_t next_table = level->table[index]; 174 if (next_table == RESERVED) { 175 ZF_LOGE("Cannot clear reserved entries mid level"); 176 return -1; 177 } 178 if (next_table != EMPTY) { 179 int error; 180 if (level_num == 1) { 181 error = clear_entries_bottom(vspace, (vspace_bottom_level_t *)next_table, start, next_start, only_reserved); 182 } else { 183 error = clear_entries_mid(vspace, (vspace_mid_level_t *)next_table, level_num - 1, start, next_start, only_reserved); 184 } 185 if (error) { 186 return error; 187 } 188 } 189 start = next_start; 190 } 191 return 0; 192} 193 194static int update_entries_bottom(vspace_t *vspace, vspace_bottom_level_t *level, uintptr_t start, uintptr_t end, 195 seL4_CPtr cap, uintptr_t cookie) 196{ 197 while (start < end) { 198 int index = INDEX_FOR_LEVEL(start, 0); 199 uintptr_t old_cap = level->cap[index]; 200 if (old_cap != RESERVED && old_cap != EMPTY) { 201 ZF_LOGE("Mapping neither reserved nor empty for vaddr %" PRIxPTR " (contains 0x%" PRIxPTR ")", start, old_cap); 202 return -1; 203 } 204 level->cap[index] = cap; 205 level->cookie[index] = cookie; 206 start += BYTES_FOR_LEVEL(0); 207 } 208 return 0; 209} 210 211static int update_entries_mid(vspace_t *vspace, vspace_mid_level_t *level, int level_num, uintptr_t start, 212 uintptr_t end, seL4_CPtr cap, uintptr_t cookie) 213{ 214 /* walk entries at this level until we complete this range */ 215 while (start < end) { 216 int index = INDEX_FOR_LEVEL(start, level_num); 217 /* align the start so we can check for alignment later */ 218 uintptr_t aligned_start = start & ALIGN_FOR_LEVEL(level_num); 219 /* calculate the start of the next index */ 220 uintptr_t next_start = aligned_start + BYTES_FOR_LEVEL(level_num); 221 if (next_start > end) { 222 next_start = end; 223 } 224 uintptr_t next_table = level->table[index]; 225 if (next_table == EMPTY || next_table == RESERVED) { 226 /* allocate new level */ 227 if (level_num == 1) { 228 next_table = (uintptr_t)create_bottom_level(vspace, next_table); 229 } else { 230 next_table = (uintptr_t)create_mid_level(vspace, next_table); 231 } 232 if (next_table == EMPTY) { 233 ZF_LOGE("Failed to allocate and map book keeping frames during bootstrapping"); 234 return -1; 235 } 236 level->table[index] = next_table; 237 } 238 int error; 239 if (level_num == 1) { 240 error = update_entries_bottom(vspace, (vspace_bottom_level_t *)next_table, start, next_start, cap, cookie); 241 } else { 242 error = update_entries_mid(vspace, (vspace_mid_level_t *)next_table, level_num - 1, start, next_start, cap, cookie); 243 } 244 if (error) { 245 return error; 246 } 247 start = next_start; 248 } 249 return 0; 250} 251 252static bool is_reserved_or_empty_bottom(vspace_bottom_level_t *level, uintptr_t start, uintptr_t end, uintptr_t good, 253 uintptr_t bad) 254{ 255 while (start < end) { 256 int index = INDEX_FOR_LEVEL(start, 0); 257 uintptr_t cap = level->cap[index]; 258 if (cap != good) { 259 return false; 260 } 261 start += BYTES_FOR_LEVEL(0); 262 } 263 return true; 264} 265 266static bool is_reserved_or_empty_mid(vspace_mid_level_t *level, int level_num, uintptr_t start, uintptr_t end, 267 uintptr_t good, uintptr_t bad) 268{ 269 /* walk entries at this level until we complete this range */ 270 while (start < end) { 271 int index = INDEX_FOR_LEVEL(start, level_num); 272 /* align the start so we can check for alignment later */ 273 uintptr_t aligned_start = start & ALIGN_FOR_LEVEL(level_num); 274 /* calculate the start of the next index */ 275 uintptr_t next_start = aligned_start + BYTES_FOR_LEVEL(level_num); 276 if (next_start > end) { 277 next_start = end; 278 } 279 uintptr_t next_table = level->table[index]; 280 if (next_table == bad) { 281 return false; 282 } 283 if (next_table != good) { 284 int succ; 285 if (level_num == 1) { 286 succ = is_reserved_or_empty_bottom((vspace_bottom_level_t *)next_table, start, next_start, good, bad); 287 } else { 288 succ = is_reserved_or_empty_mid((vspace_mid_level_t *)next_table, level_num - 1, start, next_start, good, bad); 289 } 290 if (!succ) { 291 return false; 292 } 293 } 294 start = next_start; 295 } 296 return true; 297} 298 299/* update entry in page table and handle large pages */ 300static inline int update_entries(vspace_t *vspace, uintptr_t vaddr, seL4_CPtr cap, size_t size_bits, uintptr_t cookie) 301{ 302 uintptr_t start = vaddr; 303 uintptr_t end = vaddr + BIT(size_bits); 304 sel4utils_alloc_data_t *data = get_alloc_data(vspace); 305 return update_entries_mid(vspace, data->top_level, VSPACE_NUM_LEVELS - 1, start, end, cap, cookie); 306} 307 308static inline int reserve_entries_range(vspace_t *vspace, uintptr_t start, uintptr_t end, bool preserve_frames) 309{ 310 sel4utils_alloc_data_t *data = get_alloc_data(vspace); 311 return reserve_entries_mid(vspace, data->top_level, VSPACE_NUM_LEVELS - 1, start, end, preserve_frames); 312} 313 314static inline int reserve_entries(vspace_t *vspace, uintptr_t vaddr, size_t size_bits) 315{ 316 uintptr_t start = vaddr; 317 uintptr_t end = vaddr + BIT(size_bits); 318 return reserve_entries_range(vspace, start, end, false); 319} 320 321static inline int clear_entries_range(vspace_t *vspace, uintptr_t start, uintptr_t end, bool only_reserved) 322{ 323 sel4utils_alloc_data_t *data = get_alloc_data(vspace); 324 int error = clear_entries_mid(vspace, data->top_level, VSPACE_NUM_LEVELS - 1, start, end, only_reserved); 325 if (error) { 326 return error; 327 } 328 329 if (start < data->last_allocated) { 330 data->last_allocated = start; 331 } 332 333 return 0; 334} 335 336static inline int clear_entries(vspace_t *vspace, uintptr_t vaddr, size_t size_bits) 337{ 338 uintptr_t start = vaddr; 339 uintptr_t end = vaddr + BIT(size_bits); 340 return clear_entries_range(vspace, start, end, false); 341} 342 343static inline bool is_reserved_or_empty_range(vspace_mid_level_t *top_level, uintptr_t start, uintptr_t end, 344 uintptr_t good, uintptr_t bad) 345{ 346 return is_reserved_or_empty_mid(top_level, VSPACE_NUM_LEVELS - 1, start, end, good, bad); 347} 348 349static inline bool is_reserved_or_empty(vspace_mid_level_t *top_level, uintptr_t vaddr, size_t size_bits, 350 uintptr_t good, uintptr_t bad) 351{ 352 uintptr_t start = vaddr; 353 uintptr_t end = vaddr + BIT(size_bits); 354 return is_reserved_or_empty_range(top_level, start, end, good, bad); 355} 356 357static inline bool is_available_range(vspace_mid_level_t *top_level, uintptr_t start, uintptr_t end) 358{ 359 return is_reserved_or_empty_range(top_level, start, end, EMPTY, RESERVED); 360} 361 362static inline bool is_available(vspace_mid_level_t *top_level, uintptr_t vaddr, size_t size_bits) 363{ 364 return is_reserved_or_empty(top_level, vaddr, size_bits, EMPTY, RESERVED); 365} 366 367static inline bool is_reserved_range(vspace_mid_level_t *top_level, uintptr_t start, uintptr_t end) 368{ 369 return is_reserved_or_empty_range(top_level, start, end, RESERVED, EMPTY); 370} 371 372static inline bool is_reserved(vspace_mid_level_t *top_level, uintptr_t vaddr, size_t size_bits) 373{ 374 return is_reserved_or_empty(top_level, vaddr, size_bits, RESERVED, EMPTY); 375} 376 377static inline seL4_CPtr get_cap(vspace_mid_level_t *top, uintptr_t vaddr) 378{ 379 vspace_mid_level_t *level = top; 380 for (int i = VSPACE_NUM_LEVELS - 1; i > 1; i--) { 381 int index = INDEX_FOR_LEVEL(vaddr, i); 382 uintptr_t next = level->table[index]; 383 if (next == EMPTY || next == RESERVED) { 384 return 0; 385 } 386 level = (vspace_mid_level_t *)next; 387 } 388 uintptr_t next = level->table[INDEX_FOR_LEVEL(vaddr, 1)]; 389 if (next == EMPTY || next == RESERVED) { 390 return 0; 391 } 392 vspace_bottom_level_t *bottom = (vspace_bottom_level_t *)next; 393 return bottom->cap[INDEX_FOR_LEVEL(vaddr, 0)]; 394} 395 396static inline uintptr_t get_cookie(vspace_mid_level_t *top, uintptr_t vaddr) 397{ 398 vspace_mid_level_t *level = top; 399 for (int i = VSPACE_NUM_LEVELS - 1; i > 1; i--) { 400 int index = INDEX_FOR_LEVEL(vaddr, i); 401 uintptr_t next = level->table[index]; 402 if (next == EMPTY || next == RESERVED) { 403 return 0; 404 } 405 level = (vspace_mid_level_t *)next; 406 } 407 uintptr_t next = level->table[INDEX_FOR_LEVEL(vaddr, 1)]; 408 if (next == EMPTY || next == RESERVED) { 409 return 0; 410 } 411 vspace_bottom_level_t *bottom = (vspace_bottom_level_t *)next; 412 return bottom->cookie[INDEX_FOR_LEVEL(vaddr, 0)]; 413} 414 415/* Internal interface functions */ 416int sel4utils_map_page_pd(vspace_t *vspace, seL4_CPtr cap, void *vaddr, seL4_CapRights_t rights, int cacheable, 417 size_t size_bits); 418#ifdef CONFIG_VTX 419int sel4utils_map_page_ept(vspace_t *vspace, seL4_CPtr cap, void *vaddr, seL4_CapRights_t rights, int cacheable, 420 size_t size_bits); 421#endif /* CONFIG_VTX */ 422#ifdef CONFIG_IOMMU 423int sel4utils_map_page_iommu(vspace_t *vspace, seL4_CPtr cap, void *vaddr, seL4_CapRights_t rights, int cacheable, 424 size_t size_bits); 425#endif /* CONFIG_IOMMU */ 426 427/* interface functions */ 428seL4_CPtr sel4utils_get_root(vspace_t *vspace); 429seL4_CPtr sel4utils_get_cap(vspace_t *vspace, void *vaddr); 430uintptr_t sel4utils_get_cookie(vspace_t *vspace, void *vaddr); 431 432void *sel4utils_map_pages(vspace_t *vspace, seL4_CPtr caps[], uintptr_t cookies[], 433 seL4_CapRights_t rights, size_t num_pages, size_t size_bits, 434 int cacheable); 435int sel4utils_map_pages_at_vaddr(vspace_t *vspace, seL4_CPtr caps[], uintptr_t cookies[], void *vaddr, 436 size_t num_pages, size_t size_bits, reservation_t reservation); 437int sel4utils_deferred_rights_map_pages_at_vaddr(vspace_t *vspace, seL4_CPtr caps[], uintptr_t cookies[], void *vaddr, 438 size_t num_pages, size_t size_bits, seL4_CapRights_t rights, 439 reservation_t reservation); 440void sel4utils_unmap_pages(vspace_t *vspace, void *vaddr, size_t num_pages, size_t size_bits, vka_t *vka); 441 442void *sel4utils_new_pages(vspace_t *vspace, seL4_CapRights_t rights, 443 size_t num_pages, size_t size_bits); 444int sel4utils_new_pages_at_vaddr(vspace_t *vspace, void *vaddr, size_t num_pages, 445 size_t size_bits, reservation_t reservation, bool can_use_dev); 446 447reservation_t sel4utils_reserve_range_aligned(vspace_t *vspace, size_t size, size_t size_bits, seL4_CapRights_t rights, 448 int cacheable, void **vaddr); 449reservation_t sel4utils_reserve_range_at(vspace_t *vspace, void *vaddr, size_t size, 450 seL4_CapRights_t rights, int cacheable); 451reservation_t sel4utils_reserve_deferred_rights_range_at(vspace_t *vspace, void *vaddr, 452 size_t size, int cacheable); 453void sel4utils_free_reservation(vspace_t *vspace, reservation_t reservation); 454void sel4utils_free_reservation_by_vaddr(vspace_t *vspace, void *vaddr); 455void sel4utils_tear_down(vspace_t *vspace, vka_t *vka); 456int sel4utils_share_mem_at_vaddr(vspace_t *from, vspace_t *to, void *start, int num_pages, 457 size_t size_bits, void *vaddr, reservation_t reservation); 458 459