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