Add Pancake serial drivers

.github/workflows/examples.yaml

@@ -23,6 +23,7 @@ env:
   MICROKIT_VERSION: 2.3.0
   MICROKIT_URL: https://github.com/seL4/microkit/releases/download/2.3.0/
   SDFGEN_VERSION: 0.35.0
+  CAKE_JOB_ID: 3440
 
 jobs:
   build_linux_x86_64:
@@ -51,6 +52,39 @@ jobs:
         env:
           PYTHON: ${{ github.workspace }}/venv/bin/python
 
+  build_pancake_linux_x86_64:
+    name: Build Pancake (Linux x86-64)
+    runs-on: ubuntu-24.04
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v6
+      - name: Download Microkit SDK
+        run: |
+          wget ${{ env.MICROKIT_URL }}/microkit-sdk-${{ env.MICROKIT_VERSION }}-linux-x86-64.tar.gz
+          tar xf microkit-sdk-${{ env.MICROKIT_VERSION }}-linux-x86-64.tar.gz
+      - name: Install dependencies (via apt)
+        run: sudo apt update && sudo apt install -y make llvm lld imagemagick device-tree-compiler
+      - name: Setup pyenv
+        run: |
+          python3 -m venv venv
+          ./venv/bin/pip install --upgrade sdfgen==${{ env.SDFGEN_VERSION }}
+      - name: Setup systems-ci
+        uses: au-ts/systems-ci@main
+        with:
+          path: systems-ci
+      - name: Setup Pancake compiler
+        run: |
+          wget https://cakeml.org/regression/artefacts/${{ env.CAKE_JOB_ID }}/cake-x64-64.tar.gz
+          tar -xf cake-x64-64.tar.gz
+          cd cake-x64-64
+          make
+          echo "$(pwd):$PATH" >> $GITHUB_PATH
+      - name: Build examples
+        run: ./ci/build.py ${PWD}/microkit-sdk-${{ env.MICROKIT_VERSION }} $(nproc) --pancake --example=serial
+        shell: bash
+        env:
+          PYTHON: ${{ github.workspace }}/venv/bin/python
+
   build_linux_x86_64_nix:
     name: Build (Linux x86-64 Nix)
     runs-on: [self-hosted, Linux, X64]
@@ -76,6 +110,31 @@ jobs:
             ci_build/**/sel4_32.elf
           if-no-files-found: error
 
+  build_pancake_linux_x86_64_nix:
+    name: Build Pancake (Linux x86-64 Nix)
+    runs-on: [self-hosted, Linux, X64]
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v6
+      - name: Setup systems-ci
+        uses: au-ts/systems-ci@main
+        with:
+          path: systems-ci
+      - name: Setup Nix
+        uses: cachix/install-nix-action@v27
+      - name: Get Nix dependencies
+        run: nix develop -c bash -c 'echo Hello World'
+      - name: Build examples
+        run: nix develop --ignore-environment -c bash -c 'source systems-ci/setup.sh && CI=1 ./ci/build.py ${PWD}/microkit-sdk-${{ env.MICROKIT_VERSION }} $(nproc) --pancake --example=serial'
+      - name: Archive image artifacts
+        uses: actions/upload-artifact@v7
+        with:
+          name: loader-images-pancake
+          path: |
+            ci_build/**/loader.img
+            ci_build/**/sel4_32.elf
+          if-no-files-found: error
+
   build_macos_arm64_nix:
     name: Build (macOS ARM64 Nix)
     runs-on: [self-hosted, macos, ARM64]

ci/build.py

@@ -26,6 +26,11 @@ def build_make(args: argparse.Namespace, test_config: common.TestConfig):
     build_dir = common.example_build_path(test_config)
     example_dir = get_example_dir(test_config.example)
 
