Add support for Microkit on riscv64

crates/sel4-generate-target-specs/src/main.rs

@@ -186,7 +186,7 @@ impl Arch {
     }
 
     fn microkit_support(&self) -> bool {
-        matches!(self, Self::AArch64)
+        matches!(self, Self::AArch64 | Self::RiscV64(_))
     }
 
     fn unwinding_support(&self) -> bool {

hacking/nix/scope/microkit/default.nix

@@ -68,6 +68,13 @@ let
     dontConfigure = true;
     dontFixup = true;
 
+    # TODO make PR upstream to improve flexibility
+    postPatch = ''
+      substituteInPlace build_sdk.py --replace \
+        '"riscv64-unknown-elf-"' \
+        '"${stdenv.cc.targetPrefix}"'
+    '';
+
     buildPhase = ''
       python3 build_sdk.py \
         --sel4=${kernelSourcePatched} \

hacking/nix/scope/sources.nix

@@ -55,14 +55,14 @@ in rec {
 
     rust-microkit = fetchGit {
       url = "https://github.com/coliasgroup/seL4.git";
-      rev = "0cdbffec9cf6b4c7c9c57971cbee5a24a70c8fd0"; # branch "rust-microkit"
+      rev = "4cae30a6ef166a378d4d23697b00106ce7e4e76f"; # branch "rust-microkit"
       local = localRoot + "/seL4";
     };
   };
 
   microkit = fetchGit {
     url = "https://github.com/coliasgroup/microkit.git";
-    rev = "9d5c0957720ae1093ab1a3cc9e15fc926dbe0431"; # branch "rust-nix"
+    rev = "2492fa64b2e4930e5f3beb77be8914e5f35a2746"; # branch "rust-nix"
     local = localRoot + "/microkit";
   };
 

hacking/nix/scope/world/instances/microkit/default.nix

@@ -4,7 +4,7 @@
 # SPDX-License-Identifier: BSD-2-Clause
 #
 
-{ lib, stdenv
+{ lib, stdenv, hostPlatform
 , buildPackages, pkgsBuildBuild
 , linkFarm, symlinkJoin, writeText, runCommand, runCommandCC
 , callPackage
@@ -62,7 +62,7 @@ in {
         }
     );
 
-    banscii = maybe isMicrokit (callPackage ./banscii {
+    banscii = maybe (isMicrokit && seL4Config.PLAT == "qemu-arm-virt") (callPackage ./banscii {
       inherit canSimulate;
       inherit mkPD;
     });
@@ -106,7 +106,7 @@ in {
         }
     );
 
-    reset = maybe isMicrokit (
+    reset = maybe (isMicrokit && hostPlatform.isAarch64) (
       let
         pd = rec {
           orig = mkPD rec {

hacking/nix/scope/worlds.nix

@@ -269,13 +269,27 @@ in rec {
           mk =
             { mcs ? false
             , smp ? false
+            , mkLoaderQEMUArgs ? loader: [ "-kernel" loader ]
+
+            , debugBuild ? null
+
+            , isMicrokit ? false
+            , microkitBoard ? null
+            , microkitConfig ? if debugBuild == null || debugBuild then "debug" else "release"
+
+            , extraQEMUArgs ? []
             }:
             let
               numCores = if smp then "2" else "1";
-              qemuMemory = "3072";
+              qemuMemory = "2048";
             in
               mkWorld {
-                inherit kernelLoaderConfig microkitConfig;
+                inherit kernelLoaderConfig;
+                inherit isMicrokit;
+                microkitConfig = {
+                  board = microkitBoard;
+                  config = microkitConfig;
+                };
                 kernelConfig = kernelConfigCommon // {
                   QEMU_MEMORY = mkString qemuMemory;
                   KernelArch = mkString "riscv";
@@ -292,9 +306,8 @@ in rec {
                       "-cpu" "rv64" "-smp" numCores "-m" "size=${qemuMemory}"
                       "-nographic"
                       "-serial" "mon:stdio"
-                      "-kernel" loader
                       # "-d" "unimp,guest_errors"
-                  ];
+                  ] ++ mkLoaderQEMUArgs loader ++ extraQEMUArgs;
                 };
               };
         in rec {
@@ -307,6 +320,11 @@ in rec {
             smp = mk { mcs = false; smp = true; };
             nosmp = mk { mcs = false; smp = false; };
           };
+          microkit = mk {
+            mcs = true;
+            isMicrokit = true;
+            microkitBoard = "qemu_virt_riscv64";
+          };
         };
 
       spike = mkWorld {

hacking/nix/top-level/default.nix

@@ -19,6 +19,7 @@ in {
     pkgs.host.aarch64.none.this.worlds.qemu-arm-virt.microkit
     pkgs.host.aarch32.none.this.worlds.default
     pkgs.host.riscv64.default.none.this.worlds.default
+    pkgs.host.riscv64.default.none.this.worlds.qemu-riscv-virt.microkit
     pkgs.host.riscv32.default.none.this.worlds.default
     pkgs.host.x86_64.none.this.worlds.default
   ];

support/targets/riscv64gc-sel4-microkit-minimal.json

@@ -0,0 +1,31 @@
+{
+  "arch": "riscv64",
+  "code-model": "medium",
+  "cpu": "generic-rv64",
+  "crt-objects-fallback": "false",
+  "data-layout": "e-m:e-p:64:64-i64:64-i128:128-n32:64-S128",
+  "eh-frame-header": false,
+  "emit-debug-gdb-scripts": false,
+  "env": "sel4",
+  "exe-suffix": ".elf",
+  "features": "+m,+a,+f,+d,+c",
+  "link-script": "__sel4_ipc_buffer_obj = (__ehdr_start & ~(4096 - 1)) - 4096;",
+  "linker": "rust-lld",
+  "linker-flavor": "gnu-lld",
+  "llvm-abiname": "lp64d",
+  "llvm-target": "riscv64",
+  "max-atomic-width": 64,
+  "metadata": {
+    "description": "Bare RISC-V (RV64IMAFDC ISA)",
+    "host_tools": false,
+    "std": false,
+    "tier": 2
+  },
+  "panic-strategy": "abort",
+  "relocation-model": "static",
+  "supported-sanitizers": [
+    "shadow-call-stack",
+    "kernel-address"
+  ],
+  "target-pointer-width": "64"
+}

support/targets/riscv64gc-sel4-microkit-resettable-minimal.json

@@ -0,0 +1,31 @@
+{
+  "arch": "riscv64",
+  "code-model": "medium",
+  "cpu": "generic-rv64",
+  "crt-objects-fallback": "false",
+  "data-layout": "e-m:e-p:64:64-i64:64-i128:128-n32:64-S128",
+  "eh-frame-header": false,
+  "emit-debug-gdb-scripts": false,
+  "env": "sel4",
+  "exe-suffix": ".elf",
+  "features": "+m,+a,+f,+d,+c",
+  "link-script": "SECTIONS {\n    .persistent : {\n        *(.persistent .persistent.*)\n    }\n} INSERT BEFORE .data;\n\nASSERT(DEFINED(_reset), \"_reset is not defined\")\n\nENTRY(_reset)\n__sel4_ipc_buffer_obj = (__ehdr_start & ~(4096 - 1)) - 4096;",
+  "linker": "rust-lld",
+  "linker-flavor": "gnu-lld",
+  "llvm-abiname": "lp64d",
+  "llvm-target": "riscv64",
+  "max-atomic-width": 64,
+  "metadata": {
+    "description": "Bare RISC-V (RV64IMAFDC ISA)",
+    "host_tools": false,
+    "std": false,
+    "tier": 2
+  },
+  "panic-strategy": "abort",
+  "relocation-model": "static",
+  "supported-sanitizers": [
+    "shadow-call-stack",
+    "kernel-address"
+  ],
+  "target-pointer-width": "64"
+}

support/targets/riscv64gc-sel4-microkit-resettable.json

@@ -0,0 +1,30 @@
+{
+  "arch": "riscv64",
+  "code-model": "medium",
+  "cpu": "generic-rv64",
+  "crt-objects-fallback": "false",
+  "data-layout": "e-m:e-p:64:64-i64:64-i128:128-n32:64-S128",
+  "emit-debug-gdb-scripts": false,
+  "env": "sel4",
+  "exe-suffix": ".elf",
+  "features": "+m,+a,+f,+d,+c",
+  "has-thread-local": true,
+  "link-script": "SECTIONS {\n    .persistent : {\n        *(.persistent .persistent.*)\n    }\n} INSERT BEFORE .data;\n\nASSERT(DEFINED(_reset), \"_reset is not defined\")\n\nENTRY(_reset)\n__sel4_ipc_buffer_obj = (__ehdr_start & ~(4096 - 1)) - 4096;",
+  "linker": "rust-lld",
+  "linker-flavor": "gnu-lld",
+  "llvm-abiname": "lp64d",
+  "llvm-target": "riscv64",
+  "max-atomic-width": 64,
+  "metadata": {
+    "description": "Bare RISC-V (RV64IMAFDC ISA)",
+    "host_tools": false,
+    "std": false,
+    "tier": 2
+  },
+  "relocation-model": "static",
+  "supported-sanitizers": [
+    "shadow-call-stack",
+    "kernel-address"
+  ],
+  "target-pointer-width": "64"
+}

support/targets/riscv64gc-sel4-microkit.json

@@ -0,0 +1,30 @@
+{
+  "arch": "riscv64",
+  "code-model": "medium",
+  "cpu": "generic-rv64",
+  "crt-objects-fallback": "false",
+  "data-layout": "e-m:e-p:64:64-i64:64-i128:128-n32:64-S128",
+  "emit-debug-gdb-scripts": false,
+  "env": "sel4",
+  "exe-suffix": ".elf",
+  "features": "+m,+a,+f,+d,+c",
+  "has-thread-local": true,
+  "link-script": "__sel4_ipc_buffer_obj = (__ehdr_start & ~(4096 - 1)) - 4096;",
+  "linker": "rust-lld",
+  "linker-flavor": "gnu-lld",
+  "llvm-abiname": "lp64d",
+  "llvm-target": "riscv64",
+  "max-atomic-width": 64,
+  "metadata": {
+    "description": "Bare RISC-V (RV64IMAFDC ISA)",
+    "host_tools": false,
+    "std": false,
+    "tier": 2
+  },
+  "relocation-model": "static",
+  "supported-sanitizers": [
+    "shadow-call-stack",
+    "kernel-address"
+  ],
+  "target-pointer-width": "64"
+}

support/targets/riscv64imac-sel4-microkit-minimal.json

@@ -0,0 +1,30 @@
+{
+  "arch": "riscv64",
+  "code-model": "medium",
+  "cpu": "generic-rv64",
+  "crt-objects-fallback": "false",
+  "data-layout": "e-m:e-p:64:64-i64:64-i128:128-n32:64-S128",
+  "eh-frame-header": false,
+  "emit-debug-gdb-scripts": false,
+  "env": "sel4",
+  "exe-suffix": ".elf",
+  "features": "+m,+a,+c",
+  "link-script": "__sel4_ipc_buffer_obj = (__ehdr_start & ~(4096 - 1)) - 4096;",
+  "linker": "rust-lld",
+  "linker-flavor": "gnu-lld",
+  "llvm-target": "riscv64",
+  "max-atomic-width": 64,
+  "metadata": {
+    "description": "Bare RISC-V (RV64IMAC ISA)",
+    "host_tools": false,
+    "std": false,
+    "tier": 2
+  },
+  "panic-strategy": "abort",
+  "relocation-model": "static",
+  "supported-sanitizers": [
+    "shadow-call-stack",
+    "kernel-address"
+  ],
+  "target-pointer-width": "64"
+}

support/targets/riscv64imac-sel4-microkit-resettable-minimal.json

@@ -0,0 +1,30 @@
+{
+  "arch": "riscv64",
+  "code-model": "medium",
+  "cpu": "generic-rv64",
+  "crt-objects-fallback": "false",
+  "data-layout": "e-m:e-p:64:64-i64:64-i128:128-n32:64-S128",
+  "eh-frame-header": false,
+  "emit-debug-gdb-scripts": false,
+  "env": "sel4",
+  "exe-suffix": ".elf",
+  "features": "+m,+a,+c",
+  "link-script": "SECTIONS {\n    .persistent : {\n        *(.persistent .persistent.*)\n    }\n} INSERT BEFORE .data;\n\nASSERT(DEFINED(_reset), \"_reset is not defined\")\n\nENTRY(_reset)\n__sel4_ipc_buffer_obj = (__ehdr_start & ~(4096 - 1)) - 4096;",
+  "linker": "rust-lld",
+  "linker-flavor": "gnu-lld",
+  "llvm-target": "riscv64",
+  "max-atomic-width": 64,
+  "metadata": {
+    "description": "Bare RISC-V (RV64IMAC ISA)",
+    "host_tools": false,
+    "std": false,
+    "tier": 2
+  },
+  "panic-strategy": "abort",
+  "relocation-model": "static",
+  "supported-sanitizers": [
+    "shadow-call-stack",
+    "kernel-address"
+  ],
+  "target-pointer-width": "64"
+}

support/targets/riscv64imac-sel4-microkit-resettable.json

@@ -0,0 +1,29 @@
+{
+  "arch": "riscv64",
+  "code-model": "medium",
+  "cpu": "generic-rv64",
+  "crt-objects-fallback": "false",
+  "data-layout": "e-m:e-p:64:64-i64:64-i128:128-n32:64-S128",
+  "emit-debug-gdb-scripts": false,
+  "env": "sel4",
+  "exe-suffix": ".elf",
+  "features": "+m,+a,+c",
+  "has-thread-local": true,
+  "link-script": "SECTIONS {\n    .persistent : {\n        *(.persistent .persistent.*)\n    }\n} INSERT BEFORE .data;\n\nASSERT(DEFINED(_reset), \"_reset is not defined\")\n\nENTRY(_reset)\n__sel4_ipc_buffer_obj = (__ehdr_start & ~(4096 - 1)) - 4096;",
+  "linker": "rust-lld",
+  "linker-flavor": "gnu-lld",
+  "llvm-target": "riscv64",
+  "max-atomic-width": 64,
+  "metadata": {
+    "description": "Bare RISC-V (RV64IMAC ISA)",
+    "host_tools": false,
+    "std": false,
+    "tier": 2
+  },
+  "relocation-model": "static",
+  "supported-sanitizers": [
+    "shadow-call-stack",
+    "kernel-address"
+  ],
+  "target-pointer-width": "64"
+}

support/targets/riscv64imac-sel4-microkit.json

@@ -0,0 +1,29 @@
+{
+  "arch": "riscv64",
+  "code-model": "medium",
+  "cpu": "generic-rv64",
+  "crt-objects-fallback": "false",
+  "data-layout": "e-m:e-p:64:64-i64:64-i128:128-n32:64-S128",
+  "emit-debug-gdb-scripts": false,
+  "env": "sel4",
+  "exe-suffix": ".elf",
+  "features": "+m,+a,+c",
+  "has-thread-local": true,
+  "link-script": "__sel4_ipc_buffer_obj = (__ehdr_start & ~(4096 - 1)) - 4096;",
+  "linker": "rust-lld",
+  "linker-flavor": "gnu-lld",
+  "llvm-target": "riscv64",
+  "max-atomic-width": 64,
+  "metadata": {
+    "description": "Bare RISC-V (RV64IMAC ISA)",
+    "host_tools": false,
+    "std": false,
+    "tier": 2
+  },
+  "relocation-model": "static",
+  "supported-sanitizers": [
+    "shadow-call-stack",
+    "kernel-address"
+  ],
+  "target-pointer-width": "64"
+}