libsel4: export seL4_IOPageTable{Index,Entry}Bits

This is useful for all x86 IOMMU work, which otherwise has
to duplicate the definitions of VTD_PT_INDEX_BITS in userspace
code. Follow the same pattern as many other existing code in
the libsel4 headers where the kernel depends on it.

Note we can't define seL4_IOPageTableBits in terms of Index + Entry
because the capDL tool does the c-preprocessor to make a YAML file
containing the constant, and it won't do evaluation.

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>

include/arch/x86/arch/object/structures.h

@@ -16,6 +16,7 @@
 #include <arch/machine/hardware.h>
 #include <arch/machine/registerset.h>
 #include <sel4/arch/constants.h>
+#include <sel4/sel4_arch/constants.h>
 
 enum tcb_arch_cnode_index {
 #ifdef CONFIG_VTX
@@ -54,9 +55,9 @@ typedef struct arch_tcb {
 #define VTD_CT_BITS       8
 #define VTD_CT_SIZE_BITS  (VTD_CT_BITS + VTD_CTE_SIZE_BITS)
 
-#define VTD_PTE_SIZE_BITS 3
+#define VTD_PTE_SIZE_BITS seL4_IOPageTableEntryBits
 #define VTD_PTE_PTR(r)    ((vtd_pte_t*)(r))
-#define VTD_PT_INDEX_BITS       9
+#define VTD_PT_INDEX_BITS seL4_IOPageTableIndexBits
 
 compile_assert(vtd_pt_size_sane, VTD_PT_INDEX_BITS + VTD_PTE_SIZE_BITS == seL4_IOPageTableBits)
 

libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h

@@ -38,12 +38,15 @@
 #define seL4_PageDirIndexBits 10
 #define seL4_VSpaceBits seL4_PageDirBits
 
-#define seL4_IOPageTableBits 12
 #define seL4_NumASIDPoolsBits 2
 #define seL4_ASIDPoolBits    12
 #define seL4_ASIDPoolIndexBits 10
 #define seL4_WordSizeBits 2
 
+#define seL4_IOPageTableBits      12
+#define seL4_IOPageTableIndexBits 9
+#define seL4_IOPageTableEntryBits 3
+
 #define seL4_HugePageBits    30 /* 1GB */
 #define seL4_PDPTBits         0
 #define seL4_LargePageBits    22 /* 4MB */
@@ -52,6 +55,7 @@
 SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits);
 SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits);
 SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits);
+SEL4_SIZE_SANITY(seL4_IOPageTableEntryBits, seL4_IOPageTableIndexBits, seL4_IOPageTableBits);
 #endif
 
 /* Previously large frames were explicitly assumed to be 4M. If not using

libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h

@@ -54,6 +54,9 @@
 #define seL4_VSpaceBits seL4_PML4Bits
 
 #define seL4_IOPageTableBits      12
+#define seL4_IOPageTableIndexBits 9
+#define seL4_IOPageTableEntryBits 3
+
 #define seL4_LargePageBits      21
 #define seL4_HugePageBits       30
 #define seL4_NumASIDPoolsBits    3
@@ -71,6 +74,7 @@ SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits)
 SEL4_SIZE_SANITY(seL4_PDPTEntryBits, seL4_PDPTIndexBits, seL4_PDPTBits);
 SEL4_SIZE_SANITY(seL4_PML4EntryBits, seL4_PML4IndexBits, seL4_PML4Bits);
 SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits);
+SEL4_SIZE_SANITY(seL4_IOPageTableEntryBits, seL4_IOPageTableIndexBits, seL4_IOPageTableBits);
 
 typedef enum {
     seL4_VMFault_IP,