55 lines
1.7 KiB
C
55 lines
1.7 KiB
C
/**
|
|
* \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
|