boot: document region types

Mention that it can be Ok for regions to overflow. State explicitly
that the end is exclusive.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

include/basic_types.h

@@ -46,19 +46,28 @@ enum _bool {
 };
 typedef word_t bool_t;
 
+/**
+ * A region [start..end) of kernel-virtual memory.
+ *
+ * Empty when start == end. If end < start, the region wraps around, that is,
+ * it represents the addresses in the set [start..-1] union [0..end). This is
+ * possible after address translation and fine for e.g. device memory regions.
+ */
 typedef struct region {
-    pptr_t start;
+    pptr_t start; /* inclusive */
-    pptr_t end;
+    pptr_t end;   /* exclusive */
 } region_t;
 
+/** A region [start..end) of physical memory addresses. */
 typedef struct p_region {
-    paddr_t start;
+    paddr_t start; /* inclusive */
-    paddr_t end;
+    paddr_t end;   /* exclusive */
 } p_region_t;
 
+/** A region [start..end) of user-virtual addresses. */
 typedef struct v_region {
-    vptr_t start;
+    vptr_t start; /* inclusive */
-    vptr_t end;
+    vptr_t end;   /* exclusive */
 } v_region_t;
 
 #define REG_EMPTY (region_t){ .start = 0, .end = 0 }

src/kernel/boot.c

@@ -764,7 +764,8 @@ BOOT_CODE static bool_t check_available_memory(word_t n_available,
             return false;
         }
 
-        /* Regions must be ordered and must not overlap. */
+        /* Regions must be ordered and must not overlap. Regions are [start..end),
+           so the == case is fine. Directly adjacent regions are allowed. */
         if ((i > 0) && (r->start < available[i - 1].end)) {
             printf("ERROR: memory region %d in wrong order\n", (int)i);
             return false;
@@ -791,7 +792,8 @@ BOOT_CODE static bool_t check_reserved_memory(word_t n_reserved,
             return false;
         }
 
-        /* Regions must be ordered and must not overlap. */
+        /* Regions must be ordered and must not overlap. Regions are [start..end),
+           so the == case is fine. Directly adjacent regions are allowed. */
         if ((i > 0) && (r->start < reserved[i - 1].end)) {
             printf("ERROR: reserved region %"SEL4_PRIu_word" in wrong order\n", i);
             return false;