seL4 · nspin · Jun 24, 2024 · Jun 21, 2024 · Jun 21, 2024 · Jun 22, 2024
@@ -34,7 +34,6 @@ let
   fenixRev = "9af557bccdfa8fb6a425661c33dbae46afef0afa";
   fenixSource = fetchTarball "https://github.com/nix-community/fenix/archive/${fenixRev}.tar.gz";
   fenix = import fenixSource {};
-
 in
 
 superCallPackage ../rust-utils {} self //
@@ -228,7 +227,11 @@ superCallPackage ../rust-utils {} self //
 
   ### worlds
 
-  mkWorld = unelaboratedWorldConfig: lib.makeScope newScope (callPackage ./world {} unelaboratedWorldConfig);
+  overrideWorldScope = self: super: {};
+
+  mkWorldFrom = newScope: unelaboratedWorldConfig: (lib.makeScope newScope (callPackage ./world {} unelaboratedWorldConfig)).overrideScope' overrideWorldScope;
+
+  mkWorld = mkWorldFrom newScope;
 
   worlds = (callPackage ./worlds.nix {})."${seL4Arch}";
 

@@ -44,13 +44,6 @@ let
     '';
   };
 
-  vendoredLockfile = vendorLockfile {
-    inherit rustToolchain;
-    lockfile = microkitSource + "/tool/microkit/Cargo.lock";
-  };
-
-  cargoConfigFile = toTOMLFile "config.toml" vendoredLockfile.configFragment;
-
   sdk = stdenv.mkDerivation {
     name = "microkit-sdk-without-tool";
 
@@ -90,100 +83,87 @@ let
     '';
   };
 
