| /* | |
| * Copyright 2017, Data61 | |
| * Commonwealth Scientific and Industrial Research Organisation (CSIRO) | |
| * ABN 41 687 119 230. | |
| * | |
| * This software may be distributed and modified according to the terms of | |
| * the BSD 2-Clause license. Note that NO WARRANTY is provided. | |
| * See "LICENSE_BSD2.txt" for details. | |
| * | |
| * @TAG(DATA61_BSD) | |
| */ | |
| #pragma once | |
| #include <autoconf.h> | |
| #include <sel4utils/gen_config.h> | |
| #include <assert.h> | |
| #include <stdint.h> | |
| #include <utils/util.h> | |
| #include <vspace/page.h> | |
| #include <sel4utils/arch/util.h> | |
| #include <sel4utils/sel4_zf_logif.h> | |
| #include <sel4utils/strerror.h> | |
| /* Number of words in 64bits */ | |
| #define SEL4UTILS_64_WORDS (sizeof(uint64_t) / sizeof(seL4_Word)) | |
| /* | |
| * Get a 64bit value from the ipc buffer, starting from offset. | |
| * Assumes the low bits are in the first register and so on. | |
| * | |
| * @param offset the offser in the ipc buffer to start reading MRs at. | |
| * @return the 64bit value read from the ipc buffer. | |
| */ | |
| static inline uint64_t sel4utils_64_get_mr(seL4_Word offset) | |
| { | |
| uint64_t result = seL4_GetMR(offset); | |
| if (SEL4UTILS_64_WORDS == 2) { | |
| result += (((uint64_t) seL4_GetMR(offset + 1)) << 32llu); | |
| } | |
| return result; | |
| } | |
| /* | |
| * Set the correct MRs for a 64bit value. SEL4UTILS_WORDS_IN_64 MRs will be used. | |
| * | |
| * @param offset offset in the IPC buffer to start setting MRs at. | |
| * @param value the value to set | |
| */ | |
| static inline void sel4utils_64_set_mr(seL4_Word offset, uint64_t value) | |
| { | |
| seL4_SetMR(offset, (seL4_Word) value); | |
| if (SEL4UTILS_64_WORDS == 2) { | |
| seL4_SetMR(offset + 1, (seL4_Word)(value >> 32llu)); | |
| } | |
| assert(sel4utils_64_get_mr(offset) == value); | |
| } | |