1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6 7#include <config.h> 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 <machine/fpu.h> 15#include <arch/object/objecttype.h> 16#include <arch/object/ioport.h> 17#include <arch/kernel/ept.h> 18 19#include <arch/object/iospace.h> 20#include <plat/machine/intel-vtd.h> 21 22 23bool_t Arch_isFrameType(word_t type) 24{ 25 switch (type) { 26 case seL4_X86_4K: 27 return true; 28 case seL4_X86_LargePageObject: 29 return true; 30 case seL4_X64_HugePageObject: 31 return true; 32 default: 33 return false; 34 } 35} 36 37deriveCap_ret_t Mode_deriveCap(cte_t *slot, cap_t cap) 38{ 39 deriveCap_ret_t ret; 40 41 switch (cap_get_capType(cap)) { 42 case cap_pml4_cap: 43 if (cap_pml4_cap_get_capPML4IsMapped(cap)) { 44 ret.cap = cap; 45 ret.status = EXCEPTION_NONE; 46 } else { 47 userError("Deriving a PML4 cap without an assigned ASID"); 48 current_syscall_error.type = seL4_IllegalOperation; 49 ret.cap = cap_null_cap_new(); 50 ret.status = EXCEPTION_SYSCALL_ERROR; 51 } 52 return ret; 53 54 case cap_pdpt_cap: 55 if (cap_pdpt_cap_get_capPDPTIsMapped(cap)) { 56 ret.cap = cap; 57 ret.status = EXCEPTION_NONE; 58 } else { 59 userError("Deriving an unmapped PTPD cap"); 60 current_syscall_error.type = seL4_IllegalOperation; 61 ret.cap = cap_null_cap_new(); 62 ret.status = EXCEPTION_SYSCALL_ERROR; 63 } 64 return ret; 65 66 case cap_frame_cap: 67 cap = cap_frame_cap_set_capFMapType(cap, X86_MappingNone); 68 ret.cap = cap_frame_cap_set_capFMappedASID(cap, asidInvalid); 69 ret.status = EXCEPTION_NONE; 70 return ret; 71 72 default: 73 fail("Invalid arch cap type"); 74 } 75} 76 77finaliseCap_ret_t Mode_finaliseCap(cap_t cap, bool_t final) 78{ 79 finaliseCap_ret_t fc_ret; 80 81 switch (cap_get_capType(cap)) { 82 83 case cap_pml4_cap: 84 if (final && cap_pml4_cap_get_capPML4IsMapped(cap)) { 85 deleteASID( 86 cap_pml4_cap_get_capPML4MappedASID(cap), 87 PML4E_PTR(cap_pml4_cap_get_capPML4BasePtr(cap)) 88 ); 89 } 90 break; 91 92 case cap_pdpt_cap: 93 if (final && cap_pdpt_cap_get_capPDPTIsMapped(cap)) { 94 unmapPDPT( 95 cap_pdpt_cap_get_capPDPTMappedASID(cap), 96 cap_pdpt_cap_get_capPDPTMappedAddress(cap), 97 PDPTE_PTR(cap_pdpt_cap_get_capPDPTBasePtr(cap)) 98 ); 99 } 100 break; 101 102 case cap_frame_cap: 103 if (cap_frame_cap_get_capFMappedASID(cap)) { 104 switch (cap_frame_cap_get_capFMapType(cap)) { 105#ifdef CONFIG_VTX 106 case X86_MappingEPT: 107 unmapEPTPage( 108 cap_frame_cap_get_capFSize(cap), 109 cap_frame_cap_get_capFMappedASID(cap), 110 cap_frame_cap_get_capFMappedAddress(cap), 111 (void *)cap_frame_cap_get_capFBasePtr(cap) 112 ); 113 break; 114#endif 115#ifdef CONFIG_IOMMU 116 case X86_MappingIOSpace: 117 unmapIOPage(cap); 118 break; 119#endif 120 case X86_MappingVSpace: 121 unmapPage( 122 cap_frame_cap_get_capFSize(cap), 123 cap_frame_cap_get_capFMappedASID(cap), 124 cap_frame_cap_get_capFMappedAddress(cap), 125 (void *)cap_frame_cap_get_capFBasePtr(cap) 126 ); 127 break; 128 default: 129 fail("Invalid map type"); 130 } 131 } 132 break; 133 134 default: 135 fail("Invalid arch cap type"); 136 } 137 138 fc_ret.remainder = cap_null_cap_new(); 139 fc_ret.cleanupInfo = cap_null_cap_new(); 140 return fc_ret; 141} 142 143bool_t CONST Mode_sameRegionAs(cap_t cap_a, cap_t cap_b) 144{ 145 switch (cap_get_capType(cap_a)) { 146 147 case cap_pdpt_cap: 148 if (cap_get_capType(cap_b) == cap_pdpt_cap) { 149 return cap_pdpt_cap_get_capPDPTBasePtr(cap_a) == 150 cap_pdpt_cap_get_capPDPTBasePtr(cap_b); 151 } 152 return false; 153 154 case cap_pml4_cap: 155 if (cap_get_capType(cap_b) == cap_pml4_cap) { 156 return cap_pml4_cap_get_capPML4BasePtr(cap_a) == 157 cap_pml4_cap_get_capPML4BasePtr(cap_b); 158 } 159 return false; 160 default: 161 return false; 162 } 163} 164 165word_t Mode_getObjectSize(word_t t) 166{ 167 switch (t) { 168 case seL4_X64_PML4Object: 169 return seL4_PML4Bits; 170 171 case seL4_X64_HugePageObject: 172 return pageBitsForSize(X64_HugePage); 173 174 default: 175 fail("Invalid object type"); 176 return 0; 177 } 178} 179 180cap_t Mode_createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory) 181{ 182 switch (t) { 183 184 case seL4_X86_4K: 185 if (deviceMemory) { 186 /** AUXUPD: "(True, ptr_retyps 1 187 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */ 188 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.X64SmallPage 189 (ptr_val \<acute>regionBase) 190 (unat X64SmallPageBits))" */ 191 } else { 192 /** AUXUPD: "(True, ptr_retyps 1 193 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */ 194 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.X64SmallPage 195 (ptr_val \<acute>regionBase) 196 (unat X64SmallPageBits))" */ 197 } 198 return cap_frame_cap_new( 199 asidInvalid, /* capFMappedASID */ 200 (word_t)regionBase, /* capFBasePtr */ 201 X86_SmallPage, /* capFSize */ 202 X86_MappingNone, /* capFMapType */ 203 0, /* capFMappedAddress */ 204 VMReadWrite, /* capFVMRights */ 205 deviceMemory /* capFIsDevice */ 206 ); 207 208 case seL4_X86_LargePageObject: 209 if (deviceMemory) { 210 /** AUXUPD: "(True, ptr_retyps 512 211 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */ 212 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.X64LargePage 213 (ptr_val \<acute>regionBase) 214 (unat X64LargePageBits))" */ 215 } else { 216 /** AUXUPD: "(True, ptr_retyps 512 217 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */ 218 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.X64LargePage 219 (ptr_val \<acute>regionBase) 220 (unat X64LargePageBits))" */ 221 } 222 return cap_frame_cap_new( 223 asidInvalid, /* capFMappedASID */ 224 (word_t)regionBase, /* capFBasePtr */ 225 X86_LargePage, /* capFSize */ 226 X86_MappingNone, /* capFMapType */ 227 0, /* capFMappedAddress */ 228 VMReadWrite, /* capFVMRights */ 229 deviceMemory /* capFIsDevice */ 230 ); 231 232 case seL4_X64_HugePageObject: 233 if (deviceMemory) { 234 /** AUXUPD: "(True, ptr_retyps 262144 235 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */ 236 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.X64HugePage 237 (ptr_val \<acute>regionBase) 238 (unat X64HugePageBits))" */ 239 } else { 240 /** AUXUPD: "(True, ptr_retyps 262144 241 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */ 242 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.X64HugePage 243 (ptr_val \<acute>regionBase) 244 (unat X64HugePageBits))" */ 245 } 246 return cap_frame_cap_new( 247 asidInvalid, /* capFMappedASID */ 248 (word_t)regionBase, /* capFBasePtr */ 249 X64_HugePage, /* capFSize */ 250 X86_MappingNone, /* capFMapType */ 251 0, /* capFMappedAddress */ 252 VMReadWrite, /* capFVMRights */ 253 deviceMemory /* capFIsDevice */ 254 ); 255 256 case seL4_X86_PageTableObject: 257 /** AUXUPD: "(True, ptr_retyps 1 258 (Ptr (ptr_val \<acute>regionBase) :: (pte_C[512]) ptr))" */ 259 return cap_page_table_cap_new( 260 asidInvalid, /* capPTMappedASID */ 261 (word_t)regionBase, /* capPTBasePtr */ 262 0, /* capPTIsMapped */ 263 0 /* capPTMappedAddress */ 264 ); 265 266 case seL4_X86_PageDirectoryObject: 267 /** AUXUPD: "(True, ptr_retyps 1 268 (Ptr (ptr_val \<acute>regionBase) :: (pde_C[512]) ptr))" */ 269 return cap_page_directory_cap_new( 270 asidInvalid, /* capPDMappedASID */ 271 (word_t)regionBase, /* capPDBasePtr */ 272 0, /* capPDIsMapped */ 273 0 /* capPDMappedAddress */ 274 ); 275 276 case seL4_X86_PDPTObject: 277 /** AUXUPD: "(True, ptr_retyps 1 278 (Ptr (ptr_val \<acute>regionBase) :: (pdpte_C[512]) ptr))" */ 279 return cap_pdpt_cap_new( 280 asidInvalid, /* capPDPTMappedASID */ 281 (word_t)regionBase, /* capPDPTBasePtr */ 282 0, /* capPDPTIsMapped */ 283 0 /* capPDPTMappedAddress */ 284 ); 285 286 case seL4_X64_PML4Object: 287 /** AUXUPD: "(True, ptr_retyps 1 288 (Ptr (ptr_val \<acute>regionBase) :: (pml4e_C[512]) ptr))" */ 289 copyGlobalMappings(PML4_PTR(regionBase)); 290 return cap_pml4_cap_new( 291 asidInvalid, /* capPML4MappedASID */ 292 (word_t)regionBase, /* capPML4BasePtr */ 293 0 /* capPML4IsMapped */ 294 ); 295 296#ifdef CONFIG_IOMMU 297 case seL4_X86_IOPageTableObject: 298 return cap_io_page_table_cap_new( 299 0, 300 0, 301 0, 302 asidInvalid, 303 (word_t)regionBase 304 ); 305#endif 306 307 default: 308 /* 309 * This is a conflation of the haskell error: "Arch.createNewCaps 310 * got an API type" and the case where an invalid object type is 311 * passed (which is impossible in haskell). 312 */ 313 fail("Arch_createObject got an API type or invalid object type"); 314 } 315} 316 317exception_t Mode_decodeInvocation( 318 word_t label, 319 word_t length, 320 cptr_t cptr, 321 cte_t *slot, 322 cap_t cap, 323 extra_caps_t extraCaps, 324 word_t *buffer 325) 326{ 327 switch (cap_get_capType(cap)) { 328 case cap_pml4_cap: 329 case cap_pdpt_cap: 330 case cap_page_directory_cap: 331 case cap_page_table_cap: 332 case cap_frame_cap: 333 return decodeX86MMUInvocation(label, length, cptr, slot, cap, extraCaps, buffer); 334 335 default: 336 current_syscall_error.type = seL4_InvalidCapability; 337 current_syscall_error.invalidCapNumber = 0; 338 return EXCEPTION_SYSCALL_ERROR; 339 } 340} 341