Imagelibrary/seL4
1
0
Fork 1
mirror of https://github.com/seL4/seL4.git synced 2026-04-04 22:39:54 +00:00
Code Issues Packages Projects Releases Wiki Activity

boot: handle failure to find root server memory

Browse Source 
Previously, the case where there was no memory region large enough for
the root server objects was unhandled. The loop termination condition
(i>=0) was trivially true for all values of the loop variable. This
commit fixes the issue by making the loop variable signed, and adding a
failure case.

It also:
- adds a check for underflow in the calculation of the address to begin
  allocating root server objects,
- removes two redundant checks that were guaranteed to be true, and
- adds some clarifying comments.

Co-authored-by: Axel Heider <axelheider@gmx.de>
Signed-off-by: Matthew Brecknell <matthew@brecknell.net>
This commit is contained in:
Matthew Brecknell
2021-09-21 22:12:10 +10:00
parent f908fd8517
commit 577ca01803
1 changed files with 42 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files

54
src/kernel/boot.c
View File

@@ -861,7 +861,7 @@ BOOT_CODE bool_t init_freemem(word_t n_available, const p_region_t *available,
}
/* now try to fit the root server objects into a region */
word_t i = ARRAY_SIZE(ndks_boot.freemem) - 1;
int i = ARRAY_SIZE(ndks_boot.freemem) - 1;
if (!is_reg_empty(ndks_boot.freemem[i])) {
printf("Insufficient MAX_NUM_FREEMEM_REG\n");
return false;
@@ -874,20 +874,50 @@ BOOT_CODE bool_t init_freemem(word_t n_available, const p_region_t *available,
word_t size = calculate_rootserver_size(it_v_reg, extra_bi_size_bits);
word_t max = rootserver_max_size_bits(extra_bi_size_bits);
for (; i >= 0; i--) {
word_t next = i + 1;
pptr_t start = ROUND_DOWN(ndks_boot.freemem[i].end - size, max);
if (start >= ndks_boot.freemem[i].start) {
/* Invariant: both i and (i + 1) are valid indices in ndks_boot.freemem. */
assert(i < ARRAY_SIZE(ndks_boot.freemem) - 1);
/* Invariant; the region at index i is the current candidate.
* Invariant: regions 0 up to (i - 1), if any, are additional candidates.
* Invariant: region (i + 1) is empty. */
assert(is_reg_empty(ndks_boot.freemem[i + 1]));
/* Invariant: regions above (i + 1), if any, are empty or too small to use.
* Invariant: all non-empty regions are ordered, disjoint and unallocated. */
/* We make a fresh variable to index the known-empty region, because the
* SimplExportAndRefine verification test has poor support for array
* indices that are sums of variables and small constants. */
int empty_index = i + 1;
/* Try to take the top-most suitably sized and aligned chunk. */
pptr_t unaligned_start = ndks_boot.freemem[i].end - size;
pptr_t start = ROUND_DOWN(unaligned_start, max);
/* if unaligned_start didn't underflow, and start fits in the region,
* then we've found a region that fits the root server objects. */
if (unaligned_start <= ndks_boot.freemem[i].end
&& start >= ndks_boot.freemem[i].start) {
create_rootserver_objects(start, it_v_reg, extra_bi_size_bits);
if (i < ARRAY_SIZE(ndks_boot.freemem)) {
ndks_boot.freemem[next].end = ndks_boot.freemem[i].end;
ndks_boot.freemem[next].start = start + size;
}
/* There may be leftovers before and after the memory we used. */
/* Shuffle the after leftover up to the empty slot (i + 1). */
ndks_boot.freemem[empty_index] = (region_t) {
.start = start + size,
.end = ndks_boot.freemem[i].end
};
/* Leave the before leftover in current slot i. */
ndks_boot.freemem[i].end = start;
break;
} else if (i < ARRAY_SIZE(ndks_boot.freemem)) {
ndks_boot.freemem[next] = ndks_boot.freemem[i];
/* Regions i and (i + 1) are now well defined, ordered, disjoint,
* and unallocated, so we can return successfully. */
return true;
}
/* Region i isn't big enough, so shuffle it up to slot (i + 1),
* which we know is unused. */
ndks_boot.freemem[empty_index] = ndks_boot.freemem[i];
/* Now region i is unused, so make it empty to reestablish the invariant
* for the next iteration (when it will be slot i + 1). */
ndks_boot.freemem[i] = REG_EMPTY;
}
return true;
/* We didn't find a big enough region. */
printf("ERROR: no free memory region is big enough for root server "
"objects, need size/alignment of 2^%"SEL4_PRIu_word"\n", max);
return false;
}