1/*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#include <assert.h>
8#include <config.h>
9#include <sel4/arch/constants.h>
10#include <arch/machine/registerset.h>
11#include <machine/fpu.h>
12#include <arch/object/structures.h>
13#include <machine/debug.h>
14
15const register_t msgRegisters[] = {
16    EDI,
17#ifndef CONFIG_KERNEL_MCS
18    EBP
19#endif
20};
21compile_assert(
22    consistent_message_registers,
23    sizeof(msgRegisters) / sizeof(msgRegisters[0]) == n_msgRegisters
24);
25
26const register_t frameRegisters[] = {
27    FaultIP, ESP, FLAGS, EAX, EBX, ECX, EDX, ESI, EDI, EBP
28};
29compile_assert(
30    consistent_frame_registers,
31    sizeof(frameRegisters) / sizeof(frameRegisters[0]) == n_frameRegisters
32);
33
34const register_t gpRegisters[] = {
35    FS_BASE, GS_BASE
36};
37compile_assert(
38    consistent_gp_registers,
39    sizeof(gpRegisters) / sizeof(gpRegisters[0]) == n_gpRegisters
40);
41
42void Mode_initContext(user_context_t *context)
43{
44    context->registers[EAX] = 0;
45    context->registers[EBX] = 0;
46    context->registers[ECX] = 0;
47    context->registers[EDX] = 0;
48    context->registers[ESI] = 0;
49    context->registers[EDI] = 0;
50    context->registers[EBP] = 0;
51    context->registers[ESP] = 0;
52}
53
54word_t Mode_sanitiseRegister(register_t reg, word_t v)
55{
56    return v;
57}
58
59#ifdef CONFIG_KERNEL_MCS
60word_t getNBSendRecvDest(void)
61{
62    seL4_IPCBuffer *buffer = (seL4_IPCBuffer *) lookupIPCBuffer(false, NODE_STATE(ksCurThread));
63    if (buffer != NULL) {
64        return buffer->userData;
65    } else {
66        return 0;
67    }
68}
69#endif
70