+    if args.pancake:
+        pancake_args = ["PANCAKE_SERIAL_DRIVER=1"]
+    else:
+        pancake_args = []
+
     subprocess.run(
         [
             "make",
@@ -35,7 +40,8 @@ def build_make(args: argparse.Namespace, test_config: common.TestConfig):
             f"MICROKIT_SDK={args.microkit_sdk}",
             f"MICROKIT_BOARD={test_config.board}",
             f"MICROKIT_CONFIG={test_config.config}",
-        ],
+        ]
+        + pancake_args,
         check=True,
     )
 
@@ -137,6 +143,9 @@ def build(args: argparse.Namespace, test_config: common.TestConfig):
         action="store_true",
         help="Do not remove any pre-existing CI build directory before building",
     )
+    parser.add_argument(
+        "--pancake", action="store_true", help="Use Pancake implementations"
+    )
 
     filters = parser.add_argument_group(title="filters")
     filters.add_argument(

ci/cakeml.nix

@@ -0,0 +1,49 @@
+{
+  stdenv,
+  fetchzip,
+  pancakeVersion ? 3440,
+}:
+
+stdenv.mkDerivation (rec {
+  pname = "pancake";
+  version = "3440";
+
+  src =
+    let
+      hostArch = stdenv.hostPlatform.qemuArch;
+
+      cakemlPlatformNameAndHash =
+        {
+          aarch64 = {
+            arch = "arm8-64";
+            hash = "sha256-1xVVQFunYSxMvGkmApWLfZ+s+hvQ2B5a7sJsoE1K5Qg=";
+          };
+          x86_64 = {
+            arch = "x64-64";
+            hash = "sha256-uNt5HhpBixfEItqdfWuDxt/RKq2kySyh7Fbk08tmSx4=";
+          };
+        }
+        .${hostArch} or (throw "Unsupported architecture: ${hostArch}");
+    in
+    fetchzip {
+      url = "https://cakeml.org/regression/artefacts/${toString pancakeVersion}/cake-${cakemlPlatformNameAndHash.arch}.tar.gz";
+      hash = cakemlPlatformNameAndHash.hash;
+    };
+
+  buildPhase = ''
+    runHook preBuild
+
+    make
+
+    runHook postBuild
+  '';
+
+  installPhase = ''
+    runHook preInstall
+
+    mkdir -p $out/bin
+    cp cake $out/bin/
+
+    runHook postInstall
+  '';
+})

drivers/serial/arm/serial_driver.mk

@@ -8,18 +8,37 @@
 
 SERIAL_DRIVER_DIR := $(dir $(lastword $(MAKEFILE_LIST)))
 
+ifeq ($(PANCAKE_SERIAL_DRIVER),1)
+DRIVER_PNK = \
+	${UTIL}/util.pnk \
+	${SDDF}/include/sddf/serial/queue.pnk \
+	${SERIAL_DRIVER_DIR}/uart.pnk
+
+serial_driver.elf: serial/arm/serial_driver_pnk.o serial/arm/serial_driver.o util/pancake_ffi.o
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+serial/arm/serial_driver_pnk.o: serial/arm/serial_driver_pnk.S |serial/arm
+	$(CC) -c $(CFLAGS) -o $@ $<
+
+serial/arm/serial_driver_pnk.S: $(DRIVER_PNK) |serial/arm
+	cat $(DRIVER_PNK) | cpp -P | $(PANCAKE_COMPILER) $(PANCAKE_FLAGS) > $@
+
+serial/arm/serial_driver.o: ${SERIAL_DRIVER_DIR}/uart.c |serial/arm $(SDDF_LIBC_INCLUDE)
+	$(CC) -c $(CFLAGS) -DPANCAKE_SERIAL_DRIVER -I${SERIAL_DRIVER_DIR}/include -o $@ $<
+else
 serial_driver.elf: serial/arm/serial_driver.o
 	$(LD) $(LDFLAGS) $< $(LIBS) -o $@
 
 serial/arm/serial_driver.o: ${SERIAL_DRIVER_DIR}/uart.c |serial/arm $(SDDF_LIBC_INCLUDE)
 	$(CC) -c $(CFLAGS) -I${SERIAL_DRIVER_DIR}/include -o $@ $<
+endif
 
 serial/arm:
 	mkdir -p $@
 
 -include serial/arm/serial_driver.d
 
 clean::
-	rm -f serial/arm/serial_driver.[do]
+	rm -f serial/arm/serial_driver.[do] serial/arm/serial_driver_pnk.[oS]
 clobber:: clean
 	rm -rf serial_driver.elf serial

drivers/serial/arm/uart.c

@@ -15,6 +15,43 @@ __attribute__((__section__(".serial_driver_config"))) serial_driver_config_t con
 
 __attribute__((__section__(".device_resources"))) device_resources_t device_resources;
 
+#ifdef PANCAKE_SERIAL_DRIVER
+static char cml_memory[1024 * 20];
+extern void *cml_heap;
+extern void *cml_stack;
+extern void *cml_stackend;
+
+extern void cml_main(void);
+
+void cml_exit(int arg)
+{
+    microkit_dbg_puts("ERROR! We should not be getting here\n");
+}
+
+void cml_err(int arg)
+{
+    if (arg == 3) {
+        microkit_dbg_puts("Memory not ready for entry. You may have not run the init code yet, or be trying to enter "
+                          "during an FFI call.\n");
+    }
+    cml_exit(arg);
+}
+
+void cml_clear()
+{
+    microkit_dbg_puts("Trying to clear cache\n");
+}
+
+void init_pancake_mem()
+{
+    unsigned long cml_heap_sz = 1024 * 10;
+    unsigned long cml_stack_sz = 1024 * 10;
+    cml_heap = cml_memory;
+    cml_stack = cml_heap + cml_heap_sz;
+    cml_stackend = cml_stack + cml_stack_sz;
+}
+#endif /* PANCAKE_SERIAL_DRIVER */
+
 serial_queue_handle_t rx_queue_handle;
 serial_queue_handle_t tx_queue_handle;
 
@@ -39,6 +76,7 @@ static void set_baud(long bps)
     uart_regs->fbrd = baud_div_frac;
 }
 
