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 <autoconf.h>
16#include <sel4vka/gen_config.h>
17
18#include <sel4/sel4.h>
19#include <sel4/types.h>
20#ifdef CONFIG_DEBUG_BUILD
21#include <sel4debug/debug.h>
22#endif
23#include <assert.h>
24#include <stdint.h>
25#include <utils/util.h>
26#include <vka/cspacepath_t.h>
27
28/**
29 * Allocate a slot in a cspace.
30 *
31 * @param data cookie for the underlying allocator
32 * @param res pointer to a cptr to store the allocated slot
33 * @return 0 on success
34 */
35typedef int (*vka_cspace_alloc_fn)(void *data, seL4_CPtr *res);
36
37/**
38 * Convert an allocated cptr to a cspacepath, for use in
39 * operations such as Untyped_Retype
40 *
41 * @param data cookie for the underlying allocator
42 * @param slot a cslot allocated by the cspace alloc function
43 * @param res pointer to a cspacepath struct to fill out
44 */
45typedef void (*vka_cspace_make_path_fn)(void *data, seL4_CPtr slot, cspacepath_t *res);
46
47/**
48 * Free an allocated cslot
49 *
50 * @param data cookie for the underlying allocator
51 * @param slot a cslot allocated by the cspace alloc function
52 */
53typedef void (*vka_cspace_free_fn)(void *data, seL4_CPtr slot);
54
55/**
56 * Allocate a portion of an untyped into an object
57 *
58 * @param data cookie for the underlying allocator
59 * @param dest path to an empty cslot to place the cap to the allocated object
60 * @param type the seL4 object type to allocate (as passed to Untyped_Retype)
61 * @param size_bits the size of the object to allocate (as passed to Untyped_Retype)
62 * @param res pointer to a location to store the cookie representing this allocation
63 * @return 0 on success
64 */
65typedef int (*vka_utspace_alloc_fn)(void *data, const cspacepath_t *dest, seL4_Word type, seL4_Word size_bits,
66                                    seL4_Word *res);
67
68/**
69 * Allocate a portion of an untyped into an object
70 *
71 * @param data cookie for the underlying allocator
72 * @param dest path to an empty cslot to place the cap to the allocated object
73 * @param type the seL4 object type to allocate (as passed to Untyped_Retype)
74 * @param size_bits the size of the object to allocate (as passed to Untyped_Retype)
75 * @param paddr The desired physical address that this object should start at
76 * @param cookie pointer to a location to store the cookie representing this allocation
77 * @return 0 on success
78 */
79typedef int (*vka_utspace_alloc_at_fn)(void *data, const cspacepath_t *dest, seL4_Word type, seL4_Word size_bits,
80                                       uintptr_t paddr, seL4_Word *cookie);
81
82/**
83 * Allocate a portion of an untyped into an object
84 *
85 * @param data cookie for the underlying allocator
86 * @param dest path to an empty cslot to place the cap to the allocated object
87 * @param type the seL4 object type to allocate (as passed to Untyped_Retype)
88 * @param size_bits the size of the object to allocate (as passed to Untyped_Retype)
89 * @param can_use_dev whether the allocator can use device untyped instead of regular untyped
90 * @param res pointer to a location to store the cookie representing this allocation
91 * @return 0 on success
92 */
93typedef int (*vka_utspace_alloc_maybe_device_fn)(void *data, const cspacepath_t *dest, seL4_Word type,
94                                                 seL4_Word size_bits, bool can_use_dev, seL4_Word *res);
95
96/**
97 * Free a portion of an allocated untyped. Is the responsibility of the caller to
98 * have already deleted the object (by deleting all capabilities) first
99 *
100 * @param data cookie for the underlying allocator
101 * @param type the seL4 object type that was allocated (as passed to Untyped_Retype)
102 * @param size_bits the size of the object that was allocated (as passed to Untyped_Retype)
103 * @param target cookie to the allocation as given by the utspace alloc function
104 */
105typedef void (*vka_utspace_free_fn)(void *data, seL4_Word type, seL4_Word size_bits, seL4_Word target);
106
107/**
108 * Request the physical address of an object.
109 *
110 * @param data cookie for the underlying allocator
111 * @param target cookie to the allocation as given by the utspace alloc function
112 * @param type the seL4 object type that was allocated (as passed to Untyped_Retype)
113 * @param size_bits the size of the object that was allocated (as passed to Untyped_Retype)
114 * @return paddr of object, or VKA_NO_PADDR on error
115 */
116typedef uintptr_t (*vka_utspace_paddr_fn)(void *data, seL4_Word target, seL4_Word type, seL4_Word size_bits);
117
118#define VKA_NO_PADDR 1
119
120/*
121 * Generic Virtual Kernel Allocator (VKA) data structure.
122 *
123 * This is similar in concept to the Linux VFS structures, but for
124 * the seL4 kernel object allocator instead of the Linux file system.
125 *
126 * Alternatively, you can think of this as a abstract class in an
127 * OO hierarchy, of which has several implementations.
128 */
129
130typedef struct vka {
131    void *data;
132    vka_cspace_alloc_fn cspace_alloc;
133    vka_cspace_make_path_fn cspace_make_path;
134    vka_utspace_alloc_fn utspace_alloc;
135    vka_utspace_alloc_maybe_device_fn utspace_alloc_maybe_device;
136    vka_utspace_alloc_at_fn utspace_alloc_at;
137    vka_cspace_free_fn cspace_free;
138    vka_utspace_free_fn utspace_free;
139    vka_utspace_paddr_fn utspace_paddr;
140} vka_t;
141
142static inline int vka_cspace_alloc(vka_t *vka, seL4_CPtr *res)
143{
144    if (!vka) {
145        ZF_LOGE("vka is NULL");
146        return -1;
147    }
148
149    if (!res) {
150        ZF_LOGE("res is NULL");
151        return -1;
152    }
153
154    if (!vka->cspace_alloc) {
155        ZF_LOGE("Unimplemented");
156        return -1;
157    }
158
159    return vka->cspace_alloc(vka->data, res);
160}
161
162static inline void vka_cspace_make_path(vka_t *vka, seL4_CPtr slot, cspacepath_t *res)
163{
164
165    if (!res) {
166        ZF_LOGF("res is NULL");
167    }
168
169    if (!vka) {
170        ZF_LOGF("vka is NULL");
171    }
172
173    if (!vka->cspace_make_path) {
174        ZF_LOGF("Unimplmented");
175    }
176
177    vka->cspace_make_path(vka->data, slot, res);
178}
179
180/*
181 * Wrapper functions to make calls more convenient
182 */
183static inline int vka_cspace_alloc_path(vka_t *vka, cspacepath_t *res)
184{
185    seL4_CPtr slot;
186    int error = vka_cspace_alloc(vka, &slot);
187
188    if (error == seL4_NoError) {
189        vka_cspace_make_path(vka, slot, res);
190    }
191
192    return error;
193}
194
195static inline void vka_cspace_free(vka_t *vka, seL4_CPtr slot)
196{
197#ifdef CONFIG_DEBUG_BUILD
198    if (debug_cap_is_valid(slot)) {
199        ZF_LOGF("slot is not free: call vka_cnode_delete first");
200        /* this terminates the system */
201    }
202#endif
203
204    if (!vka->cspace_free) {
205        ZF_LOGE("Not implemented");
206        return;
207    }
208
209    vka->cspace_free(vka->data, slot);
210}
211
212static inline void vka_cspace_free_path(vka_t *vka, cspacepath_t path)
213{
214    vka_cspace_free(vka, path.capPtr);
215}
216
217static inline int vka_utspace_alloc(vka_t *vka, const cspacepath_t *dest, seL4_Word type, seL4_Word size_bits,
218                                    seL4_Word *res)
219{
220    if (!vka) {
221        ZF_LOGE("vka is NULL");
222        return -1;
223    }
224
225    if (!res) {
226        ZF_LOGE("res is NULL");
227        return -1;
228    }
229
230    if (!vka->utspace_alloc) {
231        ZF_LOGE("Not implemented");
232        return -1;
233    }
234
235    return vka->utspace_alloc(vka->data, dest, type, size_bits, res);
236}
237
238static inline int vka_utspace_alloc_maybe_device(vka_t *vka, const cspacepath_t *dest, seL4_Word type,
239                                                 seL4_Word size_bits, bool can_use_dev, seL4_Word *res)
240{
241    if (!vka) {
242        ZF_LOGE("vka is NULL");
243        return -1;
244    }
245
246    if (!res) {
247        ZF_LOGE("res is NULL");
248        return -1;
249    }
250
251    if (!vka->utspace_alloc_maybe_device) {
252        ZF_LOGE("Not implemented");
253        return -1;
254    }
255
256    return vka->utspace_alloc_maybe_device(vka->data, dest, type, size_bits, can_use_dev, res);
257}
258
259static inline int vka_utspace_alloc_at(vka_t *vka, const cspacepath_t *dest, seL4_Word type, seL4_Word size_bits,
260                                       uintptr_t paddr, seL4_Word *cookie)
261{
262    if (!vka) {
263        ZF_LOGE("vka is NULL");
264        return -1;
265    }
266    if (!cookie) {
267        ZF_LOGE("cookie is NULL");
268        return -1;
269    }
270    if (!vka->utspace_alloc_at) {
271        ZF_LOGE("Not implemented");
272        return -1;
273    }
274
275    return vka->utspace_alloc_at(vka->data, dest, type, size_bits, paddr, cookie);
276}
277
278static inline void vka_utspace_free(vka_t *vka, seL4_Word type, seL4_Word size_bits, seL4_Word target)
279{
280    if (!vka) {
281        ZF_LOGE("vka is NULL");
282        return ;
283    }
284
285    if (!vka->utspace_free) {
286#ifndef CONFIG_LIB_VKA_ALLOW_MEMORY_LEAKS
287        ZF_LOGF("Not implemented");
288        /* This terminates the system */
289#endif
290        return;
291    }
292
293    vka->utspace_free(vka->data, type, size_bits, target);
294}
295
296static inline uintptr_t vka_utspace_paddr(vka_t *vka, seL4_Word target, seL4_Word type, seL4_Word size_bits)
297{
298
299    if (!vka) {
300        ZF_LOGE("vka is NULL");
301        return VKA_NO_PADDR;
302    }
303
304    if (!vka->utspace_paddr) {
305        ZF_LOGE("Not implemented");
306        return VKA_NO_PADDR;
307    }
308
309    return vka->utspace_paddr(vka->data, target, type, size_bits);
310}
311
312