diff --git a/.github/workflows/camkes-vm-deploy.yml b/.github/workflows/camkes-vm-deploy.yml index f0c6de0d..43b4d63a 100644 --- a/.github/workflows/camkes-vm-deploy.yml +++ b/.github/workflows/camkes-vm-deploy.yml @@ -68,7 +68,6 @@ jobs: with: repository: seL4/machine_queue path: machine_queue - token: ${{ secrets.PRIV_REPO_TOKEN }} - name: Download image uses: actions/download-artifact@v3 with: diff --git a/.github/workflows/test-hw.yml b/.github/workflows/test-hw.yml new file mode 100644 index 00000000..c4fa9a22 --- /dev/null +++ b/.github/workflows/test-hw.yml @@ -0,0 +1,95 @@ +# Copyright 2021, Proofcraft Pty Ltd +# +# SPDX-License-Identifier: BSD-2-Clause + +# camkes-vm-examples hardware builds and runs +# +# See camkes-vm-hw/builds.yml in the repo seL4/ci-actions for configs. + +name: HW + +on: + # needs PR target for secrets access; guard by requiring label + pull_request_target: + types: [opened, reopened, synchronize, labeled] + +# downgrade permissions to read-only as you would have in a standard PR action +permissions: + contents: read + +jobs: + code: + name: Freeze Code + runs-on: ubuntu-latest + if: ${{ github.event_name == 'push' || + github.event_name == 'pull_request_target' && + github.event.action != 'labeled' && + (contains(github.event.pull_request.labels.*.name, 'hw-build') || + contains(github.event.pull_request.labels.*.name, 'hw-test')) || + github.event_name == 'pull_request_target' && + github.event.action == 'labeled' && + (github.event.label.name == 'hw-build' || + github.event.label.name == 'hw-test') }} + outputs: + xml: ${{ steps.repo.outputs.xml }} + steps: + - id: repo + uses: seL4/ci-actions/repo-checkout@master + with: + manifest_repo: camkes-vm-examples-manifest + manifest: master.xml + + build: + name: Build + needs: code + runs-on: ubuntu-latest + strategy: + fail-fast: true + matrix: + march: [nehalem, armv7a, armv8a] + steps: + - uses: seL4/ci-actions/camkes-vm@master + with: + xml: ${{ needs.code.outputs.xml }} + march: ${{ matrix.march }} + - name: Upload images + uses: actions/upload-artifact@v3 + with: + name: images-${{ matrix.march }} + path: '*-images.tar.gz' + + run: + name: Hardware + runs-on: ubuntu-latest + needs: [build] + if: ${{ github.repository_owner == 'seL4' && + (github.event_name == 'push' || + github.event_name == 'pull_request_target' && + github.event.action != 'labeled' && + contains(github.event.pull_request.labels.*.name, 'hw-test') || + github.event_name == 'pull_request_target' && + github.event.action == 'labeled' && + github.event.label.name == 'hw-test') }} + strategy: + fail-fast: true + matrix: + march: [nehalem, armv7a, armv8a] + # do not run concurrently with previous jobs in PRs, but do run concurrently in the build matrix + concurrency: camkes-hw-pr-${{ strategy.job-index }} + steps: + - name: Get machine queue + uses: actions/checkout@v4 + with: + repository: seL4/machine_queue + path: machine_queue + - name: Download image + uses: actions/download-artifact@v3 + with: + name: images-${{ matrix.march }} + - name: Run + uses: seL4/ci-actions/camkes-vm-hw@master + with: + march: ${{ matrix.march }} + index: $${{ strategy.job-index }} + env: + HW_SSH: ${{ secrets.HW_SSH }} diff --git a/apps/Arm/vm_introspect/src/cross_vm_connection.c b/apps/Arm/vm_introspect/src/cross_vm_connection.c index a14b061f..35d1ce49 100644 --- a/apps/Arm/vm_introspect/src/cross_vm_connection.c +++ b/apps/Arm/vm_introspect/src/cross_vm_connection.c @@ -19,7 +19,7 @@ #endif //example going from linux to native component -static void sys_ipa_to_pa(void *cookie) +static void sys_ipa_to_pa(void) { printf("address from linux is %x\n", *(seL4_Word *)introspect_data); diff --git a/apps/Arm/vm_introspect/src/init_dataport_ram.c b/apps/Arm/vm_introspect/src/init_dataport_ram.c index 715f9daf..91ee41bd 100644 --- a/apps/Arm/vm_introspect/src/init_dataport_ram.c +++ b/apps/Arm/vm_introspect/src/init_dataport_ram.c @@ -12,23 +12,21 @@ #include #include -extern unsigned long linux_ram_base; -extern unsigned long linux_ram_size; - extern dataport_caps_handle_t memdev_handle; static vm_frame_t dataport_memory_iterator(uintptr_t addr, void *cookie) { cspacepath_t return_frame; vm_frame_t frame_result = { seL4_CapNull, seL4_NoRights, 0, 0 }; + const vm_config_t *vm_config = (const vm_config_t *)cookie; uintptr_t frame_start = ROUND_DOWN(addr, BIT(seL4_PageBits)); - if (frame_start < linux_ram_base || frame_start > linux_ram_base + linux_ram_size) { + if (frame_start < vm_config->ram.base || frame_start > vm_config->ram.base + vm_config->ram.size) { ZF_LOGE("Error: Not dataport ram region"); return frame_result; } - int page_idx = (frame_start - linux_ram_base) / BIT(seL4_PageBits); + int page_idx = (frame_start - vm_config->ram.base) / BIT(seL4_PageBits); frame_result.cptr = dataport_get_nth_frame_cap(&memdev_handle, page_idx); frame_result.rights = seL4_AllRights; frame_result.vaddr = frame_start; @@ -36,10 +34,15 @@ static vm_frame_t dataport_memory_iterator(uintptr_t addr, void *cookie) return frame_result; } +/* This overwrites the weak function in the VMM module init_ram */ void init_ram_module(vm_t *vm, void *cookie) { int err; - err = vm_ram_register_at_custom_iterator(vm, linux_ram_base, linux_ram_size, dataport_memory_iterator, NULL); + void *reg_cookie = (void *)&vm_config; + err = vm_ram_register_at_custom_iterator(vm, vm_config.ram.base, + vm_config.ram.size, + dataport_memory_iterator, + reg_cookie); assert(!err); } diff --git a/apps/x86/minimal_64/app_settings.cmake b/apps/x86/minimal_64/app_settings.cmake index 562dc923..8a92dc2e 100644 --- a/apps/x86/minimal_64/app_settings.cmake +++ b/apps/x86/minimal_64/app_settings.cmake @@ -10,3 +10,4 @@ cmake_minimum_required(VERSION 3.8.2) set(KernelSel4Arch x86_64 CACHE STRING "" FORCE) set(KernelX86_64VTX64BitGuests ON CACHE BOOL "" FORCE) set(KernelMaxNumNodes 1 CACHE STRING "" FORCE) +set(LibSel4VMMUseHPET ON CACHE BOOL "" FORCE)