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#pragma once 13 14#include <vka/vka.h> 15#include <vka/capops.h> 16#include <vka/object.h> 17 18/** 19 * Mint an object cap across cspaces, allocating a new slot in the dest cspace. 20 * 21 * @param[in] src_vka the vka the object cap was allocated with. 22 * @param[in] dest_vka the vka to allocate the new slot in and mint the cap to. 23 * 24 * Other parameters refer to @see vka_mint_object. 25 * 26 */ 27static inline int 28vka_mint_object_inter_cspace(vka_t *src_vka, vka_object_t *object, vka_t *dest_vka, cspacepath_t *result, seL4_CapRights_t rights, seL4_Word badge) 29{ 30 int error = vka_cspace_alloc_path(dest_vka, result); 31 if (error != seL4_NoError) { 32 return error; 33 } 34 35 cspacepath_t src; 36 vka_cspace_make_path(src_vka, object->cptr, &src); 37 return vka_cnode_mint(result, &src, rights, badge); 38} 39 40/* 41 * Mint an object cap into a new cslot in the same cspace. 42 * 43 * @param[in] vka allocator for the cspace. 44 * @param[in] object target object for cap minting. 45 * @param[out] allocated cspacepath. 46 * @param[in] rights the rights for the minted cap. 47 * @param[in] badge the badge for the minted cap. 48 */ 49static inline int 50vka_mint_object(vka_t *vka, vka_object_t *object, cspacepath_t *result, 51 seL4_CapRights_t rights, seL4_Word badge) 52{ 53 return vka_mint_object_inter_cspace(vka, object, vka, result, rights, badge); 54} 55 56