/**
 * \file
 * \brief Kernel capability predicates (to be generated by Hamlet).
 */

/*
 * Copyright (c) 2009, 2010, ETH Zurich.
 * All rights reserved.
 *
 * This file is distributed under the terms in the attached LICENSE file.
 * If you do not find this file, copies can be found by writing to:
 * ETH Zurich D-INFK, Universitaetstrasse 6, CH-8092 Zurich. Attn: Systems Group.
 */

#ifndef CAP_PREDICATES_H
#define CAP_PREDICATES_H

struct capability;
struct cte;
enum objtype;

/**
 * \brief Returns true if parent is an ancestor of child or
 * maybe a copy of child.
 *
 * The functionality is strange because Hamlet doesn't have enough knowledge.
 * A ram cap can be an ancestor of a frame cap and
 * refer to exactly the same range of memory.
 * This is not true for two ram caps, they are copies and not ancestors.
 * Hamlet fails this when checking for caps of same types
 * that can be retyped into each other.
 * For such caps, it will return true even though they are copies
 * and do not have a parent-child relationship.
 */
bool is_ancestor(struct capability *, struct capability *);

/**
 * \brief Check if the capabilities are copies of each other.
 *
 * The type of the cap determines how to check for copies.
 * Under certain instances of retype, this code may report parent/child
 * as copies.
 */
bool is_copy(struct capability *, struct capability *);

bool is_revoked_first(struct cte *, enum objtype);
bool is_well_founded(enum objtype, enum objtype);
bool is_equal_type(enum objtype, enum objtype);
int8_t compare_caps(struct capability *, struct capability *, bool);
genpaddr_t get_address(struct capability *);
gensize_t get_size(struct capability *);
uint8_t get_type_root(enum objtype);

#endif