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

SELFOUR-499: X86, ARM: Add userspace invocations for hardware debugging

Browse source 
This commit implements the body of SELFOUR-499. The API exposes the x86 DR0-7
and ARM coprocessor 14 features to userspace by virtualizing them as context-
switched registers in the TCB. Implemented as TCB invocations. This feature is
only built when CONFIG_HARDWARE_DEBUG_API is selected.

* Add low-level support routines for setting, unsetting, getting, enabling
  and disabling breakpoints.
* Add support for single-stepping as well.
  ^ Single-stepping is not supported on ARMv6 since the hardware
    doesn't have support.
  ^ ARM implements single-stepping as instruction breakpoints
    configured to fault on every instruction -- this is achieved through
    the "mismatch" mode, which is only supported from ARMv7 onwards.
* Also support explicit software break requests, a la "BKPT" and "INT $3".

* New invocations:
  * seL4_TCB_SetBreakpoint().
  * seL4_TCB_GetBreakpoint().
  * seL4_TCB_UnsetBreakpoint().
  * seL4_TCB_ConfigureSingleStepping().
* New constants:
  ^ Event types:
    ^ seL4_InstructionBreakpoint.
    ^ seL4_DataBreakpoint.
    ^ seL4_SoftwareBreakRequest.
  ^ Access types:
    ^ seL4_BreakOnRead.
    ^ seL4_BreakOnWrite.
    ^ seL4_BreakOnReadWrite.
  ^ Exports:
    ^ seL4_NumHWBreakpoints.
    ^ seL4_NumExclusiveBreakpoints.
    ^ seL4_NumExclusiveWatchpoints.
    ^ seL4_NumDualFunctionMonitors.
    ^ seL4_FirstBreakpoint.
    ^ seL4_FirstWatchpoint.
    ^ seL4_FirstDualFunctionMonitor.

See documentation in the seL4 API manual.
This commit is contained in:
Kofi Doku Atuah 2016-06-23 23:09:44 +10:00
parent 8b39c73544
commit bebfcf6d27
94 changed files with 4499 additions and 330 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
Kconfig
View file

@ -401,6 +401,15 @@ menu "Build Options"
help
Allow the kernel to print out messages to the serial console during bootup and execution.
config HARDWARE_DEBUG_API
bool "Enable hardware breakpoint and single-stepping API"
depends on !VERIFICATION_BUILD
default n
help
Builds the kernel with support for a userspace debug API, which can
allows userspace processes to set breakpoints, watchpoints and to
single-step through thread execution.
config IRQ_REPORTING
bool "Report spurious or undelivered IRQs"
depends on PRINTING

11
include/api/debug.h
View file

@ -10,7 +10,7 @@
#include <config.h>
#ifdef DEBUG
#ifdef CONFIG_DEBUG_BUILD
#ifndef __API_DEBUG_H
#define __API_DEBUG_H
@ -38,6 +38,11 @@ debug_printKernelEntryReason(void)
case Entry_UserLevelFault:
printf("User level fault, number: %lu", (unsigned long) ksKernelEntry.word);
break;
#ifdef CONFIG_HARDWARE_DEBUG_API
case Entry_DebugFault:
printf("Debug fault. Fault Vaddr: 0x%lx", (unsigned long) ksKernelEntry.word);
break;
#endif
case Entry_Syscall:
printf("Syscall, number: %ld\n", (long) ksKernelEntry.syscall_no);
if (ksKernelEntry.syscall_no == SysSend ||
@ -49,7 +54,7 @@ debug_printKernelEntryReason(void)
}
}
}
#endif
#endif /* CONFIG_PRINTING */
#endif /* __API_DEBUG_H */
#endif /* DEBUG */
#endif /* CONFIG_DEBUG_BUILD */

206
include/arch/arm/arch/32/mode/machine/debug.h
View file