+#ifndef PANCAKE_SERIAL_DRIVER
 static void tx_provide(void)
 {
     bool transferred = false;
@@ -104,6 +142,7 @@ static void handle_irq(void)
         uart_int_reg = uart_regs->mis;
     }
 }
+#endif /* PANCAKE_SERIAL_DRIVER */
 
 static void uart_setup(void)
 {
@@ -165,8 +204,27 @@ void init(void)
         serial_queue_init(&rx_queue_handle, config.rx.queue.vaddr, config.rx.data.size, config.rx.data.vaddr);
     }
     serial_queue_init(&tx_queue_handle, config.tx.queue.vaddr, config.tx.data.size, config.tx.data.vaddr);
+
+#ifdef PANCAKE_SERIAL_DRIVER
+    init_pancake_mem();
+
+    uintptr_t *pnk_mem = (uintptr_t *)cml_heap;
+
+    pnk_mem[0] = (uintptr_t)uart_regs;
+    pnk_mem[1] = device_resources.irqs[0].id;
+    pnk_mem[2] = config.rx.id;
+    pnk_mem[3] = config.tx.id;
+    pnk_mem[4] = (uintptr_t)&rx_queue_handle;
+    pnk_mem[5] = (uintptr_t)&tx_queue_handle;
+    pnk_mem[1024] = config.rx_enabled;
+
+    cml_main();
+#endif /* PANCAKE_SERIAL_DRIVER */
 }
 
+#ifdef PANCAKE_SERIAL_DRIVER
+extern void notified(sddf_channel ch);
+#else
 void notified(sddf_channel ch)
 {
     if (ch == device_resources.irqs[0].id) {
@@ -181,3 +239,4 @@ void notified(sddf_channel ch)
         sddf_dprintf("UART|LOG: received notification on unexpected channel: %u\n", ch);
     }
 }
+#endif /* PANCAKE_SERIAL_DRIVER */