RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

Add VSpace_Read/Write_Word workaround

Browse Source 
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
This commit is contained in:
Alwin Joshy
2024-08-26 11:53:13 +10:00
committed by Ivan-Velickovic
parent 595fff33a2
commit 3862d14fe4
2 changed files with 256 additions and 73 deletions
Download Patch File Download Diff File Expand all files Collapse all files

70
libsel4/sel4_arch_include/aarch64/interfaces/object-api-sel4-arch.xml
View File

@@ -216,6 +216,76 @@
</description>
</error>
</method>
<method id="ARMVSpaceRead_Word" name="Read_Word" manual_label="vspace_read_word" manual_name="Read Word">
<condition><config var="CONFIG_DEBUG_BUILD"/></condition>
<brief>
Read a word from some address in a vspace.
</brief>
<param dir="in" name="vaddr" type="seL4_Word" description="Address to read from" />
<param dir="out" name="value" type="seL4_Word" description="Value read from the address" />
<error name="seL4_FailedLookup">
<description>
The <texttt text="_service"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="end"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start"/> is greater than or equal to <texttt text="end"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_RangeError">
<description>
The specified range crosses a page boundary.
</description>
</error>
</method>
<method id="ARMVSpaceWrite_Word" name="Write_Word" manual_label="vspace_write_word" manual_name="Write Word">
<condition><config var="CONFIG_DEBUG_BUILD"/></condition>
<brief>
Write a word to some address in a vspace.
</brief>
<param dir="in" name="vaddr" type="seL4_Word" description="Address to read from" />
<param dir="in" name="value" type="seL4_Word" description="Value to write to the address" />
<error name="seL4_FailedLookup">
<description>
The <texttt text="_service"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="end"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start"/> is greater than or equal to <texttt text="end"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_RangeError">
<description>
The specified range crosses a page boundary.
</description>
</error>
</method>
</interface>
<interface name="seL4_ARM_SMC" manual_name="SMC" cap_description="Capability to allow threads to make Secure Monitor Calls.">
<method id="ARMSMCCall" name="Call" manual_name="SMC Call" manual_label="smc_call">

259
src/arch/arm/64/kernel/vspace.c
View File