@ -1,22 +1,28 @@
/*
* Copyright 2014, General Dynamics C4 Systems
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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)
* @TAG(D61_GPL)
*/
#pragma once
#ifndef __ARCH_MACHINE_DEBUG_32_H
#define __ARCH_MACHINE_DEBUG_32_H
#include <config.h>
#if defined(CONFIG_DEBUG_BUILD) || defined (CONFIG_HARDWARE_DEBUG_API)
#ifdef DEBUG
#define DBGDSCR_int "p14,0,%0,c0,c1,0"
#define DBGDSCR_ext "p14, 0, %0, c0, c2, 2"
#define MAX_BREAKPOINTS 16
#define DBGWFAR "p14,0,%0,c0,c6,0"
#define DFAR "p15,0,%0,c6,c0,0"
#ifndef __ASSEMBLER__
#include <stdint.h>
#include <mode/machine.h>
#include <arch/machine/registerset.h>
void debug_init(void) VISIBLE;
@ -71,6 +77,21 @@ getDIDR(void)
return x;
}
#ifdef CONFIG_HARDWARE_DEBUG_API
#define DEBUG_REPLY_N_REQUIRED_REGISTERS (1)
/* Get Watchpoint Fault Address register value (for async watchpoints). */
static inline word_t
getWFAR(void)
{
word_t ret;
MRC(DBGWFAR, ret);
return ret;
}
#endif
#endif /* !__ASSEMBLER__ */
/* Debug Status and Control Register */
@ -81,30 +102,13 @@ getDIDR(void)
#define DEBUG_ENTRY_DBGTAP_HALT 0
#define DEBUG_ENTRY_BREAKPOINT 1
#define DEBUG_ENTRY_WATCHPOINT 2
#define DEBUG_ENTRY_ASYNC_WATCHPOINT 2
#define DEBUG_ENTRY_EXPLICIT_BKPT 3
#define DEBUG_ENTRY_EDBGRQ 4
#define DEBUG_ENTRY_VECTOR_CATCH 5
#define DEBUG_ENTRY_DATA_ABORT 6
#define DEBUG_ENTRY_INSTRUCTION_ABORT 7
#ifndef __ASSEMBLER__
static inline uint32_t
getDSCR(void)
{
uint32_t x;
asm volatile("mrc p14, 0, %0, c0, c1, 0" : "=r"(x));
return x;
}
static inline void
setDSCR(uint32_t x)
{
asm volatile("mcr p14, 0, %0, c0, c1, 0" : : "r"(x));
}
#endif /* !__ASSEMBLER__ */
#define DEBUG_ENTRY_SYNC_WATCHPOINT (0xA)
/* Vector Catch Register */
#define VCR_FIQ 7
@ -132,64 +136,6 @@ setVCR(uint32_t x)
asm volatile("mcr p14, 0, %0, c0, c7, 0" : : "r"(x));
}
/* Breakpoint Value Registers */
static inline uint32_t
getBVR(int n)
{
uint32_t x = 0;
switch (n) {
case 0:
asm volatile("mrc p14, 0, %0, c0, c0, 4" : "=r"(x));
break;
case 1:
asm volatile("mrc p14, 0, %0, c0, c1, 4" : "=r"(x));
break;
case 2:
asm volatile("mrc p14, 0, %0, c0, c2, 4" : "=r"(x));
break;
case 3:
asm volatile("mrc p14, 0, %0, c0, c3, 4" : "=r"(x));
break;
case 4:
asm volatile("mrc p14, 0, %0, c0, c4, 4" : "=r"(x));
break;
case 5:
asm volatile("mrc p14, 0, %0, c0, c5, 4" : "=r"(x));
break;
default:
break;
}
return x;
}
static inline void
setBVR(int n, uint32_t x)
{
switch (n) {
case 0:
asm volatile("mcr p14, 0, %0, c0, c0, 4" : : "r"(x));
break;
case 1:
asm volatile("mcr p14, 0, %0, c0, c1, 4" : : "r"(x));
break;
case 2:
asm volatile("mcr p14, 0, %0, c0, c2, 4" : : "r"(x));
break;
case 3:
asm volatile("mcr p14, 0, %0, c0, c3, 4" : : "r"(x));
break;
case 4:
asm volatile("mcr p14, 0, %0, c0, c4, 4" : : "r"(x));
break;
case 5:
asm volatile("mcr p14, 0, %0, c0, c5, 4" : : "r"(x));
break;
default:
break;
}
}
#endif /* !__ASSEMBLER__ */
/* Breakpoint Control Registers */
@ -200,66 +146,56 @@ setBVR(int n, uint32_t x)
#define BCR_SUPERVISOR 1
#define BCR_ENABLE 0
#define FSR_SHORTDESC_STATUS_DEBUG_EVENT (0x2)
#define FSR_LONGDESC_STATUS_DEBUG_EVENT (0x22)
#define FSR_LPAE_SHIFT (9)
#define FSR_STATUS_BIT4_SHIFT (10)
#ifndef __ASSEMBLER__
static inline uint32_t
getBCR(int n)
#ifdef CONFIG_HARDWARE_DEBUG_API
/** Determines whether or not a Prefetch Abort or Data Abort was really a debug
* exception.
*
* Examines the FSR bits, looking for the "Debug event" value, and also examines
* DBGDSCR looking for the "Async watchpoint abort" value, since async
* watchpoints behave differently.
*/
bool_t isDebugFault(word_t hsr_or_fsr);
/** Determines and carries out what needs to be done for a debug exception.
*
* This could be handling a single-stepping exception, or a breakpoint or
* watchpoint.
*/
fault_t handleUserLevelDebugException(word_t fault_vaddr);
/** These next two functions are part of some state flags.
*
* A bitfield of all currently enabled breakpoints for a thread is kept in that
* thread's TCB. These two functions here set and unset the bits in that
* bitfield.
*/
static inline void
setBreakpointUsedFlag(arch_tcb_t *uds, uint16_t bp_num)
{
uint32_t x = 0;
switch (n) {
case 0:
asm volatile("mrc p14, 0, %0, c0, c0, 5" : "=r"(x));
break;
case 1:
asm volatile("mrc p14, 0, %0, c0, c1, 5" : "=r"(x));
break;
case 2:
asm volatile("mrc p14, 0, %0, c0, c2, 5" : "=r"(x));
break;
case 3:
asm volatile("mrc p14, 0, %0, c0, c3, 5" : "=r"(x));
break;
case 4:
asm volatile("mrc p14, 0, %0, c0, c4, 5" : "=r"(x));
break;
case 5:
asm volatile("mrc p14, 0, %0, c0, c5, 5" : "=r"(x));
break;
default:
break;
if (uds != NULL) {
uds->tcbContext.breakpointState.used_breakpoints_bf |= BIT(bp_num);
}
return x;
}
static inline void
setBCR(int n, uint32_t x)
unsetBreakpointUsedFlag(arch_tcb_t *uds, uint16_t bp_num)
{
switch (n) {
case 0:
asm volatile("mcr p14, 0, %0, c0, c0, 5" : : "r"(x));
break;
case 1:
asm volatile("mcr p14, 0, %0, c0, c1, 5" : : "r"(x));
break;
case 2:
asm volatile("mcr p14, 0, %0, c0, c2, 5" : : "r"(x));
break;
case 3:
asm volatile("mcr p14, 0, %0, c0, c3, 5" : : "r"(x));
break;
case 4:
asm volatile("mcr p14, 0, %0, c0, c4, 5" : : "r"(x));
break;
case 5:
asm volatile("mcr p14, 0, %0, c0, c5, 5" : : "r"(x));
break;
default:
break;
if (uds != NULL) {
uds->tcbContext.breakpointState.used_breakpoints_bf &= ~BIT(bp_num);
}
}
void restore_user_debug_context(tcb_t *target_thread);
#endif /* CONFIG_HARDWARE_DEBUG_API */
#endif /* !__ASSEMBLER__ */
#endif /* DEBUG */
#endif /* !__ARCH_MACHINE_DEBUG_32_H */
#endif /* defined(CONFIG_DEBUG_BUILD) || defined (CONFIG_HARDWARE_DEBUG_API) */

43
include/arch/arm/arch/32/mode/machine/registerset.h
View file

@ -18,7 +18,7 @@
* they are useful in identifying invalid memory access bugs
* so we enable them in debug mode.
*/
#ifdef DEBUG
#ifdef CONFIG_DEBUG_BUILD
#define CPSR_EXTRA_FLAGS 0
#else
#define CPSR_EXTRA_FLAGS PMASK_ASYNC_ABORT
@ -49,8 +49,10 @@
#include <config.h>
#include <stdint.h>
#include <assert.h>
#include <util.h>
#include <arch/types.h>
#include <plat/api/constants.h>
/* These are the indices of the registers in the
* saved thread context. The values are determined
@ -118,15 +120,52 @@ extern const register_t gpRegisters[] VISIBLE;
extern const register_t exceptionMessage[] VISIBLE;
extern const register_t syscallMessage[] VISIBLE;
/* ARM user-code context: size = 72 bytes */
#ifdef CONFIG_HARDWARE_DEBUG_API
typedef struct debug_register_pair {
word_t cr, vr;
} debug_register_pair_t;
typedef struct user_breakpoint_state {
/* We don't use context comparisons. */
debug_register_pair_t breakpoint[seL4_NumExclusiveBreakpoints],
watchpoint[seL4_NumExclusiveWatchpoints];
uint32_t used_breakpoints_bf;
word_t n_instructions;
bool_t single_step_enabled;
uint16_t single_step_hw_bp_num;
} user_breakpoint_state_t;
void Arch_initBreakpointContext(user_breakpoint_state_t *context);
#endif
/* ARM user-code context: size = 72 bytes
* Or with hardware debug support built in:
* 72 + sizeof(word_t) * (NUM_BPS + NUM_WPS) * 2
*
* The "word_t registers" member of this struct must come first, because in
* head.S, we assume that an "ldr %0, =ksCurThread" will point to the beginning
* of the current thread's registers. The assert below should help.
*/
struct user_context {
word_t registers[n_contextRegisters];
#ifdef CONFIG_HARDWARE_DEBUG_API
user_breakpoint_state_t breakpointState;
#endif
};
typedef struct user_context user_context_t;
#ifdef CONFIG_DEBUG_BUILD
compile_assert(registers_are_first_member_of_user_context,
__builtin_offsetof(user_context_t, registers) == 0)
#endif
static inline void Arch_initContext(user_context_t* context)
{
context->registers[CPSR] = CPSR_USER;
#ifdef CONFIG_HARDWARE_DEBUG_API
Arch_initBreakpointContext(&context->breakpointState);
#endif
}
static inline word_t CONST

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

@ -219,9 +219,12 @@ tagged_union fault faultType {
tag vm_fault 2
tag unknown_syscall 3
tag user_exception 4
#ifdef CONFIG_HARDWARE_DEBUG_API
tag debug_exception 5
#endif
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
tag vgic_maintenance 5
tag vcpu_fault 6
tag vgic_maintenance 6
tag vcpu_fault 7
#endif
}
@ -515,3 +518,79 @@ tagged_union virq virqType {
tag virq_active 2
}
#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
#ifdef CONFIG_HARDWARE_DEBUG_API
-- ARM breakpoint/watchpoint register layouts
-- Debug ID reg
block dbg_didr {
field numWrps 4
field numBrps 4
field numContextIdBrps 4
field version 4
padding 8
field variant 4
field revision 4
}
-- Status and control reg
block dbg_dscr {
padding 3
padding 10
field nonSecureState 1
field securePrivilegedNIDebugDisabled 1
field securePrivilegedIDebugDisabled 1
field monitorDebugEnable 1
field haltingDebugEnable 1
padding 1
field disableAllUserAccesses 1
field interruptDisable 1
field debugAcknowledge 1
padding 2
field stickyImpreciseAbort 1
field stickyPreciseAbort 1
field methodOfEntry 4
padding 2
}
-- Breakpoint control reg
block dbg_bcr {
padding 3
field addressMask 5
#ifdef CONFIG_ARCH_ARM_V6
padding 1
field meaning 2
field enableLinking 1
#else
field breakpointType 4
#endif
field linkedBrp 4
field secureStateControl 2
field hypeModeControl 1
padding 4
field byteAddressSelect 4
padding 2
field supervisorAccess 2
field enabled 1
}
-- Watchpoint control reg
block dbg_wcr {
padding 3
field addressMask 5
padding 3
field enableLinking 1
field linkedBrp 4
#ifndef CONFIG_ARCH_ARM_V6
field secureStateControl 2
field hypeModeControl 1
field byteAddressSelect 8
#else
padding 7
field byteAddressSelect 4
#endif
field loadStore 2
field supervisorAccess 2
field enabled 1
}
#endif /* CONFIG_HARDWARE_DEBUG_API */

5
include/arch/arm/arch/fastpath/fastpath.h
View file

@ -14,6 +14,7 @@
#include <arch/linker.h>
#include <mode/fastpath/fastpath.h>
#include <benchmark_track.h>
#include <mode/machine/debug.h>
void slowpath(syscall_t syscall) NORETURN;
@ -23,6 +24,10 @@ static inline void NORETURN fastpath_restore(word_t badge, word_t msgInfo, tcb_t
c_exit_hook();
#ifdef CONFIG_HARDWARE_DEBUG_API
restore_user_debug_context(ksCurThread);
#endif
register word_t badge_reg asm("r0") = badge;
register word_t msgInfo_reg asm("r1") = msgInfo;
register word_t cur_thread_reg asm("r2") = (word_t)cur_thread;

178
include/arch/arm/arch/machine/debug.h
View file

@ -1,16 +1,186 @@
/*
* Copyright 2014, General Dynamics C4 Systems
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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)
* @TAG(D61_GPL)
*/
#ifndef __ARCH_MACHINE_DEBUG_H
#define __ARCH_MACHINE_DEBUG_H
#include <mode/machine/debug.h>
#include <util.h>
#include <plat/api/constants.h>
#include <armv/debug.h>
#ifdef CONFIG_HARDWARE_DEBUG_API
static uint16_t
convertBpNumToArch(uint16_t bp_num)
{
if (bp_num >= seL4_NumExclusiveBreakpoints) {
bp_num -= seL4_NumExclusiveBreakpoints;
}
return bp_num;
}
static word_t
getTypeFromBpNum(uint16_t bp_num)
{
return (bp_num >= seL4_NumExclusiveBreakpoints)
? seL4_DataBreakpoint
: seL4_InstructionBreakpoint;
}
static inline syscall_error_t
Arch_decodeConfigureSingleStepping(arch_tcb_t *at,
uint16_t bp_num,
word_t n_instr,
bool_t is_reply)
{
word_t type;
syscall_error_t ret = {
.type = seL4_NoError
};
if (is_reply) {
/* If this is a single-step fault reply, just default to the already-
* configured bp_num. Of course, this assumes that a register had
* already previously been configured for single-stepping.
*/
if (!at->tcbContext.breakpointState.single_step_enabled) {
userError("Debug: Single-step reply when single-stepping not "
"enabled.");
ret.type = seL4_IllegalOperation;
return ret;
}
type = seL4_InstructionBreakpoint;
bp_num = at->tcbContext.breakpointState.single_step_hw_bp_num;
} else {
type = getTypeFromBpNum(bp_num);
bp_num = convertBpNumToArch(bp_num);
}
if (type != seL4_InstructionBreakpoint || bp_num >= seL4_FirstWatchpoint) {
/* Must use an instruction BP register */
userError("Debug: Single-stepping can only be used with an instruction "
"breakpoint.");
ret.type = seL4_InvalidArgument;
ret.invalidArgumentNumber = 0;
return ret;
}
if (at->tcbContext.breakpointState.single_step_enabled == true) {
if (bp_num != at->tcbContext.breakpointState.single_step_hw_bp_num) {
/* Can't configure more than one register for stepping. */
userError("Debug: Only one register can be configured for "
"single-stepping at a time.");
ret.type = seL4_InvalidArgument;
ret.invalidArgumentNumber = 0;
return ret;
}
}
return ret;
}
bool_t byte8WatchpointsSupported(void);
static inline syscall_error_t
Arch_decodeSetBreakpoint(arch_tcb_t *uds,
uint16_t bp_num, word_t vaddr, word_t type,
word_t size, word_t rw)
{
syscall_error_t ret = {
.type = seL4_NoError
};
bp_num = convertBpNumToArch(bp_num);
if (type == seL4_DataBreakpoint) {
if (bp_num >= seL4_NumExclusiveWatchpoints) {
userError("Debug: invalid data-watchpoint number %u.", bp_num);
ret.type = seL4_RangeError;
ret.rangeErrorMin = 0;
ret.rangeErrorMax = seL4_NumExclusiveBreakpoints - 1;
return ret;
}
} else if (type == seL4_InstructionBreakpoint) {
if (bp_num >= seL4_NumExclusiveBreakpoints) {
userError("Debug: invalid instruction breakpoint nunber %u.", bp_num);
ret.type = seL4_RangeError;
ret.rangeErrorMin = 0;
ret.rangeErrorMax = seL4_NumExclusiveWatchpoints - 1;
return ret;
}
}
if (size == 8 && !byte8WatchpointsSupported()) {
userError("Debug: 8-byte watchpoints not supported on this CPU.");
ret.type = seL4_InvalidArgument;
ret.invalidArgumentNumber = 3;
return ret;
}
if (size == 8 && type != seL4_DataBreakpoint) {
userError("Debug: 8-byte sizes can only be used with watchpoints.");
ret.type = seL4_InvalidArgument;
ret.invalidArgumentNumber = 3;
return ret;
}
return ret;
}
static inline syscall_error_t
Arch_decodeGetBreakpoint(arch_tcb_t *uds, uint16_t bp_num)
{
syscall_error_t ret = {
.type = seL4_NoError
};
if (bp_num >= seL4_FirstWatchpoint + seL4_NumExclusiveWatchpoints) {
userError("Arch Debug: Invalid API bp_num %u.", bp_num);
ret.type = seL4_NoError;
return ret;
}
return ret;
}
static inline syscall_error_t
Arch_decodeUnsetBreakpoint(arch_tcb_t *uds, uint16_t bp_num)
{
syscall_error_t ret = {
.type = seL4_NoError
};
if (bp_num >= seL4_FirstWatchpoint + seL4_NumExclusiveWatchpoints) {
userError("Arch Debug: Invalid API bp_num %u.", bp_num);
ret.type = seL4_NoError;
return ret;
}
word_t type;
dbg_bcr_t bcr;
type = getTypeFromBpNum(bp_num);
bp_num = convertBpNumToArch(bp_num);
bcr.words[0] = uds->tcbContext.breakpointState.breakpoint[bp_num].cr;
if (type == seL4_InstructionBreakpoint) {
if (Arch_breakpointIsMismatch(bcr) == true && dbg_bcr_get_enabled(bcr)) {
userError("Rejecting call to unsetBreakpoint on breakpoint configured "
"for single-stepping (hwid %u).", bp_num);
ret.type = seL4_IllegalOperation;
return ret;
}
}
return ret;
}
#endif /* CONFIG_HARDWARE_DEBUG_API */
#endif /* !__ARCH_MACHINE_DEBUG_H */

146
include/arch/arm/armv/armv6/armv/debug.h Normal file
View file

@ -0,0 +1,146 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_GPL)
*/
#pragma once
#include <config.h>
#ifdef CONFIG_HARDWARE_DEBUG_API
#define DBGVCR_RESERVED_BITS_MASK (0xFFFFFFF0|BIT(5))
enum v6_breakpoint_meaning /* BCR[22:21] */ {
DBGBCR_V6MEANING_INSTRUCTION_VADDR_MATCH = 0u,
DBGBCR_V6MEANING_CONTEXT_ID_MATCH = 1u,
DBGBCR_V6MEANING_INSTRUCTION_VADDR_MISMATCH = 2u
};
/** Read DBGDSCR from CP14.
*
* DBGDSCR_ext (external view) is not exposed on debug v6. Accessing it on
* v6 triggers an #UNDEFINED abort.
*/
static word_t
readDscrCp(void)
{
word_t v;
MRC(DBGDSCR_int, v);
return v;
}
/** Write DBGDSCR (Status and control register).
*
* On ARMv6, there is no mmapping, and the coprocessor doesn't expose an
* external vs internal view of DSCR. There's only the internal, but the MDBGEn
* but is RW (as opposed to V7 where the internal MDBGEn is RO).
*
* Even so, the KZM still ignores our writes anyway *shrug*.
*/
static void
writeDscrCp(word_t val)
{
MCR(DBGDSCR_int, val);
}
/** Determines whether or not 8-byte watchpoints are supported.
*/
static inline bool_t
watchpoint8bSupported(void)
{
/* V6 doesn't support 8B watchpoints. */
return false;
}
/** Enables the debug architecture mode that allows us to receive debug events
* as exceptions.
*
* CPU can operate in one of 2 debug architecture modes: "halting" and
* "monitor". In halting mode, when a debug event occurs, the CPU will halt
* execution and enter a special state in which it can be examined by an
* external debugger dongle.
*
* In monitor mode, the CPU will deliver debug events to the kernel as
* exceptions. Monitor mode is what's actually useful to us. If it's not
* supported by the CPU, it's impossible for the API to work.
*
* Unfortunately, it's also gated behind a hardware pin signal, #DBGEN. If
* #DBGEN is held low, monitor mode is unavailable.
*/
BOOT_CODE static bool_t
enableMonitorMode(void)
{
dbg_dscr_t dscr;
dscr.words[0] = readDscrCp();
/* HDBGEn is read-only on v6 debug. */
if (dbg_dscr_get_haltingDebugEnable(dscr) != 0) {
printf("Halting debug is enabled, and can't be disabled. Monitor mode "
"unavailable.\n");
return false;
}
dscr = dbg_dscr_set_monitorDebugEnable(dscr, 1);
writeDscrCp(dscr.words[0]);
isb();
/* On V6 debug, we can tell if the #DBGEN signal is enabled by setting
* the DBGDSCR.MDBGEn bit. If the #DBGEN signal is not enabled, writes
* to DBGDSCR.MDBGEn will be ignored, and it will always read as zero.
*
* We test here to see if the DBGDSCR.MDBGEn bit is still 0, even after
* we set it to 1 in enableMonitorMode().
*
* ARMv6 manual, sec D3.3.2, "Monitor debug-mode enable, bit[15]":
*
* "Monitor debug-mode has to be both selected and enabled (bit 14
* clear and bit 15 set) for the core to take a Debug exception."
*
* "If the external interface input DBGEN is low, DSCR[15:14] reads as
* 0b00. The programmed value is masked until DBGEN is taken high, at
* which time value is read and behavior reverts to the programmed
* value."
*/
/* Re-read the value */
dscr.words[0] = readDscrCp();
if (dbg_dscr_get_monitorDebugEnable(dscr) == 0) {
printf("#DBGEN signal held low. Monitor mode unavailable.\n");
return false;
}
return true;
}
static inline dbg_bcr_t
Arch_setupBcr(dbg_bcr_t in_val, bool_t is_match)
{
dbg_bcr_t bcr;
if (is_match) {
bcr = dbg_bcr_set_meaning(in_val, DBGBCR_V6MEANING_INSTRUCTION_VADDR_MATCH);
} else {
bcr = dbg_bcr_set_meaning(in_val, DBGBCR_V6MEANING_INSTRUCTION_VADDR_MISMATCH);
}
bcr = dbg_bcr_set_enableLinking(bcr, 0);
return bcr;
}
static inline dbg_wcr_t
Arch_setupWcr(dbg_wcr_t in_val)
{
return in_val;
}
static inline bool_t
Arch_breakpointIsMismatch(dbg_bcr_t in_val)
{
return dbg_bcr_get_meaning(in_val) == DBGBCR_V6MEANING_INSTRUCTION_VADDR_MISMATCH;
}
#endif /* CONFIG_HARDWARE_DEBUG_API */

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

@ -0,0 +1,177 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_GPL)
*/
#pragma once
#include <config.h>
#ifdef CONFIG_HARDWARE_DEBUG_API
#include <mode/machine.h> /* MRC/MCR */
#define DBGVCR_RESERVED_BITS_MASK \
(BIT(5)|BIT(8)|BIT(9)|BIT(13)|BIT(16)|BIT(24)|BIT(29))
#define DBGWCR_BAS_HIGH_SHIFT (9u)
#define DBGWCR_0 "p14,0,%0,c0,c0,7"
enum v7_breakpoint_type {
DBGBCR_TYPE_UNLINKED_INSTRUCTION_MATCH = 0u,
DBGBCR_TYPE_LINKED_INSTRUCTION_MATCH = 0x1u,
DBGBCR_TYPE_UNLINKED_CONTEXT_MATCH = 0x2u,
DBGBCR_TYPE_LINKED_CONTEXT_MATCH = 0x3u,
DBGBCR_TYPE_UNLINKED_INSTRUCTION_MISMATCH = 0x4u,
DBGBCR_TYPE_LINKED_INSTRUCTION_MISMATCH = 0x5u,
DBGBCR_TYPE_UNLINKED_VMID_MATCH = 0x8u,
DBGBCR_TYPE_LINKED_VMID_MATCH = 0x9u,
DBGBCR_TYPE_UNLINKED_VMID_AND_CONTEXT_MATCH = 0xAu,
DBGBCR_TYPE_LINKED_VMID_AND_CONTEXT_MATCH = 0xBu
};
/** Read DBGDSCR from CP14.
*/
static word_t
readDscrCp(void)
{
word_t v;
MRC(DBGDSCR_ext, v);
return v;
}
/** Write DBGDSCR (Status and control register).
* On ARMv7, the external view of the CP14 DBGDSCR register is preferred since
* the internal view is fully read-only.
*/
static void
writeDscrCp(word_t val)
{
MCR(DBGDSCR_ext, val);
}
/** Determines whether or not 8-byte watchpoints are supported.
*
* Checks to see if the 8-byte byte-address-select high bits ignore writes.
*/
static inline bool_t
watchpoint8bSupported(void)
{
word_t wcrtmp;
/* ARMv7 manual: C11.11.44:
* "A 4-bit Byte address select field is DBGWCR[8:5]. DBGWCR[12:9] is RAZ/WI."
*
* So if 8-byte WPs aren't supported, then the higher 4-bits of the BAS
* field will be RAZ/WI. We can just test the first WP's BAS bits and see
* what happens.
*/
MRC(DBGWCR_0, wcrtmp);
wcrtmp |= BIT(DBGWCR_BAS_HIGH_SHIFT);
MCR(DBGWCR_0, wcrtmp);
/* Re-read to know if the write to the bit was ignored */
MRC(DBGWCR_0, wcrtmp);
return wcrtmp & BIT(DBGWCR_BAS_HIGH_SHIFT);
}
/** Enables the debug architecture mode that allows us to receive debug events
* as exceptions.
*
* CPU can operate in one of 2 debug architecture modes: "halting" and
* "monitor". In halting mode, when a debug event occurs, the CPU will halt
* execution and enter a special state in which it can be examined by an
* external debugger dongle.
*
* In monitor mode, the CPU will deliver debug events to the kernel as
* exceptions. Monitor mode is what's actually useful to us. If it's not
* supported by the CPU, it's impossible for the API to work.
*
* Unfortunately, it's also gated behind a hardware pin signal, #DBGEN. If
* #DBGEN is held low, monitor mode is unavailable.
*/
BOOT_CODE static bool_t
enableMonitorMode(void)
{
dbg_dscr_t dscr;
dscr.words[0] = readDscrCp();
dscr = dbg_dscr_set_haltingDebugEnable(dscr, 0);
dscr = dbg_dscr_set_disableAllUserAccesses(dscr, 1);
dscr = dbg_dscr_set_monitorDebugEnable(dscr, 1);
writeDscrCp(dscr.words[0]);
isb();
/* We can tell if the #DBGEN signal is enabled by setting
* the DBGDSCR.MDBGEn bit. If the #DBGEN signal is not enabled, writes
* to DBGDSCR.MDBGEn will be ignored, and it will always read as zero.
*
* We test here to see if the DBGDSCR.MDBGEn bit is still 0, even after
* we set it to 1 in enableMonitorMode().
*
* ARMv6 manual, sec D3.3.2, "Monitor debug-mode enable, bit[15]":
*
* "Monitor debug-mode has to be both selected and enabled (bit 14
* clear and bit 15 set) for the core to take a Debug exception."
*
* "If the external interface input DBGEN is low, DSCR[15:14] reads as
* 0b00. The programmed value is masked until DBGEN is taken high, at
* which time value is read and behavior reverts to the programmed
* value."
*/
/* Re-read the value */
dscr.words[0] = readDscrCp();
if (dbg_dscr_get_monitorDebugEnable(dscr) == 0) {
printf("#DBGEN signal held low. Monitor mode unavailable.\n");
return false;
}
return true;
}
static inline dbg_bcr_t
Arch_setupBcr(dbg_bcr_t in_val, bool_t is_match)
{
dbg_bcr_t bcr;
bcr = dbg_bcr_set_addressMask(in_val, 0);
bcr = dbg_bcr_set_hypeModeControl(bcr, 0);
bcr = dbg_bcr_set_secureStateControl(bcr, 0);
if (is_match) {
bcr = dbg_bcr_set_breakpointType(bcr, DBGBCR_TYPE_UNLINKED_INSTRUCTION_MATCH);
} else {
bcr = dbg_bcr_set_breakpointType(bcr, DBGBCR_TYPE_UNLINKED_INSTRUCTION_MISMATCH);
}
return bcr;
}
static inline dbg_wcr_t
Arch_setupWcr(dbg_wcr_t in_val)
{
dbg_wcr_t wcr;
wcr = dbg_wcr_set_addressMask(in_val, 0);
wcr = dbg_wcr_set_hypeModeControl(wcr, 0);
wcr = dbg_wcr_set_secureStateControl(wcr, 0);
return wcr;
}
static inline bool_t
Arch_breakpointIsMismatch(dbg_bcr_t in_val)
{
/* Detect if the register is set up for mismatch (single-step). */
if (dbg_bcr_get_breakpointType(in_val) == DBGBCR_TYPE_UNLINKED_INSTRUCTION_MISMATCH) {
return true;
}
return false;
}
#endif /* CONFIG_HARDWARE_DEBUG_API */

1
include/arch/arm/armv/armv8-a/armv/debug.h Symbolic link
View file

@ -0,0 +1 @@
../../armv7-a/armv/debug.h

10
include/arch/x86/arch/32/mode/fastpath/fastpath.h
View file

@ -13,6 +13,7 @@
#include <util.h>
#include <arch/linker.h>
#include <arch/machine/debug.h>
#include <api/types.h>
#include <api/syscall.h>
#include <benchmark_track.h>
@ -112,11 +113,12 @@ fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread)
* is currently disabled */
}
/* save kernel stack pointer for next exception */
SMP_COND_STATEMENT(ksCurThread->tcbArch.tcbContext.kernelSP = ((word_t)kernel_stack_alloc[getCurrentCPUIndex()]) + 0xffc);
#ifdef CONFIG_HARDWARE_DEBUG_API
restore_user_debug_context(ksCurThread);
#endif
setKernelEntryStackPointer(ksCurThread);
/* set the tss.esp0 */
tss_ptr_set_esp0(&ARCH_NODE_STATE(x86KStss).tss, ((uint32_t)&ksCurThread->tcbArch.tcbContext.registers) + (sizeof(word_t)*n_contextRegisters));
if (likely(hasDefaultSelectors(cur_thread))) {
asm volatile(
"movl %%ecx, %%esp\n"

137
include/arch/x86/arch/32/mode/machine/debug.h Normal file
View file

@ -0,0 +1,137 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_GPL)
*/
#pragma once
#include <assert.h>
#ifdef CONFIG_HARDWARE_DEBUG_API
#define X86_DEBUG_BP_N_REGS (4)
static inline word_t
readDr6Reg(void)
{
word_t ret;
asm volatile(
"movl %%dr6, %0 \n\t"
: "=r" (ret));
return ret;
}
static inline void
writeDr6Reg(word_t val)
{
asm volatile(
"movl %0, %%dr6 \n\t"
:
: "r" (val));
}
static inline word_t
readDr7Reg(void)
{
word_t ret;
asm volatile(
"movl %%dr7, %0 \n\t"
: "=r" (ret));
return ret;
}
static inline void
writeDr7Reg(word_t val)
{
asm volatile(
"movl %0, %%dr7 \n\t"
:
: "r" (val));
}
static inline word_t
readDrReg(uint8_t reg)
{
word_t ret;
assert(reg < X86_DEBUG_BP_N_REGS);
switch (reg) {
case 0:
asm volatile("movl %%dr0, %0 \n\t" : "=r" (ret));
break;
case 1:
asm volatile("movl %%dr1, %0 \n\t" : "=r" (ret));
break;
case 2:
asm volatile("movl %%dr2, %0 \n\t" : "=r" (ret));
break;
default:
asm volatile("movl %%dr3, %0 \n\t" : "=r" (ret));
break;
}
return ret;
}
static inline void
writeDrReg(uint8_t reg, word_t val)
{
assert(reg < X86_DEBUG_BP_N_REGS);
switch (reg) {
case 0:
asm volatile("movl %0, %%dr0 \n\t" :: "r" (val));
break;
case 1:
asm volatile("movl %0, %%dr1 \n\t" :: "r" (val));
break;
case 2:
asm volatile("movl %0, %%dr2 \n\t" :: "r" (val));
break;
default:
asm volatile("movl %0, %%dr3 \n\t" :: "r" (val));
break;
}
}
/** Restore debug register context from a block of memory.
*@param source The memory block from which to load the register values.
*/
static inline void
loadBreakpointState(arch_tcb_t *source)
{
/* Order does matter when restoring the registers: we want to restore the
* breakpoint control register (DR7) last since it is what "activates" the
* effects of the configuration described by the other registers.
*/
asm volatile (
"movl %0, %%edx \n\t"
"movl (%%edx), %%ecx \n\t"
"movl %%ecx, %%dr0 \n\t"
"addl $4, %%edx \n\t"
"movl (%%edx), %%ecx \n\t"
"movl %%ecx, %%dr1 \n\t"
"addl $4, %%edx \n\t"
"movl (%%edx), %%ecx \n\t"
"movl %%ecx, %%dr2 \n\t"
"addl $4, %%edx \n\t"
"movl (%%edx), %%ecx \n\t"
"movl %%ecx, %%dr3 \n\t"
"addl $4, %%edx \n\t"
"movl (%%edx), %%ecx \n\t"
"movl %%ecx, %%dr6 \n\t"
"addl $4, %%edx \n\t"
"movl (%%edx), %%ecx \n\t"
"movl %%ecx, %%dr7 \n\t"
:
: "r" (source->tcbContext.breakpointState.dr)
: "edx", "ecx");
}
#endif /* CONFIG_HARDWARE_DEBUG_API */

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

@ -181,6 +181,9 @@ tagged_union fault faultType {
tag vm_fault 2
tag unknown_syscall 3
tag user_exception 4
#ifdef CONFIG_HARDWARE_DEBUG_API
tag debug_exception 5
#endif
}
-- VM attributes

35
include/arch/x86/arch/machine.h
View file

@ -17,9 +17,9 @@
#include <arch/machine/hardware.h>
#include <arch/machine/pat.h>
#include <arch/machine/cpu_registers.h>
#include <model/statedata.h>
#include <arch/model/statedata.h>
#define IA32_APIC_BASE_MSR 0x01B
#define IA32_SYSENTER_CS_MSR 0x174
#define IA32_SYSENTER_ESP_MSR 0x175
@ -101,6 +101,39 @@ static inline void x86_wrmsr(const uint32_t reg, const uint64_t val)
asm volatile("wrmsr" :: "a"(low), "d"(high), "c"(reg));
}
/** Hardware stack switching on exception/IRQ entry.
*
* We need to tell the CPU where the TCB register context structure is so it
* can push to it on entry.
* @param target_thread The thread we're about to switch to.
*/
tcb_t *ksCurThread;
static inline void
setKernelEntryStackPointer(tcb_t *target_thread)
{
word_t register_context_top;
SMP_COND_STATEMENT(word_t kernel_stack_top);
/* Update both the TSS and the IA32_SYSENTER_ESP MSR, because both are used.
*
* The stack pointer is loaded from the TSS on IRQ and exception entry.
* The IA32_SYSENTER_ESP MSR is used on syscall entry when SYSENTER is used.
*
* For an SMP build, we also have to set the location of the kernel stack for the
* current CPU, because we use per-CPU stacks.
*/
/* save kernel stack pointer for next exception */
SMP_COND_STATEMENT(kernel_stack_top = ((word_t)kernel_stack_alloc[getCurrentCPUIndex()]) + 0xffc);
SMP_COND_STATEMENT(ksCurThread->tcbArch.tcbContext.kernelSP = kernel_stack_top);
register_context_top = (word_t)&target_thread->tcbArch.tcbContext.registers[n_contextRegisters];
tss_ptr_set_esp0(&ARCH_NODE_STATE(x86KStss).tss, register_context_top);
#ifdef CONFIG_HARDWARE_DEBUG_API
x86_wrmsr(IA32_SYSENTER_ESP_MSR, register_context_top);
#endif
}
/* Read different parts of CPUID */
static inline uint32_t x86_cpuid_edx(uint32_t eax, uint32_t ecx)
{

183
include/arch/x86/arch/machine/debug.h Normal file
View file

@ -0,0 +1,183 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_GPL)
*/
#pragma once
#include <config.h>
#ifdef CONFIG_HARDWARE_DEBUG_API
#include <types.h>
#include <api/types.h>
#include <arch/machine/registerset.h>
#include <mode/machine/debug.h>
#define X86_EFLAGS_TRAP_FLAG_SHIFT (8u)
/* Bit in DR7 that will enable each BP respectively. */
#define X86_DEBUG_BP0_ENABLE_BIT ((word_t)BIT(1))
#define X86_DEBUG_BP1_ENABLE_BIT ((word_t)BIT(3))
#define X86_DEBUG_BP2_ENABLE_BIT ((word_t)BIT(5))
#define X86_DEBUG_BP3_ENABLE_BIT ((word_t)BIT(7))
/** Per-thread initial state setting.
*
* The most significant thing done here is that we pre-load reserved bits from
* the hardware registers into the TCB context.
*
* @param context TCB breakpoint context for the thread being initialized.
*/
void Arch_initBreakpointContext(user_breakpoint_state_t *context);
/** Discerns and handles a debug exception.
*
* Determines which hardware breakpoint triggered a debug exception, and
* generates a message to userspace for that breakpoint exception, or generates
* a message to userspace for a single-step exception, if it was a single-step
* event that triggered the exception.
*
* ARM's exception-path flow works differently.
*
* @param int_vector Processor-level vector number on which the exception
* occured. May be 1 or 3, depending on whether the exception
* is a breakpoint, single-step, or INT3 exception.
*/
exception_t handleUserLevelDebugException(int int_vector);
/** These next two functions are part of some state flags.
*
* A bitfield of all currently enabled breakpoints for a thread is kept in that
* thread's TCB. These two functions here set and unset the bits in that
* bitfield.
*/
static inline void
setBreakpointUsedFlag(arch_tcb_t *uds, uint16_t bp_num)
{
if (uds != NULL) {
uds->tcbContext.breakpointState.used_breakpoints_bf |= BIT(bp_num);
}
}
static inline void
unsetBreakpointUsedFlag(arch_tcb_t *uds, uint16_t bp_num)
{
if (uds != NULL) {
uds->tcbContext.breakpointState.used_breakpoints_bf &= ~BIT(bp_num);
}
}
/** Program the debug registers with values that will disable all breakpoints.
*
* This is an optimization for threads that don't use any breakpoints: we won't
* try to pop all the context from a block of memory, but just unset all the
* "enable" bits in the registers.
* @param at arch_tcb_t from which the reserved bits will be loaded before
* setting the disable bits.
*/
static void
loadAllDisabledBreakpointState(arch_tcb_t *at)
{
word_t disable_value;
disable_value = at->tcbContext.breakpointState.dr[5];
disable_value &= ~(X86_DEBUG_BP0_ENABLE_BIT | X86_DEBUG_BP1_ENABLE_BIT
| X86_DEBUG_BP2_ENABLE_BIT | X86_DEBUG_BP3_ENABLE_BIT);
writeDr7Reg(disable_value);
}
static inline void
restore_user_debug_context(tcb_t *target_thread)
{
arch_tcb_t *uds = &target_thread->tcbArch;
if (uds->tcbContext.breakpointState.used_breakpoints_bf != 0) {
loadBreakpointState(uds);
} else {
loadAllDisabledBreakpointState(uds);
}
/* If single-stepping was enabled, we need to re-set the TF flag as well. */
if (uds->tcbContext.breakpointState.single_step_enabled == true) {
uds->tcbContext.registers[EFLAGS] |= BIT(X86_EFLAGS_TRAP_FLAG_SHIFT);
}
}
static inline syscall_error_t
Arch_decodeConfigureSingleStepping(arch_tcb_t *uc,
uint16_t bp_num,
word_t n_instr,
bool_t is_reply)
{
syscall_error_t ret;
ret.type = seL4_NoError;
return ret;
}
bool_t byte8BreakpointsSupported(void);
static inline syscall_error_t
Arch_decodeSetBreakpoint(arch_tcb_t *uds,
uint16_t bp_num, word_t vaddr, word_t types,
word_t size, word_t rw)
{
syscall_error_t ret = {
.type = seL4_NoError
};
if (bp_num >= X86_DEBUG_BP_N_REGS) {
userError("Debug: invalid bp_num %u.", bp_num);
ret.rangeErrorMin = 0;
ret.rangeErrorMax = 3;
ret.type = seL4_RangeError;
return ret;
}
if (size == 8 && !byte8BreakpointsSupported()) {
userError("Debug: 8-byte breakpoints/watchpoints unsupported on this CPU.");
ret.invalidArgumentNumber = 3;
ret.type = seL4_InvalidArgument;
return ret;
}
return ret;
}
static inline syscall_error_t
Arch_decodeGetBreakpoint(arch_tcb_t *uds, uint16_t bp_num)
{
syscall_error_t ret = {
.type = seL4_NoError
};
if (bp_num >= X86_DEBUG_BP_N_REGS) {
userError("Debug: invalid bp_num %u.", bp_num);
ret.rangeErrorMin = 0;
ret.rangeErrorMax = 3;
ret.type = seL4_RangeError;
}
return ret;
}
static inline syscall_error_t
Arch_decodeUnsetBreakpoint(arch_tcb_t *uds, uint16_t bp_num)
{
syscall_error_t ret = {
.type = seL4_NoError
};
if (bp_num >= X86_DEBUG_BP_N_REGS) {
userError("Debug: invalid bp_num %u.", bp_num);
ret.rangeErrorMin = 0;
ret.rangeErrorMax = 3;
ret.type = seL4_RangeError;
}
return ret;
}
#endif /* CONFIG_HARDWARE_DEBUG_API */

