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 <sel4/types.h>
17#include <allocman/utspace/utspace.h>
18#include <vka/cspacepath_t.h>
19#include <vka/vka.h>
20#include <vka/kobject_t.h>
21#include <assert.h>
22
23/* This is an untyped manager that just proxies calls to a VKA interface.
24 * We also need to do some extra book keeping work */
25
26typedef struct utspace_vka_cookie {
27    seL4_Word original_cookie;
28    seL4_Word type;
29} utspace_vka_cookie_t;
30
31static inline seL4_Word _utspace_vka_alloc(struct allocman *alloc, void *_vka, size_t size_bits, seL4_Word type, const cspacepath_t *slot, uintptr_t paddr, bool canBeDevice, int *error)
32{
33    vka_t *vka = (vka_t *)_vka;
34    size_t sel4_size_bits = get_sel4_object_size(type, size_bits);
35    utspace_vka_cookie_t *cookie = (utspace_vka_cookie_t*)malloc(sizeof(*cookie));
36    if (!cookie) {
37        SET_ERROR(error, 1);
38        return 0;
39    }
40    int _error;
41    if (paddr == ALLOCMAN_NO_PADDR) {
42        _error = vka_utspace_alloc(vka, slot, type, sel4_size_bits, &cookie->original_cookie);
43    } else {
44        _error = vka_utspace_alloc_at(vka, slot, type, sel4_size_bits, paddr, &cookie->original_cookie);
45    }
46    SET_ERROR(error, _error);
47    if (!_error) {
48        cookie->type = type;
49    } else {
50        free(cookie);
51        cookie = NULL;
52    }
53    return (seL4_Word)cookie;
54}
55
56static inline void _utspace_vka_free(struct allocman *alloc, void *_vka, seL4_Word _cookie, size_t size_bits)
57{
58    vka_t *vka = (vka_t *)_vka;
59    utspace_vka_cookie_t *cookie = (utspace_vka_cookie_t*)_cookie;
60    vka_utspace_free(vka, cookie->original_cookie, cookie->type, get_sel4_object_size(cookie->type, size_bits));
61}
62
63static inline uintptr_t _utspace_vka_paddr(void *_vka, seL4_Word _cookie, size_t size_bits)
64{
65    vka_t *vka = (vka_t *)_vka;
66    utspace_vka_cookie_t *cookie = (utspace_vka_cookie_t*)_cookie;
67    return vka_utspace_paddr(vka, cookie->original_cookie, cookie->type, get_sel4_object_size(cookie->type, size_bits));
68}
69
70static inline int _utspace_vka_add_uts(struct allocman *alloc, void *_trickle, size_t num, const cspacepath_t *uts, size_t *size_bits, uintptr_t *paddr, int utType)
71{
72    assert(!"VKA interface does not support adding untypeds after creation");
73    return -1;
74}
75
76/**
77 * Make a utspace interface from a VKA. It is the responsibility of the caller to ensure
78 * that this pointer remains valid for as long as this cspace is used
79 *
80 * @param vka Allocator to proxy cspace calls to
81 * @return utspace_interface that can be given to allocman
82 */
83static inline struct utspace_interface utspace_vka_make_interface(vka_t *vka) {
84    return (struct utspace_interface) {
85        .alloc = _utspace_vka_alloc,
86        .free = _utspace_vka_free,
87        .add_uts = _utspace_vka_add_uts,
88        .paddr = _utspace_vka_paddr,
89        .properties = ALLOCMAN_DEFAULT_PROPERTIES,
90        .utspace = vka
91    };
92}
93
94