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