1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 */ 10 11#include <types.h> 12#include <object.h> 13#include <api/failures.h> 14#include <kernel/thread.h> 15#include <kernel/cspace.h> 16#include <model/statedata.h> 17#include <arch/machine.h> 18 19lookupCap_ret_t 20lookupCap(tcb_t *thread, cptr_t cPtr) 21{ 22 lookupSlot_raw_ret_t lu_ret; 23 lookupCap_ret_t ret; 24 25 lu_ret = lookupSlot(thread, cPtr); 26 if (unlikely(lu_ret.status != EXCEPTION_NONE)) { 27 ret.status = lu_ret.status; 28 ret.cap = cap_null_cap_new(); 29 return ret; 30 } 31 32 ret.status = EXCEPTION_NONE; 33 ret.cap = lu_ret.slot->cap; 34 return ret; 35} 36 37lookupCapAndSlot_ret_t 38lookupCapAndSlot(tcb_t *thread, cptr_t cPtr) 39{ 40 lookupSlot_raw_ret_t lu_ret; 41 lookupCapAndSlot_ret_t ret; 42 43 lu_ret = lookupSlot(thread, cPtr); 44 if (unlikely(lu_ret.status != EXCEPTION_NONE)) { 45 ret.status = lu_ret.status; 46 ret.slot = NULL; 47 ret.cap = cap_null_cap_new(); 48 return ret; 49 } 50 51 ret.status = EXCEPTION_NONE; 52 ret.slot = lu_ret.slot; 53 ret.cap = lu_ret.slot->cap; 54 return ret; 55} 56 57lookupSlot_raw_ret_t 58lookupSlot(tcb_t *thread, cptr_t capptr) 59{ 60 cap_t threadRoot; 61 resolveAddressBits_ret_t res_ret; 62 lookupSlot_raw_ret_t ret; 63 64 threadRoot = TCB_PTR_CTE_PTR(thread, tcbCTable)->cap; 65 res_ret = resolveAddressBits(threadRoot, capptr, wordBits); 66 67 ret.status = res_ret.status; 68 ret.slot = res_ret.slot; 69 return ret; 70} 71 72lookupSlot_ret_t 73lookupSlotForCNodeOp(bool_t isSource, cap_t root, cptr_t capptr, 74 word_t depth) 75{ 76 resolveAddressBits_ret_t res_ret; 77 lookupSlot_ret_t ret; 78 79 ret.slot = NULL; 80 81 if (unlikely(cap_get_capType(root) != cap_cnode_cap)) { 82 current_syscall_error.type = seL4_FailedLookup; 83 current_syscall_error.failedLookupWasSource = isSource; 84 current_lookup_fault = lookup_fault_invalid_root_new(); 85 ret.status = EXCEPTION_SYSCALL_ERROR; 86 return ret; 87 } 88 89 if (unlikely(depth < 1 || depth > wordBits)) { 90 current_syscall_error.type = seL4_RangeError; 91 current_syscall_error.rangeErrorMin = 1; 92 current_syscall_error.rangeErrorMax = wordBits; 93 ret.status = EXCEPTION_SYSCALL_ERROR; 94 return ret; 95 } 96 res_ret = resolveAddressBits(root, capptr, depth); 97 if (unlikely(res_ret.status != EXCEPTION_NONE)) { 98 current_syscall_error.type = seL4_FailedLookup; 99 current_syscall_error.failedLookupWasSource = isSource; 100 /* current_lookup_fault will have been set by resolveAddressBits */ 101 ret.status = EXCEPTION_SYSCALL_ERROR; 102 return ret; 103 } 104 105 if (unlikely(res_ret.bitsRemaining != 0)) { 106 current_syscall_error.type = seL4_FailedLookup; 107 current_syscall_error.failedLookupWasSource = isSource; 108 current_lookup_fault = 109 lookup_fault_depth_mismatch_new(0, res_ret.bitsRemaining); 110 ret.status = EXCEPTION_SYSCALL_ERROR; 111 return ret; 112 } 113 114 ret.slot = res_ret.slot; 115 ret.status = EXCEPTION_NONE; 116 return ret; 117} 118 119lookupSlot_ret_t 120lookupSourceSlot(cap_t root, cptr_t capptr, word_t depth) 121{ 122 return lookupSlotForCNodeOp(true, root, capptr, depth); 123} 124 125lookupSlot_ret_t 126lookupTargetSlot(cap_t root, cptr_t capptr, word_t depth) 127{ 128 return lookupSlotForCNodeOp(false, root, capptr, depth); 129} 130 131lookupSlot_ret_t 132lookupPivotSlot(cap_t root, cptr_t capptr, word_t depth) 133{ 134 return lookupSlotForCNodeOp(true, root, capptr, depth); 135} 136 137resolveAddressBits_ret_t 138resolveAddressBits(cap_t nodeCap, cptr_t capptr, word_t n_bits) 139{ 140 resolveAddressBits_ret_t ret; 141 word_t radixBits, guardBits, levelBits, guard; 142 word_t capGuard, offset; 143 cte_t *slot; 144 145 ret.bitsRemaining = n_bits; 146 ret.slot = NULL; 147 148 if (unlikely(cap_get_capType(nodeCap) != cap_cnode_cap)) { 149 current_lookup_fault = lookup_fault_invalid_root_new(); 150 ret.status = EXCEPTION_LOOKUP_FAULT; 151 return ret; 152 } 153 154 while (1) { 155 radixBits = cap_cnode_cap_get_capCNodeRadix(nodeCap); 156 guardBits = cap_cnode_cap_get_capCNodeGuardSize(nodeCap); 157 levelBits = radixBits + guardBits; 158 159 /* Haskell error: "All CNodes must resolve bits" */ 160 assert(levelBits != 0); 161 162 capGuard = cap_cnode_cap_get_capCNodeGuard(nodeCap); 163 164 /* sjw --- the MASK(5) here is to avoid the case where n_bits = 32 165 and guardBits = 0, as it violates the C spec to >> by more 166 than 31 */ 167 168 guard = (capptr >> ((n_bits - guardBits) & MASK(wordRadix))) & MASK(guardBits); 169 if (unlikely(guardBits > n_bits || guard != capGuard)) { 170 current_lookup_fault = 171 lookup_fault_guard_mismatch_new(capGuard, n_bits, guardBits); 172 ret.status = EXCEPTION_LOOKUP_FAULT; 173 return ret; 174 } 175 176 if (unlikely(levelBits > n_bits)) { 177 current_lookup_fault = 178 lookup_fault_depth_mismatch_new(levelBits, n_bits); 179 ret.status = EXCEPTION_LOOKUP_FAULT; 180 return ret; 181 } 182 183 offset = (capptr >> (n_bits - levelBits)) & MASK(radixBits); 184 slot = CTE_PTR(cap_cnode_cap_get_capCNodePtr(nodeCap)) + offset; 185 186 if (likely(n_bits <= levelBits)) { 187 ret.status = EXCEPTION_NONE; 188 ret.slot = slot; 189 ret.bitsRemaining = 0; 190 return ret; 191 } 192 193 /** GHOSTUPD: "(\<acute>levelBits > 0, id)" */ 194 195 n_bits -= levelBits; 196 nodeCap = slot->cap; 197 198 if (unlikely(cap_get_capType(nodeCap) != cap_cnode_cap)) { 199 ret.status = EXCEPTION_NONE; 200 ret.slot = slot; 201 ret.bitsRemaining = n_bits; 202 return ret; 203 } 204 } 205 206 ret.status = EXCEPTION_NONE; 207 return ret; 208} 209