1/*
2 * Copyright 2018, 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
13#include <autoconf.h>
14#include <vspace/mapping.h>
15
16static seL4_Error vspace_map_io(seL4_CPtr cap, seL4_CPtr iospace_root, seL4_Word vaddr, UNUSED seL4_Word attr)
17{
18#ifdef CONFIG_TK1_SMMU
19    return seL4_ARM_IOPageTable_Map(cap, iospace_root, vaddr);
20#endif
21}
22
23int vspace_get_iospace_map_obj(UNUSED seL4_Word failed_bits, vspace_map_obj_t *obj)
24{
25    if (unlikely(obj == NULL) || !config_set(CONFIG_TK1_SMMU)) {
26        return EINVAL;
27    }
28#ifdef CONFIG_TK1_SMMU
29    obj->size_bits = seL4_IOPageTableBits;
30    obj->type = seL4_ARM_IOPageTableObject;
31    obj->map_fn = vspace_map_io;
32#endif
33    return 0;
34}
35