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 <autoconf.h> 15#include <sel4utils/gen_config.h> 16#include <assert.h> 17#include <stdint.h> 18 19#include <utils/util.h> 20 21#include <vspace/page.h> 22#include <sel4utils/arch/util.h> 23#include <sel4utils/sel4_zf_logif.h> 24#include <sel4utils/strerror.h> 25 26/* Number of words in 64bits */ 27#define SEL4UTILS_64_WORDS (sizeof(uint64_t) / sizeof(seL4_Word)) 28 29/* 30 * Get a 64bit value from the ipc buffer, starting from offset. 31 * Assumes the low bits are in the first register and so on. 32 * 33 * @param offset the offser in the ipc buffer to start reading MRs at. 34 * @return the 64bit value read from the ipc buffer. 35 */ 36static inline uint64_t sel4utils_64_get_mr(seL4_Word offset) 37{ 38 uint64_t result = seL4_GetMR(offset); 39 40 if (SEL4UTILS_64_WORDS == 2) { 41 result += (((uint64_t) seL4_GetMR(offset + 1)) << 32llu); 42 } 43 44 return result; 45} 46 47/* 48 * Set the correct MRs for a 64bit value. SEL4UTILS_WORDS_IN_64 MRs will be used. 49 * 50 * @param offset offset in the IPC buffer to start setting MRs at. 51 * @param value the value to set 52 */ 53static inline void sel4utils_64_set_mr(seL4_Word offset, uint64_t value) 54{ 55 seL4_SetMR(offset, (seL4_Word) value); 56 if (SEL4UTILS_64_WORDS == 2) { 57 seL4_SetMR(offset + 1, (seL4_Word)(value >> 32llu)); 58 } 59 assert(sel4utils_64_get_mr(offset) == value); 60} 61 62