capdl_spec.c: Remove seL4_libs dependencies from generated spec

[kent-mcleod]

The capdl_spec.c file is generated by capDL-tool and is compiled into the capdl-loader-app program to define the system that the loader will load. The file is supposed to only be a C-language representation of the capDL spec for a particular system. Currently, the header files required to compile this spec file introduces dependencies on a C library, and libraries from seL4/util_libs and seL4/sel4_libs including libsel4utils and libutils (and any libraries they depend on). The spec itself doesn't inherently require any type definitions other than what's provided by libsel4, and so it shouldn't require these additional dependencies.

The file generated by the capDL-tool only has the following header file dependencies: capdl_spec.h:

#include <capdl.h>
#include <sel4/sel4.h>

capdl.h:

#include <autoconf.h>
#include <capdl_loader_app/gen_config.h>

#include <sel4/types.h>

// These should all be removed 
#include <sel4utils/mapping.h>
#include <limits.h>
#include <stdbool.h>
#include <stdlib.h>
#include <utils/util.h>

These are the following non-libsel4 types in the capDL spec and how they can be replaced:

• uint8_t -> seL4_Uint8
• bool -> seL4_Bool
• uint64_t -> seL4_Uint64
• size_t -> seL4_Word (All usages of size_t are for non-negative integers and so unsigned long is safe)
• uint32_t -> seL4_Uint32
• seL4_ARCH_VMAttributes -> unsigned (The CDL_Cap struct definition uses an unsigned 3 bitfield definition already.)

In addition some constructions the spec uses can be manually defined:

#include <sel4/bootinfo_types.h>

#define BIT(x) (1lu << x)
#define PACKED       __attribute__((packed))

#if defined(CONFIG_ARCH_ARM)
#define CDL_VM_CacheEnabled seL4_ARM_Default_VMAttributes
#define CDL_VM_CacheDisabled 0

#elif defined (CONFIG_ARCH_X86)
#define CDL_VM_CacheEnabled seL4_X86_Default_VMAttributes
#define CDL_VM_CacheDisabled seL4_X86_CacheDisabled

#elif defined (CONFIG_ARCH_RISCV)
#define CDL_VM_CacheEnabled seL4_RISCV_Default_VMAttributes
#define CDL_VM_CacheDisabled 0

#else
#error "Unsupported architecture"
#endif

And a small update to the capDL-tool's C generation:

diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs
index 290b1c8..c058176 100644
--- a/capDL-tool/CapDL/PrintC.hs
+++ b/capDL-tool/CapDL/PrintC.hs
@@ -142,7 +142,7 @@ showCap objs (FrameCap id rights _ cached maybe_mapping) _ is_orig _ =
     ", .is_orig = " ++ is_orig ++
     ", .rights = " ++ showRights rights ++
     ", .vm_attribs = " ++
-          (if cached then "seL4_ARCH_Default_VMAttributes" else "CDL_VM_CacheDisabled") ++
+          (if cached then "CDL_VM_CacheEnabled" else "CDL_VM_CacheDisabled") ++
     ", .mapping_container_id = " ++
           (case maybe_mapping of
                Just (mapping_container, _) -> showObjID objs mapping_container;
@@ -216,7 +216,7 @@ showSlots objs obj_id (x:xs) irqNode cdt ms =
     where
         index = fst x
         slot = showCap objs (snd x) irqNode is_orig ms
-        is_orig = if Map.notMember (obj_id, index) cdt then "true" else "false"
+        is_orig = if Map.notMember (obj_id, index) cdt then "1" else "0"

 memberSlots :: Map ObjID Int -> ObjID -> CapMap Word -> IRQMap -> CDT -> ObjMap Word -> String
 memberSlots objs obj_id slots irqNode cdt ms =
@@ -451,7 +451,7 @@ showUntypedDerivations :: AllocationType -> Map ObjID Int -> CoverMap -> String
 showUntypedDerivations DynamicAlloc{} _ untypedCovers
   | all null (Map.elems untypedCovers) =
       ".num_untyped = 0," +++
-      ".untyped = NULL,"
+      ".untyped = 0,"
   | otherwise = error $
       "refusing to generate spec for dynamic allocation because the " ++
       "following untypeds already have children:\n" ++

[lsf37]

I'd be up for that. @corlewis any concerns from your side on this?

[corlewis]

Sorry, just noticed that I never replied. No concerns from my side and I think it is a good idea to minimise the dependencies.