/*
 * Copyright 2017, Data61
 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
 * ABN 41 687 119 230.
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 */

#pragma once

#include <autoconf.h>
#include <stdlib.h>
#include <sel4/types.h>
#include <allocman/cspace/cspace.h>

/* This is a very simple cspace allocator that monotinically allocates cptrs
   in a range, free is not possible. */
struct cspace_simple1level_config {
    /* A cptr to the cnode that we are managing slots in */
    seL4_CPtr cnode;
    /* Size in bits of the cnode */
    size_t cnode_size_bits;
    /* Guard depth added to this cspace. */
    size_t cnode_guard_bits;
    /* First valid slot (as an index) */
    size_t first_slot;
    /* Last valid slot + 1 (as an index) */
    size_t end_slot;
};

typedef struct cspace_simple1level {
    struct cspace_simple1level_config config;
    size_t current_slot;
} cspace_simple1level_t;

static inline cspacepath_t _cspace_simple1level_make_path(void *_cspace, seL4_CPtr slot)
{
    cspace_simple1level_t *cspace = (cspace_simple1level_t*)_cspace;
    return (cspacepath_t) {
        .root = cspace->config.cnode,
        .capPtr = slot,
        .offset = slot,
        .capDepth = cspace->config.cnode_size_bits + cspace->config.cnode_guard_bits,
        .dest = 0,
        .destDepth = 0,
        .window = 1
    };
}

/* Construction of this cspace is simplified by the fact it has a completely
   constant memory pool and is defined here. */
void cspace_simple1level_create(cspace_simple1level_t *cspace, struct cspace_simple1level_config config);

/* These functions are defined here largely so the interface definition can be
   made static, instead of returning it from a function. Also so that we can
   do away with this struct if using statically chosen allocators. cspaces are
   declared as void* to make type siginatures match up. I know it's ugly, but
   not my fault that this is the pattern for doing ADTs in C */
int _cspace_simple1level_alloc(struct allocman *alloc, void *_cspace, cspacepath_t *slot);
void _cspace_simple1level_free(struct allocman *alloc, void *_cspace, const cspacepath_t *slot);

static inline struct cspace_interface cspace_simple1level_make_interface(cspace_simple1level_t *cspace) {
    return (struct cspace_interface){
        .alloc = _cspace_simple1level_alloc,
        .free = _cspace_simple1level_free,
        .make_path = _cspace_simple1level_make_path,
        /* We could give arbitrary recursion properties here. Since we perform no
           other allocations we never even have the potential to recurse */
        .properties = ALLOCMAN_DEFAULT_PROPERTIES,
        .cspace = cspace
    };
}