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