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