From 66fa71a9ddfbf8c79b8d4a0918f3385852c0b5d7 Mon Sep 17 00:00:00 2001
From: Sangwan Kwon <sangwan.kwon@samsung.com>
Date: Tue, 19 Nov 2024 13:26:59 +0900
Subject: [PATCH] Fix build errors with kani

Signed-off-by: Sangwan Kwon <sangwan.kwon@samsung.com>
---
 rmm/src/monitor.rs | 11 +++++++++--
 rmm/src/rmi/rtt.rs |  3 +++
 2 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/rmm/src/monitor.rs b/rmm/src/monitor.rs
index 3d56964338b6..cd8c47cc517d 100644
--- a/rmm/src/monitor.rs
+++ b/rmm/src/monitor.rs
@@ -16,7 +16,10 @@ pub struct Monitor {
 #[cfg(kani)]
 // `rsi` and `page_table` are removed in model checking harnesses
 // to reduce overall state space
-pub struct Monitor {}
+pub struct Monitor {
+    pub rmi: RmiHandle,
+    mainloop: Mainloop,
+}
 
 impl Monitor {
     #[cfg(not(kani))]
@@ -31,7 +34,10 @@ impl Monitor {
 
     #[cfg(kani)]
     pub fn new() -> Self {
-        Self {}
+        Self {
+            rmi: RmiHandle::new(),
+            mainloop: Mainloop::new(),
+        }
     }
 
     #[cfg(not(kani))]
@@ -132,6 +138,7 @@ impl Monitor {
     }
 
     pub fn handle_rsi(&self, ctx: &mut Context, rec: &mut Rec<'_>, run: &mut Run) -> usize {
+        #[cfg(not(kani))]
         match self.rsi.on_event.get(&ctx.cmd) {
             Some(handler) => {
                 ctx.do_rsi(|arg, ret| handler(arg, ret, self, rec, run));
diff --git a/rmm/src/rmi/rtt.rs b/rmm/src/rmi/rtt.rs
index ee9a92ec90f4..5036ba817edc 100644
--- a/rmm/src/rmi/rtt.rs
+++ b/rmm/src/rmi/rtt.rs
@@ -56,6 +56,7 @@ pub fn set_event_handler(rmi: &mut RmiHandle) {
 
         // The below is added to avoid a fault regarding the RTT entry
         // during the `create_pgtbl_at()` in `rtt::create()`.
+        #[cfg(not(kani))]
         rmm.page_table.map(rtt_addr, true);
         rtt::create(&rd, rtt_addr, ipa, level)?;
         set_granule(&mut rtt_granule, GranuleState::RTT)?;
@@ -197,8 +198,10 @@ pub fn set_event_handler(rmi: &mut RmiHandle) {
         rmm.page_table.map(target_pa, true);
 
         // copy src to target
+        #[cfg(not(kani))]
         rmm.page_table.map(src_pa, false);
         host::copy_to_obj::<DataPage>(src_pa, &mut target_page).ok_or(Error::RmiErrorInput)?;
+        #[cfg(not(kani))]
         rmm.page_table.unmap(src_pa);
 
         // map ipa to taget_pa in S2 table