portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Split fault types into arch/generic

Browse source 
Prior to this commit faults were separate
per architecture. This commit extracts the common
fault types and introduces arch specific faults,
reducing code duplication across architectures.
This commit is contained in:
Anna Lyons 2016-07-12 17:26:39 +10:00 committed by Anna Lyons
parent b3b7e3cbf9
commit 33a771d3cb
23 changed files with 324 additions and 558 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
include/api/faults.h
View file

@ -11,10 +11,13 @@
#ifndef __API_FAULTS_H
#define __API_FAULTS_H
#include <api/failures.h>
#include <object.h>
#include <object/structures.h>
#include <types.h>
word_t setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer);
word_t Arch_setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer, word_t faultType);
bool_t handleFaultReply(tcb_t *receiver, tcb_t *sender);
bool_t Arch_handleFaultReply(tcb_t *receiver, tcb_t *sender, word_t faultType);
#endif

19
include/arch/arm/arch/32/mode/object/structures.bf
View file

@ -150,7 +150,7 @@ tagged_union cap capType {
tag reply_cap 8
tag cnode_cap 10
tag thread_cap 12
-- Do not extend even 4-bit caps types beyond 12, as we use
-- Do not extend even 4-bit caps types beyond 12, as we use
-- 14 (0xe) to determine which caps are 8-bit.
-- 4-bit tag arch caps
@ -160,7 +160,7 @@ tagged_union cap capType {
tag page_table_cap 7
tag page_directory_cap 9
tag asid_control_cap 11
-- Do not extend odd 4-bit caps types beyond 13, as we use
-- Do not extend odd 4-bit caps types beyond 13, as we use
-- 15 (0xf) to determine which caps are 8-bit.
-- 8-bit tag caps
@ -181,7 +181,7 @@ tagged_union cap capType {
#endif
}
---- Arch-independent object types
---- Arm specific fault types
block vm_fault {
field address 32
@ -214,17 +214,20 @@ block vcpu_fault {
#endif
tagged_union fault faultType {
-- generic faults
tag null_fault 0
tag cap_fault 1
tag vm_fault 2
tag unknown_syscall 3
tag user_exception 4
tag unknown_syscall 2
tag user_exception 3
#ifdef CONFIG_HARDWARE_DEBUG_API
tag debug_exception 5
tag debug_exception 4
#endif
-- arch specific faults
tag vm_fault 5
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
tag vgic_maintenance 6
tag vcpu_fault 7
tag vcpu_fault 7
#endif
}

23
include/arch/arm/arch/object/tcb.h
View file

@ -1,23 +0,0 @@
/*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#ifndef __ARCH_OBJECT_TCB_H
#define __ARCH_OBJECT_TCB_H
#include <types.h>
#include <object/structures.h>
word_t setMRs_fault(tcb_t *sender, tcb_t* receiver,
word_t *receiveIPCBuffer);
word_t CONST Arch_decodeTransfer(word_t flags);
exception_t CONST Arch_performTransfer(word_t arch, tcb_t *tcb_src,
tcb_t *tcb_dest);
#endif

1
include/arch/arm/armv/armv7-a/armv/debug.h
View file

@ -16,6 +16,7 @@
#include <config.h>
#ifdef CONFIG_HARDWARE_DEBUG_API
#include <mode/machine/debug.h>
#include <mode/machine.h> /* MRC/MCR */
#define DBGVCR_RESERVED_BITS_MASK \

21
include/arch/x86/arch/32/mode/object/structures.bf
View file

@ -107,7 +107,7 @@ block io_space_cap {
field capPCIDevice 16
padding 28
field capType 4
field capType 4
}
block io_space_capdata {
@ -194,7 +194,7 @@ tagged_union cap capType {
tag reply_cap 8
tag cnode_cap 10
tag thread_cap 12
-- Do not extend even 4-bit caps types beyond 12, as we use
-- Do not extend even 4-bit caps types beyond 12, as we use
-- 14 (0xe) to determine which caps are 8-bit.
-- 4-bit tag arch caps
@ -205,9 +205,9 @@ tagged_union cap capType {
tag asid_control_cap 9
tag asid_pool_cap 11
tag io_space_cap 13
-- Do not extend odd 4-bit caps types beyond 13, as we use
-- Do not extend odd 4-bit caps types beyond 13, as we use
-- 15 (0xf) to determine which caps are 8-bit.
-- 8-bit tag caps
tag irq_control_cap 0x0e
tag irq_handler_cap 0x1e
@ -224,7 +224,7 @@ tagged_union cap capType {
tag ept_pml4_cap 0x6f
}
---- Arch-independent object types
---- IA32 specific fault types
block vm_fault {
field address 32
@ -236,14 +236,17 @@ block vm_fault {
}
tagged_union fault faultType {
-- generic faults
tag null_fault 0
tag cap_fault 1
tag vm_fault 2
tag unknown_syscall 3
tag user_exception 4
tag unknown_syscall 2
tag user_exception 3
#ifdef CONFIG_HARDWARE_DEBUG_API
tag debug_exception 5
tag debug_exception 4
#endif
-- arch specific faults
tag vm_fault 5
}
-- VM attributes

26
include/arch/x86/arch/object/tcb.h
View file

@ -1,26 +0,0 @@
/*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#ifndef __ARCH_OBJECT_TCB_H
#define __ARCH_OBJECT_TCB_H
#include <config.h>
#include <types.h>
#include <object/structures.h>
word_t setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer);
word_t CONST Arch_decodeTransfer(word_t flags);
exception_t CONST Arch_performTransfer(word_t arch, tcb_t *tcb_src, tcb_t *tcb_dest);
#ifdef CONFIG_VTX
exception_t decodeSetEPTRoot(cap_t cap, extra_caps_t extraCaps);
void Arch_leaveVMAsyncTransfer(tcb_t *tcb);
#endif
#endif

4
include/object/tcb.h
View file

@ -15,7 +15,6 @@
#include <api/failures.h>
#include <object/structures.h>
#include <arch/object/tcb.h>
#include <machine/registerset.h>
#include <object/cnode.h>
@ -135,6 +134,9 @@ void setExtraBadge(word_t *bufferPtr, word_t badge, word_t i);
exception_t lookupExtraCaps(tcb_t* thread, word_t *bufferPtr, seL4_MessageInfo_t info);
word_t setMRs_syscall_error(tcb_t *thread, word_t *receiveIPCBuffer);
word_t CONST Arch_decodeTransfer(word_t flags);
exception_t CONST Arch_performTransfer(word_t arch, tcb_t *tcb_src,
tcb_t *tcb_dest);
#if CONFIG_MAX_NUM_NODES > 1
void migrateTCB(tcb_t *thread);

1
include/util.h
View file

@ -17,6 +17,7 @@
#define ROUND_DOWN(n, b) (((n) >> (b)) << (b))
#define ROUND_UP(n, b) (((((n) - 1ul) >> (b)) + 1ul) << (b))
#define ARRAY_SIZE(x) (sizeof(x) / sizeof(x[0]))
#define MIN(a,b) (((a)<(b))?(a):(b))
#ifndef __ASSEMBLER__

2
libsel4/arch_include/arm/sel4/arch/pfIPC.h
View file

@ -15,7 +15,7 @@
* This is what pagefault ipc looks like
* Not a standalone include! include messages.h
*/
#define SEL4_PFIPC_LABEL 2
#define SEL4_PFIPC_LABEL seL4_VMFault
#define SEL4_PFIPC_LENGTH 4
#define SEL4_PFIPC_FAULT_IP 0

2
libsel4/arch_include/x86/sel4/arch/pfIPC.h
View file

@ -15,7 +15,7 @@
* This is what pagefault ipc looks like
* Not a standalone include! include messages.h
*/
#define SEL4_PFIPC_LABEL 2
#define SEL4_PFIPC_LABEL seL4_VMFault
#define SEL4_PFIPC_LENGTH 4
#define SEL4_PFIPC_FAULT_IP 0

1
libsel4/include/sel4/messages.h
View file

@ -11,6 +11,7 @@
#ifndef __LIBSEL4_MESSAGES_H
#define __LIBSEL4_MESSAGES_H
#include <sel4/types.h>
#include <sel4/arch/pfIPC.h> /* format of pagefault ipc */
#include <sel4/arch/exIPC.h> /* format of exception ipc */
#include <sel4/arch/mapping.h> /* format and meaning of errors for mapping invocations */

12
libsel4/include/sel4/types.h
View file

@ -30,16 +30,16 @@
typedef enum {
seL4_NoFault = 0,
seL4_CapFault,
seL4_VMFault,
seL4_UnknownSyscall,
seL4_UserException,
seL4_CapFault = 1,
seL4_UnknownSyscall = 2,
seL4_UserException = 3,
#ifdef CONFIG_HARDWARE_DEBUG_API
seL4_DebugException,
seL4_DebugException = 4,
#endif
seL4_VMFault = 5,
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
seL4_VGICMaintenance = 6,
seL4_VCPUFault,
seL4_VCPUFault = 7,
#endif
SEL4_FORCE_LONG_ENUM(seL4_FaultType),
} seL4_FaultType;

4
libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/exIPC.h
View file

@ -19,8 +19,8 @@
* NOT A STANDALONE INCLUDE
*/
#define SEL4_EXCEPT_IPC_LABEL 3
#define SEL4_USER_EXCEPTION_LABEL 4
#define SEL4_EXCEPT_IPC_LABEL seL4_UnknownSyscall
#define SEL4_USER_EXCEPTION_LABEL seL4_UserException
#define SEL4_USER_EXCEPTION_LENGTH 5
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
#define SEL4_VGIC_MAINTENANCE_LENGTH 1

4
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/exIPC.h
View file

@ -16,10 +16,10 @@
*/
/* Unknown syscall exception message. */
#define SEL4_EXCEPT_IPC_LABEL 3
#define SEL4_EXCEPT_IPC_LABEL seL4_UnknownSyscall
/* User exception (such as divide by zero) message. */
#define SEL4_USER_EXCEPTION_LABEL 4
#define SEL4_USER_EXCEPTION_LABEL seL4_UserException
#define SEL4_USER_EXCEPTION_LENGTH 5
typedef enum {

1
src/api/Makefile
View file

@ -11,3 +11,4 @@
DIRECTORIES += src/api
C_SOURCES += src/api/syscall.c
C_SOURCES += src/api/faults.c

224
src/api/faults.c Normal file
View file

@ -0,0 +1,224 @@
/*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#include <config.h>
#include <types.h>
#include <api/faults.h>
#include <api/syscall.h>
#include <kernel/thread.h>
#include <machine/debug.h>
static inline unsigned int
setMRs_lookup_failure(tcb_t *receiver, word_t* receiveIPCBuffer,
lookup_fault_t luf, unsigned int offset)
{
word_t lufType = lookup_fault_get_lufType(luf);
word_t i;
i = setMR(receiver, receiveIPCBuffer, offset, lufType + 1);
switch (lufType) {
case lookup_fault_invalid_root:
return i;
case lookup_fault_missing_capability:
return setMR(receiver, receiveIPCBuffer, offset + 1,
lookup_fault_missing_capability_get_bitsLeft(luf));
case lookup_fault_depth_mismatch:
setMR(receiver, receiveIPCBuffer, offset + 1,
lookup_fault_depth_mismatch_get_bitsLeft(luf));
return setMR(receiver, receiveIPCBuffer, offset + 2,
lookup_fault_depth_mismatch_get_bitsFound(luf));
case lookup_fault_guard_mismatch:
setMR(receiver, receiveIPCBuffer, offset + 1,
lookup_fault_guard_mismatch_get_bitsLeft(luf));
setMR(receiver, receiveIPCBuffer, offset + 2,
lookup_fault_guard_mismatch_get_guardFound(luf));
return setMR(receiver, receiveIPCBuffer, offset + 3,
lookup_fault_guard_mismatch_get_bitsFound(luf));
default:
fail("Invalid lookup failure");
}
}
static inline void
copyMRsFaultReply(tcb_t *sender, tcb_t *receiver, const register_t
message[], word_t length)
{
word_t i;
for (i = 0; i < MIN(length, n_msgRegisters); i++) {
register_t r = message[i];
word_t v = getRegister(sender, msgRegisters[i]);
setRegister(receiver, r, sanitiseRegister(r, v));
}
if (i < length) {
word_t *sendBuf = lookupIPCBuffer(false, sender);
if (sendBuf) {
for (; i < length; i++) {
register_t r = message[i];
word_t v = sendBuf[i + 1];
setRegister(receiver, r, sanitiseRegister(r, v));
}
}
}
}
static inline void
copyMRsFault(tcb_t *sender, tcb_t *receiver, const register_t message[],
word_t length, word_t *receiveIPCBuffer)
{
word_t i;
for (i = 0; i < MIN(length, n_msgRegisters); i++) {
setRegister(receiver, msgRegisters[i], getRegister(sender, message[i]));
}
if (receiveIPCBuffer) {
for (; i < length; i++) {
receiveIPCBuffer[i + 1] = getRegister(sender, message[i]);
}
}
}
bool_t
handleFaultReply(tcb_t *receiver, tcb_t *sender)
{
/* These lookups are moved inward from doReplyTransfer */
seL4_MessageInfo_t tag = messageInfoFromWord(getRegister(sender, msgInfoRegister));
word_t label = seL4_MessageInfo_get_label(tag);
word_t length = seL4_MessageInfo_get_length(tag);
fault_t fault = receiver->tcbFault;
switch (fault_get_faultType(fault)) {
case fault_cap_fault:
return true;
case fault_unknown_syscall:
copyMRsFaultReply(sender, receiver, syscallMessage, MIN(length, n_syscallMessage));
return (label == 0);
case fault_user_exception:
copyMRsFaultReply(sender, receiver, exceptionMessage, MIN(length, n_exceptionMessage));
return (label == 0);
#ifdef CONFIG_HARDWARE_DEBUG_API
case fault_debug_exception: {
word_t n_instrs;
if (fault_debug_exception_get_exceptionReason(fault) != seL4_SingleStep) {
/* Only single-step replies are required to set message registers.
*/
return (label == 0);
}
if (length < DEBUG_REPLY_N_EXPECTED_REGISTERS) {
/* A single-step reply doesn't mean much if it isn't composed of the bp
* number and number of instructions to skip. But even if both aren't
* set, we can still allow the thread to continue because replying
* should uniformly resume thread execution, based on the general seL4
* API model.
*
* If it was single-step, but no reply registers were set, just
* default to skipping 1 and continuing.
*
* On x86, bp_num actually doesn't matter for single-stepping
* because single-stepping doesn't use a hardware register -- it
* uses EFLAGS.TF.
*/
n_instrs = 1;
} else {
/* If the reply had all expected registers set, proceed as normal */
n_instrs = getRegister(sender, msgRegisters[0]);
}
syscall_error_t res;
res = Arch_decodeConfigureSingleStepping(&receiver->tcbArch, 0, n_instrs, true);
if (res.type != seL4_NoError) {
return false;
};
configureSingleStepping(&receiver->tcbArch, 0, n_instrs, true);
/* Replying will always resume the thread: the only variant behaviour
* is whether or not the thread will be resumed with stepping still
* enabled.
*/
return (label == 0);
}
#endif
default:
return Arch_handleFaultReply(receiver, sender, fault_get_faultType(fault));
}
}
word_t
setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer)
{
switch (fault_get_faultType(sender->tcbFault)) {
case fault_cap_fault:
setMR(receiver, receiveIPCBuffer, 0, getRestartPC(sender));
setMR(receiver, receiveIPCBuffer, 1u,
fault_cap_fault_get_address(sender->tcbFault));
setMR(receiver, receiveIPCBuffer, 2u,
fault_cap_fault_get_inReceivePhase(sender->tcbFault));
return setMRs_lookup_failure(receiver, receiveIPCBuffer,
sender->tcbLookupFailure, 3u);
case fault_unknown_syscall: {
copyMRsFault(sender, receiver, syscallMessage, n_syscallMessage,
receiveIPCBuffer);
return setMR(receiver, receiveIPCBuffer, n_syscallMessage,
fault_unknown_syscall_get_syscallNumber(sender->tcbFault));
}
case fault_user_exception: {
copyMRsFault(sender, receiver, exceptionMessage,
n_exceptionMessage, receiveIPCBuffer);
setMR(receiver, receiveIPCBuffer, n_exceptionMessage,
fault_user_exception_get_number(sender->tcbFault));
return setMR(receiver, receiveIPCBuffer, n_exceptionMessage + 1u,
fault_user_exception_get_code(sender->tcbFault));
}
#ifdef CONFIG_HARDWARE_DEBUG_API
case fault_debug_exception: {
unsigned int ret;
word_t reason = fault_debug_exception_get_exceptionReason(sender->tcbFault);
setMR(receiver, receiveIPCBuffer,
seL4_DebugException_FaultIP, getRestartPC(sender));
setMR(receiver, receiveIPCBuffer,
seL4_DebugException_ExceptionReason, reason);
if (reason != seL4_SingleStep && reason != seL4_SoftwareBreakRequest) {
ret = setMR(receiver, receiveIPCBuffer,
seL4_DebugException_TriggerAddress,
fault_debug_exception_get_breakpointAddress(sender->tcbFault));
/* Breakpoint messages also set a "breakpoint number" register. */
ret = setMR(receiver, receiveIPCBuffer,
seL4_DebugException_BreakpointNumber,
fault_debug_exception_get_breakpointNumber(sender->tcbFault));
}
return ret;
}
#endif /* CONFIG_HARDWARE_DEBUG_API */
default:
return Arch_setMRs_fault(sender, receiver, receiveIPCBuffer,
fault_get_faultType(sender->tcbFault));
}
}

1
src/arch/arm/32/kernel/vspace.c
View file

@ -24,7 +24,6 @@
#include <arch/api/invocation.h>
#include <arch/kernel/vspace.h>
#include <arch/linker.h>
#include <arch/object/tcb.h>
#include <plat/machine/devices.h>
#include <plat/machine/hardware.h>
#include <armv/context_switch.h>

127
src/arch/arm/api/faults.c
View file

@ -16,23 +16,9 @@
#include <api/syscall.h>
bool_t
handleFaultReply(tcb_t *receiver, tcb_t *sender)
Arch_handleFaultReply(tcb_t *receiver, tcb_t *sender, word_t faultType)
{
seL4_MessageInfo_t tag;
word_t label;
fault_t fault;
word_t length;
/* These lookups are moved inward from doReplyTransfer */
tag = messageInfoFromWord(getRegister(sender, msgInfoRegister));
label = seL4_MessageInfo_get_label(tag);
length = seL4_MessageInfo_get_length(tag);
fault = receiver->tcbFault;
switch (fault_get_faultType(fault)) {
case fault_cap_fault:
return true;
switch (faultType) {
case fault_vm_fault:
return true;
@ -42,88 +28,43 @@ handleFaultReply(tcb_t *receiver, tcb_t *sender)
case fault_vcpu_fault:
return true;
#endif
case fault_unknown_syscall: {
word_t i;
register_t r;
word_t v;
word_t *sendBuf;
sendBuf = lookupIPCBuffer(false, sender);
/* Assumes n_syscallMessage > n_msgRegisters */
for (i = 0; i < length && i < n_msgRegisters; i++) {
r = syscallMessage[i];
v = getRegister(sender, msgRegisters[i]);
setRegister(receiver, r, sanitiseRegister(r, v));
}
if (sendBuf) {
for (; i < length && i < n_syscallMessage; i++) {
r = syscallMessage[i];
v = sendBuf[i + 1];
setRegister(receiver, r, sanitiseRegister(r, v));
}
}
default:
fail("Invalid fault");
}
return (label == 0);
}
case fault_user_exception: {
word_t i;
register_t r;
word_t v;
/* Assumes n_exceptionMessage <= n_msgRegisters */
for (i = 0; i < length && i < n_exceptionMessage; i++) {
r = exceptionMessage[i];
v = getRegister(sender, msgRegisters[i]);
setRegister(receiver, r, sanitiseRegister(r, v));
}
}
return (label == 0);
#ifdef CONFIG_HARDWARE_DEBUG_API
case fault_debug_exception: {
word_t n_instrs;
if (fault_debug_exception_get_exceptionReason(fault) != seL4_SingleStep) {
/* Only single-step replies are required to set message registers.
*/
return (label == 0);
}
if (length < DEBUG_REPLY_N_EXPECTED_REGISTERS) {
/* If the user didn't set all the expected registers, assume
* the number of instructions to step is 1.
*/
n_instrs = 1;
word_t
Arch_setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer, word_t faultType)
{
switch (faultType) {
case fault_vm_fault: {
if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {
word_t ipa, va;
va = getRestartPC(sender);
ipa = (addressTranslateS1CPR(va) & ~MASK(PAGE_BITS)) | (va & MASK(PAGE_BITS));
setMR(receiver, receiveIPCBuffer, 0, ipa);
} else {
/* If the reply had all expected registers set, proceed as normal */
n_instrs = getRegister(sender, msgRegisters[0]);
setMR(receiver, receiveIPCBuffer, 0, getRestartPC(sender));
}
/* When replying to a single-step fault, default the bp_num to the
* one that was configured and cached in the TCB context.
*
* configureSingleStepping() will know this because we pass "true" to
* is_reply.
*/
syscall_error_t res;
res = Arch_decodeConfigureSingleStepping(&receiver->tcbArch, 0, n_instrs, true);
if (res.type != seL4_NoError) {
return false;
};
configureSingleStepping(&receiver->tcbArch, 0, n_instrs, true);
/* Replying will always resume the thread: the only variant behaviour
* is whether or not the thread will be resumed with stepping still
* enabled.
*/
return (label == 0);
setMR(receiver, receiveIPCBuffer, 1,
fault_vm_fault_get_address(sender->tcbFault));
setMR(receiver, receiveIPCBuffer, 2,
fault_vm_fault_get_instructionFault(sender->tcbFault));
return setMR(receiver, receiveIPCBuffer, 3,
fault_vm_fault_get_FSR(sender->tcbFault));
}
#endif /* CONFIG_HARDWARE_DEBUG_API */
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
case fault_vgic_maintenance:
if (fault_vgic_maintenance_get_idxValid(sender->tcbFault)) {
return setMR(receiver, receiveIPCBuffer, 0,
fault_vgic_maintenance_get_idx(sender->tcbFault));
} else {
return setMR(receiver, receiveIPCBuffer, 0, -1);
}
case fault_vcpu_fault:
return setMR(receiver, receiveIPCBuffer, 0, fault_vcpu_fault_get_hsr(sender->tcbFault));
#endif
default:
fail("Invalid fault");

145
src/arch/arm/object/tcb.c
View file

@ -15,151 +15,6 @@
#include <machine/registerset.h>
#include <object/structures.h>
#include <arch/machine.h>
#include <arch/object/tcb.h>
static inline unsigned int
setMRs_lookup_failure(tcb_t *receiver, word_t* receiveIPCBuffer,
lookup_fault_t luf, unsigned int offset)
{
word_t lufType = lookup_fault_get_lufType(luf);
word_t i;
i = setMR(receiver, receiveIPCBuffer, offset, lufType + 1);
switch (lufType) {
case lookup_fault_invalid_root:
return i;
case lookup_fault_missing_capability:
return setMR(receiver, receiveIPCBuffer, offset + 1,
lookup_fault_missing_capability_get_bitsLeft(luf));
case lookup_fault_depth_mismatch:
setMR(receiver, receiveIPCBuffer, offset + 1,
lookup_fault_depth_mismatch_get_bitsLeft(luf));
return setMR(receiver, receiveIPCBuffer, offset + 2,
lookup_fault_depth_mismatch_get_bitsFound(luf));
case lookup_fault_guard_mismatch:
setMR(receiver, receiveIPCBuffer, offset + 1,
lookup_fault_guard_mismatch_get_bitsLeft(luf));
setMR(receiver, receiveIPCBuffer, offset + 2,
lookup_fault_guard_mismatch_get_guardFound(luf));
return setMR(receiver, receiveIPCBuffer, offset + 3,
lookup_fault_guard_mismatch_get_bitsFound(luf));
default:
fail("Invalid lookup failure");
}
}
word_t
setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer)
{
switch (fault_get_faultType(sender->tcbFault)) {
case fault_cap_fault:
setMR(receiver, receiveIPCBuffer, 0, getRestartPC(sender));
setMR(receiver, receiveIPCBuffer, 1,
fault_cap_fault_get_address(sender->tcbFault));
setMR(receiver, receiveIPCBuffer, 2,
fault_cap_fault_get_inReceivePhase(sender->tcbFault));
return setMRs_lookup_failure(receiver, receiveIPCBuffer,
sender->tcbLookupFailure, 3);
case fault_vm_fault: {
if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {
word_t ipa, va;
va = getRestartPC(sender);
ipa = (addressTranslateS1CPR(va) & ~MASK(PAGE_BITS)) | (va & MASK(PAGE_BITS));
setMR(receiver, receiveIPCBuffer, 0, ipa);
} else {
setMR(receiver, receiveIPCBuffer, 0, getRestartPC(sender));
}
setMR(receiver, receiveIPCBuffer, 1,
fault_vm_fault_get_address(sender->tcbFault));
setMR(receiver, receiveIPCBuffer, 2,
fault_vm_fault_get_instructionFault(sender->tcbFault));
return setMR(receiver, receiveIPCBuffer, 3,
fault_vm_fault_get_FSR(sender->tcbFault));
}
case fault_unknown_syscall: {
word_t i;
assert (n_syscallMessage >= n_msgRegisters);
for (i = 0; i < n_msgRegisters; i++) {
setRegister(receiver, msgRegisters[i],
getRegister(sender, syscallMessage[i]));
}
if (receiveIPCBuffer) {
for (; i < n_syscallMessage; i++) {
receiveIPCBuffer[i + 1] =
getRegister(sender, syscallMessage[i]);
}
receiveIPCBuffer[i + 1] =
fault_unknown_syscall_get_syscallNumber(sender->tcbFault);
return n_syscallMessage + 1;
} else {
return n_msgRegisters;
}
}
case fault_user_exception: {
word_t i;
assert (n_exceptionMessage < n_msgRegisters);
for (i = 0; i < n_exceptionMessage; i++) {
setRegister(receiver, msgRegisters[i],
getRegister(sender, exceptionMessage[i]));
}
setMR(receiver, receiveIPCBuffer, n_exceptionMessage,
fault_user_exception_get_number(sender->tcbFault));
return setMR(receiver, receiveIPCBuffer, n_exceptionMessage + 1,
fault_user_exception_get_code(sender->tcbFault));
}
#ifdef CONFIG_HARDWARE_DEBUG_API
case fault_debug_exception: {
unsigned int ret;
word_t reason = fault_debug_exception_get_exceptionReason(sender->tcbFault);
setMR(receiver, receiveIPCBuffer,
seL4_DebugException_FaultIP, getRestartPC(sender));
setMR(receiver, receiveIPCBuffer,
seL4_DebugException_ExceptionReason, reason);
if (reason != seL4_SingleStep && reason != seL4_SoftwareBreakRequest) {
ret = setMR(receiver, receiveIPCBuffer,
seL4_DebugException_TriggerAddress,
fault_debug_exception_get_breakpointAddress(sender->tcbFault));
/* Breakpoint messages also set a "breakpoint number" register. */
ret = setMR(receiver, receiveIPCBuffer,
seL4_DebugException_BreakpointNumber,
fault_debug_exception_get_breakpointNumber(sender->tcbFault));
}
return ret;
}
#endif /* CONFIG_HARDWARE_DEBUG_API */
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
case fault_vgic_maintenance:
if (fault_vgic_maintenance_get_idxValid(sender->tcbFault)) {
return setMR(receiver, receiveIPCBuffer, 0,
fault_vgic_maintenance_get_idx(sender->tcbFault));
} else {
return setMR(receiver, receiveIPCBuffer, 0, -1);
}
case fault_vcpu_fault:
return setMR(receiver, receiveIPCBuffer, 0, fault_vcpu_fault_get_hsr(sender->tcbFault));
#endif
default:
fail("Invalid fault");
}
}
word_t CONST
Arch_decodeTransfer(word_t flags)

2
src/arch/x86/32/machine/registerset.c
View file

@ -31,7 +31,7 @@ const register_t exceptionMessage[] = {
};
const register_t syscallMessage[] = {
EAX, EBX, ECX, EDX, ESI, EDI, EBP, NextIP, ESP, FLAGS
EAX, EBX, ECX, EDX, ESI, EDI, EBP, FaultIP, ESP, EFLAGS
};
#ifdef CONFIG_VTX

134
src/arch/x86/api/faults.c
View file

@ -9,135 +9,35 @@
*/
#include <types.h>
#include <object.h>
#include <machine/io.h>
#include <machine/debug.h>
#include <plat/api/constants.h>
#include <kernel/vspace.h>
#include <api/faults.h>
#include <api/syscall.h>
#include <util.h>
bool_t handleFaultReply(tcb_t *receiver, tcb_t *sender)
bool_t Arch_handleFaultReply(tcb_t *receiver, tcb_t *sender, word_t faultType)
{
seL4_MessageInfo_t tag;
word_t label;
fault_t fault;
unsigned int length;
/* These lookups are moved inward from doReplyTransfer */
tag = messageInfoFromWord(getRegister(sender, msgInfoRegister));
label = seL4_MessageInfo_get_label(tag);
length = seL4_MessageInfo_get_length(tag);
fault = receiver->tcbFault;
switch (fault_get_faultType(fault)) {
case fault_cap_fault:
return true;
switch (faultType) {
case fault_vm_fault:
return true;
case fault_unknown_syscall: {
word_t i;
register_t r;
word_t v;
word_t* sendBuf;
sendBuf = lookupIPCBuffer(false, sender);
/* Assumes n_syscallMessage > n_msgRegisters */
for (i = 0; i < length && i < n_msgRegisters; i++) {
r = syscallMessage[i];
v = getRegister(sender, msgRegisters[i]);
setRegister(receiver, r, sanitiseRegister(r, v));
}
if (sendBuf) {
for (; i < length && i < n_syscallMessage; i++) {
r = syscallMessage[i];
v = sendBuf[i + 1];
setRegister(receiver, r, sanitiseRegister(r, v));
}
}
/* HACK: Copy NextIP to FaultIP because FaultIP will be copied */
/* back to NextIP later on (and we don't wanna lose NextIP) */
setRegister(receiver, FaultIP, getRegister(receiver, NextIP));
default:
fail("Invalid fault");
}
return (label == 0);
}
case fault_user_exception: {
word_t i;
register_t r;
word_t v;
word_t* sendBuf;
sendBuf = lookupIPCBuffer(false, sender);
/* Assumes n_exceptionMessage > n_msgRegisters */
for (i = 0; i < length && i < n_msgRegisters; i++) {
r = exceptionMessage[i];
v = getRegister(sender, msgRegisters[i]);
setRegister(receiver, r, sanitiseRegister(r, v));
}
if (sendBuf) {
for (; i < length && i < n_exceptionMessage; i++) {
r = exceptionMessage[i];
v = sendBuf[i + 1];
setRegister(receiver, r, sanitiseRegister(r, v));
}
}
word_t
Arch_setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer, word_t faultType)
{
switch (faultType) {
case fault_vm_fault: {
setMR(receiver, receiveIPCBuffer, 0, getRestartPC(sender));
setMR(receiver, receiveIPCBuffer, 1,
fault_vm_fault_get_address(sender->tcbFault));
setMR(receiver, receiveIPCBuffer, 2,
fault_vm_fault_get_instructionFault(sender->tcbFault));
return setMR(receiver, receiveIPCBuffer, 3,
fault_vm_fault_get_FSR(sender->tcbFault));
}
return (label == 0);
#ifdef CONFIG_HARDWARE_DEBUG_API
case fault_debug_exception: {
word_t n_instrs;
if (fault_debug_exception_get_exceptionReason(fault) != seL4_SingleStep) {
/* Only single-step replies are required to set message registers.
*/
return (label == 0);
}
if (length < DEBUG_REPLY_N_EXPECTED_REGISTERS) {
/* A single-step reply doesn't mean much if it isn't composed of the bp
* number and number of instructions to skip. But even if both aren't
* set, we can still allow the thread to continue because replying
* should uniformly resume thread execution, based on the general seL4
* API model.
*
* If it was single-step, but no reply registers were set, just
* default to skipping 1 and continuing.
*
* On x86, bp_num actually doesn't matter for single-stepping
* because single-stepping doesn't use a hardware register -- it
* uses EFLAGS.TF.
*/
n_instrs = 1;
} else {
/* If the reply had all expected registers set, proceed as normal */
n_instrs = getRegister(sender, msgRegisters[0]);
}
syscall_error_t res;
res = Arch_decodeConfigureSingleStepping(&receiver->tcbArch, 0, n_instrs, true);
if (res.type != seL4_NoError) {
return false;
};
configureSingleStepping(&receiver->tcbArch, 0, n_instrs, true);
/* Replying will always resume the thread: the only variant behaviour
* is whether or not the thread will be resumed with stepping still
* enabled.
*/
return (label == 0);
}
#endif
default:
fail("Invalid fault");
}

1
src/arch/x86/c_traps.c
View file

@ -119,6 +119,7 @@ slowpath(syscall_t syscall)
ksKernelEntry.path = Entry_UnknownSyscall;
/* ksKernelEntry.word word is already set to syscall */
#endif /* TRACK_KERNEL_ENTRIES */
ksCurThread->tcbArch.tcbContext.registers[FaultIP] = ksCurThread->tcbArch.tcbContext.registers[NextIP];
handleUnknownSyscall(syscall);
} else {
#ifdef TRACK_KERNEL_ENTIRES

120
src/arch/x86/object/tcb.c
View file

@ -13,126 +13,6 @@
#include <machine/registerset.h>
#include <object/structures.h>
#include <arch/machine.h>
#include <arch/object/tcb.h>
/* NOTE: offset is either 1 or 3 */
static inline unsigned int
setMRs_lookup_failure(tcb_t *receiver, word_t* receiveIPCBuffer, lookup_fault_t luf, unsigned int offset)
{
word_t lufType = lookup_fault_get_lufType(luf);
word_t i;
i = setMR(receiver, receiveIPCBuffer, offset, lufType + 1);
switch (lufType) {
case lookup_fault_invalid_root:
return i;
case lookup_fault_missing_capability:
return setMR(receiver, receiveIPCBuffer, offset + 1,
lookup_fault_missing_capability_get_bitsLeft(luf));
case lookup_fault_depth_mismatch:
setMR(receiver, receiveIPCBuffer, offset + 1,
lookup_fault_depth_mismatch_get_bitsLeft(luf));
return setMR(receiver, receiveIPCBuffer, offset + 2,
lookup_fault_depth_mismatch_get_bitsFound(luf));
case lookup_fault_guard_mismatch:
setMR(receiver, receiveIPCBuffer, offset + 1,
lookup_fault_guard_mismatch_get_bitsLeft(luf));
setMR(receiver, receiveIPCBuffer, offset + 2,
lookup_fault_guard_mismatch_get_guardFound(luf));
return setMR(receiver, receiveIPCBuffer, offset + 3,
lookup_fault_guard_mismatch_get_bitsFound(luf));
default:
fail("Invalid lookup failure");
}
}
word_t setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer)
{
switch (fault_get_faultType(sender->tcbFault)) {
case fault_cap_fault:
setMR(receiver, receiveIPCBuffer, 0, getRestartPC(sender));
setMR(receiver, receiveIPCBuffer, 1, fault_cap_fault_get_address(sender->tcbFault));
setMR(receiver, receiveIPCBuffer, 2, fault_cap_fault_get_inReceivePhase(sender->tcbFault));
return setMRs_lookup_failure(receiver, receiveIPCBuffer, sender->tcbLookupFailure, 3);
case fault_vm_fault:
setMR(receiver, receiveIPCBuffer, 0, getRestartPC(sender));
setMR(receiver, receiveIPCBuffer, 1, fault_vm_fault_get_address(sender->tcbFault));
setMR(receiver, receiveIPCBuffer, 2, fault_vm_fault_get_instructionFault(sender->tcbFault));
return setMR(receiver, receiveIPCBuffer, 3, fault_vm_fault_get_FSR(sender->tcbFault));
case fault_unknown_syscall: {
word_t i;
for (i = 0; i < n_msgRegisters; i++) {
setRegister(receiver, msgRegisters[i],
getRegister(sender, syscallMessage[i]));
}
if (receiveIPCBuffer) {
for (; i < n_syscallMessage; i++) {
receiveIPCBuffer[i + 1] =
getRegister(sender, syscallMessage[i]);
}
receiveIPCBuffer[i + 1] =
fault_unknown_syscall_get_syscallNumber(sender->tcbFault);
return n_syscallMessage + 1;
} else {
return n_msgRegisters;
}
}
case fault_user_exception: {
word_t i;
for (i = 0; i < n_msgRegisters; i++) {
setRegister(receiver, msgRegisters[i],
getRegister(sender, exceptionMessage[i]));
}
if (receiveIPCBuffer) {
for (; i < n_exceptionMessage; i++) {
receiveIPCBuffer[i + 1] =
getRegister(sender, exceptionMessage[i]);
}
receiveIPCBuffer[n_exceptionMessage + 1] =
fault_user_exception_get_number(sender->tcbFault);
receiveIPCBuffer[n_exceptionMessage + 2] =
fault_user_exception_get_code(sender->tcbFault);
return n_exceptionMessage + 2;
} else {
return n_msgRegisters;
}
}
#ifdef CONFIG_HARDWARE_DEBUG_API
case fault_debug_exception: {
unsigned int ret;
word_t reason = fault_debug_exception_get_exceptionReason(sender->tcbFault);
setMR(receiver, receiveIPCBuffer,
seL4_DebugException_FaultIP, getRestartPC(sender));
ret = setMR(receiver, receiveIPCBuffer,
seL4_DebugException_ExceptionReason, reason);
if (reason != seL4_SingleStep && reason != seL4_SoftwareBreakRequest) {
ret = setMR(receiver, receiveIPCBuffer,
seL4_DebugException_TriggerAddress,
fault_debug_exception_get_breakpointAddress(sender->tcbFault));
/* Breakpoint messages also set a "breakpoint number" register. */
ret = setMR(receiver, receiveIPCBuffer,
seL4_DebugException_BreakpointNumber,
fault_debug_exception_get_breakpointNumber(sender->tcbFault));
}
return ret;
}
#endif
default:
fail("Invalid fault");
}
}
word_t CONST Arch_decodeTransfer(word_t flags)
{