1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6 7#pragma once 8 9#include <autoconf.h> 10#include <capdl_loader_app/gen_config.h> 11 12#include <sel4/types.h> 13#include <sel4utils/mapping.h> 14#include <limits.h> 15#include <stdbool.h> 16#include <stdlib.h> 17#include <utils/util.h> 18 19#define CDL_VM_CacheEnabled seL4_ARCH_Default_VMAttributes 20#define CDL_VM_CacheDisabled seL4_ARCH_Uncached_VMAttributes 21 22#if defined(CONFIG_ARCH_ARM) 23 24/* ARM does not support write through */ 25#define CDL_VM_WriteThrough CDL_VM_CacheDisabled 26/* Note that this is the number of bits translated by the PT 27 * not the size of the actual PT object */ 28#elif defined(CONFIG_ARCH_X86) 29 30#define CDL_VM_WriteThrough seL4_X86_WriteThrough 31 32#endif 33 34/* Binary CapDL representation -- capdl.h */ 35 36/* CapRights: Access rights of capabilities 37 * This type is used internally by capDL, and doesn't 38 * reflect the representation of cap rights in the kernel api. 39 */ 40typedef enum { 41 CDL_CanWrite = BIT(0), 42 CDL_CanRead = BIT(1), 43 CDL_CanGrant = BIT(2), 44 CDL_CanGrantReply = BIT(3), 45 CDL_AllRights = (BIT(0) | BIT(1) | BIT(2) | BIT(3)), 46} CDL_CapRights; 47 48/* ObjectID: index into the objects array */ 49typedef seL4_Word CDL_ObjID; 50#define INVALID_OBJ_ID ((CDL_ObjID)-1) 51 52/* IRQ number: Hardware IRQ number */ 53typedef seL4_Word CDL_IRQ; 54/* Core id */ 55typedef seL4_Word CDL_Core; 56 57/* Capability: */ 58typedef enum { 59 CDL_NullCap, 60 CDL_UntypedCap, 61 CDL_EPCap, 62 CDL_NotificationCap, 63 CDL_ReplyCap, 64 CDL_MasterReplyCap, 65 CDL_CNodeCap, 66 CDL_TCBCap, 67 CDL_IRQControlCap, 68 CDL_IRQHandlerCap, 69 CDL_FrameCap, 70 CDL_PTCap, 71 CDL_PDCap, 72 CDL_PML4Cap, 73 CDL_PDPTCap, 74 CDL_PUDCap, 75 CDL_PGDCap, 76 CDL_ASIDControlCap, 77 CDL_ASIDPoolCap, 78#if defined(CONFIG_ARCH_X86) 79 CDL_IOPortsCap, 80 CDL_IOSpaceCap, 81#endif 82#if defined(CONFIG_ARCH_ARM) 83 CDL_ARMIOSpaceCap, 84 CDL_SIDCap, 85 CDL_CBCap, 86#endif 87#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_VTX) 88 CDL_VCPUCap, 89#endif 90 CDL_SCCap, 91 CDL_SchedControlCap, 92 CDL_RTReplyCap, 93 CDL_DomainCap, 94} CDL_CapType; 95 96#define CDL_CapData_Badge 0 97#define CDL_CapData_Guard 1 98#define CDL_CapData_Raw 2 99 100typedef struct { 101 union { 102 struct { 103 seL4_Word guard_bits: 18; /* guards have an 18-bit value */ 104seL4_Word guard_size: 105 seL4_WordBits - 18; 106 }; 107 seL4_Word badge; 108 seL4_Word data; 109 }; 110 unsigned tag: 2; /* One of CDL_CapData_* */ 111} PACKED CDL_CapData; 112 113typedef struct { 114 CDL_ObjID obj_id; 115 CDL_CapData data; 116 CDL_IRQ irq; 117 CDL_ObjID mapping_container_id; 118 seL4_Word mapping_slot; 119 seL4_CPtr mapped_frame_cap; 120 121 /* This type tag actually has a more specific type, but we force it to be represented as a 122 * uint8_t to compress the size of this struct in memory. 123 */ 124 /* CDL_CapType */ uint8_t type; 125 126 /* The following map to more specific seL4 types, but the seL4 types are padded to word size, 127 * wasting space. This padding is necessary for ABI compatibility, but we have no such 128 * requirements here and can instead reduce the in-memory size of specs by packing these fields 129 * into fewer bits. 130 */ 131 /* seL4_ARCH_VMAttributes */ unsigned vm_attribs: 3; 132 /* bool */ unsigned is_orig: 1; 133/* seL4_CapRights */ unsigned rights: 134 seL4_CapRightsBits; 135} PACKED CDL_Cap; 136 137/* CapMap: is just an array of cap slots, position of the slot and cap */ 138typedef struct { 139 seL4_Word slot; 140 CDL_Cap cap; 141} PACKED CDL_CapSlot; 142 143typedef struct { 144 seL4_Word num; 145 CDL_CapSlot *slot; 146} CDL_CapMap; 147 148/* ObjMap: is just an array of object slots */ 149typedef struct { 150 seL4_Word slot; 151 CDL_ObjID id; 152} CDL_ObjSlot; 153 154typedef struct { 155 seL4_Word num; 156 CDL_ObjSlot *slot; 157} CDL_ObjMap; 158 159/* KernelObject: */ 160typedef enum { 161 CDL_Endpoint = seL4_EndpointObject, 162 CDL_Notification = seL4_NotificationObject, 163 CDL_TCB = seL4_TCBObject, 164 CDL_CNode = seL4_CapTableObject, 165 CDL_Untyped = seL4_UntypedObject, 166#if defined(CONFIG_ARCH_ARM) 167 CDL_PT = seL4_ARM_PageTableObject, 168 CDL_PD = seL4_ARM_PageDirectoryObject, 169 CDL_Frame = seL4_ARM_SmallPageObject, 170#ifdef CONFIG_ARCH_AARCH64 171 CDL_PUD = seL4_ARM_PageUpperDirectoryObject, 172 CDL_PGD = seL4_ARM_PageGlobalDirectoryObject, 173#endif 174#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 175 CDL_VCPU = seL4_ARM_VCPUObject, 176#endif 177#ifdef CONFIG_VTX 178 CDL_VCPU = seL4_X86_VCPUObject, 179#endif 180#elif defined(CONFIG_ARCH_X86) 181 CDL_PT = seL4_X86_PageTableObject, 182 CDL_PD = seL4_X86_PageDirectoryObject, 183 CDL_Frame = seL4_X86_4K, 184#ifdef CONFIG_ARCH_X86_64 185 CDL_PML4 = seL4_X64_PML4Object, 186 CDL_PDPT = seL4_X86_PDPTObject, 187#endif 188#endif 189 CDL_ASIDPool = seL4_ObjectTypeCount + 1, 190 CDL_Interrupt = seL4_ObjectTypeCount + 2, 191#if defined(CONFIG_ARCH_X86) 192 CDL_IOPorts = seL4_ObjectTypeCount + 3, 193 CDL_IODevice = seL4_ObjectTypeCount + 4, 194#endif 195#ifdef CONFIG_KERNEL_MCS 196 CDL_SchedContext = seL4_SchedContextObject, 197 CDL_RTReply = seL4_ReplyObject, 198#else 199 CDL_SchedContext = seL4_ObjectTypeCount + 5, 200 CDL_RTReply = seL4_ObjectTypeCount + 6, 201#endif 202#if defined(CONFIG_ARCH_X86) 203 CDL_IOAPICInterrupt = seL4_ObjectTypeCount + 7, 204 CDL_MSIInterrupt = seL4_ObjectTypeCount + 8, 205#endif 206#if defined(CONFIG_ARCH_ARM) 207 CDL_ARMIODevice = seL4_ObjectTypeCount + 9, 208 CDL_ARMInterrupt = seL4_ObjectTypeCount + 11, 209 CDL_SID = seL4_ObjectTypeCount + 12, 210 CDL_CB = seL4_ObjectTypeCount + 13, 211#endif 212#ifdef CONFIG_ARCH_RISCV 213 CDL_Frame = seL4_RISCV_4K_Page, 214 CDL_PT = seL4_RISCV_PageTableObject, 215 /* We use this hack to distiguish a PageTableObject that is used as a root vspace 216 * as parts of the loader assume that the root vspace object types are unique 217 */ 218 CDL_PT_ROOT_ALIAS = seL4_ObjectTypeCount + 10, 219#endif 220} CDL_ObjectType; 221 222#ifdef CONFIG_ARCH_AARCH64 223#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined(CONFIG_ARM_PA_SIZE_BITS_40) 224#define CDL_TOP_LEVEL_PD CDL_PUD 225#define CDL_PT_NUM_LEVELS 3 226#else 227#define CDL_TOP_LEVEL_PD CDL_PGD 228#define CDL_PT_NUM_LEVELS 4 229#define CDL_PT_LEVEL_1_MAP seL4_ARM_PageUpperDirectory_Map 230#endif 231#define CDL_PT_LEVEL_1_IndexBits seL4_PUDIndexBits 232#define CDL_PT_LEVEL_2_MAP seL4_ARM_PageDirectory_Map 233#define CDL_PT_LEVEL_2_IndexBits seL4_PageDirIndexBits 234#define CDL_PT_LEVEL_3_MAP seL4_ARM_PageTable_Map 235#define CDL_PT_LEVEL_3_IndexBits seL4_PageTableIndexBits 236#elif CONFIG_ARCH_X86_64 237#define CDL_TOP_LEVEL_PD CDL_PML4 238#define CDL_PT_LEVEL_1_MAP seL4_X86_PDPT_Map 239#define CDL_PT_LEVEL_1_IndexBits seL4_PDPTIndexBits 240#define CDL_PT_LEVEL_2_MAP seL4_X86_PageDirectory_Map 241#define CDL_PT_LEVEL_2_IndexBits seL4_PageDirIndexBits 242#define CDL_PT_LEVEL_3_MAP seL4_X86_PageTable_Map 243#define CDL_PT_LEVEL_3_IndexBits seL4_PageTableIndexBits 244#define CDL_PT_NUM_LEVELS 4 245#elif CONFIG_ARCH_RISCV 246#define CDL_TOP_LEVEL_PD CDL_PT_ROOT_ALIAS 247#define CDL_PT_LEVEL_0_MAP seL4_RISCV_PageTable_Map 248#define CDL_PT_LEVEL_0_IndexBits seL4_PageTableIndexBits 249#define CDL_PT_LEVEL_1_MAP seL4_RISCV_PageTable_Map 250#define CDL_PT_LEVEL_1_IndexBits seL4_PageTableIndexBits 251#define CDL_PT_LEVEL_2_MAP seL4_RISCV_PageTable_Map 252#define CDL_PT_LEVEL_2_IndexBits seL4_PageTableIndexBits 253#define CDL_PT_LEVEL_3_MAP seL4_RISCV_PageTable_Map 254#define CDL_PT_LEVEL_3_IndexBits seL4_PageTableIndexBits 255#define CDL_PT_NUM_LEVELS CONFIG_PT_LEVELS 256#else 257#define CDL_TOP_LEVEL_PD CDL_PD 258#define CDL_PT_NUM_LEVELS 2 259#endif 260 261typedef struct { 262 uint8_t priority; 263 uint8_t max_priority; 264 uint8_t affinity; 265 uint8_t domain; 266 seL4_Word pc; 267 seL4_Word sp; 268 const char *elf_name; 269 const seL4_Word *init; 270 seL4_Word init_sz; 271 seL4_CPtr fault_ep; 272 seL4_Word ipcbuffer_addr; 273 bool resume; 274} CDL_TCBExtraInfo; 275 276typedef struct { 277 uint64_t period; 278 uint64_t budget; 279 seL4_Word data; 280} CDL_SCExtraInfo; 281 282typedef struct { 283 uint8_t bank; 284} CDL_CBExtraInfo; 285 286typedef struct { 287 int ioapic; 288 int ioapic_pin; 289 int level; 290 int polarity; 291} CDL_IOAPICIRQExtraInfo; 292 293typedef struct { 294 int handle; 295 int pci_bus; 296 int pci_dev; 297 int pci_fun; 298} CDL_MSIIRQExtraInfo; 299 300typedef struct { 301 int trigger; 302 int target; 303} CDL_ARMIRQExtraInfo; 304 305typedef enum { 306 CDL_FrameFill_None = 0, 307 CDL_FrameFill_BootInfo, 308 CDL_FrameFill_FileData, 309} CDL_FrameFillType_t; 310 311typedef enum { 312 CDL_FrameFill_BootInfo_Padding = SEL4_BOOTINFO_HEADER_FDT, 313 CDL_FrameFill_BootInfo_X86_VBE = SEL4_BOOTINFO_HEADER_X86_VBE, 314 CDL_FrameFill_BootInfo_X86_MBMMAP = SEL4_BOOTINFO_HEADER_X86_MBMMAP, 315 CDL_FrameFill_BootInfo_X86_ACPI_RSDP = SEL4_BOOTINFO_HEADER_X86_ACPI_RSDP, 316 CDL_FrameFill_BootInfo_X86_Framebuffer = SEL4_BOOTINFO_HEADER_X86_FRAMEBUFFER, 317 CDL_FrameFill_BootInfo_X86_TSC_Freq = SEL4_BOOTINFO_HEADER_X86_TSC_FREQ, 318 CDL_FrameFill_BootInfo_FDT = SEL4_BOOTINFO_HEADER_FDT 319} CDL_FrameFill_BootInfoEnum_t; 320 321typedef struct { 322 CDL_FrameFill_BootInfoEnum_t type; 323 size_t src_offset; 324} CDL_FrameFill_BootInfoType_t; 325 326typedef struct { 327 char *filename; 328 size_t file_offset; 329} CDL_FrameFill_FileDataType_t; 330 331typedef struct { 332 CDL_FrameFillType_t type; 333 size_t dest_offset; 334 size_t dest_len; 335 union { 336 CDL_FrameFill_BootInfoType_t bi_type; 337 CDL_FrameFill_FileDataType_t file_data_type; 338 }; 339} CDL_FrameFill_Element_t; 340 341typedef struct { 342 CDL_FrameFill_Element_t fill[CONFIG_CAPDL_LOADER_FILLS_PER_FRAME]; 343 seL4_Word paddr; 344} CDL_FrameExtraInfo; 345 346typedef struct { 347#ifdef CONFIG_DEBUG_BUILD 348 const char *name; /* textual ObjID from the capDL spec */ 349#endif 350 351 CDL_CapMap slots; 352 union { 353 CDL_TCBExtraInfo tcb_extra; 354 CDL_SCExtraInfo sc_extra; 355 CDL_CBExtraInfo cb_extra; 356 CDL_IOAPICIRQExtraInfo ioapicirq_extra; 357 CDL_MSIIRQExtraInfo msiirq_extra; 358 CDL_ARMIRQExtraInfo armirq_extra; 359 CDL_FrameExtraInfo frame_extra; 360 seL4_Word paddr; /* Physical address; only relevant for untyped objects. */ 361 seL4_Word asid_high; /* for ASID pools */ 362 struct { 363 seL4_Word start; 364 seL4_Word end; 365 }; 366 }; 367 CDL_ObjectType type; 368 /* The configuration for IO ports on x86 is currently overloaded into the 369 * size_bits parameter. */ 370 uint32_t size_bits; 371 372} PACKED CDL_Object; 373 374typedef struct { 375 /* The untyped that the children should be derived from */ 376 CDL_ObjID untyped; 377 /* Number of children to derive from this untyped */ 378 seL4_Word num; 379 /* Children to derive from this untyped */ 380 CDL_ObjID *children; 381} CDL_UntypedDerivation; 382 383/* CapDLModel: is described by a map from ObjectIDs (array index) to Objects */ 384typedef struct { 385 seL4_Word num; 386 CDL_Object *objects; 387 seL4_Word num_irqs; 388 CDL_ObjID *irqs; 389 390 seL4_Word num_untyped; 391 CDL_UntypedDerivation *untyped; 392 393 /* Array from ASID slot number to ASID pool object. 394 NB: asid_slots[0] is unused, so the array size is one larger 395 than the number of slots being allocated. 396 Slot 0 is unused because it is the root thread's ASID slot, 397 which the loader uses for loading other component VSpaces. */ 398 seL4_Word num_asid_slots; 399 CDL_ObjID *asid_slots; 400} CDL_Model; 401 402/* helper functions ---------------------------------------------------------------------------- */ 403 404#define CDL_TCB_CTable_Slot 0 405#define CDL_TCB_VTable_Slot 1 406#define CDL_TCB_Reply_Slot 2 407#define CDL_TCB_Caller_Slot 3 408#define CDL_TCB_IPCBuffer_Slot 4 409#define CDL_TCB_FaultEP_Slot 5 410#define CDL_TCB_SC_Slot 6 411#define CDL_TCB_TemporalFaultEP_Slot 7 412 413#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_VTX) 414#define CDL_TCB_VCPU_SLOT 8 415#endif 416 417#define CDL_CapData_MakeGuard(x, y) \ 418{ .tag = CDL_CapData_Guard, .guard_bits = (y), .guard_size = (x) } 419 420static inline CDL_CapType CDL_Cap_Type(CDL_Cap *cap) 421{ 422 return cap->type; 423} 424static inline CDL_CapData CDL_Cap_Data(CDL_Cap *cap) 425{ 426 return cap->data; 427} 428static inline seL4_ARCH_VMAttributes CDL_Cap_VMAttributes(CDL_Cap *cap) 429{ 430 return cap->vm_attribs; 431} 432static inline CDL_ObjID CDL_Cap_ObjID(CDL_Cap *cap) 433{ 434 return cap->obj_id; 435} 436static inline CDL_CapRights CDL_Cap_Rights(CDL_Cap *cap) 437{ 438 return cap->rights; 439} 440static inline CDL_IRQ CDL_Cap_IRQ(CDL_Cap *cap) 441{ 442 return cap->irq; 443} 444static inline bool CDL_Cap_IsOrig(CDL_Cap *cap) 445{ 446 return cap->is_orig; 447} 448 449static inline seL4_Word CDL_CapSlot_Slot(CDL_CapSlot *cap_slot) 450{ 451 return cap_slot->slot; 452} 453static inline CDL_Cap *CDL_CapSlot_Cap(CDL_CapSlot *cap_slot) 454{ 455 return &cap_slot->cap; 456} 457 458static inline seL4_Word CDL_ObjSlot_Slot(CDL_ObjSlot *obj_slot) 459{ 460 return obj_slot->slot; 461} 462static inline CDL_ObjID CDL_ObjSlot_ObjID(CDL_ObjSlot *obj_slot) 463{ 464 return obj_slot->id; 465} 466 467/* Returns the sel4utils representation of a CDL_Cap's rights */ 468static inline seL4_CapRights_t CDL_seL4_Cap_Rights(CDL_Cap *cap) 469{ 470 return seL4_CapRights_new(!!(cap->rights & CDL_CanGrantReply), 471 !!(cap->rights & CDL_CanGrant), 472 !!(cap->rights & CDL_CanRead), 473 !!(cap->rights & CDL_CanWrite)); 474} 475 476static inline const char *CDL_Obj_Name(CDL_Object *obj) 477{ 478#ifdef CONFIG_DEBUG_BUILD 479 if (obj->name == NULL) { 480 return "<unnamed>"; 481 } else { 482 return obj->name; 483 } 484#else 485 return "<unnamed>"; 486#endif 487} 488 489static inline CDL_ObjectType CDL_Obj_Type(CDL_Object *obj) 490{ 491 return obj->type; 492} 493static inline seL4_Word CDL_Obj_SizeBits(CDL_Object *obj) 494{ 495 return obj->size_bits; 496} 497 498static inline seL4_Word CDL_Obj_Paddr(CDL_Object *obj) 499{ 500 switch (obj->type) { 501 case CDL_Frame: 502 return obj->frame_extra.paddr; 503 case CDL_Untyped: 504 return obj->paddr; 505 default: 506 return 0; 507 } 508} 509 510static inline seL4_Word CDL_Obj_NumSlots(CDL_Object *obj) 511{ 512 return obj->slots.num; 513} 514static inline CDL_CapSlot *CDL_Obj_GetSlot(CDL_Object *obj, seL4_Word i) 515{ 516 return &obj->slots.slot[i]; 517} 518 519static inline seL4_Word CDL_TCB_IPCBuffer_Addr(CDL_Object *obj) 520{ 521 return obj->tcb_extra.ipcbuffer_addr; 522} 523 524static inline uint8_t CDL_TCB_Priority(CDL_Object *obj) 525{ 526 return obj->tcb_extra.priority; 527} 528 529static inline uint8_t CDL_CB_Bank(CDL_Object *obj) 530{ 531 return obj->cb_extra.bank; 532} 533 534static inline uint8_t CDL_TCB_MaxPriority(CDL_Object *obj) 535{ 536 return obj->tcb_extra.max_priority; 537} 538 539static inline uint8_t CDL_TCB_Affinity(CDL_Object *obj) 540{ 541 return obj->tcb_extra.affinity; 542} 543 544static inline uint32_t CDL_TCB_Domain(CDL_Object *obj) 545{ 546 return obj->tcb_extra.domain; 547} 548 549static inline seL4_Word CDL_TCB_PC(CDL_Object *obj) 550{ 551 return obj->tcb_extra.pc; 552} 553 554static inline seL4_Word CDL_TCB_SP(CDL_Object *obj) 555{ 556 return obj->tcb_extra.sp; 557} 558 559static inline const char *CDL_TCB_ElfName(CDL_Object *obj) 560{ 561 return obj->tcb_extra.elf_name; 562} 563 564static inline uint64_t CDL_SC_Period(CDL_Object *obj) 565{ 566 return obj->sc_extra.period; 567} 568 569static inline uint64_t CDL_SC_Budget(CDL_Object *obj) 570{ 571 return obj->sc_extra.budget; 572} 573 574static inline seL4_Word CDL_SC_Data(CDL_Object *obj) 575{ 576 return obj->sc_extra.data; 577} 578