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#include <simple/simple_helpers.h>
14
15bool simple_is_untyped_cap(simple_t *simple, seL4_CPtr pos)
16{
17    int i;
18
19    for (i = 0; i < simple_get_untyped_count(simple); i++) {
20        seL4_CPtr ut_pos = simple_get_nth_untyped(simple, i, NULL, NULL, NULL);
21        if (ut_pos == pos) {
22            return true;
23        }
24    }
25
26    return false;
27}
28
29int simple_vka_cspace_alloc(void *data, seL4_CPtr *slot)
30{
31    assert(data && slot);
32
33    simple_t *simple = data;
34    seL4_CNode cnode = simple_get_cnode(simple);
35    int i = 0;
36
37    /* Keep trying to find the next free slot by seeing if we can copy something there */
38    seL4_Error error = seL4_CNode_Copy(cnode, simple_get_cap_count(simple) + i, seL4_WordBits, cnode, cnode, seL4_WordBits, seL4_AllRights);
39    while (error == seL4_DeleteFirst) {
40        i++;
41        error = seL4_CNode_Copy(cnode, simple_get_cap_count(simple) + i, seL4_WordBits, cnode, cnode, seL4_WordBits, seL4_AllRights);
42    }
43
44    if (error != seL4_NoError) {
45        error = seL4_CNode_Delete(cnode, simple_get_cap_count(simple) + i, seL4_WordBits);
46        return error;
47    }
48
49    error = seL4_CNode_Delete(cnode, simple_get_cap_count(simple) + i, seL4_WordBits);
50    if (error != seL4_NoError) {
51        return error;
52    }
53
54    *slot = simple_get_cap_count(simple) + i;
55    return seL4_NoError;
56}
57
58void simple_vka_cspace_make_path(void *data, seL4_CPtr slot, cspacepath_t *path)
59{
60    assert(data && path);
61
62    simple_t *simple = data;
63
64    path->capPtr = slot;
65    path->capDepth = seL4_WordBits;
66    path->root = simple_get_cnode(simple);
67    path->dest = simple_get_cnode(simple);
68    path->offset = slot;
69    path->destDepth = seL4_WordBits;
70}
71
72void simple_make_vka(simple_t *simple, vka_t *vka)
73{
74    vka->data = simple;
75    vka->cspace_alloc = &simple_vka_cspace_alloc;
76    vka->cspace_make_path = &simple_vka_cspace_make_path;
77    vka->utspace_alloc = NULL;
78    vka->utspace_alloc_maybe_device = NULL;
79    vka->cspace_free = NULL;
80    vka->utspace_free = NULL;
81}
82
83seL4_CPtr simple_last_valid_cap(simple_t *simple)
84{
85    seL4_CPtr largest = 0;
86    int i;
87    for (i = 0; i < simple_get_cap_count(simple); i++) {
88        seL4_CPtr cap = simple_get_nth_cap(simple, i);
89        if (cap > largest) {
90            largest = cap;
91        }
92    }
93    return largest;
94}
95