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
lookupCap(tcb_t * thread,cptr_t cPtr)15 lookupCap_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
lookupCapAndSlot(tcb_t * thread,cptr_t cPtr)32 lookupCapAndSlot_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
lookupSlot(tcb_t * thread,cptr_t capptr)51 lookupSlot_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
lookupSlotForCNodeOp(bool_t isSource,cap_t root,cptr_t capptr,word_t depth)65 lookupSlot_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
lookupSourceSlot(cap_t root,cptr_t capptr,word_t depth)111 lookupSlot_ret_t lookupSourceSlot(cap_t root, cptr_t capptr, word_t depth)
112 {
113 return lookupSlotForCNodeOp(true, root, capptr, depth);
114 }
115
lookupTargetSlot(cap_t root,cptr_t capptr,word_t depth)116 lookupSlot_ret_t lookupTargetSlot(cap_t root, cptr_t capptr, word_t depth)
117 {
118 return lookupSlotForCNodeOp(false, root, capptr, depth);
119 }
120
lookupPivotSlot(cap_t root,cptr_t capptr,word_t depth)121 lookupSlot_ret_t lookupPivotSlot(cap_t root, cptr_t capptr, word_t depth)
122 {
123 return lookupSlotForCNodeOp(true, root, capptr, depth);
124 }
125
resolveAddressBits(cap_t nodeCap,cptr_t capptr,word_t n_bits)126 resolveAddressBits_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