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