peel back ignores and trusted

PLSysSec · Jul 24, 2024 · 4ae65cb · 4ae65cb
1 parent 5d8862f
commit 4ae65cb
Show file tree

Hide file tree

Showing 6 changed files with 9 additions and 13 deletions.
diff --git a/kernel/src/hil/mod.rs b/kernel/src/hil/mod.rs
@@ -9,6 +9,7 @@ pub mod analog_comparator;
 pub mod ble_advertising;
 pub mod bus8080;
 pub mod buzzer;
+#[flux::ignore]
 pub mod can;
 pub mod crc;
 pub mod dac;
@@ -17,14 +18,17 @@ pub mod digest;
 pub mod eic;
 pub mod entropy;
 pub mod flash;
+#[flux::ignore]
 pub mod gpio;
 pub mod gpio_async;
 pub mod hasher;
 pub mod i2c;
 pub mod kv;
+#[flux::ignore]
 pub mod led;
 pub mod log;
 pub mod nonvolatile_storage;
+#[flux::ignore]
 pub mod public_key_crypto;
 pub mod pwm;
 pub mod radio;
@@ -34,6 +38,7 @@ pub mod sensors;
 pub mod spi;
 pub mod symmetric_encryption;
 pub mod text_screen;
+#[flux::ignore]
 pub mod time;
 pub mod touch;
 pub mod uart;

diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs
@@ -113,43 +113,32 @@ pub mod deferred_call;
 pub mod errorcode;
 #[flux::trusted]
 pub mod grant;
-#[flux::ignore]
 pub mod hil;
-#[flux::ignore]
 pub mod introspection;
 #[flux::trusted]
 pub mod ipc;
 pub mod platform;
-// #[flux::ignore]
 pub mod process;
 #[flux::ignore]
 pub mod process_checker;
-// #[flux::ignore]
 pub mod processbuffer;
 #[flux::ignore]
 pub mod scheduler;
 pub mod storage_permissions;
-// #[flux::ignore]
 pub mod syscall;
-// #[flux::ignore]
 pub mod upcall;
 pub mod utilities;
 
 mod config;
-// #[flux::ignore]
 mod kernel;
 mod memop;
-#[flux::ignore]
 mod process_binary;
 #[flux::ignore]
 mod process_loading;
-#[flux::ignore]
 mod process_policies;
-#[flux::ignore]
 mod process_printer;
 #[flux::ignore]
 mod process_standard;
-// #[flux::ignore]
 mod syscall_driver;
 
 // Core resources exposed as `kernel::Type`.

diff --git a/kernel/src/process_binary.rs b/kernel/src/process_binary.rs
@@ -126,6 +126,7 @@ pub struct ProcessBinary {
 }
 
 impl ProcessBinary {
+    #[flux::trusted]
     pub(crate) fn create(
         app_flash: &'static [u8],
         header_length: usize,

diff --git a/kernel/src/process_printer.rs b/kernel/src/process_printer.rs
@@ -98,6 +98,7 @@ impl ProcessPrinter for ProcessPrinterText {
     //    being duplicated. However, it does not make sense that the kernel
     //    would want to run the process while it is displaying debugging
     //    information about it, so this should be a safe assumption.
+    #[flux::trusted]
     fn print_overview(
         &self,
         process: &dyn Process,

diff --git a/kernel/src/utilities/binary_write.rs b/kernel/src/utilities/binary_write.rs
@@ -94,6 +94,7 @@ impl<'a> WriteToBinaryOffsetWrapper<'a> {
 }
 
 impl<'a> core::fmt::Write for WriteToBinaryOffsetWrapper<'a> {
+    #[flux::trusted]
     fn write_str(&mut self, s: &str) -> core::fmt::Result {
         let string_len = s.len();
         if self.index + string_len < self.offset {

diff --git a/kernel/src/utilities/mod.rs b/kernel/src/utilities/mod.rs
@@ -3,14 +3,13 @@
 // Copyright Tock Contributors 2022.
 
 //! Utility functions and macros provided by the kernel crate.
-#[flux::ignore]
+// #[flux::ignore]
 pub mod binary_write;
 pub mod copy_slice;
 pub mod helpers;
 pub mod leasable_buffer;
 pub mod math;
 pub mod mut_imut_buffer;
-#[flux::ignore]
 pub mod peripheral_management;
 pub mod static_init;
 pub mod storage_volume;