From 41c39e6561c7f4ddafcb391bdfbc0dee34c00d80 Mon Sep 17 00:00:00 2001 From: Samir Rashid Date: Thu, 26 Sep 2024 20:07:26 +0000 Subject: [PATCH 1/9] Add ci --- .github/workflows/benchmarks.yml | 39 ++++++++ .github/workflows/ci-nightly.yml | 88 ++++++++++++++++ .github/workflows/ci.yml | 126 +++++++++++++++++++++++ .github/workflows/labeler.yml | 21 ++++ .github/workflows/litex_sim.yml | 138 ++++++++++++++++++++++++++ .github/workflows/mergequeue_docs.yml | 34 +++++++ .github/workflows/tockbot-nightly.yml | 134 +++++++++++++++++++++++++ 7 files changed, 580 insertions(+) create mode 100644 .github/workflows/benchmarks.yml create mode 100644 .github/workflows/ci-nightly.yml create mode 100644 .github/workflows/ci.yml create mode 100644 .github/workflows/labeler.yml create mode 100644 .github/workflows/litex_sim.yml create mode 100644 .github/workflows/mergequeue_docs.yml create mode 100644 .github/workflows/tockbot-nightly.yml diff --git a/.github/workflows/benchmarks.yml b/.github/workflows/benchmarks.yml new file mode 100644 index 0000000000..2e179aa664 --- /dev/null +++ b/.github/workflows/benchmarks.yml @@ -0,0 +1,39 @@ +# Licensed under the Apache License, Version 2.0 or the MIT License. +# SPDX-License-Identifier: Apache-2.0 OR MIT +# Copyright Tock Contributors 2023. + +# This workflow calculates size diffs for the compiled binary of each supported tock board + +name: Benchmarks + +# Controls when the action will run. Triggers the workflow on pull request +# events but only for the master branch +on: + pull_request: + branches: master + +# A workflow run is made up of one or more jobs that can run sequentially or in parallel +# If you add additional jobs, remember to add them to bors.toml +permissions: + contents: read + +jobs: + benchmarks: + # The type of runner that the job will run on + runs-on: ubuntu-latest + + # Steps represent a sequence of tasks that will be executed as part of the job + steps: + - uses: actions/checkout@v3 + - name: Set up Python + uses: actions/setup-python@v4 + with: + python-version: '3.x' + - name: Install dependencies + run: | + python -m pip install --upgrade pip setuptools wheel + pip install --user cxxfilt + sudo apt install llvm + - name: size report + run: | + ./tools/github_actions_size_changes.sh diff --git a/.github/workflows/ci-nightly.yml b/.github/workflows/ci-nightly.yml new file mode 100644 index 0000000000..46d25f08bd --- /dev/null +++ b/.github/workflows/ci-nightly.yml @@ -0,0 +1,88 @@ +# Licensed under the Apache License, Version 2.0 or the MIT License. +# SPDX-License-Identifier: Apache-2.0 OR MIT +# Copyright Tock Contributors 2024. + +name: tock-nightly-ci + +on: + schedule: + - cron: "0 0 * * *" + +env: + TERM: xterm # Makes tput work in actions output + +# A workflow run is made up of one or more jobs that can run sequentially or in parallel +# If you add additional jobs, remember to add them to bors.toml +permissions: + contents: read + issues: write + +jobs: + ci-build: + strategy: + matrix: + os: [ubuntu-latest, macos-latest] + runs-on: ${{ matrix.os }} + + steps: + - uses: actions/checkout@v3 + + - name: ci-job-syntax + run: make ci-job-syntax + - name: ci-job-compilation + run: make ci-job-compilation + - name: ci-job-debug-support-targets + run: make ci-job-debug-support-targets + + - name: ci-job-collect-artifacts + run: make ci-job-collect-artifacts + - name: upload-build-artifacts + uses: actions/upload-artifact@v3 + with: + name: build-artifacts + path: tools/ci-artifacts + + ci-tests: + strategy: + matrix: + os: [ubuntu-latest, macos-latest] + runs-on: ${{ matrix.os }} + + steps: + - name: Update package repositories + run: | + sudo apt update + if: matrix.os == 'ubuntu-latest' + - name: Install dependencies for ubuntu-latest + run: | + sudo apt install libudev-dev libzmq3-dev + if: matrix.os == 'ubuntu-latest' + - name: Install dependencies for macos-latest + run: | + brew install zeromq + if: matrix.os == 'macos-latest' + - uses: actions/checkout@v3 + - name: ci-job-libraries + run: make ci-job-libraries + - name: ci-job-archs + run: make ci-job-archs + - name: ci-job-kernel + run: make ci-job-kernel + - name: ci-job-chips + run: make ci-job-chips + - name: ci-job-tools + run: make ci-job-tools + - name: Create Issue on Failed workflow + if: failure() + uses: dacbd/create-issue-action@main + with: + token: ${{ github.token }} + title: Nightly CI failed + body: | + ### Context + [Failed Run](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) + [Codebase](https://github.com/${{ github.repository }}/tree/${{ github.sha }}) + Workflow name - `${{ github.workflow }}` + Job - `${{ github.job }}` + status - `${{ job.status }}` + assignees: tock/core-wg diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000000..6732130e97 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,126 @@ +# Licensed under the Apache License, Version 2.0 or the MIT License. +# SPDX-License-Identifier: Apache-2.0 OR MIT +# Copyright Tock Contributors 2023. + +# This workflow contains all tock-ci, separated into jobs + +name: tock-ci +env: + TERM: xterm # Makes tput work in actions output + +# Controls when the action will run. Triggers the workflow on push or pull request +# events but only for the master branch +on: + push: # Run CI for all branches except GitHub merge queue tmp branches + branches-ignore: + - "gh-readonly-queue/**" + pull_request: # Run CI for PRs on any branch + merge_group: # Run CI for the GitHub merge queue + +# A workflow run is made up of one or more jobs that can run sequentially or in parallel +# If you add additional jobs, remember to add them to bors.toml +permissions: + contents: read + +jobs: + ci-format: + strategy: + matrix: + os: [ubuntu-latest] + # The type of runner that the job will run on + runs-on: ${{ matrix.os }} + + # Steps represent a sequence of tasks that will be executed as part of the job + steps: + - uses: actions/checkout@v3 + - uses: actions/setup-node@v3 + - name: ci-job-format + run: make ci-job-format + - name: ci-job-markdown-toc + run: make ci-job-markdown-toc + - name: ci-job-readme-check + run: make ci-job-readme-check + + ci-clippy: + strategy: + matrix: + os: [ubuntu-latest] + # The type of runner that the job will run on + runs-on: ${{ matrix.os }} + + # Steps represent a sequence of tasks that will be executed as part of the job + steps: + - uses: actions/checkout@v3 + - name: ci-job-clippy + run: make ci-job-clippy + + ci-build: + strategy: + matrix: + os: [ubuntu-latest] + runs-on: ${{ matrix.os }} + + steps: + - uses: actions/checkout@v3 + - name: ci-job-syntax + run: make ci-job-syntax + - name: ci-job-compilation + run: make ci-job-compilation + - name: ci-job-debug-support-targets + run: make ci-job-debug-support-targets + - name: ci-job-collect-artifacts + run: make ci-job-collect-artifacts + - name: upload-build-artifacts + uses: actions/upload-artifact@v3 + with: + name: build-artifacts + path: tools/ci-artifacts + + ci-tests: + strategy: + matrix: + os: [ubuntu-latest] + runs-on: ${{ matrix.os }} + + steps: + - name: Update package repositories + run: | + sudo apt update + if: matrix.os == 'ubuntu-latest' + - name: Install dependencies for ubuntu-latest + run: | + sudo apt install libudev-dev libzmq3-dev + if: matrix.os == 'ubuntu-latest' + - uses: actions/checkout@v3 + - name: ci-job-libraries + run: make ci-job-libraries + - name: ci-job-archs + run: make ci-job-archs + - name: ci-job-kernel + run: make ci-job-kernel + - name: ci-job-capsules + run: make ci-job-capsules + - name: ci-job-chips + run: make ci-job-chips + - name: ci-job-tools + run: make ci-job-tools + - name: ci-job-cargo-test-build + run: make ci-job-cargo-test-build + + ci-qemu: + strategy: + matrix: + os: [ubuntu-latest] + runs-on: ${{ matrix.os }} + + steps: + - name: Update package repositories + run: | + sudo apt update + - name: Install dependencies + continue-on-error: true + run: | + sudo apt install meson + - uses: actions/checkout@v3 + - name: ci-job-qemu + run: make ci-job-qemu diff --git a/.github/workflows/labeler.yml b/.github/workflows/labeler.yml new file mode 100644 index 0000000000..d7d87957db --- /dev/null +++ b/.github/workflows/labeler.yml @@ -0,0 +1,21 @@ +# Licensed under the Apache License, Version 2.0 or the MIT License. +# SPDX-License-Identifier: Apache-2.0 OR MIT +# Copyright Tock Contributors 2023. + +name: "Pull Request Labeler" +on: +- pull_request_target + +permissions: + contents: read + +jobs: + triage: + permissions: + contents: read # for actions/labeler to determine modified files + pull-requests: write # for actions/labeler to add labels to PRs + runs-on: ubuntu-latest + steps: + - uses: actions/labeler@v4.3.0 + with: + repo-token: "${{ secrets.GITHUB_TOKEN }}" diff --git a/.github/workflows/litex_sim.yml b/.github/workflows/litex_sim.yml new file mode 100644 index 0000000000..f2877aea3f --- /dev/null +++ b/.github/workflows/litex_sim.yml @@ -0,0 +1,138 @@ +# Licensed under the Apache License, Version 2.0 or the MIT License. +# SPDX-License-Identifier: Apache-2.0 OR MIT +# Copyright Tock Contributors 2023. + +# This workflow contains the litex-ci-runner job, which uses the LiteX Verilated +# simulation to run a Tock kernel and perform various tests using libtock-c +# example applications. + +name: litex-sim-ci +env: + TERM: xterm # Makes tput work in actions output + +# Controls when the action will run. Triggers the workflow on push or pull +# request events but only for the master branch +on: + push: # Run CI for all branches except GitHub merge queue tmp branches + branches-ignore: + - "gh-readonly-queue/**" + pull_request: # Run CI for PRs on any branch + merge_group: # Run CI for the GitHub merge queue + +# A workflow run is made up of one or more jobs that can run sequentially or in parallel +# If you add additional jobs, remember to add them to bors.toml +permissions: + contents: read + +jobs: + litex-sim-ci: + strategy: + matrix: + os: [ubuntu-latest] + + # The type of runner that the job will run on + runs-on: ${{ matrix.os }} + + # Steps represent a sequence of tasks that will be executed as part of the job + steps: + # Checkout the Tock repo, needs to happen at the beginning given + # that other steps (such as the Rust toolchain) depend on files + # in this repo. + - name: Checkout the current repository + uses: actions/checkout@v3 + + # Install basic packages required for the GitHub actions workflow + - name: Update packages and install dependencies + run: | + sudo apt update + sudo apt install python3-pip python3-venv gcc-riscv64-unknown-elf \ + verilator libevent-dev libjson-c-dev libz-dev libzmq3-dev + + # Install elf2tab to be able to build userspace apps + - name: Install elf2tab + run: | + cargo install elf2tab@0.12.0 + + # Install tockloader, which is used to prepare binaries with userspace + # applications. + - name: Install tockloader + run: | + pip3 install tockloader==1.12.0 + + # Clone tock-litex support repository under ./tock-litex, check out the + # targeted release. + - name: Checkout the tock-litex repository + uses: actions/checkout@v3 + with: + repository: lschuermann/tock-litex + # The pinned revision is different from the targeted release as + # documented in the LiteX boards, as the CI requires special patches + # to LiteX for interacting with the simulation: + ref: 2024011101-tock-ci-1 + path: tock-litex + + # Install all of the required Python packages from the tock-litex' + # requirements.txt file + - name: Install Python packages pinned by the tock-litex revision + run: | + pushd tock-litex + # Migen is the DSL which the LiteX ecosystem uses as its + # hardware-description language. It effectively provides a set of + # Python classes and constructs which can be translated into Verilog. + # It is not a package of the LiteX ecosystem, and thus not in the + # requirements.txt, but it is required to be present on the system. + # It should not require any specific or patched version. + pip3 install migen==0.9.2 + pip3 install -r requirements.txt + popd + + # Build the LiteX simulator Tock kernel. This kernel is never touched, the + # litex-ci-runner will use its own temporary flash files. + - name: Build the LiteX simulator Tock kernel + run: | + pushd boards/litex/sim + make + popd + + # Revision to checkout defined in the main tock repository in + # .libtock_c_ci_rev + - name: Checkout libtock-c CI revision + uses: actions/checkout@v3 + with: + repository: tock/libtock-c + # Pins a libtock-c revision for LiteX CI tests. In case of + # bugs fixed in libtock-c, backwards-incompatible changes in + # Tock or new tests this might need to be updated. + # + # libtock-c of Feb 9, 2024, 3:08 PM EST + ref: 0e72c922e13cd83a1aaae7a5f587099d45815e6a + path: libtock-c + + - name: Build libtock-c apps + run: | + # We only need to build for a single target, but at multiple flash and + # memory addresses such that tockloader can place the non-PIC apps + # into the kernel binary properly. + export TOCK_TARGETS="\ + rv32imc|rv32imc.0x00080080.0x40008000|0x00080080|0x40008000 + rv32imc|rv32imc.0x00088080.0x40010000|0x00088080|0x40010000" + export LIBTOCK_C_APPS="\ + c_hello \ + tests/console_timeout \ + tests/mpu_walk_region \ + tests/printf_long \ + rot13_service \ + rot13_client \ + tests/console_recv_short \ + tests/console_recv_long" + pushd libtock-c/examples + for APP in $LIBTOCK_C_APPS; do + make -C "$APP" + done + popd + + # Run the LiteX simulation with required options for Tock + - name: Run various tests in the LiteX simulation using the litex-ci-runner + run: | + pushd tools/litex-ci-runner + cargo run diff --git a/.github/workflows/mergequeue_docs.yml b/.github/workflows/mergequeue_docs.yml new file mode 100644 index 0000000000..6cf8794b62 --- /dev/null +++ b/.github/workflows/mergequeue_docs.yml @@ -0,0 +1,34 @@ +# Licensed under the Apache License, Version 2.0 or the MIT License. +# SPDX-License-Identifier: Apache-2.0 OR MIT +# Copyright Tock Contributors 2023. + +# Netlify's own CI builds both deploy previews for PRs, as well as the +# production deploy for the master branch. We use this workflow purely as we +# can't have Netlify build the wildcard gh-readonly-queue/* branches. This +# workflow thus ensures that docs build successfully (albeit not in the exact +# same environment as Netlify's). +# +# See issue #3428 for more information. + +name: docs-ci +env: + TERM: dumb # Identical to Netlify build environment + +on: + merge_group: + +permissions: + contents: read + +jobs: + ci-docs: + strategy: + matrix: + os: [ubuntu-latest] + runs-on: ${{ matrix.os }} + + steps: + - uses: actions/checkout@v3 + - # This also sets up the rustup environment + name: ci-netlify-build + run: tools/netlify-build.sh diff --git a/.github/workflows/tockbot-nightly.yml b/.github/workflows/tockbot-nightly.yml new file mode 100644 index 0000000000..158373505d --- /dev/null +++ b/.github/workflows/tockbot-nightly.yml @@ -0,0 +1,134 @@ +# Licensed under the Apache License, Version 2.0 or the MIT License. +# SPDX-License-Identifier: Apache-2.0 OR MIT +# Copyright Tock Contributors 2024. + +name: "Tockbot" + +on: + schedule: + - cron: "0 0 * * *" + workflow_dispatch: + inputs: + dispatch-job: + description: 'Which job to execute (choose between "all", "maint-nightly")' + required: true + default: 'all' + dry-run: + description: 'Whether to execute the jobs as dry-run' + required: true + default: true + +jobs: + dispatcher: + runs-on: ubuntu-latest + + # This job determines which other jobs should be run: + outputs: + run-maint-nightly: ${{ steps.dispatch-logic.outputs.run-maint-nightly }} + dry-run: ${{ steps.dispatch-logic.outputs.dry-run }} + + steps: + # On pushes we want to check whether any changes have been made + # to the Tockbot code base. Disabled for now: + - uses: actions/checkout@v4 + + # Dispatcher business logic: + - name: Dispatch Tockbot Jobs + id: dispatch-logic + env: + DISPATCH_JOB: ${{ github.event.inputs.dispatch-job }} + DISPATCH_DRY_RUN: ${{ github.event.inputs.dry-run }} + run: | + if [ "$GITHUB_EVENT_NAME" == "workflow_dispatch" ]; then + if [ "$DISPATCH_DRY_RUN" == "true" ]; then + echo "dry-run=true" >> $GITHUB_OUTPUT + elif [ "$DISPATCH_DRY_RUN" == "false" ]; then + echo "dry-run=false" >> $GITHUB_OUTPUT + else + echo "Error: dry-run not a boolean: \"$DISPATCH_DRY_RUN\"" >&2 + exit 1 + fi + + if [ "$DISPATCH_JOB" == "all" ]; then + echo "run-maint-nightly=true" >> $GITHUB_OUTPUT + elif [ "$DISPATCH_JOB" == "maint-nightly" ]; then + echo "run-maint-nightly=true" >> $GITHUB_OUTPUT + else + echo "Error: unknown job \"$DISPATCH_JOB\"" >&2 + exit 1 + fi + elif [ "$GITHUB_EVENT_NAME" == "pull_request" ]; then + echo "dry-run=true" >> $GITHUB_OUTPUT + echo "run-maint-nightly=true" >> $GITHUB_OUTPUT + elif [ "$GITHUB_EVENT_NAME" == "schedule" ]; then + echo "dry-run=false" >> $GITHUB_OUTPUT + echo "run-maint-nightly=true" >> $GITHUB_OUTPUT + else + echo "Error: unknown event name \"$GITHUB_EVENT_NAME\"" >&2 + exit 1 + fi + + maint-nightly: + runs-on: ubuntu-latest + + # Only run this job if the dispatcher determined to schedule the + # "maint-nightly" or "dry-run" jobs: + needs: dispatcher + if: ${{ needs.dispatcher.outputs.run-maint-nightly == 'true' && needs.dispatcher.outputs.dry-run != 'true' }} + + permissions: + # Give GITHUB_TOKEN write permissions to modify PRs and issues: + pull-requests: write + issues: write + + steps: + # Requires a tock checkout to run from: + - uses: actions/checkout@v4 + + # Setup Python and install dependencies: + - uses: actions/setup-python@v5 + - name: Install Python Dependencies + run: pip install -r tools/tockbot/requirements.txt + + # Run nightly tockbot maintenance: + - name: Nightly Tockbot Maintenance + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + DRY_RUN: ${{ needs.dispatcher.outputs.dry-run == 'true' && '-n' || '' }} + run: | + cd tools/tockbot/ + ./tockbot.py -v $DRY_RUN maint-nightly -c ./maint_nightly.yaml + + # We'd like to avoid duplicating this, either by using conditionals in the + # permissions key, or by using YAML anchors, neither of which are supported by + # GH Actions... + maint-nightly-dry-run: + runs-on: ubuntu-latest + + # Only run this job if the dispatcher determined to schedule the + # "maint-nightly" or "dry-run" jobs: + needs: dispatcher + if: ${{ needs.dispatcher.outputs.run-maint-nightly == 'true' && needs.dispatcher.outputs.dry-run == 'true' }} + + permissions: + # Dry-run, read-only access: + pull-requests: read + issues: read + + steps: + # Requires a tock checkout to run from: + - uses: actions/checkout@v4 + + # Setup Python and install dependencies: + - uses: actions/setup-python@v5 + - name: Install Python Dependencies + run: pip install -r tools/tockbot/requirements.txt + + # Run nightly tockbot maintenance: + - name: Nightly Tockbot Maintenance + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + DRY_RUN: ${{ needs.dispatcher.outputs.dry-run == 'true' && '-n' || '' }} + run: | + cd tools/tockbot/ + ./tockbot.py -v $DRY_RUN maint-nightly -c ./maint_nightly.yaml From 669b0385affc1860b7e3b1fb72c0ac6b6bd1a0d5 Mon Sep 17 00:00:00 2001 From: Samir Rashid Date: Thu, 26 Sep 2024 23:19:44 +0000 Subject: [PATCH 2/9] Fix rv32i compile errors --- arch/cortex-m/src/lib.rs | 18 ++++---- arch/rv32i/Cargo.toml | 3 +- arch/rv32i/src/lib.rs | 10 ++-- arch/rv32i/src/pmp.rs | 45 +++++++++--------- arch/rv32i/src/support.rs | 4 +- arch/rv32i/src/syscall.rs | 29 ++++++------ capsules/system/src/process_checker/basic.rs | 20 ++++---- .../system/src/process_checker/signature.rs | 10 ++-- flux_support/src/extern_specs/iter.rs | 12 ++--- flux_support/src/extern_specs/slice.rs | 3 +- flux_support/src/flux_ptr.rs | 46 +++++++++++++++++++ .../tock-register-interface/src/fields.rs | 2 +- 12 files changed, 127 insertions(+), 75 deletions(-) diff --git a/arch/cortex-m/src/lib.rs b/arch/cortex-m/src/lib.rs index 700b9beefa..81b8eca1ba 100644 --- a/arch/cortex-m/src/lib.rs +++ b/arch/cortex-m/src/lib.rs @@ -13,20 +13,20 @@ use core::fmt::Write; #[cfg(all(target_arch = "arm", target_os = "none"))] use core::arch::global_asm; -#[flux::ignore] +#[flux_rs::ignore] pub mod dcb; -#[flux::ignore] +#[flux_rs::ignore] pub mod dwt; pub mod mpu; -#[flux::ignore] +#[flux_rs::ignore] pub mod nvic; -#[flux::ignore] +#[flux_rs::ignore] pub mod scb; -#[flux::ignore] +#[flux_rs::ignore] pub mod support; -#[flux::ignore] +#[flux_rs::ignore] pub mod syscall; -#[flux::ignore] +#[flux_rs::ignore] pub mod systick; // These constants are defined in the linker script. @@ -120,7 +120,7 @@ pub trait CortexMVariant { /// Format and display architecture-specific state useful for debugging. /// /// This is generally used after a `panic!()` to aid debugging. - #[flux::ignore] + #[flux_rs::ignore] unsafe fn print_cortexm_state(writer: &mut dyn Write); } @@ -207,7 +207,7 @@ global_asm!( etext = sym _etext, ); -#[flux::ignore] +#[flux_rs::ignore] pub unsafe fn print_cortexm_state(writer: &mut dyn Write) { let _ccr = syscall::SCB_REGISTERS[0]; let cfsr = syscall::SCB_REGISTERS[1]; diff --git a/arch/rv32i/Cargo.toml b/arch/rv32i/Cargo.toml index 110302f11b..12f3bc422a 100644 --- a/arch/rv32i/Cargo.toml +++ b/arch/rv32i/Cargo.toml @@ -13,10 +13,11 @@ enabled = true [dependencies] kernel = { path = "../../kernel" } +flux_support = { path = "../../flux_support" } tock-registers = { path = "../../libraries/tock-register-interface" } riscv-csr = { path = "../../libraries/riscv-csr" } riscv = { path = "../riscv" } - +flux-rs = { git = "https://github.com/flux-rs/flux" } [lints] workspace = true diff --git a/arch/rv32i/src/lib.rs b/arch/rv32i/src/lib.rs index 60fefeead3..c77a36a807 100644 --- a/arch/rv32i/src/lib.rs +++ b/arch/rv32i/src/lib.rs @@ -4,9 +4,11 @@ //! Support for the 32-bit RISC-V architecture. +#![feature(proc_macro_hygiene)] #![crate_name = "rv32i"] #![crate_type = "rlib"] #![no_std] +use flux_rs::*; use core::fmt::Write; @@ -18,9 +20,9 @@ use kernel::utilities::registers::interfaces::{Readable, Writeable}; pub mod clic; pub mod machine_timer; pub mod pmp; -#[flux::ignore] +#[flux_rs::ignore] pub mod support; -#[flux::ignore] +#[flux_rs::ignore] pub mod syscall; // Re-export the shared CSR library so that dependent crates do not have to have @@ -429,7 +431,7 @@ pub unsafe fn semihost_command(_command: usize, _arg0: usize, _arg1: usize) -> u } /// Print a readable string for an mcause reason. -#[flux::ignore] +#[flux_rs::ignore] pub unsafe fn print_mcause(mcval: csr::mcause::Trap, writer: &mut dyn Write) { match mcval { csr::mcause::Trap::Interrupt(interrupt) => match interrupt { @@ -516,7 +518,7 @@ pub unsafe fn print_mcause(mcval: csr::mcause::Trap, writer: &mut dyn Write) { /// Prints out RISCV machine state, including basic system registers /// (mcause, mstatus, mtvec, mepc, mtval, interrupt status). -#[flux::ignore] +#[flux_rs::ignore] pub unsafe fn print_riscv_state(writer: &mut dyn Write) { let mcval: csr::mcause::Trap = core::convert::From::from(csr::CSR.mcause.extract()); let _ = writer.write_fmt(format_args!("\r\n---| RISC-V Machine State |---\r\n")); diff --git a/arch/rv32i/src/pmp.rs b/arch/rv32i/src/pmp.rs index 606d4a055b..b5e988f403 100644 --- a/arch/rv32i/src/pmp.rs +++ b/arch/rv32i/src/pmp.rs @@ -7,12 +7,12 @@ use core::num::NonZeroUsize; use core::ops::Range; use core::{cmp, fmt}; +use crate::csr; +use flux_support::*; use kernel::platform::mpu; use kernel::utilities::cells::OptionalCell; use kernel::utilities::registers::{register_bitfields, LocalRegisterCopy}; -use crate::csr; - register_bitfields![u8, /// Generic `pmpcfg` octet. /// @@ -569,7 +569,7 @@ impl + 'static> kernel::pla { type MpuConfig = PMPUserMPUConfig; - fn enable_app_mpu(&self) { + fn enable_app_mpu(&mut self) { // TODO: This operation may fail when the PMP is not exclusively used // for userspace. Instead of panicing, we should handle this case more // gracefully and return an error in the `MPU` trait. Process @@ -579,7 +579,7 @@ impl + 'static> kernel::pla self.pmp.enable_user_pmp().unwrap() } - fn disable_app_mpu(&self) { + fn disable_app_mpu(&mut self) { self.pmp.disable_user_pmp() } @@ -617,7 +617,7 @@ impl + 'static> kernel::pla fn allocate_region( &self, - unallocated_memory_start: *const u8, + unallocated_memory_start: FluxPtr, unallocated_memory_size: usize, min_region_size: usize, permissions: mpu::Permissions, @@ -635,7 +635,7 @@ impl + 'static> kernel::pla // provided start address and size, transform them to meet the // constraints, and then check that we're still within the bounds of the // provided values: - let mut start = unallocated_memory_start as usize; + let mut start = usize::from(unallocated_memory_start); let mut size = min_region_size; // Region start always has to align to 4 bytes. Round up to a 4 byte @@ -659,7 +659,7 @@ impl + 'static> kernel::pla // allocation constraints, namely ensure that // // start + size <= unallocated_memory_start + unallocated_memory_size - if start + size > (unallocated_memory_start as usize) + unallocated_memory_size { + if start + size > (usize::from(unallocated_memory_start)) + unallocated_memory_size { // We're overflowing the provided memory region, can't make // allocation. Normally, we'd abort here. // @@ -686,7 +686,7 @@ impl + 'static> kernel::pla if writeable || (start + size - > (unallocated_memory_start as usize) + unallocated_memory_size + 3) + > (usize::from(unallocated_memory_start)) + unallocated_memory_size + 3) { return None; } @@ -708,7 +708,7 @@ impl + 'static> kernel::pla ); config.is_dirty.set(true); - Some(mpu::Region::new(start as *const u8, size)) + Some(mpu::Region::new(flux_support::FluxPtr::from(start), size)) } fn remove_memory_region( @@ -723,8 +723,8 @@ impl + 'static> kernel::pla .find(|(_i, r)| { // `start as usize + size` in lieu of a safe pointer offset method r.0 != TORUserPMPCFG::OFF - && r.1 == region.start_address() - && r.2 == (region.start_address() as usize + region.size()) as *const u8 + && r.1 == u8::from(region.start_address()) as *const u8 + && r.2 == (usize::from(region.start_address()) + region.size()) as *const u8 }) .map(|(i, _)| i) .ok_or(())?; @@ -737,14 +737,14 @@ impl + 'static> kernel::pla fn allocate_app_memory_region( &self, - unallocated_memory_start: *const u8, + unallocated_memory_start: FluxPtr, unallocated_memory_size: usize, min_memory_size: usize, initial_app_memory_size: usize, initial_kernel_memory_size: usize, permissions: mpu::Permissions, config: &mut Self::MpuConfig, - ) -> Option<(*const u8, usize)> { + ) -> Option<(FluxPtr, usize)> { // An app memory region can only be allocated once per `MpuConfig`. // If we already have one, abort: if config.app_memory_region.is_some() { @@ -764,7 +764,7 @@ impl + 'static> kernel::pla // protected by the PMP). For this, start with the provided start // address and size, transform them to meet the constraints, and then // check that we're still within the bounds of the provided values: - let mut start = unallocated_memory_start as usize; + let mut start = usize::from(unallocated_memory_start); let mut pmp_region_size = initial_app_memory_size; // Region start always has to align to 4 bytes. Round up to a 4 byte @@ -802,7 +802,8 @@ impl + 'static> kernel::pla // , which ensures the PMP constraints didn't push us over the bounds of // the provided memory region, and we can fit the entire allocation as // requested by the kernel: - if start + memory_block_size > (unallocated_memory_start as usize) + unallocated_memory_size + if start + memory_block_size + > (usize::from(unallocated_memory_start)) + unallocated_memory_size { // Overflowing the provided memory region, can't make allocation: return None; @@ -828,20 +829,20 @@ impl + 'static> kernel::pla config.is_dirty.set(true); config.app_memory_region.replace(region_num); - Some((start as *const u8, memory_block_size)) + Some((flux_support::FluxPtr::from(start), memory_block_size)) } fn update_app_memory_region( &self, - app_memory_break: *const u8, - kernel_memory_break: *const u8, + app_memory_break: FluxPtr, + kernel_memory_break: FluxPtr, permissions: mpu::Permissions, config: &mut Self::MpuConfig, ) -> Result<(), ()> { let region_num = config.app_memory_region.get().ok_or(())?; - let mut app_memory_break = app_memory_break as usize; - let kernel_memory_break = kernel_memory_break as usize; + let mut app_memory_break = app_memory_break as FluxPtr; + let kernel_memory_break = kernel_memory_break as FluxPtr; // Ensure that the requested app_memory_break complies with PMP // alignment constraints, namely that the region's end address is 4 byte @@ -858,13 +859,13 @@ impl + 'static> kernel::pla // If we're not out of memory, update the region configuration // accordingly: config.regions[region_num].0 = permissions.into(); - config.regions[region_num].2 = app_memory_break as *const u8; + config.regions[region_num].2 = u8::from(app_memory_break) as *const u8; config.is_dirty.set(true); Ok(()) } - fn configure_mpu(&self, config: &Self::MpuConfig) { + fn configure_mpu(&mut self, config: &Self::MpuConfig) { if !self.last_configured_for.contains(&config.id) || config.is_dirty.get() { self.pmp.configure_pmp(&config.regions).unwrap(); config.is_dirty.set(false); diff --git a/arch/rv32i/src/support.rs b/arch/rv32i/src/support.rs index af057c54cc..05ae44b6b5 100644 --- a/arch/rv32i/src/support.rs +++ b/arch/rv32i/src/support.rs @@ -5,6 +5,8 @@ //! Core low-level operations. use crate::csr::{mstatus::mstatus, CSR}; +use flux_rs::*; +use flux_support::*; #[cfg(all(target_arch = "riscv32", target_os = "none"))] #[inline(always)] @@ -24,7 +26,7 @@ pub unsafe fn wfi() { asm!("wfi", options(nomem, nostack)); } -#[flux::trusted] +#[flux_rs::trusted] pub unsafe fn atomic(f: F) -> R where F: FnOnce() -> R, diff --git a/arch/rv32i/src/syscall.rs b/arch/rv32i/src/syscall.rs index 348d9425f1..83b804f8fe 100644 --- a/arch/rv32i/src/syscall.rs +++ b/arch/rv32i/src/syscall.rs @@ -9,9 +9,10 @@ use core::mem::size_of; use core::ops::Range; use crate::csr::mcause; +use flux_rs::*; +use flux_support::*; use kernel::errorcode::ErrorCode; use kernel::syscall::ContextSwitchReason; - /// This holds all of the state that the kernel must keep for the process when /// the process is not executing. #[derive(Default)] @@ -128,8 +129,8 @@ impl kernel::syscall::UserspaceKernelBoundary for SysCall { unsafe fn initialize_process( &self, - accessible_memory_start: *const u8, - _app_brk: *const u8, + accessible_memory_start: FluxPtr, + _app_brk: FluxPtr, state: &mut Self::StoredState, ) -> Result<(), ()> { // Need to clear the stored state when initializing. @@ -141,7 +142,7 @@ impl kernel::syscall::UserspaceKernelBoundary for SysCall { // pointer in the sp register. // // We do not pre-allocate any stack for RV32I processes. - state.regs[R_SP] = accessible_memory_start as u32; + state.regs[R_SP] = u32::from(accessible_memory_start); // We do not use memory for UKB, so just return ok. Ok(()) @@ -149,8 +150,8 @@ impl kernel::syscall::UserspaceKernelBoundary for SysCall { unsafe fn set_syscall_return_value( &self, - _accessible_memory_start: *const u8, - _app_brk: *const u8, + _accessible_memory_start: FluxPtr, + _app_brk: FluxPtr, state: &mut Self::StoredState, return_value: kernel::syscall::SyscallReturn, ) -> Result<(), ()> { @@ -185,8 +186,8 @@ impl kernel::syscall::UserspaceKernelBoundary for SysCall { unsafe fn set_process_function( &self, - _accessible_memory_start: *const u8, - _app_brk: *const u8, + _accessible_memory_start: FluxPtr, + _app_brk: FluxPtr, state: &mut Riscv32iStoredState, callback: kernel::process::FunctionCall, ) -> Result<(), ()> { @@ -215,10 +216,10 @@ impl kernel::syscall::UserspaceKernelBoundary for SysCall { #[cfg(not(all(target_arch = "riscv32", target_os = "none")))] unsafe fn switch_to_process( &self, - _accessible_memory_start: *const u8, - _app_brk: *const u8, + _accessible_memory_start: FluxPtr, + _app_brk: FluxPtr, _state: &mut Riscv32iStoredState, - ) -> (ContextSwitchReason, Option<*const u8>) { + ) -> (ContextSwitchReason, Option) { // Convince lint that 'mcause' and 'R_A4' are used during test build let _cause = mcause::Trap::from(_state.mcause as usize); let _arg4 = _state.regs[R_A4]; @@ -651,11 +652,11 @@ impl kernel::syscall::UserspaceKernelBoundary for SysCall { let new_stack_pointer = state.regs[R_SP]; (ret, Some(new_stack_pointer as *const u8)) } - #[flux::ignore] + #[flux_rs::ignore] unsafe fn print_context( &self, - _accessible_memory_start: *const u8, - _app_brk: *const u8, + _accessible_memory_start: FluxPtr, + _app_brk: FluxPtr, state: &Riscv32iStoredState, writer: &mut dyn Write, ) { diff --git a/capsules/system/src/process_checker/basic.rs b/capsules/system/src/process_checker/basic.rs index 59478b5342..ad3455aee6 100644 --- a/capsules/system/src/process_checker/basic.rs +++ b/capsules/system/src/process_checker/basic.rs @@ -99,7 +99,7 @@ pub struct AppCheckerSha256 { } impl AppCheckerSha256 { - #[flux::trusted] + #[flux_rs::trusted] pub fn new( hash: &'static dyn Sha256Verifier<'static>, buffer: &'static mut [u8; 32], @@ -118,7 +118,7 @@ impl AppCredentialsPolicy<'static> for AppCheckerSha256 { fn require_credentials(&self) -> bool { true } - #[flux::trusted] + #[flux_rs::trusted] fn check_credentials( &self, credentials: TbfFooterV2Credentials, @@ -139,7 +139,7 @@ impl AppCredentialsPolicy<'static> for AppCheckerSha256 { _ => Err((ErrorCode::NOSUPPORT, credentials, binary)), } } - #[flux::trusted] + #[flux_rs::trusted] fn set_client(&self, client: &'static dyn AppCredentialsPolicyClient<'static>) { self.client.replace(client); } @@ -147,7 +147,7 @@ impl AppCredentialsPolicy<'static> for AppCheckerSha256 { impl ClientData<32_usize> for AppCheckerSha256 { fn add_mut_data_done(&self, _result: Result<(), ErrorCode>, _data: SubSliceMut<'static, u8>) {} - #[flux::trusted] + #[flux_rs::trusted] fn add_data_done(&self, result: Result<(), ErrorCode>, data: SubSlice<'static, u8>) { match result { Err(e) => panic!("Internal error during application binary checking. SHA256 engine threw error in adding data: {:?}", e), @@ -161,7 +161,7 @@ impl ClientData<32_usize> for AppCheckerSha256 { } impl ClientVerify<32_usize> for AppCheckerSha256 { - #[flux::trusted] + #[flux_rs::trusted] fn verification_done( &self, result: Result, @@ -218,7 +218,7 @@ pub struct AppIdAssignerNames<'a, F: Fn(&'static str) -> u32> { hasher: &'a F, } -#[flux::trusted] +#[flux_rs::trusted] impl<'a, F: Fn(&'static str) -> u32> AppIdAssignerNames<'a, F> { pub fn new(hasher: &'a F) -> Self { Self { hasher } @@ -248,7 +248,7 @@ impl<'a, F: Fn(&'static str) -> u32> AppUniqueness for AppIdAssignerNames<'a, F> } impl<'a, F: Fn(&'static str) -> u32> Compress for AppIdAssignerNames<'a, F> { - #[flux::trusted] + #[flux_rs::trusted] fn to_short_id(&self, process: &ProcessBinary) -> ShortId { let name = process.header.get_package_name().unwrap_or(""); let sum = (self.hasher)(name); @@ -271,7 +271,7 @@ pub struct AppCheckerRsaSimulated<'a> { binary: OptionalCell<&'a [u8]>, } -#[flux::trusted] +#[flux_rs::trusted] impl<'a> AppCheckerRsaSimulated<'a> { pub fn new() -> AppCheckerRsaSimulated<'a> { Self { @@ -284,7 +284,7 @@ impl<'a> AppCheckerRsaSimulated<'a> { } impl<'a> DeferredCallClient for AppCheckerRsaSimulated<'a> { - #[flux::trusted] + #[flux_rs::trusted] fn handle_deferred_call(&self) { // This checker does not actually verify the RSA signature; it // assumes the signature is valid and so accepts any RSA @@ -330,7 +330,7 @@ impl<'a> AppCredentialsPolicy<'a> for AppCheckerRsaSimulated<'a> { Err((ErrorCode::BUSY, credentials, binary)) } } - #[flux::trusted] + #[flux_rs::trusted] fn set_client(&self, client: &'a dyn AppCredentialsPolicyClient<'a>) { self.client.replace(client); } diff --git a/capsules/system/src/process_checker/signature.rs b/capsules/system/src/process_checker/signature.rs index 93958f98d4..1263f219e8 100644 --- a/capsules/system/src/process_checker/signature.rs +++ b/capsules/system/src/process_checker/signature.rs @@ -46,7 +46,7 @@ impl< const SL: usize, > AppCheckerSignature<'a, S, H, HL, SL> { - #[flux::trusted] + #[flux_rs::trusted] pub fn new( hasher: &'a H, verifier: &'a S, @@ -76,7 +76,7 @@ impl< > hil::digest::ClientData for AppCheckerSignature<'a, S, H, HL, SL> { fn add_mut_data_done(&self, _result: Result<(), ErrorCode>, _data: SubSliceMut<'static, u8>) {} - #[flux::trusted] + #[flux_rs::trusted] fn add_data_done(&self, result: Result<(), ErrorCode>, data: SubSlice<'static, u8>) { self.binary.set(data.take()); @@ -103,7 +103,7 @@ impl< } } } -#[flux::trusted] +#[flux_rs::trusted] impl< 'a, S: hil::public_key_crypto::signature::SignatureVerify<'static, HL, SL>, @@ -160,7 +160,7 @@ impl< // Needed to make the sha256 client work. } } -#[flux::trusted] +#[flux_rs::trusted] impl< 'a, S: hil::public_key_crypto::signature::SignatureVerify<'static, HL, SL>, @@ -192,7 +192,7 @@ impl< }); } } -#[flux::trusted] +#[flux_rs::trusted] impl< 'a, S: hil::public_key_crypto::signature::SignatureVerify<'static, HL, SL>, diff --git a/flux_support/src/extern_specs/iter.rs b/flux_support/src/extern_specs/iter.rs index dfa8725f3e..f1c63677cc 100644 --- a/flux_support/src/extern_specs/iter.rs +++ b/flux_support/src/extern_specs/iter.rs @@ -25,18 +25,18 @@ struct Iter<'a, T>; // } // #[flux_rs::extern_spec(std::slice)] -// #[flux::generics(T as base)] -// #[flux::assoc(fn done(x: Iter) -> bool { x.idx >= x.len })] -// #[flux::assoc(fn step(x: Iter, y: Iter) -> bool { x.idx + 1 == y.idx && x.len == y.len})] +// #[flux_rs::generics(T as base)] +// #[flux_rs::assoc(fn done(x: Iter) -> bool { x.idx >= x.len })] +// #[flux_rs::assoc(fn step(x: Iter, y: Iter) -> bool { x.idx + 1 == y.idx && x.len == y.len})] // impl<'a, T> Iterator for Iter<'a, T> { // #[flux_rs::sig(fn(self: &strg Iter[@curr_s]) -> Option<_>[curr_s.idx < curr_s.len] ensures self: Iter{next_s: curr_s.idx + 1 == next_s.idx && curr_s.len == next_s.len})] // fn next(&mut self) -> Option<&'a T>; // } // #[flux_rs::extern_spec(std::iter)] -// #[flux::generics(I as base)] -// #[flux::assoc(fn done(x: Enumerate) -> bool { ::done(x.inner)})] -// #[flux::assoc(fn step(x: Enumerate, y: Enumerate) -> bool { ::step(x.inner, y.inner)})] +// #[flux_rs::generics(I as base)] +// #[flux_rs::assoc(fn done(x: Enumerate) -> bool { ::done(x.inner)})] +// #[flux_rs::assoc(fn step(x: Enumerate, y: Enumerate) -> bool { ::step(x.inner, y.inner)})] // impl Iterator for Enumerate { // // #[flux_rs::sig(fn(self: &strg Enumerate[@curr_s]) -> Option<(usize[curr_s.idx], _)>[curr_s.idx < curr_s.len] ensures self: Enumerate{next_s: curr_s.idx + 1 == next_s.idx && curr_s.len == next_s.len})] // #[flux_rs::sig(fn(self: &strg Enumerate[@curr_s]) -> Option<(usize[curr_s.idx], _)>[!::done(curr_s.inner)] diff --git a/flux_support/src/extern_specs/slice.rs b/flux_support/src/extern_specs/slice.rs index 888c939113..869219ce30 100644 --- a/flux_support/src/extern_specs/slice.rs +++ b/flux_support/src/extern_specs/slice.rs @@ -14,7 +14,6 @@ use std::slice::{Iter, SliceIndex}; // #[assoc(fn in_bounds(idx: int, len: int) -> bool {idx < len} )] // impl SliceIndex<[T]> for usize {} - #[flux_rs::extern_spec] impl [T] { #[flux_rs::sig(fn(&[T][@len]) -> usize[len])] @@ -23,7 +22,7 @@ impl [T] { #[flux_rs::sig(fn(&[T][@len]) -> Iter[0, len])] fn iter(v: &[T]) -> Iter<'_, T>; - // #[flux::generics(I as base)] + // #[flux_rs::generics(I as base)] // #[flux_rs::sig(fn(&[T][@len], I[@idx]) -> Option<_>[>::in_bounds(idx, len)])] // fn get(&self, index: I) -> Option<&>::Output>; } diff --git a/flux_support/src/flux_ptr.rs b/flux_support/src/flux_ptr.rs index 3eb3835bac..a990ae4ef6 100644 --- a/flux_support/src/flux_ptr.rs +++ b/flux_support/src/flux_ptr.rs @@ -1,6 +1,7 @@ use core::ops::{Deref, DerefMut}; use core::ptr::NonNull; use flux_rs::{refined_by, sig}; +use std::ops::Rem; #[flux_rs::opaque] #[derive(Clone, Copy, Debug, PartialEq, Eq, Ord)] @@ -9,6 +10,51 @@ pub struct FluxPtr { inner: *mut u8, } +impl From for FluxPtr { + fn from(value: usize) -> Self { + FluxPtr { + inner: value as *mut u8, + } + } +} + +// Support cast from FluxPtr to u32 +impl From for u32 { + fn from(ptr: FluxPtr) -> u32 { + ptr.as_u32() + } +} +// convert FluxPtr to *const u8 +impl From for u8 { + fn from(ptr: FluxPtr) -> u8 { + ptr.inner as u8 + } +} +// FluxPtr to usize +impl From for usize { + fn from(ptr: FluxPtr) -> usize { + ptr.as_usize() + } +} + +// Implement Rem trait for FluxPtr +impl Rem for FluxPtr { + type Output = usize; + + fn rem(self, rhs: usize) -> Self::Output { + (self.inner as usize) % rhs + } +} + +// implement implement `AddAssign`` for FluxPtr +impl core::ops::AddAssign for FluxPtr { + fn add_assign(&mut self, rhs: usize) { + *self = FluxPtr { + inner: (self.inner as usize + rhs) as *mut u8, + } + } +} + // VTOCK-TODO: fill in these functions with obvious implementations impl FluxPtr { #[sig(fn(self: Self[@lhs], rhs: usize) -> Self{r: ((lhs + rhs <= usize::MAX) => r == lhs + rhs) && ((lhs + rhs > usize::MAX) => r == lhs + rhs - usize::MAX) })] diff --git a/libraries/tock-register-interface/src/fields.rs b/libraries/tock-register-interface/src/fields.rs index 72985b632f..ebb5cc5cb5 100644 --- a/libraries/tock-register-interface/src/fields.rs +++ b/libraries/tock-register-interface/src/fields.rs @@ -200,7 +200,7 @@ Field_impl_for!(usize); pub struct FieldValue { pub mask: T, pub value: T, - associated_register: PhantomData, + pub associated_register: PhantomData, } macro_rules! FieldValue_impl_for { From be5b65c96a3b44be95709d68562bd5a6c45c95a3 Mon Sep 17 00:00:00 2001 From: Samir Rashid Date: Thu, 26 Sep 2024 23:28:10 +0000 Subject: [PATCH 3/9] fmt --- arch/cortex-m/src/lib.rs | 1 + capsules/system/Cargo.toml | 1 + flux_support/src/extern_specs/non_null.rs | 2 +- flux_support/src/extern_specs/num.rs | 22 +++++++------- kernel/src/collections/ring_buffer.rs | 29 +++++++++---------- kernel/src/hil/can.rs | 1 - kernel/src/process_binary.rs | 1 - kernel/src/utilities/binary_write.rs | 1 - kernel/src/utilities/math.rs | 3 +- .../tock-register-interface/src/registers.rs | 1 - 10 files changed, 29 insertions(+), 33 deletions(-) diff --git a/arch/cortex-m/src/lib.rs b/arch/cortex-m/src/lib.rs index 81b8eca1ba..0c8e13af6a 100644 --- a/arch/cortex-m/src/lib.rs +++ b/arch/cortex-m/src/lib.rs @@ -7,6 +7,7 @@ #![crate_name = "cortexm"] #![crate_type = "rlib"] #![no_std] +#![feature(proc_macro_hygiene)] use core::fmt::Write; diff --git a/capsules/system/Cargo.toml b/capsules/system/Cargo.toml index 2cec4b28b3..dd41baef79 100644 --- a/capsules/system/Cargo.toml +++ b/capsules/system/Cargo.toml @@ -11,6 +11,7 @@ edition.workspace = true [dependencies] kernel = { path = "../../kernel" } tock-tbf = { path = "../../libraries/tock-tbf" } +flux-rs = { git = "https://github.com/flux-rs/flux" } [lints] workspace = true diff --git a/flux_support/src/extern_specs/non_null.rs b/flux_support/src/extern_specs/non_null.rs index 7c8761da03..51ad106e92 100644 --- a/flux_support/src/extern_specs/non_null.rs +++ b/flux_support/src/extern_specs/non_null.rs @@ -1,3 +1,3 @@ #[flux_rs::extern_spec(core::ptr)] #[refined_by(n: int)] -struct NonNull; \ No newline at end of file +struct NonNull; diff --git a/flux_support/src/extern_specs/num.rs b/flux_support/src/extern_specs/num.rs index bd61963600..96dbd963c5 100644 --- a/flux_support/src/extern_specs/num.rs +++ b/flux_support/src/extern_specs/num.rs @@ -1,21 +1,21 @@ // The spec we need to prove log_base_two #[flux_rs::extern_spec] impl u32 { - #[sig(fn(num: u32) -> u32{r: (num == 0 => r == 32) && - (num > 0 => r <= 31) && - (num > 1 => r <= 30) + #[sig(fn(num: u32) -> u32{r: (num == 0 => r == 32) && + (num > 0 => r <= 31) && + (num > 1 => r <= 30) })] fn leading_zeros(self) -> u32; - + #[sig(fn(num: u32) -> u32{r: (num == 0 => r == 32) && (num != 0 =>r <= 31) })] fn trailing_zeros(self) -> u32; } #[flux_rs::extern_spec] impl u64 { - #[sig(fn(num: u64) -> u32{r: (num == 0 => r == 64) && - (num > 0 => r <= 63) && - (num > 1 => r <= 62) + #[sig(fn(num: u64) -> u32{r: (num == 0 => r == 64) && + (num > 0 => r <= 63) && + (num > 1 => r <= 62) })] fn leading_zeros(self) -> u32; } @@ -23,9 +23,9 @@ impl u64 { // Only works when usize is 32-bits #[flux_rs::extern_spec] impl usize { - #[sig(fn(num: usize{num < 4294967295}) -> u32{r: (num == 0 => r == 32) && - (num > 0 => r <= 31) && - (num > 1 => r <= 30) + #[sig(fn(num: usize{num < 4294967295}) -> u32{r: (num == 0 => r == 32) && + (num > 0 => r <= 31) && + (num > 1 => r <= 30) })] fn leading_zeros(self) -> u32; -} \ No newline at end of file +} diff --git a/kernel/src/collections/ring_buffer.rs b/kernel/src/collections/ring_buffer.rs index 766645193b..51b5392fdf 100644 --- a/kernel/src/collections/ring_buffer.rs +++ b/kernel/src/collections/ring_buffer.rs @@ -6,8 +6,6 @@ use crate::collections::queue; - - #[flux_rs::refined_by(ring_len: int, head: int, tail: int)] #[flux_rs::invariant(ring_len > 1)] pub struct RingBuffer<'a, T: 'a> { @@ -27,7 +25,6 @@ flux_rs::defs! { fn next_tl(rb: RingBuffer) -> int { rb_next(rb.tail, rb.ring_len) } } - impl<'a, T: Copy> RingBuffer<'a, T> { #[flux_rs::sig(fn({&mut [T][@ring_len] | ring_len > 1}) -> RingBuffer[ring_len, 0, 0])] pub fn new(ring: &'a mut [T]) -> RingBuffer<'a, T> { @@ -102,12 +99,12 @@ impl queue::Queue for RingBuffer<'_, T> { } #[flux_rs::sig( - fn(self: &strg RingBuffer[@ring_len, @hd, @tl], _) -> bool - ensures self: RingBuffer{ rg: + fn(self: &strg RingBuffer[@ring_len, @hd, @tl], _) -> bool + ensures self: RingBuffer{ rg: // if this is the case then we've overlapped and will overwrite a space // that hasn't been read - rg.head != rg.tail - && + rg.head != rg.tail + && // either we're full and don't update // hd == rb_next(tl, ring_len) -> rg.tail == tl && rg.head == hd (hd == rb_next(tl, ring_len) => rg.tail == tl && rg.head == hd) @@ -129,13 +126,13 @@ impl queue::Queue for RingBuffer<'_, T> { } #[flux_rs::sig( - fn(self: &strg RingBuffer[@old], _) -> Option - ensures self: RingBuffer{ rg: + fn(self: &strg RingBuffer[@old], _) -> Option + ensures self: RingBuffer{ rg: // if this is the case then we've overlapped and will overwrite a space // that hasn't been read rg.head != rg.tail - && - // either the buffer is full so we dequeue and then enqueue + && + // either the buffer is full so we dequeue and then enqueue (full(old) => (rg.head == next_hd(old) && rg.tail == next_tl(old))) && // or we have space so we just enqueue @@ -157,9 +154,9 @@ impl queue::Queue for RingBuffer<'_, T> { } #[flux_rs::sig( - fn(self: &strg RingBuffer[@ring_len, @hd, @tl]) -> Option + fn(self: &strg RingBuffer[@ring_len, @hd, @tl]) -> Option ensures self: RingBuffer{ - rg: + rg: (hd == tl => (rg.head == hd && rg.tail == tl && rg.head == rg.tail)) && (hd != tl => rg.head == rb_next(hd, ring_len)) @@ -183,7 +180,7 @@ impl queue::Queue for RingBuffer<'_, T> { /// /// If an element was removed, this function returns it as `Some(elem)`. #[flux_rs::sig( - fn(self: &strg RingBuffer[@ring_len, @hd, @tl], _) -> Option + fn(self: &strg RingBuffer[@ring_len, @hd, @tl], _) -> Option ensures self: RingBuffer{rg: rg.tail < rg.ring_len} )] // NOTE: May want to strengthen this to talk about correctness @@ -214,7 +211,7 @@ impl queue::Queue for RingBuffer<'_, T> { } #[flux_rs::sig( - fn(self: &strg RingBuffer[@ring_len, @hd, @tl]) + fn(self: &strg RingBuffer[@ring_len, @hd, @tl]) ensures self: RingBuffer[ring_len, 0, 0] )] fn empty(&mut self) { @@ -223,7 +220,7 @@ impl queue::Queue for RingBuffer<'_, T> { } #[flux_rs::sig( - fn(self: &strg RingBuffer[@ring_len, @hd, @tl], _) + fn(self: &strg RingBuffer[@ring_len, @hd, @tl], _) ensures self: RingBuffer{rg: rg.tail < rg.ring_len} )] fn retain(&mut self, mut f: F) diff --git a/kernel/src/hil/can.rs b/kernel/src/hil/can.rs index 55ed9ba2aa..a9b77ff20b 100644 --- a/kernel/src/hil/can.rs +++ b/kernel/src/hil/can.rs @@ -320,7 +320,6 @@ impl StandardBitTiming for T { } ts = clock_rate / (prescaler * bitrate); - sample_point_err = calc_sample_point_err( sp, ts, diff --git a/kernel/src/process_binary.rs b/kernel/src/process_binary.rs index 2c930de87e..4776bbdab3 100644 --- a/kernel/src/process_binary.rs +++ b/kernel/src/process_binary.rs @@ -144,7 +144,6 @@ impl ProcessBinary { tbf_version: u16, require_kernel_version: bool, ) -> Result { - // Get a slice for just the app header. let header_flash = app_flash .get(0..header_length) diff --git a/kernel/src/utilities/binary_write.rs b/kernel/src/utilities/binary_write.rs index 040d697bb6..3f00e75d3c 100644 --- a/kernel/src/utilities/binary_write.rs +++ b/kernel/src/utilities/binary_write.rs @@ -8,7 +8,6 @@ //! binary slice. This mirrors the `core::fmt::Write` interface but doesn't //! expect a `&str`. - /// Interface for writing an arbitrary buffer. pub trait BinaryWrite { /// Write the `buffer` to some underlying print mechanism. diff --git a/kernel/src/utilities/math.rs b/kernel/src/utilities/math.rs index 67f376ac4f..9d1f9eda46 100644 --- a/kernel/src/utilities/math.rs +++ b/kernel/src/utilities/math.rs @@ -24,7 +24,8 @@ pub fn closest_power_of_two(mut num: u32) -> u32 { num } -#[flux_rs::trusted] // bitwise arithmetic +#[flux_rs::trusted] +// bitwise arithmetic // 2147483648 is half of u32::MAX. Anything higher than that deviates from closest_power_of_two // I added this function to avoid unnecessary downcasts, which can be dangerous. #[flux_rs::sig(fn(num: usize) -> usize{r: (num < 2147483648 => r > num)})] diff --git a/libraries/tock-register-interface/src/registers.rs b/libraries/tock-register-interface/src/registers.rs index 5fa796acd5..b72983102f 100644 --- a/libraries/tock-register-interface/src/registers.rs +++ b/libraries/tock-register-interface/src/registers.rs @@ -110,7 +110,6 @@ impl Readable for ReadOnly { // be removed. We `allow(dead_code)` here to suppress this warning. #[allow(dead_code)] #[repr(transparent)] -#[allow(dead_code)] pub struct WriteOnly { value: UnsafeCell, associated_register: PhantomData, From b2031907ac9b183492ee7b2eb6efce0df3701732 Mon Sep 17 00:00:00 2001 From: Samir Rashid Date: Mon, 30 Sep 2024 21:37:46 -0700 Subject: [PATCH 4/9] clippy is happy --- arch/rv32i/src/lib.rs | 1 - arch/rv32i/src/support.rs | 2 -- arch/rv32i/src/syscall.rs | 1 - flux_support/src/flux_ptr.rs | 14 +++++++++++--- kernel/src/grant.rs | 1 + kernel/src/hil/can.rs | 1 + kernel/src/kernel.rs | 1 + kernel/src/memop.rs | 1 + kernel/src/platform/mpu.rs | 1 + kernel/src/process.rs | 1 + kernel/src/process_binary.rs | 1 + kernel/src/process_loading.rs | 1 + kernel/src/process_standard.rs | 3 ++- kernel/src/processbuffer.rs | 1 + kernel/src/syscall.rs | 1 + kernel/src/utilities/leasable_buffer.rs | 1 + 16 files changed, 24 insertions(+), 8 deletions(-) diff --git a/arch/rv32i/src/lib.rs b/arch/rv32i/src/lib.rs index c77a36a807..0035262f19 100644 --- a/arch/rv32i/src/lib.rs +++ b/arch/rv32i/src/lib.rs @@ -8,7 +8,6 @@ #![crate_name = "rv32i"] #![crate_type = "rlib"] #![no_std] -use flux_rs::*; use core::fmt::Write; diff --git a/arch/rv32i/src/support.rs b/arch/rv32i/src/support.rs index 05ae44b6b5..2dce9ec7a3 100644 --- a/arch/rv32i/src/support.rs +++ b/arch/rv32i/src/support.rs @@ -5,8 +5,6 @@ //! Core low-level operations. use crate::csr::{mstatus::mstatus, CSR}; -use flux_rs::*; -use flux_support::*; #[cfg(all(target_arch = "riscv32", target_os = "none"))] #[inline(always)] diff --git a/arch/rv32i/src/syscall.rs b/arch/rv32i/src/syscall.rs index 83b804f8fe..6b78513f59 100644 --- a/arch/rv32i/src/syscall.rs +++ b/arch/rv32i/src/syscall.rs @@ -9,7 +9,6 @@ use core::mem::size_of; use core::ops::Range; use crate::csr::mcause; -use flux_rs::*; use flux_support::*; use kernel::errorcode::ErrorCode; use kernel::syscall::ContextSwitchReason; diff --git a/flux_support/src/flux_ptr.rs b/flux_support/src/flux_ptr.rs index a990ae4ef6..84a16b8c04 100644 --- a/flux_support/src/flux_ptr.rs +++ b/flux_support/src/flux_ptr.rs @@ -4,7 +4,7 @@ use flux_rs::{refined_by, sig}; use std::ops::Rem; #[flux_rs::opaque] -#[derive(Clone, Copy, Debug, PartialEq, Eq, Ord)] +#[derive(Clone, Copy, Debug, PartialEq, Eq)] #[refined_by(ptr: int)] pub struct FluxPtr { inner: *mut u8, @@ -55,6 +55,12 @@ impl core::ops::AddAssign for FluxPtr { } } +impl core::cmp::Ord for FluxPtr { + fn cmp(&self, other: &Self) -> core::cmp::Ordering { + self.as_usize().cmp(&other.as_usize()) + } +} + // VTOCK-TODO: fill in these functions with obvious implementations impl FluxPtr { #[sig(fn(self: Self[@lhs], rhs: usize) -> Self{r: ((lhs + rhs <= usize::MAX) => r == lhs + rhs) && ((lhs + rhs > usize::MAX) => r == lhs + rhs - usize::MAX) })] @@ -96,10 +102,12 @@ impl FluxPtr { unimplemented!() } + /// # Safety pub const unsafe fn offset(self, _count: isize) -> Self { unimplemented!() } + /// # Safety pub const unsafe fn add(self, _count: usize) -> Self { unimplemented!() } @@ -111,8 +119,8 @@ impl FluxPtr { #[flux_rs::trusted] impl PartialOrd for FluxPtr { - fn partial_cmp(&self, _other: &Self) -> Option { - todo!() + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) } // Provided methods diff --git a/kernel/src/grant.rs b/kernel/src/grant.rs index f7f91ed097..3d7bf40f99 100644 --- a/kernel/src/grant.rs +++ b/kernel/src/grant.rs @@ -139,6 +139,7 @@ use crate::processbuffer::{ReadOnlyProcessBuffer, ReadWriteProcessBuffer}; use crate::processbuffer::{ReadOnlyProcessBufferRef, ReadWriteProcessBufferRef}; use crate::upcall::{Upcall, UpcallError, UpcallId}; use crate::ErrorCode; +#[allow(clippy::wildcard_imports)] use flux_support::*; /// Tracks how many upcalls a grant instance supports automatically. diff --git a/kernel/src/hil/can.rs b/kernel/src/hil/can.rs index a9b77ff20b..22bc47feec 100644 --- a/kernel/src/hil/can.rs +++ b/kernel/src/hil/can.rs @@ -39,6 +39,7 @@ //! use crate::ErrorCode; +#[allow(clippy::wildcard_imports)] use flux_support::*; pub const STANDARD_CAN_PACKET_SIZE: usize = 8; diff --git a/kernel/src/kernel.rs b/kernel/src/kernel.rs index 0477109265..e9ed3f8aa9 100644 --- a/kernel/src/kernel.rs +++ b/kernel/src/kernel.rs @@ -34,6 +34,7 @@ use crate::syscall::{Syscall, YieldCall}; use crate::syscall_driver::CommandReturn; use crate::upcall::{Upcall, UpcallId}; use crate::utilities::cells::NumericCellExt; +#[allow(clippy::wildcard_imports)] use flux_support::*; /// Threshold in microseconds to consider a process's timeslice to be exhausted. diff --git a/kernel/src/memop.rs b/kernel/src/memop.rs index 2c343b09f5..46ac33cf03 100644 --- a/kernel/src/memop.rs +++ b/kernel/src/memop.rs @@ -7,6 +7,7 @@ use crate::process::Process; use crate::syscall::SyscallReturn; use crate::ErrorCode; +#[allow(clippy::wildcard_imports)] use flux_support::*; /// Handle the `memop` syscall. diff --git a/kernel/src/platform/mpu.rs b/kernel/src/platform/mpu.rs index 813810ea5f..b2dc554226 100644 --- a/kernel/src/platform/mpu.rs +++ b/kernel/src/platform/mpu.rs @@ -6,6 +6,7 @@ use core::cmp; use core::fmt::{self, Display}; +#[allow(clippy::wildcard_imports)] use flux_support::*; /// User mode access permissions. diff --git a/kernel/src/process.rs b/kernel/src/process.rs index 9f96e08389..0ea905ebdb 100644 --- a/kernel/src/process.rs +++ b/kernel/src/process.rs @@ -19,6 +19,7 @@ use crate::processbuffer::{ReadOnlyProcessBuffer, ReadWriteProcessBuffer}; use crate::storage_permissions; use crate::syscall::{self, Syscall, SyscallReturn}; use crate::upcall::UpcallId; +#[allow(clippy::wildcard_imports)] use flux_support::*; use tock_tbf::types::CommandPermissions; diff --git a/kernel/src/process_binary.rs b/kernel/src/process_binary.rs index 4776bbdab3..225c5d46a8 100644 --- a/kernel/src/process_binary.rs +++ b/kernel/src/process_binary.rs @@ -13,6 +13,7 @@ use crate::config; use crate::debug; use crate::process_checker::AcceptedCredential; use crate::utilities::cells::OptionalCell; +#[allow(clippy::wildcard_imports)] use flux_support::*; /// Errors resulting from trying to load a process binary structure from flash. diff --git a/kernel/src/process_loading.rs b/kernel/src/process_loading.rs index fc61f0f9cd..2d8106522a 100644 --- a/kernel/src/process_loading.rs +++ b/kernel/src/process_loading.rs @@ -28,6 +28,7 @@ use crate::process_checker::{AppIdPolicy, ProcessCheckError, ProcessCheckerMachi use crate::process_policies::ProcessFaultPolicy; use crate::process_standard::ProcessStandard; use crate::utilities::cells::{MapCell, OptionalCell}; +#[allow(clippy::wildcard_imports)] use flux_support::*; /// Errors that can occur when trying to load and create processes. diff --git a/kernel/src/process_standard.rs b/kernel/src/process_standard.rs index cf2de94c71..2ef2497a66 100644 --- a/kernel/src/process_standard.rs +++ b/kernel/src/process_standard.rs @@ -13,6 +13,7 @@ use core::fmt::Write; use core::num::NonZeroU32; use core::ptr::NonNull; use core::{mem, slice, str}; +#[allow(clippy::wildcard_imports)] use flux_support::*; use crate::collections::queue::Queue; @@ -2155,7 +2156,7 @@ impl ProcessStandard<'_, C> { /// The lowest address of the grant region for the process. fn kernel_memory_break(&self) -> FluxPtrU8Mut { - self.breaks.get().app_break + self.breaks.get().kernel_memory_break } /// Return the highest address the process has access to, or the current diff --git a/kernel/src/processbuffer.rs b/kernel/src/processbuffer.rs index f801999fa8..074bb8a8d2 100644 --- a/kernel/src/processbuffer.rs +++ b/kernel/src/processbuffer.rs @@ -30,6 +30,7 @@ use crate::ErrorCode; use core::cell::Cell; use core::marker::PhantomData; use core::ops::{Deref, Index, Range, RangeFrom, RangeTo}; +#[allow(clippy::wildcard_imports)] use flux_support::*; /// Convert a process buffer's internal representation to a diff --git a/kernel/src/syscall.rs b/kernel/src/syscall.rs index 3a2f5e2ee9..94b149b784 100644 --- a/kernel/src/syscall.rs +++ b/kernel/src/syscall.rs @@ -71,6 +71,7 @@ use core::fmt::Write; use crate::errorcode::ErrorCode; use crate::process; pub use crate::syscall_driver::{CommandReturn, SyscallDriver}; +#[allow(clippy::wildcard_imports)] use flux_support::*; /// Helper function to split a [`u64`] into a higher and lower [`u32`]. diff --git a/kernel/src/utilities/leasable_buffer.rs b/kernel/src/utilities/leasable_buffer.rs index 77fbde08a1..2d388801d3 100644 --- a/kernel/src/utilities/leasable_buffer.rs +++ b/kernel/src/utilities/leasable_buffer.rs @@ -170,6 +170,7 @@ use core::ops::{Bound, RangeBounds}; use core::ops::{Index, IndexMut}; use core::slice::SliceIndex; +#[allow(clippy::wildcard_imports)] use flux_support::*; /// A mutable leasable buffer implementation. From 66b31498c4b1254c748c8d89e43954f83f3cfd0f Mon Sep 17 00:00:00 2001 From: Samir Rashid Date: Mon, 30 Sep 2024 22:28:05 -0700 Subject: [PATCH 5/9] test ci --- .vscode/settings.json | 6 ++++++ arch/rv32i/Cargo.toml | 2 +- capsules/system/src/process_checker/signature.rs | 1 + chips/virtio/Cargo.toml | 1 + kernel/src/deferred_call.rs | 2 +- shell.nix | 2 ++ 6 files changed, 12 insertions(+), 2 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index e20461eb81..fb8f1fb6e5 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -6,4 +6,10 @@ "RUSTUP_TOOLCHAIN": "nightly-2024-07-08" }, "rust-analyzer.check.allTargets": false, + "rust-analyzer.check.overrideCommand": [ + "cargo", + "flux", + "--workspace", + "--message-format=json-diagnostic-rendered-ansi" + ] } diff --git a/arch/rv32i/Cargo.toml b/arch/rv32i/Cargo.toml index 12f3bc422a..8ef36604d4 100644 --- a/arch/rv32i/Cargo.toml +++ b/arch/rv32i/Cargo.toml @@ -17,7 +17,7 @@ flux_support = { path = "../../flux_support" } tock-registers = { path = "../../libraries/tock-register-interface" } riscv-csr = { path = "../../libraries/riscv-csr" } riscv = { path = "../riscv" } -flux-rs = { git = "https://github.com/flux-rs/flux" } +flux-rs = { git = "https://github.com/flux-rs/flux.git" } [lints] workspace = true diff --git a/capsules/system/src/process_checker/signature.rs b/capsules/system/src/process_checker/signature.rs index 1263f219e8..c03cc92ce4 100644 --- a/capsules/system/src/process_checker/signature.rs +++ b/capsules/system/src/process_checker/signature.rs @@ -3,6 +3,7 @@ // Copyright Tock Contributors 2024. //! Signature credential checker for checking process credentials. +use flux_rs::*; use kernel::hil; use kernel::process_checker::CheckResult; use kernel::process_checker::{AppCredentialsPolicy, AppCredentialsPolicyClient}; diff --git a/chips/virtio/Cargo.toml b/chips/virtio/Cargo.toml index 6d3756e2c2..2b11702875 100644 --- a/chips/virtio/Cargo.toml +++ b/chips/virtio/Cargo.toml @@ -10,6 +10,7 @@ edition.workspace = true [dependencies] kernel = { path = "../../kernel" } +flux-rs = { git = "https://github.com/flux-rs/flux" } [lints] workspace = true diff --git a/kernel/src/deferred_call.rs b/kernel/src/deferred_call.rs index 061b485d5c..aa711c871c 100644 --- a/kernel/src/deferred_call.rs +++ b/kernel/src/deferred_call.rs @@ -98,7 +98,7 @@ impl<'a> DynDefCallRef<'a> { #[flux_rs::trusted] // unsupported cast `PointerCoercion(ClosureFnPointer(Safe))` fn new(x: &'a T) -> Self { Self { - data: x as *const _ as *const (), + data: core::ptr::from_ref(x) as *const (), callback: |p| unsafe { T::handle_deferred_call(&*p.cast()) }, _lifetime: PhantomData, } diff --git a/shell.nix b/shell.nix index cf994f17a8..b1ec39a26e 100644 --- a/shell.nix +++ b/shell.nix @@ -63,6 +63,7 @@ in # --- CI support packages --- qemu + z3 # --- Flashing tools --- # If your board requires J-Link to flash and you are on NixOS, @@ -88,5 +89,6 @@ in shellHook = '' unset OBJCOPY unset OBJDUMP + PATH=/home/mod/.local/bin:$PATH ''; } From 5830a93b839f455bd6c0c72b0ff5bd6a9cd05f0b Mon Sep 17 00:00:00 2001 From: Samir Rashid Date: Mon, 30 Sep 2024 22:42:26 -0700 Subject: [PATCH 6/9] fix license checker --- .lcignore | 2 ++ capsules/system/src/process_checker/signature.rs | 2 +- flux_support/src/flux_ptr.rs | 4 ++++ flux_support/src/lib.rs | 1 + 4 files changed, 8 insertions(+), 1 deletion(-) diff --git a/.lcignore b/.lcignore index 14c91de026..d49906b495 100644 --- a/.lcignore +++ b/.lcignore @@ -30,3 +30,5 @@ /tools/license-checker/testdata/many_errors.rs /tools/license-checker/testdata/no_copyright.rs /tools/license-checker/testdata/no_spdx.rs + +/flux_support/* diff --git a/capsules/system/src/process_checker/signature.rs b/capsules/system/src/process_checker/signature.rs index c03cc92ce4..d8f4d552cd 100644 --- a/capsules/system/src/process_checker/signature.rs +++ b/capsules/system/src/process_checker/signature.rs @@ -1,9 +1,9 @@ // Licensed under the Apache License, Version 2.0 or the MIT License. // SPDX-License-Identifier: Apache-2.0 OR MIT // Copyright Tock Contributors 2024. + //! Signature credential checker for checking process credentials. -use flux_rs::*; use kernel::hil; use kernel::process_checker::CheckResult; use kernel::process_checker::{AppCredentialsPolicy, AppCredentialsPolicyClient}; diff --git a/flux_support/src/flux_ptr.rs b/flux_support/src/flux_ptr.rs index 84a16b8c04..7d622569ae 100644 --- a/flux_support/src/flux_ptr.rs +++ b/flux_support/src/flux_ptr.rs @@ -1,4 +1,8 @@ +use core::cmp::PartialOrd; +use core::convert::From; use core::ops::{Deref, DerefMut}; +use core::option::Option; +use core::option::Option::Some; use core::ptr::NonNull; use flux_rs::{refined_by, sig}; use std::ops::Rem; diff --git a/flux_support/src/lib.rs b/flux_support/src/lib.rs index b4ac0889f9..afa2422a60 100644 --- a/flux_support/src/lib.rs +++ b/flux_support/src/lib.rs @@ -3,6 +3,7 @@ mod flux_ptr; mod flux_range; mod flux_register_interface; mod math; +use core::panic; pub use flux_ptr::*; pub use flux_range::*; pub use flux_register_interface::*; From 527bbe327f412b05def42aeed5bc0511677bcb49 Mon Sep 17 00:00:00 2001 From: Samir Rashid Date: Mon, 30 Sep 2024 22:54:46 -0700 Subject: [PATCH 7/9] typo --- capsules/core/src/adc.rs | 2 +- flux_support/README.md | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) create mode 100644 flux_support/README.md diff --git a/capsules/core/src/adc.rs b/capsules/core/src/adc.rs index 446f3d3cf8..d4380b7a83 100644 --- a/capsules/core/src/adc.rs +++ b/capsules/core/src/adc.rs @@ -1060,7 +1060,7 @@ impl<'a, A: hil::adc::Adc<'a> + hil::adc::AdcHighSpeed<'a>> hil::adc::HighSpeedC kernel_data .schedule_upcall( 0, - (self.mode.get() as usize, len_chan, buf_ptr as usize), + (self.mode.get() as usize, len_chan, usize::from(buf_ptr)), ) .ok(); diff --git a/flux_support/README.md b/flux_support/README.md new file mode 100644 index 0000000000..c378e817cc --- /dev/null +++ b/flux_support/README.md @@ -0,0 +1 @@ +Helper Flux functions From 9bc12371f7745c960174d6dbea1e0ab5c4aae50f Mon Sep 17 00:00:00 2001 From: Samir Rashid Date: Mon, 30 Sep 2024 23:07:16 -0700 Subject: [PATCH 8/9] no std allowed --- flux_support/src/extern_specs/iter.rs | 2 +- flux_support/src/extern_specs/slice.rs | 2 +- flux_support/src/flux_ptr.rs | 10 +++++++++- flux_support/src/flux_range.rs | 7 +++++++ flux_support/src/flux_register_interface.rs | 4 ++++ 5 files changed, 22 insertions(+), 3 deletions(-) diff --git a/flux_support/src/extern_specs/iter.rs b/flux_support/src/extern_specs/iter.rs index f1c63677cc..b101fb22e4 100644 --- a/flux_support/src/extern_specs/iter.rs +++ b/flux_support/src/extern_specs/iter.rs @@ -1,6 +1,6 @@ #![allow(unused)] use crate::assert; -use std::slice::Iter; +use std::slice::Iter; // TODO: not allowed to use std #[flux_rs::extern_spec(std::slice)] #[flux_rs::refined_by(idx: int, len: int)] diff --git a/flux_support/src/extern_specs/slice.rs b/flux_support/src/extern_specs/slice.rs index 869219ce30..eab0303537 100644 --- a/flux_support/src/extern_specs/slice.rs +++ b/flux_support/src/extern_specs/slice.rs @@ -1,5 +1,5 @@ #![allow(unused)] -use std::slice::{Iter, SliceIndex}; +use std::slice::{Iter, SliceIndex}; // TODO: not allowed to use std // #[flux_rs::extern_spec] // #[generics(Self as base, T as base)] diff --git a/flux_support/src/flux_ptr.rs b/flux_support/src/flux_ptr.rs index 7d622569ae..1ccd40b7af 100644 --- a/flux_support/src/flux_ptr.rs +++ b/flux_support/src/flux_ptr.rs @@ -1,11 +1,19 @@ +use core::clone::Clone; +use core::cmp::Eq; +use core::cmp::PartialEq; use core::cmp::PartialOrd; use core::convert::From; +use core::fmt::Debug; +use core::marker::Copy; use core::ops::{Deref, DerefMut}; use core::option::Option; use core::option::Option::Some; +use core::prelude::rust_2021::derive; use core::ptr::NonNull; +use core::todo; +use core::unimplemented; use flux_rs::{refined_by, sig}; -use std::ops::Rem; +use std::ops::Rem; // TODO: not allowed to use std #[flux_rs::opaque] #[derive(Clone, Copy, Debug, PartialEq, Eq)] diff --git a/flux_support/src/flux_range.rs b/flux_support/src/flux_range.rs index 1cb0c0c468..58910ad2a6 100644 --- a/flux_support/src/flux_range.rs +++ b/flux_support/src/flux_range.rs @@ -1,3 +1,10 @@ +use core::clone::Clone; +use core::cmp::Eq; +use core::cmp::PartialEq; +use core::fmt::Debug; +use core::marker::Copy; +use core::prelude::rust_2021::derive; + #[derive(Clone, Copy, Debug, PartialEq, Eq)] #[flux_rs::refined_by(start: int, end: int)] pub struct FluxRange { diff --git a/flux_support/src/flux_register_interface.rs b/flux_support/src/flux_register_interface.rs index dd3b753be0..39bbe63b2f 100644 --- a/flux_support/src/flux_register_interface.rs +++ b/flux_support/src/flux_register_interface.rs @@ -1,5 +1,9 @@ // VTOCK-TODO: how to do defs without breaking compilation +use core::clone::Clone; +use core::marker::Copy; use core::ops::{Add, AddAssign}; +use core::prelude::rust_2021::derive; +use core::unimplemented; pub use tock_registers::debug; pub use tock_registers::fields::TryFromValue; use tock_registers::fields::{Field, FieldValue}; From b90ff3afb2a1718bbb3bd8b6550217e39ac2e584 Mon Sep 17 00:00:00 2001 From: Samir Rashid Date: Tue, 1 Oct 2024 22:55:13 -0700 Subject: [PATCH 9/9] mark `flux_support` as `#![no_std]` --- flux_support/src/extern_specs/iter.rs | 4 ++-- flux_support/src/extern_specs/mem.rs | 2 +- flux_support/src/extern_specs/slice.rs | 2 +- flux_support/src/flux_ptr.rs | 7 ++++++- flux_support/src/lib.rs | 2 ++ 5 files changed, 12 insertions(+), 5 deletions(-) diff --git a/flux_support/src/extern_specs/iter.rs b/flux_support/src/extern_specs/iter.rs index b101fb22e4..5dc7b40127 100644 --- a/flux_support/src/extern_specs/iter.rs +++ b/flux_support/src/extern_specs/iter.rs @@ -1,8 +1,8 @@ #![allow(unused)] use crate::assert; -use std::slice::Iter; // TODO: not allowed to use std +use core::slice::Iter; -#[flux_rs::extern_spec(std::slice)] +#[flux_rs::extern_spec(core::slice)] #[flux_rs::refined_by(idx: int, len: int)] struct Iter<'a, T>; diff --git a/flux_support/src/extern_specs/mem.rs b/flux_support/src/extern_specs/mem.rs index f70200d685..6479a63993 100644 --- a/flux_support/src/extern_specs/mem.rs +++ b/flux_support/src/extern_specs/mem.rs @@ -1,5 +1,5 @@ // alignment of data types must be at least 0: // https://doc.rust-lang.org/reference/type-layout.html -#[flux_rs::extern_spec(std::mem)] +#[flux_rs::extern_spec(core::mem)] #[flux_rs::sig(fn() -> usize{align: align > 0})] fn align_of() -> usize; diff --git a/flux_support/src/extern_specs/slice.rs b/flux_support/src/extern_specs/slice.rs index eab0303537..03da9dac45 100644 --- a/flux_support/src/extern_specs/slice.rs +++ b/flux_support/src/extern_specs/slice.rs @@ -1,5 +1,5 @@ #![allow(unused)] -use std::slice::{Iter, SliceIndex}; // TODO: not allowed to use std +use core::slice::{Iter, SliceIndex}; // TODO: not allowed to use std // #[flux_rs::extern_spec] // #[generics(Self as base, T as base)] diff --git a/flux_support/src/flux_ptr.rs b/flux_support/src/flux_ptr.rs index 1ccd40b7af..758b5223a1 100644 --- a/flux_support/src/flux_ptr.rs +++ b/flux_support/src/flux_ptr.rs @@ -1,10 +1,12 @@ use core::clone::Clone; use core::cmp::Eq; +use core::cmp::Ord; use core::cmp::PartialEq; use core::cmp::PartialOrd; use core::convert::From; use core::fmt::Debug; use core::marker::Copy; +use core::ops::Rem; use core::ops::{Deref, DerefMut}; use core::option::Option; use core::option::Option::Some; @@ -13,7 +15,6 @@ use core::ptr::NonNull; use core::todo; use core::unimplemented; use flux_rs::{refined_by, sig}; -use std::ops::Rem; // TODO: not allowed to use std #[flux_rs::opaque] #[derive(Clone, Copy, Debug, PartialEq, Eq)] @@ -22,6 +23,7 @@ pub struct FluxPtr { inner: *mut u8, } +#[flux_rs::trusted] impl From for FluxPtr { fn from(value: usize) -> Self { FluxPtr { @@ -37,6 +39,7 @@ impl From for u32 { } } // convert FluxPtr to *const u8 +#[flux_rs::trusted] impl From for u8 { fn from(ptr: FluxPtr) -> u8 { ptr.inner as u8 @@ -50,6 +53,7 @@ impl From for usize { } // Implement Rem trait for FluxPtr +#[flux_rs::trusted] impl Rem for FluxPtr { type Output = usize; @@ -59,6 +63,7 @@ impl Rem for FluxPtr { } // implement implement `AddAssign`` for FluxPtr +#[flux_rs::trusted] impl core::ops::AddAssign for FluxPtr { fn add_assign(&mut self, rhs: usize) { *self = FluxPtr { diff --git a/flux_support/src/lib.rs b/flux_support/src/lib.rs index afa2422a60..f46a979f92 100644 --- a/flux_support/src/lib.rs +++ b/flux_support/src/lib.rs @@ -1,3 +1,5 @@ +#![no_std] + mod extern_specs; mod flux_ptr; mod flux_range;