From 4ae65cbaffccd5c6cb19809228ee86cb5b3b3a70 Mon Sep 17 00:00:00 2001
From: Evan Johnson <e5johnso@eng.ucsd.edu>
Date: Wed, 24 Jul 2024 10:51:05 -0700
Subject: [PATCH] peel back ignores and trusted

---
 kernel/src/hil/mod.rs                |  5 +++++
 kernel/src/lib.rs                    | 11 -----------
 kernel/src/process_binary.rs         |  1 +
 kernel/src/process_printer.rs        |  1 +
 kernel/src/utilities/binary_write.rs |  1 +
 kernel/src/utilities/mod.rs          |  3 +--
 6 files changed, 9 insertions(+), 13 deletions(-)

diff --git a/kernel/src/hil/mod.rs b/kernel/src/hil/mod.rs
index 0eb367d21a..5c9b32e02a 100644
--- 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
index 7f1f1cd167..c367f6644f 100644
--- 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
index e9597c18a5..9205f61b85 100644
--- 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
index 64a7a09d9e..1eca5fdf96 100644
--- 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
index 37a686246a..365d4c6222 100644
--- 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
index 883005abdf..66daaed217 100644
--- 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;