1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com> 4 * 5 * SPDX-License-Identifier: GPL-2.0-only 6 */ 7 8#include <types.h> 9#include <api/failures.h> 10#include <kernel/vspace.h> 11#include <object/structures.h> 12#include <arch/machine.h> 13#include <arch/model/statedata.h> 14#include <arch/object/objecttype.h> 15 16deriveCap_ret_t Arch_deriveCap(cte_t *slot, cap_t cap) 17{ 18 deriveCap_ret_t ret; 19 20 switch (cap_get_capType(cap)) { 21 22 case cap_page_table_cap: 23 if (cap_page_table_cap_get_capPTIsMapped(cap)) { 24 ret.cap = cap; 25 ret.status = EXCEPTION_NONE; 26 } else { 27 userError("Deriving an unmapped PT cap"); 28 current_syscall_error.type = seL4_IllegalOperation; 29 ret.cap = cap_null_cap_new(); 30 ret.status = EXCEPTION_SYSCALL_ERROR; 31 } 32 return ret; 33 34 case cap_frame_cap: 35 cap = cap_frame_cap_set_capFMappedAddress(cap, 0); 36 ret.cap = cap_frame_cap_set_capFMappedASID(cap, asidInvalid); 37 ret.status = EXCEPTION_NONE; 38 return ret; 39 40 case cap_asid_control_cap: 41 case cap_asid_pool_cap: 42 ret.cap = cap; 43 ret.status = EXCEPTION_NONE; 44 return ret; 45 46 default: 47 /* This assert has no equivalent in haskell, 48 * as the options are restricted by type */ 49 fail("Invalid arch cap type"); 50 } 51} 52 53cap_t CONST Arch_updateCapData(bool_t preserve, word_t data, cap_t cap) 54{ 55 return cap; 56} 57 58cap_t CONST Arch_maskCapRights(seL4_CapRights_t cap_rights_mask, cap_t cap) 59{ 60 if (cap_get_capType(cap) == cap_frame_cap) { 61 vm_rights_t vm_rights; 62 63 vm_rights = vmRightsFromWord(cap_frame_cap_get_capFVMRights(cap)); 64 vm_rights = maskVMRights(vm_rights, cap_rights_mask); 65 return cap_frame_cap_set_capFVMRights(cap, wordFromVMRights(vm_rights)); 66 } else { 67 return cap; 68 } 69} 70 71finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final) 72{ 73 finaliseCap_ret_t fc_ret; 74 75 switch (cap_get_capType(cap)) { 76 case cap_frame_cap: 77 78 if (cap_frame_cap_get_capFMappedASID(cap)) { 79 unmapPage(cap_frame_cap_get_capFSize(cap), 80 cap_frame_cap_get_capFMappedASID(cap), 81 cap_frame_cap_get_capFMappedAddress(cap), 82 cap_frame_cap_get_capFBasePtr(cap)); 83 } 84 break; 85 case cap_page_table_cap: 86 if (final && cap_page_table_cap_get_capPTIsMapped(cap)) { 87 /* 88 * This PageTable is either mapped as a vspace_root or otherwise exists 89 * as an entry in another PageTable. We check if it is a vspace_root and 90 * if it is delete the entry from the ASID pool otherwise we treat it as 91 * a mapped PageTable and unmap it from whatever page table it is mapped 92 * into. 93 */ 94 asid_t asid = cap_page_table_cap_get_capPTMappedASID(cap); 95 findVSpaceForASID_ret_t find_ret = findVSpaceForASID(asid); 96 pte_t *pte = PTE_PTR(cap_page_table_cap_get_capPTBasePtr(cap)); 97 if (find_ret.status == EXCEPTION_NONE && find_ret.vspace_root == pte) { 98 deleteASID(asid, pte); 99 } else { 100 unmapPageTable(asid, cap_page_table_cap_get_capPTMappedAddress(cap), pte); 101 } 102 } 103 break; 104 case cap_asid_pool_cap: 105 if (final) { 106 deleteASIDPool( 107 cap_asid_pool_cap_get_capASIDBase(cap), 108 ASID_POOL_PTR(cap_asid_pool_cap_get_capASIDPool(cap)) 109 ); 110 } 111 break; 112 case cap_asid_control_cap: 113 break; 114 } 115 fc_ret.remainder = cap_null_cap_new(); 116 fc_ret.cleanupInfo = cap_null_cap_new(); 117 return fc_ret; 118} 119 120bool_t CONST Arch_sameRegionAs(cap_t cap_a, cap_t cap_b) 121{ 122 switch (cap_get_capType(cap_a)) { 123 case cap_frame_cap: 124 if (cap_get_capType(cap_b) == cap_frame_cap) { 125 word_t botA, botB, topA, topB; 126 botA = cap_frame_cap_get_capFBasePtr(cap_a); 127 botB = cap_frame_cap_get_capFBasePtr(cap_b); 128 topA = botA + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_a))); 129 topB = botB + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_b))) ; 130 return ((botA <= botB) && (topA >= topB) && (botB <= topB)); 131 } 132 break; 133 134 case cap_page_table_cap: 135 if (cap_get_capType(cap_b) == cap_page_table_cap) { 136 return cap_page_table_cap_get_capPTBasePtr(cap_a) == 137 cap_page_table_cap_get_capPTBasePtr(cap_b); 138 } 139 break; 140 case cap_asid_control_cap: 141 if (cap_get_capType(cap_b) == cap_asid_control_cap) { 142 return true; 143 } 144 break; 145 146 case cap_asid_pool_cap: 147 if (cap_get_capType(cap_b) == cap_asid_pool_cap) { 148 return cap_asid_pool_cap_get_capASIDPool(cap_a) == 149 cap_asid_pool_cap_get_capASIDPool(cap_b); 150 } 151 break; 152 } 153 154 return false; 155} 156 157 158bool_t CONST Arch_sameObjectAs(cap_t cap_a, cap_t cap_b) 159{ 160 if ((cap_get_capType(cap_a) == cap_frame_cap) && 161 (cap_get_capType(cap_b) == cap_frame_cap)) { 162 return ((cap_frame_cap_get_capFBasePtr(cap_a) == 163 cap_frame_cap_get_capFBasePtr(cap_b)) && 164 (cap_frame_cap_get_capFSize(cap_a) == 165 cap_frame_cap_get_capFSize(cap_b)) && 166 ((cap_frame_cap_get_capFIsDevice(cap_a) == 0) == 167 (cap_frame_cap_get_capFIsDevice(cap_b) == 0))); 168 } 169 return Arch_sameRegionAs(cap_a, cap_b); 170} 171 172word_t Arch_getObjectSize(word_t t) 173{ 174 switch (t) { 175 case seL4_RISCV_4K_Page: 176 case seL4_RISCV_PageTableObject: 177 return seL4_PageBits; 178 case seL4_RISCV_Mega_Page: 179 return seL4_LargePageBits; 180#if CONFIG_PT_LEVELS > 2 181 case seL4_RISCV_Giga_Page: 182 return seL4_HugePageBits; 183#endif 184#if CONFIG_PT_LEVELS > 3 185 case seL4_RISCV_Tera_Page: 186 return seL4_TeraPageBits; 187#endif 188 default: 189 fail("Invalid object type"); 190 return 0; 191 } 192} 193 194cap_t Arch_createObject(object_t t, void *regionBase, word_t userSize, bool_t 195 deviceMemory) 196{ 197 switch (t) { 198 case seL4_RISCV_4K_Page: 199 if (deviceMemory) { 200 /** AUXUPD: "(True, ptr_retyps 1 201 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */ 202 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.RISCVSmallPage 203 (ptr_val \<acute>regionBase) 204 (unat RISCVPageBits))" */ 205 } else { 206 /** AUXUPD: "(True, ptr_retyps 1 207 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */ 208 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.RISCVSmallPage 209 (ptr_val \<acute>regionBase) 210 (unat RISCVPageBits))" */ 211 } 212 return cap_frame_cap_new( 213 asidInvalid, /* capFMappedASID */ 214 (word_t) regionBase, /* capFBasePtr */ 215 RISCV_4K_Page, /* capFSize */ 216 wordFromVMRights(VMReadWrite), /* capFVMRights */ 217 deviceMemory, /* capFIsDevice */ 218 0 /* capFMappedAddress */ 219 ); 220 221 case seL4_RISCV_Mega_Page: { 222 if (deviceMemory) { 223 /** AUXUPD: "(True, ptr_retyps (2^9) 224 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */ 225 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.RISCVLargePage 226 (ptr_val \<acute>regionBase) 227 (unat RISCVMegaPageBits))" */ 228 } else { 229 /** AUXUPD: "(True, ptr_retyps (2^9) 230 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */ 231 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.RISCVLargePage 232 (ptr_val \<acute>regionBase) 233 (unat RISCVMegaPageBits))" */ 234 } 235 return cap_frame_cap_new( 236 asidInvalid, /* capFMappedASID */ 237 (word_t) regionBase, /* capFBasePtr */ 238 RISCV_Mega_Page, /* capFSize */ 239 wordFromVMRights(VMReadWrite), /* capFVMRights */ 240 deviceMemory, /* capFIsDevice */ 241 0 /* capFMappedAddress */ 242 ); 243 } 244 245#if CONFIG_PT_LEVELS > 2 246 case seL4_RISCV_Giga_Page: { 247 if (deviceMemory) { 248 /** AUXUPD: "(True, ptr_retyps (2^18) 249 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */ 250 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.RISCVHugePage 251 (ptr_val \<acute>regionBase) 252 (unat RISCVGigaPageBits))" */ 253 } else { 254 /** AUXUPD: "(True, ptr_retyps (2^18) 255 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */ 256 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.RISCVHugePage 257 (ptr_val \<acute>regionBase) 258 (unat RISCVGigaPageBits))" */ 259 } 260 return cap_frame_cap_new( 261 asidInvalid, /* capFMappedASID */ 262 (word_t) regionBase, /* capFBasePtr */ 263 RISCV_Giga_Page, /* capFSize */ 264 wordFromVMRights(VMReadWrite), /* capFVMRights */ 265 deviceMemory, /* capFIsDevice */ 266 0 /* capFMappedAddress */ 267 ); 268 } 269#endif 270 271 case seL4_RISCV_PageTableObject: 272 /** AUXUPD: "(True, ptr_retyps 1 273 (Ptr (ptr_val \<acute>regionBase) :: (pte_C[512]) ptr))" */ 274 return cap_page_table_cap_new( 275 asidInvalid, /* capPTMappedASID */ 276 (word_t)regionBase, /* capPTBasePtr */ 277 0, /* capPTIsMapped */ 278 0 /* capPTMappedAddress */ 279 ); 280 281 default: 282 /* 283 * This is a conflation of the haskell error: "Arch.createNewCaps 284 * got an API type" and the case where an invalid object type is 285 * passed (which is impossible in haskell). 286 */ 287 fail("Arch_createObject got an API type or invalid object type"); 288 } 289} 290 291exception_t Arch_decodeInvocation( 292 word_t label, 293 word_t length, 294 cptr_t cptr, 295 cte_t *slot, 296 cap_t cap, 297 extra_caps_t extraCaps, 298 bool_t call, 299 word_t *buffer 300) 301{ 302 return decodeRISCVMMUInvocation(label, length, cptr, slot, cap, extraCaps, buffer); 303} 304 305void Arch_prepareThreadDelete(tcb_t *thread) 306{ 307#ifdef CONFIG_HAVE_FPU 308 fpuThreadDelete(thread); 309#endif 310} 311 312bool_t Arch_isFrameType(word_t type) 313{ 314 switch (type) { 315#if CONFIG_PT_LEVELS == 4 316 case seL4_RISCV_Tera_Page: 317#endif 318#if CONFIG_PT_LEVELS > 2 319 case seL4_RISCV_Giga_Page: 320#endif 321 case seL4_RISCV_Mega_Page: 322 case seL4_RISCV_4K_Page: 323 return true; 324 default: 325 return false; 326 } 327} 328