Add extern specs for all core functions used by ring buffer

crates/flux-bin/src/lib.rs

@@ -30,7 +30,7 @@ pub struct FluxMetadata {
     /// relative to the location of the manifest file.
     pub include: Option<Vec<String>>,
     /// If present, every function in the module is implicitly labeled with a `no_panic` by default.
-    /// This means that the only way a function can panic is (1) if it panics, or (2) it calls an external function without this attribute.
+    /// This means that the only way a function can panic is if it calls an external function without this attribute.
     pub no_panic: Option<bool>,
 }
 

lib/flux-core/src/lib.rs

@@ -17,6 +17,9 @@ mod clone;
 #[cfg(flux)]
 mod slice;
 
+#[cfg(flux)]
+mod num;
+
 // -------------------------------------------------------------------
 
 #[macro_export]

lib/flux-core/src/num/mod.rs

@@ -0,0 +1,7 @@
+use flux_attrs::*;
+
+#[extern_spec(core::num)]
+impl usize {
+    #[no_panic]
+    fn saturating_sub(self, other: usize) -> usize;
+}

lib/flux-core/src/slice/index.rs

@@ -11,6 +11,7 @@ impl<T, I: SliceIndex<[T]>> ops::Index<I> for [T] {
         }
     )]
 
+    #[no_panic]
     #[sig(fn(&Self[@len], {I[@idx] | <Self as ops::Index<I>>::in_bounds(len, idx)}) -> &I::Output)]
     fn index(&self, index: I) -> &I::Output;
 }

lib/flux-core/src/slice/mod.rs

@@ -5,6 +5,7 @@ use flux_attrs::*;
 
 #[extern_spec(core::slice)]
 impl<T> [T] {
+    #[no_panic]
     #[sig(fn(&Self[@n]) -> usize[n])]
     fn len(&self) -> usize;
 
@@ -16,6 +17,10 @@ impl<T> [T] {
 
     #[sig(fn(&Self[@n]) -> Iter<T>[0, n])]
     fn iter(&self) -> Iter<'_, T>;
+
+    #[no_panic]
+    #[sig(fn(&Self[@n], mid: usize{mid <= n}) -> (&[T][mid], &[T][n - mid]))]
+    fn split_at(&self, mid: usize) -> (&[T], &[T]);
 }
 
 #[cfg(flux_sysroot_test)]

tests/tests/pos/surface/no_panic04.rs

@@ -0,0 +1,22 @@
+trait MyTrait {
+    fn f1(&self) -> usize;
+    fn f2(&self) -> usize;
+}
+
+struct MyImpl {}
+
+impl MyTrait for MyImpl {
+    #[flux_rs::no_panic]
+    fn f1(&self) -> usize {
+        self.f2()
+    }
+    #[flux_rs::no_panic]
+    fn f2(&self) -> usize {
+        2
+    }
+}
+
+#[flux_rs::no_panic]
+fn test00(x: &MyImpl) -> usize {
+    x.f1() + x.f2()
+}