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#pragma once
14
15/* macros for accessing compiler builtins */
16
17#include <assert.h>
18
19#define CTZ(x) __builtin_ctz(x)
20#define CLZ(x) __builtin_clz(x)
21#define CTZL(x) __builtin_ctzl(x)
22#define CLZL(x) __builtin_clzl(x)
23#define FFS(x) __builtin_ffs(x)
24#define FFSL(x) __builtin_ffsl(x)
25#define OFFSETOF(type, member) __builtin_offsetof(type, member)
26#define TYPES_COMPATIBLE(t1, t2) __builtin_types_compatible_p(t1, t2)
27#define CHOOSE_EXPR(cond, x, y) __builtin_choose_expr(cond, x, y)
28#define IS_CONSTANT(expr) __builtin_constant_p(expr)
29#define POPCOUNT(x) __builtin_popcount(x)
30#define POPCOUNTL(x) __builtin_popcountl(x)
31
32#if CONFIG_WORD_SIZE == 32
33#define BSWAP_WORD(x) __builtin_bswap32(x)
34#elif CONFIG_WORD_SIZE == 64
35#define BSWAP_WORD(x) __builtin_bswap64(x)
36#endif
37
38/* The UNREACHABLE macro is used in some code that is imported to Isabelle via
39 * the C-to-Simpl parser. This parser can handle calls to uninterpreted
40 * functions, but it needs to see a function declaration before the call site,
41 * as it is unaware of this compiler builtin. We also provide a spec for the
42 * function indicating that any execution that reaches it represents failure.
43 */
44/** MODIFIES:
45    FNSPEC
46        builtin_unreachable_spec: "\<Gamma> \<turnstile> {} Call StrictC'__builtin_unreachable'_proc {}"
47*/
48void __builtin_unreachable(void);
49
50#define UNREACHABLE() \
51    do { \
52        assert(!"unreachable"); \
53        __builtin_unreachable(); \
54    } while (0)
55
56/* Borrowed from linux/include/linux/compiler.h */
57#define likely(x)   __builtin_expect(!!(x), 1)
58#define unlikely(x) __builtin_expect(!!(x), 0)
59