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