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 GNU General Public License version 2. Note that NO WARRANTY is provided.
8 * See "LICENSE_GPLv2.txt" for details.
9 *
10 * @TAG(DATA61_GPL)
11 */
12
13#include <config.h>
14#include <types.h>
15#include <api/faults.h>
16#include <api/syscall.h>
17#include <mode/api/constants.h>
18#include <kernel/thread.h>
19#include <arch/kernel/thread.h>
20#include <machine/debug.h>
21#include <mode/api/ipc_buffer.h>
22#include <object/schedcontext.h>
23
24/* consistency with libsel4 */
25compile_assert(InvalidRoot, lookup_fault_invalid_root + 1 == seL4_InvalidRoot)
26compile_assert(MissingCapability, lookup_fault_missing_capability + 1 == seL4_MissingCapability)
27compile_assert(DepthMismatch, lookup_fault_depth_mismatch + 1 == seL4_DepthMismatch)
28compile_assert(GuardMismatch, lookup_fault_guard_mismatch + 1 == seL4_GuardMismatch)
29compile_assert(seL4_UnknownSyscall_Syscall, (word_t) n_syscallMessage == seL4_UnknownSyscall_Syscall)
30compile_assert(seL4_UserException_Number, (word_t) n_exceptionMessage == seL4_UserException_Number)
31compile_assert(seL4_UserException_Code, (word_t) n_exceptionMessage + 1 == seL4_UserException_Code)
32
33static inline unsigned int
34setMRs_lookup_failure(tcb_t *receiver, word_t* receiveIPCBuffer,
35                      lookup_fault_t luf, unsigned int offset)
36{
37    word_t lufType = lookup_fault_get_lufType(luf);
38    word_t i;
39
40    i = setMR(receiver, receiveIPCBuffer, offset, lufType + 1);
41
42    /* check constants match libsel4 */
43    if (offset == seL4_CapFault_LookupFailureType) {
44        assert(offset + 1 == seL4_CapFault_BitsLeft);
45        assert(offset + 2 == seL4_CapFault_DepthMismatch_BitsFound);
46        assert(offset + 2 == seL4_CapFault_GuardMismatch_GuardFound);
47        assert(offset + 3 == seL4_CapFault_GuardMismatch_BitsFound);
48    } else {
49        assert(offset == 1);
50    }
51
52    switch (lufType) {
53    case lookup_fault_invalid_root:
54        return i;
55
56    case lookup_fault_missing_capability:
57        return setMR(receiver, receiveIPCBuffer, offset + 1,
58                     lookup_fault_missing_capability_get_bitsLeft(luf));
59
60    case lookup_fault_depth_mismatch:
61        setMR(receiver, receiveIPCBuffer, offset + 1,
62              lookup_fault_depth_mismatch_get_bitsLeft(luf));
63        return setMR(receiver, receiveIPCBuffer, offset + 2,
64                     lookup_fault_depth_mismatch_get_bitsFound(luf));
65
66    case lookup_fault_guard_mismatch:
67        setMR(receiver, receiveIPCBuffer, offset + 1,
68              lookup_fault_guard_mismatch_get_bitsLeft(luf));
69        setMR(receiver, receiveIPCBuffer, offset + 2,
70              lookup_fault_guard_mismatch_get_guardFound(luf));
71        return setMR(receiver, receiveIPCBuffer, offset + 3,
72                     lookup_fault_guard_mismatch_get_bitsFound(luf));
73
74    default:
75        fail("Invalid lookup failure");
76    }
77}
78
79static inline void
80copyMRsFaultReply(tcb_t *sender, tcb_t *receiver, MessageID_t id, word_t length)
81{
82    word_t i;
83    bool_t archInfo;
84
85    archInfo = Arch_getSanitiseRegisterInfo(receiver);
86
87    for (i = 0; i < MIN(length, n_msgRegisters); i++) {
88        register_t r = fault_messages[id][i];
89        word_t v = getRegister(sender, msgRegisters[i]);
90        setRegister(receiver, r, sanitiseRegister(r, v, archInfo));
91    }
92
93    if (i < length) {
94        word_t *sendBuf = lookupIPCBuffer(false, sender);
95        if (sendBuf) {
96            for (; i < length; i++) {
97                register_t r = fault_messages[id][i];
98                word_t v = sendBuf[i + 1];
99                setRegister(receiver, r, sanitiseRegister(r, v, archInfo));
100            }
101        }
102    }
103}
104
105static inline void
106copyMRsFault(tcb_t *sender, tcb_t *receiver, MessageID_t id,
107             word_t length, word_t *receiveIPCBuffer)
108{
109    word_t i;
110    for (i = 0; i < MIN(length, n_msgRegisters); i++) {
111        setRegister(receiver, msgRegisters[i], getRegister(sender, fault_messages[id][i]));
112    }
113
114    if (receiveIPCBuffer) {
115        for (; i < length; i++) {
116            receiveIPCBuffer[i + 1] = getRegister(sender, fault_messages[id][i]);
117        }
118    }
119}
120
121bool_t
122handleFaultReply(tcb_t *receiver, tcb_t *sender)
123{
124    /* These lookups are moved inward from doReplyTransfer */
125    seL4_MessageInfo_t tag = messageInfoFromWord(getRegister(sender, msgInfoRegister));
126    word_t label = seL4_MessageInfo_get_label(tag);
127    word_t length = seL4_MessageInfo_get_length(tag);
128    seL4_Fault_t fault = receiver->tcbFault;
129
130    switch (seL4_Fault_get_seL4_FaultType(fault)) {
131    case seL4_Fault_CapFault:
132        return true;
133
134    case seL4_Fault_UnknownSyscall:
135        copyMRsFaultReply(sender, receiver, MessageID_Syscall, MIN(length, n_syscallMessage));
136        return (label == 0);
137
138    case seL4_Fault_UserException:
139        copyMRsFaultReply(sender, receiver, MessageID_Exception, MIN(length, n_exceptionMessage));
140        return (label == 0);
141
142    case seL4_Fault_Timeout:
143        copyMRsFaultReply(sender, receiver, MessageID_TimeoutReply, MIN(length, n_timeoutMessage));
144        return (label == 0);
145#ifdef CONFIG_HARDWARE_DEBUG_API
146    case seL4_Fault_DebugException: {
147        word_t n_instrs;
148
149        if (seL4_Fault_DebugException_get_exceptionReason(fault) != seL4_SingleStep) {
150            /* Only single-step replies are required to set message registers.
151             */
152            return (label == 0);
153        }
154
155        if (length < DEBUG_REPLY_N_EXPECTED_REGISTERS) {
156            /* A single-step reply doesn't mean much if it isn't composed of the bp
157             * number and number of instructions to skip. But even if both aren't
158             * set, we can still allow the thread to continue because replying
159             * should uniformly resume thread execution, based on the general seL4
160             * API model.
161             *
162             * If it was single-step, but no reply registers were set, just
163             * default to skipping 1 and continuing.
164             *
165             * On x86, bp_num actually doesn't matter for single-stepping
166             * because single-stepping doesn't use a hardware register -- it
167             * uses EFLAGS.TF.
168             */
169            n_instrs = 1;
170        } else {
171            /* If the reply had all expected registers set, proceed as normal */
172            n_instrs = getRegister(sender, msgRegisters[0]);
173        }
174
175        syscall_error_t res;
176
177        res = Arch_decodeConfigureSingleStepping(receiver, 0, n_instrs, true);
178        if (res.type != seL4_NoError) {
179            return false;
180        };
181
182        configureSingleStepping(receiver, 0, n_instrs, true);
183
184        /* Replying will always resume the thread: the only variant behaviour
185         * is whether or not the thread will be resumed with stepping still
186         * enabled.
187         */
188        return (label == 0);
189    }
190#endif
191
192    default:
193        return Arch_handleFaultReply(receiver, sender, seL4_Fault_get_seL4_FaultType(fault));
194    }
195}
196
197word_t
198setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer)
199{
200    switch (seL4_Fault_get_seL4_FaultType(sender->tcbFault)) {
201    case seL4_Fault_CapFault:
202        setMR(receiver, receiveIPCBuffer, seL4_CapFault_IP, getRestartPC(sender));
203        setMR(receiver, receiveIPCBuffer, seL4_CapFault_Addr,
204              seL4_Fault_CapFault_get_address(sender->tcbFault));
205        setMR(receiver, receiveIPCBuffer, seL4_CapFault_InRecvPhase,
206              seL4_Fault_CapFault_get_inReceivePhase(sender->tcbFault));
207        return setMRs_lookup_failure(receiver, receiveIPCBuffer,
208                                     sender->tcbLookupFailure, seL4_CapFault_LookupFailureType);
209
210    case seL4_Fault_UnknownSyscall: {
211        copyMRsFault(sender, receiver, MessageID_Syscall, n_syscallMessage,
212                     receiveIPCBuffer);
213
214        return setMR(receiver, receiveIPCBuffer, n_syscallMessage,
215                     seL4_Fault_UnknownSyscall_get_syscallNumber(sender->tcbFault));
216    }
217
218    case seL4_Fault_UserException: {
219        copyMRsFault(sender, receiver, MessageID_Exception,
220                     n_exceptionMessage, receiveIPCBuffer);
221        setMR(receiver, receiveIPCBuffer, n_exceptionMessage,
222              seL4_Fault_UserException_get_number(sender->tcbFault));
223        return setMR(receiver, receiveIPCBuffer, n_exceptionMessage + 1u,
224                     seL4_Fault_UserException_get_code(sender->tcbFault));
225    }
226
227    case seL4_Fault_Timeout: {
228        word_t len = setMR(receiver, receiveIPCBuffer, seL4_Timeout_Data,
229                           seL4_Fault_Timeout_get_badge(sender->tcbFault));
230        if (sender->tcbSchedContext) {
231            time_t consumed = schedContext_updateConsumed(sender->tcbSchedContext);
232            return mode_setTimeArg(len, consumed,
233                                   receiveIPCBuffer, receiver);
234        } else {
235            return len;
236        }
237    }
238#ifdef CONFIG_HARDWARE_DEBUG_API
239    case seL4_Fault_DebugException: {
240        word_t reason = seL4_Fault_DebugException_get_exceptionReason(sender->tcbFault);
241
242        setMR(receiver, receiveIPCBuffer,
243              seL4_DebugException_FaultIP, getRestartPC(sender));
244        unsigned int ret = setMR(receiver, receiveIPCBuffer,
245                                 seL4_DebugException_ExceptionReason, reason);
246
247        if (reason != seL4_SingleStep && reason != seL4_SoftwareBreakRequest) {
248            ret = setMR(receiver, receiveIPCBuffer,
249                        seL4_DebugException_TriggerAddress,
250                        seL4_Fault_DebugException_get_breakpointAddress(sender->tcbFault));
251
252            /* Breakpoint messages also set a "breakpoint number" register. */
253            ret = setMR(receiver, receiveIPCBuffer,
254                        seL4_DebugException_BreakpointNumber,
255                        seL4_Fault_DebugException_get_breakpointNumber(sender->tcbFault));
256        }
257        return ret;
258    }
259#endif /* CONFIG_HARDWARE_DEBUG_API */
260
261    default:
262        return Arch_setMRs_fault(sender, receiver, receiveIPCBuffer,
263                                 seL4_Fault_get_seL4_FaultType(sender->tcbFault));
264    }
265}
266