From be5b65c96a3b44be95709d68562bd5a6c45c95a3 Mon Sep 17 00:00:00 2001 From: Samir Rashid Date: Thu, 26 Sep 2024 23:28:10 +0000 Subject: [PATCH] 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,