#ifndef LIBSEL4_H
#define LIBSEL4_H

#include <pthread.h>
#include <stdbool.h>
#include <stdint.h>

#define ENDPOINT_MSG_LEN 15

extern const int TYPE_UNTYPED;
extern const int TYPE_CNODE;
extern const int TYPE_UNTYPED_OLD;
extern const int TYPE_TCB;
extern const int TYPE_ENDPOINT;

extern const int RET_OK;
extern const int RET_ERR;

/*
 * An info struct is a capability slot entry in a CNode. It provides "info"
 * about the type of the capability and additional type-specific information.
 */
typedef struct info {
    void * address;
    int type;
    int padding;
} info_t;

/*
 * An untyped_object_info struct specifies the size of untyped memory and
 * the address of the start of the untyped memory region.
 */
typedef struct untyped_object_info {
    void * address;
    int type;
    int size;
} untyped_object_info_t;

/*
 * A cnode_info struct specifies the radix of the CNode and the address
 * at which the CNode's slot table can be found.
 */
typedef struct cnode_info {
    info_t * address;
    int type;
    int radix;
} cnode_info_t;

/*
 * A TCB object. Holds the TCB's CSpace root and entry point, as well as the
 * pthread corresponding to the TCB.
 */
typedef struct tcb {
    cnode_info_t * cspace_root;
    void (* entry_point)(cnode_info_t *);
    pthread_t pthread;
} tcb_t;

/*
 * Specifies the location of a TCB struct in memory.
 */
typedef struct tcb_info {
    tcb_t * address;
    int type;
    int padding;
} tcb_info_t;

/*
 * An endpoint object. Holds a buffer used to transfer data between sender and
 * receiver, the mutex and condition variables used to coordinate sender and
 * receiver rendezvous, and required bookkeeping variables.
 */
typedef struct endpoint {
    uint32_t buf[ENDPOINT_MSG_LEN];
    int msg_len;
    bool transfer_in_progress;
    bool transfer_completed;
    int num_waiting_receivers;
    pthread_mutex_t mutex;
    pthread_cond_t sender_wait_cond;
    pthread_cond_t receiver_wait_cond;
} endpoint_t;

/*
 * Specifies the location of an endpoint struct in memory.
 */
typedef struct endpoint_info {
    endpoint_t * address;
    int type;
    int padding;
} endpoint_info_t;

/*
 * Retypes untyped memory based on the description of seL4_Untyped_Retype() in
 * the seL4 Reference Manual.
 *
 * root:        The root of the CSpace in which to place capabilities to the
 *              new objects.
 * cap:         A capability to the untyped memory that will be retyped.
 * type:        The type of object into which to retype the untyped memory.
 * num_objects: The number of retyped objects to create.
 * size_bits:   Specifies the size of the retyped objects according to the
 *              object-specific logic in Table 2.1 of the reference manual.
 * node_index:  A capability to the CNode in which to place capabilities to
 *              the new objects.
 * node_depth:  The depth limit to use when looking up the CNode specified by
 *              node_index.
 * node_offset: The slot in the CNode in which to start placing capabilities
 *              to the newly retyped objects.
 */
int seL4_Untyped_Retype(cnode_info_t * root, uint32_t cap, int type,
        int num_objects, int size_bits, uint32_t node_index, int node_depth,
        int node_offset);

/*
 * Copies a capability into a different CNode slot.
 *
 * root:         The CSpace root to use when looking up capabilities.
 * cap:          The capability to be copied.
 * cap_depth:    The bit depth to use when looking up the capability to be
 *               copied.
 * cnode_cap:    A capability to the CNode into which to copy the capability.
 * cnode_depth:  The bit depth to use when looking up the destination CNode.
 * cnode_offset: The offset into the CNode's slot table at which to put the
 *               copied capability.
 */
int seL4_CNode_Copy(cnode_info_t * root, uint32_t cap, int cap_depth,
        uint32_t cnode_cap, int cnode_depth, int cnode_offset);

/*
 * Bootstraps the system by allocating a root CNode and a region of untyped
 * memory and installing a capability to the untyped memory in the first slot
 * of the CNode. (The size_bits arguments are interpreted according to Table
 * 2.1 of the seL4 Reference Manual).
 *
 * cnode_size_bits:          If a value of n is supplied here, the resulting
 *                           CNode will have 2^n 16-byte slots.
 *
 * untyped_memory_size_bits: If a value of n is supplied here, the resulting
 *                           region of untyped memory will hold 2^n bytes.
 */
cnode_info_t * initialize(int cnode_size_bits, int untyped_memory_size_bits);

/*
 * Given a capability integer, traverses the CSpace in order to find the slot
 * entry corresponding to that capability according to the logic in section
 * 3.3 of the seL4 Reference Manual.
 *
 * A depth_limit value of 0 will result in the root being returned.
 */
info_t * look_up_cap(cnode_info_t * root, uint32_t cap, int depth_limit);

/*
 * Set the CSpace root of a TCB.
 *
 * root:        Root used to look up capabilities.
 * tcb_cap:     Capability to the TCB for which to set the CSpace root.
 * cnode_cap:   Capability to the CNode to set as the CSpace root of the TCB.
 * depth_limit: Bit depth to be used when looking up cnode_cap.
 */
int seL4_TCB_SetSpace(cnode_info_t * root, uint32_t tcb_cap, uint32_t cnode_cap, int depth_limit);

/*
 * Takes the place of seL4_TCB_WriteRegisters(). Sets the entry point of a TCB
 * to the specified function.
 */
int seL4_TCB_SetEntryPoint(cnode_info_t * root, uint32_t tcb_cap, void (* entry_point)(cnode_info_t *));

/*
 * Begins execution of a thread corresponding to the specified TCB.
 */
int seL4_TCB_Resume(cnode_info_t * root, uint32_t tcb_cap);

/*
 * Sends a message using an endpoint capability.
 *
 * root:         Root used to look up capabilities.
 * endpoint_cap: Capability to the endpoint object to use.
 * buf:          Buffer holding the contents of the message to send.
 * len:          Length of buf (the maximum allowed length is ENDPOINT_MSG_LEN).
 */
int seL4_Send(cnode_info_t * root, uint32_t endpoint_cap, uint32_t * buf, int len);

/*
 * Receives a message using an endpoint capability.
 *
 * root:         Root used to look up capabilities.
 * endpoint_cap: Capability to the endpoint object to use.
 * buf:          Buffer into which the received message will be copied.
 * len:          Length of buf (must be at least ENDPOINT_MSG_LEN).
 * recv_len:     Pointer to the location into which the length of the received
 *               message will be written.
 */
int seL4_Recv(cnode_info_t * root, uint32_t endpoint_cap, uint32_t * buf, int buf_len, int * recv_len);

info_t * look_up_cap_internal(cnode_info_t * root, uint32_t cap, int depth_limit, int bits_translated);
int int_pow(int base, int exponent);
void * pthread_entry_func(void * arg);

#endif