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 <stdlib.h>
17#include <sel4/types.h>
18#include <allocman/cspace/cspace.h>
19
20/* This is a very simple cspace allocator that monotinically allocates cptrs
21   in a range, free is not possible. */
22struct cspace_simple1level_config {
23    /* A cptr to the cnode that we are managing slots in */
24    seL4_CPtr cnode;
25    /* Size in bits of the cnode */
26    size_t cnode_size_bits;
27    /* Guard depth added to this cspace. */
28    size_t cnode_guard_bits;
29    /* First valid slot (as an index) */
30    size_t first_slot;
31    /* Last valid slot + 1 (as an index) */
32    size_t end_slot;
33};
34
35typedef struct cspace_simple1level {
36    struct cspace_simple1level_config config;
37    size_t current_slot;
38} cspace_simple1level_t;
39
40static inline cspacepath_t _cspace_simple1level_make_path(void *_cspace, seL4_CPtr slot)
41{
42    cspace_simple1level_t *cspace = (cspace_simple1level_t*)_cspace;
43    return (cspacepath_t) {
44        .root = cspace->config.cnode,
45        .capPtr = slot,
46        .offset = slot,
47        .capDepth = cspace->config.cnode_size_bits + cspace->config.cnode_guard_bits,
48        .dest = 0,
49        .destDepth = 0,
50        .window = 1
51    };
52}
53
54/* Construction of this cspace is simplified by the fact it has a completely
55   constant memory pool and is defined here. */
56void cspace_simple1level_create(cspace_simple1level_t *cspace, struct cspace_simple1level_config config);
57
58/* These functions are defined here largely so the interface definition can be
59   made static, instead of returning it from a function. Also so that we can
60   do away with this struct if using statically chosen allocators. cspaces are
61   declared as void* to make type siginatures match up. I know it's ugly, but
62   not my fault that this is the pattern for doing ADTs in C */
63int _cspace_simple1level_alloc(struct allocman *alloc, void *_cspace, cspacepath_t *slot);
64void _cspace_simple1level_free(struct allocman *alloc, void *_cspace, const cspacepath_t *slot);
65
66static inline struct cspace_interface cspace_simple1level_make_interface(cspace_simple1level_t *cspace) {
67    return (struct cspace_interface){
68        .alloc = _cspace_simple1level_alloc,
69        .free = _cspace_simple1level_free,
70        .make_path = _cspace_simple1level_make_path,
71        /* We could give arbitrary recursion properties here. Since we perform no
72           other allocations we never even have the potential to recurse */
73        .properties = ALLOCMAN_DEFAULT_PROPERTIES,
74        .cspace = cspace
75    };
76}
77
78