41
include/arch/x86/arch/machine/registerset.h
View file

@ -21,6 +21,43 @@
/* Minimum hardware-enforced alignment needed for FPU state. */
#define MIN_FPU_ALIGNMENT 64
#ifdef CONFIG_HARDWARE_DEBUG_API
/* X86 Debug register context */
struct user_debug_state {
/* DR0-3 = Breakpoint linear address.
* DR4-5 = reserved or aliased, depending on value of CR4.DE.
* DR6 = Debug status register.
* DR7 = Debug control register.
*/
word_t dr[6];
/* For each breakpoint currently being used by a thread, a bit in this
* bitfield is set, and for each breakpoint that is cleared, a bit is
* cleared. This enables an optimization: when a thread is being context-
* switched to, we can check to see if it's using breakpoints, and
* if so, we pop the whole register context.
*
* If it's not using breakpoints, we just pop all 0s into the ENABLED
* bits in DR7.
*/
uint32_t used_breakpoints_bf;
/* The API supports stepping N instructions forward, where N can 1..N.
* That feature is provided using this counter. Everytime a debug exception
* occurs, the kernel will decrement, then check the counter, and only when
* the counter is 0 will we deliver the fault to the userspace thread.
*/
word_t n_instructions;
/* This is part of the state machine that allows a thread to make
* syscalls while being single-stepped. Basically helps the kernel to
* disable single-stepping while executing the syscall, and then re-enable
* it just before returning from the syscall into userspace.
*/
bool_t single_step_enabled;
};
typedef struct user_debug_state user_breakpoint_state_t;
#endif /* CONFIG_HARDWARE_DEBUG_API */
/* X86 FPU context. */
struct user_fpu_state {
uint8_t state[CONFIG_XSAVE_SIZE];
@ -30,8 +67,10 @@ typedef struct user_fpu_state user_fpu_state_t;
/* X86 user-code context */
struct user_context {
user_fpu_state_t fpuState;
#ifdef CONFIG_HARDWARE_DEBUG_API
user_breakpoint_state_t breakpointState;
#endif
word_t registers[n_contextRegisters];
#if CONFIG_MAX_NUM_NODES > 1
/* stored pointer to kernel stack used when kernel run in current TCB context. */
word_t kernelSP;

88
include/machine/debug.h
View file

@ -1,16 +1,94 @@
/*
* Copyright 2014, General Dynamics C4 Systems
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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)
* @TAG(D61_GPL)
*/
#pragma once
#include <config.h>
#ifndef __MACHINE_DEBUG_H
#define __MACHINE_DEBUG_H
#ifdef CONFIG_HARDWARE_DEBUG_API
#include <arch/machine/debug.h>
#endif
#define DEBUG_REPLY_N_EXPECTED_REGISTERS (1)
/* Arch specific setup functions */
BOOT_CODE bool_t Arch_initHardwareBreakpoints(void);
void Arch_breakpointThreadDelete(tcb_t *thread);
/** Sets up (and overwrites) the current configuration of a hardware breakpoint.
* @param bp_num Hardware breakpoint ID. Usually an integer from 0..N.
* @param vaddr Address that the breakpoint should be triggered by.
* @param type Type of operation that should trigger the breakpoint.
* @param size Operand size that should trigger the breakpoint.
* @param rwx Access type (read/write) that should trigger the breakpoint.
* @param uds If NULL, this function call will write directly to the hardware
* registers.
* If non-NULL, 'uds' is assumed to be a pointer to a debug register
* context-saving memory block, and this function will write to that
* context-saving memory block instead.
*/
void setBreakpoint(arch_tcb_t *uds,
uint16_t bp_num,
word_t vaddr, word_t type, word_t size, word_t rw);
/** Reads and returns the current configuration of a hardware breakpoint.
* @param bp_num Hardware breakpoint ID. Usually an integer from 0..N.
*
* @return Filled out getBreakpoint_t with the following fields:
* @param vaddr[out] Address that the breakpoint is set to trigger on.
* @param type[out] Type of operation that will trigger the breakpoint.
* @param size[out] operand size that will trigger the breakpoint.
* @param rw[out] Access type (read/write) that will trigger thr breakpoint.
* @param uds If NULL, this function call will read directly from the hardware
* registers.
* If non-NULL, 'uds' is assumed to be a pointer to a debug register
* context-saving memory block, and this function will read from that
* context-saving memory block instead.
* @param is_enabled Bool stating whether or not the breakpoint is enabled.
*/
typedef struct getBreakpointRet {
word_t vaddr, type, size, rw;
bool_t is_enabled;
} getBreakpoint_t;
getBreakpoint_t getBreakpoint(arch_tcb_t *uds, uint16_t bp_num);
/** Clears a breakpoint's configuration and disables it.
* @param bp_num Hardware breakpoint ID. Usually an integer from 0..N.
* @param uds If NULL, this function call will write directly to the hardware
* registers.
* If non-NULL, 'uds' is assumed to be a pointer to a debug register
* context-saving memory block, and this function will write to that
* context-saving memory block instead.
*/
void unsetBreakpoint(arch_tcb_t *uds, uint16_t bp_num);
bool_t configureSingleStepping(arch_tcb_t *uc,
uint16_t bp_num,
word_t n_instr,
bool_t is_reply);
static inline bool_t
singleStepFaultCounterReady(arch_tcb_t *uc)
{
/* For a single-step exception, the user may have specified a certain
* number of instructions to skip over before the next stop-point, so
* we need to decrement the counter.
*
* We will check the counter's value when deciding whether or not to
* actually send a fault message to userspace.
*/
if (uc->tcbContext.breakpointState.n_instructions > 0) {
uc->tcbContext.breakpointState.n_instructions--;
}
return uc->tcbContext.breakpointState.n_instructions == 0;
}
#endif /* CONFIG_HARDWARE_DEBUG_API */

15
include/object/structures_32.bf
View file

@ -261,6 +261,21 @@ block user_exception {
field faultType 3
}
#ifdef CONFIG_HARDWARE_DEBUG_API
block debug_exception {
field breakpointAddress 32
padding 21
-- X86 has 4 breakpoints (DR0-3).
-- ARM has between 2 and 16 breakpoints
-- ( ARM Ref manual, C3.3).
-- So we just use 4 bits to cater for both.
field breakpointNumber 4
field exceptionReason 4
field faultType 3
}
#endif
-- Thread state: size = 12 bytes
block thread_state(blockingIPCBadge, blockingIPCCanGrant, blockingIPCIsCall,
tcbQueued, blockingObject,

1
include/plat/allwinnerA20/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/allwinnerA20/sel4/plat/api/constants.h

9
include/plat/allwinnerA20/plat/machine/devices.h
View file

@ -19,9 +19,10 @@
/* These devices are used by the seL4 kernel. */
#define UART0_PPTR 0xfff01000
#define TIMER0_PPTR 0xfff02000
#define TIMER0_PPTR 0xfff02000
#define GIC_DISTRIBUTOR_PPTR 0xfff03000
#define GIC_CONTROLLER_PPTR 0xfff04000
#define ARM_DEBUG_MMAPPING_PPTR 0xfff05000
#define GIC_PL390_CONTROLLER_PPTR GIC_CONTROLLER_PPTR
#define GIC_PL390_DISTRIBUTOR_PPTR GIC_DISTRIBUTOR_PPTR
@ -31,13 +32,13 @@
#define UART0_PADDR 0x01C28000
#define UART0_PADDR 0x01C28000
/* CCU, Interrupt, Timer, OWA */
/* Timer = PPTR + 0xC00 */
#define TIMER0_PADDR 0x01C20000
#define TIMER0_PADDR 0x01C20000
#define GIC_PADDR 0x01C80000
#define GIC_PADDR 0x01C80000
/* TODO: Add other devices PADDRs */

1
include/plat/am335x/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/am335x/sel4/plat/api/constants.h

11
include/plat/am335x/plat/machine/devices.h
View file

@ -12,11 +12,12 @@
#define __PLAT_MACHINE_DEVICES_H
/* These devices are used by the kernel. */
#define INTC_PPTR 0xfff01000
#define UART0_PPTR 0xfff02000
#define DMTIMER0_PPTR 0xfff03000
#define WDT1_PPTR 0xfff04000
#define CMPER_PPTR 0xfff05000
#define INTC_PPTR 0xfff01000
#define UART0_PPTR 0xfff02000
#define DMTIMER0_PPTR 0xfff03000
#define WDT1_PPTR 0xfff04000
#define CMPER_PPTR 0xfff05000
#define ARM_DEBUG_MMAPPING_PPTR 0xfff06000
/* Other devices on the SoC. */

1
include/plat/apq8064/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/apq8064/sel4/plat/api/constants.h

1
include/plat/apq8064/plat/machine/devices.h
View file

@ -16,6 +16,7 @@
#define TIMER_PPTR 0xfff02000
#define GIC_DISTRIBUTOR_PPTR 0xfff04000
#define GIC_CONTROLLER_PPTR 0xfff05000
#define ARM_DEBUG_MMAPPING_PPTR 0xfff06000
#define GIC_PL390_CONTROLLER_PPTR GIC_CONTROLLER_PPTR
#define GIC_PL390_DISTRIBUTOR_PPTR GIC_DISTRIBUTOR_PPTR

1
include/plat/bcm2837/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/bcm2837/sel4/plat/api/constants.h

1
include/plat/exynos4/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/exynos4/sel4/plat/api/constants.h

1
include/plat/exynos4/plat/machine/devices.h
View file

@ -17,6 +17,7 @@
#define L2CC_PPTR 0xfff03000
#define GIC_CONTROLLER_PPTR 0xfff04000
#define GIC_DISTRIBUTOR_PPTR 0xfff05000
#define ARM_DEBUG_MMAPPING_PPTR 0xfff06000
#define L2CC_L2C310_PPTR L2CC_PPTR
#define GIC_PL390_CONTROLLER_PPTR GIC_CONTROLLER_PPTR

1
include/plat/exynos5/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/exynos5/sel4/plat/api/constants.h

3
include/plat/exynos5/plat/machine/devices.h
View file

@ -17,9 +17,10 @@
#define L2CC_PPTR 0xfff03000
#define GIC_DISTRIBUTOR_PPTR 0xfff04000
#define GIC_CONTROLLER_PPTR 0xfff05000
#define GIC_VCPUCTRL_PPTR 0xfff06000
#define ARM_DEBUG_MMAPPING_PPTR 0xfff07000
/* HYP mode kernel devices */
#define GIC_VCPUCTRL_PPTR 0xfff06000
#define GIC_PL400_VCPUCTRL_PPTR GIC_VCPUCTRL_PPTR
#define L2CC_L2C310_PPTR L2CC_PPTR

1
include/plat/hikey/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/hikey/sel4/plat/api/constants.h

1
include/plat/hikey/plat/machine/devices.h
View file

@ -21,6 +21,7 @@
#define UART0_PPTR 0xfff01000
#define GIC_DISTRIBUTOR_PPTR 0xfff03000
#define GIC_CONTROLLER_PPTR 0xfff04000
#define ARM_DEBUG_MMAPPING_PPTR 0xfff05000
#define GIC_PL390_CONTROLLER_PPTR GIC_CONTROLLER_PPTR
#define GIC_PL390_DISTRIBUTOR_PPTR GIC_DISTRIBUTOR_PPTR

1
include/plat/imx31/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/imx31/sel4/plat/api/constants.h

20
include/plat/imx31/plat/machine/devices.h
View file

@ -15,14 +15,19 @@
/* kernel devices */
#define EPIT_PADDR 0x53f94000
#define EPIT_PPTR 0xfff00000
#define EPIT_PADDR 0x53f94000
#define EPIT_PPTR 0xfff00000
#define AVIC_PADDR 0x68000000
#define AVIC_PPTR 0xfff01000
#define AVIC_PADDR 0x68000000
#define AVIC_PPTR 0xfff01000
#define L2CC_PADDR 0x30000000
#define L2CC_PPTR 0xfff02000
#define L2CC_PADDR 0x30000000
#define L2CC_PPTR 0xfff02000
#define UART_PADDR 0x43f90000
#define UART_PPTR 0xfff03000
#define ARM_DEBUG_MMAPPING_PPTR 0xfff04000
struct imx31_l2cc_id {
uint32_t id; /* 000 */
@ -66,7 +71,4 @@ struct imx31_l2cc_lockdown {
#define imx32_l2cc_lockdown_regs \
((volatile struct imx31_l2cc_lockdown *)(L2CC_PPTR + 0x900))
#define UART_PADDR 0x43f90000
#define UART_PPTR 0xfff03000
#endif

1
include/plat/imx6/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/imx6/sel4/plat/api/constants.h

1
include/plat/imx6/plat/machine/devices.h
View file

@ -25,6 +25,7 @@
#define L2CC_PL310_PPTR 0xfff03000
#define ARM_MP_PPTR1 0xfff04000
#define ARM_MP_PPTR2 0xfff05000
#define ARM_DEBUG_MMAPPING_PPTR 0xfff06000
#define L2CC_L2C310_PPTR (L2CC_PL310_PPTR )
#define ARM_MP_PRIV_TIMER_PPTR (ARM_MP_PPTR1 + 0x600 )

1
include/plat/imx7/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/imx7/sel4/plat/api/constants.h

2
include/plat/imx7/plat/machine/devices.h
View file

@ -19,6 +19,8 @@
#define ARM_MP_PPTR1 0xfff03000
#define ARM_MP_PPTR2 0xfff04000
#define ARM_MP_PPTR3 0xfff05000
#define ARM_DEBUG_MMAPPING_PPTR 0xfff06000
#define ARM_MP_PRIV_TIMER_PPTR (ARM_MP_PPTR1 + 0x600 )
#define ARM_MP_GLOBAL_TIMER_PPTR (ARM_MP_PPTR1 + 0x200 )

1
include/plat/omap3/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/omap3/sel4/plat/api/constants.h

1
include/plat/omap3/plat/machine/devices.h
View file

@ -22,6 +22,7 @@
#define UART3_PPTR 0xfff01000
#define INTC_PPTR 0xfff02000
#define GPTIMER9_PPTR 0xfff03000
#define ARM_DEBUG_MMAPPING_PPTR 0xfff04000
/* Boot space */
/* 0x00000000 - 0x40000000 */

1
include/plat/pc99/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/pc99/sel4/plat/api/constants.h

32
include/plat/pc99/plat/machine.h
View file

@ -19,21 +19,23 @@
#define IRQ_INT_OFFSET 0x20
typedef enum _interrupt_t {
int_invalid = -1,
int_unimpl_dev = 7,
int_page_fault = 14,
int_irq_min = IRQ_INT_OFFSET, /* First IRQ. */
int_irq_isa_min = IRQ_INT_OFFSET, /* Beginning of PIC IRQs */
int_irq_isa_max = IRQ_INT_OFFSET + PIC_IRQ_LINES - 1, /* End of PIC IRQs */
int_irq_user_min = IRQ_INT_OFFSET + PIC_IRQ_LINES, /* First user available vector */
int_irq_user_max = 157,
int_iommu = 158,
int_timer = 159,
int_irq_max = 159, /* int_timer is the max irq */
int_trap_min = 160,
int_trap_max = 254,
int_spurious = 255,
int_max = 255
int_invalid = -1,
int_debug = 1,
int_software_break_request = 3,
int_unimpl_dev = 7,
int_page_fault = 14,
int_irq_min = IRQ_INT_OFFSET, /* First IRQ. */
int_irq_isa_min = IRQ_INT_OFFSET, /* Beginning of PIC IRQs */
int_irq_isa_max = IRQ_INT_OFFSET + PIC_IRQ_LINES - 1, /* End of PIC IRQs */
int_irq_user_min = IRQ_INT_OFFSET + PIC_IRQ_LINES, /* First user available vector */
int_irq_user_max = 157,
int_iommu = 158,
int_timer = 159,
int_irq_max = 159, /* int_timer is the max irq */
int_trap_min = 160,
int_trap_max = 254,
int_spurious = 255,
int_max = 255
} interrupt_t;
typedef enum _irq_t {

1
include/plat/tk1/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/tk1/sel4/plat/api/constants.h

2
include/plat/tk1/plat/machine/devices.h
View file

@ -23,6 +23,8 @@
#define GIC_VCPUCTRL_PPTR 0xfff06000
/* SMMU registers */
#define SMMU_PPTR 0Xfff07000
#define ARM_DEBUG_MMAPPING_PPTR 0xfff08000
#define GIC_PL390_CONTROLLER_PPTR GIC_CONTROLLER_PPTR
#define GIC_PL390_DISTRIBUTOR_PPTR GIC_DISTRIBUTOR_PPTR

1
include/plat/zynq7000/plat/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../libsel4/sel4_plat_include/zynq7000/sel4/plat/api/constants.h

1
include/plat/zynq7000/plat/machine/devices.h
View file

@ -18,6 +18,7 @@
#define L2CC_PL310_PPTR 0xfff02000
#define ARM_MP_PPTR1 0xfff03000
#define ARM_MP_PPTR2 0xfff04000
#define ARM_DEBUG_MMAPPING_PPTR 0xfff05000
#define L2CC_L2C310_PPTR (L2CC_PL310_PPTR )
#define ARM_MP_PRIV_TIMER_PPTR (ARM_MP_PPTR1 + 0x600 )

1
libsel4/Makefile
View file

@ -41,6 +41,7 @@ HDRFILES := \
$(wildcard $(SOURCE_DIR)/include/*) \
$(wildcard $(SOURCE_DIR)/arch_include/$(ARCH)/*) \
$(wildcard $(SOURCE_DIR)/sel4_arch_include/$(SEL4_ARCH)/*) \
$(wildcard $(SOURCE_DIR)/sel4_plat_include/$(PLAT)/*) \
$(BUILD_DIR)/include/sel4 \
$(BUILD_DIR)/include/interfaces #TODO proper prefix instruction

1
libsel4/arch_include/arm/sel4/arch/constants.h
View file

@ -12,6 +12,7 @@
#define __LIBSEL4_ARCH_CONSTANTS_H
#include <sel4/sel4_arch/constants.h>
#include <sel4/plat/api/constants.h>
#include <sel4/sel4_arch/objecttype.h>
#include <sel4/arch/objecttype.h>

1
libsel4/arch_include/x86/sel4/arch/constants.h
View file

@ -14,6 +14,7 @@
#include <autoconf.h>
#include <sel4/sel4_arch/constants.h>
#include <sel4/plat/api/constants.h>
#ifndef __ASM__
#include <sel4/sel4_arch/objecttype.h>

23
libsel4/include/interfaces/sel4.xml
View file

@ -75,6 +75,29 @@
</method>
<method id="TCBUnbindNotification" name="UnbindNotification">
</method>
<method id="TCBSetBreakpoint" name="SetBreakpoint" config="CONFIG_HARDWARE_DEBUG_API">
<param dir="in" name="bp_num" type="seL4_Uint16"/>
<param dir="in" name="vaddr" type="seL4_Word"/>
<param dir="in" name="type" type="seL4_Word"/>
<param dir="in" name="size" type="seL4_Word"/>
<param dir="in" name="rw" type="seL4_Word"/>
</method>
<method id="TCBGetBreakpoint" name="GetBreakpoint" config="CONFIG_HARDWARE_DEBUG_API">
<param dir="in" name="bp_num" type="seL4_Uint16"/>
<param dir="out" name="vaddr" type="seL4_Word"/>
<param dir="out" name="type" type="seL4_Word"/>
<param dir="out" name="size" type="seL4_Word"/>
<param dir="out" name="rw" type="seL4_Word"/>
<param dir="out" name="is_enabled" type="seL4_Bool"/>
</method>
<method id="TCBUnsetBreakpoint" name="UnsetBreakpoint" config="CONFIG_HARDWARE_DEBUG_API">
<param dir="in" name="bp_num" type="seL4_Uint16"/>
</method>
<method id="TCBConfigureSingleStepping" name="ConfigureSingleStepping" config="CONFIG_HARDWARE_DEBUG_API">
<param dir="in" name="bp_num" type="seL4_Uint16"/>
<param dir="in" name="num_instructions" type="seL4_Word"/>
<param dir="out" name="bp_was_consumed" type="seL4_Bool"/>
</method>
</interface>
<interface name="seL4_CNode">
<method id="CNodeRevoke" name="Revoke">

5
libsel4/include/sel4/benchmark_track_types.h
View file

@ -15,7 +15,7 @@
#include <autoconf.h>
#endif
#if (defined CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES || defined DEBUG)
#if (defined CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES || defined CONFIG_DEBUG_BUILD)
/* the following code can be used at any point in the kernel
* to determine detail about the kernel entry point */
@ -23,6 +23,7 @@ typedef enum {
Entry_Interrupt,
Entry_UnknownSyscall,
Entry_UserLevelFault,
Entry_DebugFault,
Entry_VMFault,
Entry_Syscall,
Entry_UnimplementedDevice,
@ -60,6 +61,6 @@ typedef struct benchmark_syscall_log_entry {
kernel_entry_t entry;
} benchmark_track_kernel_entry_t;
#endif /* CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES */
#endif /* CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES || CONFIG_DEBUG_BUILD */
#endif /* BENCHMARK_TRACK_TYPES_H */

34
libsel4/include/sel4/constants.h
View file

@ -11,8 +11,42 @@
#ifndef __API_CONSTANTS_H
#define __API_CONSTANTS_H
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#define LIBSEL4_BIT(n) (1ul<<(n))
#ifdef CONFIG_HARDWARE_DEBUG_API
/* API arg values for breakpoint API, "type" arguments. */
typedef enum {
seL4_DataBreakpoint = 0,
seL4_InstructionBreakpoint,
seL4_SingleStep,
seL4_SoftwareBreakRequest,
SEL4_FORCE_LONG_ENUM(seL4_BreakpointType)
} seL4_BreakpointType;
/* API arg values for breakpoint API, "access" arguments. */
typedef enum {
seL4_BreakOnRead = 0,
seL4_BreakOnWrite,
seL4_BreakOnReadWrite,
seL4_MaxBreakpointAccess,
SEL4_FORCE_LONG_ENUM(seL4_BreakpointAccess)
} seL4_BreakpointAccess;
/* Format of a debug-exception message. */
enum {
seL4_DebugException_FaultIP,
seL4_DebugException_ExceptionReason,
seL4_DebugException_TriggerAddress,
seL4_DebugException_BreakpointNumber,
seL4_DebugException_Length,
SEL4_FORCE_LONG_ENUM(seL4_DebugException_Msg)
} seL4_DebugException_Msg;
#endif
enum priorityConstants {
seL4_InvalidPrio = -1,
seL4_MinPrio = 0,

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

@ -11,6 +11,9 @@
#ifndef __LIBSEL4_TYPES_H
#define __LIBSEL4_TYPES_H
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#include <sel4/simple_types.h>
#include <sel4/macros.h>
#include <sel4/arch/types.h>
@ -31,6 +34,9 @@ typedef enum {
seL4_VMFault,
seL4_UnknownSyscall,
seL4_UserException,
#ifdef CONFIG_HARDWARE_DEBUG_API
seL4_DebugException,
#endif
SEL4_FORCE_LONG_ENUM(seL4_FaultType),
} seL4_FaultType;

6
libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h
View file

@ -54,4 +54,10 @@ enum {
#define seL4_LogBufferSize (LIBSEL4_BIT(20))
#endif /* CONFIG_ENABLE_BENCHMARKS */
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint (0)
#define seL4_FirstDualFunctionMonitor (-1)
#define seL4_NumDualFunctionMonitors (0)
#endif
#endif

2
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
View file

@ -11,7 +11,9 @@
#ifndef __LIBSEL4_SEL4_ARCH_CONSTANTS_H
#define __LIBSEL4_SEL4_ARCH_CONSTANTS_H
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#define TLS_GDT_ENTRY 6
#define TLS_GDT_SELECTOR ((TLS_GDT_ENTRY << 3) | 3)

26
libsel4/sel4_plat_include/allwinnerA20/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Cortex A7 manual, table 10-2 */
#define seL4_NumHWBreakpoints (10)
#define seL4_NumExclusiveBreakpoints (6)
#define seL4_FirstWatchpoint (6)
#define seL4_NumExclusiveWatchpoints (4)
#define seL4_NumDualFunctionMonitors (0)
#endif

25
libsel4/sel4_plat_include/am335x/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,25 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Cortex a8 manual, table 12-11 */
#define seL4_NumHWBreakpoints (8)
#define seL4_NumExclusiveBreakpoints (6)
#define seL4_FirstWatchpoint (6)
#define seL4_NumExclusiveWatchpoints (2)
#define seL4_NumDualFunctionMonitors (0)
#endif

26
libsel4/sel4_plat_include/apq8064/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Cortex a15 manual, section 10.2.2 */
#define seL4_NumHWBreakpoints (10)
#define seL4_NumExclusiveBreakpoints (6)
#define seL4_FirstWatchpoint (6)
#define seL4_NumExclusiveWatchpoints (4)
#define seL4_NumDualFunctionMonitors (0)
#endif

26
libsel4/sel4_plat_include/bcm2837/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Cortex A57 manual, section 10.6.1 */
#define seL4_NumHWBreakpoints (10)
#define seL4_NumExclusiveBreakpoints (6)
#define seL4_FirstWatchpoint (6)
#define seL4_NumExclusiveWatchpoints (4)
#define seL4_NumDualFunctionMonitors (0)
#endif

26
libsel4/sel4_plat_include/exynos4/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Cortex a9 manual, section 10.1.2 */
#define seL4_NumHWBreakpoints (10)
#define seL4_NumExclusiveBreakpoints (6)
#define seL4_FirstWatchpoint (6)
#define seL4_NumExclusiveWatchpoints (4)
#define seL4_NumDualFunctionMonitors (0)
#endif

26
libsel4/sel4_plat_include/exynos5/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Cortex a15 manual, section 10.2.2 */
#define seL4_NumHWBreakpoints (10)
#define seL4_NumExclusiveBreakpoints (6)
#define seL4_FirstWatchpoint (6)
#define seL4_NumExclusiveWatchpoints (4)
#define seL4_NumDualFunctionMonitors (0)
#endif

13
libsel4/sel4_plat_include/exynos_common/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,13 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once

26
libsel4/sel4_plat_include/hikey/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Cortex A57 manual, section 10.6.1 */
#define seL4_NumHWBreakpoints (10)
#define seL4_NumExclusiveBreakpoints (6)
#define seL4_FirstWatchpoint (6)
#define seL4_NumExclusiveWatchpoints (4)
#define seL4_NumDualFunctionMonitors (0)
#endif

26
libsel4/sel4_plat_include/imx31/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* ARM1136-JF-S manual, table 13-3 */
#define seL4_NumHWBreakpoints (8)
#define seL4_NumExclusiveBreakpoints (6)
#define seL4_FirstWatchpoint (6)
#define seL4_NumExclusiveWatchpoints (2)
#define seL4_NumDualFunctionMonitors (0)
#endif

26
libsel4/sel4_plat_include/imx6/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Cortex a9 manual, section 10.1.2 */
#define seL4_NumHWBreakpoints (10)
#define seL4_NumExclusiveBreakpoints (6)
#define seL4_FirstWatchpoint (6)
#define seL4_NumExclusiveWatchpoints (4)
#define seL4_NumDualFunctionMonitors (0)
#endif

26
libsel4/sel4_plat_include/imx7/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Cortex A7 manual, table 10-2 */
#define seL4_NumHWBreakpoints (10)
#define seL4_NumExclusiveBreakpoints (6)
#define seL4_FirstWatchpoint (6)
#define seL4_NumExclusiveWatchpoints (4)
#define seL4_NumDualFunctionMonitors (0)
#endif

26
libsel4/sel4_plat_include/omap3/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Cortex a8 manual, table 12-11 */
#define seL4_NumHWBreakpoints (8)
#define seL4_NumExclusiveBreakpoints (6)
#define seL4_FirstWatchpoint (6)
#define seL4_NumExclusiveWatchpoints (2)
#define seL4_NumDualFunctionMonitors (0)
#endif

30
libsel4/sel4_plat_include/pc99/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,30 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
/* Defined for each architecture: the number of hardware breakpoints
* available.
*/
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_NumHWBreakpoints (4)
#define seL4_FirstBreakpoint (-1)
#define seL4_NumExclusiveBreakpoints (0)
#define seL4_FirstWatchpoint (-1)
#define seL4_NumExclusiveWatchpoints (0)
#define seL4_FirstDualFunctionMonitor (0)
#define seL4_NumDualFunctionMonitors (4)
#endif

26
libsel4/sel4_plat_include/tk1/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Cortex a15 manual, section 10.2.2 */
#define seL4_NumHWBreakpoints (10)
#define seL4_NumExclusiveBreakpoints (6)
#define seL4_FirstWatchpoint (6)
#define seL4_NumExclusiveWatchpoints (4)
#define seL4_NumDualFunctionMonitors (0)
#endif

26
libsel4/sel4_plat_include/zynq7000/sel4/plat/api/constants.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Cortex a9 manual, section 10.1.2 */
#define seL4_NumHWBreakpoints (10)
#define seL4_NumExclusiveBreakpoints (6)
#define seL4_FirstWatchpoint (6)
#define seL4_NumExclusiveWatchpoints (4)
#define seL4_NumDualFunctionMonitors (0)
#endif

53
manual/parts/api.tex
View file

@ -27,7 +27,7 @@
\begin{minipage}{0.95\textwidth}
\begin{tabularx}{\textwidth}{llX}
\toprule
\textbf{Type} & \textbf{Name} & \textbf{Description} \\
\textbf{Type} & \textbf{Name} & \textbf{Description} \\
\midrule
#5
\bottomrule
@ -67,6 +67,32 @@
\newcommand{\vmcaprightsdesc}{Rights for the mapping. Possible values for this type are given in \autoref{sec:cap_rights}.}
\newcommand{\vmattribsdescarm}{VM Attributes for the mapping. Possible values for this type are given in \autoref{ch:vspace}.}
\newcommand{\debugargbpnumshortdesc}{
The API-ID of a target breakpoint. This ID will be a positive integer, with
values ranging from \texttt{0} to \texttt{seL4\_NumHWBreakpoints - 1}.
}
\newcommand{\debugargvaddrshortdesc}{A virtual address which forms part of the
match conditions for the triggering of the breakpoint.
}
\newcommand{\debugargtypeshortdesc}{One of: \texttt{seL4\_InstructionBreakpoint}, which specifies
that the breakpoint should occur on instruction execution at the specified
\texttt{vaddr} or \texttt{seL4\_DataBreakpoint}, which states that the breakpoint
should occur on data access at the specified \texttt{vaddr}.
}
\newcommand{\debugargsizeshortdesc}{A positive integer indicating the
trigger-span of the watchpoint. Must be zero when 'type' is \texttt{seL4\_InstructionBreakpoint}.
}
\newcommand{\debugargrwshortdesc}{One of \texttt{seL4\_BreakOnRead}, meaning the breakpoint will only be
triggered on read-access; \texttt{seL4\_BreakOnWrite} meaning the
breakpoint will only be triggered on write-access, and
\texttt{seL4\_BreakOnReadWrite} meaning the breakpoint will be triggered on
any access.
}
\ifxeightsix
\newcommand{\vmattribsdescintel}{VM Attributes for the
mapping. Possible values for this type are given in \autoref{ch:vspace}. }
@ -101,6 +127,27 @@
\newcommand{\noret}{This method does not return anything.}
\newcommand{\errorenumdesc}{A return value of \texttt{0} indicates success. A non-zero value indicates that an error occurred. See \autoref{sec:errors} for a description of the message register and tag contents upon error.}
\newcommand{\pagegetaddresstdesc}{struct that contains \texttt{seL4\_Word paddr}, which holds the physical address of the page, and \texttt{int error}. See \autoref{sec:errors} for a description of the message register and tag contents upon error.}
\newcommand{\tcbgetbreakpointtdesc}{Struct that contains
'\texttt{seL4\_Error error}', an seL4 API error value,
'\texttt{seL4\_Word vaddr}', the virtual address at which the breakpoint will currently
be triggered;
'\texttt{seL4\_Word type}', the type of operation which will currently trigger the
breakpoint, whether instruction execution, or data access;
'\texttt{seL4\_Word size}', integer value for the span-size of the breakpoint.
Usually a multiple of two (1, 2, 4, etc.);
'\texttt{seL4\_Word rw}', the access direction that will currently trigger the breakpoint,
whether read, write, or both and
'\texttt{seL4\_Bool is\_enabled}', which indicates whether or not the breakpoint
will currently be triggered if the match conditions are met.
}
\newcommand{\tcbconfiguresinglesteppingtdesc}{Struct that contains
'\texttt{seL4\_Error error}', an seL4 API error value,
'\texttt{seL4\_Bool bp\_was\_consumed}', a boolean which indicates whether or not the \texttt{bp\_num}
breakpoint ID that was passed to the function, was consumed in the setup of the single-stepping
functionality: if this is \texttt{true}, the caller should not attempt to re-use \texttt{bp\_num}
until it has disabled the single-stepping functionality via a subsequent call to
seL4\_TCB\_ConfigureSingleStepping with an \texttt{nun\_instructions} argument of 0.
}
\newcommand{\domcapdesc}{Capability allowing domain configuration.}
\newcommand{\domargdesc}{The thread's new domain.}
@ -275,6 +322,10 @@ complete the \apifunc{seL4\_Untyped\_Retype}{untyped_retype} request.
\inputapidoc{tcb_setspace}
\inputapidoc{tcb_suspend}
\inputapidoc{tcb_writeregisters}
\inputapidoc{tcb_setbreakpoint}
\inputapidoc{tcb_getbreakpoint}
\inputapidoc{tcb_unsetbreakpoint}
\inputapidoc{tcb_configuresinglestepping}
\inputapidoc{untyped_retype}
\ifxeightsix

31
manual/parts/api/tcb_configuresinglestepping.tex Normal file
View file

@ -0,0 +1,31 @@
%
% Copyright 2016, Data61
% Commonwealth Scientific and Industrial Research Organisation (CSIRO)
% ABN 41 687 119 230.
%
% 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(D61_GPL)
%
\apidoc
{tcb_configuresinglestepping}
{TCB - Configure Single Stepping}
{Set or modify single stepping options for the target TCB. Subsequent calls to this
function overwrite previous configuration. Depending on your processor architecture,
this may or may not require the consumption of a hardware register.}
{static inline seL4\_TCB\_ConfigureSingleStepping\_t seL4\_TCB\_ConfigureSingleStepping}
{
\param{seL4\_TCB}{\_service}{\tcbcapdesc}
\param{seL4\_Uint16}{bp\_num}{\debugargbpnumshortdesc
See \autoref{sec:debug_exceptions} to understand how, and whether, a
hardware breakpoint register may or may not be consumed by this invocation, and
how this may be handled.}
\param{seL4\_Word}{num\_instructions}{Number of instructions to step over before
delivering a fault to the target thread's fault endpoint. Setting this to
\texttt{0} disables single-stepping.}
}
{A \texttt{seL4\_TCB\_ConfigureSingleStepping\_t}: \tcbconfiguresinglesteppingtdesc}
{See \autoref{sec:single_stepping_debug_exception}}

23
manual/parts/api/tcb_getbreakpoint.tex Normal file
View file

@ -0,0 +1,23 @@
%
% Copyright 2016, Data61
% Commonwealth Scientific and Industrial Research Organisation (CSIRO)
% ABN 41 687 119 230.
%
% 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(D61_GPL)
%
\apidoc
{tcb_getbreakpoint}
{TCB - Get Breakpoint}
{Read a breakpoint or watchpoint's current configuration.}
{static inline seL4\_TCB\_GetBreakpoint\_t seL4\_TCB\_GetBreakpoint}
{
\param{seL4\_TCB}{\_service}{\tcbcapdesc}
\param{seL4\_Uint16}{bp\_num}{\debugargbpnumshortdesc}
}
{A \texttt{seL4\_TCB\_GetBreakpoint\_t}: \tcbgetbreakpointtdesc}
{See \autoref{sec:debug_exceptions}}

30
manual/parts/api/tcb_setbreakpoint.tex Normal file
View file

@ -0,0 +1,30 @@
%
% Copyright 2016, Data61
% Commonwealth Scientific and Industrial Research Organisation (CSIRO)
% ABN 41 687 119 230.
%
% 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(D61_GPL)
%
\apidoc
{tcb_setbreakpoint}
{TCB - Set Breakpoint}
{Set or modify a thread's breakpoints or watchpoints. Calls to this function
overwrite previous configurations for the target breakpoint. Do not use this
with seL4\_SingleStep: the API will reject the call and return an error.
Instead, use seL4\_TCB\_ConfigureSingleStepping to configure single-stepping.}
{static inline int seL4\_TCB\_SetBreakpoint}
{
\param{seL4\_TCB}{\_service}{\tcbcapdesc}
\param{seL4\_Uint16}{bp\_num}{\debugargbpnumshortdesc}
\param{seL4\_Word}{vaddr}{\debugargvaddrshortdesc}
\param{seL4\_Word}{type}{\debugargtypeshortdesc}
\param{seL4\_Word}{size}{\debugargsizeshortdesc}
\param{seL4\_Word}{rw}{\debugargrwshortdesc}
}
{\errorenumdesc}
{See \autoref{sec:debug_exceptions}}

27
manual/parts/api/tcb_unsetbreakpoint.tex Normal file
View file

@ -0,0 +1,27 @@
%
% Copyright 2016, Data61
% Commonwealth Scientific and Industrial Research Organisation (CSIRO)
% ABN 41 687 119 230.
%
% 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(D61_GPL)
%
\apidoc
{tcb_unsetbreakpoint}
{TCB - Unset Breakpoint}
{Disables a hardware breakpoint or watchpoint. The caller should assume that
the underlying configuration of the hardware registers has also been cleared.
Do not use this to clear single-stepping: the API will reject the call and
return an error. Instead, use seL4\_TCB\_ConfigureSingleStepping to disable
single-stepping.}
{static inline int seL4\_TCB\_UnsetBreakpoint}
{
\param{seL4\_TCB}{\_service}{\tcbcapdesc}
\param{seL4\_Uint16}{bp\_num}{\debugargbpnumshortdesc}
}
{\errorenumdesc}
{See \autoref{sec:debug_exceptions}}

125
manual/parts/threads.tex
View file

@ -97,7 +97,15 @@ See \autoref{sec:faults} for details.
\label{sec:read_write_registers}
The registers of a thread can be read and written with the
\apifunc{seL4\_TCB\_ReadRegisters}{tcb_readregisters} and \apifunc{seL4\_TCB\_WriteRegisters}{tcb_writeregisters} methods. The register contents are transferred via the IPC buffer. The IPC buffer locations that registers are copied to/from are given below.
\apifunc{seL4\_TCB\_ReadRegisters}{tcb_readregisters} and \apifunc{seL4\_TCB\_WriteRegisters}{tcb_writeregisters} methods.
For some registers, the kernel will silently mask certain bits or ranges of bits off, and force them to contain certain
values to ensure that they cannot be maliciously set to values that would compromise the running system, or to respect
values that the architecture specifications have mandated to be certain values. On X86, these bits currently are:
\begin{itemize}
\item \texttt{EFLAGS}: Bits 1, 3 and 5, TF, Bits 12-31, and IF.
\end{itemize}
The register contents are transferred via the IPC buffer. The IPC buffer locations that registers are copied to/from are given below.
\ifxeightsix
\subsubsection{IA-32}
@ -146,8 +154,8 @@ The registers of a thread can be read and written with the
A thread's actions may result in a fault. Faults are delivered to the
thread's exception handler so that it can take the appropriate action.
The fault type is specified in the message label and is one of:
seL4\_CapFault, seL4\_VMFault, seL4\_UnknownSyscall, seL4\_UserException
or seL4\_Interrupt.
seL4\_CapFault, seL4\_VMFault, seL4\_UnknownSyscall, seL4\_UserException,
seL4\_DebugException or seL4\_Interrupt.
\subsection{Capability Faults}
@ -301,6 +309,117 @@ IA-32 architecture.}
\end{table}
\fi
\subsection{Debug Exception: Breakpoints and Watchpoints}
\label{sec:debug_exceptions}
Debug exceptions are used to deliver trace and debug related events to threads.
Breakpoints, watchpoints, trace-events and instruction-performance sampling
events are examples. These events are supported for userspace threads when the kernel
is configured to include them (when CONFIG\_HARDWARE\_DEBUG\_API is set). Information
on the available hardware debugging resources is presented in the form of the following constants:
\begin{description}
\item[seL4\_NumHWBreakpoints]: Defines the total number of hardware break
registers available, of all types available on the hardware platform. On the ARM
Cortex A7 for example, there are 6 exclusive instruction breakpoint registers,
and 4 exclusive data watchpoint registers, for a total of 10 monitor registers.
On this platform therefore, \texttt{seL4\_NumHWBreakpoints} is defined as 10.
The instruction breakpoint registers will always be assigned the lower API-IDs,
and the data watchpoints will always be assigned following them.
Additionally, \texttt{seL4\_NumExclusiveBreakpoints}, \texttt{seL4\_NumExclusiveWatchpoints}
and \texttt{seL4\_NumDualFunctionMonitors}
are defined for each target platform to reflect the number of available
hardware breakpoints/watchpoints of a certain type.
\item[seL4\_NumExclusiveBreakpoints]: Defines the number of hardware registers
capable of generating a fault \textbf{only} on instruction execution. Currently this will be
set only on ARM platforms. The API-ID of the first exclusive breakpoint is given
in \texttt{seL4\_FirstBreakpoint}. If there are no instruction-break exclusive
registers, \texttt{seL4\_NumExclusiveBreakpoints} will be set to \texttt{0} and
\texttt{seL4\_FirstBreakpoint} will be set to -1.
\item[seL4\_NumExclusiveWatchpoints]: Defines the number of hardware registers
capable of generating a fault \textbf{only} on data access. Currently this will be set only
on ARM platforms. The API-ID of the first exclusive watchpoint is given
in \texttt{seL4\_FirstWatchpoint}. If there are no data-break exclusive
registers, \texttt{seL4\_NumExclusiveWatchpoints} will be set to \texttt{0} and
\texttt{seL4\_FirstWatchpoint} will be set to -1.
\item[seL4\_NumDualFunctionMonitors]: Defines the number of hardware registers
capable of generating a fault on either type of access -- i.e, the register
supports both instruction and data breaks. Currently this will be set only on
x86 platforms. The API-ID of the first dual-function monitor is given
in \texttt{seL4\_FirstDualFunctionMonitor}. If there are no dual-function break
registers, \texttt{seL4\_NumDualFunctionMonitors} will be set to \texttt{0} and
\texttt{seL4\_FirstDualFunctionMonitor} will be set to -1.
\end{description}
\begin{table}[h]
\begin{tabularx}{\textwidth}{XXX}
\toprule
\textbf{Value sent} & \textbf{IPC buffer location} \\
\midrule
\reg{Breakpoint instruction address} & \ipcbloc{IPCBuffer[0]} \\
\reg{Exception reason} & \ipcbloc{IPCBuffer[1]} \\
\reg{Watchpoint data access address} & \ipcbloc{IPCBuffer[2]} \\
\reg{Register API-ID} & \ipcbloc{IPCBuffer[3]} \\
\bottomrule
\end{tabularx}
\caption{\label{tbl:debug_exception_result}Debug fault message layout. The
register API-ID is not returned in the fault message from the kernel on
single-step faults.}
\end{table}
\subsection{Debug Exception: Single-stepping}
\label{sec:single_stepping_debug_exception}
The kernel provides support for the use of hardware single-stepping of userspace
threads when configured to do so (when CONFIG\_HARDWARE\_DEBUG\_API is set). To
this end it exposes the invocation, \texttt{seL4\_TCB\_ConfigureSingleStepping}.
The caller is expected to select an API-ID that corresponds to
an instruction breakpoint, to use when setting up the single-stepping
functionality (i.e, API-ID from 0 to \texttt{seL4\_NumExclusiveBreakpoints} - 1).
However, not all hardware platforms require an actual hardware breakpoint
register to provide single-stepping functionality. If the caller's hardware platform requires the
use of a hardware breakpoint register, it will use the breakpoint register given to it in \texttt{bp\_num},
and return \texttt{true} in \texttt{bp\_was\_consumed}. If the underlying platform does not need a hardware
breakpoint to provide single-stepping, seL4 will return \texttt{false} in \texttt{bp\_was\_consumed} and
leave \texttt{bp\_num} unchanged.
If \texttt{bp\_was\_consumed} is \texttt{true}, the caller should not
attempt to re-configure \texttt{bp\_num} for Breakpoint or Watchpoint usage until
the caller has disabled single-stepping and released that register, via a subsequent
call to \texttt{seL4\_TCB\_ConfigureSingleStepping}, or a fault-reply with
\texttt{n\_instr} being 0. Setting \texttt{num\_instructions} to \texttt{0}
\textbf{disables single stepping}.
On architectures that require an actual hardware registers to be configured for
single-stepping functionality, seL4 will restrict the number of registers that
can be configured as single-steppers, to one at any given time. The register that
is currently configured (if any) for single-stepping will be the implicit
\texttt{bp\_num} argument in a single-step debug fault reply.
The kernel's single-stepping, also supports skipping a certain number of
instructions before delivering the single-step fault message. \texttt{Num\_instructions}
should be set to \texttt{1} when single-stepping, or any non-zero integer value to skip that many
instructions before resuming single-stepping. This skip-count can also be set in
the fault-reply to a single-step debug fault.
\begin{table}[h]
\begin{tabularx}{\textwidth}{XXX}
\toprule
\textbf{Value sent} & \textbf{Register set by reply} & \textbf{IPC buffer location} \\
\midrule
\reg{Breakpoint instruction address} & \texttt{num\_instructions} to skip & \ipcbloc{IPCBuffer[0]} \\
\reg{Exception reason} & --- & \ipcbloc{IPCBuffer[1]} \\
\bottomrule
\end{tabularx}
\caption{\label{tbl:single_step_exception_result}Single-step fault message layout.}
\end{table}
\subsection{VM Fault}
\label{sec:vm-fault}

3
src/arch/arm/32/c_traps.c
View file

@ -24,6 +24,9 @@ static inline void FORCE_INLINE NORETURN restore_user_context(void)
word_t cur_thread_reg = (word_t) ksCurThread;
c_exit_hook();
#ifdef CONFIG_HARDWARE_DEBUG_API
restore_user_debug_context(ksCurThread);
#endif
if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {
asm volatile(

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

@ -17,6 +17,7 @@
#include <kernel/cspace.h>
#include <kernel/thread.h>
#include <machine/io.h>
#include <machine/debug.h>
#include <model/statedata.h>
#include <object/cnode.h>
#include <object/untyped.h>
@ -1334,6 +1335,20 @@ handleVMFault(tcb_t *thread, vm_fault_type_t vm_faultType)
addr = getFAR();
fault = getDFSR();
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Debug exceptions come in on the Prefetch and Data abort vectors.
* We have to test the fault-status bits in the IFSR/DFSR to determine
* if it's a debug exception when one occurs.
*
* If it is a debug exception, return early and don't fallthrough to the
* normal VM Fault handling path.
*/
if (isDebugFault(fault)) {
current_fault = handleUserLevelDebugException(0);
return EXCEPTION_FAULT;
}
#endif
current_fault = fault_vm_fault_new(addr, fault, false);
return EXCEPTION_FAULT;
}
@ -1350,6 +1365,22 @@ handleVMFault(tcb_t *thread, vm_fault_type_t vm_faultType)
#else
fault = getIFSR();
#endif
#ifdef CONFIG_HARDWARE_DEBUG_API
if (isDebugFault(fault)) {
current_fault = handleUserLevelDebugException(pc);
if (fault_debug_exception_get_exceptionReason(current_fault) == seL4_SingleStep
&& !singleStepFaultCounterReady(&thread->tcbArch)) {
/* Don't send a fault message to the thread yet if we were asked
* to step through N instructions and the counter isn't depleted
* yet.
*/
return EXCEPTION_NONE;
}
return EXCEPTION_FAULT;
}
#endif
current_fault = fault_vm_fault_new(pc, fault, true);
return EXCEPTION_FAULT;
}

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

@ -82,6 +82,49 @@ handleFaultReply(tcb_t *receiver, tcb_t *sender)
}
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;
} else {
/* If the reply had all expected registers set, proceed as normal */
n_instrs = getRegister(sender, msgRegisters[0]);
}
/* 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);
}
#endif /* CONFIG_HARDWARE_DEBUG_API */
default:
fail("Invalid fault");
}

22
src/arch/arm/kernel/boot.c
View file

@ -177,15 +177,29 @@ create_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg)
return true;
}
/* This and only this function initialises the CPU. It does NOT initialise any kernel state. */
BOOT_CODE static void
/** This and only this function initialises the CPU.
*
* It does NOT initialise any kernel state.
* @return For the verification build, this currently returns true always.
*/
BOOT_CODE static bool_t
init_cpu(void)
{
activate_global_pd();
if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {
vcpu_boot_init();
}
#ifdef CONFIG_HARDWARE_DEBUG_API
if (!Arch_initHardwareBreakpoints()) {
printf("Kernel built with CONFIG_HARDWARE_DEBUG_API, but this board doesn't "
"reliably support it.\n");
return false;
}
#endif
return true;
}
/* This and only this function initialises the platform. It does NOT initialise any kernel state. */
@ -243,7 +257,9 @@ try_init_kernel(
map_kernel_window();
/* initialise the CPU */
init_cpu();
if (!init_cpu()) {
return false;
}
/* debug output via serial port is only available from here */
printf("Bootstrapping kernel\n");

5
src/arch/arm/machine/Makefile
View file

@ -12,7 +12,8 @@ DIRECTORIES += src/arch/arm/machine
ARCH_C_SOURCES += machine/cache.c \
machine/errata.c \
machine/io.c
machine/io.c \
machine/debug.c
ifeq ($(CPU), cortex-a9)
ARCH_C_SOURCES += machine/gic_pl390.c
@ -33,5 +34,5 @@ ifeq ($(CPU), $(filter $(CPU), cortex-a15 cortex-a7 cortex-a57))
endif
ifdef DEBUG
ARCH_C_SOURCES += machine/debug.c machine/capdl.c
ARCH_C_SOURCES += machine/capdl.c
endif

1343
src/arch/arm/machine/debug.c
View file

File diff suppressed because it is too large Load diff

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

@ -11,6 +11,7 @@
#include <config.h>
#include <types.h>
#include <api/failures.h>
#include <api/constants.h>
#include <machine/registerset.h>
#include <object/structures.h>
#include <arch/machine.h>
@ -119,6 +120,30 @@ setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer)
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)) {

11
src/arch/x86/32/c_traps.c
View file

@ -12,6 +12,7 @@
#include <model/statedata.h>
#include <arch/machine/fpu.h>
#include <arch/fastpath/fastpath.h>
#include <arch/machine/debug.h>
#include <benchmark_track.h>
#include <api/syscall.h>
@ -22,11 +23,7 @@ void NORETURN VISIBLE restore_user_context(void)
{
c_exit_hook();
/* save kernel stack pointer for next exception */
SMP_COND_STATEMENT(ksCurThread->tcbArch.tcbContext.kernelSP = ((word_t)kernel_stack_alloc[getCurrentCPUIndex()]) + 0xffc);
/* set the tss.esp0 */
tss_ptr_set_esp0(&ARCH_NODE_STATE(x86KStss).tss, ((uint32_t)&ksCurThread->tcbArch.tcbContext.registers) + (n_contextRegisters * sizeof(word_t)));
setKernelEntryStackPointer(ksCurThread);
if (unlikely(ksCurThread == ARCH_NODE_STATE(x86KSfpuOwner))) {
/* We are using the FPU, make sure it is enabled */
enableFpu();
@ -37,6 +34,10 @@ void NORETURN VISIBLE restore_user_context(void)
/* No-one (including us) is using the FPU, so we assume it
* is currently disabled */
}
#ifdef CONFIG_HARDWARE_DEBUG_API
restore_user_debug_context(ksCurThread);
#endif
/* see if we entered via syscall */
if (likely(ksCurThread->tcbArch.tcbContext.registers[Error] == -1)) {
asm volatile(

2
src/arch/x86/32/kernel/vspace.c
View file

@ -190,7 +190,7 @@ init_idt_entry(idt_entry_t* idt, interrupt_t interrupt, void(*handler)(void))
uint32_t handler_addr = (uint32_t)handler;
uint32_t dpl = 3;
if (interrupt < int_trap_min) {
if (interrupt < int_trap_min && interrupt != int_software_break_request) {
dpl = 0;
}

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

@ -8,9 +8,11 @@
* @TAG(GD_GPL)
*/
#include <config.h>
#include <arch/machine/registerset.h>
#include <arch/machine/fpu.h>
#include <arch/object/structures.h>
#include <machine/debug.h>
const register_t msgRegisters[] = {
EDI, EBP
@ -55,6 +57,9 @@ void Arch_initContext(user_context_t* context)
context->registers[SS] = SEL_DS_3;
Arch_initFpuContext(context);
#ifdef CONFIG_HARDWARE_DEBUG_API
Arch_initBreakpointContext(&context->breakpointState);
#endif
}
word_t sanitiseRegister(register_t reg, word_t v)
@ -63,6 +68,10 @@ word_t sanitiseRegister(register_t reg, word_t v)
v |= BIT(1); /* reserved bit that must be set to 1 */
v &= ~BIT(3); /* reserved bit that must be set to 0 */
v &= ~BIT(5); /* reserved bit that must be set to 0 */
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Disallow setting Trap Flag: use the API instead */
v &= ~BIT(X86_EFLAGS_TRAP_FLAG_SHIFT);
#endif
v |= BIT(9); /* interrupts must be enabled in userland */
v &= MASK(12); /* bits 12:31 have to be 0 */
}

61
src/arch/x86/32/traps.S
View file

@ -8,6 +8,7 @@
* @TAG(GD_GPL)
*/
#include <config.h>
#include <machine/assembler.h>
# On kernel entry, ESP points to the end of the thread's registers array.
@ -367,7 +368,61 @@ handle_interrupt:
# Handle a kernel exception
BEGIN_FUNC(kernel_exception)
#ifdef DEBUG
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Before giving up and panicking, we need to test for the extra case that
* this might be a kernel exception that is the result of EFLAGS.TF being
* set when SYSENTER was called.
*
* Since EFLAGS.TF is not disabled by SYSENTER, single-stepping continues
* into the kernel, and so causes a debug-exception in kernel code, since
* the CPU is trying to single-step the kernel code.
*
* So we test for EFLAGS.TF, and if it's set, we unset it, and let the
* exception continue. The debug exception handler will notice that it was
* kernel exception, and handle it appropriately -- that really just means
* setting EFLAGS.TF before SYSEXIT so that single-stepping resumes in the
* userspace thread.
*/
movl 64(%esp), %eax
movl $(1<<8), %ebx
testl %ebx, %eax
je .not_eflags_tf
/* Else it was EFLAGS.TF that caused the kernel exception on SYSENTER.
* So, unset the EFLAGS.TF on the stack and this causes the syscall that we
* will return to, to be able to execute properly.
*
* It will then be the debug exception handler's responsibility to re-set
* EFLAGS.TF for the userspace thread before it returns.
*
* So at this point we want to just unset EFLAGS.TF and IRET immediately.
*/
andl $~(1<<8), %eax
movl %eax, 64(%esp)
/* Begin popping registers to IRET now. We don't need to consider any
* unexpected side effects because we are just immediately returning after
* entering.
*/
popl %eax
popl %ebx
popl %ecx
popl %edx
popl %esi
popl %esi
popl %ebp
popl %ds
popl %es
popl %fs
popl %gs
/* Skip FaultIP, TLS_BASE and error-code. */
addl $12, %esp
iretl
.not_eflags_tf:
#endif /* CONFIG_HARDWARE_DEBUG_API */
#ifdef CONFIG_DEBUG_BUILD
# prepare debug info
movl 52(%esp), %eax # EAX contains Error Code
movl 56(%esp), %ebx # EBX contains EIP of the exception generating instruction
@ -390,7 +445,7 @@ BEGIN_FUNC(kernel_exception)
pushl %eax
pushl %ecx
call handleKernelException
#endif
#endif /* CONFIG_DEBUG_BUILD */
jmp halt
END_FUNC(kernel_exception)
@ -409,7 +464,9 @@ END_FUNC(kernel_exception)
# ESP : points to tss.esp0 which points to the end of the thread's registers array
BEGIN_FUNC(handle_syscall)
#ifndef CONFIG_HARDWARE_DEBUG_API
movl (%esp), %esp # ESP := tss.esp0
#endif
subl $4, %esp # skip SS
pushl %ecx # save ESP (passed in ECX)

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

@ -11,6 +11,8 @@
#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>
@ -89,6 +91,53 @@ bool_t handleFaultReply(tcb_t *receiver, tcb_t *sender)
}
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");
}

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

@ -13,6 +13,7 @@
#include <arch/machine/fpu.h>
#include <arch/fastpath/fastpath.h>
#include <arch/kernel/traps.h>
#include <machine/debug.h>
#include <api/syscall.h>
#include <benchmark_track.h>
@ -38,6 +39,15 @@ c_handle_interrupt(int irq, int syscall)
ksKernelEntry.word = type;
#endif
handleVMFaultEvent(type);
#ifdef CONFIG_HARDWARE_DEBUG_API
} else if (irq == int_debug || irq == int_software_break_request) {
/* Debug exception */
#ifdef TRACK_KERNEL_ENTRIES
ksKernelEntry.path = Entry_DebugFault;
ksKernelEntry.word = ksCurThread->tcbArch.tcbContext.registers[FaultIP];
#endif
handleUserLevelDebugException(irq);
#endif /* CONFIG_HARDWARE_DEBUG_API */
} else if (irq < int_irq_min) {
#ifdef TRACK_KERNEL_ENTRIES
ksKernelEntry.path = Entry_UserLevelFault;

5
src/arch/x86/kernel/boot.c
View file

@ -435,6 +435,11 @@ init_cpu(
return false;
}
#ifdef CONFIG_HARDWARE_DEBUG_API
/* Initialize hardware breakpoints */
Arch_initHardwareBreakpoints();
#endif
/* initialise floating-point unit */
if (!Arch_initFpu()) {
return false;

3
src/arch/x86/machine/Makefile
View file

@ -12,7 +12,8 @@ DIRECTORIES += src/arch/$(ARCH)/machine
ARCH_C_SOURCES += machine/hardware.c \
machine/fpu.c \
machine/cpu_identification.c
machine/cpu_identification.c \
machine/breakpoint.c
ifdef DEBUG
ARCH_C_SOURCES += machine/capdl.c

703
src/arch/x86/machine/breakpoint.c Normal file
View file

@ -0,0 +1,703 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_GPL)
*/
#ifdef CONFIG_HARDWARE_DEBUG_API
#include <arch/machine/debug.h>
#include <mode/machine/debug.h>
#include <arch/machine.h>
#include <machine/registerset.h>
#include <plat/api/constants.h> /* seL4_NumHWBReakpoints */
/* Intel manual Vol3, 17.2.4 */
#define X86_DEBUG_BP_SIZE_1B (0x0u)
#define X86_DEBUG_BP_SIZE_2B (0x1u)
#define X86_DEBUG_BP_SIZE_4B (0x3u)
#define X86_DEBUG_BP_SIZE_8B (0x2u)
#define X86_DEBUG_BP0_SIZE_SHIFT (18)
#define X86_DEBUG_BP1_SIZE_SHIFT (22)
#define X86_DEBUG_BP2_SIZE_SHIFT (26)
#define X86_DEBUG_BP3_SIZE_SHIFT (30)
/* NOTE: Intel manual 17.2.4:
* I/O breakpoints are supported by every processor later than i486, but only
* when CR4.DE=1.
* When CR4.DE=0, or if processor is earlier than i586, this bit is "Undefined",
* which is not the same as "Reserved", so it won't trigger an exception - it
* will just cause an undefined reaction from the CPU.
*/
#define X86_DEBUG_BP_TYPE_IO (0x2u)
#define X86_DEBUG_BP_TYPE_INSTR (0x0u)
#define X86_DEBUG_BP_TYPE_DATA_WRITE (0x1u)
#define X86_DEBUG_BP_TYPE_DATA_READWRITE (0x3u)
#define X86_DEBUG_BP0_TYPE_SHIFT (16)
#define X86_DEBUG_BP1_TYPE_SHIFT (20)
#define X86_DEBUG_BP2_TYPE_SHIFT (24)
#define X86_DEBUG_BP3_TYPE_SHIFT (28)
#define X86_DEBUG_EFLAGS_TRAP_FLAG ((word_t)BIT(8))
#define X86_DEBUG_EFLAGS_RESUME_FLAG ((word_t)BIT(16))
#define X86_DEBUG_DR6_SINGLE_STEP_FLAG ((word_t)BIT(14))
#define X86_DEBUG_DR6_BP_MASK (0xFu)
static bool_t byte8_bps_supported = false;
bool_t
byte8BreakpointsSupported(void)
{
return byte8_bps_supported;
}
static inline void
bitwiseAndDr6Reg(word_t mask)
{
word_t tmp;
tmp = readDr6Reg() & mask;
writeDr6Reg(tmp);
}
static inline word_t
readDr7Context(arch_tcb_t *uds)
{
return uds->tcbContext.breakpointState.dr[5];
}
static inline void
bitwiseOrDr7Context(arch_tcb_t *uds, word_t val)
{
uds->tcbContext.breakpointState.dr[5] |= val;
}
static inline void
bitwiseAndDr7Context(arch_tcb_t *uds, word_t mask)
{
uds->tcbContext.breakpointState.dr[5] &= mask;
}
static void
unsetDr7BitsFor(arch_tcb_t *uds, uint16_t bp_num)
{
word_t mask;
switch (bp_num) {
case 0:
mask = (0x3u << X86_DEBUG_BP0_SIZE_SHIFT) | (0x3u << X86_DEBUG_BP0_TYPE_SHIFT);
break;
case 1:
mask = (0x3u << X86_DEBUG_BP1_SIZE_SHIFT) | (0x3u << X86_DEBUG_BP1_TYPE_SHIFT);
break;
case 2:
mask = (0x3u << X86_DEBUG_BP2_SIZE_SHIFT) | (0x3u << X86_DEBUG_BP2_TYPE_SHIFT);
break;
default: /* 3 */
assert(bp_num == 3);
mask = (0x3u << X86_DEBUG_BP3_SIZE_SHIFT) | (0x3u << X86_DEBUG_BP3_TYPE_SHIFT);
break;
}
mask = ~mask;
bitwiseAndDr7Context(uds, mask);
}
/** Converts an seL4_BreakpointType value into the underlying hardware
* equivalent.
* @param bp_num Breakpoint number.
* @param type One of the values of seL4_BreakpointType.
* @param rw Access trigger condition (read/write).
* @return Hardware specific register value representing the inputs.
*/
static inline word_t
convertTypeAndAccessToArch(uint16_t bp_num, word_t type, word_t rw)
{
switch (type) {
case seL4_InstructionBreakpoint:
type = X86_DEBUG_BP_TYPE_INSTR;
break;
default: /* seL4_DataBreakpoint */
assert(type == seL4_DataBreakpoint);
type = (rw == seL4_BreakOnWrite)
? X86_DEBUG_BP_TYPE_DATA_WRITE
: X86_DEBUG_BP_TYPE_DATA_READWRITE;
}
switch (bp_num) {
case 0:
return type << X86_DEBUG_BP0_TYPE_SHIFT;
case 1:
return type << X86_DEBUG_BP1_TYPE_SHIFT;
case 2:
return type << X86_DEBUG_BP2_TYPE_SHIFT;
default: /* 3 */
assert(bp_num == 3);
return type << X86_DEBUG_BP3_TYPE_SHIFT;
}
}
/** Reverse of convertTypeAndAccessToArch(): converts hardware values into
* seL4 API values.
* @param dr7 Hardware register value as input for conversion.
* @param bp_num Breakpoint number.
* @param type[out] Converted type value.
* @param rw[out] Converted output access trigger value.
*/
typedef struct {
word_t type, rw;
} convertedTypeAndAccess_t;
static inline convertedTypeAndAccess_t
convertArchToTypeAndAccess(word_t dr7, uint16_t bp_num)
{
convertedTypeAndAccess_t ret;
switch (bp_num) {
case 0:
dr7 &= 0x3u << X86_DEBUG_BP0_TYPE_SHIFT;
dr7 >>= X86_DEBUG_BP0_TYPE_SHIFT;
break;
case 1:
dr7 &= 0x3u << X86_DEBUG_BP1_TYPE_SHIFT;
dr7 >>= X86_DEBUG_BP1_TYPE_SHIFT;
break;
case 2:
dr7 &= 0x3u << X86_DEBUG_BP2_TYPE_SHIFT;
dr7 >>= X86_DEBUG_BP2_TYPE_SHIFT;
break;
default: /* 3 */
assert(bp_num == 3);
dr7 &= 0x3u << X86_DEBUG_BP3_TYPE_SHIFT;
dr7 >>= X86_DEBUG_BP3_TYPE_SHIFT;
}
switch (dr7) {
case X86_DEBUG_BP_TYPE_INSTR:
ret.type = seL4_InstructionBreakpoint;
ret.rw = seL4_BreakOnRead;
break;
case X86_DEBUG_BP_TYPE_DATA_WRITE:
ret.type = seL4_DataBreakpoint;
ret.rw = seL4_BreakOnWrite;
break;
default: /* Read-write */
assert(dr7 == X86_DEBUG_BP_TYPE_DATA_READWRITE);
ret.type = seL4_DataBreakpoint;
ret.rw = seL4_BreakOnReadWrite;
break;
}
return ret;
}
/** Converts an integer size number into an equivalent hardware register value.
* @param n Breakpoint number.
* @param type One value from seL4_BreakpointType.
* @param size An integer for the operand size of the breakpoint.
* @return Converted, hardware-specific value.
*/
static inline word_t
convertSizeToArch(uint16_t bp_num, word_t type, word_t size)
{
if (type == seL4_InstructionBreakpoint) {
/* Intel manual vol3 17.2.4:
* "If the corresponding RWn field in register DR7 is 00 (instruction
* execution), then the LENn field should also be 00"
*/
size = 0;
} else {
switch (size) {
case 1:
size = X86_DEBUG_BP_SIZE_1B;
break;
case 2:
size = X86_DEBUG_BP_SIZE_2B;
break;
case 8:
size = X86_DEBUG_BP_SIZE_8B;
break;
default: /* 4B */
assert(size == 4);
size = X86_DEBUG_BP_SIZE_4B;
}
}
switch (bp_num) {
case 0:
return size << X86_DEBUG_BP0_SIZE_SHIFT;
case 1:
return size << X86_DEBUG_BP1_SIZE_SHIFT;
case 2:
return size << X86_DEBUG_BP2_SIZE_SHIFT;
default: /* 3 */
assert(bp_num == 3);
return size << X86_DEBUG_BP3_SIZE_SHIFT;
}
}
/** Reverse of convertSizeToArch(): converts a hardware-specific size value
* into an integer representation.
* @param dr7 Hardware register value as input.
* @param n Breakpoint number.
* @return Converted size value.
*/
static inline word_t
convertArchToSize(word_t dr7, uint16_t bp_num)
{
word_t type;
switch (bp_num) {
case 0:
type = dr7 & (0x3u << X86_DEBUG_BP0_TYPE_SHIFT);
type >>= X86_DEBUG_BP0_TYPE_SHIFT;
dr7 &= 0x3u << X86_DEBUG_BP0_SIZE_SHIFT;
dr7 >>= X86_DEBUG_BP0_SIZE_SHIFT;
break;
case 1:
type = dr7 & (0x3u << X86_DEBUG_BP1_TYPE_SHIFT);
type >>= X86_DEBUG_BP1_TYPE_SHIFT;
dr7 &= 0x3u << X86_DEBUG_BP1_SIZE_SHIFT;
dr7 >>= X86_DEBUG_BP1_SIZE_SHIFT;
break;
case 2:
type = dr7 & (0x3u << X86_DEBUG_BP2_TYPE_SHIFT);
type >>= X86_DEBUG_BP2_TYPE_SHIFT;
dr7 &= 0x3u << X86_DEBUG_BP2_SIZE_SHIFT;
dr7 >>= X86_DEBUG_BP2_SIZE_SHIFT;
break;
default: /* 3 */
assert(bp_num == 3);
type = dr7 & (0x3u << X86_DEBUG_BP3_TYPE_SHIFT);
type >>= X86_DEBUG_BP3_TYPE_SHIFT;
dr7 &= 0x3u << X86_DEBUG_BP3_SIZE_SHIFT;
dr7 >>= X86_DEBUG_BP3_SIZE_SHIFT;
}
/* Force size to 0 if type is instruction breakpoint. */
if (type == X86_DEBUG_BP_TYPE_INSTR) {
return 0;
}
switch (dr7) {
case X86_DEBUG_BP_SIZE_1B:
return 1;
case X86_DEBUG_BP_SIZE_2B:
return 2;
case X86_DEBUG_BP_SIZE_8B:
return 8;
default: /* 4B */
assert(dr7 == X86_DEBUG_BP_SIZE_4B);
return 4;
}
}
/** Enables a breakpoint.
* @param bp_num Hardware breakpoint ID. Usually an integer from 0..N.
*/
static void
enableBreakpoint(arch_tcb_t *uds, uint16_t bp_num)
{
word_t enable_bit;
assert(uds != NULL);
assert(bp_num < X86_DEBUG_BP_N_REGS);
switch (bp_num) {
case 0:
enable_bit = X86_DEBUG_BP0_ENABLE_BIT;
break;
case 1:
enable_bit = X86_DEBUG_BP1_ENABLE_BIT;
break;
case 2:
enable_bit = X86_DEBUG_BP2_ENABLE_BIT;
break;
default:
enable_bit = X86_DEBUG_BP3_ENABLE_BIT;
break;
}
bitwiseOrDr7Context(uds, enable_bit);
}
/** Disables a breakpoint without clearing its configuration.
* @param bp_num Hardware breakpoint ID. Usually an integer from 0..N.
*/
static void
disableBreakpoint(arch_tcb_t *uds, uint16_t bp_num)
{
word_t disable_mask;
assert(uds != NULL);
assert(bp_num < X86_DEBUG_BP_N_REGS);
switch (bp_num) {
case 0:
disable_mask = ~X86_DEBUG_BP0_ENABLE_BIT;
break;
case 1:
disable_mask = ~X86_DEBUG_BP1_ENABLE_BIT;
break;
case 2:
disable_mask = ~X86_DEBUG_BP2_ENABLE_BIT;
break;
default:
disable_mask = ~X86_DEBUG_BP3_ENABLE_BIT;
break;
}
bitwiseAndDr7Context(uds, disable_mask);
}
/** Returns a boolean for whether or not a breakpoint is enabled.
* @param bp_num Hardware breakpoint ID. Usually an integer from 0..N.
*/
static bool_t
breakpointIsEnabled(arch_tcb_t *uds, uint16_t bp_num)
{
word_t dr7;
assert(uds != NULL);
assert(bp_num < X86_DEBUG_BP_N_REGS);
dr7 = readDr7Context(uds);
switch (bp_num) {
case 0:
return !!(dr7 & X86_DEBUG_BP0_ENABLE_BIT);
case 1:
return !!(dr7 & X86_DEBUG_BP1_ENABLE_BIT);
case 2:
return !!(dr7 & X86_DEBUG_BP2_ENABLE_BIT);
default:
return !!(dr7 & X86_DEBUG_BP3_ENABLE_BIT);
}
}
static void
setBpVaddrContext(user_breakpoint_state_t *uds, uint16_t bp_num, word_t vaddr)
{
assert(uds != NULL);
switch (bp_num) {
case 0:
uds->dr[0] = vaddr;
break;
case 1:
uds->dr[1] = vaddr;
break;
case 2:
uds->dr[2] = vaddr;
break;
default:
assert(bp_num == 3);
uds->dr[3] = vaddr;
break;
}
return;
}
/** Backend for the seL4_TCB_SetBreakpoint invocation.
*
* @param uds Arch TCB register context structure.
* @param bp_num Hardware breakpoint ID.
* @param vaddr USerspace virtual address on which you'd like this breakpoing
* to trigger.
* @param types One of the seL4_BreakpointType values.
* @param size positive integer indicating the byte-range size that should
* trigger the breakpoint. 0 is valid for Instruction breakpoints.
* @param rw Access type that should trigger the BP (read/write).
*/
void
setBreakpoint(arch_tcb_t *uds,
uint16_t bp_num, word_t vaddr, word_t types, word_t size, word_t rw)
{
word_t dr7val;
assert(uds != NULL);
dr7val = convertTypeAndAccessToArch(bp_num, types, rw);
dr7val |= convertSizeToArch(bp_num, types, size);
setBpVaddrContext(&uds->tcbContext.breakpointState, bp_num, vaddr);
unsetDr7BitsFor(uds, bp_num);
bitwiseOrDr7Context(uds, dr7val);
enableBreakpoint(uds, bp_num);
}
static word_t
getBpVaddrContext(user_breakpoint_state_t *uds, uint16_t bp_num)
{
assert(uds != NULL);
switch (bp_num) {
case 0:
return uds->dr[0];
case 1:
return uds->dr[1];
case 2:
return uds->dr[2];
default:
assert(bp_num == 3);
return uds->dr[3];
}
}
/** Backend for the x86 seL4_TCB_GetBreakpoint invocation.
*
* Returns information about a particular breakpoint ID, including whether or
* not it's enabled.
*
* @param uds Arch TCB register context pointer.
* @param bp_num Hardware breakpoint ID of the BP you'd like to query.
* @return Structure containing information about the status of the breakpoint.
*/
getBreakpoint_t
getBreakpoint(arch_tcb_t *uds, uint16_t bp_num)
{
word_t dr7val;
getBreakpoint_t ret;
convertedTypeAndAccess_t res;
dr7val = readDr7Context(uds);
ret.vaddr = getBpVaddrContext(&uds->tcbContext.breakpointState, bp_num);
ret.size = convertArchToSize(dr7val, bp_num);
res = convertArchToTypeAndAccess(dr7val, bp_num);
ret.type = res.type;
ret.rw = res.rw;
ret.is_enabled = breakpointIsEnabled(uds, bp_num);
return ret;
}
/** Backend for the x86 seL4_TCB_UnsetBreakpoint invocation.
*
* Unsets and *clears* a hardware breakpoint.
* @param uds Arch TCB register context pointer.
* @param bp_num The hardware breakpoint ID you'd like to clear.
*/
void
unsetBreakpoint(arch_tcb_t *uds, uint16_t bp_num)
{
disableBreakpoint(uds, bp_num);
unsetDr7BitsFor(uds, bp_num);
setBpVaddrContext(&uds->tcbContext.breakpointState, bp_num, 0);
}
/** Used in the exception path to determine if an exception was caused by
* single-stepping being active.
*
* @param uc Arch TCB register context structure.
* @return a structure stating whether or not the exception was caused by
* hardware single-stepping, and what the instruction vaddr was.
*/
typedef struct {
bool_t ret;
word_t instr_vaddr;
} testAndResetSingleStepException_t;
static testAndResetSingleStepException_t
testAndResetSingleStepException(arch_tcb_t *uc)
{
testAndResetSingleStepException_t ret;
word_t dr6;
dr6 = readDr6Reg();
if (!(dr6 & X86_DEBUG_DR6_SINGLE_STEP_FLAG)) {
ret.ret = false;
return ret;
}
ret.ret = true;
ret.instr_vaddr = uc->tcbContext.registers[FaultIP];
bitwiseAndDr6Reg(~X86_DEBUG_DR6_SINGLE_STEP_FLAG);
/* And that's not all: if the breakpoint is an instruction breakpoint, we
* also need to set EFLAGS.RF. The processor raises the #DB exception BEFORE
* the instruction executes. This means that when we IRET to userspace, the
* SAME breakpoint will trigger again, and so on ad infinitum. EFLAGS.RF
* solves this problem:
*
* When EFLAGS.RF is set, the processor will ignore instruction breakpoints
* that should be raised, for one instruction. After that instruction
* executes, the processor will also automatically unset EFLAGS.RF. See
* Intel manuals, vol3, section 17.3.1.1.
*/
/* This will automatically be popped by restore_user_context() */
uc->tcbContext.registers[EFLAGS] |= X86_DEBUG_EFLAGS_RESUME_FLAG;
return ret;
}
bool_t
configureSingleStepping(arch_tcb_t *uc, uint16_t bp_num, word_t n_instr,
UNUSED bool_t is_reply)
{
/* On x86 no hardware breakpoints are needed for single stepping. */
if (n_instr == 0) {
/* If n_instr (number of instructions to single-step) is 0, that is the
* same as requesting that single-stepping be disabled.
*/
uc->tcbContext.breakpointState.single_step_enabled = false;
uc->tcbContext.registers[EFLAGS] &= ~X86_DEBUG_EFLAGS_TRAP_FLAG;
} else {
uc->tcbContext.breakpointState.single_step_enabled = true;
}
uc->tcbContext.breakpointState.n_instructions = n_instr;
return false;
}
/** Used in the exception path to determine which breakpoint triggered the
* exception.
*
* First, checks to see which hardware breakpoint was triggered, and saves
* the ID of that breakpoint. Secondly, resets that breakpoint such that its
* "triggered" bit is no longer in the asserted state -- whatever that means
* for the arch. So on x86, that means clearing the indicator bit in DR6.
*
* Aside from the ID of the breakpoint that was raised, also returns
* information about the breakpoint (vaddr, access, type, etc).
*
* @param uc Arch TCB register context pointer.
* @return Structure with a "bp_num" member that states which hardware
* breakpoint was triggered, and gives information describing the
* breakpoint.
*/
typedef struct {
int bp_num;
word_t vaddr, reason;
} getAndResetActiveBreakpoint_t;
static getAndResetActiveBreakpoint_t
getAndResetActiveBreakpoint(arch_tcb_t *at)
{
convertedTypeAndAccess_t tmp;
getAndResetActiveBreakpoint_t ret;
/* Read from the hardware regs, not user context */
word_t dr6 = readDr6Reg();
if (dr6 & BIT(0)) {
ret.bp_num = 0;
} else if (dr6 & BIT(1)) {
ret.bp_num = 1;
} else if (dr6 & BIT(2)) {
ret.bp_num = 2;
} else if (dr6 & BIT(3)) {
ret.bp_num = 3;
} else {
ret.bp_num = -1;
return ret;
}
tmp = convertArchToTypeAndAccess(readDr7Context(at), ret.bp_num);
ret.vaddr = getBpVaddrContext(&at->tcbContext.breakpointState, ret.bp_num);
ret.reason = tmp.type;
bitwiseAndDr6Reg(~BIT(ret.bp_num));
return ret;
}
exception_t
handleUserLevelDebugException(int int_vector)
{
arch_tcb_t *context;
getAndResetActiveBreakpoint_t active_bp;
testAndResetSingleStepException_t single_step_info;
#if defined(DEBUG) || defined(CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES)
ksKernelEntry.path = Entry_UserLevelFault;
ksKernelEntry.word = int_vector;
#else
(void)int_vector;
#endif /* DEBUG */
#ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES
benchmark_track_start();
#endif
context = &ksCurThread->tcbArch;
/* Software break request (INT3) is detected by the vector number */
if (int_vector == int_software_break_request) {
current_fault = fault_debug_exception_new(getRestartPC(ksCurThread),
0, seL4_SoftwareBreakRequest);
} else {
/* Hardware breakpoint trigger is detected using DR6 */
active_bp = getAndResetActiveBreakpoint(context);
if (active_bp.bp_num >= 0) {
current_fault = fault_debug_exception_new(active_bp.vaddr,
active_bp.bp_num,
active_bp.reason);
} else {
single_step_info = testAndResetSingleStepException(context);
if (single_step_info.ret == true) {
/* If the caller asked us to skip over N instructions before
* generating the next single-step breakpoint, we shouldn't
* bother to construct a fault message until we've skipped N
* instructions.
*/
if (singleStepFaultCounterReady(context) == false) {
return EXCEPTION_NONE;
}
current_fault = fault_debug_exception_new(single_step_info.instr_vaddr,
0, seL4_SingleStep);
} else {
return EXCEPTION_SYSCALL_ERROR;
}
}
}
handleFault(ksCurThread);
schedule();
activateThread();
return EXCEPTION_NONE;
}
BOOT_CODE bool_t
Arch_initHardwareBreakpoints(void)
{
x86_cpu_identity_t *modelinfo;
modelinfo = x86_cpuid_get_model_info();
/* Intel manuals, vol3, section 17.2.4, "NOTES". */
if (modelinfo->family == 15) {
if (modelinfo->model == 3 || modelinfo->model == 4
|| modelinfo->model == 6) {
byte8_bps_supported = true;
}
}
if (modelinfo->family == 6) {
if (modelinfo->model == 15 || modelinfo->model == 23
|| modelinfo->model == 0x1C) {
byte8_bps_supported = true;
}
}
return true;
}
void
Arch_initBreakpointContext(user_breakpoint_state_t *uds)
{
memset(uds, 0, sizeof(*uds));
/* Preload reserved values into register context */
uds->dr[4] = readDr6Reg() &
~(BIT(0)
| BIT(1)
| BIT(2)
| BIT(3)
| X86_DEBUG_DR6_SINGLE_STEP_FLAG);
uds->dr[5] = readDr7Reg() &
~(X86_DEBUG_BP0_ENABLE_BIT | X86_DEBUG_BP1_ENABLE_BIT
| X86_DEBUG_BP2_ENABLE_BIT
| X86_DEBUG_BP3_ENABLE_BIT);
}
#endif

2
src/arch/x86/machine/hardware.c
View file

@ -23,9 +23,11 @@ init_sysenter_msrs(void)
{
x86_wrmsr(IA32_SYSENTER_CS_MSR, (uint64_t)(word_t)SEL_CS_0);
x86_wrmsr(IA32_SYSENTER_EIP_MSR, (uint64_t)(word_t)&handle_syscall);
#ifndef CONFIG_HARDWARE_DEBUG_API
/* manually add 4 bytes to x86KStss so that it is valid for both
* 32-bit and 64-bit */
x86_wrmsr(IA32_SYSENTER_ESP_MSR, (uint64_t)(word_t)((char *)&ARCH_NODE_STATE(x86KStss).tss.words[0] + 4));
#endif
}
word_t PURE getRestartPC(tcb_t *thread)

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

@ -136,6 +136,30 @@ word_t setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer)
}
}
#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");
}

260
src/object/tcb.c
View file

@ -12,6 +12,7 @@
#include <api/failures.h>
#include <api/invocation.h>
#include <api/syscall.h>
#include <api/shared_types.h>
#include <machine/io.h>
#include <object/structures.h>
#include <object/objecttype.h>
@ -23,6 +24,7 @@
#include <model/statedata.h>
#include <util.h>
#include <string.h>
#include <stdint.h>
#define NULL_PRIO 0
@ -305,6 +307,250 @@ copyMRs(tcb_t *sender, word_t *sendBuf, tcb_t *receiver,
return i;
}
#ifdef CONFIG_HARDWARE_DEBUG_API
static exception_t
invokeConfigureSingleStepping(word_t *buffer, arch_tcb_t *context,
uint16_t bp_num, word_t n_instrs)
{
bool_t bp_was_consumed;
bp_was_consumed = configureSingleStepping(context, bp_num, n_instrs, false);
if (n_instrs == 0) {
unsetBreakpointUsedFlag(context, bp_num);
setMR(ksCurThread, buffer, 0, false);
} else {
setBreakpointUsedFlag(context, bp_num);
setMR(ksCurThread, buffer, 0, bp_was_consumed);
}
return EXCEPTION_NONE;
}
static exception_t
decodeConfigureSingleStepping(cap_t cap, word_t *buffer)
{
uint16_t bp_num;
word_t n_instrs;
tcb_t *tcb;
arch_tcb_t *context;
syscall_error_t syserr;
tcb = TCB_PTR(cap_thread_cap_get_capTCBPtr(cap));
context = &tcb->tcbArch;
bp_num = getSyscallArg(0, buffer);
n_instrs = getSyscallArg(1, buffer);
syserr = Arch_decodeConfigureSingleStepping(context, bp_num, n_instrs, false);
if (syserr.type != seL4_NoError) {
current_syscall_error = syserr;
return EXCEPTION_SYSCALL_ERROR;
}
setThreadState(ksCurThread, ThreadState_Restart);
return invokeConfigureSingleStepping(buffer, context, bp_num, n_instrs);
}
static exception_t
invokeSetBreakpoint(arch_tcb_t *context, uint16_t bp_num,
word_t vaddr, word_t type, word_t size, word_t rw)
{
setBreakpoint(context, bp_num, vaddr, type, size, rw);
/* Signal restore_user_context() to pop the breakpoint context on return. */
setBreakpointUsedFlag(context, bp_num);
return EXCEPTION_NONE;
}
static exception_t
decodeSetBreakpoint(cap_t cap, word_t *buffer)
{
uint16_t bp_num;
word_t vaddr, type, size, rw;
tcb_t *tcb;
arch_tcb_t *context;
syscall_error_t error;
tcb = TCB_PTR(cap_thread_cap_get_capTCBPtr(cap));
bp_num = getSyscallArg(0, buffer);
vaddr = getSyscallArg(1, buffer);
type = getSyscallArg(2, buffer);
size = getSyscallArg(3, buffer);
rw = getSyscallArg(4, buffer);
/* We disallow the user to set breakpoint addresses that are in the kernel
* vaddr range.
*/
if (vaddr >= (word_t)kernelBase) {
userError("Debug: Invalid address %lx: bp addresses must be userspace "
"addresses.",
vaddr);
current_syscall_error.type = seL4_InvalidArgument;
current_syscall_error.invalidArgumentNumber = 1;
return EXCEPTION_SYSCALL_ERROR;
}
if (type != seL4_InstructionBreakpoint && type != seL4_DataBreakpoint) {
userError("Debug: Unknown breakpoint type %lx.", type);
current_syscall_error.type = seL4_InvalidArgument;
current_syscall_error.invalidArgumentNumber = 2;
return EXCEPTION_SYSCALL_ERROR;
} else if (type == seL4_InstructionBreakpoint) {
if (size != 0) {
userError("Debug: Instruction bps must have size of 0.");
current_syscall_error.type = seL4_InvalidArgument;
current_syscall_error.invalidArgumentNumber = 3;
return EXCEPTION_SYSCALL_ERROR;
}
if (rw != seL4_BreakOnRead) {
userError("Debug: Instruction bps must be break-on-read.");
current_syscall_error.type = seL4_InvalidArgument;
current_syscall_error.invalidArgumentNumber = 4;
return EXCEPTION_SYSCALL_ERROR;
}
if (bp_num >= seL4_FirstWatchpoint
&& seL4_FirstBreakpoint != seL4_FirstWatchpoint) {
userError("Debug: Can't specify a watchpoint ID with type seL4_InstructionBreakpoint.");
current_syscall_error.type = seL4_InvalidArgument;
current_syscall_error.invalidArgumentNumber = 2;
return EXCEPTION_SYSCALL_ERROR;
}
} else if (type == seL4_DataBreakpoint) {
if (size == 0) {
userError("Debug: Data bps cannot have size of 0.");
current_syscall_error.type = seL4_InvalidArgument;
current_syscall_error.invalidArgumentNumber = 3;
return EXCEPTION_SYSCALL_ERROR;
}
if (bp_num < seL4_FirstWatchpoint) {
userError("Debug: Data watchpoints cannot specify non-data watchpoint ID.");
current_syscall_error.type = seL4_InvalidArgument;
current_syscall_error.invalidArgumentNumber = 2;
return EXCEPTION_SYSCALL_ERROR;
}
} else if (type == seL4_SoftwareBreakRequest) {
userError("Debug: Use a software breakpoint instruction to trigger a "
"software breakpoint.");
current_syscall_error.type = seL4_InvalidArgument;
current_syscall_error.invalidArgumentNumber = 2;
return EXCEPTION_SYSCALL_ERROR;
}
if (rw != seL4_BreakOnRead && rw != seL4_BreakOnWrite
&& rw != seL4_BreakOnReadWrite) {
userError("Debug: Unknown access-type %lu.", rw);
current_syscall_error.type = seL4_InvalidArgument;
current_syscall_error.invalidArgumentNumber = 3;
return EXCEPTION_SYSCALL_ERROR;
}
if (size != 0 && size != 1 && size != 2 && size != 4 && size != 8) {
userError("Debug: Invalid size %lu.", size);
current_syscall_error.type = seL4_InvalidArgument;
current_syscall_error.invalidArgumentNumber = 3;
return EXCEPTION_SYSCALL_ERROR;
}
if (size > 0 && vaddr & (size - 1)) {
/* Just Don't allow unaligned watchpoints. They are undefined
* both ARM and x86.
*
* X86: Intel manuals, vol3, 17.2.5:
* "Two-byte ranges must be aligned on word boundaries; 4-byte
* ranges must be aligned on doubleword boundaries"
* "Unaligned data or I/O breakpoint addresses do not yield valid
* results"
*
* ARM: ARMv7 manual, C11.11.44:
* "A DBGWVR is programmed with a word-aligned address."
*/
userError("Debug: Unaligned data watchpoint address %lx (size %lx) "
"rejected.\n",
vaddr, size);
current_syscall_error.type = seL4_AlignmentError;
return EXCEPTION_SYSCALL_ERROR;
}
context = &tcb->tcbArch;
error = Arch_decodeSetBreakpoint(context, bp_num, vaddr, type, size, rw);
if (error.type != seL4_NoError) {
current_syscall_error = error;
return EXCEPTION_SYSCALL_ERROR;
}
setThreadState(ksCurThread, ThreadState_Restart);
return invokeSetBreakpoint(context, bp_num,
vaddr, type, size, rw);
}
static exception_t
invokeGetBreakpoint(word_t *buffer, arch_tcb_t *context, uint16_t bp_num)
{
getBreakpoint_t res;
res = getBreakpoint(context, bp_num);
setMR(ksCurThread, buffer, 0, res.vaddr);
setMR(ksCurThread, buffer, 1, res.type);
setMR(ksCurThread, buffer, 2, res.size);
setMR(ksCurThread, buffer, 3, res.rw);
setMR(ksCurThread, buffer, 4, res.is_enabled);
return EXCEPTION_NONE;
}
static exception_t
decodeGetBreakpoint(cap_t cap, word_t *buffer)
{
tcb_t *tcb;
uint16_t bp_num;
arch_tcb_t *context;
syscall_error_t error;
tcb = TCB_PTR(cap_thread_cap_get_capTCBPtr(cap));
bp_num = getSyscallArg(0, buffer);
context = &tcb->tcbArch;
error = Arch_decodeGetBreakpoint(context, bp_num);
if (error.type != seL4_NoError) {
current_syscall_error = error;
return EXCEPTION_SYSCALL_ERROR;
}
setThreadState(ksCurThread, ThreadState_Restart);
return invokeGetBreakpoint(buffer, context, bp_num);
}
static exception_t
invokeUnsetBreakpoint(arch_tcb_t *context, uint16_t bp_num)
{
/* Maintain the bitfield of in-use breakpoints. */
unsetBreakpoint(context, bp_num);
unsetBreakpointUsedFlag(context, bp_num);
return EXCEPTION_NONE;
}
static exception_t
decodeUnsetBreakpoint(cap_t cap, word_t *buffer)
{
tcb_t *tcb;
uint16_t bp_num;
arch_tcb_t *context;
syscall_error_t error;
tcb = TCB_PTR(cap_thread_cap_get_capTCBPtr(cap));
bp_num = getSyscallArg(0, buffer);
context = &tcb->tcbArch;
error = Arch_decodeUnsetBreakpoint(context, bp_num);
if (error.type != seL4_NoError) {
current_syscall_error = error;
return EXCEPTION_SYSCALL_ERROR;
}
setThreadState(ksCurThread, ThreadState_Restart);
return invokeUnsetBreakpoint(context, bp_num);
}
#endif /* CONFIG_HARDWARE_DEBUG_API */
/* The following functions sit in the syscall error monad, but include the
* exception cases for the preemptible bottom end, as they call the invoke
* functions directly. This is a significant deviation from the Haskell
@ -357,6 +603,20 @@ decodeTCBInvocation(word_t invLabel, word_t length, cap_t cap,
case TCBUnbindNotification:
return decodeUnbindNotification(cap);
#ifdef CONFIG_HARDWARE_DEBUG_API
case TCBConfigureSingleStepping:
return decodeConfigureSingleStepping(cap, buffer);
case TCBSetBreakpoint:
return decodeSetBreakpoint(cap, buffer);
case TCBGetBreakpoint:
return decodeGetBreakpoint(cap, buffer);
case TCBUnsetBreakpoint:
return decodeUnsetBreakpoint(cap, buffer);
#endif
default:
/* Haskell: "throw IllegalOperation" */
userError("TCB: Illegal operation.");