1/*
2 * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 */
6
7#include <sel4vm/guest_vm.h>
8#include <sel4vm/guest_vm_util.h>
9#include <sel4vm/guest_memory.h>
10
11uintptr_t vm_arm_ipa_to_pa(vm_t *vm, uintptr_t ipa_base, size_t size)
12{
13    seL4_ARM_Page_GetAddress_t ret;
14    uintptr_t pa_base = 0;
15    uintptr_t ipa;
16    vspace_t *vspace;
17    vspace = vm_get_vspace(vm);
18    ipa = ipa_base;
19    do {
20        seL4_CPtr cap;
21        int bits;
22        /* Find the cap */
23        cap = vspace_get_cap(vspace, (void *)ipa);
24        if (cap == seL4_CapNull) {
25            return 0;
26        }
27        /* Find mapping size */
28        bits = vspace_get_cookie(vspace, (void *)ipa);
29        assert(bits == 12 || bits == 21);
30        /* Find the physical address */
31        ret = seL4_ARM_Page_GetAddress(cap);
32        if (ret.error) {
33            return 0;
34        }
35        if (ipa == ipa_base) {
36            /* Record the result */
37            pa_base = ret.paddr + (ipa & MASK(bits));
38            /* From here on, ipa and ret.paddr will be aligned */
39            ipa &= ~MASK(bits);
40        } else {
41            /* Check for a contiguous mapping */
42            if (ret.paddr - pa_base != ipa - ipa_base) {
43                return 0;
44            }
45        }
46        ipa += BIT(bits);
47    } while (ipa - ipa_base < size);
48    return pa_base;
49}
50