1--
2-- Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3--
4-- SPDX-License-Identifier: BSD-2-Clause
5--
6
7#include <autoconf.h>
8
9base 64
10
11block VMFault {
12   padding 960
13   field IP 64
14   field Addr 64
15   field PrefetchFault 64
16   field FSR 64
17   padding 60
18   field seL4_FaultType 4
19}
20
21block NullFault {
22   padding 1216
23   padding 60
24   field seL4_FaultType 4
25}
26
27block CapFault {
28   padding 768
29   field IP   64
30   field Addr 64
31   field InRecvPhase 64
32   field LookupFailureType 64
33   -- these vary according to LookupFailureType
34   field MR4 64
35   field MR5 64
36   field MR6 64
37   padding 60
38   field seL4_FaultType 4
39}
40
41block UnknownSyscall {
42   field RAX 64
43   field RBX 64
44   field RCX 64
45   field RDX 64
46   field RSI 64
47   field RDI 64
48   field RBP 64
49   field R8 64
50   field R9 64
51   field R10 64
52   field R11 64
53   field R12 64
54   field R13 64
55   field R14 64
56   field R15 64
57   field FaultIP 64
58   field RSP 64
59   field FLAGS 64
60   field Syscall 64
61   padding 60
62   field seL4_FaultType 4
63}
64
65block UserException {
66   padding 896
67   field FaultIP 64
68   field Stack   64
69   field FLAGS  64
70   field Number  64
71   field Code    64
72   padding 60
73   field seL4_FaultType 4
74}
75
76#ifdef CONFIG_HARDWARE_DEBUG_API
77block DebugException {
78    padding 960
79    field FaultIP 64
80    field ExceptionReason 64
81    field TriggerAddress 64
82    field BreakpointNumber 64
83    padding 60
84    field seL4_FaultType 4
85}
86#endif
87
88#ifdef CONFIG_KERNEL_MCS
89block Timeout {
90    padding 1088
91    field data 64
92    field consumed 64
93    padding 60
94    field seL4_FaultType 4
95}
96#endif
97
98#include <sel4/arch/shared_types.bf>
99