From e7062520ae92dd6c31426cd4b3a2a61ea382bddb Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 29 Oct 2024 10:29:16 -0700 Subject: [PATCH 1/4] update to account for trait-impl checks --- kernel/Cargo.toml | 3 ++- kernel/src/collections/queue.rs | 6 ++++++ kernel/src/hil/time.rs | 8 ++++++++ kernel/src/processbuffer.rs | 4 +++- rust-toolchain.toml | 9 ++------- 5 files changed, 21 insertions(+), 9 deletions(-) diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml index db97ff0dfc..25194cf6f1 100644 --- a/kernel/Cargo.toml +++ b/kernel/Cargo.toml @@ -16,7 +16,8 @@ tock-registers = { path = "../libraries/tock-register-interface" } tock-cells = { path = "../libraries/tock-cells" } tock-tbf = { path = "../libraries/tock-tbf" } flux_support = { path = "../flux_support" } -flux-rs = { git = "https://github.com/flux-rs/flux.git" } +# flux-rs = { git = "https://github.com/flux-rs/flux.git" } +flux-rs = { path = "../../flux/lib/flux-rs" } # In general, Tock discourages the use of cargo features. However for certain # kernel crate configuration, we have not found reasonable alternatives to diff --git a/kernel/src/collections/queue.rs b/kernel/src/collections/queue.rs index 08f1c626c9..906f80d3eb 100644 --- a/kernel/src/collections/queue.rs +++ b/kernel/src/collections/queue.rs @@ -16,23 +16,29 @@ pub trait Queue { /// If the queue isn't full, add a new element to the back of the queue. /// Returns whether the element was added. + #[flux_rs::trusted_impl] fn enqueue(&mut self, val: T) -> bool; /// Add a new element to the back of the queue, poping one from the front if necessary. + #[flux_rs::trusted_impl] fn push(&mut self, val: T) -> Option; /// Remove the element from the front of the queue. + #[flux_rs::trusted_impl] fn dequeue(&mut self) -> Option; /// Remove and return one (the first) element that matches the predicate. + #[flux_rs::trusted_impl] fn remove_first_matching(&mut self, f: F) -> Option where F: Fn(&T) -> bool; /// Remove all elements from the ring buffer. + #[flux_rs::trusted_impl] fn empty(&mut self); /// Retains only the elements that satisfy the predicate. + #[flux_rs::trusted_impl] fn retain(&mut self, f: F) where F: FnMut(&T) -> bool; diff --git a/kernel/src/hil/time.rs b/kernel/src/hil/time.rs index ab4fe326e5..7d3da0ac2c 100644 --- a/kernel/src/hil/time.rs +++ b/kernel/src/hil/time.rs @@ -134,6 +134,7 @@ pub trait Ticks: Clone + Copy + From + fmt::Debug + Ord + PartialOrd + Eq { /// Scales the ticks by the specified numerator and denominator. If the resulting value would /// be greater than u32,`u32::MAX` is returned instead + #[flux_rs::sig(fn(Self, u32, u32{denom: denom > 0}) -> u32)] fn saturating_scale(self, numerator: u32, denominator: u32) -> u32; } @@ -402,6 +403,7 @@ pub trait Timer<'a>: Time { #[derive(Debug)] pub enum Freq100MHz {} impl Frequency for Freq100MHz { + #[flux_rs::sig(fn() -> u32{r: r > 0})] fn frequency() -> u32 { 100_000_000 } @@ -411,6 +413,7 @@ impl Frequency for Freq100MHz { #[derive(Debug)] pub enum Freq16MHz {} impl Frequency for Freq16MHz { + #[flux_rs::sig(fn() -> u32{r: r > 0})] fn frequency() -> u32 { 16_000_000 } @@ -419,6 +422,7 @@ impl Frequency for Freq16MHz { /// 10MHz `Frequency` pub enum Freq10MHz {} impl Frequency for Freq10MHz { + #[flux_rs::sig(fn() -> u32{r: r > 0})] fn frequency() -> u32 { 10_000_000 } @@ -428,6 +432,7 @@ impl Frequency for Freq10MHz { #[derive(Debug)] pub enum Freq1MHz {} impl Frequency for Freq1MHz { + #[flux_rs::sig(fn() -> u32{r: r > 0})] fn frequency() -> u32 { 1_000_000 } @@ -437,6 +442,7 @@ impl Frequency for Freq1MHz { #[derive(Debug)] pub enum Freq32KHz {} impl Frequency for Freq32KHz { + #[flux_rs::sig(fn() -> u32{r: r > 0})] fn frequency() -> u32 { 32_768 } @@ -446,6 +452,7 @@ impl Frequency for Freq32KHz { #[derive(Debug)] pub enum Freq16KHz {} impl Frequency for Freq16KHz { + #[flux_rs::sig(fn() -> u32{r: r > 0})] fn frequency() -> u32 { 16_000 } @@ -455,6 +462,7 @@ impl Frequency for Freq16KHz { #[derive(Debug)] pub enum Freq1KHz {} impl Frequency for Freq1KHz { + #[flux_rs::sig(fn() -> u32{r: r > 0})] fn frequency() -> u32 { 1_000 } diff --git a/kernel/src/processbuffer.rs b/kernel/src/processbuffer.rs index 074bb8a8d2..3020726d50 100644 --- a/kernel/src/processbuffer.rs +++ b/kernel/src/processbuffer.rs @@ -868,7 +868,8 @@ impl Index for ReadableProcessSlice { // Cell to read-only operations type Output = ReadableProcessByte; - #[flux_rs::sig(fn(self: &ReadableProcessSlice[@len], idx: usize) -> &Self::Output requires len > idx)] + #[flux_rs::trusted_impl] + #[flux_rs::sig(fn(self: &ReadableProcessSlice[@len], idx: usize ) -> &Self::Output requires len > idx)] fn index(&self, idx: usize) -> &Self::Output { // As ReadableProcessSlice is a transparent wrapper around its // inner type, [ReadableProcessByte], we can use the regular @@ -1108,6 +1109,7 @@ impl Index for WriteableProcessSlice { // mutating the memory contents is allowed. type Output = Cell; + #[flux_rs::trusted_impl] #[flux_rs::sig(fn(self: &WriteableProcessSlice[@len], idx: usize) -> &Self::Output requires len > idx)] fn index(&self, idx: usize) -> &Self::Output { // As WriteableProcessSlice is a transparent wrapper around diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 00e595944e..93922b8928 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,8 +1,3 @@ -# Licensed under the Apache License, Version 2.0 or the MIT License. -# SPDX-License-Identifier: Apache-2.0 OR MIT -# Copyright Tock Contributors 2023. - [toolchain] -channel = "nightly-2024-07-08" -components = ["miri", "llvm-tools", "rust-src", "rustfmt", "clippy"] -targets = ["thumbv6m-none-eabi", "thumbv7em-none-eabi", "thumbv7em-none-eabihf", "riscv32imc-unknown-none-elf", "riscv32imac-unknown-none-elf"] +channel = "nightly-2024-08-20" +components = ["rust-src", "rustc-dev", "llvm-tools", "rustfmt"] From bddd61e330ed6ad8e4c7f07db7b612b4921e1930 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 29 Oct 2024 10:34:53 -0700 Subject: [PATCH 2/4] add test for trusted_impl --- kernel/Cargo.toml | 3 +-- rust-toolchain.toml | 9 +++++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml index 25194cf6f1..db97ff0dfc 100644 --- a/kernel/Cargo.toml +++ b/kernel/Cargo.toml @@ -16,8 +16,7 @@ tock-registers = { path = "../libraries/tock-register-interface" } tock-cells = { path = "../libraries/tock-cells" } tock-tbf = { path = "../libraries/tock-tbf" } flux_support = { path = "../flux_support" } -# flux-rs = { git = "https://github.com/flux-rs/flux.git" } -flux-rs = { path = "../../flux/lib/flux-rs" } +flux-rs = { git = "https://github.com/flux-rs/flux.git" } # In general, Tock discourages the use of cargo features. However for certain # kernel crate configuration, we have not found reasonable alternatives to diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 93922b8928..00e595944e 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,8 @@ +# Licensed under the Apache License, Version 2.0 or the MIT License. +# SPDX-License-Identifier: Apache-2.0 OR MIT +# Copyright Tock Contributors 2023. + [toolchain] -channel = "nightly-2024-08-20" -components = ["rust-src", "rustc-dev", "llvm-tools", "rustfmt"] +channel = "nightly-2024-07-08" +components = ["miri", "llvm-tools", "rust-src", "rustfmt", "clippy"] +targets = ["thumbv6m-none-eabi", "thumbv7em-none-eabi", "thumbv7em-none-eabihf", "riscv32imc-unknown-none-elf", "riscv32imac-unknown-none-elf"] From aaf124d1718b61e8c2b60e8914bf15dc30a88ec4 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Wed, 30 Oct 2024 11:01:36 -0700 Subject: [PATCH 3/4] passes `trait` branch non-debug build --- kernel/Cargo.toml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml index db97ff0dfc..25194cf6f1 100644 --- a/kernel/Cargo.toml +++ b/kernel/Cargo.toml @@ -16,7 +16,8 @@ tock-registers = { path = "../libraries/tock-register-interface" } tock-cells = { path = "../libraries/tock-cells" } tock-tbf = { path = "../libraries/tock-tbf" } flux_support = { path = "../flux_support" } -flux-rs = { git = "https://github.com/flux-rs/flux.git" } +# flux-rs = { git = "https://github.com/flux-rs/flux.git" } +flux-rs = { path = "../../flux/lib/flux-rs" } # In general, Tock discourages the use of cargo features. However for certain # kernel crate configuration, we have not found reasonable alternatives to From 6418445f414b30ef5d1230288aac5173eb3c4792 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Wed, 30 Oct 2024 11:02:12 -0700 Subject: [PATCH 4/4] passes `trait` branch non-debug build --- kernel/Cargo.toml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml index 25194cf6f1..db97ff0dfc 100644 --- a/kernel/Cargo.toml +++ b/kernel/Cargo.toml @@ -16,8 +16,7 @@ tock-registers = { path = "../libraries/tock-register-interface" } tock-cells = { path = "../libraries/tock-cells" } tock-tbf = { path = "../libraries/tock-tbf" } flux_support = { path = "../flux_support" } -# flux-rs = { git = "https://github.com/flux-rs/flux.git" } -flux-rs = { path = "../../flux/lib/flux-rs" } +flux-rs = { git = "https://github.com/flux-rs/flux.git" } # In general, Tock discourages the use of cargo features. However for certain # kernel crate configuration, we have not found reasonable alternatives to