Add extern specs to Tock to make 6 drivers panic free

capsules/core/Cargo.toml

@@ -12,10 +12,12 @@ edition.workspace = true
 kernel = { path = "../../kernel" }
 enum_primitive = { path = "../../libraries/enum_primitive" }
 tickv = { path = "../../libraries/tickv" }
+flux-rs = { git  = "https://github.com/flux-rs/flux.git" }
 
 [package.metadata.flux]
 enabled = true
 check_overflow = "lazy"
+no_panic = true
 include = [ "src/button.rs", "src/led.rs", "src/console.rs", "src/alarm.rs", "src/spi_peripheral.rs", "src/stream.rs"  ]
 
 [lints]

capsules/core/src/alarm.rs

@@ -9,6 +9,7 @@ use kernel::grant::{AllowRoCount, AllowRwCount, Grant, UpcallCount};
 use kernel::hil::time::{self, Alarm, Ticks};
 use kernel::syscall::{CommandReturn, SyscallDriver};
 use kernel::{ErrorCode, ProcessId};
+use kernel::process;
 
 /// Syscall driver number.
 use crate::driver;
@@ -76,6 +77,8 @@ impl<'a, A: Alarm<'a>> AlarmDriver<'a, A> {
     /// To stop iteration on any expired [`Expiration`], its callback can return
     /// `Some(R)`. Then this function will return `Err(Expiration, UD, R)`.
     /// This avoids consuming the entire iterator.