@@ -20,6 +20,7 @@
#include <object/untyped.h>
#include <arch/api/invocation.h>
#include <arch/kernel/vspace.h>
#include <mode/machine/debug.h>
#include <linker.h>
#include <plat/machine/hardware.h>
#include <armv/context_switch.h>
@@ -1298,22 +1299,203 @@ static exception_t performASIDControlInvocation(void *frame, cte_t *slot,
return EXCEPTION_NONE;
}
#if defined(CONFIG_PRINTING) || defined(CONFIG_DEBUG_BUILD)
typedef struct readWordFromVSpace_ret {
exception_t status;
word_t value;
} readWordFromVSpace_ret_t;
static readWordFromVSpace_ret_t readWordFromVSpace(vspace_root_t *pd, word_t vaddr)
{
readWordFromVSpace_ret_t ret;
word_t offset;
pptr_t kernel_vaddr;
word_t *value;
lookupPTSlot_ret_t lookup_ret = lookupPTSlot(pd, vaddr);
/* Check that the returned slot is a page. */
if (!pte_ptr_get_valid(lookup_ret.ptSlot) ||
(pte_pte_table_ptr_get_present(lookup_ret.ptSlot) && lookup_ret.ptBitsLeft > PAGE_BITS)) {
ret.status = EXCEPTION_LOOKUP_FAULT;
return ret;
}
offset = vaddr & MASK(lookup_ret.ptBitsLeft);
kernel_vaddr = (word_t)paddr_to_pptr(pte_page_ptr_get_page_base_address(lookup_ret.ptSlot));
value = (word_t *)(kernel_vaddr + offset);
ret.status = EXCEPTION_NONE;
ret.value = *value;
return ret;
}
#ifdef CONFIG_PRINTING
void Arch_userStackTrace(tcb_t *tptr)
{
cap_t threadRoot;
vspace_root_t *vspaceRoot;
word_t sp;
threadRoot = TCB_PTR_CTE_PTR(tptr, tcbVTable)->cap;
/* lookup the vspace root */
if (cap_get_capType(threadRoot) != cap_vspace_cap) {
printf("Invalid vspace\n");
return;
}
vspaceRoot = VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(threadRoot));
sp = getRegister(tptr, SP_EL0);
/* check for alignment so we don't have to worry about accessing
* words that might be on two different pages */
if (!IS_ALIGNED(sp, seL4_WordSizeBits)) {
printf("SP not aligned\n");
return;
}
for (unsigned int i = 0; i < CONFIG_USER_STACK_TRACE_LENGTH; i++) {
word_t address = sp + (i * sizeof(word_t));
readWordFromVSpace_ret_t result = readWordFromVSpace(vspaceRoot,
address);
if (result.status == EXCEPTION_NONE) {
printf("0x%"SEL4_PRIx_word": 0x%"SEL4_PRIx_word"\n",
address, result.value);
} else {
printf("0x%"SEL4_PRIx_word": INVALID\n", address);
}
}
}
#endif /* CONFIG_PRINTING */
#ifdef CONFIG_DEBUG_BUILD
typedef struct writeWordToVSpace_ret {
exception_t status;
} writeWordToVSpace_ret_t;
static writeWordToVSpace_ret_t writeWordtoVSpace(vspace_root_t *pd, asid_t asid, word_t vaddr, word_t value) {
writeWordToVSpace_ret_t ret;
word_t offset;
pptr_t kernel_vaddr;
word_t *addr;
lookupPTSlot_ret_t lookup_ret = lookupPTSlot(pd, vaddr);
if (!pte_ptr_get_valid(lookup_ret.ptSlot) ||
(pte_pte_table_ptr_get_present(lookup_ret.ptSlot) && lookup_ret.ptBitsLeft > PAGE_BITS)) {
ret.status = EXCEPTION_LOOKUP_FAULT;
return ret;
}
offset = vaddr & MASK(lookup_ret.ptBitsLeft);
kernel_vaddr = (word_t) paddr_to_pptr(pte_page_ptr_get_page_base_address(lookup_ret.ptSlot));
addr = (word_t *) (kernel_vaddr + offset);
*addr = value;
performVSpaceFlush(ARMVSpaceUnify_Instruction, pd, asid, vaddr, vaddr + sizeof(word_t),
pte_page_ptr_get_page_base_address(lookup_ret.ptSlot) + offset);
ret.status = EXCEPTION_NONE;
return ret;
}
#endif /* CONFIG_DEBUG_BUILD */
#endif /* defined(CONFIG_PRINTING) || defined(CONFIG_DEBUG_BUILD) */
static exception_t decodeARMVSpaceRootInvocation(word_t invLabel, word_t length,
cte_t *cte, cap_t cap, word_t *buffer)
{
vptr_t start, end;
paddr_t pstart;
asid_t asid;
vspace_root_t *vspaceRoot;
lookupPTSlot_ret_t resolve_ret;
findVSpaceForASID_ret_t find_ret;
pte_t pte;
switch (invLabel) {
#ifdef CONFIG_DEBUG_BUILD
case ARMVSpaceRead_Word:
case ARMVSpaceWrite_Word:
{
vptr_t vaddr;
word_t value = 0;
if ((invLabel == ARMVSpaceRead_Word && length < 1) ||
(invLabel == ARMVSpaceWrite_Word && length < 2)) {
userError("VSpaceRoot Read/Write Word: Truncated message.");
current_syscall_error.type = seL4_TruncatedMessage;
return EXCEPTION_SYSCALL_ERROR;
}
vaddr = getSyscallArg(0, buffer);
if (invLabel == ARMVSpaceWrite_Word) {
value = getSyscallArg(1, buffer);
}
if (vaddr > USER_TOP) {
userError("VSpaceRoot Read/Write Word: Exceed the user addressable region.");
current_syscall_error.type = seL4_IllegalOperation;
return EXCEPTION_SYSCALL_ERROR;
}
if (unlikely(!isValidNativeRoot(cap))) {
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 0;
return EXCEPTION_SYSCALL_ERROR;
}
vspaceRoot = VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(cap));
asid = cap_vspace_cap_get_capVSMappedASID(cap);
find_ret = findVSpaceForASID(asid);
if (unlikely(find_ret.status != EXCEPTION_NONE)) {
userError("VSpaceRoot Read/Write Word: No VSpace for ASID");
current_syscall_error.type = seL4_FailedLookup;
current_syscall_error.failedLookupWasSource = false;
return EXCEPTION_SYSCALL_ERROR;
}
if (unlikely(find_ret.vspace_root != vspaceRoot)) {
userError("VSpaceRoot Read/Write Word: Invalid VSpace Cap");
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 0;
return EXCEPTION_SYSCALL_ERROR;
}
if (invLabel == ARMVSpaceRead_Word) {
readWordFromVSpace_ret_t ret = readWordFromVSpace(vspaceRoot, vaddr);
if (!ret.status) {
word_t *ipcBuffer = lookupIPCBuffer(true, NODE_STATE(ksCurThread));
setRegister(NODE_STATE(ksCurThread), badgeRegister, 0);
unsigned int length = setMR(NODE_STATE(ksCurThread), ipcBuffer, 0, ret.value);
setRegister(NODE_STATE(ksCurThread), msgInfoRegister, wordFromMessageInfo(
seL4_MessageInfo_new(0, 0, 0, length)));
return EXCEPTION_NONE;
} else {
current_syscall_error.type = seL4_FailedLookup;
}
} else {
writeWordToVSpace_ret_t ret = writeWordtoVSpace(vspaceRoot, asid, vaddr, value);
if (!ret.status) {
setRegister(NODE_STATE(ksCurThread), badgeRegister, 0);
setRegister(NODE_STATE(ksCurThread), msgInfoRegister, wordFromMessageInfo(
seL4_MessageInfo_new(0, 0, 0, 0)));
return EXCEPTION_NONE;
} else {
current_syscall_error.type = seL4_FailedLookup;
}
}
return EXCEPTION_SYSCALL_ERROR;
}
#endif /* CONFIG_DEBUG_BUILD */
case ARMVSpaceClean_Data:
case ARMVSpaceInvalidate_Data:
case ARMVSpaceCleanInvalidate_Data:
case ARMVSpaceUnify_Instruction:
{
vptr_t start, end;
paddr_t pstart;
lookupPTSlot_ret_t resolve_ret;
if (length < 2) {
userError("VSpaceRoot Flush: Truncated message.");
@@ -1405,7 +1587,7 @@ static exception_t decodeARMVSpaceRootInvocation(word_t invLabel, word_t length,
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
return performVSpaceFlush(invLabel, vspaceRoot, asid, start, end - 1, pstart);
}
default:
current_syscall_error.type = seL4_IllegalOperation;
return EXCEPTION_SYSCALL_ERROR;
@@ -1877,75 +2059,6 @@ void kernelDataAbort(word_t pc)
}
#endif /* CONFIG_DEBUG_BUILD */
#ifdef CONFIG_PRINTING
typedef struct readWordFromVSpace_ret {
exception_t status;
word_t value;
} readWordFromVSpace_ret_t;
static readWordFromVSpace_ret_t readWordFromVSpace(vspace_root_t *pd, word_t vaddr)
{
readWordFromVSpace_ret_t ret;
word_t offset;
pptr_t kernel_vaddr;
word_t *value;
lookupPTSlot_ret_t lookup_ret = lookupPTSlot(pd, vaddr);
/* Check that the returned slot is a page. */
if (!pte_ptr_get_valid(lookup_ret.ptSlot) ||
(pte_pte_table_ptr_get_present(lookup_ret.ptSlot) && lookup_ret.ptBitsLeft > PAGE_BITS)) {
ret.status = EXCEPTION_LOOKUP_FAULT;
return ret;
}
offset = vaddr & MASK(lookup_ret.ptBitsLeft);
kernel_vaddr = (word_t)paddr_to_pptr(pte_page_ptr_get_page_base_address(lookup_ret.ptSlot));
value = (word_t *)(kernel_vaddr + offset);
ret.status = EXCEPTION_NONE;
ret.value = *value;
return ret;
}
void Arch_userStackTrace(tcb_t *tptr)
{
cap_t threadRoot;
vspace_root_t *vspaceRoot;
word_t sp;
threadRoot = TCB_PTR_CTE_PTR(tptr, tcbVTable)->cap;
/* lookup the vspace root */
if (cap_get_capType(threadRoot) != cap_vspace_cap) {
printf("Invalid vspace\n");
return;
}
vspaceRoot = VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(threadRoot));
sp = getRegister(tptr, SP_EL0);
/* check for alignment so we don't have to worry about accessing
* words that might be on two different pages */
if (!IS_ALIGNED(sp, seL4_WordSizeBits)) {
printf("SP not aligned\n");
return;
}
for (unsigned int i = 0; i < CONFIG_USER_STACK_TRACE_LENGTH; i++) {
word_t address = sp + (i * sizeof(word_t));
readWordFromVSpace_ret_t result = readWordFromVSpace(vspaceRoot,
address);
if (result.status == EXCEPTION_NONE) {
printf("0x%"SEL4_PRIx_word": 0x%"SEL4_PRIx_word"\n",
address, result.value);
} else {
printf("0x%"SEL4_PRIx_word": INVALID\n", address);
}
}
}
#endif /* CONFIG_PRINTING */
#if defined(CONFIG_KERNEL_LOG_BUFFER)
exception_t benchmark_arch_map_logBuffer(word_t frame_cptr)
{