-  tool = stdenv.mkDerivation {
-    name = "microkit-sdk-just-tool";
+  tool =
+    let
+      vendoredLockfile = vendorLockfile {
+        inherit rustToolchain;
+        lockfile = microkitSource + "/tool/microkit/Cargo.lock";
+      };
 
-    src = lib.cleanSource (microkitSource + "/tool/microkit");
+      cargoConfigFile = toTOMLFile "config.toml" vendoredLockfile.configFragment;
 
-    nativeBuildInputs = [
-      rustToolchain
-    ];
+    in
+      stdenv.mkDerivation {
+        name = "microkit-sdk-just-tool";
 
-    depsBuildBuild = [
-      buildPackages.stdenv.cc
-    ];
+        src = lib.cleanSource (microkitSource + "/tool/microkit");
 
-    dontInstall = true;
-    dontFixup = true;
+        nativeBuildInputs = [
+          rustToolchain
+        ];
 
-    configurePhase = ''
-      d=.cargo
-      mkdir $d
-      cp ${cargoConfigFile} $d/config.toml
-    '';
+        depsBuildBuild = [
+          buildPackages.stdenv.cc
+        ];
 
-    buildPhase = ''
-      cargo build -Z unstable-options --frozen --out-dir $out/bin
-    '';
-  };
+        dontInstall = true;
+        dontFixup = true;
 
-  mkSystem = { searchPath, systemXML }:
-    lib.fix (self: runCommand "system" {
-      MICROKIT_SDK = sdk;
-      MICROKIT_BOARD = board;
-      MICROKIT_CONFIG = config;
+        configurePhase = ''
+          d=.cargo
+          mkdir $d
+          cp ${cargoConfigFile} $d/config.toml
+        '';
 
-      nativeBuildInputs = [
-        python3Packages.sel4-deps
-      ];
+        buildPhase = ''
+          cargo build -Z unstable-options --frozen --config ${cargoConfigFile} --out-dir $out/bin
+        '';
+      };
 
-      passthru = rec {
+  mkLoader =
+    { systemXML
+    , searchPath
+    }:
+    lib.fix (self: runCommand "system" {
+      passthru = {
         inherit systemXML;
-        loader = "${self}/loader.img";
-        links = [
-          { name = "pds"; path = searchPath; }
-          { name = "loader.elf"; 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
-      ${tool}/bin/microkit ${systemXML} \
-        --search-path ${searchPath} \
-        --board $MICROKIT_BOARD \
-        --config $MICROKIT_CONFIG \
-        -o $out/loader.img \
-        -r $out/report.txt
+      MICROKIT_SDK=${sdk} \
+        ${tool}/bin/microkit ${systemXML} \
+          --search-path ${lib.concatStringsSep " " searchPath} \
+          --board ${board} \
+          --config ${config} \
+          -o $out/loader.img \
+          -r $out/report.txt
     '');
 
-  exampleSource = microkitSource + "/example/${board}/hello";
-
-  examplePDs = stdenv.mkDerivation {
-    name = "example";
-
-    src = exampleSource;
-
-    MICROKIT_SDK = sdk;
-    MICROKIT_BOARD = board;
-    MICROKIT_CONFIG = config;
-
-    MICROKIT_TOOL = "${tool}/bin/microkit";
-
-    dontConfigure = true;
-    dontFixup = true;
-
-    buildPhase = ''
-      mkdir build
-      make BUILD_DIR=build
-    '';
-
-    installPhase = ''
-      mkdir $out
-      mv build/hello.elf $out
-    '';
-  };
-
-  example = assert board == "qemu_virt_aarch64"; mkSystem {
-    searchPath = examplePDs;
-    systemXML = exampleSource + "/hello.system";
-  };
+  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
     mkSystem
-    example
   ;
 }
@@ -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;
   };

@@ -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;
         };

@@ -39,28 +39,32 @@ let
   uBootBin = "${uBoot}/u-boot.bin";
 
   imageAddr = "0x30000000";
+  defaultBootCmd = "load mmc 0:1 ${imageAddr} /image.elf; bootelf -p ${imageAddr}";
 
-  uBootEnvTxt = writeText "uboot.env.txt" ''
+  uBootEnvTxt = { bootCmd }: writeText "uboot.env.txt" ''
     bootdelay=0
-    bootcmd=load mmc 0:1 ${imageAddr} /image.elf; bootelf -p ${imageAddr}"
+    bootcmd=${bootCmd}"
     autostart=1
   '';
 
-  uBootEnv = runCommand "uboot.env" {
-    nativeBuildInputs = [
-      ubootTools
-    ];
-  } ''
-    mkenvimage \
-      -s 0x4000 \
-      -o $out \
-      ${uBootEnvTxt}
-  '';
+  uBootEnv = { bootCmd }:
+    assert lib.stringLength bootCmd < 3 * 4096; # conservative
+    runCommand "uboot.env" {
+      nativeBuildInputs = [
+        ubootTools
+      ];
+    } ''
+      mkenvimage \
+        -s 0x4000 \
+        -o $out \
+        ${uBootEnvTxt { inherit bootCmd; }}
+    '';
 
   kernelFileName = "kernel${if hostPlatform.is32bit then "7l" else "8"}.img";
 
   mkBootLinks =
     { image ? null
+    , bootCmd ? defaultBootCmd
     , extraCommands ? ""
     }:
     runCommand "boot" {} ''
@@ -74,7 +78,7 @@ let
       rm $out/kernel*.img
       ln -s ${uBootBin} $out/${kernelFileName}
 
-      ln -s ${uBootEnv} $out/uboot.env
+      ln -s ${uBootEnv { inherit bootCmd; }} $out/uboot.env
 
       ${lib.optionalString (image != null) ''
         ln -s ${image} $out/image.elf
@@ -89,18 +93,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"
@@ -110,10 +117,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;
       };
@@ -129,6 +136,7 @@ in {
     firmware
     uBoot
     defaultBootLinks
-    mkInstanceForPlatform
+    mkBootLinks
+    mkPlatformSystemExtension
   ;
 }
@@ -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;
 }