1/*
2 * Copyright 2016, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#pragma once
8
9#include <config.h>
10#include <util.h>
11
12static inline void arch_c_entry_hook(void)
13{
14#ifdef CONFIG_FSGSBASE_INST
15    tcb_t *tcb = NODE_STATE(ksCurThread);
16    x86_save_fsgs_base(tcb, SMP_TERNARY(getCurrentCPUIndex(), 0));
17#endif
18}
19
20static inline void arch_c_exit_hook(void)
21{
22    /* Restore the values ofthe FS and GS base. */
23    tcb_t *tcb = NODE_STATE(ksCurThread);
24    x86_load_fsgs_base(tcb,  SMP_TERNARY(getCurrentCPUIndex(), 0));
25}
26
27#ifdef CONFIG_KERNEL_MCS
28void c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall, word_t reply)
29#else
30void c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall)
31#endif
32VISIBLE NORETURN;
33
34void restore_user_context(void)
35VISIBLE NORETURN;
36
37void c_nested_interrupt(int irq)
38VISIBLE;
39
40void c_handle_interrupt(int irq, int syscall)
41VISIBLE NORETURN;
42
43void c_handle_vmexit(void)
44VISIBLE NORETURN;
45