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

SELFOUR-413: changes for verification

Browse source 
Avoid using ptrs to arrays at all

Another macrofull change brought to your by verification. This should
avoid nasty proofs about const pointers.
This commit is contained in:
Anna Lyons 2016-09-23 14:44:31 +10:00
parent 2fea9a0fe2
commit ed95f84a43
12 changed files with 113 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -122,11 +122,32 @@ enum messageSizes {
n_syscallMessage = 12,
};
#define EXCEPTION_MESSAGE \
{\
[seL4_UserException_FaultIP] = FaultInstruction,\
[seL4_UserException_SP] = SP,\
[seL4_UserException_CPSR] = CPSR\
}
#define SYSCALL_MESSAGE \
{\
[seL4_UnknownSyscall_R0] = R0,\
[seL4_UnknownSyscall_R1] = R1,\
[seL4_UnknownSyscall_R2] = R2,\
[seL4_UnknownSyscall_R3] = R3,\
[seL4_UnknownSyscall_R4] = R4,\
[seL4_UnknownSyscall_R5] = R5,\
[seL4_UnknownSyscall_R6] = R6,\
[seL4_UnknownSyscall_R7] = R7,\
[seL4_UnknownSyscall_FaultIP] = FaultInstruction,\
[seL4_UnknownSyscall_SP] = SP,\
[seL4_UnknownSyscall_LR] = LR,\
[seL4_UnknownSyscall_CPSR] = CPSR\
}
extern const register_t msgRegisters[];
extern const register_t frameRegisters[];
extern const register_t gpRegisters[];
extern const register_t exceptionMessage[];
extern const register_t syscallMessage[];
#ifdef CONFIG_HARDWARE_DEBUG_API
typedef struct debug_register_pair {

23
include/arch/x86/arch/32/mode/machine/registerset.h
View file

@ -69,11 +69,30 @@ enum messageSizes {
n_syscallMessage = 10
};
#define SYSCALL_MESSAGE \
{ \
[seL4_UnknownSyscall_EAX] = EAX,\
[seL4_UnknownSyscall_EBX] = EBX,\
[seL4_UnknownSyscall_ECX] = ECX,\
[seL4_UnknownSyscall_EDX] = EDX,\
[seL4_UnknownSyscall_ESI] = ESI,\
[seL4_UnknownSyscall_EDI] = EDI,\
[seL4_UnknownSyscall_EBP] = EBP,\
[seL4_UnknownSyscall_FaultIP] = FaultIP,\
[seL4_UnknownSyscall_SP] = ESP,\
[seL4_UnknownSyscall_FLAGS] = FLAGS\
}
#define EXCEPTION_MESSAGE \
{ \
[seL4_UserException_FaultIP] = FaultIP,\
[seL4_UserException_SP] = ESP,\
[seL4_UserException_FLAGS] = FLAGS\
}
extern const register_t msgRegisters[];
extern const register_t frameRegisters[];
extern const register_t gpRegisters[];
extern const register_t exceptionMessage[];
extern const register_t syscallMessage[];
#ifdef CONFIG_VTX
extern const register_t crExitRegs[];
#endif

31
include/arch/x86/arch/64/mode/machine/registerset.h
View file

@ -78,11 +78,38 @@ enum messageSizes {
n_syscallMessage = 18
};
#define SYSCALL_MESSAGE \
{ \
[seL4_UnknownSyscall_RAX] = RAX,\
[seL4_UnknownSyscall_RBX] = RBX,\
[seL4_UnknownSyscall_RCX] = RCX,\
[seL4_UnknownSyscall_RDX] = RDX,\
[seL4_UnknownSyscall_RSI] = RSI,\
[seL4_UnknownSyscall_RDI] = RDI,\
[seL4_UnknownSyscall_RBP] = RBP,\
[seL4_UnknownSyscall_R8] = R8,\
[seL4_UnknownSyscall_R9] = R9,\
[seL4_UnknownSyscall_R10] = R10,\
[seL4_UnknownSyscall_R11] = R11,\
[seL4_UnknownSyscall_R12] = R12,\
[seL4_UnknownSyscall_R13] = R13,\
[seL4_UnknownSyscall_R14] = R14,\
[seL4_UnknownSyscall_R15] = R15,\
[seL4_UnknownSyscall_FaultIP] = FaultIP,\
[seL4_UnknownSyscall_SP] = RSP,\
[seL4_UnknownSyscall_FLAGS] = FLAGS\
}
#define EXCEPTION_MESSAGE \
{ \
[seL4_UserException_FaultIP] = FaultIP,\
[seL4_UserException_SP] = RSP,\
[seL4_UserException_FLAGS] = FLAGS\
}
extern const register_t msgRegisters[];
extern const register_t frameRegisters[];
extern const register_t gpRegisters[];
extern const register_t exceptionMessage[];
extern const register_t syscallMessage[];
#define FPU_PADDING word_t padding[1];

9
include/machine/registerset.h
View file

@ -11,10 +11,19 @@
#ifndef __MACHINE_REGISTERSET_H
#define __MACHINE_REGISTERSET_H
#include <util.h>
#include <arch/types.h>
#include <arch/machine/registerset.h>
#include <arch/object/structures.h>
typedef enum {
MessageID_Syscall,
MessageID_Exception
} MessageID_t;
#define MAX_MSG_SIZE MAX(n_syscallMessage, n_exceptionMessage)
extern const register_t fault_messages[][MAX_MSG_SIZE] VISIBLE;
static inline void
setRegister(tcb_t *thread, register_t reg, word_t w)
{

1
include/util.h
View file

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

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

@ -35,7 +35,7 @@ seL4_getArchFault(seL4_MessageInfo_t tag)
case seL4_Fault_UserException:
return seL4_Fault_UserException_new(seL4_GetMR(seL4_UserException_FaultIP),
seL4_GetMR(seL4_UserException_SP),
seL4_GetMR(seL4_UserException_EFLAGS),
seL4_GetMR(seL4_UserException_FLAGS),
seL4_GetMR(seL4_UserException_Number),
seL4_GetMR(seL4_UserException_Code));
case seL4_Fault_VMFault:

2
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/types.bf
View file

@ -73,7 +73,7 @@ block UserException {
#ifdef CONFIG_HARDWARE_DEBUG_API
block DebugException {
padding 288
padding 224
field FaultIP 32
field ExceptionReason 32
field TriggerAddress 32

21
src/api/faults.c
View file

@ -73,12 +73,11 @@ setMRs_lookup_failure(tcb_t *receiver, word_t* receiveIPCBuffer,
}
static inline void
copyMRsFaultReply(tcb_t *sender, tcb_t *receiver, const register_t
message[], word_t length)
copyMRsFaultReply(tcb_t *sender, tcb_t *receiver, MessageID_t id, word_t length)
{
word_t i;
for (i = 0; i < MIN(length, n_msgRegisters); i++) {
register_t r = message[i];
register_t r = fault_messages[id][i];
word_t v = getRegister(sender, msgRegisters[i]);
setRegister(receiver, r, sanitiseRegister(r, v));
}
@ -87,7 +86,7 @@ copyMRsFaultReply(tcb_t *sender, tcb_t *receiver, const register_t
word_t *sendBuf = lookupIPCBuffer(false, sender);
if (sendBuf) {
for (; i < length; i++) {
register_t r = message[i];
register_t r = fault_messages[id][i];
word_t v = sendBuf[i + 1];
setRegister(receiver, r, sanitiseRegister(r, v));
}
@ -96,17 +95,17 @@ copyMRsFaultReply(tcb_t *sender, tcb_t *receiver, const register_t
}
static inline void
copyMRsFault(tcb_t *sender, tcb_t *receiver, const register_t message[],
copyMRsFault(tcb_t *sender, tcb_t *receiver, MessageID_t id,
word_t length, word_t *receiveIPCBuffer)
{
word_t i;
for (i = 0; i < MIN(length, n_msgRegisters); i++) {
setRegister(receiver, msgRegisters[i], getRegister(sender, message[i]));
setRegister(receiver, msgRegisters[i], getRegister(sender, fault_messages[id][i]));
}
if (receiveIPCBuffer) {
for (; i < length; i++) {
receiveIPCBuffer[i + 1] = getRegister(sender, message[i]);
receiveIPCBuffer[i + 1] = getRegister(sender, fault_messages[id][i]);
}
}
}
@ -125,11 +124,11 @@ handleFaultReply(tcb_t *receiver, tcb_t *sender)
return true;
case seL4_Fault_UnknownSyscall:
copyMRsFaultReply(sender, receiver, syscallMessage, MIN(length, n_syscallMessage));
copyMRsFaultReply(sender, receiver, MessageID_Syscall, MIN(length, n_syscallMessage));
return (label == 0);
case seL4_Fault_UserException:
copyMRsFaultReply(sender, receiver, exceptionMessage, MIN(length, n_exceptionMessage));
copyMRsFaultReply(sender, receiver, MessageID_Exception, MIN(length, n_exceptionMessage));
return (label == 0);
#ifdef CONFIG_HARDWARE_DEBUG_API
@ -198,7 +197,7 @@ setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer)
sender->tcbLookupFailure, seL4_CapFault_LookupFailureType);
case seL4_Fault_UnknownSyscall: {
copyMRsFault(sender, receiver, syscallMessage, n_syscallMessage,
copyMRsFault(sender, receiver, MessageID_Syscall, n_syscallMessage,
receiveIPCBuffer);
return setMR(receiver, receiveIPCBuffer, n_syscallMessage,
@ -206,7 +205,7 @@ setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer)
}
case seL4_Fault_UserException: {
copyMRsFault(sender, receiver, exceptionMessage,
copyMRsFault(sender, receiver, MessageID_Exception,
n_exceptionMessage, receiveIPCBuffer);
setMR(receiver, receiveIPCBuffer, n_exceptionMessage,
seL4_Fault_UserException_get_number(sender->tcbFault));

20
src/arch/arm/32/machine/registerset.c
View file

@ -23,23 +23,3 @@ const register_t gpRegisters[] = {
R2, R3, R4, R5, R6, R7, R14
};
const register_t exceptionMessage[] = {
[seL4_UserException_FaultIP] = FaultInstruction,
[seL4_UserException_SP] = SP,
[seL4_UserException_CPSR] = CPSR
};
const register_t syscallMessage[] = {
[seL4_UnknownSyscall_R0] = R0,
[seL4_UnknownSyscall_R1] = R1,
[seL4_UnknownSyscall_R2] = R2,
[seL4_UnknownSyscall_R3] = R3,
[seL4_UnknownSyscall_R4] = R4,
[seL4_UnknownSyscall_R5] = R5,
[seL4_UnknownSyscall_R6] = R6,
[seL4_UnknownSyscall_R7] = R7,
[seL4_UnknownSyscall_FaultIP] = FaultInstruction,
[seL4_UnknownSyscall_SP] = SP,
[seL4_UnknownSyscall_LR] = LR,
[seL4_UnknownSyscall_CPSR] = CPSR
};

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

@ -27,25 +27,6 @@ const register_t gpRegisters[] = {
TLS_BASE, FS, GS
};
const register_t exceptionMessage[] = {
[seL4_UserException_FaultIP] = FaultIP,
[seL4_UserException_SP] = ESP,
[seL4_UserException_FLAGS] = FLAGS
};
const register_t syscallMessage[] = {
[seL4_UnknownSyscall_EAX] = EAX,
[seL4_UnknownSyscall_EBX] = EBX,
[seL4_UnknownSyscall_ECX] = ECX,
[seL4_UnknownSyscall_EDX] = EDX,
[seL4_UnknownSyscall_ESI] = ESI,
[seL4_UnknownSyscall_EDI] = EDI,
[seL4_UnknownSyscall_EBP] = EBP,
[seL4_UnknownSyscall_FaultIP] = FaultIP,
[seL4_UnknownSyscall_SP] = ESP,
[seL4_UnknownSyscall_FLAGS] = FLAGS
};
#ifdef CONFIG_VTX
const register_t crExitRegs[] = {
EAX, ECX, EDX, EBX, ESP, EBP, ESI, EDI

1
src/machine/Makefile
View file

@ -11,3 +11,4 @@
DIRECTORIES += src/machine
C_SOURCES += src/machine/io.c
C_SOURCES += src/machine/registerset.c

17
src/machine/registerset.c Normal file
View file

@ -0,0 +1,17 @@
/*
* 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)
*/
#include <machine/registerset.h>
const register_t fault_messages[][MAX_MSG_SIZE] = {
[MessageID_Syscall] = SYSCALL_MESSAGE,
[MessageID_Exception] = EXCEPTION_MESSAGE
};