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