| /* |
| * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230) |
| * |
| * SPDX-License-Identifier: BSD-2-Clause |
| */ |
| |
| #pragma once |
| |
| /* macros for accessing compiler builtins */ |
| |
| #include <assert.h> |
| |
| #define CTZ(x) __builtin_ctz(x) |
| #define CLZ(x) __builtin_clz(x) |
| #define CTZL(x) __builtin_ctzl(x) |
| #define CLZL(x) __builtin_clzl(x) |
| #define FFS(x) __builtin_ffs(x) |
| #define FFSL(x) __builtin_ffsl(x) |
| #define OFFSETOF(type, member) __builtin_offsetof(type, member) |
| #define TYPES_COMPATIBLE(t1, t2) __builtin_types_compatible_p(t1, t2) |
| #define CHOOSE_EXPR(cond, x, y) __builtin_choose_expr(cond, x, y) |
| #define IS_CONSTANT(expr) __builtin_constant_p(expr) |
| #define POPCOUNT(x) __builtin_popcount(x) |
| #define POPCOUNTL(x) __builtin_popcountl(x) |
| |
| #if CONFIG_WORD_SIZE == 32 |
| #define BSWAP_WORD(x) __builtin_bswap32(x) |
| #elif CONFIG_WORD_SIZE == 64 |
| #define BSWAP_WORD(x) __builtin_bswap64(x) |
| #endif |
| |
| /* The UNREACHABLE macro is used in some code that is imported to Isabelle via |
| * the C-to-Simpl parser. This parser can handle calls to uninterpreted |
| * functions, but it needs to see a function declaration before the call site, |
| * as it is unaware of this compiler builtin. We also provide a spec for the |
| * function indicating that any execution that reaches it represents failure. |
| */ |
| /** MODIFIES: |
| FNSPEC |
| builtin_unreachable_spec: "\<Gamma> \<turnstile> {} Call StrictC'__builtin_unreachable'_proc {}" |
| */ |
| void __builtin_unreachable(void); |
| |
| #define UNREACHABLE() \ |
| do { \ |
| assert(!"unreachable"); \ |
| __builtin_unreachable(); \ |
| } while (0) |
| |
| /* Borrowed from linux/include/linux/compiler.h */ |
| #define likely(x) __builtin_expect(!!(x), 1) |
| #define unlikely(x) __builtin_expect(!!(x), 0) |