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

remove slot_range_t

Browse source 
The RISC-V calling convention specifies that when a C function takes an
argument by value, the binary function should take the argument by
reference, if the value is larger than 2 pointer words.

For binary verification, we avoid implementing this aspect of the RISC-V
calling convention, by eliminating all such function arguments for
functions which are not inlined.

In this commit, we remove the `slot_range_t` structure altogether. For
the small number of functions which previously used this type, we unpack
the structure into three separate arguments.

Even though we are primarily concerned with RISC-V, we remove
`slot_range_t` arguments across all architectures.

Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
This commit is contained in:
Matthew Brecknell 2020-05-12 17:21:03 +10:00
parent b2ad98214d
commit 4520503c8a
5 changed files with 18 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
include/object/cnode.h
View file

@ -10,13 +10,6 @@
#include <api/failures.h>
#include <object/structures.h>
struct slot_range {
cte_t *cnode;
word_t offset;
word_t length;
};
typedef struct slot_range slot_range_t;
exception_t decodeCNodeInvocation(word_t invLabel, word_t length,
cap_t cap, word_t *buffer);
exception_t invokeCNodeRevoke(cte_t *destSlot);

3
include/object/objecttype.h
View file

@ -23,7 +23,8 @@ bool_t CONST sameObjectAs(cap_t cap_a, cap_t cap_b);
cap_t CONST updateCapData(bool_t preserve, word_t newData, cap_t cap);
cap_t CONST maskCapRights(seL4_CapRights_t seL4_CapRights, cap_t cap);
cap_t createObject(object_t t, void *regionBase, word_t, bool_t deviceMemory);
void createNewObjects(object_t t, cte_t *parent, slot_range_t slots,
void createNewObjects(object_t t, cte_t *parent,
cte_t *destCNode, word_t destOffset, word_t destLength,
void *regionBase, word_t userSize, bool_t deviceMemory);
#ifdef CONFIG_KERNEL_MCS
exception_t decodeInvocation(word_t invLabel, word_t length,

4
include/object/untyped.h
View file

@ -31,6 +31,6 @@ exception_t decodeUntypedInvocation(word_t invLabel, word_t length,
cte_t *slot, cap_t cap,
bool_t call, word_t *buffer);
exception_t invokeUntyped_Retype(cte_t *srcSlot, bool_t reset,
void *retypeBase, object_t newType,
word_t userSize, slot_range_t destSlots,
void *retypeBase, object_t newType, word_t userSize,
cte_t *destCNode, word_t destOffset, word_t destLength,
bool_t deviceMemory);

9
src/object/objecttype.c
View file

@ -583,7 +583,8 @@ cap_t createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceM
}
}
void createNewObjects(object_t t, cte_t *parent, slot_range_t slots,
void createNewObjects(object_t t, cte_t *parent,
cte_t *destCNode, word_t destOffset, word_t destLength,
void *regionBase, word_t userSize, bool_t deviceMemory)
{
word_t objectSize;
@ -593,19 +594,19 @@ void createNewObjects(object_t t, cte_t *parent, slot_range_t slots,
/* ghost check that we're visiting less bytes than the max object size */
objectSize = getObjectSize(t, userSize);
totalObjectSize = slots.length << objectSize;
totalObjectSize = destLength << objectSize;
/** GHOSTUPD: "(gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0
\<or> \<acute>totalObjectSize <= gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state, id)" */
/* Create the objects. */
nextFreeArea = regionBase;
for (i = 0; i < slots.length; i++) {
for (i = 0; i < destLength; i++) {
/* Create the object. */
/** AUXUPD: "(True, typ_region_bytes (ptr_val \<acute> nextFreeArea + ((\<acute> i) << unat (\<acute> objectSize))) (unat (\<acute> objectSize)))" */
cap_t cap = createObject(t, (void *)((word_t)nextFreeArea + (i << objectSize)), userSize, deviceMemory);
/* Insert the cap into the user's cspace. */
insertNewCap(parent, &slots.cnode[slots.offset + i], cap);
insertNewCap(parent, &destCNode[destOffset + i], cap);
/* Move along to the next region of memory. been merged into a formula of i */
}

19
src/object/untyped.c
View file

@ -34,7 +34,7 @@ exception_t decodeUntypedInvocation(word_t invLabel, word_t length, cte_t *slot,
lookupSlot_ret_t lu_ret;
word_t nodeSize;
word_t i;
slot_range_t slots;
cte_t *destCNode;
word_t freeRef, alignedFreeRef, objectSize, untypedFreeBytes;
word_t freeIndex;
bool_t deviceMemory;
@ -159,11 +159,9 @@ exception_t decodeUntypedInvocation(word_t invLabel, word_t length, cte_t *slot,
}
/* Ensure that the destination slots are all empty. */
slots.cnode = CTE_PTR(cap_cnode_cap_get_capCNodePtr(nodeCap));
slots.offset = nodeOffset;
slots.length = nodeWindow;
destCNode = CTE_PTR(cap_cnode_cap_get_capCNodePtr(nodeCap));
for (i = nodeOffset; i < nodeOffset + nodeWindow; i++) {
status = ensureEmptySlot(slots.cnode + i);
status = ensureEmptySlot(destCNode + i);
if (status != EXCEPTION_NONE) {
userError("Untyped Retype: Slot #%d in destination window non-empty.",
(int)i);
@ -231,7 +229,7 @@ exception_t decodeUntypedInvocation(word_t invLabel, word_t length, cte_t *slot,
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
return invokeUntyped_Retype(slot, reset,
(void *)alignedFreeRef, newType, userObjSize,
slots, deviceMemory);
destCNode, nodeOffset, nodeWindow, deviceMemory);
}
static exception_t resetUntypedCap(cte_t *srcSlot)
@ -275,7 +273,8 @@ static exception_t resetUntypedCap(cte_t *srcSlot)
exception_t invokeUntyped_Retype(cte_t *srcSlot,
bool_t reset, void *retypeBase,
object_t newType, word_t userSize,
slot_range_t destSlots, bool_t deviceMemory)
cte_t *destCNode, word_t destOffset, word_t destLength,
bool_t deviceMemory)
{
word_t freeRef;
word_t totalObjectSize;
@ -294,14 +293,14 @@ exception_t invokeUntyped_Retype(cte_t *srcSlot,
* Note that userSize is not necessarily the true size of the object in
* memory. In the case where newType is seL4_CapTableObject, the size is
* transformed by getObjectSize. */
totalObjectSize = destSlots.length << getObjectSize(newType, userSize);
totalObjectSize = destLength << getObjectSize(newType, userSize);
freeRef = (word_t)retypeBase + totalObjectSize;
srcSlot->cap = cap_untyped_cap_set_capFreeIndex(srcSlot->cap,
GET_FREE_INDEX(regionBase, freeRef));
/* Create new objects and caps. */
createNewObjects(newType, srcSlot, destSlots, retypeBase, userSize,
deviceMemory);
createNewObjects(newType, srcSlot, destCNode, destOffset, destLength,
retypeBase, userSize, deviceMemory);
return EXCEPTION_NONE;
}