nix: Rework mkSystem

Signed-off-by: Nick Spinale <[email protected]>
seL4 · Jun 24, 2024 · 72c6e8a · 72c6e8a
1 parent 2aea11a
commit 72c6e8a
Show file tree

Hide file tree

Showing 16 changed files with 237 additions and 265 deletions.
diff --git a/hacking/nix/scope/microkit/default.nix b/hacking/nix/scope/microkit/default.nix
@@ -120,30 +120,47 @@ let
         '';
       };
 
-  mkSystem = { searchPath, systemXML }:
+  mkLoader =
+    { systemXML
+    , searchPath
+    }:
     lib.fix (self: runCommand "system" {
-      passthru = rec {
+      passthru = {
         inherit systemXML;
-        loader = "${self}/loader.img";
-        links = [
-          { name = "pds"; path = searchPath; }
-          { name = "loader.img"; path = loader; }
-          { name = "report.txt"; path = "${self}/report.txt"; }
-          { name = "sdk/monitor.elf"; path = "${sdk}/board/${board}/${config}/elf/monitor.elf"; }
-          { name = "sdk/loader.elf"; path = "${sdk}/board/${board}/${config}/elf/loader.elf"; }
-        ];
+        image = "${self}/loader.img";
       };
     } ''
       mkdir $out
       MICROKIT_SDK=${sdk} \
         ${tool}/bin/microkit ${systemXML} \
-          --search-path ${searchPath} \
+          --search-path ${lib.concatStringsSep " " searchPath} \
           --board ${board} \
           --config ${config} \
           -o $out/loader.img \
           -r $out/report.txt
     '');
 
+  mkSystem =
+    { systemXML
+    , searchPath
+    , extraDebuggingLinks ? []
+    , passthru ? {}
+    }:
+    let
+      loader = mkLoader { inherit systemXML searchPath; };
+    in {
+      inherit loader;
+      loaderImage = loader.image;
+      debuggingLinks = [
+        { name = "loader.img"; path = loader; }
+        { name = "report.txt"; path = "${loader}/report.txt"; }
+        { name = "sdk/elf"; path = "${sdk}/board/${board}/${config}/elf"; }
+        { name = "sel4-symbolize-backtrace";
+          path = "${buildPackages.this.sel4-backtrace-cli}/bin/sel4-symbolize-backtrace";
+        }
+      ] ++ extraDebuggingLinks;
+    } // passthru;
+
 in rec {
   inherit
     sdk tool

diff --git a/hacking/nix/scope/plat-utils/default.nix b/hacking/nix/scope/plat-utils/default.nix
@@ -10,7 +10,7 @@
   qemu = callPackage ./qemu {};
   rpi4 = callPackage ./rpi4 {};
 
-  composeInstanceForPlatformAttrs = a: b: {
+  composePlatformExtensions = a: b: {
     attrs = a.attrs // b.attrs;
     links = a.links ++ b.links;
   };

diff --git a/hacking/nix/scope/plat-utils/qemu/default.nix b/hacking/nix/scope/plat-utils/qemu/default.nix
@@ -22,7 +22,7 @@ let
 
 in rec {
 
-  automateQemuSimple = { simulate, timeout }:
+  automateQEMUSimple = { simulate, timeout }:
     let
       py = buildPackages.python3.withPackages (pkgs: [
         pkgs.pexpect
@@ -35,24 +35,24 @@ in rec {
         ${py}/bin/python3 ${./automate_simple.py} --simulate ${simulate} --timeout ${toString timeout}
       '';
 
-  mkMkInstanceForPlatform =
-    { mkQemuCmd
-    , platformRequiresLoader ? true
+  mkMkPlatformSystemExtension =
+    { mkQEMUCmd
     }:
 
-    { rootTask ? null
-    , loader ? null
+    { worldConfig
+    , rootTaskImage ? null
+    , loaderImage ? null
+    , extraQEMUArgs ? []
     , canAutomateSimply ? false
     , simpleAutomationParams ? if canAutomateSimply then {} else null
-    , extraQemuArgs ? []
     }:
 
     let
-      qemuCmd = mkQemuCmd (if platformRequiresLoader then loader else rootTask);
+      qemuCmd = mkQEMUCmd (if worldConfig.platformRequiresLoader then loaderImage else rootTaskImage);
 
       simulate = writeScript "run.sh" ''
         #!${buildPackages.runtimeShell}
-        exec ${lib.concatStringsSep " " (qemuCmd ++ extraQemuArgs)} "$@"
+        exec ${lib.concatStringsSep " " (qemuCmd ++ extraQEMUArgs)} "$@"
       '';
 
       elaboratedSimpleAutomationParams =
@@ -63,7 +63,7 @@ in rec {
       automate =
         if elaboratedSimpleAutomationParams == null
         then null
-        else automateQemuSimple {
+        else automateQEMUSimple {
           inherit simulate;
           inherit (elaboratedSimpleAutomationParams) timeout;
         };

diff --git a/hacking/nix/scope/plat-utils/rpi4/default.nix b/hacking/nix/scope/plat-utils/rpi4/default.nix
@@ -89,20 +89,21 @@ let
 
   defaultBootLinks = mkBootLinks {};
 
-  mkInstanceForPlatform =
-    { loader
-    , rootTask
+  mkPlatformSystemExtension =
+    { worldConfig
+    , loaderImage
+    , extraQEMUPlatformArgs ? {}
     , bootLinksExtraCommands ? ""
     , simpleAutomationParams ? null # TODO
     }:
     let
       boot = mkBootLinks {
-        image = loader;
+        image = loaderImage;
         extraCommands = bootLinksExtraCommands;
       };
       bootCopied = mkBootCopied boot;
-      qemu = platUtils.qemu.mkMkInstanceForPlatform {
-        mkQemuCmd = loader: [
+      qemu = platUtils.qemu.mkMkPlatformSystemExtension {
+        mkQEMUCmd = loader: [
           "${pkgsBuildBuild.this.qemuForSeL4}/bin/qemu-system-${if hostPlatform.is32bit then "arm" else "aarch64"}"
             "-smp" "4"
             "-m" "size=2048"
@@ -112,10 +113,10 @@ let
             "-serial" "mon:stdio"
             "-kernel" loader
         ];
-      } {
-        inherit loader rootTask;
-      };
-    in platUtils.composeInstanceForPlatformAttrs qemu (rec {
+      } ({
+        inherit worldConfig loaderImage;
+      } // extraQEMUPlatformArgs);
+    in platUtils.composePlatformExtensions qemu (rec {
       attrs = {
         inherit boot bootCopied;
       };
@@ -131,6 +132,6 @@ in {
     firmware
     uBoot
     defaultBootLinks
-    mkInstanceForPlatform
+    mkPlatformSystemExtension
   ;
 }
diff --git a/hacking/nix/scope/world/capdl/dummy-capdl-spec.nix b/hacking/nix/scope/world/capdl/dummy-capdl-spec.nix
@@ -7,15 +7,13 @@
 { lib, emptyDirectory, linkFarm, writeText }:
 
 {
-  passthru = {
-    spec = writeText "x.cdl" ''
-      arch aarch64
+  cdl = writeText "x.cdl" ''
+    arch aarch64
 
-      objects {
-        foo = notification
-      }
-      caps {}
-    '';
-    fill = emptyDirectory;
-  };
+    objects {
+      foo = notification
+    }
+    caps {}
+  '';
+  fill = emptyDirectory;
 }
diff --git a/hacking/nix/scope/world/capdl/mk-capdl-initializer-with-spec.nix b/hacking/nix/scope/world/capdl/mk-capdl-initializer-with-spec.nix
@@ -14,11 +14,11 @@
 , sel4-capdl-initializer
 }:
 
-{ spec, fill }:
+{ cdl, fill }:
 
 let
   json = serializeCapDLSpec {
-    inherit spec;
+    inherit cdl;
   };
 
 in lib.fix (self: runCommand "sel4-capdl-initializer-with-spec" {
@@ -28,7 +28,7 @@ in lib.fix (self: runCommand "sel4-capdl-initializer-with-spec" {
   ];
 
   passthru = {
-    inherit spec json fill;
+    inherit cdl json fill;
     elf = self;
     split = {
       full = sel4-capdl-initializer.elf;

diff --git a/hacking/nix/scope/world/capdl/mk-simple-composition-capdl-spec.nix b/hacking/nix/scope/world/capdl/mk-simple-composition-capdl-spec.nix
@@ -66,8 +66,8 @@ lib.fix (self: runCommand "manifest" {
 
   passthru = {
     config = augmentedConfig;
-    cdl = {
-      spec = "${self}/spec.cdl";
+    specAttrs = {
+      cdl = "${self}/spec.cdl";
       fill = "${self}/links";
     };
   };

diff --git a/hacking/nix/scope/world/capdl/mk-small-capdl-initializer.nix b/hacking/nix/scope/world/capdl/mk-small-capdl-initializer.nix
@@ -14,11 +14,11 @@
 , mkSeL4RustTargetTriple
 }:
 
-{ spec, fill }:
+{ cdl, fill }:
 
 let
   json = serializeCapDLSpec {
-    inherit spec;
+    inherit cdl;
   };
 
 in mkTask {
@@ -48,7 +48,7 @@ in mkTask {
       CAPDL_EMBED_FRAMES = 1;
 
       passthru = (super.passthru or {}) // {
-        inherit spec json fill;
+        inherit cdl json fill;
       };
     });
   });

diff --git a/hacking/nix/scope/world/capdl/serialize-capdl-spec.nix b/hacking/nix/scope/world/capdl/serialize-capdl-spec.nix
@@ -10,7 +10,7 @@
 , sources
 }:
 
-{ spec }:
+{ cdl }:
 
 let
   exe = "parse-capDL";
@@ -25,5 +25,5 @@ runCommand "spec.json" {
     # (import <nixpkgs> {}).stack
   ];
 } ''
-  ${exe} --object-sizes=${objectSizes} --json=$out ${spec}
+  ${exe} --object-sizes=${objectSizes} --json=$out ${cdl}
 ''
diff --git a/hacking/nix/scope/world/default.nix b/hacking/nix/scope/world/default.nix
@@ -6,7 +6,8 @@
 
 { lib
 , hostPlatform
-, runCommand, runCommandCC
+, buildPackages
+, runCommand, runCommandCC, linkFarm, writeScript
 , jq
 , symlinkToRegularFile
 , crateUtils
@@ -23,7 +24,7 @@ let
     , microkitConfig ? null
     , canSimulate ? false
     , platformRequiresLoader ? true
-    , mkInstanceForPlatform ? _: { attrs = {}; links = []; }
+    , mkPlatformSystemExtension ? _: { attrs = {}; links = []; }
     , ...
     } @ args:
     args // {
@@ -34,7 +35,7 @@ let
         microkitConfig
         canSimulate
         platformRequiresLoader
-        mkInstanceForPlatform
+        mkPlatformSystemExtension
       ;
     };
 in
@@ -125,8 +126,26 @@ self: with self;
   mkSimpleCompositionCapDLSpec = callPackage ./capdl/mk-simple-composition-capdl-spec.nix {};
   mkCapDLInitializerWithSpec = callPackage ./capdl/mk-capdl-initializer-with-spec.nix {};
 
-  # mkCapDLInitializer = mkSmallCapDLInitializer;
-  mkCapDLInitializer = mkCapDLInitializerWithSpec;
+  mkCapDLInitializer =
+    { spec ? null
+    , specAttrs ? spec.specAttrs
+    , small ? false
+    , extraDebuggingLinks ? []
+    }:
+
+    lib.fix (self:
+      (if small then mkSmallCapDLInitializer else mkCapDLInitializerWithSpec) spec.specAttrs // {
+        inherit spec;
+        debuggingLinks = [
+          { name = "spec.cdl"; path = spec.specAttrs.cdl; }
+          { name = "fill"; path = spec.specAttrs.fill; }
+        ] ++ lib.optionals (spec != null) [
+          { name = "spec"; path = spec; }
+        ] ++ lib.optionals (!small) [
+          { name = "initializer.full.elf"; path = self.split.full; }
+        ] ++ extraDebuggingLinks;
+      }
+    );
 
   sel4-kernel-loader = callPackage ./sel4-kernel-loader.nix {
     inherit (worldConfig) kernelLoaderConfig;
@@ -136,9 +155,61 @@ self: with self;
     app = appELF;
   };
 
-  inherit (callPackage ./mk-instance.nix {})
-    mkInstance mkMicrokitInstance mkSimpleCompositionCapDLRootTask
-  ;
+  mkSystem =
+    { rootTask
+    , extraDebuggingLinks ? []
+    , passthru ? {}
+    }:
+    let
+      loader =
+        assert worldConfig.platformRequiresLoader;
+        mkSeL4KernelLoaderWithPayload {
+          appELF = rootTask.elf;
+        };
+
+      symbolizeRootTaskBacktrace = writeScript "x.sh" ''
+        #!${buildPackages.runtimeShell}
+        exec ${buildPackages.this.sel4-backtrace-cli}/bin/sel4-symbolize-backtrace -f ${rootTask.elf} "$@"
+      '';
+    in {
+      inherit loader rootTask;
+      rootTaskImage = rootTask.elf;
+      loaderImage = loader.elf;
+      debuggingLinks = [
+        { name = "kernel.elf"; path = "${seL4ForBoot}/bin/kernel.elf"; }
+        { name = "root-task.elf"; path = rootTask.elf; }
+        { name = "symbolize-root-task-backtrace"; path = symbolizeRootTaskBacktrace; }
+        { name = "sel4-symbolize-backtrace";
+          path = "${buildPackages.this.sel4-backtrace-cli}/bin/sel4-symbolize-backtrace";
+        }
+      ] ++ lib.optionals worldConfig.platformRequiresLoader [
+        { name = "loader.elf"; path = loader.elf; }
+        { name = "loader.debug.elf"; path = loader.split.full; }
+      ] ++ (rootTask.debuggingLinks or []) ++ extraDebuggingLinks;
+    } // passthru;
+
+  callPlatform =
+    { system
+    , extraPlatformArgs ? {}
+    , extraDebuggingLinks ? []
+    , ...
+    } @ args:
+    let
+      platformSystemExtension = worldConfig.mkPlatformSystemExtension ({
+        inherit worldConfig;
+      } // (
+        if worldConfig.platformRequiresLoader
+        then { inherit (system) loaderImage; }
+        else { inherit (system) rootTaskImage; }
+      ) // extraPlatformArgs);
+    in {
+      links = linkFarm "links" (
+        system.debuggingLinks ++ platformSystemExtension.links
+      );
+    }
+    // platformSystemExtension.attrs
+    // builtins.removeAttrs system [ "debuggingLinks" ]
+    // builtins.removeAttrs args [ "extraPlatformArgs" "extraDebuggingLinks" ];
 
   instances = callPackage ./instances {};