1 /*
2  * Copyright 2014, General Dynamics C4 Systems
3  *
4  * SPDX-License-Identifier: GPL-2.0-only
5  */
6 
7 #pragma once
8 
9 #include <stdint.h>
10 #include <arch/types.h>
11 
12 /* arch/types.h is supposed to define word_t and _seL4_word_fmt */
13 #ifndef _seL4_word_fmt
14 #error "missing _seL4_word_fmt"
15 #endif
16 
17 /* Using multiple macro layers may look strange, but this is required to make
18  * the preprocessor fully evaluate all macro parameters first and then pass the
19  * result as parameter to the next macro layer. This allows passing macros as
20  * parameters also, and not just plain strings. The final concatenation will
21  * always be from the strings behind all macros then - and not the macro names
22  * that are passed as parameters.
23  */
24 #define _macro_concat_helper2(x,y,z)    x ## y ## z
25 #define _macro_concat_helper(x,y,z)     _macro_concat_helper2(x,y,z)
26 
27 #define _macro_str_concat_helper2(x)    #x
28 #define _macro_str_concat_helper1(x,y)  _macro_str_concat_helper2(x ## y)
29 #define _macro_str_concat(x,y)          _macro_str_concat_helper1(x,y)
30 
31 #define SEL4_PRIu_word  _macro_str_concat(_seL4_word_fmt, u)
32 #define SEL4_PRIx_word  _macro_str_concat(_seL4_word_fmt, x)
33 #define SEL4_PRI_word   SEL4_PRIu_word
34 
35 /* The C parser from the verification toolchain requires declaring word_t
36  * constants without casting integer values to word_t. Since the printf() format
37  * specifiers are aligned with the C integer type suffixes, _seL4_word_fmt can
38  * be used there also.
39  */
40 #define SEL4_WORD_CONST(x)  _macro_concat_helper(x, _seL4_word_fmt, u)
41 
42 
43 enum _bool {
44     false = 0,
45     true  = 1
46 };
47 typedef word_t bool_t;
48 
49 typedef struct region {
50     pptr_t start;
51     pptr_t end;
52 } region_t;
53 
54 typedef struct p_region {
55     paddr_t start;
56     paddr_t end;
57 } p_region_t;
58 
59 typedef struct v_region {
60     vptr_t start;
61     vptr_t end;
62 } v_region_t;
63 
64 #define REG_EMPTY (region_t){ .start = 0, .end = 0 }
65 #define P_REG_EMPTY (p_region_t){ .start = 0, .end = 0 }
66 
67 /* equivalent to a word_t except that we tell the compiler that we may alias with
68  * any other type (similar to a char pointer) */
69 typedef word_t __attribute__((__may_alias__)) word_t_may_alias;
70