+    #[flux_rs::no_panic]
+    #[flux_rs::trusted] // Andrew note: trusted because of closure usage
     fn earliest_alarm<UD, R, F: FnOnce(Expiration<A::Ticks>, &UD) -> Option<R>>(
         now: A::Ticks,
         expirations: impl Iterator<Item = (Expiration<A::Ticks>, UD, F)>,
@@ -150,6 +153,8 @@ impl<'a, A: Alarm<'a>> AlarmDriver<'a, A> {
     /// - invoke upcalls for all expired app alarms, resetting them afterwards,
     /// - re-arming the alarm for the next earliest [`Expiration`], or
     /// - disarming the alarm if no unexpired [`Expiration`] is found.
+    #[flux_rs::no_panic]
+    #[flux_rs::trusted] // Andrew note: The `unreachable!()` here needs to be a refinement
     fn process_rearm_or_callback(&self) {
         // Ask the clock about a current reference once. This can incur a
         // volatile read, and this may not be optimized if done in a loop:
@@ -501,7 +506,7 @@ impl<'a, A: Alarm<'a>> SyscallDriver for AlarmDriver<'a, A> {
                 }
             })
             .map_or_else(
-                |err| CommandReturn::failure(err.into()),
+                |err: process::Error| CommandReturn::failure(err.into()),
                 |(retval, rearm_timer)| {
                     if rearm_timer {
                         self.process_rearm_or_callback();

flux_support/src/extern_specs/cell.rs

@@ -0,0 +1,28 @@
+use core::cell::Cell;
+
+#[flux_rs::extern_spec(core::cell)]
+struct Cell<T: ?Sized>;
+
+#[flux_rs::extern_spec(core::cell)]
+impl<T: Copy> Cell<T> {
+    #[flux_rs::no_panic]
+    fn get(&self) -> T;
+}
+
+#[flux_rs::extern_spec(core::cell)]
+impl<T> Cell<T> {
+    #[flux_rs::no_panic]
+    fn new(value: T) -> Cell<T>;
+
+    #[flux_rs::no_panic]
+    fn set(&self, value: T);
+
+    #[flux_rs::no_panic]
+    fn replace(&self, val: T) -> T;
+}
+
+#[flux_rs::extern_spec(core::cell)]
+impl<T: Default> Cell<T> {
+    #[flux_rs::no_panic]
+    fn take(&self) -> T;
+}

flux_support/src/extern_specs/cmp.rs

@@ -0,0 +1,7 @@
+#[flux_rs::extern_spec(core::cmp)]
+#[flux_rs::no_panic]
+fn min<T: Ord>(v1: T, v2: T) -> T;
+
+#[flux_rs::extern_spec(core::cmp)]
+#[flux_rs::no_panic]
+fn max<T: Ord>(v1: T, v2: T) -> T;

flux_support/src/extern_specs/default.rs

@@ -0,0 +1,5 @@
+#[flux_rs::extern_spec(core::default)]
+trait Default {
+    #[flux_rs::no_panic]
+    fn default() -> Self;
+}

flux_support/src/extern_specs/from.rs

@@ -0,0 +1,18 @@
+#[flux_rs::extern_spec(core::convert)]
+trait From<T>: Sized {
+    #[flux_rs::no_panic]
+    fn from(value: T) -> Self;
+}
+
+#[flux_rs::extern_spec(core::convert)]
+trait Into<T>: Sized {
+    #[flux_rs::no_panic]
+    fn into(self) -> T;
+}
+
+
+#[flux_rs::extern_spec(core::convert)]
+impl<T, U: From<T>> Into<U> for T {
+    #[flux_rs::no_panic]
+    fn into(self) -> U;
+}

flux_support/src/extern_specs/func.rs

@@ -0,0 +1,5 @@
+// #[flux_rs::extern_spec]
+// trait FnOnce<Args: Tuple> {
+//     #[flux_rs::no_panic]
+//     fn call_once(&self) -> Self::Output;
+// }

flux_support/src/extern_specs/iter.rs

@@ -1,27 +1,97 @@
 #![allow(unused)]
 use crate::assert;
-use core::slice::Iter;
+use core::iter::Enumerate;
+use core::iter::FilterMap;
+use core::iter::IntoIterator;
 
 #[flux_rs::extern_spec(core::slice)]
 #[flux_rs::refined_by(idx: int, len: int)]
 struct Iter<'a, T>;
 
+#[flux_rs::extern_spec]
+trait FromIterator<A> {}
+
+#[flux_rs::extern_spec(core::iter)]
+trait IntoIterator {
+    #[flux_rs::spec(fn(self: Self) -> Self::IntoIter)]
+    #[flux_rs::no_panic]
+    fn into_iter(self) -> Self::IntoIter
+    where
+        Self: Sized;
+}
+
+#[flux_rs::extern_spec(core::ops)]
+impl<I: Iterator> IntoIterator for I {
+    #[flux_rs::spec(fn(self: I[@s]) -> I[s])]
+    #[flux_rs::no_panic]
+    fn into_iter(self) -> I;
+}
+
 // #[flux_rs::extern_spec(std::iter)]
 // #[flux_rs::refined_by(idx: int, inner: I)]
 // struct Enumerate<I>;
 
 // #[flux_rs::extern_spec(std::iter)]
 // #[flux_rs::assoc(fn done(self: Self) -> bool )]
 // #[flux_rs::assoc(fn step(self: Self, other: Self) -> bool )]
-// trait Iterator {
-//     #[flux_rs::sig(fn(self: &strg Self[@curr_s]) -> Option<Self::Item>[!<Self as Iterator>::done(curr_s)] ensures self: Self{next_s: <Self as Iterator>::step(curr_s, next_s)})]
-//     fn next(&mut self) -> Option<Self::Item>;
-
-//     #[flux_rs::sig(fn(Self[@s]) -> Enumerate<Self>[0, s])]
-//     fn enumerate(self) -> Enumerate<Self>
-//     where
-//         Self: Sized;
-// }
+
+#[flux_rs::extern_spec(core::iter)]
+trait Iterator {
+    #[flux_rs::no_panic]
+    fn filter_map<B, F>(self, f: F) -> FilterMap<Self, F>
+    where
+        Self: Sized,
+        F: FnMut(Self::Item) -> Option<B>;
+
+    #[flux_rs::no_panic]
+    fn find_map<B, F>(&mut self, f: F) -> Option<B>
+    where
+        Self: Sized,
+        F: FnMut(Self::Item) -> Option<B>;
+
+    #[flux_rs::no_panic]
+    fn next(&mut self) -> Option<Self::Item>;
+
+    #[flux_rs::no_panic]
+    fn enumerate(self) -> Enumerate<Self>
+    where
+        Self: Sized;
+
+    #[flux_rs::no_panic]
+    fn rev(self) -> Rev<Self>
+    where
+        Self: Sized + DoubleEndedIterator;
+
+    #[flux_rs::no_panic]
+    fn take(self, n: usize) -> Take<Self>
+    where
+        Self: Sized;
+
+    #[flux_rs::no_panic]
+    fn zip<U>(self, other: U) -> Zip<Self, U::IntoIter>
+    where
+        Self: Sized,
+        U: IntoIterator;
+}
+
+#[flux_rs::extern_spec(core::iter)]
+struct Enumerate<I>;
+
+#[flux_rs::extern_spec(core::iter)]
+impl<I: Iterator> Iterator for Enumerate<I> {
+    // Andrew note: This indeed can panic!
+    // Don't merge until we create a refinement for this so that
+    // we can't call it unless we're sure it won't panic.
+    #[flux_rs::no_panic]
+    fn next(&mut self) -> Option<(usize, I::Item)>;
+}
+
+#[flux_rs::extern_spec(core::iter)]
+impl<A: Iterator, B: Iterator> Iterator for Zip<A, B> {
+    #[flux_rs::no_panic]
+    fn next(&mut self) -> Option<<Zip<A, B> as Iterator>::Item>;
+}
+
 
 // #[flux_rs::extern_spec(std::slice)]
 // #[flux_rs::assoc(fn done(x: Iter<T>) -> bool { x.idx >= x.len })]

flux_support/src/extern_specs/mem.rs

@@ -2,4 +2,11 @@
 // https://doc.rust-lang.org/reference/type-layout.html
 #[flux_rs::extern_spec(core::mem)]
 #[flux_rs::sig(fn<T>() -> usize{align: align > 0})]
+#[flux_rs::no_panic]
 fn align_of<T>() -> usize;
+
+
+
+#[flux_rs::extern_spec(core::mem)]
+#[flux_rs::no_panic]
+fn size_of<T>() -> usize;

flux_support/src/extern_specs/mod.rs

@@ -1,9 +1,16 @@
+mod cell;
+mod cmp;
+mod default;
+mod func;
+mod fmt;
+mod from;
 mod iter;
 mod mem;
 mod non_null;
 mod num;
 mod option;
 mod partial_cmp;
+mod ptr;
 mod range;
 mod result;
-mod slice;
+mod slice;

flux_support/src/extern_specs/num.rs

@@ -9,6 +9,12 @@ impl u32 {
 
     #[sig(fn(num: u32) -> u32{r: (num == 0 => r == 32) && (num != 0 =>r <= 31) })]
     fn trailing_zeros(self) -> u32;
+
+    #[flux_rs::no_panic]
+    fn saturating_sub(self, rhs: u32) -> u32;
+
+    #[flux_rs::no_panic]
+    fn from_be_bytes(bytes: [u8; 4]) -> u32;
 }
 
 #[flux_rs::extern_spec]

flux_support/src/extern_specs/option.rs

@@ -10,8 +10,41 @@ enum Option<T> {
 #[flux_rs::extern_spec]
 impl<T> Option<T> {
     #[sig(fn(&Option<T>[@b]) -> bool[b])]
+    #[flux_rs::no_panic]
     const fn is_some(&self) -> bool;
 
     #[sig(fn(&Option<T>[@b]) -> bool[!b])]
+    #[flux_rs::no_panic]
     const fn is_none(&self) -> bool;
+
+    #[flux_rs::no_panic]
+    fn map_or<U, F>(self, default: U, f: F) -> U
+    where
+        F: FnOnce(T) -> U;
+
+
+    #[flux_rs::no_panic]
+    fn map<U, F>(self, op: F) -> Option<U>
+    where
+        F: FnOnce(T) -> U;
+
+    #[flux_rs::no_panic]
+    fn inspect<F>(self, op: F) -> Self
+    where
+        F: FnOnce(&T);
+
+    #[flux_rs::no_panic]
+    fn unwrap_or_default(self) -> T
+    where
+        T: Default;
+
+    #[flux_rs::no_panic]
+    fn map_or_else<U, D, F>(self, default: D, f: F) -> U
+    where
+        // Andrew note: why does this not match up with source?
+        D: FnOnce() -> U,
+        F: FnOnce(T) -> U;
+
+    #[flux_rs::no_panic]
+    fn ok_or<E>(self, err: E) -> Result<T, E>;
 }

flux_support/src/extern_specs/partial_cmp.rs

@@ -2,10 +2,24 @@
 
 use core::cmp::PartialOrd;
 
-// #[flux_rs::extern_spec(core::cmp)]
-// #[flux_rs::assoc(fn lt(this: Self, other: Self) -> bool)]
-// #[flux_rs::assoc(fn le(this: Self, other: Self) -> bool)]
-// trait PartialOrd<Rhs: ?Sized = Self>: PartialEq<Rhs> {
-//     fn lt(&self, other: &Rhs) -> bool;
-//     fn le(&self, other: &Rhs) -> bool;
-// }
+#[flux_rs::extern_spec(core::cmp)]
+trait Ord {
+    #[flux_rs::no_panic]
+    fn min(self, other: Self) -> Self
+    where
+        Self: Sized;
+}
+
+#[flux_rs::extern_spec(core::cmp)]
+trait PartialOrd<Rhs: ?Sized = Self>: PartialEq<Rhs> {
+    #[flux_rs::no_panic]
+    fn lt(&self, other: &Rhs) -> bool;
+    fn le(&self, other: &Rhs) -> bool;
+}
+
+
+#[flux_rs::extern_spec(core::cmp)]
+trait PartialEq<Rhs: ?Sized = Self> {
+    #[flux_rs::no_panic]
+    fn eq(&self, other: &Rhs) -> bool;
+}

flux_support/src/extern_specs/ptr.rs

@@ -0,0 +1,15 @@
+use core::marker::PointeeSized;
+
+#[flux_rs::extern_spec(core::ptr)]
+impl<T: Sized> NonNull<T> {
+    #[flux_rs::no_panic]
+    fn as_ptr(self) -> *mut T;
+
+    #[flux_rs::no_panic]
+    fn cast<U>(self) -> NonNull<U>;
+}
+
+#[flux_rs::extern_spec(core::ptr)]
+#[flux_rs::no_panic]
+fn null_mut<T: PointeeSized + Thin>() -> *mut T;
+

flux_support/src/extern_specs/range.rs

@@ -1,7 +1,10 @@
 #![allow(unused)]
 
 use core::ops::Bound;
+use core::ops;
 use core::ops::{Range, RangeBounds};
+use core::iter::Step;
+
 
 #[flux_rs::extern_spec]
 #[flux_rs::refined_by(included: bool, unbounded: bool)]
@@ -54,6 +57,16 @@ trait RangeBounds<T> {
     // }
 }
 
+
+#[flux_rs::extern_spec(core::iter)]
+trait Step {}
+
+#[flux_rs::extern_spec(core::ops)]
+impl<A: core::iter::Step> Iterator for ops::Range<A> {
+    #[flux_rs::no_panic]
+    fn next(&mut self) -> Option<A>;
+}
+
 #[flux_rs::extern_spec(core::ops)]
 #[flux_rs::assoc(fn start(self: Range<T>) -> T { self.end })]
 #[flux_rs::assoc(fn end(self: Range<T>) -> T { self.end })]