1/*
2 * Copyright 2017, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 * See "LICENSE_BSD2.txt" for details.
9 *
10 * @TAG(DATA61_BSD)
11 */
12
13#pragma once
14
15#include <assert.h>
16#include <errno.h>
17#include <vka/vka.h>
18#include <vka/kobject_t.h>
19#include <stdio.h>
20#include <string.h>
21#include <utils/util.h>
22
23/*
24 * A wrapper to hold all the allocation information for an 'object'
25 * An object here is just combination of cptr and untyped allocation
26 * The type and size of the allocation is also stored to make free
27 * more convenient.
28 */
29
30typedef struct vka_object {
31    seL4_CPtr cptr;
32    seL4_Word ut;
33    seL4_Word type;
34    seL4_Word size_bits;
35} vka_object_t;
36
37/*
38 * Generic object allocator used by functions below, can also be used directly
39 */
40static inline int vka_alloc_object_at_maybe_dev(vka_t *vka, seL4_Word type, seL4_Word size_bits, uintptr_t paddr,
41                                                bool can_use_dev, vka_object_t *result)
42{
43    int error = -1;
44    if (!(type < seL4_ObjectTypeCount)) {
45        result->cptr = 0;
46        ZF_LOGE("Unknown object type: %ld", (long) type);
47        goto error;
48    }
49
50    error = vka_cspace_alloc(vka, &result->cptr);
51    if (unlikely(error)) {
52        result->cptr = 0;
53        ZF_LOGE("Failed to allocate cslot: error %d", error);
54        goto error;
55    }
56
57    cspacepath_t path;
58    vka_cspace_make_path(vka, result->cptr, &path);
59
60    if (paddr == VKA_NO_PADDR) {
61        error = vka_utspace_alloc_maybe_device(vka, &path, type, size_bits, can_use_dev, &result->ut);
62        if (unlikely(error)) {
63            ZF_LOGE("Failed to allocate object of size %lu, error %d",
64                    BIT(size_bits), error);
65            goto error;
66        }
67    } else {
68        error = vka_utspace_alloc_at(vka, &path, type, size_bits, paddr, &result->ut);
69        if (unlikely(error)) {
70            ZF_LOGE("Failed to allocate object of size %lu at paddr %p, error %d",
71                    BIT(size_bits), (void *)paddr, error);
72            goto error;
73        }
74    }
75
76    result->type = type;
77    result->size_bits = size_bits;
78    return 0;
79
80error:
81    if (result->cptr) {
82        vka_cspace_free(vka, result->cptr);
83    }
84    /* don't return garbage to the caller */
85    memset(result, 0, sizeof(*result));
86    return error;
87}
88
89static inline int vka_alloc_object_at(vka_t *vka, seL4_Word type, seL4_Word size_bits, uintptr_t paddr,
90                                      vka_object_t *result)
91{
92    return vka_alloc_object_at_maybe_dev(vka, type, size_bits, paddr, false, result);
93}
94static inline int vka_alloc_object(vka_t *vka, seL4_Word type, seL4_Word size_bits, vka_object_t *result)
95{
96    return vka_alloc_object_at(vka, type, size_bits, VKA_NO_PADDR, result);
97}
98
99/* convenient wrapper that throws away the vka_object_t and just returns the cptr -
100 * note you cannot use this if you intend to free the object */
101static inline seL4_CPtr vka_alloc_object_leaky(vka_t *vka, seL4_Word type, seL4_Word size_bits) WARN_UNUSED_RESULT;
102static inline seL4_CPtr vka_alloc_object_leaky(vka_t *vka, seL4_Word type, seL4_Word size_bits)
103{
104    vka_object_t result = {.cptr = 0, .ut = 0, .type = 0, size_bits = 0};
105    return vka_alloc_object(vka, type, size_bits, &result) == -1 ? 0 : result.cptr;
106}
107
108static inline void vka_free_object(vka_t *vka, vka_object_t *object)
109{
110    cspacepath_t path;
111    vka_cspace_make_path(vka, object->cptr, &path);
112
113    if (path.capPtr == 0) {
114        ZF_LOGE("Failed to create cspace path to object");
115        return;
116    }
117
118    /* ignore any errors */
119    seL4_CNode_Delete(path.root, path.capPtr, path.capDepth);
120
121    vka_cspace_free(vka, object->cptr);
122    vka_utspace_free(vka, object->type, object->size_bits, object->ut);
123}
124
125static inline uintptr_t vka_object_paddr(vka_t *vka, vka_object_t *object)
126{
127    return vka_utspace_paddr(vka, object->ut, object->type, object->size_bits);
128}
129
130/* Convenience wrappers for allocating objects */
131static inline int vka_alloc_untyped(vka_t *vka, uint32_t size_bits, vka_object_t *result)
132{
133    return vka_alloc_object(vka, seL4_UntypedObject, size_bits, result);
134}
135
136static inline int vka_alloc_untyped_at(vka_t *vka, uint32_t size_bits, uintptr_t paddr,
137                                       vka_object_t *result)
138{
139    return vka_alloc_object_at(vka, seL4_UntypedObject, size_bits, paddr, result);
140}
141
142static inline int vka_alloc_tcb(vka_t *vka, vka_object_t *result)
143{
144    return vka_alloc_object(vka, seL4_TCBObject, seL4_TCBBits, result);
145}
146
147static inline int vka_alloc_sched_context(UNUSED vka_t *vka, UNUSED vka_object_t *result)
148{
149#ifdef CONFIG_KERNEL_MCS
150    return vka_alloc_object(vka, seL4_SchedContextObject, seL4_MinSchedContextBits, result);
151#else
152    ZF_LOGW("Allocating sched context on non RT kernel");
153    return ENOSYS;
154#endif
155}
156
157static inline int vka_alloc_sched_context_size(UNUSED vka_t *vka, UNUSED vka_object_t *result,
158                                               UNUSED uint32_t size_bits)
159{
160#ifdef CONFIG_KERNEL_MCS
161    if (size_bits < seL4_MinSchedContextBits) {
162        ZF_LOGE("Invalid size bits for sc");
163        return -1;
164    }
165    return vka_alloc_object(vka, seL4_SchedContextObject, size_bits, result);
166#else
167    ZF_LOGW("Allocating sched context on non RT kernel");
168    return ENOSYS;
169#endif
170}
171
172static inline int vka_alloc_endpoint(vka_t *vka, vka_object_t *result)
173{
174    return vka_alloc_object(vka, seL4_EndpointObject, seL4_EndpointBits, result);
175}
176
177static inline int vka_alloc_notification(vka_t *vka, vka_object_t *result)
178{
179    return vka_alloc_object(vka, seL4_NotificationObject, seL4_NotificationBits, result);
180}
181
182/* @deprecated use vka_alloc_notification */
183static inline int DEPRECATED("Use vka_alloc_notification")
184vka_alloc_async_endpoint(vka_t *vka, vka_object_t *result)
185{
186    return vka_alloc_notification(vka, result);
187}
188
189static inline int vka_alloc_reply(UNUSED vka_t *vka, vka_object_t *result)
190{
191#ifdef CONFIG_KERNEL_MCS
192    return vka_alloc_object(vka, seL4_ReplyObject, seL4_ReplyBits, result);
193#else
194    *result = (vka_object_t) {};
195    ZF_LOGW("Allocating reply on non RT kernel");
196    return ENOSYS;
197#endif
198}
199
200static inline int vka_alloc_cnode_object(vka_t *vka, uint32_t slot_bits, vka_object_t *result)
201{
202    return vka_alloc_object(vka, seL4_CapTableObject, slot_bits, result);
203}
204
205/* For arch specific allocations we call upon kobject to avoid code duplication */
206static inline int vka_alloc_frame(vka_t *vka, uint32_t size_bits, vka_object_t *result)
207{
208    return vka_alloc_object(vka, kobject_get_type(KOBJECT_FRAME, size_bits), size_bits, result);
209}
210
211/* For arch specific allocations we call upon kobject to avoid code duplication */
212static inline int vka_alloc_frame_maybe_device(vka_t *vka, uint32_t size_bits, bool can_use_dev, vka_object_t *result)
213{
214    return vka_alloc_object_at_maybe_dev(vka, kobject_get_type(KOBJECT_FRAME, size_bits),
215                                         size_bits, VKA_NO_PADDR, can_use_dev, result);
216}
217
218static inline int vka_alloc_frame_at(vka_t *vka, uint32_t size_bits, uintptr_t paddr,
219                                     vka_object_t *result)
220{
221    return vka_alloc_object_at(vka, kobject_get_type(KOBJECT_FRAME, size_bits), size_bits,
222                               paddr, result);
223}
224
225static inline int vka_alloc_page_directory(vka_t *vka, vka_object_t *result)
226{
227    return vka_alloc_object(vka, kobject_get_type(KOBJECT_PAGE_DIRECTORY, 0), seL4_PageDirBits, result);
228}
229
230static inline int vka_alloc_page_table(vka_t *vka, vka_object_t *result)
231{
232    return vka_alloc_object(vka, kobject_get_type(KOBJECT_PAGE_TABLE, 0), seL4_PageTableBits, result);
233}
234
235#ifdef CONFIG_CACHE_COLORING
236
237static inline int vka_alloc_kernel_image(vka_t *vka, vka_object_t *result)
238{
239    return vka_alloc_object(vka, kobject_get_type(KOBJECT_KERNEL_IMAGE, 0), seL4_KernelImageBits, result);
240}
241
242#endif
243
244/* Implement a kobject interface */
245static inline int vka_alloc_kobject(vka_t *vka, kobject_t type, seL4_Word size_bits,
246                                    vka_object_t *result)
247{
248    return vka_alloc_object(vka, kobject_get_type(type, size_bits), size_bits, result);
249}
250
251/* leaky versions of the object allocation functions - throws away the kobject_t */
252
253#define LEAKY(name) \
254    static inline seL4_CPtr vka_alloc_##name##_leaky(vka_t *vka) WARN_UNUSED_RESULT; \
255    static inline seL4_CPtr vka_alloc_##name##_leaky(vka_t *vka) \
256{\
257    vka_object_t object;\
258    if (vka_alloc_##name(vka, &object) != 0) {\
259        return 0;\
260    }\
261    return object.cptr;\
262}
263
264LEAKY(tcb)
265LEAKY(endpoint)
266LEAKY(notification)
267LEAKY(page_directory)
268LEAKY(page_table)
269LEAKY(sched_context)
270LEAKY(reply)
271
272static inline DEPRECATED("use vka_alloc_notification_leaky") seL4_CPtr
273vka_alloc_async_endpoint_leaky(vka_t *vka)
274{
275    return vka_alloc_notification_leaky(vka);
276}
277
278#define LEAKY_SIZE_BITS(name) \
279    static inline seL4_CPtr vka_alloc_##name##_leaky(vka_t *vka, uint32_t size_bits) WARN_UNUSED_RESULT; \
280    static inline seL4_CPtr vka_alloc_##name##_leaky(vka_t *vka, uint32_t size_bits) \
281{\
282    vka_object_t object;\
283    if (vka_alloc_##name(vka, size_bits, &object) != 0) {\
284        return 0;\
285    }\
286    return object.cptr;\
287}
288
289LEAKY_SIZE_BITS(untyped)
290LEAKY_SIZE_BITS(frame)
291LEAKY_SIZE_BITS(cnode_object)
292
293#include <vka/arch/object.h>
294
295/*
296 * Get the size (in bits) of the untyped memory required to create an object of
297 * the given size.
298 */
299static inline unsigned long
300vka_get_object_size(seL4_Word objectType, seL4_Word objectSize)
301{
302    switch (objectType) {
303    /* Generic objects. */
304    case seL4_UntypedObject:
305        return objectSize;
306    case seL4_TCBObject:
307        return seL4_TCBBits;
308#ifdef CONFIG_KERNEL_MCS
309    case seL4_SchedContextObject:
310        return objectSize > seL4_MinSchedContextBits ? objectSize : seL4_MinSchedContextBits;
311    case seL4_ReplyObject:
312        return seL4_ReplyBits;
313#endif
314    case seL4_EndpointObject:
315        return seL4_EndpointBits;
316    case seL4_NotificationObject:
317        return seL4_NotificationBits;
318    case seL4_CapTableObject:
319        return (seL4_SlotBits + objectSize);
320#ifdef CONFIG_CACHE_COLORING
321    case seL4_KernelImageObject:
322        return seL4_KernelImageBits;
323#endif
324    default:
325        return vka_arch_get_object_size(objectType);
326    }
327}
328
329