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
13#ifndef __LIBSEL4_SEL4_SEL4_ARCH_FUNCTIONS_H_
14#define __LIBSEL4_SEL4_SEL4_ARCH_FUNCTIONS_H_
15
16#include <sel4/types.h>
17
18/* the segment loaded into GS points directly to the IPC buffer */
19#define SEL4_GET_IPCBUF_SCALE(field, i, res) \
20    do {\
21        asm volatile ("movq %%gs:%c2(,%1,%c3), %0"\
22                      : [result] "=r" (res) /* outputs */\
23                      : [scale] "r" (i), /* inputs */\
24                        [offset] "i" (SEL4_OFFSETOF(seL4_IPCBuffer, field)),\
25                        [scale_factor] "i" (sizeof(seL4_Word))\
26                       /* no clobber */);\
27    } while(0)
28
29
30#define SEL4_SET_IPCBUF_SCALE(field, i, val) \
31    do {\
32        asm volatile ("movq %0, %%gs:%c2(,%1,%c3)"\
33                      : /* no outputs */\
34                      : [value] "r" (val), /* inputs */\
35                        [scale] "r" (i),\
36                        [offset] "i" (SEL4_OFFSETOF(seL4_IPCBuffer, field)),\
37                        [scale_factor] "i" (sizeof(seL4_Word))\
38                      : "memory"); /* clobber */\
39    } while(0)
40
41#define SEL4_GET_IPCBUF(field, res) \
42    do {\
43        asm volatile ("movq %%gs:%c1, %0"\
44                      : [result] "=r" (res) /* inputs */\
45                      : [offset] "i" (SEL4_OFFSETOF(seL4_IPCBuffer, field)) /* outputs */\
46                       /* no clobber */);\
47    } while(0)
48
49
50#define SEL4_SET_IPCBUF(field, val) \
51    do {\
52        asm volatile ("movq %0, %%gs:%c1"\
53                      : /* no outputs */\
54                      : [value] "r" (val), /* inputs */\
55                        [offset] "i" (SEL4_OFFSETOF(seL4_IPCBuffer, field))\
56                      : "memory"); /* clobber */\
57    } while(0)
58
59#endif /* __LIBSEL4_SEL4_SEL4_ARCH_FUNCTIONS_H_ */
60